Skip to content

Commit

Permalink
Switch to an explicitly typed core language
Browse files Browse the repository at this point in the history
  • Loading branch information
@brendanzab
brendanzab committed Jan 23, 2023
1 parent 289c397 commit cff2b4c
Show file tree
Hide file tree
Showing 84 changed files with 1,096 additions and 1,020 deletions.
51 changes: 26 additions & 25 deletions fathom/src/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,15 +140,12 @@ pub enum Term<'arena> {
// - https://lib.rs/crates/smallbitvec
// - https://lib.rs/crates/bit-vec
InsertedMeta(Span, Level, &'arena [LocalInfo]),
/// Annotated expressions.
Ann(Span, &'arena Term<'arena>, &'arena Term<'arena>),
/// Let expressions.
Let(
Span,
Option<StringId>,
&'arena Term<'arena>,
&'arena Term<'arena>,
&'arena Term<'arena>,
),

/// The type of types.
Expand All @@ -167,7 +164,13 @@ pub enum Term<'arena> {
/// Function literals.
///
/// Also known as: lambda expressions, anonymous functions.
FunLit(Span, Plicity, Option<StringId>, &'arena Term<'arena>),
FunLit(
Span,
Plicity,
Option<StringId>,
&'arena Term<'arena>,
&'arena Term<'arena>,
),
/// Function applications.
FunApp(Span, Plicity, &'arena Term<'arena>, &'arena Term<'arena>),

Expand Down Expand Up @@ -208,26 +211,25 @@ impl<'arena> Term<'arena> {
/// Get the source span of the term.
pub fn span(&self) -> Span {
match self {
Term::ItemVar(span, _)
| Term::LocalVar(span, _)
| Term::MetaVar(span, _)
| Term::InsertedMeta(span, _, _)
| Term::Ann(span, _, _)
| Term::Let(span, _, _, _, _)
Term::ItemVar(span, ..)
| Term::LocalVar(span, ..)
| Term::MetaVar(span, ..)
| Term::InsertedMeta(span, ..)
| Term::Let(span, ..)
| Term::Universe(span)
| Term::FunType(span, ..)
| Term::FunLit(span, ..)
| Term::FunApp(span, ..)
| Term::RecordType(span, _, _)
| Term::RecordLit(span, _, _)
| Term::RecordProj(span, _, _)
| Term::RecordType(span, ..)
| Term::RecordLit(span, ..)
| Term::RecordProj(span, ..)
| Term::ArrayLit(span, _)
| Term::FormatRecord(span, _, _)
| Term::FormatCond(span, _, _, _)
| Term::FormatOverlap(span, _, _)
| Term::Prim(span, _)
| Term::ConstLit(span, _)
| Term::ConstMatch(span, _, _, _) => *span,
| Term::FormatRecord(span, ..)
| Term::FormatCond(span, ..)
| Term::FormatOverlap(span, ..)
| Term::Prim(span, ..)
| Term::ConstLit(span, ..)
| Term::ConstMatch(span, ..) => *span,
}
}

Expand All @@ -242,16 +244,15 @@ impl<'arena> Term<'arena> {
| Term::Prim(_, _)
| Term::ConstLit(_, _) => false,

Term::Ann(_, expr, r#type) => expr.binds_local(var) || r#type.binds_local(var),
Term::Let(_, _, def_type, def_expr, body_expr) => {
def_type.binds_local(var)
|| def_expr.binds_local(var)
|| body_expr.binds_local(var.prev())
Term::Let(_, _, def_expr, body_expr) => {
def_expr.binds_local(var) || body_expr.binds_local(var.prev())
}
Term::FunType(.., param_type, body_type) => {
param_type.binds_local(var) || body_type.binds_local(var.prev())
}
Term::FunLit(.., body_expr) => body_expr.binds_local(var.prev()),
Term::FunLit(.., param_type, body_expr) => {
param_type.binds_local(var) || body_expr.binds_local(var.prev())
}
Term::FunApp(.., head_expr, arg_expr) => {
head_expr.binds_local(var) || arg_expr.binds_local(var)
}
Expand Down
41 changes: 20 additions & 21 deletions fathom/src/core/pretty.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,26 +137,13 @@ impl<'interner, 'arena> Context<'interner> {
Term::InsertedMeta(_, level, info) => {
RcDoc::text(format!("InsertedMeta({level:?}, {info:?})"))
}
Term::Ann(_, expr, r#type) => self.paren(
prec > Prec::Top,
RcDoc::concat([
RcDoc::concat([
self.term_prec(Prec::Let, expr),
RcDoc::space(),
RcDoc::text(":"),
])
.group(),
RcDoc::softline(),
self.term_prec(Prec::Top, r#type),
]),
),
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren(
Term::Let(_, def_pattern, def_expr, 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.pattern(*def_pattern),
RcDoc::space(),
RcDoc::text("="),
RcDoc::softline(),
Expand Down Expand Up @@ -201,17 +188,29 @@ impl<'interner, 'arena> Context<'interner> {
self.term_prec(Prec::Fun, body_type),
]),
),
Term::FunLit(_, plicity, param_name, body_expr) => self.paren(
Term::FunLit(_, plicity, param_name, param_type, body_expr) => self.paren(
prec > Prec::Fun,
RcDoc::concat([
RcDoc::concat([
RcDoc::text("fun"),
RcDoc::space(),
self.plicity(*plicity),
match param_name {
Some(name) => self.string_id(*name),
None => RcDoc::text("_"),
},
self.paren(
prec > Prec::Top,
RcDoc::concat([
RcDoc::concat([
self.plicity(*plicity),
match param_name {
Some(name) => self.string_id(*name),
None => RcDoc::text("_"),
},
RcDoc::space(),
RcDoc::text(":"),
])
.group(),
RcDoc::softline(),
self.term_prec(Prec::Top, param_type),
]),
),
RcDoc::space(),
RcDoc::text("=>"),
])
Expand Down
37 changes: 19 additions & 18 deletions fathom/src/core/semantics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ pub enum Value<'arena> {
/// Dependent function types.
FunType(Plicity, Option<StringId>, ArcValue<'arena>, Closure<'arena>),
/// Function literals.
FunLit(Plicity, Option<StringId>, Closure<'arena>),
FunLit(Plicity, Option<StringId>, ArcValue<'arena>, Closure<'arena>),

/// Record types.
RecordType(&'arena [StringId], Telescope<'arena>),
Expand Down Expand Up @@ -298,8 +298,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
let head_expr = self.eval(&Term::MetaVar(*span, *var));
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) => {
Term::Let(span, _, def_expr, body_expr) => {
let def_expr = self.eval(def_expr);
self.local_exprs.push(def_expr);
let body_expr = self.eval(body_expr);
Expand All @@ -318,11 +317,12 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
Closure::new(self.local_exprs.clone(), body_type),
)),
),
Term::FunLit(span, plicity, param_name, body_expr) => Spanned::new(
Term::FunLit(span, plicity, param_name, param_type, body_expr) => Spanned::new(
*span,
Arc::new(Value::FunLit(
*plicity,
*param_name,
self.eval(param_type),
Closure::new(self.local_exprs.clone(), body_expr),
)),
),
Expand Down Expand Up @@ -521,7 +521,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
) -> ArcValue<'arena> {
match Arc::make_mut(&mut head_expr) {
// Beta-reduction
Value::FunLit(fun_plicity, _, body_expr) => {
Value::FunLit(fun_plicity, _, _, body_expr) => {
assert_eq!(arg_plicity, *fun_plicity, "Plicities must be equal");
// FIXME: use span from head/arg exprs?
self.apply_closure(body_expr, arg_expr)
Expand Down Expand Up @@ -722,10 +722,11 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
scope.to_scope(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, param_type, body_expr) => Term::FunLit(
span,
*plicity,
*param_name,
scope.to_scope(self.quote(scope, param_type)),
self.quote_closure(scope, body_expr),
),

Expand Down Expand Up @@ -874,15 +875,9 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
Term::InsertedMeta(*span, *var, infos)
}
},
Term::Ann(span, expr, r#type) => Term::Ann(
*span,
scope.to_scope(self.unfold_metas(scope, expr)),
scope.to_scope(self.unfold_metas(scope, r#type)),
),
Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let(
Term::Let(span, def_name, def_expr, body_expr) => Term::Let(
*span,
*def_name,
scope.to_scope(self.unfold_metas(scope, def_type)),
scope.to_scope(self.unfold_metas(scope, def_expr)),
self.unfold_bound_metas(scope, body_expr),
),
Expand All @@ -896,10 +891,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
scope.to_scope(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, param_type, body_expr) => Term::FunLit(
*span,
*plicity,
*param_name,
scope.to_scope(self.unfold_metas(scope, param_type)),
self.unfold_bound_metas(scope, body_expr),
),

Expand Down Expand Up @@ -1117,13 +1113,18 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
&& self.is_equal(param_type0, param_type1)
&& self.is_equal_closures(body_type0, body_type1)
}
(Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) => {
plicity0 == plicity1 && self.is_equal_closures(body_expr0, body_expr1)
(
Value::FunLit(plicity0, _, param_type0, body_expr0),
Value::FunLit(plicity1, _, param_type1, body_expr1),
) => {
plicity0 == plicity1
&& self.is_equal(param_type0, param_type1)
&& self.is_equal_closures(body_expr0, body_expr1)
}
(Value::FunLit(plicity, _, body_expr), _) => {
(Value::FunLit(plicity, .., body_expr), _) => {
self.is_equal_fun_lit(*plicity, body_expr, &value1)
}
(_, Value::FunLit(plicity, _, body_expr)) => {
(_, Value::FunLit(plicity, .., body_expr)) => {
self.is_equal_fun_lit(*plicity, body_expr, &value0)
}

Expand Down
57 changes: 23 additions & 34 deletions fathom/src/surface/distillation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -276,14 +276,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {

fn check_prec(&mut self, prec: Prec, core_term: &core::Term<'_>) -> Term<'arena, ()> {
match core_term {
core::Term::Ann(_span, expr, _) => {
// Avoid adding extraneous type annotations!
self.check_prec(prec, expr)
}
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
let def_type = self.check_prec(Prec::Top, def_type);
let def_expr = self.check_prec(Prec::Let, def_expr);

core::Term::Let(_, def_name, def_expr, body_expr) => {
let def_expr = self.check_prec(Prec::Top, def_expr);
let def_name = self.freshen_name(*def_name, body_expr);
let def_name = self.push_local(def_name);
let def_pattern = name_to_pattern(def_name);
Expand All @@ -295,29 +289,32 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
Term::Let(
(),
def_pattern,
Some(self.scope.to_scope(def_type)),
None,
self.scope.to_scope(def_expr),
self.scope.to_scope(body_expr),
),
)
}
core::Term::FunLit(..) => {
let initial_local_len = self.local_len();

let mut params = Vec::new();
let mut body_expr = core_term;
while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr {
let param_name = self.freshen_name(*param_name, next_body_expr);
params.push((*plicity, self.push_local(param_name)));

while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr {
let r#type = self.check(r#type);
let name = self.freshen_name(*name, next_body_expr);
params.push((*plicity, self.push_local(name), r#type));
body_expr = next_body_expr;
}

let body_expr = self.check_prec(Prec::Let, body_expr);
self.truncate_local(initial_local_len);

let params = params.into_iter().map(|(plicity, name)| Param {
let params = params.into_iter().map(|(plicity, name, r#type)| Param {
plicity,
pattern: name_to_pattern(name),
r#type: None,
r#type: Some(r#type),
});

self.paren(
Expand Down Expand Up @@ -492,30 +489,20 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
self.paren(prec > Prec::App, Term::App((), head_expr, args.into()))
}
}
core::Term::Ann(_span, expr, r#type) => {
let expr = self.check_prec(Prec::Let, expr);
let r#type = self.check_prec(Prec::Top, r#type);

self.paren(
prec > Prec::Top,
Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type)),
)
}
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
let def_type = self.check_prec(Prec::Top, def_type);
let def_expr = self.check_prec(Prec::Let, def_expr);

core::Term::Let(_, def_name, def_expr, body_expr) => {
let def_expr = self.check_prec(Prec::Top, def_expr);
let def_name = self.freshen_name(*def_name, body_expr);
let def_name = self.push_local(def_name);
let def_pattern = name_to_pattern(def_name);
let body_expr = self.synth_prec(Prec::Let, body_expr);
self.pop_local();

self.paren(
prec > Prec::Let,
Term::Let(
(),
name_to_pattern(def_name),
Some(self.scope.to_scope(def_type)),
def_pattern,
None,
self.scope.to_scope(def_expr),
self.scope.to_scope(body_expr),
),
Expand Down Expand Up @@ -581,22 +568,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
}
core::Term::FunLit(..) => {
let initial_local_len = self.local_len();

let mut params = Vec::new();
let mut body_expr = core_term;

while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr {
let param_name = self.freshen_name(*param_name, next_body_expr);
params.push((*plicity, self.push_local(param_name)));
while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr {
let r#type = self.check(r#type);
let name = self.freshen_name(*name, next_body_expr);
params.push((*plicity, self.push_local(name), r#type));
body_expr = next_body_expr;
}

let body_expr = self.synth_prec(Prec::Let, body_expr);
self.truncate_local(initial_local_len);

let params = params.into_iter().map(|(plicity, name)| Param {
let params = params.into_iter().map(|(plicity, name, r#type)| Param {
plicity,
pattern: name_to_pattern(name),
r#type: None,
r#type: Some(r#type),
});

self.paren(
Expand Down
Loading

0 comments on commit cff2b4c

Please sign in to comment.