Skip to content

Commit c31c1d1

Browse files
KmeakinKmeakin
committed
Use new pattern match compiler and coverage checker
1 parent 2f7e6a8 commit c31c1d1

34 files changed

+1474
-375
lines changed

‎fathom/src/core.rs

Lines changed: 165 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
//! Core language.
22
3-
use crate::env::{Index, Level};
3+
use scoped_arena::Scope;
4+
5+
use crate::env::{EnvLen, Index, Level};
46
use crate::source::{Span, StringId};
57

68
pub mod binary;
@@ -185,6 +187,10 @@ pub enum Term<'arena> {
185187
}
186188

187189
impl<'arena> Term<'arena> {
190+
pub fn error(span: Span) -> Self {
191+
Self::Prim(span, Prim::ReportedError)
192+
}
193+
188194
/// Get the source span of the term.
189195
pub fn span(&self) -> Span {
190196
match self {
@@ -255,6 +261,149 @@ impl<'arena> Term<'arena> {
255261
}
256262
}
257263
}
264+
265+
// TODO: Add a new `Weaken` variant to `core::Term` instead of eagerly traversing the term?
266+
pub fn shift(&self, scope: &'arena Scope<'arena>, amount: EnvLen) -> Term<'arena> {
267+
self.shift_inner(scope, Index::last(), amount)
268+
}
269+
270+
/// Increment all `LocalVar`s greater than or equal to `min` by `amount`
271+
fn shift_inner(
272+
&self,
273+
scope: &'arena Scope<'arena>,
274+
mut min: Index,
275+
amount: EnvLen,
276+
) -> Term<'arena> {
277+
// Skip traversing and rebuilding the term if it would make no change. Increases sharing.
278+
if amount == EnvLen::new() {
279+
return self.clone();
280+
}
281+
282+
match self {
283+
Term::LocalVar(span, var) if *var >= min => Term::LocalVar(*span, *var + amount),
284+
Term::LocalVar(..)
285+
| Term::ItemVar(..)
286+
| Term::MetaVar(..)
287+
| Term::InsertedMeta(..)
288+
| Term::Prim(..)
289+
| Term::ConstLit(..)
290+
| Term::Universe(..) => self.clone(),
291+
Term::Ann(span, expr, r#type) => Term::Ann(
292+
*span,
293+
scope.to_scope(expr.shift_inner(scope, min, amount)),
294+
scope.to_scope(r#type.shift_inner(scope, min, amount)),
295+
),
296+
Term::Let(span, name, def_type, def_expr, body) => Term::Let(
297+
*span,
298+
*name,
299+
scope.to_scope(def_type.shift_inner(scope, min, amount)),
300+
scope.to_scope(def_expr.shift_inner(scope, min, amount)),
301+
scope.to_scope(body.shift_inner(scope, min.prev(), amount)),
302+
),
303+
Term::FunType(span, name, input, output) => Term::FunType(
304+
*span,
305+
*name,
306+
scope.to_scope(input.shift_inner(scope, min, amount)),
307+
scope.to_scope(output.shift_inner(scope, min.prev(), amount)),
308+
),
309+
Term::FunLit(span, name, body) => Term::FunLit(
310+
*span,
311+
*name,
312+
scope.to_scope(body.shift_inner(scope, min.prev(), amount)),
313+
),
314+
Term::FunApp(span, fun, arg) => Term::FunApp(
315+
*span,
316+
scope.to_scope(fun.shift_inner(scope, min, amount)),
317+
scope.to_scope(arg.shift_inner(scope, min, amount)),
318+
),
319+
Term::RecordType(span, labels, types) => Term::RecordType(
320+
*span,
321+
labels,
322+
scope.to_scope_from_iter(types.iter().map(|r#type| {
323+
let ret = r#type.shift_inner(scope, min, amount);
324+
min = min.prev();
325+
ret
326+
})),
327+
),
328+
Term::RecordLit(span, labels, exprs) => Term::RecordLit(
329+
*span,
330+
labels,
331+
scope.to_scope_from_iter(
332+
exprs
333+
.iter()
334+
.map(|expr| expr.shift_inner(scope, min, amount)),
335+
),
336+
),
337+
Term::RecordProj(span, head, label) => Term::RecordProj(
338+
*span,
339+
scope.to_scope(head.shift_inner(scope, min, amount)),
340+
*label,
341+
),
342+
Term::ArrayLit(span, terms) => Term::ArrayLit(
343+
*span,
344+
scope.to_scope_from_iter(
345+
terms
346+
.iter()
347+
.map(|term| term.shift_inner(scope, min, amount)),
348+
),
349+
),
350+
Term::FormatRecord(span, labels, terms) => Term::FormatRecord(
351+
*span,
352+
labels,
353+
scope.to_scope_from_iter(terms.iter().map(|term| {
354+
let ret = term.shift_inner(scope, min, amount);
355+
min = min.prev();
356+
ret
357+
})),
358+
),
359+
Term::FormatCond(span, name, format, pred) => Term::FormatCond(
360+
*span,
361+
*name,
362+
scope.to_scope(format.shift_inner(scope, min, amount)),
363+
scope.to_scope(pred.shift_inner(scope, min.prev(), amount)),
364+
),
365+
Term::FormatOverlap(span, labels, terms) => Term::FormatOverlap(
366+
*span,
367+
labels,
368+
scope.to_scope_from_iter(terms.iter().map(|term| {
369+
let ret = term.shift_inner(scope, min, amount);
370+
min = min.prev();
371+
ret
372+
})),
373+
),
374+
Term::ConstMatch(span, scrut, branches, default) => Term::ConstMatch(
375+
*span,
376+
scope.to_scope(scrut.shift_inner(scope, min, amount)),
377+
scope.to_scope_from_iter(
378+
branches
379+
.iter()
380+
.map(|(r#const, term)| (*r#const, term.shift_inner(scope, min, amount))),
381+
),
382+
default.map(|(name, term)| {
383+
(
384+
name,
385+
scope.to_scope(term.shift_inner(scope, min.prev(), amount)) as &_,
386+
)
387+
}),
388+
),
389+
}
390+
}
391+
392+
/// Returns `true` if `self` can be evaluated in a single step.
393+
/// Used as a heuristic to prevent increase in runtime when expanding pattern matches
394+
pub fn is_atomic(&self) -> bool {
395+
match self {
396+
Term::ItemVar(_, _)
397+
| Term::LocalVar(_, _)
398+
| Term::MetaVar(_, _)
399+
| Term::InsertedMeta(_, _, _)
400+
| Term::Universe(_)
401+
| Term::Prim(_, _)
402+
| Term::ConstLit(_, _) => true,
403+
Term::RecordProj(_, head, _) => head.is_atomic(),
404+
_ => false,
405+
}
406+
}
258407
}
259408

260409
macro_rules! def_prims {
@@ -572,6 +721,21 @@ pub enum Const {
572721
Ref(usize),
573722
}
574723

724+
impl Const {
725+
/// Return the number of inhabitants of `self`.
726+
/// `None` represents infinity
727+
pub fn num_inhabitants(&self) -> Option<u128> {
728+
match self {
729+
Const::Bool(_) => Some(2),
730+
Const::U8(_, _) | Const::S8(_) => Some(1 << 8),
731+
Const::U16(_, _) | Const::S16(_) => Some(1 << 16),
732+
Const::U32(_, _) | Const::S32(_) => Some(1 << 32),
733+
Const::U64(_, _) | Const::S64(_) => Some(1 << 64),
734+
Const::F32(_) | Const::F64(_) | Const::Pos(_) | Const::Ref(_) => None,
735+
}
736+
}
737+
}
738+
575739
impl PartialEq for Const {
576740
fn eq(&self, other: &Self) -> bool {
577741
match (*self, *other) {

‎fathom/src/core/semantics.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ pub enum Value<'arena> {
5252
}
5353

5454
impl<'arena> Value<'arena> {
55+
pub const ERROR: Self = Self::Stuck(Head::Prim(Prim::ReportedError), Vec::new());
56+
5557
pub fn prim(prim: Prim, params: impl IntoIterator<Item = ArcValue<'arena>>) -> Value<'arena> {
5658
let params = params.into_iter().map(Elim::FunApp).collect();
5759
Value::Stuck(Head::Prim(prim), params)
@@ -71,6 +73,13 @@ impl<'arena> Value<'arena> {
7173
_ => None,
7274
}
7375
}
76+
77+
pub fn as_record_type(&self) -> Option<&Telescope<'arena>> {
78+
match self {
79+
Value::RecordType(_, telescope) => Some(telescope),
80+
_ => None,
81+
}
82+
}
7483
}
7584

7685
/// The head of a [stuck value][Value::Stuck].

‎fathom/src/env.rs

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
//! and [`SliceEnv`], but when we need to copy environments often, we use a
1818
//! [`SharedEnv`] to increase the amount of sharing at the expense of locality.
1919
20-
use std::fmt;
20+
use std::{fmt, ops::Add};
2121

2222
/// Underlying variable representation.
2323
type RawVar = u16;
@@ -56,6 +56,13 @@ impl Index {
5656
}
5757
}
5858

59+
impl Add<EnvLen> for Index {
60+
type Output = Self;
61+
fn add(self, rhs: EnvLen) -> Self::Output {
62+
Self(self.0 + rhs.0) // FIXME: check overflow?
63+
}
64+
}
65+
5966
impl fmt::Debug for Index {
6067
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
6168
write!(f, "Index(")?;
@@ -140,6 +147,10 @@ impl EnvLen {
140147
Level(self.0)
141148
}
142149

150+
pub fn next(&self) -> EnvLen {
151+
Self(self.0 + 1) // FIXME: check overflow?
152+
}
153+
143154
/// Push an entry onto the environment.
144155
pub fn push(&mut self) {
145156
self.0 += 1; // FIXME: check overflow?

‎fathom/src/surface/distillation.rs

Lines changed: 63 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -311,11 +311,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
311311
core::Const::Ref(number) => self.check_number_literal(number),
312312
},
313313
core::Term::ConstMatch(_span, head_expr, branches, default_branch) => {
314-
if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_branch)
314+
if let Some(((then_name, then_expr), (else_name, else_expr))) =
315+
match_if_then_else(branches, *default_branch)
315316
{
316317
let cond_expr = self.check(head_expr);
317-
let then_expr = self.check(then_expr);
318-
let else_expr = self.check(else_expr);
318+
319+
let then_expr = match then_name {
320+
None => self.check(then_expr),
321+
Some(name) => {
322+
self.push_local(name);
323+
let then_expr = self.check(then_expr);
324+
self.pop_local();
325+
then_expr
326+
}
327+
};
328+
329+
let else_expr = match else_name {
330+
None => self.check(else_expr),
331+
Some(name) => {
332+
self.push_local(name);
333+
let else_expr = self.check(else_expr);
334+
self.pop_local();
335+
else_expr
336+
}
337+
};
338+
319339
return Term::If(
320340
(),
321341
self.scope.to_scope(cond_expr),
@@ -373,11 +393,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
373393
match core_term {
374394
core::Term::ItemVar(_span, var) => match self.get_item_name(*var) {
375395
Some(name) => Term::Name((), name),
376-
None => todo!("misbound variable"), // TODO: error?
396+
None => panic!("misbound item variable: {var:?}"),
377397
},
378398
core::Term::LocalVar(_span, var) => match self.get_local_name(*var) {
379399
Some(name) => Term::Name((), name),
380-
None => todo!("misbound variable"), // TODO: error?
400+
None => panic!("Unbound local variable: {var:?}"),
381401
},
382402
core::Term::MetaVar(_span, var) => match self.get_hole_name(*var) {
383403
Some(name) => Term::Hole((), name),
@@ -643,10 +663,31 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
643663
core::Const::Ref(number) => self.synth_number_literal(number, core::Prim::RefType),
644664
},
645665
core::Term::ConstMatch(_span, head_expr, branches, default_expr) => {
646-
if let Some((then_expr, else_expr)) = match_if_then_else(branches, *default_expr) {
666+
if let Some(((then_name, then_expr), (else_name, else_expr))) =
667+
match_if_then_else(branches, *default_expr)
668+
{
647669
let cond_expr = self.check(head_expr);
648-
let then_expr = self.synth(then_expr);
649-
let else_expr = self.synth(else_expr);
670+
671+
let then_expr = match then_name {
672+
None => self.synth(then_expr),
673+
Some(name) => {
674+
self.push_local(name);
675+
let then_expr = self.synth(then_expr);
676+
self.pop_local();
677+
then_expr
678+
}
679+
};
680+
681+
let else_expr = match else_name {
682+
None => self.synth(else_expr),
683+
Some(name) => {
684+
self.push_local(name);
685+
let else_expr = self.synth(else_expr);
686+
self.pop_local();
687+
else_expr
688+
}
689+
};
690+
650691
return Term::If(
651692
(),
652693
self.scope.to_scope(cond_expr),
@@ -772,15 +813,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
772813
}
773814
}
774815

816+
#[allow(clippy::type_complexity)]
775817
fn match_if_then_else<'arena>(
776818
branches: &'arena [(Const, core::Term<'arena>)],
777819
default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>,
778-
) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> {
820+
) -> Option<(
821+
(Option<Option<StringId>>, &'arena core::Term<'arena>),
822+
(Option<Option<StringId>>, &'arena core::Term<'arena>),
823+
)> {
779824
match (branches, default_branch) {
780-
([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None)
781-
// TODO: Normalise boolean branches when elaborating patterns
782-
| ([(Const::Bool(true), then_expr)], Some((_, else_expr)))
783-
| ([(Const::Bool(false), else_expr)], Some((_, then_expr))) => Some((then_expr, else_expr)),
825+
([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None) => {
826+
Some(((None, then_expr), (None, else_expr)))
827+
}
828+
([(Const::Bool(true), then_expr)], Some((name, else_expr))) => {
829+
Some(((None, then_expr), (Some(name), else_expr)))
830+
}
831+
([(Const::Bool(false), else_expr)], Some((name, then_expr))) => {
832+
Some(((Some(name), then_expr), (None, else_expr)))
833+
}
784834
_ => None,
785835
}
786836
}

0 commit comments

Comments
 (0)