Add array16_map primitive

Author: wezm

fathom/src/core.rs

@@ -367,6 +367,8 @@ def_prims! {
     FormatArray8 => "array8",
     /// Array formats, with unsigned 16-bit indices.
     FormatArray16 => "array16",
+    /// Map a function over an Array16
+    FormatArray16Map => "array16_map",
     /// Array formats, with unsigned 32-bit indices.
     FormatArray32 => "array32",
     /// Array formats, with unsigned 64-bit indices.

fathom/src/core/binary.rs

@@ -415,6 +415,7 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> {
             (Prim::FormatArray16, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
             (Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
             (Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
+            (Prim::FormatArray16Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array),
             (Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format),
             (Prim::FormatRepeatUntilFull, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format),
             (Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format),
@@ -458,6 +459,30 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> {
         Ok(Spanned::new(span, Arc::new(Value::ArrayLit(elem_exprs))))
     }
 
+    fn array_map(
+        &mut self,
+        reader: &mut BufferReader<'data>,
+        span: Span,
+        map_fn: &ArcValue<'arena>,
+        array: &ArcValue<'arena>,
+    ) -> Result<ArcValue<'arena>, ReadError<'arena>> {
+        let array = self.elim_env().force(array);
+        let array = match array.as_ref() {
+            Value::ArrayLit(ary) => ary,
+            _ => return Err(ReadError::InvalidValue(array.span())),
+        };
+
+        let elem_exprs = array
+            .iter()
+            .map(|elem| {
+                let elem_format = self.elim_env().fun_app(map_fn.clone(), elem.clone());
+                self.read_format(reader, &elem_format)
+            })
+            .collect::<Result<_, _>>()?;
+
+        Ok(Spanned::new(span, Arc::new(Value::ArrayLit(elem_exprs))))
+    }
+
     fn read_repeat_until_end(
         &mut self,
         reader: &mut BufferReader<'data>,

fathom/src/core/semantics.rs

@@ -844,6 +844,9 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
                 (Prim::FormatArray16, [Elim::FunApp(len), Elim::FunApp(elem)]) => {
                     Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(elem)])
                 }
+                (Prim::FormatArray16Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => {
+                    Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(map_fn)])
+                }
                 (Prim::FormatArray32, [Elim::FunApp(len), Elim::FunApp(elem)]) => {
                     Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(elem)])
                 }

fathom/src/surface/elaboration.rs

@@ -186,6 +186,39 @@ impl<'arena> RigidEnv<'arena> {
         env.define_prim_fun(FormatArray16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
         env.define_prim_fun(FormatArray32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
         env.define_prim_fun(FormatArray64, [&U64_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
+        // (A@0 -> Format)
+        let map_fn = Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE);
+        // Array16 len@2 A@1
+        let array_ty = Term::FunApp(
+            Span::Empty,
+            scope.to_scope(Term::FunApp(Span::Empty, &ARRAY16_TYPE, &VAR2)),
+            &VAR1,
+        );
+        // array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format;
+        env.define_prim(
+            FormatArray16Map,
+            scope.to_scope(Term::FunType(
+                Span::Empty,
+                env.name("len"),
+                &U16_TYPE,
+                scope.to_scope(Term::FunType(
+                    Span::Empty,
+                    env.name("A"),
+                    &UNIVERSE,
+                    scope.to_scope(Term::FunType(
+                        Span::Empty,
+                        None,
+                        scope.to_scope(map_fn),
+                        scope.to_scope(Term::FunType(
+                            Span::Empty,
+                            None,
+                            scope.to_scope(array_ty),
+                            &FORMAT_TYPE,
+                        )),
+                    )),
+                )),
+            )),
+        );
         env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE);
         // repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format
         env.define_prim(

tests/succeed/primitives.fathom

@@ -61,6 +61,7 @@ let _ = array8 : U8 -> Format -> Format;
 let _ = array16 : U16 -> Format -> Format;
 let _ = array32 : U32 -> Format -> Format;
 let _ = array64 : U64 -> Format -> Format;
+let _ = array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format;
 let _ = link : Pos -> Format -> Format;
 let _ = deref : fun (f : Format) -> Ref f -> Format;
 let _ = stream_pos : Format;