Skip to content

Commit 7b68e75

Browse files
wezmwezm
committed
Add array{8,32,64}_map
1 parent 0f3c9b7 commit 7b68e75

File tree

5 files changed

+49
-19
lines changed

5 files changed

+49
-19
lines changed

‎fathom/src/core.rs‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -367,12 +367,18 @@ def_prims! {
367367
FormatArray8 => "array8",
368368
/// Array formats, with unsigned 16-bit indices.
369369
FormatArray16 => "array16",
370-
/// Map a function over an Array16
371-
FormatArray16Map => "array16_map",
372370
/// Array formats, with unsigned 32-bit indices.
373371
FormatArray32 => "array32",
374372
/// Array formats, with unsigned 64-bit indices.
375373
FormatArray64 => "array64",
374+
/// Map a function over an Array8
375+
FormatArray8Map => "array8_map",
376+
/// Map a function over an Array16
377+
FormatArray16Map => "array16_map",
378+
/// Map a function over an Array32
379+
FormatArray32Map => "array32_map",
380+
/// Map a function over an Array64
381+
FormatArray64Map => "array64_map",
376382
/// Repeat a format until the length of the given parse scope is reached.
377383
FormatRepeatUntilEnd => "repeat_until_end",
378384
/// Repeat a format until the array is filled.

‎fathom/src/core/binary.rs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -415,7 +415,10 @@ impl<'arena, 'env, 'data> Context<'arena, 'env, 'data> {
415415
(Prim::FormatArray16, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
416416
(Prim::FormatArray32, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
417417
(Prim::FormatArray64, [FunApp(len), FunApp(format)]) => self.read_array(reader, span, len, format),
418+
(Prim::FormatArray8Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array),
418419
(Prim::FormatArray16Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array),
420+
(Prim::FormatArray32Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array),
421+
(Prim::FormatArray64Map, [_, _, FunApp(map_fn), FunApp(array)]) => self.array_map(reader, span, map_fn, array),
419422
(Prim::FormatRepeatUntilEnd, [FunApp(format)]) => self.read_repeat_until_end(reader, format),
420423
(Prim::FormatRepeatUntilFull, [FunApp(len), FunApp(format), FunApp(replicate)]) => self.read_repeat_until_full(reader, len, replicate, format),
421424
(Prim::FormatLimit8, [FunApp(limit), FunApp(format)]) => self.read_limit(reader, limit, format),

‎fathom/src/core/semantics.rs‎

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -842,15 +842,24 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
842842
(Prim::FormatArray16, [Elim::FunApp(len), Elim::FunApp(elem)]) => {
843843
Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(elem)])
844844
}
845-
(Prim::FormatArray16Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => {
846-
Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(map_fn)])
847-
}
848845
(Prim::FormatArray32, [Elim::FunApp(len), Elim::FunApp(elem)]) => {
849846
Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(elem)])
850847
}
851848
(Prim::FormatArray64, [Elim::FunApp(len), Elim::FunApp(elem)]) => {
852849
Value::prim(Prim::Array64Type, [len.clone(), self.format_repr(elem)])
853850
}
851+
(Prim::FormatArray8Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => {
852+
Value::prim(Prim::Array8Type, [len.clone(), self.format_repr(map_fn)])
853+
}
854+
(Prim::FormatArray16Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => {
855+
Value::prim(Prim::Array16Type, [len.clone(), self.format_repr(map_fn)])
856+
}
857+
(Prim::FormatArray32Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => {
858+
Value::prim(Prim::Array32Type, [len.clone(), self.format_repr(map_fn)])
859+
}
860+
(Prim::FormatArray64Map, [Elim::FunApp(len), _, Elim::FunApp(map_fn), _]) => {
861+
Value::prim(Prim::Array64Type, [len.clone(), self.format_repr(map_fn)])
862+
}
854863
(Prim::FormatLimit8, [_, Elim::FunApp(elem)]) => return self.format_repr(elem),
855864
(Prim::FormatLimit16, [_, Elim::FunApp(elem)]) => return self.format_repr(elem),
856865
(Prim::FormatLimit32, [_, Elim::FunApp(elem)]) => return self.format_repr(elem),

‎fathom/src/surface/elaboration.rs‎

Lines changed: 23 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -186,21 +186,20 @@ impl<'arena> RigidEnv<'arena> {
186186
env.define_prim_fun(FormatArray16, [&U16_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
187187
env.define_prim_fun(FormatArray32, [&U32_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
188188
env.define_prim_fun(FormatArray64, [&U64_TYPE, &FORMAT_TYPE], &FORMAT_TYPE);
189-
// (A@0 -> Format)
190-
let map_fn = Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE);
191-
// Array16 len@2 A@1
192-
let array_ty = Term::FunApp(
193-
Span::Empty,
194-
scope.to_scope(Term::FunApp(Span::Empty, &ARRAY16_TYPE, &VAR2)),
195-
&VAR1,
196-
);
197-
// array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format;
198-
env.define_prim(
199-
FormatArray16Map,
189+
let format_array_map = |index_type, array_type| {
190+
// (A@0 -> Format)
191+
let map_fn = Term::FunType(Span::Empty, None, &VAR0, &FORMAT_TYPE);
192+
// Array16 len@2 A@1
193+
let array_ty = Term::FunApp(
194+
Span::Empty,
195+
scope.to_scope(Term::FunApp(Span::Empty, array_type, &VAR2)),
196+
&VAR1,
197+
);
198+
// array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format;
200199
scope.to_scope(Term::FunType(
201200
Span::Empty,
202201
env.name("len"),
203-
&U16_TYPE,
202+
index_type,
204203
scope.to_scope(Term::FunType(
205204
Span::Empty,
206205
env.name("A"),
@@ -217,9 +216,19 @@ impl<'arena> RigidEnv<'arena> {
217216
)),
218217
)),
219218
)),
220-
)),
221-
);
219+
))
220+
};
221+
222+
let format_array8_map = format_array_map(&U8_TYPE, &ARRAY8_TYPE);
223+
let format_array16_map = format_array_map(&U16_TYPE, &ARRAY16_TYPE);
224+
let format_array32_map = format_array_map(&U32_TYPE, &ARRAY32_TYPE);
225+
let format_array64_map = format_array_map(&U64_TYPE, &ARRAY64_TYPE);
226+
env.define_prim(FormatArray8Map, &format_array8_map);
227+
env.define_prim(FormatArray16Map, &format_array16_map);
228+
env.define_prim(FormatArray32Map, &format_array32_map);
229+
env.define_prim(FormatArray64Map, &format_array64_map);
222230
env.define_prim_fun(FormatRepeatUntilEnd, [&FORMAT_TYPE], &FORMAT_TYPE);
231+
223232
// repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format
224233
env.define_prim(
225234
FormatRepeatUntilFull,

‎tests/succeed/primitives.fathom‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,10 @@ let _ = array8 : U8 -> Format -> Format;
6161
let _ = array16 : U16 -> Format -> Format;
6262
let _ = array32 : U32 -> Format -> Format;
6363
let _ = array64 : U64 -> Format -> Format;
64+
let _ = array8_map : fun (len : U8) -> fun (A : Type) -> (A -> Format) -> Array8 len A -> Format;
6465
let _ = array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format;
66+
let _ = array32_map : fun (len : U32) -> fun (A : Type) -> (A -> Format) -> Array32 len A -> Format;
67+
let _ = array64_map : fun (len : U64) -> fun (A : Type) -> (A -> Format) -> Array64 len A -> Format;
6568
let _ = link : Pos -> Format -> Format;
6669
let _ = deref : fun (f : Format) -> Ref f -> Format;
6770
let _ = stream_pos : Format;

0 commit comments

Comments
 (0)