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 Nov 10, 2022
1 parent 9d75e85 commit fd53851
Show file tree
Hide file tree
Showing 52 changed files with 690 additions and 500 deletions.
51 changes: 27 additions & 24 deletions fathom/src/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,8 +122,6 @@ 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,
Expand All @@ -148,7 +146,12 @@ pub enum Term<'arena> {
/// Function literals.
///
/// Also known as: lambda expressions, anonymous functions.
FunLit(Span, Option<StringId>, &'arena Term<'arena>),
FunLit(
Span,
Option<StringId>,
&'arena Term<'arena>,
&'arena Term<'arena>,
),
/// Function applications.
FunApp(Span, &'arena Term<'arena>, &'arena Term<'arena>),

Expand Down Expand Up @@ -190,26 +193,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::ArrayLit(span, _)
| Term::FormatRecord(span, _, _)
| Term::FormatCond(span, _, _, _)
| Term::FormatOverlap(span, _, _)
| Term::Prim(span, _)
| Term::ConstLit(span, _)
| Term::ConstMatch(span, _, _, _) => *span,
| Term::FunType(span, ..)
| Term::FunLit(span, ..)
| Term::FunApp(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,
}
}

Expand All @@ -224,7 +226,6 @@ 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)
Expand All @@ -233,7 +234,9 @@ impl<'arena> Term<'arena> {
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
12 changes: 6 additions & 6 deletions fathom/src/core/binary.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -380,12 +380,12 @@ impl<'arena, 'data> Context<'arena, 'data> {
Value::Stuck(Head::LocalVar(_), _)
| Value::Stuck(Head::MetaVar(_), _)
| Value::Universe
| Value::FunType(_, _, _)
| Value::FunLit(_, _)
| Value::RecordType(_, _)
| Value::RecordLit(_, _)
| Value::ArrayLit(_)
| Value::ConstLit(_) => Err(ReadError::InvalidFormat(format.span())),
| Value::FunType(..)
| Value::FunLit(..)
| Value::RecordType(..)
| Value::RecordLit(..)
| Value::ArrayLit(..)
| Value::ConstLit(..) => Err(ReadError::InvalidFormat(format.span())),
}
}

Expand Down
39 changes: 21 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(Option<StringId>, ArcValue<'arena>, Closure<'arena>),
/// Function literals.
FunLit(Option<StringId>, Closure<'arena>),
FunLit(Option<StringId>, ArcValue<'arena>, Closure<'arena>),

/// Record types.
RecordType(&'arena [StringId], Telescope<'arena>),
Expand Down Expand Up @@ -291,7 +291,6 @@ 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) => {
let def_expr = self.eval(def_expr);
self.local_exprs.push(def_expr);
Expand All @@ -310,10 +309,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
Closure::new(self.local_exprs.clone(), body_type),
)),
),
Term::FunLit(span, param_name, body_expr) => Spanned::new(
Term::FunLit(span, param_name, param_type, body_expr) => Spanned::new(
*span,
Arc::new(Value::FunLit(
*param_name,
self.eval(param_type),
Closure::new(self.local_exprs.clone(), body_expr),
)),
),
Expand Down Expand Up @@ -498,7 +498,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
) -> ArcValue<'arena> {
match Arc::make_mut(&mut head_expr) {
// Beta-reduction
Value::FunLit(_, body_expr) => self.apply_closure(body_expr, arg_expr), // FIXME: use span from head/arg exprs?
Value::FunLit(_, _, body_expr) => self.apply_closure(body_expr, arg_expr), // FIXME: use span from head/arg exprs?
// The computation is stuck, preventing further reduction
Value::Stuck(head, spine) => {
spine.push(Elim::FunApp(arg_expr));
Expand Down Expand Up @@ -689,9 +689,12 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
scope.to_scope(self.quote(scope, param_type)),
self.quote_closure(scope, body_type),
),
Value::FunLit(param_name, body_expr) => {
Term::FunLit(span, *param_name, self.quote_closure(scope, body_expr))
}
Value::FunLit(param_name, param_type, body_expr) => Term::FunLit(
span,
*param_name,
scope.to_scope(self.quote(scope, param_type)),
self.quote_closure(scope, body_expr),
),

Value::RecordType(labels, types) => Term::RecordType(
span,
Expand Down Expand Up @@ -842,11 +845,6 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
None => panic_any(Error::UnboundMetaVar),
}
}
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(
*span,
*def_name,
Expand All @@ -863,9 +861,10 @@ 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, param_name, body_expr) => Term::FunLit(
Term::FunLit(span, param_name, param_type, body_expr) => Term::FunLit(
*span,
*param_name,
scope.to_scope(self.unfold_metas(scope, param_type)),
self.unfold_bound_metas(scope, body_expr),
),

Expand Down Expand Up @@ -1095,11 +1094,15 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
self.is_equal(param_type0, param_type1)
&& self.is_equal_closures(body_type0, body_type1)
}
(Value::FunLit(_, body_expr0), Value::FunLit(_, body_expr1)) => {
self.is_equal_closures(body_expr0, body_expr1)
(
Value::FunLit(_, param_type0, body_expr0),
Value::FunLit(_, param_type1, body_expr1),
) => {
self.is_equal(param_type0, param_type1)
&& self.is_equal_closures(body_expr0, body_expr1)
}
(Value::FunLit(_, body_expr), _) => self.is_equal_fun_lit(body_expr, &value1),
(_, Value::FunLit(_, body_expr)) => self.is_equal_fun_lit(body_expr, &value0),
(Value::FunLit(_, _, body_expr), _) => self.is_equal_fun_lit(body_expr, &value1),
(_, Value::FunLit(_, _, body_expr)) => self.is_equal_fun_lit(body_expr, &value0),

(Value::RecordType(labels0, types0), Value::RecordType(labels1, types1)) => {
labels0 == labels1 && self.is_equal_telescopes(types0, types1)
Expand Down Expand Up @@ -1275,7 +1278,7 @@ mod tests {
Value::Stuck(_, _) => {}
Value::Universe => {}
Value::FunType(_, _, _) => {}
Value::FunLit(_, _) => {}
Value::FunLit(_, _, _) => {}
Value::RecordType(_, _) => {}
Value::RecordLit(_, _) => {}
Value::ArrayLit(_) => {}
Expand Down
40 changes: 18 additions & 22 deletions fathom/src/surface/distillation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,10 +203,6 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
/// Distill a core term into a surface term, in a 'checkable' context.
pub fn check(&mut self, core_term: &core::Term<'_>) -> Term<'arena, ()> {
match core_term {
core::Term::Ann(_span, expr, _) => {
// Avoid adding extraneous type annotations!
self.check(expr)
}
core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => {
let def_type = self.check(def_type);
let def_expr = self.check(def_expr);
Expand All @@ -223,20 +219,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
self.scope.to_scope(body_expr),
)
}
core::Term::FunLit(_, param_name, mut body_expr) => {
core::Term::FunLit(..) => {
let initial_local_len = self.local_len();
let mut param_names = vec![self.push_local(*param_name)];
while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
param_names.push(self.push_local(*param_name));
let mut param_names = Vec::new();
let mut body_expr = core_term;

while let core::Term::FunLit(_, param_name, param_type, next_body_expr) = body_expr
{
param_names.push((self.push_local(*param_name), self.check(param_type)));
body_expr = next_body_expr;
}

let body_expr = self.check(body_expr);
self.truncate_local(initial_local_len);

let patterns = param_names
.into_iter()
.map(|name| (Pattern::Name((), name), None));
let patterns = param_names.into_iter().map(|(name, r#type)| {
let r#type = self.scope.to_scope(r#type) as &_;
(Pattern::Name((), name), Some(r#type))
});

Term::FunLiteral(
(),
Expand Down Expand Up @@ -394,12 +394,6 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
Term::App((), head_expr, arg_exprs.into())
}
}
core::Term::Ann(_span, expr, r#type) => {
let r#type = self.check(r#type);
let expr = self.check(expr);

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(def_type);
let def_expr = self.check(def_expr);
Expand Down Expand Up @@ -474,17 +468,19 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
let mut param_names = Vec::new();
let mut body_expr = core_term;

while let core::Term::FunLit(_, param_name, next_body_expr) = body_expr {
param_names.push(self.push_local(*param_name));
while let core::Term::FunLit(_, param_name, param_type, next_body_expr) = body_expr
{
param_names.push((self.push_local(*param_name), self.check(param_type)));
body_expr = next_body_expr;
}

let body_expr = self.synth(body_expr);
self.truncate_local(initial_local_len);

let patterns = param_names
.into_iter()
.map(|name| (Pattern::Name((), name), None));
let patterns = param_names.into_iter().map(|(name, r#type)| {
let r#type = self.scope.to_scope(r#type) as &_;
(Pattern::Name((), name), Some(r#type))
});

Term::FunLiteral(
(),
Expand Down
30 changes: 13 additions & 17 deletions fathom/src/surface/elaboration.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1239,18 +1239,11 @@ impl<'interner, 'arena> Context<'interner, 'arena> {

(expr, r#type)
}
Term::Ann(range, expr, r#type) => {
Term::Ann(_, expr, r#type) => {
let r#type = self.check(r#type, &self.universe.clone());
let type_value = self.eval_env().eval(&r#type);
let expr = self.check(expr, &type_value);

let ann_expr = core::Term::Ann(
range.into(),
self.scope.to_scope(expr),
self.scope.to_scope(r#type),
);

(ann_expr, type_value)
(self.check(expr, &type_value), type_value)
}
Term::Let(range, def_pattern, def_type, def_expr, body_expr) => {
let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
Expand Down Expand Up @@ -1589,7 +1582,13 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
self.check_fun_lit(range, next_patterns, body_expr, &body_type);
self.local_env.pop();

core::Term::FunLit(range.into(), name, self.scope.to_scope(body_expr))
let param_type = self.quote_env().quote(self.scope, param_type);
core::Term::FunLit(
range.into(),
name,
self.scope.to_scope(param_type),
self.scope.to_scope(body_expr),
)
}
// Attempt to elaborate the the body of the function in synthesis
// mode if we are checking against a metavariable.
Expand Down Expand Up @@ -1654,13 +1653,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {

// Construct the function literal and type from the parameters in reverse
for (range, name, r#type) in params.into_iter().rev() {
fun_lit = core::Term::FunLit(range.into(), name, self.scope.to_scope(fun_lit));
fun_type = core::Term::FunType(
Span::Empty,
name,
self.scope.to_scope(r#type),
self.scope.to_scope(fun_type),
);
let r#type = self.scope.to_scope(r#type);
fun_lit = core::Term::FunLit(range.into(), name, r#type, self.scope.to_scope(fun_lit));
fun_type =
core::Term::FunType(Span::Empty, name, r#type, self.scope.to_scope(fun_type));
}

(fun_lit, self.eval_env().eval(&fun_type))
Expand Down
Loading

0 comments on commit fd53851

Please sign in to comment.