Skip to content

Commit c2aa1d7

Browse files
brendanzabbrendanzab
authored
Merge pull request #462 from brendanzab/avoid-quotation
Avoid unnecessary quotation in elaboration
2 parents c0784c9 + 73d3f5a commit c2aa1d7

File tree

20 files changed

+171
-234
lines changed

20 files changed

+171
-234
lines changed

‎fathom/src/surface/elaboration.rs‎

Lines changed: 20 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -657,10 +657,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
657657
for item in elab_order.iter().copied().map(|i| &surface_module.items[i]) {
658658
match item {
659659
Item::Def(item) => {
660-
let (expr, type_value) =
660+
let (expr, r#type) =
661661
self.synth_fun_lit(item.range, item.params, item.expr, item.r#type);
662662
let expr_value = self.eval_env().eval(&expr);
663-
let r#type = self.quote_env().quote(self.scope, &type_value);
663+
let type_value = self.eval_env().eval(&r#type);
664664

665665
self.item_env
666666
.push_definition(item.label.1, type_value, expr_value);
@@ -899,13 +899,17 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
899899
&mut self,
900900
pattern: &Pattern<ByteRange>,
901901
r#type: Option<&Term<'_, ByteRange>>,
902-
) -> (CheckedPattern, ArcValue<'arena>) {
902+
) -> (CheckedPattern, core::Term<'arena>, ArcValue<'arena>) {
903903
match r#type {
904-
None => self.synth_pattern(pattern),
904+
None => {
905+
let (pattern, type_value) = self.synth_pattern(pattern);
906+
let r#type = self.quote_env().quote(self.scope, &type_value);
907+
(pattern, r#type, type_value)
908+
}
905909
Some(r#type) => {
906910
let r#type = self.check(r#type, &self.universe.clone());
907911
let type_value = self.eval_env().eval(&r#type);
908-
(self.check_pattern(pattern, &type_value), type_value)
912+
(self.check_pattern(pattern, &type_value), r#type, type_value)
909913
}
910914
}
911915
}
@@ -970,9 +974,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
970974

971975
Vec::from_iter(params.iter().map(|param| {
972976
let range = param.pattern.range();
973-
let (pattern, type_value) =
977+
let (pattern, r#type, type_value) =
974978
self.synth_ann_pattern(&param.pattern, param.r#type.as_ref());
975-
let r#type = self.quote_env().quote(self.scope, &type_value);
976979
let (name, _) = self.push_local_param(pattern, type_value);
977980

978981
(range, param.plicity, name, r#type)
@@ -992,8 +995,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
992995

993996
match (surface_term, expected_type.as_ref()) {
994997
(Term::Let(_, def_pattern, def_type, def_expr, body_expr), _) => {
995-
let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
996-
let def_type = self.quote_env().quote(self.scope, &def_type_value);
998+
let (def_pattern, def_type, def_type_value) =
999+
self.synth_ann_pattern(def_pattern, *def_type);
9971000
let def_expr = self.check(def_expr, &def_type_value);
9981001
let def_expr_value = self.eval_env().eval(&def_expr);
9991002

@@ -1398,8 +1401,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
13981401
(ann_expr, type_value)
13991402
}
14001403
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => {
1401-
let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
1402-
let def_type = self.quote_env().quote(self.scope, &def_type_value);
1404+
let (def_pattern, def_type, def_type_value) =
1405+
self.synth_ann_pattern(def_pattern, *def_type);
14031406
let def_expr = self.check(def_expr, &def_type_value);
14041407
let def_expr_value = self.eval_env().eval(&def_expr);
14051408

@@ -1494,7 +1497,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14941497
(fun_type, self.universe.clone())
14951498
}
14961499
Term::FunLiteral(range, params, body_expr) => {
1497-
self.synth_fun_lit(*range, params, body_expr, None)
1500+
let (expr, r#type) = self.synth_fun_lit(*range, params, body_expr, None);
1501+
(expr, self.eval_env().eval(&r#type))
14981502
}
14991503
Term::App(range, head_expr, args) => {
15001504
let mut head_range = head_expr.range();
@@ -1803,7 +1807,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
18031807
Value::Stuck(Head::MetaVar(_), _) => {
18041808
let range = ByteRange::merge(param.pattern.range(), body_expr.range());
18051809
let (expr, r#type) = self.synth_fun_lit(range, params, body_expr, None);
1806-
self.convert(range, expr, &r#type, expected_type)
1810+
let type_value = self.eval_env().eval(&r#type);
1811+
self.convert(range, expr, &type_value, expected_type)
18071812
}
18081813
Value::Stuck(Head::Prim(Prim::ReportedError), _) => {
18091814
core::Term::Prim(file_range.into(), Prim::ReportedError)
@@ -1829,7 +1834,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
18291834
params: &[Param<'_, ByteRange>],
18301835
body_expr: &Term<'_, ByteRange>,
18311836
body_type: Option<&Term<'_, ByteRange>>,
1832-
) -> (core::Term<'arena>, ArcValue<'arena>) {
1837+
) -> (core::Term<'arena>, core::Term<'arena>) {
18331838
self.local_env.reserve(params.len());
18341839
let initial_local_len = self.local_env.len();
18351840

@@ -1871,7 +1876,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
18711876
);
18721877
}
18731878

1874-
(fun_lit, self.eval_env().eval(&fun_type))
1879+
(fun_lit, fun_type)
18751880
}
18761881

18771882
fn synth_bin_op(

‎formats/opentype.snap‎

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -30,28 +30,28 @@ def link_table : Pos -> {
3030
} -> Format -> Format =
3131
fun file_start table_record table_format => link (file_start + table_record.offset) (limit32 table_record.length table_format);
3232
def platform_id : Format = u16be;
33-
def encoding_id : U16 -> Format = fun platform => u16be;
33+
def encoding_id : Repr platform_id -> Format = fun platform => u16be;
3434
def empty : Format = ();
3535
def offset32 : Pos -> Format -> Format = fun base format => {
3636
offset <- u32be,
3737
link <- match offset { 0 => empty, _ => link (base + offset) format },
3838
};
3939
def language_id : Format = u16be;
40-
def cmap_language_id : U16 -> Format = fun platform => language_id;
40+
def cmap_language_id : Repr platform_id -> Format = fun platform => language_id;
4141
def small_glyph_id : Format = u8;
42-
def cmap_subtable_format0 : U16 -> Format = fun platform => {
42+
def cmap_subtable_format0 : Repr platform_id -> Format = fun platform => {
4343
length <- u16be,
4444
language <- cmap_language_id platform,
4545
glyph_id_array <- array16 256 small_glyph_id,
4646
};
47-
def cmap_subtable_format2 : U16 -> Format = fun platform => {
47+
def cmap_subtable_format2 : Repr platform_id -> Format = fun platform => {
4848
length <- u16be,
4949
language <- cmap_language_id platform,
5050
sub_header_keys <- array16 256 u16be,
5151
};
5252
def reserved : fun (format : Format) -> Repr format -> Format =
5353
fun format default => format;
54-
def cmap_subtable_format4 : U16 -> Format = fun platform => {
54+
def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => {
5555
length <- u16be,
5656
language <- cmap_language_id platform,
5757
seg_count_x2 <- u16be,
@@ -65,45 +65,46 @@ def cmap_subtable_format4 : U16 -> Format = fun platform => {
6565
id_delta <- array16 seg_count s16be,
6666
id_range_offsets <- array16 seg_count u16be,
6767
};
68-
def cmap_subtable_format6 : U16 -> Format = fun platform => {
68+
def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => {
6969
length <- u16be,
7070
language <- cmap_language_id platform,
7171
first_code <- u16be,
7272
entry_count <- u16be,
7373
glyph_id_array <- array16 entry_count u16be,
7474
};
7575
def language_id32 : Format = u32be;
76-
def cmap_language_id32 : U16 -> Format = fun platform => language_id32;
76+
def cmap_language_id32 : Repr platform_id -> Format =
77+
fun platform => language_id32;
7778
def sequential_map_group : Format = {
7879
start_char_code <- u32be,
7980
end_char_code <- u32be,
8081
start_glyph_id <- u32be,
8182
};
82-
def cmap_subtable_format8 : U16 -> Format = fun platform => {
83+
def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => {
8384
_reserved <- reserved u16be 0,
8485
length <- u32be,
8586
language <- cmap_language_id32 platform,
8687
is32 <- array16 8192 u8,
8788
num_groups <- u32be,
8889
groups <- array32 num_groups sequential_map_group,
8990
};
90-
def cmap_subtable_format10 : U16 -> Format = fun platform => {
91+
def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => {
9192
_reserved <- reserved u16be 0,
9293
length <- u32be,
9394
language <- cmap_language_id32 platform,
9495
start_char_code <- u32be,
9596
num_chars <- u32be,
9697
glyph_id_array <- array32 num_chars u16be,
9798
};
98-
def cmap_subtable_format12 : U16 -> Format = fun platform => {
99+
def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => {
99100
_reserved <- reserved u16be 0,
100101
length <- u32be,
101102
language <- cmap_language_id32 platform,
102103
num_groups <- u32be,
103104
groups <- array32 num_groups sequential_map_group,
104105
};
105106
def constant_map_group : Format = sequential_map_group;
106-
def cmap_subtable_format13 : U16 -> Format = fun platform => {
107+
def cmap_subtable_format13 : Repr platform_id -> Format = fun platform => {
107108
_reserved <- reserved u16be 0,
108109
length <- u32be,
109110
language <- cmap_language_id32 platform,
@@ -129,14 +130,14 @@ def variation_selector : Pos -> Format = fun table_start => {
129130
default_uvs_offset <- offset32 table_start default_uvs_table,
130131
non_default_uvs_offset <- offset32 table_start non_default_uvs_table,
131132
};
132-
def cmap_subtable_format14 : U16 -> Pos -> Format =
133+
def cmap_subtable_format14 : Repr platform_id -> Pos -> Format =
133134
fun platform table_start => {
134135
length <- u32be,
135136
num_var_selector_records <- u32be,
136137
var_selector <- array32 num_var_selector_records (variation_selector table_start),
137138
};
138139
def unknown_table : Format = ();
139-
def cmap_subtable : U16 -> Format = fun platform => {
140+
def cmap_subtable : Repr platform_id -> Format = fun platform => {
140141
table_start <- stream_pos,
141142
format <- u16be,
142143
data <- match format {

‎tests/succeed/equality.snap‎

Lines changed: 26 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -2,51 +2,40 @@ stdout = '''
22
let id : fun (A : Type) -> A -> A = fun A a => a;
33
let Eq : fun (A : Type) -> A -> A -> Type = fun A a0 a1 => fun (P : A ->
44
Type) -> P a0 -> P a1;
5-
let refl : fun (A : Type) (a : A) (P : A -> Type) -> P a -> P a =
6-
fun A a P => id (P a);
7-
let fun_eta_left : fun (f : Type -> Type) (P : (Type -> Type) -> Type) -> P f ->
8-
P (fun x => f x) = fun f => refl (Type -> Type) f;
9-
let fun_eta_right : fun (f : Type -> Type) (P : (Type -> Type) -> Type) ->
10-
P (fun x => f x) -> P f = fun f => refl (Type -> Type) f;
11-
let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) ->
12-
Type) -> P f -> P (fun x => f x) = fun f => refl (Type -> Type -> Type) f;
13-
let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type)
14-
-> Type) -> P (fun x => f x) -> P f = fun f => refl (Type -> Type -> Type) f;
15-
let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) ->
16-
Type) -> P f -> P (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f;
17-
let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type)
18-
-> Type) -> P (fun x y => f x y) -> P f = fun f => refl (Type -> Type ->
5+
let refl : fun (A : Type) (a : A) -> Eq A a a = fun A a P => id (P a);
6+
let fun_eta_left : fun (f : Type -> Type) -> Eq (Type ->
7+
Type) f (fun x => f x) = fun f => refl (Type -> Type) f;
8+
let fun_eta_right : fun (f : Type -> Type) -> Eq (Type ->
9+
Type) (fun x => f x) f = fun f => refl (Type -> Type) f;
10+
let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
11+
Type) f (fun x => f x) = fun f => refl (Type -> Type -> Type) f;
12+
let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
13+
Type) (fun x => f x) f = fun f => refl (Type -> Type -> Type) f;
14+
let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
15+
Type) f (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f;
16+
let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
17+
Type) (fun x y => f x y) f = fun f => refl (Type -> Type -> Type) f;
18+
let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
19+
Type) (fun x => f x) (fun x y => f x y) = fun f => refl (Type -> Type ->
1920
Type) f;
20-
let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) ->
21-
Type) -> P (fun x => f x) -> P (fun x y => f x y) = fun f => refl (Type -> Type
22-
-> Type) f;
23-
let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type)
24-
-> Type) -> P (fun x y => f x y) -> P (fun x => f x) = fun f => refl (Type ->
25-
Type -> Type) f;
26-
let record_eta_left : fun (r : { x : Type, y : Type }) (P : {
27-
x : Type,
28-
y : Type,
29-
} -> Type) -> P r -> P { x = r.x, y = r.y } = fun r => refl {
30-
x : Type,
31-
y : Type,
32-
} r;
33-
let record_eta_right : fun (r : { x : Type, y : Type }) (P : {
21+
let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
22+
Type) (fun x y => f x y) (fun x => f x) = fun f => refl (Type -> Type ->
23+
Type) f;
24+
let record_eta_left : fun (r : { x : Type, y : Type }) -> Eq {
3425
x : Type,
3526
y : Type,
36-
} -> Type) -> P { x = r.x, y = r.y } -> P r = fun r => refl {
27+
} r { x = r.x, y = r.y } = fun r => refl { x : Type, y : Type } r;
28+
let record_eta_right : fun (r : { x : Type, y : Type }) -> Eq {
3729
x : Type,
3830
y : Type,
39-
} r;
40-
let four_chars : fun (P : U32 -> Type) -> P "beng" -> P 1650814567 =
41-
refl U32 "beng";
42-
let three_chars : fun (P : U32 -> Type) -> P "BEN " -> P 1111838240 =
43-
refl U32 "BEN ";
31+
} { x = r.x, y = r.y } r = fun r => refl { x : Type, y : Type } r;
32+
let four_chars : Eq U32 "beng" 1650814567 = refl U32 "beng";
33+
let three_chars : Eq U32 "BEN " 1111838240 = refl U32 "BEN ";
4434
let foo : U32 -> U32 = fun x => match x { 1 => 0, x => x };
45-
let eq_foo : fun (P : (U32 -> U32) -> Type) -> P (fun x => match x {
35+
let eq_foo : Eq (U32 -> U32) foo foo = refl (U32 -> U32) (fun a => match a {
4636
1 => 0,
4737
x => x,
48-
}) -> P (fun x => match x { 1 => 0, x => x }) = refl (U32 ->
49-
U32) (fun a => match a { 1 => 0, x => x });
38+
});
5039
Type : Type
5140
'''
5241
stderr = ''

‎tests/succeed/format-cond/simple.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ stdout = '''
22
let format : Format = {
33
sfnt_version <- { version <- u32be | version == (0xffff : U32) },
44
};
5-
let _ : { sfnt_version : U32 } -> { sfnt_version : U32 } = fun x => x;
5+
let _ : Repr format -> { sfnt_version : Repr u32be } = fun x => x;
66
() : ()
77
'''
88
stderr = ''

‎tests/succeed/format-overlap/dependent.snap‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,7 @@ let silly : Format = overlap {
88
record0 <- record0,
99
record1 <- record1 record0.length,
1010
};
11-
let _ : {
12-
record0 : { length : U8 },
13-
record1 : { _length : U8, data : Array8 record0.length U8 },
14-
} -> {
11+
let _ : Repr silly -> {
1512
record0 : { length : U8 },
1613
record1 : { _length : U8, data : Array8 record0.length U8 },
1714
} = fun silly => silly;

‎tests/succeed/format-overlap/field-refinements.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
stdout = '''
22
let number : Format = overlap { u <- u32be where u >= (2 : U32), s <- s32be };
3-
let _ : { u : U32, s : S32 } -> { u : U32, s : S32 } = fun n => n;
3+
let _ : Repr number -> { u : U32, s : S32 } = fun n => n;
44
() : ()
55
'''
66
stderr = ''

‎tests/succeed/format-overlap/numbers.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
stdout = '''
22
let number : Format = overlap { u <- u32be, s <- s32be };
3-
let _ : { u : U32, s : S32 } -> { u : U32, s : S32 } = fun n => n;
3+
let _ : Repr number -> { u : U32, s : S32 } = fun n => n;
44
() : ()
55
'''
66
stderr = ''

‎tests/succeed/format-record/computed-fields.snap‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,14 @@ let format : Format = {
55
start_code <- array16 seg_count u16be,
66
id_delta <- array16 seg_count s16be,
77
};
8-
let _ : {
9-
seg_count_x2 : U16,
10-
seg_count : U16,
11-
start_code : Array16 seg_count U16,
12-
id_delta : Array16 seg_count S16,
13-
} -> {
8+
let _ : Repr format -> {
149
seg_count_x2 : U16,
1510
seg_count : U16,
1611
start_code : Array16 seg_count U16,
1712
id_delta : Array16 seg_count S16,
1813
} = fun x => x;
1914
let format : Format = { let x : U32 = 256 };
20-
let _ : { x : U32 } -> { x : U32 } = fun x => x;
15+
let _ : Repr format -> { x : U32 } = fun x => x;
2116
() : ()
2217
'''
2318
stderr = ''

‎tests/succeed/format-record/field-refinements.snap‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,8 @@ let format : Format = {
44
len <- u8 where len <= (16 : U8),
55
data <- array8 len u8,
66
};
7-
let _ : { magic : U64, len : U8, data : Array8 len U8 } -> {
8-
magic : U64,
9-
len : U8,
10-
data : Array8 len U8,
11-
} = fun x => x;
7+
let _ : Repr format -> { magic : U64, len : U8, data : Array8 len U8 } =
8+
fun x => x;
129
() : ()
1310
'''
1411
stderr = ''

‎tests/succeed/format-repr/pair-dependent.snap‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
stdout = '''
22
let array32 : U32 -> Format -> Format = fun len Elem => Elem;
33
let pair : Format = { len <- u32be, data <- array32 len u32be };
4-
let test_pair : { len : U32, data : U32 } -> { len : U32, data : U32 } =
5-
fun p => p;
4+
let test_pair : Repr pair -> { len : U32, data : U32 } = fun p => p;
65
pair : Format
76
'''
87
stderr = ''

0 commit comments

Comments
 (0)