Use new pattern match compiler and coverage checker

fathom/src/core.rs

@@ -1,6 +1,8 @@
 //! Core language.
 
-use crate::env::{Index, Level};
+use scoped_arena::Scope;
+
+use crate::env::{EnvLen, Index, Level};
 use crate::source::{Span, StringId};
 
 pub mod binary;
@@ -185,6 +187,10 @@ pub enum Term<'arena> {
 }
 
 impl<'arena> Term<'arena> {
+    pub fn error(span: Span) -> Self {
+        Self::Prim(span, Prim::ReportedError)
+    }
+
     /// Get the source span of the term.
     pub fn span(&self) -> Span {
         match self {
@@ -255,6 +261,149 @@ impl<'arena> Term<'arena> {
             }
         }
     }
+
+    // TODO: Add a new `Weaken` variant to `core::Term` instead of eagerly traversing the term?
+    pub fn shift(&self, scope: &'arena Scope<'arena>, amount: EnvLen) -> Term<'arena> {
+        self.shift_inner(scope, Index::last(), amount)
+    }
+
+    /// Increment all `LocalVar`s greater than or equal to `min` by `amount`
+    fn shift_inner(
+        &self,
+        scope: &'arena Scope<'arena>,
+        mut min: Index,
+        amount: EnvLen,
+    ) -> Term<'arena> {
+        // Skip traversing and rebuilding the term if it would make no change. Increases sharing.
+        if amount == EnvLen::new() {
+            return self.clone();
+        }
+
+        match self {
+            Term::LocalVar(span, var) if *var >= min => Term::LocalVar(*span, *var + amount),
+            Term::LocalVar(..)
+            | Term::ItemVar(..)
+            | Term::MetaVar(..)
+            | Term::InsertedMeta(..)
+            | Term::Prim(..)
+            | Term::ConstLit(..)
+            | Term::Universe(..) => self.clone(),
+            Term::Ann(span, expr, r#type) => Term::Ann(
+                *span,
+                scope.to_scope(expr.shift_inner(scope, min, amount)),
+                scope.to_scope(r#type.shift_inner(scope, min, amount)),
+            ),
+            Term::Let(span, name, def_type, def_expr, body) => Term::Let(
+                *span,
+                *name,
+                scope.to_scope(def_type.shift_inner(scope, min, amount)),
+                scope.to_scope(def_expr.shift_inner(scope, min, amount)),
+                scope.to_scope(body.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FunType(span, name, input, output) => Term::FunType(
+                *span,
+                *name,
+                scope.to_scope(input.shift_inner(scope, min, amount)),
+                scope.to_scope(output.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FunLit(span, name, body) => Term::FunLit(
+                *span,
+                *name,
+                scope.to_scope(body.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FunApp(span, fun, arg) => Term::FunApp(
+                *span,
+                scope.to_scope(fun.shift_inner(scope, min, amount)),
+                scope.to_scope(arg.shift_inner(scope, min, amount)),
+            ),
+            Term::RecordType(span, labels, types) => Term::RecordType(
+                *span,
+                labels,
+                scope.to_scope_from_iter(types.iter().map(|r#type| {
+                    let ret = r#type.shift_inner(scope, min, amount);
+                    min = min.prev();
+                    ret
+                })),
+            ),
+            Term::RecordLit(span, labels, exprs) => Term::RecordLit(
+                *span,
+                labels,
+                scope.to_scope_from_iter(
+                    exprs
+                        .iter()
+                        .map(|expr| expr.shift_inner(scope, min, amount)),
+                ),
+            ),
+            Term::RecordProj(span, head, label) => Term::RecordProj(
+                *span,
+                scope.to_scope(head.shift_inner(scope, min, amount)),
+                *label,
+            ),
+            Term::ArrayLit(span, terms) => Term::ArrayLit(
+                *span,
+                scope.to_scope_from_iter(
+                    terms
+                        .iter()
+                        .map(|term| term.shift_inner(scope, min, amount)),
+                ),
+            ),
+            Term::FormatRecord(span, labels, terms) => Term::FormatRecord(
+                *span,
+                labels,
+                scope.to_scope_from_iter(terms.iter().map(|term| {
+                    let ret = term.shift_inner(scope, min, amount);
+                    min = min.prev();
+                    ret
+                })),
+            ),
+            Term::FormatCond(span, name, format, pred) => Term::FormatCond(
+                *span,
+                *name,
+                scope.to_scope(format.shift_inner(scope, min, amount)),
+                scope.to_scope(pred.shift_inner(scope, min.prev(), amount)),
+            ),
+            Term::FormatOverlap(span, labels, terms) => Term::FormatOverlap(
+                *span,
+                labels,
+                scope.to_scope_from_iter(terms.iter().map(|term| {
+                    let ret = term.shift_inner(scope, min, amount);
+                    min = min.prev();
+                    ret
+                })),
+            ),
+            Term::ConstMatch(span, scrut, branches, default) => Term::ConstMatch(
+                *span,
+                scope.to_scope(scrut.shift_inner(scope, min, amount)),
+                scope.to_scope_from_iter(
+                    branches
+                        .iter()
+                        .map(|(r#const, term)| (*r#const, term.shift_inner(scope, min, amount))),
+                ),
+                default.map(|(name, term)| {
+                    (
+                        name,
+                        scope.to_scope(term.shift_inner(scope, min.prev(), amount)) as &_,
+                    )
+                }),
+            ),
+        }
+    }
+
+    /// Returns `true` if `self` can be evaluated in a single step.
+    /// Used as a heuristic to prevent increase in runtime when expanding pattern matches
+    pub fn is_atomic(&self) -> bool {
+        match self {
+            Term::ItemVar(_, _)
+            | Term::LocalVar(_, _)
+            | Term::MetaVar(_, _)
+            | Term::InsertedMeta(_, _, _)
+            | Term::Universe(_)
+            | Term::Prim(_, _)
+            | Term::ConstLit(_, _) => true,
+            Term::RecordProj(_, head, _) => head.is_atomic(),
+            _ => false,
+        }
+    }
 }
 
 macro_rules! def_prims {
@@ -572,6 +721,21 @@ pub enum Const {
     Ref(usize),
 }
 
+impl Const {
+    /// Return the number of inhabitants of `self`.
+    /// `None` represents infinity
+    pub fn num_inhabitants(&self) -> Option<u128> {
+        match self {
+            Const::Bool(_) => Some(2),
+            Const::U8(_, _) | Const::S8(_) => Some(1 << 8),
+            Const::U16(_, _) | Const::S16(_) => Some(1 << 16),
+            Const::U32(_, _) | Const::S32(_) => Some(1 << 32),
+            Const::U64(_, _) | Const::S64(_) => Some(1 << 64),
+            Const::F32(_) | Const::F64(_) | Const::Pos(_) | Const::Ref(_) => None,
+        }
+    }
+}
+
 impl PartialEq for Const {
     fn eq(&self, other: &Self) -> bool {
         match (*self, *other) {

fathom/src/core/semantics.rs

@@ -52,6 +52,8 @@ pub enum Value<'arena> {
 }
 
 impl<'arena> Value<'arena> {
+    pub const ERROR: Self = Self::Stuck(Head::Prim(Prim::ReportedError), Vec::new());
+
     pub fn prim(prim: Prim, params: impl IntoIterator<Item = ArcValue<'arena>>) -> Value<'arena> {
         let params = params.into_iter().map(Elim::FunApp).collect();
         Value::Stuck(Head::Prim(prim), params)
@@ -71,6 +73,13 @@ impl<'arena> Value<'arena> {
             _ => None,
         }
     }
+
+    pub fn as_record_type(&self) -> Option<&Telescope<'arena>> {
+        match self {
+            Value::RecordType(_, telescope) => Some(telescope),
+            _ => None,
+        }
+    }
 }
 
 /// The head of a [stuck value][Value::Stuck].

fathom/src/env.rs

@@ -17,7 +17,7 @@
 //! and [`SliceEnv`], but when we need to copy environments often, we use a
 //! [`SharedEnv`] to increase the amount of sharing at the expense of locality.
 
-use std::fmt;
+use std::{fmt, ops::Add};
 
 /// Underlying variable representation.
 type RawVar = u16;
@@ -56,6 +56,13 @@ impl Index {
     }
 }
 
+impl Add<EnvLen> for Index {
+    type Output = Self;
+    fn add(self, rhs: EnvLen) -> Self::Output {
+        Self(self.0 + rhs.0) // FIXME: check overflow?
+    }
+}
+
 impl fmt::Debug for Index {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         write!(f, "Index(")?;
@@ -140,6 +147,10 @@ impl EnvLen {
         Level(self.0)
     }
 
+    pub fn next(&self) -> EnvLen {
+        Self(self.0 + 1) // FIXME: check overflow?
+    }
+
     /// Push an entry onto the environment.
     pub fn push(&mut self) {
         self.0 += 1; // FIXME: check overflow?

fathom/src/surface/distillation.rs

@@ -311,11 +311,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                 core::Const::Ref(number) => self.check_number_literal(number),
             },
             core::Term::ConstMatch(_span, head_expr, branches, default_branch) => {
-                if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_branch)
+                if let Some(((then_name, then_expr), (else_name, else_expr))) =
+                    match_if_then_else(branches, *default_branch)
                 {
                     let cond_expr = self.check(head_expr);
-                    let then_expr = self.check(then_expr);
-                    let else_expr = self.check(else_expr);
+
+                    let then_expr = match then_name {
+                        None => self.check(then_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let then_expr = self.check(then_expr);
+                            self.pop_local();
+                            then_expr
+                        }
+                    };
+
+                    let else_expr = match else_name {
+                        None => self.check(else_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let else_expr = self.check(else_expr);
+                            self.pop_local();
+                            else_expr
+                        }
+                    };
+
                     return Term::If(
                         (),
                         self.scope.to_scope(cond_expr),
@@ -373,11 +393,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
         match core_term {
             core::Term::ItemVar(_span, var) => match self.get_item_name(*var) {
                 Some(name) => Term::Name((), name),
-                None => todo!("misbound variable"), // TODO: error?
+                None => panic!("misbound item variable: {var:?}"),
             },
             core::Term::LocalVar(_span, var) => match self.get_local_name(*var) {
                 Some(name) => Term::Name((), name),
-                None => todo!("misbound variable"), // TODO: error?
+                None => panic!("Unbound local variable: {var:?}"),
             },
             core::Term::MetaVar(_span, var) => match self.get_hole_name(*var) {
                 Some(name) => Term::Hole((), name),
@@ -643,10 +663,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
                 core::Const::Ref(number) => self.synth_number_literal(number, core::Prim::RefType),
             },
             core::Term::ConstMatch(_span, head_expr, branches, default_expr) => {
-                if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_expr) {
+                if let Some(((then_name, then_expr), (else_name, else_expr))) =
+                    match_if_then_else(branches, *default_expr)
+                {
                     let cond_expr = self.check(head_expr);
-                    let then_expr = self.synth(then_expr);
-                    let else_expr = self.synth(else_expr);
+
+                    let then_expr = match then_name {
+                        None => self.synth(then_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let then_expr = self.synth(then_expr);
+                            self.pop_local();
+                            then_expr
+                        }
+                    };
+
+                    let else_expr = match else_name {
+                        None => self.synth(else_expr),
+                        Some(name) => {
+                            self.push_local(name);
+                            let else_expr = self.synth(else_expr);
+                            self.pop_local();
+                            else_expr
+                        }
+                    };
+
                     return Term::If(
                         (),
                         self.scope.to_scope(cond_expr),
@@ -772,15 +813,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
     }
 }
 
+#[allow(clippy::type_complexity)]
 fn match_if_then_else<'arena>(
     branches: &'arena [(Const, core::Term<'arena>)],
     default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>,
-) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> {
+) -> Option<(
+    (Option<Option<StringId>>, &'arena core::Term<'arena>),
+    (Option<Option<StringId>>, &'arena core::Term<'arena>),
+)> {
     match (branches, default_branch) {
-        ([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None)
-        // TODO: Normalise boolean branches when elaborating patterns
-        | ([(Const::Bool(true), then_expr)], Some((_, else_expr)))
-        | ([(Const::Bool(false), else_expr)], Some((_, then_expr))) => Some((then_expr, else_expr)),
+        ([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None) => {
+            Some(((None, then_expr), (None, else_expr)))
+        }
+        ([(Const::Bool(true), then_expr)], Some((name, else_expr))) => {
+            Some(((None, then_expr), (Some(name), else_expr)))
+        }
+        ([(Const::Bool(false), else_expr)], Some((name, then_expr))) => {
+            Some(((Some(name), then_expr), (None, else_expr)))
+        }
         _ => None,
     }
 }