Skip to content

Commit a40a259

Browse files
KmeakinKmeakin
committed
Cleanup surface::elaboration 
1 parent 3960a94 commit a40a259

File tree

14 files changed

+1721
-1333
lines changed

14 files changed

+1721
-1333
lines changed

‎fathom/src/core.rs

Lines changed: 361 additions & 13 deletions
Large diffs are not rendered by default.

‎fathom/src/core/binary.rs

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -425,15 +425,11 @@ impl<'arena, 'data> Context<'arena, 'data> {
425425
(Prim::FormatF32Le, []) => read_const(reader, span, read_f32le, Const::F32),
426426
(Prim::FormatF64Be, []) => read_const(reader, span, read_f64be, Const::F64),
427427
(Prim::FormatF64Le, []) => read_const(reader, span, read_f64le, Const::F64),
428-
(Prim::FormatRepeatLen8, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
429-
(Prim::FormatRepeatLen16, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
430-
(Prim::FormatRepeatLen32, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
431-
(Prim::FormatRepeatLen64, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
428+
(Prim::FormatRepeatLen8 | Prim::FormatRepeatLen16 | Prim::FormatRepeatLen32 | Prim::FormatRepeatLen64,
429+
[FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
432430
(Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, format),
433-
(Prim::FormatLimit8, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
434-
(Prim::FormatLimit16, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
435-
(Prim::FormatLimit32, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
436-
(Prim::FormatLimit64, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
431+
(Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64,
432+
[FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
437433
(Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, pos, format),
438434
(Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(format, r#ref),
439435
(Prim::FormatStreamPos, []) => read_stream_pos(reader, span),
@@ -642,9 +638,7 @@ fn read_s8(reader: &mut BufferReader<'_>) -> Result<i8, BufferError> {
642638
/// Generates a function that reads a multi-byte primitive.
643639
macro_rules! read_multibyte_prim {
644640
($read_multibyte_prim:ident, $from_bytes:ident, $T:ident) => {
645-
fn $read_multibyte_prim<'data>(
646-
reader: &mut BufferReader<'data>,
647-
) -> Result<$T, BufferError> {
641+
fn $read_multibyte_prim(reader: &mut BufferReader) -> Result<$T, BufferError> {
648642
Ok($T::$from_bytes(*reader.read_byte_array()?))
649643
}
650644
};

‎fathom/src/core/pretty.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -143,17 +143,17 @@ impl<'arena> Context {
143143
self.term_prec(Prec::Top, r#type),
144144
]),
145145
),
146-
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren(
146+
Term::Let(_, def, body_expr) => self.paren(
147147
prec > Prec::Let,
148148
RcDoc::concat([
149149
RcDoc::concat([
150150
RcDoc::text("let"),
151151
RcDoc::space(),
152-
self.ann_pattern(Prec::Top, *def_pattern, def_type),
152+
self.ann_pattern(Prec::Top, def.name, &def.r#type),
153153
RcDoc::space(),
154154
RcDoc::text("="),
155155
RcDoc::softline(),
156-
self.term_prec(Prec::Let, def_expr),
156+
self.term_prec(Prec::Let, &def.expr),
157157
RcDoc::text(";"),
158158
])
159159
.group(),

‎fathom/src/core/prim.rs

Lines changed: 283 additions & 373 deletions
Large diffs are not rendered by default.

‎fathom/src/core/semantics.rs

Lines changed: 54 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ use std::sync::Arc;
66

77
use scoped_arena::Scope;
88

9+
use super::{Builder, LetDef};
910
use crate::alloc::SliceVec;
1011
use crate::core::{prim, Const, LocalInfo, Plicity, Prim, Term};
1112
use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv};
@@ -300,8 +301,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
300301
self.apply_local_infos(head_expr, local_infos)
301302
}
302303
Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)),
303-
Term::Let(span, _, _, def_expr, body_expr) => {
304-
let def_expr = self.eval(def_expr);
304+
Term::Let(span, def, body_expr) => {
305+
let def_expr = self.eval(&def.expr);
305306
self.local_exprs.push(def_expr);
306307
let body_expr = self.eval(body_expr);
307308
self.local_exprs.pop();
@@ -667,21 +668,17 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
667668
// NOTE: this copies more than is necessary when `'in_arena == 'out_arena`:
668669
// for example when copying label slices.
669670

671+
let builder = Builder::new(scope);
670672
let value = self.elim_env.force(value);
671673
let span = value.span();
672674
match value.as_ref() {
673675
Value::Stuck(head, spine) => spine.iter().fold(
674676
self.quote_head(scope, span, head),
675677
|head_expr, elim| match elim {
676-
Elim::FunApp(plicity, arg_expr) => Term::FunApp(
677-
span,
678-
*plicity,
679-
scope.to_scope(head_expr),
680-
scope.to_scope(self.quote(scope, arg_expr)),
681-
),
682-
Elim::RecordProj(label) => {
683-
Term::RecordProj(span, scope.to_scope(head_expr), *label)
678+
Elim::FunApp(plicity, arg_expr) => {
679+
builder.fun_app(span, *plicity, head_expr, self.quote(scope, arg_expr))
684680
}
681+
Elim::RecordProj(label) => builder.record_proj(span, head_expr, *label),
685682
Elim::ConstMatch(branches) => {
686683
let mut branches = branches.clone();
687684
let mut pattern_branches = SliceVec::new(scope, branches.num_patterns());
@@ -699,9 +696,9 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
699696
}
700697
};
701698

702-
Term::ConstMatch(
699+
builder.const_match(
703700
span,
704-
scope.to_scope(head_expr),
701+
head_expr,
705702
pattern_branches.into(),
706703
default_branch
707704
.map(|(name, expr)| (name, self.quote_closure(scope, &expr))),
@@ -712,20 +709,19 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
712709

713710
Value::Universe => Term::Universe(span),
714711

715-
Value::FunType(plicity, param_name, param_type, body_type) => Term::FunType(
712+
Value::FunType(plicity, param_name, param_type, body_type) => builder.fun_type(
716713
span,
717714
*plicity,
718715
*param_name,
719-
scope.to_scope(self.quote(scope, param_type)),
716+
self.quote(scope, param_type),
720717
self.quote_closure(scope, body_type),
721718
),
722-
Value::FunLit(plicity, param_name, body_expr) => Term::FunLit(
719+
Value::FunLit(plicity, param_name, body_expr) => builder.fun_lit(
723720
span,
724721
*plicity,
725722
*param_name,
726723
self.quote_closure(scope, body_expr),
727724
),
728-
729725
Value::RecordType(labels, types) => Term::RecordType(
730726
span,
731727
scope.to_scope_from_iter(labels.iter().copied()),
@@ -746,10 +742,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
746742
scope.to_scope_from_iter(labels.iter().copied()),
747743
self.quote_telescope(scope, formats),
748744
),
749-
Value::FormatCond(label, format, cond) => Term::FormatCond(
745+
Value::FormatCond(label, format, cond) => builder.format_cond(
750746
span,
751747
*label,
752-
scope.to_scope(self.quote(scope, format)),
748+
self.quote(scope, format),
753749
self.quote_closure(scope, cond),
754750
),
755751
Value::FormatOverlap(labels, formats) => Term::FormatOverlap(
@@ -792,15 +788,15 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
792788
&mut self,
793789
scope: &'out_arena Scope<'out_arena>,
794790
closure: &Closure<'in_arena>,
795-
) -> &'out_arena Term<'out_arena> {
791+
) -> Term<'out_arena> {
796792
let var = Arc::new(Value::local_var(self.local_exprs.next_level()));
797793
let value = self.elim_env.apply_closure(closure, Spanned::empty(var));
798794

799795
self.push_local();
800796
let term = self.quote(scope, &value);
801797
self.pop_local();
802798

803-
scope.to_scope(term)
799+
term
804800
}
805801

806802
/// Quote a [telescope][Telescope] back into a slice of [terms][Term].
@@ -848,6 +844,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
848844
scope: &'out_arena Scope<'out_arena>,
849845
term: &Term<'arena>,
850846
) -> Term<'out_arena> {
847+
let builder = Builder::new(scope);
848+
851849
match term {
852850
Term::ItemVar(span, var) => Term::ItemVar(*span, *var),
853851
Term::LocalVar(span, var) => Term::LocalVar(*span, *var),
@@ -871,29 +869,31 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
871869
Term::InsertedMeta(*span, *var, infos)
872870
}
873871
},
874-
Term::Ann(span, expr, r#type) => Term::Ann(
872+
Term::Ann(span, expr, r#type) => builder.ann(
875873
*span,
876-
scope.to_scope(self.unfold_metas(scope, expr)),
877-
scope.to_scope(self.unfold_metas(scope, r#type)),
874+
self.unfold_metas(scope, expr),
875+
self.unfold_metas(scope, r#type),
878876
),
879-
Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let(
877+
Term::Let(span, def, body_expr) => builder.r#let(
880878
*span,
881-
*def_name,
882-
scope.to_scope(self.unfold_metas(scope, def_type)),
883-
scope.to_scope(self.unfold_metas(scope, def_expr)),
879+
LetDef {
880+
name: def.name,
881+
r#type: (self.unfold_metas(scope, &def.r#type)),
882+
expr: (self.unfold_metas(scope, &def.expr)),
883+
},
884884
self.unfold_bound_metas(scope, body_expr),
885885
),
886886

887887
Term::Universe(span) => Term::Universe(*span),
888888

889-
Term::FunType(span, plicity, param_name, param_type, body_type) => Term::FunType(
889+
Term::FunType(span, plicity, param_name, param_type, body_type) => builder.fun_type(
890890
*span,
891891
*plicity,
892892
*param_name,
893-
scope.to_scope(self.unfold_metas(scope, param_type)),
893+
self.unfold_metas(scope, param_type),
894894
self.unfold_bound_metas(scope, body_type),
895895
),
896-
Term::FunLit(span, plicity, param_name, body_expr) => Term::FunLit(
896+
Term::FunLit(span, plicity, param_name, body_expr) => builder.fun_lit(
897897
*span,
898898
*plicity,
899899
*param_name,
@@ -921,10 +921,10 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
921921
scope.to_scope_from_iter(labels.iter().copied()),
922922
self.unfold_telescope_metas(scope, formats),
923923
),
924-
Term::FormatCond(span, name, format, pred) => Term::FormatCond(
924+
Term::FormatCond(span, name, format, pred) => builder.format_cond(
925925
*span,
926926
*name,
927-
scope.to_scope(self.unfold_metas(scope, format)),
927+
self.unfold_metas(scope, format),
928928
self.unfold_bound_metas(scope, pred),
929929
),
930930
Term::FormatOverlap(span, labels, formats) => Term::FormatOverlap(
@@ -945,6 +945,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
945945
scope: &'out_arena Scope<'out_arena>,
946946
term: &Term<'arena>,
947947
) -> TermOrValue<'arena, 'out_arena> {
948+
let builder = Builder::new(scope);
949+
948950
// Recurse to find the head of an elimination, checking if it's a
949951
// metavariable. If so, check if it has a solution, and then apply
950952
// eliminations to the solution in turn on our way back out.
@@ -971,11 +973,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
971973

972974
Term::FunApp(span, plicity, head_expr, arg_expr) => {
973975
match self.unfold_meta_var_spines(scope, head_expr) {
974-
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::FunApp(
976+
TermOrValue::Term(head_expr) => TermOrValue::Term(builder.fun_app(
975977
*span,
976978
*plicity,
977-
scope.to_scope(head_expr),
978-
scope.to_scope(self.unfold_metas(scope, arg_expr)),
979+
head_expr,
980+
self.unfold_metas(scope, arg_expr),
979981
)),
980982
TermOrValue::Value(head_expr) => {
981983
let arg_expr = self.eval(arg_expr);
@@ -985,28 +987,29 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
985987
}
986988
Term::RecordProj(span, head_expr, label) => {
987989
match self.unfold_meta_var_spines(scope, head_expr) {
988-
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::RecordProj(
989-
*span,
990-
scope.to_scope(head_expr),
991-
*label,
992-
)),
990+
TermOrValue::Term(head_expr) => {
991+
TermOrValue::Term(builder.record_proj(*span, head_expr, *label))
992+
}
993993
TermOrValue::Value(head_expr) => {
994994
TermOrValue::Value(self.elim_env.record_proj(head_expr, *label))
995995
}
996996
}
997997
}
998998
Term::ConstMatch(span, head_expr, branches, default_branch) => {
999999
match self.unfold_meta_var_spines(scope, head_expr) {
1000-
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::ConstMatch(
1001-
*span,
1002-
scope.to_scope(head_expr),
1003-
scope.to_scope_from_iter(
1004-
(branches.iter())
1005-
.map(|(r#const, expr)| (*r#const, self.unfold_metas(scope, expr))),
1000+
TermOrValue::Term(head_expr) => TermOrValue::Term(
1001+
builder.const_match(
1002+
*span,
1003+
head_expr,
1004+
scope.to_scope_from_iter(
1005+
branches.iter().map(|(r#const, expr)| {
1006+
(*r#const, self.unfold_metas(scope, expr))
1007+
}),
1008+
),
1009+
default_branch
1010+
.map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
10061011
),
1007-
default_branch
1008-
.map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
1009-
)),
1012+
),
10101013
TermOrValue::Value(head_expr) => {
10111014
let branches =
10121015
Branches::new(self.local_exprs.clone(), branches, *default_branch);
@@ -1023,14 +1026,14 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
10231026
&mut self,
10241027
scope: &'out_arena Scope<'out_arena>,
10251028
term: &Term<'arena>,
1026-
) -> &'out_arena Term<'out_arena> {
1029+
) -> Term<'out_arena> {
10271030
let var = Arc::new(Value::local_var(self.local_exprs.len().next_level()));
10281031

10291032
self.local_exprs.push(Spanned::empty(var));
10301033
let term = self.unfold_metas(scope, term);
10311034
self.local_exprs.pop();
10321035

1033-
scope.to_scope(term)
1036+
term
10341037
}
10351038

10361039
fn unfold_telescope_metas<'out_arena>(

‎fathom/src/source.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,12 @@ impl fmt::Debug for ByteRange {
162162
}
163163
}
164164

165+
impl From<(BytePos, BytePos)> for ByteRange {
166+
fn from((start, end): (BytePos, BytePos)) -> Self {
167+
Self { start, end }
168+
}
169+
}
170+
165171
impl ByteRange {
166172
pub fn new(start: BytePos, end: BytePos) -> ByteRange {
167173
ByteRange { start, end }

0 commit comments

Comments
 (0)