Cleanup surface::elaboration

Author: Kmeakin

fathom/src/core.rs

@@ -425,15 +425,11 @@ impl<'arena, 'data> Context<'arena, 'data> {
             (Prim::FormatF32Le, []) => read_const(reader, span, read_f32le, Const::F32),
             (Prim::FormatF64Be, []) => read_const(reader, span, read_f64be, Const::F64),
             (Prim::FormatF64Le, []) => read_const(reader, span, read_f64le, Const::F64),
-            (Prim::FormatRepeatLen8, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatLen16, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatLen32, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatLen64, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
+            (Prim::FormatRepeatLen8 | Prim::FormatRepeatLen16 | Prim::FormatRepeatLen32 | Prim::FormatRepeatLen64,
+                [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
             (Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, format),
-            (Prim::FormatLimit8, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLimit16, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLimit32, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLimit64, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
+            (Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64,
+                [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
             (Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, pos, format),
             (Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(format, r#ref),
             (Prim::FormatStreamPos, []) => read_stream_pos(reader, span),
@@ -642,9 +638,7 @@ fn read_s8(reader: &mut BufferReader<'_>) -> Result<i8, BufferError> {
 /// Generates a function that reads a multi-byte primitive.
 macro_rules! read_multibyte_prim {
     ($read_multibyte_prim:ident, $from_bytes:ident, $T:ident) => {
-        fn $read_multibyte_prim<'data>(
-            reader: &mut BufferReader<'data>,
-        ) -> Result<$T, BufferError> {
+        fn $read_multibyte_prim(reader: &mut BufferReader) -> Result<$T, BufferError> {
             Ok($T::$from_bytes(*reader.read_byte_array()?))
         }
     };

fathom/src/core/binary.rs

@@ -143,17 +143,17 @@ impl<'arena> Context {
                     self.term_prec(Prec::Top, r#type),
                 ]),
             ),
-            Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren(
+            Term::Let(_, def, body_expr) => self.paren(
                 prec > Prec::Let,
                 RcDoc::concat([
                     RcDoc::concat([
                         RcDoc::text("let"),
                         RcDoc::space(),
-                        self.ann_pattern(Prec::Top, *def_pattern, def_type),
+                        self.ann_pattern(Prec::Top, def.name, &def.r#type),
                         RcDoc::space(),
                         RcDoc::text("="),
                         RcDoc::softline(),
-                        self.term_prec(Prec::Let, def_expr),
+                        self.term_prec(Prec::Let, &def.expr),
                         RcDoc::text(";"),
                     ])
                     .group(),

fathom/src/core/pretty.rs

@@ -6,6 +6,7 @@ use std::sync::Arc;
 
 use scoped_arena::Scope;
 
+use super::{Builder, LetDef};
 use crate::alloc::SliceVec;
 use crate::core::{prim, Const, LocalInfo, Plicity, Prim, Term};
 use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv};
@@ -300,8 +301,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                 self.apply_local_infos(head_expr, local_infos)
             }
             Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)),
-            Term::Let(span, _, _, def_expr, body_expr) => {
-                let def_expr = self.eval(def_expr);
+            Term::Let(span, def, body_expr) => {
+                let def_expr = self.eval(&def.expr);
                 self.local_exprs.push(def_expr);
                 let body_expr = self.eval(body_expr);
                 self.local_exprs.pop();
@@ -667,21 +668,17 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         // NOTE: this copies more than is necessary when `'in_arena == 'out_arena`:
         // for example when copying label slices.
 
+        let builder = Builder::new(scope);
         let value = self.elim_env.force(value);
         let span = value.span();
         match value.as_ref() {
             Value::Stuck(head, spine) => spine.iter().fold(
                 self.quote_head(scope, span, head),
                 |head_expr, elim| match elim {
-                    Elim::FunApp(plicity, arg_expr) => Term::FunApp(
-                        span,
-                        *plicity,
-                        scope.to_scope(head_expr),
-                        scope.to_scope(self.quote(scope, arg_expr)),
-                    ),
-                    Elim::RecordProj(label) => {
-                        Term::RecordProj(span, scope.to_scope(head_expr), *label)
+                    Elim::FunApp(plicity, arg_expr) => {
+                        builder.fun_app(span, *plicity, head_expr, self.quote(scope, arg_expr))
                     }
+                    Elim::RecordProj(label) => builder.record_proj(span, head_expr, *label),
                     Elim::ConstMatch(branches) => {
                         let mut branches = branches.clone();
                         let mut pattern_branches = SliceVec::new(scope, branches.num_patterns());
@@ -699,9 +696,9 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
                             }
                         };
 
-                        Term::ConstMatch(
+                        builder.const_match(
                             span,
-                            scope.to_scope(head_expr),
+                            head_expr,
                             pattern_branches.into(),
                             default_branch
                                 .map(|(name, expr)| (name, self.quote_closure(scope, &expr))),
@@ -712,20 +709,19 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
 
             Value::Universe => Term::Universe(span),
 
-            Value::FunType(plicity, param_name, param_type, body_type) => Term::FunType(
+            Value::FunType(plicity, param_name, param_type, body_type) => builder.fun_type(
                 span,
                 *plicity,
                 *param_name,
-                scope.to_scope(self.quote(scope, param_type)),
+                self.quote(scope, param_type),
                 self.quote_closure(scope, body_type),
             ),
-            Value::FunLit(plicity, param_name, body_expr) => Term::FunLit(
+            Value::FunLit(plicity, param_name, body_expr) => builder.fun_lit(
                 span,
                 *plicity,
                 *param_name,
                 self.quote_closure(scope, body_expr),
             ),
-
             Value::RecordType(labels, types) => Term::RecordType(
                 span,
                 scope.to_scope_from_iter(labels.iter().copied()),
@@ -746,10 +742,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
                 scope.to_scope_from_iter(labels.iter().copied()),
                 self.quote_telescope(scope, formats),
             ),
-            Value::FormatCond(label, format, cond) => Term::FormatCond(
+            Value::FormatCond(label, format, cond) => builder.format_cond(
                 span,
                 *label,
-                scope.to_scope(self.quote(scope, format)),
+                self.quote(scope, format),
                 self.quote_closure(scope, cond),
             ),
             Value::FormatOverlap(labels, formats) => Term::FormatOverlap(
@@ -792,15 +788,15 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         &mut self,
         scope: &'out_arena Scope<'out_arena>,
         closure: &Closure<'in_arena>,
-    ) -> &'out_arena Term<'out_arena> {
+    ) -> Term<'out_arena> {
         let var = Arc::new(Value::local_var(self.local_exprs.next_level()));
         let value = self.elim_env.apply_closure(closure, Spanned::empty(var));
 
         self.push_local();
         let term = self.quote(scope, &value);
         self.pop_local();
 
-        scope.to_scope(term)
+        term
     }
 
     /// Quote a [telescope][Telescope] back into a slice of [terms][Term].
@@ -848,6 +844,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
         scope: &'out_arena Scope<'out_arena>,
         term: &Term<'arena>,
     ) -> Term<'out_arena> {
+        let builder = Builder::new(scope);
+
         match term {
             Term::ItemVar(span, var) => Term::ItemVar(*span, *var),
             Term::LocalVar(span, var) => Term::LocalVar(*span, *var),
@@ -871,29 +869,31 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                     Term::InsertedMeta(*span, *var, infos)
                 }
             },
-            Term::Ann(span, expr, r#type) => Term::Ann(
+            Term::Ann(span, expr, r#type) => builder.ann(
                 *span,
-                scope.to_scope(self.unfold_metas(scope, expr)),
-                scope.to_scope(self.unfold_metas(scope, r#type)),
+                self.unfold_metas(scope, expr),
+                self.unfold_metas(scope, r#type),
             ),
-            Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let(
+            Term::Let(span, def, body_expr) => builder.r#let(
                 *span,
-                *def_name,
-                scope.to_scope(self.unfold_metas(scope, def_type)),
-                scope.to_scope(self.unfold_metas(scope, def_expr)),
+                LetDef {
+                    name: def.name,
+                    r#type: (self.unfold_metas(scope, &def.r#type)),
+                    expr: (self.unfold_metas(scope, &def.expr)),
+                },
                 self.unfold_bound_metas(scope, body_expr),
             ),
 
             Term::Universe(span) => Term::Universe(*span),
 
-            Term::FunType(span, plicity, param_name, param_type, body_type) => Term::FunType(
+            Term::FunType(span, plicity, param_name, param_type, body_type) => builder.fun_type(
                 *span,
                 *plicity,
                 *param_name,
-                scope.to_scope(self.unfold_metas(scope, param_type)),
+                self.unfold_metas(scope, param_type),
                 self.unfold_bound_metas(scope, body_type),
             ),
-            Term::FunLit(span, plicity, param_name, body_expr) => Term::FunLit(
+            Term::FunLit(span, plicity, param_name, body_expr) => builder.fun_lit(
                 *span,
                 *plicity,
                 *param_name,
@@ -921,10 +921,10 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                 scope.to_scope_from_iter(labels.iter().copied()),
                 self.unfold_telescope_metas(scope, formats),
             ),
-            Term::FormatCond(span, name, format, pred) => Term::FormatCond(
+            Term::FormatCond(span, name, format, pred) => builder.format_cond(
                 *span,
                 *name,
-                scope.to_scope(self.unfold_metas(scope, format)),
+                self.unfold_metas(scope, format),
                 self.unfold_bound_metas(scope, pred),
             ),
             Term::FormatOverlap(span, labels, formats) => Term::FormatOverlap(
@@ -945,6 +945,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
         scope: &'out_arena Scope<'out_arena>,
         term: &Term<'arena>,
     ) -> TermOrValue<'arena, 'out_arena> {
+        let builder = Builder::new(scope);
+
         // Recurse to find the head of an elimination, checking if it's a
         // metavariable. If so, check if it has a solution, and then apply
         // eliminations to the solution in turn on our way back out.
@@ -971,11 +973,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
 
             Term::FunApp(span, plicity, head_expr, arg_expr) => {
                 match self.unfold_meta_var_spines(scope, head_expr) {
-                    TermOrValue::Term(head_expr) => TermOrValue::Term(Term::FunApp(
+                    TermOrValue::Term(head_expr) => TermOrValue::Term(builder.fun_app(
                         *span,
                         *plicity,
-                        scope.to_scope(head_expr),
-                        scope.to_scope(self.unfold_metas(scope, arg_expr)),
+                        head_expr,
+                        self.unfold_metas(scope, arg_expr),
                     )),
                     TermOrValue::Value(head_expr) => {
                         let arg_expr = self.eval(arg_expr);
@@ -985,28 +987,29 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
             }
             Term::RecordProj(span, head_expr, label) => {
                 match self.unfold_meta_var_spines(scope, head_expr) {
-                    TermOrValue::Term(head_expr) => TermOrValue::Term(Term::RecordProj(
-                        *span,
-                        scope.to_scope(head_expr),
-                        *label,
-                    )),
+                    TermOrValue::Term(head_expr) => {
+                        TermOrValue::Term(builder.record_proj(*span, head_expr, *label))
+                    }
                     TermOrValue::Value(head_expr) => {
                         TermOrValue::Value(self.elim_env.record_proj(head_expr, *label))
                     }
                 }
             }
             Term::ConstMatch(span, head_expr, branches, default_branch) => {
                 match self.unfold_meta_var_spines(scope, head_expr) {
-                    TermOrValue::Term(head_expr) => TermOrValue::Term(Term::ConstMatch(
-                        *span,
-                        scope.to_scope(head_expr),
-                        scope.to_scope_from_iter(
-                            (branches.iter())
-                                .map(|(r#const, expr)| (*r#const, self.unfold_metas(scope, expr))),
+                    TermOrValue::Term(head_expr) => TermOrValue::Term(
+                        builder.const_match(
+                            *span,
+                            head_expr,
+                            scope.to_scope_from_iter(
+                                branches.iter().map(|(r#const, expr)| {
+                                    (*r#const, self.unfold_metas(scope, expr))
+                                }),
+                            ),
+                            default_branch
+                                .map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
                         ),
-                        default_branch
-                            .map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
-                    )),
+                    ),
                     TermOrValue::Value(head_expr) => {
                         let branches =
                             Branches::new(self.local_exprs.clone(), branches, *default_branch);
@@ -1023,14 +1026,14 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
         &mut self,
         scope: &'out_arena Scope<'out_arena>,
         term: &Term<'arena>,
-    ) -> &'out_arena Term<'out_arena> {
+    ) -> Term<'out_arena> {
         let var = Arc::new(Value::local_var(self.local_exprs.len().next_level()));
 
         self.local_exprs.push(Spanned::empty(var));
         let term = self.unfold_metas(scope, term);
         self.local_exprs.pop();
 
-        scope.to_scope(term)
+        term
     }
 
     fn unfold_telescope_metas<'out_arena>(

fathom/src/core/prim.rs

@@ -54,6 +54,16 @@ impl Index {
     pub const fn prev(self) -> Index {
         Index(self.0 + 1)
     }
+
+    /// An iterator over indices, listed from the most recently bound.
+    pub fn iter() -> impl Iterator<Item = Self> {
+        (0..).map(Self)
+    }
+
+    /// An iterator over indices, listed from `self`
+    pub fn iter_from(self) -> impl Iterator<Item = Self> {
+        (self.0..).map(Self)
+    }
 }
 
 impl fmt::Debug for Index {
@@ -70,11 +80,6 @@ impl fmt::Display for Index {
     }
 }
 
-/// An iterator over indices, listed from the most recently bound.
-pub fn indices() -> impl Iterator<Item = Index> {
-    (0..).map(Index)
-}
-
 /// A de Bruijn level, which represents a variable by counting the number of
 /// binders between the binder that introduced the variable and the start of the
 /// environment. For example:
@@ -101,6 +106,16 @@ impl Level {
     pub const fn next(self) -> Level {
         Level(self.0 + 1)
     }
+
+    /// An iterator over levels, listed from the least recently bound.
+    pub fn iter() -> impl Iterator<Item = Self> {
+        (0..).map(Self)
+    }
+
+    /// An iterator over levels, listed from `self`
+    pub fn iter_from(self) -> impl Iterator<Item = Self> {
+        (self.0..).map(Self)
+    }
 }
 
 impl fmt::Debug for Level {
@@ -117,11 +132,6 @@ impl fmt::Display for Level {
     }
 }
 
-/// An iterator over levels, listed from the least recently bound.
-pub fn levels() -> impl Iterator<Item = Level> {
-    (0..).map(Level)
-}
-
 /// The length of an environment.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
 pub struct EnvLen(RawVar);
@@ -270,11 +280,12 @@ impl<Entry> SliceEnv<Entry> {
 
 impl<Entry: PartialEq> SliceEnv<Entry> {
     pub fn elem_level(&self, entry: &Entry) -> Option<Level> {
-        Iterator::zip(levels(), self.iter()).find_map(|(var, e)| (entry == e).then_some(var))
+        Iterator::zip(Level::iter(), self.iter()).find_map(|(var, e)| (entry == e).then_some(var))
     }
 
     pub fn elem_index(&self, entry: &Entry) -> Option<Index> {
-        Iterator::zip(indices(), self.iter().rev()).find_map(|(var, e)| (entry == e).then_some(var))
+        Iterator::zip(Index::iter(), self.iter().rev())
+            .find_map(|(var, e)| (entry == e).then_some(var))
     }
 }
 

fathom/src/core/semantics.rs

@@ -162,6 +162,12 @@ impl fmt::Debug for ByteRange {
     }
 }
 
+impl From<(BytePos, BytePos)> for ByteRange {
+    fn from((start, end): (BytePos, BytePos)) -> Self {
+        Self { start, end }
+    }
+}
+
 impl ByteRange {
     pub fn new(start: BytePos, end: BytePos) -> ByteRange {
         ByteRange { start, end }