Add array*_index function

Author: wezm

doc/reference.md

@@ -994,11 +994,29 @@ fixed-length array type.
 
 The following operations are defined on arrays:
 
+#### find
+
+`array*_find` takes a function that returns true or false. It applies this
+function to each element of the array. If the function returns true, then
+`array*_find` returns `some element`. If they all return false, it returns
+`none`.
+
 - `array8_find : fun (len : U8) -> fun (A : Type) -> (A -> Bool) -> Array8 len A -> Option A`
 - `array16_find : fun (len : U16) -> fun (A : Type) -> (A -> Bool) -> Array16 len A -> Option A`
 - `array32_find : fun (len : U32) -> fun (A : Type) -> (A -> Bool) -> Array32 len A -> Option A`
 - `array64_find : fun (len : U64) -> fun (A : Type) -> (A -> Bool) -> Array64 len A -> Option A`
 
+#### index
+
+`array*_index` returns the item at the supplied index in the array. The
+operation will not evaluate fully if the index is out of bounds. If this
+happens when parsing a binary format, a parse failure will be triggered.
+
+- `array8_index : fun (len : U8) -> fun (A : Type) -> fun (index : U8) -> Array8 len A -> A`
+- `array16_index : fun (len : U16) -> fun (A : Type) -> fun (index : U16) -> Array16 len A -> A`
+- `array32_index : fun (len : U32) -> fun (A : Type) -> fun (index : U32) -> Array32 len A -> A`
+- `array64_index : fun (len : U64) -> fun (A : Type) -> fun (index : U64) -> Array64 len A -> A`
+
 ## Positions
 
 Position types represent locations in the binary stream, relative to the

fathom/src/core.rs

@@ -493,6 +493,11 @@ def_prims! {
     Array32Find => "array32_find",
     Array64Find => "array64_find",
 
+    Array8Index => "array8_index",
+    Array16Index => "array16_index",
+    Array32Index => "array32_index",
+    Array64Index => "array64_index",
+
     PosAddU8  => "pos_add_u8",
     PosAddU16 => "pos_add_u16",
     PosAddU32 => "pos_add_u32",

fathom/src/core/semantics.rs

@@ -598,6 +598,22 @@ fn prim_step(prim: Prim) -> Option<PrimStep> {
             })
         }
 
+        Prim::Array8Index | Prim::Array16Index | Prim::Array32Index | Prim::Array64Index => {
+            step!(_context, [_, _, index, array] => match array.as_ref() {
+                Value::ArrayLit(elems) => {
+                    let index = match (index).as_ref() {
+                        Value::ConstLit(Const::U8(index, _)) => Some(usize::from(*index)),
+                        Value::ConstLit(Const::U16(index, _)) => Some(usize::from(*index)),
+                        Value::ConstLit(Const::U32(index, _)) => usize::try_from(*index).ok(),
+                        Value::ConstLit(Const::U64(index, _)) => usize::try_from(*index).ok(),
+                        _ => return None,
+                    }?;
+                    elems.get(index).cloned()?
+                }
+                _ => return None,
+            })
+        }
+
         Prim::PosAddU8 => const_step!([x: Pos, y: U8] => Const::Pos(usize::checked_add(*x, usize::from(*y))?)),
         Prim::PosAddU16 => const_step!([x: Pos, y: U16] => Const::Pos(usize::checked_add(*x, usize::from(*y))?)),
         Prim::PosAddU32 => const_step!([x: Pos, y: U32] => Const::Pos(usize::checked_add(*x, usize::try_from(*y).ok()?)?)),

fathom/src/surface/elaboration.rs

@@ -468,6 +468,45 @@ impl<'arena> RigidEnv<'arena> {
         env.define_prim(Array32Find, array32_find_type);
         env.define_prim(Array64Find, array64_find_type);
 
+        // fun (len : UN) -> (A : Type) -> (index : UN) -> ArrayN len   A   -> A
+        // fun (len : UN) -> (A : Type) -> (index : UN) -> ArrayN len@2 A@1 -> A@2
+        let array_index_type = |index_type, array_type| {
+            scope.to_scope(core::Term::FunType(
+                Span::Empty,
+                env.name("len"),
+                index_type,
+                scope.to_scope(core::Term::FunType(
+                    Span::Empty,
+                    env.name("A"),
+                    &UNIVERSE,
+                    scope.to_scope(core::Term::FunType(
+                        Span::Empty,
+                        env.name("index"),
+                        &index_type,
+                        scope.to_scope(core::Term::FunType(
+                            Span::Empty,
+                            None,
+                            // ArrayN len@2 A@1
+                            scope.to_scope(Term::FunApp(
+                                Span::Empty,
+                                scope.to_scope(Term::FunApp(Span::Empty, array_type, &VAR2)),
+                                &VAR1,
+                            )),
+                            &VAR2, // A@2
+                        )),
+                    )),
+                )),
+            ))
+        };
+        let array8_index_type = array_index_type(&U8_TYPE, &ARRAY8_TYPE);
+        let array16_index_type = array_index_type(&U16_TYPE, &ARRAY16_TYPE);
+        let array32_index_type = array_index_type(&U32_TYPE, &ARRAY32_TYPE);
+        let array64_index_type = array_index_type(&U64_TYPE, &ARRAY64_TYPE);
+        env.define_prim(Array8Index, array8_index_type);
+        env.define_prim(Array16Index, array16_index_type);
+        env.define_prim(Array32Index, array32_index_type);
+        env.define_prim(Array64Index, array64_index_type);
+
         env.define_prim_fun(PosAddU8, [&POS_TYPE, &U8_TYPE], &POS_TYPE);
         env.define_prim_fun(PosAddU16, [&POS_TYPE, &U16_TYPE], &POS_TYPE);
         env.define_prim_fun(PosAddU32, [&POS_TYPE, &U32_TYPE], &POS_TYPE);

formats/data/opentype/woff/valid-005.snap

@@ -756,6 +756,8 @@ stdout = '''
                         end_pts_of_contours = [ 7, 17, 23, 27, 30 ],
                         instruction_length = 0,
                         instructions = [],
+                        last_end_point_index = 30,
+                        number_of_coords = 31,
                     },
                 },
             ],

formats/opentype.fathom

@@ -2801,6 +2801,8 @@ def simple_glyph = fun (number_of_contours : U16) => {
     instruction_length <- u16be,
     /// Array of instruction byte code for the glyph.
     instructions <- array16 instruction_length u8,
+    let last_end_point_index = array16_index _ _ (number_of_contours - (1 : U16)) end_pts_of_contours,
+    let number_of_coords = last_end_point_index + (1 : U16),
     /// Array of flag elements.
     // flags[variable] <- uint8,
     /// xCoordinates[variable] 	Contour point x-coordinates. Coordinate for the first point is relative to (0,0);

formats/opentype.snap

@@ -384,6 +384,9 @@ def simple_glyph : U16 -> Format = fun number_of_contours => {
     end_pts_of_contours <- array16 number_of_contours u16be,
     instruction_length <- u16be,
     instructions <- array16 instruction_length u8,
+    let last_end_point_index : U16 = array16_index (_ number_of_contours end_pts_of_contours instruction_length instructions) (_ number_of_contours end_pts_of_contours instruction_length instructions) (number_of_contours - (1 :
+    U16)) end_pts_of_contours,
+    let number_of_coords : U16 = last_end_point_index + (1 : U16),
 };
 def glyph : Format = {
     header <- glyph_header,

tests/succeed/primitives.fathom

@@ -208,6 +208,11 @@ let _ = array16_find : fun (len : U16) -> fun (A : Type) -> (A -> Bool) -> Array
 let _ = array32_find : fun (len : U32) -> fun (A : Type) -> (A -> Bool) -> Array32 len A -> Option A;
 let _ = array64_find : fun (len : U64) -> fun (A : Type) -> (A -> Bool) -> Array64 len A -> Option A;
 
+let _ = array8_index : fun (len : U8) -> fun (A : Type) -> U8 -> Array8 len A -> A;
+let _ = array16_index : fun (len : U16) -> fun (A : Type) -> U16 -> Array16 len A -> A;
+let _ = array32_index : fun (len : U32) -> fun (A : Type) -> U32 -> Array32 len A -> A;
+let _ = array64_index : fun (len : U64) -> fun (A : Type) -> U64 -> Array64 len A -> A;
+
 let _ = pos_add_u8 : Pos -> U8 -> Pos;
 let _ = pos_add_u16 : Pos -> U16 -> Pos;
 let _ = pos_add_u32 : Pos -> U32 -> Pos;

tests/succeed/primitives.snap

@@ -193,6 +193,10 @@ let _ : _ = array8_find;
 let _ : _ = array16_find;
 let _ : _ = array32_find;
 let _ : _ = array64_find;
+let _ : _ = array8_index;
+let _ : _ = array16_index;
+let _ : _ = array32_index;
+let _ : _ = array64_index;
 let _ : _ = pos_add_u8;
 let _ : _ = pos_add_u16;
 let _ : _ = pos_add_u32;