Skip to content

Commit 2f753e1

Browse files
brendanzabbrendanzab
authored
Merge pull request #449 from brendanzab/implicit-prims
Use implicit parameters in primitives and opentype format
2 parents bb11994 + c5f9b4e commit 2f753e1

File tree

12 files changed

+246
-147
lines changed

12 files changed

+246
-147
lines changed

‎doc/reference.md‎

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -616,29 +616,29 @@ Links formats are [represented](#format-representations) as typed
616616
Deref formats allow [references](#references) to other parts of the stream to be
617617
included in resulting parsed output.
618618

619-
- `deref : fun (f : Format) -> Ref f -> Format`
619+
- `deref : fun (@f : Format) -> Ref f -> Format`
620620

621621
#### Representation of deref formats
622622

623623
Dereferences are [represented](#format-representations) after parsing using the
624624
representation of the referenced format.
625625

626-
| format | `Repr` format |
627-
| ------------------ | ------------- |
628-
| `deref format ref` | `Repr format` |
626+
| format | `Repr` format |
627+
| ------------------- | ------------- |
628+
| `deref @format ref` | `Repr format` |
629629

630630
### Succeed format
631631

632632
The succeed format consumes no input during parsing, allowing values to be
633633
embedded in the resulting parsed output.
634634

635-
- `succeed : fun (A : Type) -> A -> Format`
635+
- `succeed : fun (@A : Type) -> A -> Format`
636636

637637
#### Representation of succeed formats
638638

639-
| format | `Repr` format |
640-
| ------------- | ------------- |
641-
| `succeed A a` | `A` |
639+
| format | `Repr` format |
640+
| -------------- | ------------- |
641+
| `succeed @A a` | `A` |
642642

643643
### Fail format
644644

@@ -661,13 +661,13 @@ The unwrap format consumes no input during parsing, succeeding with the data
661661
contained in a the `some` case of an [option](#options), or otherwise causing a
662662
parse failure.
663663

664-
- `unwrap : fun (A : Type) -> Option A -> Format`
664+
- `unwrap : fun (@A : Type) -> Option A -> Format`
665665

666666
#### Representation of unwrap formats
667667

668-
| format | `Repr` format |
669-
| ------------------- | ------------- |
670-
| `unwrap A option_a` | `A` |
668+
| format | `Repr` format |
669+
| -------------------- | ------------- |
670+
| `unwrap @A option_a` | `A` |
671671

672672
## Functions
673673

@@ -1082,14 +1082,14 @@ Data that may not be present can be formed with the following primitive:
10821082

10831083
Optional data can be introduced with the `some` or `none` primitives:
10841084

1085-
- `some : fun (A : Type) -> A -> Option A`
1086-
- `none : fun (A : Type) -> Option A`
1085+
- `some : fun (@A : Type) -> A -> Option A`
1086+
- `none : fun (@A : Type) -> Option A`
10871087

10881088
### Option operations
10891089

10901090
The following operations are defined for option types:
10911091

1092-
- `option_fold : fun (A : Type) (B : Type) -> B -> (A -> B) -> Option A -> B`
1092+
- `option_fold : fun (@A : Type) (@B : Type) -> B -> (A -> B) -> Option A -> B`
10931093

10941094
## Arrays
10951095

@@ -1139,21 +1139,21 @@ function to each element of the array. If the function returns true, then
11391139
`array*_find` returns `some element`. If they all return false, it returns
11401140
`none`.
11411141

1142-
- `array8_find : fun (len : U8) (A : Type) -> (A -> Bool) -> Array8 len A -> Option A`
1143-
- `array16_find : fun (len : U16) (A : Type) -> (A -> Bool) -> Array16 len A -> Option A`
1144-
- `array32_find : fun (len : U32) (A : Type) -> (A -> Bool) -> Array32 len A -> Option A`
1145-
- `array64_find : fun (len : U64) (A : Type) -> (A -> Bool) -> Array64 len A -> Option A`
1142+
- `array8_find : fun (@len : U8) (@A : Type) -> (A -> Bool) -> Array8 len A -> Option A`
1143+
- `array16_find : fun (@len : U16) (@A : Type) -> (A -> Bool) -> Array16 len A -> Option A`
1144+
- `array32_find : fun (@len : U32) (@A : Type) -> (A -> Bool) -> Array32 len A -> Option A`
1145+
- `array64_find : fun (@len : U64) (@A : Type) -> (A -> Bool) -> Array64 len A -> Option A`
11461146

11471147
#### index
11481148

11491149
`array*_index` returns the item at the supplied index in the array. The
11501150
operation will not evaluate fully if the index is out of bounds. If this
11511151
happens when parsing a binary format, a parse failure will be triggered.
11521152

1153-
- `array8_index : fun (len : U8) (A : Type) (index : U8) -> Array8 len A -> A`
1154-
- `array16_index : fun (len : U16) (A : Type) (index : U16) -> Array16 len A -> A`
1155-
- `array32_index : fun (len : U32) (A : Type) (index : U32) -> Array32 len A -> A`
1156-
- `array64_index : fun (len : U64) (A : Type) (index : U64) -> Array64 len A -> A`
1153+
- `array8_index : fun (@len : U8) (@A : Type) (index : U8) -> Array8 len A -> A`
1154+
- `array16_index : fun (@len : U16) (@A : Type) (index : U16) -> Array16 len A -> A`
1155+
- `array32_index : fun (@len : U32) (@A : Type) (index : U32) -> Array32 len A -> A`
1156+
- `array64_index : fun (@len : U64) (@A : Type) (index : U64) -> Array64 len A -> A`
11571157

11581158
## Positions
11591159

@@ -1195,4 +1195,4 @@ The void type is be used to mark terms that can never be constructed:
11951195

11961196
It can be eliminated by the `absurd` function:
11971197

1198-
- `absurd : fun (A : Type) -> Void -> A`
1198+
- `absurd : fun (@A : Type) -> Void -> A`

‎fathom/src/core/binary.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -440,8 +440,8 @@ impl<'arena, 'data> Context<'arena, 'data> {
440440
(Prim::FormatSucceed, [_, FunApp(_, elem)]) => Ok(elem.clone()),
441441
(Prim::FormatFail, []) => Err(ReadError::ReadFailFormat(span)),
442442
(Prim::FormatUnwrap, [_, FunApp(_, option)]) => match option.match_prim_spine() {
443-
Some((Prim::OptionSome, [FunApp(_, elem)])) => Ok(elem.clone()),
444-
Some((Prim::OptionNone, [])) => Err(ReadError::UnwrappedNone(span)),
443+
Some((Prim::OptionSome, [_, FunApp(_, elem)])) => Ok(elem.clone()),
444+
Some((Prim::OptionNone, [_])) => Err(ReadError::UnwrappedNone(span)),
445445
_ => Err(ReadError::InvalidValue(span)),
446446
},
447447
_ => Err(ReadError::InvalidFormat(span)),

‎fathom/src/core/prim.rs‎

Lines changed: 57 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use std::sync::Arc;
44
use fxhash::FxHashMap;
55
use scoped_arena::Scope;
66

7-
use crate::core::semantics::{ArcValue, Elim, ElimEnv, Value};
7+
use crate::core::semantics::{ArcValue, Elim, ElimEnv, Head, Value};
88
use crate::core::{self, Const, Plicity, Prim, UIntStyle};
99
use crate::env::{self, SharedEnv, UniqueEnv};
1010
use crate::source::{Span, Spanned, StringId, StringInterner};
@@ -58,17 +58,6 @@ impl<'arena> Env<'arena> {
5858
let mut env = EnvBuilder::new(interner, scope);
5959

6060
env.define_prim(VoidType, &UNIVERSE);
61-
// fun (A : Type) -> Void -> A
62-
env.define_prim(
63-
Absurd,
64-
&core::Term::FunType(
65-
Span::Empty,
66-
Plicity::Explicit,
67-
env.name("A"),
68-
&UNIVERSE,
69-
&core::Term::FunType(Span::Empty, Plicity::Explicit, None, &VOID_TYPE, &VAR1),
70-
),
71-
);
7261
env.define_prim(BoolType, &UNIVERSE);
7362
env.define_prim(U8Type, &UNIVERSE);
7463
env.define_prim(U16Type, &UNIVERSE);
@@ -122,8 +111,8 @@ impl<'arena> Env<'arena> {
122111
FormatDeref,
123112
&core::Term::FunType(
124113
Span::Empty,
125-
Plicity::Explicit,
126-
env.name("A"),
114+
Plicity::Implicit,
115+
env.name("f"),
127116
&FORMAT_TYPE,
128117
&Term::FunType(
129118
Span::Empty,
@@ -144,7 +133,7 @@ impl<'arena> Env<'arena> {
144133
FormatSucceed,
145134
&core::Term::FunType(
146135
Span::Empty,
147-
Plicity::Explicit,
136+
Plicity::Implicit,
148137
env.name("A"),
149138
&UNIVERSE,
150139
&Term::FunType(Span::Empty, Plicity::Explicit, None, &VAR0, &FORMAT_TYPE),
@@ -153,11 +142,11 @@ impl<'arena> Env<'arena> {
153142
env.define_prim(FormatFail, &FORMAT_TYPE);
154143
env.define_prim(
155144
FormatUnwrap,
156-
// fun (A : Type) -> Option A -> Format
157-
// fun (A : Type) -> Option A@0 -> Format
145+
// fun (@A : Type) -> Option A -> Format
146+
// fun (@A : Type) -> Option A@0 -> Format
158147
&core::Term::FunType(
159148
Span::Empty,
160-
Plicity::Explicit,
149+
Plicity::Implicit,
161150
env.name("A"),
162151
&UNIVERSE,
163152
&Term::FunType(
@@ -176,6 +165,18 @@ impl<'arena> Env<'arena> {
176165
);
177166
env.define_prim_fun(FormatRepr, [&FORMAT_TYPE], &UNIVERSE);
178167

168+
// fun (@A : Type) -> Void -> A
169+
env.define_prim(
170+
Absurd,
171+
&core::Term::FunType(
172+
Span::Empty,
173+
Plicity::Implicit,
174+
env.name("A"),
175+
&UNIVERSE,
176+
&core::Term::FunType(Span::Empty, Plicity::Explicit, None, &VOID_TYPE, &VAR1),
177+
),
178+
);
179+
179180
env.define_prim_fun(BoolEq, [&BOOL_TYPE, &BOOL_TYPE], &BOOL_TYPE);
180181
env.define_prim_fun(BoolNeq, [&BOOL_TYPE, &BOOL_TYPE], &BOOL_TYPE);
181182
env.define_prim_fun(BoolNot, [&BOOL_TYPE], &BOOL_TYPE);
@@ -309,11 +310,11 @@ impl<'arena> Env<'arena> {
309310

310311
env.define_prim(
311312
OptionSome,
312-
// fun (A : Type) -> A -> Option A
313-
// fun (A : Type) -> A@0 -> Option A@1
313+
// fun (@A : Type) -> A -> Option A
314+
// fun (@A : Type) -> A@0 -> Option A@1
314315
&core::Term::FunType(
315316
Span::Empty,
316-
Plicity::Explicit,
317+
Plicity::Implicit,
317318
env.name("A"),
318319
&UNIVERSE,
319320
&Term::FunType(
@@ -332,11 +333,11 @@ impl<'arena> Env<'arena> {
332333
);
333334
env.define_prim(
334335
OptionNone,
335-
// fun (A : Type) -> Option A
336-
// fun (A : Type) -> Option A@0
336+
// fun (@A : Type) -> Option A
337+
// fun (@A : Type) -> Option A@0
337338
&core::Term::FunType(
338339
Span::Empty,
339-
Plicity::Explicit,
340+
Plicity::Implicit,
340341
env.name("A"),
341342
&UNIVERSE,
342343
&Term::FunApp(
@@ -349,16 +350,16 @@ impl<'arena> Env<'arena> {
349350
);
350351
env.define_prim(
351352
OptionFold,
352-
// fun (A : Type) (B : Type) -> B -> (A -> B ) -> Option A -> B
353-
// fun (A : Type) (B : Type) -> B@0 -> (A@2 -> B@2) -> Option A@3 -> B@3
353+
// fun (@A : Type) (@B : Type) -> B -> (A -> B ) -> Option A -> B
354+
// fun (@A : Type) (@B : Type) -> B@0 -> (A@2 -> B@2) -> Option A@3 -> B@3
354355
scope.to_scope(core::Term::FunType(
355356
Span::Empty,
356-
Plicity::Explicit,
357+
Plicity::Implicit,
357358
env.name("A"),
358359
&UNIVERSE,
359360
scope.to_scope(core::Term::FunType(
360361
Span::Empty,
361-
Plicity::Explicit,
362+
Plicity::Implicit,
362363
env.name("B"),
363364
&UNIVERSE,
364365
scope.to_scope(core::Term::FunType(
@@ -391,17 +392,18 @@ impl<'arena> Env<'arena> {
391392
)),
392393
);
393394

394-
// fun (len : UN) (A : Type) -> (A -> Bool) -> ArrayN len A -> Option A
395-
// fun (len : UN) (A : Type) -> (A@0 -> Bool) -> ArrayN len@2 A@1 -> Option A@2
395+
// fun (@len : UN) (@A : Type) -> (A -> Bool) -> ArrayN len A -> Option A
396+
// fun (@len : UN) (@A : Type) -> (A@0 -> Bool) -> ArrayN len@2 A@1 -> Option
397+
// A@2
396398
let find_type = |index_type, array_type| {
397399
scope.to_scope(core::Term::FunType(
398400
Span::Empty,
399-
Plicity::Explicit,
401+
Plicity::Implicit,
400402
env.name("len"),
401403
index_type,
402404
scope.to_scope(core::Term::FunType(
403405
Span::Empty,
404-
Plicity::Explicit,
406+
Plicity::Implicit,
405407
env.name("A"),
406408
&UNIVERSE,
407409
scope.to_scope(core::Term::FunType(
@@ -447,17 +449,17 @@ impl<'arena> Env<'arena> {
447449
env.define_prim(Array32Find, array32_find_type);
448450
env.define_prim(Array64Find, array64_find_type);
449451

450-
// fun (len : UN) -> (A : Type) -> (index : UN) -> ArrayN len A -> A
451-
// fun (len : UN) -> (A : Type) -> (index : UN) -> ArrayN len@2 A@1 -> A@2
452+
// fun (@len : UN) (@A : Type) (index : UN) -> ArrayN len A -> A
453+
// fun (@len : UN) (@A : Type) (index : UN) -> ArrayN len@2 A@1 -> A@2
452454
let array_index_type = |index_type, array_type| {
453455
scope.to_scope(core::Term::FunType(
454456
Span::Empty,
455-
Plicity::Explicit,
457+
Plicity::Implicit,
456458
env.name("len"),
457459
index_type,
458460
scope.to_scope(core::Term::FunType(
459461
Span::Empty,
460-
Plicity::Explicit,
462+
Plicity::Implicit,
461463
env.name("A"),
462464
&UNIVERSE,
463465
scope.to_scope(core::Term::FunType(
@@ -574,7 +576,7 @@ pub type Step = for<'arena> fn(&ElimEnv<'arena, '_>, &[Elim<'arena>]) -> Option<
574576
macro_rules! step {
575577
($env:pat, [$($param:pat),*] => $body:expr) => {
576578
|$env, spine| match spine {
577-
[$(Elim::FunApp(Plicity::Explicit, $param)),*] => Some($body),
579+
[$(Elim::FunApp(_, $param)),*] => Some($body),
578580
_ => return None,
579581
}
580582
};
@@ -782,30 +784,38 @@ pub fn step(prim: Prim) -> Step {
782784

783785
Prim::OptionFold => step!(env, [_, _, on_none, on_some, option] => {
784786
match option.match_prim_spine()? {
785-
(Prim::OptionSome, [Elim::FunApp(Plicity::Explicit, value)]) => env.fun_app(
786-
Plicity::Explicit,
787-
on_some.clone(), value.clone()),
788-
(Prim::OptionNone, []) => on_none.clone(),
787+
(Prim::OptionSome, [_, Elim::FunApp(Plicity::Explicit, value)]) => {
788+
env.fun_app(Plicity::Explicit, on_some.clone(), value.clone())
789+
},
790+
(Prim::OptionNone, [_]) => on_none.clone(),
789791
_ => return None,
790792
}
791793
}),
792794

793795
Prim::Array8Find | Prim::Array16Find | Prim::Array32Find | Prim::Array64Find => {
794-
step!(env, [_, _, pred, array] => match array.as_ref() {
796+
step!(env, [_, elem_type, pred, array] => match array.as_ref() {
795797
Value::ArrayLit(elems) => {
796798
for elem in elems {
797799
match env.fun_app(
798-
Plicity::Explicit,
799-
pred.clone(), elem.clone()).as_ref() {
800+
Plicity::Explicit,
801+
pred.clone(), elem.clone()).as_ref() {
800802
Value::ConstLit(Const::Bool(true)) => {
801-
// TODO: Is elem.span right here?
802-
return Some(Spanned::new(elem.span(), Arc::new(Value::prim(Prim::OptionSome, [elem.clone()]))))
803+
return Some(Spanned::empty(Arc::new(Value::Stuck(
804+
Head::Prim(Prim::OptionSome),
805+
vec![
806+
Elim::FunApp(Plicity::Implicit, elem_type.clone()),
807+
Elim::FunApp(Plicity::Explicit, elem.clone()),
808+
],
809+
))));
803810
},
804811
Value::ConstLit(Const::Bool(false)) => {}
805812
_ => return None,
806813
}
807814
}
808-
Spanned::empty(Arc::new(Value::prim(Prim::OptionNone, [])))
815+
Spanned::empty(Arc::new(Value::Stuck(
816+
Head::Prim(Prim::OptionNone),
817+
vec![Elim::FunApp(Plicity::Implicit, elem_type.clone())],
818+
)))
809819
}
810820
_ => return None,
811821
})

0 commit comments

Comments
 (0)