Skip to content

Commit cd34f04

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

34 files changed

+1307
-367
lines changed

‎fathom/src/core.rs

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

68
pub mod binary;
79
pub mod prim;
@@ -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,176 @@ 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+
393+
/// Simple patterns that have had some initial elaboration performed on them
394+
#[derive(Debug, Clone)]
395+
pub enum CheckedPattern<'arena> {
396+
/// Error sentinel
397+
ReportedError(ByteRange),
398+
/// Placeholder patterns that match everything
399+
Placeholder(ByteRange),
400+
/// Pattern that binds local variable
401+
Binder(ByteRange, StringId),
402+
/// Constant literals
403+
ConstLit(ByteRange, Const),
404+
/// Record literals
405+
RecordLit(ByteRange, &'arena [StringId], &'arena [Self]),
406+
}
407+
408+
impl<'arena> CheckedPattern<'arena> {
409+
pub fn range(&self) -> ByteRange {
410+
match self {
411+
CheckedPattern::ReportedError(range)
412+
| CheckedPattern::Placeholder(range)
413+
| CheckedPattern::Binder(range, _)
414+
| CheckedPattern::ConstLit(range, _)
415+
| CheckedPattern::RecordLit(range, _, _) => *range,
416+
}
417+
}
418+
419+
pub fn name(&self) -> Option<StringId> {
420+
match self {
421+
CheckedPattern::Binder(_, name) => Some(*name),
422+
_ => None,
423+
}
424+
}
425+
426+
pub fn is_infalliable(&self) -> bool {
427+
match self {
428+
CheckedPattern::ReportedError(_)
429+
| CheckedPattern::Placeholder(_)
430+
| CheckedPattern::Binder(_, _) => true,
431+
CheckedPattern::ConstLit(_, _) | CheckedPattern::RecordLit(_, _, _) => false,
432+
}
433+
}
258434
}
259435

260436
macro_rules! def_prims {
@@ -571,6 +747,18 @@ pub enum Const {
571747
Pos(usize),
572748
Ref(usize),
573749
}
750+
impl Const {
751+
pub fn num_variants(&self) -> Option<u128> {
752+
match self {
753+
Const::Bool(_) => Some(2),
754+
Const::U8(_, _) | Const::S8(_) => Some(u8::MAX as u128 + 1),
755+
Const::U16(_, _) | Const::S16(_) => Some(u16::MAX as u128 + 1),
756+
Const::U32(_, _) | Const::S32(_) => Some(u32::MAX as u128 + 1),
757+
Const::U64(_, _) | Const::S64(_) => Some(u64::MAX as u128 + 1),
758+
Const::F32(_) | Const::F64(_) | Const::Pos(_) | Const::Ref(_) => None,
759+
}
760+
}
761+
}
574762

575763
impl PartialEq for Const {
576764
fn eq(&self, other: &Self) -> bool {

‎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: 60 additions & 11 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),
@@ -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),
@@ -775,12 +816,20 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
775816
fn match_if_then_else<'arena>(
776817
branches: &'arena [(Const, core::Term<'arena>)],
777818
default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>,
778-
) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> {
819+
) -> Option<(
820+
(Option<Option<StringId>>, &'arena core::Term<'arena>),
821+
(Option<Option<StringId>>, &'arena core::Term<'arena>),
822+
)> {
779823
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)),
824+
([(Const::Bool(false), else_expr), (Const::Bool(true), then_expr)], None) => {
825+
Some(((None, then_expr), (None, else_expr)))
826+
}
827+
([(Const::Bool(true), then_expr)], Some((name, else_expr))) => {
828+
Some(((None, then_expr), (Some(name), else_expr)))
829+
}
830+
([(Const::Bool(false), else_expr)], Some((name, then_expr))) => {
831+
Some(((Some(name), then_expr), (None, else_expr)))
832+
}
784833
_ => None,
785834
}
786835
}

0 commit comments

Comments
 (0)