Skip to content

Commit

Permalink
Elaborate letrec terms
Browse files Browse the repository at this point in the history
  • Loading branch information
@Kmeakin
Kmeakin committed Jan 30, 2023
1 parent 6de0471 commit 74bac1b
Show file tree
Hide file tree
Showing 9 changed files with 262 additions and 58 deletions.
37 changes: 26 additions & 11 deletions fathom/src/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,13 +143,8 @@ pub enum Term<'arena> {
/// 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>,
),
Let(Span, &'arena LetDef<'arena>, &'arena Term<'arena>),
Letrec(Span, &'arena [LetDef<'arena>], &'arena Term<'arena>),

/// The type of types.
Universe(Span),
Expand Down Expand Up @@ -204,6 +199,13 @@ pub enum Term<'arena> {
),
}

#[derive(Debug, Clone)]
pub struct LetDef<'arena> {
pub name: Option<StringId>,
pub r#type: Term<'arena>,
pub expr: Term<'arena>,
}

impl<'arena> Term<'arena> {
/// Get the source span of the term.
pub fn span(&self) -> Span {
Expand All @@ -213,7 +215,8 @@ impl<'arena> Term<'arena> {
| Term::MetaVar(span, _)
| Term::InsertedMeta(span, _, _)
| Term::Ann(span, _, _)
| Term::Let(span, _, _, _, _)
| Term::Let(span, ..)
| Term::Letrec(span, ..)
| Term::Universe(span)
| Term::FunType(span, ..)
| Term::FunLit(span, ..)
Expand Down Expand Up @@ -243,11 +246,23 @@ impl<'arena> Term<'arena> {
| 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)
Term::Let(_, def, body_expr) => {
def.r#type.binds_local(var)
|| def.expr.binds_local(var)
|| body_expr.binds_local(var.prev())
}
Term::Letrec(_, defs, body_expr) => {
for _def in defs.iter() {
var = var.prev();
}

if (defs.iter()).any(|def| def.r#type.binds_local(var) || def.expr.binds_local(var))
{
return true;
}

body_expr.binds_local(var)
}
Term::FunType(.., param_type, body_type) => {
param_type.binds_local(var) || body_type.binds_local(var.prev())
}
Expand Down
33 changes: 26 additions & 7 deletions fathom/src/core/pretty.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ use std::cell::RefCell;

use pretty::RcDoc;

use crate::core::{Item, Module, Plicity, Term};
use crate::core::{Item, LetDef, Module, Plicity, Term};
use crate::source::{StringId, StringInterner};
use crate::surface::lexer::is_keyword;

Expand Down Expand Up @@ -150,24 +150,33 @@ impl<'interner, 'arena> Context<'interner> {
self.term_prec(Prec::Top, r#type),
]),
),
Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren(
Term::Let(_, def, 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),
RcDoc::space(),
RcDoc::text("="),
RcDoc::softline(),
self.term_prec(Prec::Let, def_expr),
self.let_def(def),
RcDoc::text(";"),
])
.group(),
RcDoc::line(),
self.term_prec(Prec::Let, body_expr),
]),
),
Term::Letrec(_, defs, body_expr) => self.paren(
prec > Prec::Let,
self.sequence(
RcDoc::concat([RcDoc::text("let")]),
defs.iter().map(|def| self.let_def(def)),
RcDoc::text(","),
RcDoc::concat([
RcDoc::text(";"),
RcDoc::line(),
self.term_prec(Prec::Let, body_expr),
]),
),
),
Term::Universe(_) => RcDoc::text("Type"),
Term::FunType(_, plicity, param_name, param_type, body_type) => self.paren(
prec > Prec::Fun,
Expand Down Expand Up @@ -342,6 +351,16 @@ impl<'interner, 'arena> Context<'interner> {
}
}

fn let_def(&'arena self, def: &LetDef<'arena>) -> RcDoc {
RcDoc::concat([
self.ann_pattern(Prec::Top, def.name, &def.r#type),
RcDoc::space(),
RcDoc::text("="),
RcDoc::softline(),
self.term_prec(Prec::Let, &def.expr),
])
}

fn format_field(&'arena self, label: StringId, format: &Term<'arena>) -> RcDoc {
RcDoc::concat([
self.string_id(label),
Expand Down
56 changes: 48 additions & 8 deletions fathom/src/core/semantics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ use std::sync::Arc;
use scoped_arena::Scope;

use crate::alloc::SliceVec;
use crate::core::{prim, Const, LocalInfo, Plicity, Prim, Term};
use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv};
use crate::core::*;
use crate::env::{self, EnvLen, Index, Level, SharedEnv, SliceEnv};
use crate::source::{Span, Spanned, StringId};

/// Atomically reference counted values. We use reference counting to increase
Expand Down Expand Up @@ -53,6 +53,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()
Expand Down Expand Up @@ -299,13 +301,29 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
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);
Term::Let(span, def, body_expr) => {
let def_expr = self.eval(&def.expr);
self.local_exprs.push(def_expr);
let body_expr = self.eval(body_expr);
self.local_exprs.pop();
Spanned::merge(*span, body_expr)
}
Term::Letrec(span, defs, body_expr) => {
let initial_len = self.local_exprs.len();

for _def in defs.iter() {
// TODO: lazy evaluation?
(self.local_exprs).push(Spanned::empty(Arc::new(Value::ERROR)));
}
for (level, def) in Iterator::zip(env::levels(), defs.iter()) {
let def_expr = self.eval(&def.expr);
self.local_exprs.set_level(level, def_expr);
}

let body_expr = self.eval(body_expr);
self.local_exprs.truncate(initial_len);
Spanned::merge(*span, body_expr)
}

Term::Universe(span) => Spanned::new(*span, Arc::new(Value::Universe)),

Expand Down Expand Up @@ -879,13 +897,35 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
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, 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)),
scope.to_scope(LetDef {
name: def.name,
r#type: self.unfold_metas(scope, &def.r#type),
expr: self.unfold_metas(scope, &def.expr),
}),
self.unfold_bound_metas(scope, body_expr),
),
Term::Letrec(span, defs, body_expr) => {
let initial_len = self.local_exprs.len();

for _def in defs.iter() {
let var = Arc::new(Value::local_var(self.local_exprs.len().next_level()));
self.local_exprs.push(Spanned::empty(var));
}

let defs = scope.to_scope_from_iter(defs.iter().map(|def| {
let name = def.name;
let r#type = self.unfold_metas(scope, &def.r#type);
let expr = self.unfold_metas(scope, &def.expr);
LetDef { name, r#type, expr }
}));

let body_expr = self.unfold_metas(scope, body_expr);
self.local_exprs.truncate(initial_len);

Term::Letrec(*span, defs, scope.to_scope(body_expr))
}

Term::Universe(span) => Term::Universe(*span),

Expand Down
4 changes: 4 additions & 0 deletions fathom/src/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -337,6 +337,10 @@ impl<Entry> SharedEnv<Entry> {
self.get_level(self.len().index_to_level(index)?)
}

pub fn set_level(&mut self, level: Level, entry: Entry) {
self.entries.set_mut(level.0 as usize, entry);
}

/// Push an entry onto the environment.
pub fn push(&mut self, entry: Entry) {
assert!(self.entries.len() < usize::from(u16::MAX));
Expand Down
9 changes: 9 additions & 0 deletions fathom/src/surface.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,15 @@ impl<Range: Clone> Pattern<Range> {
}
}

impl<Range> Pattern<Range> {
pub fn name(&self) -> Option<StringId> {
match self {
Pattern::Name(_, name) => Some(*name),
_ => None,
}
}
}

/// Surface terms.
#[derive(Debug, Clone)]
pub enum Term<'arena, Range> {
Expand Down
64 changes: 56 additions & 8 deletions fathom/src/surface/distillation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -278,11 +278,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
// 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(_span, def, body_expr) => {
let def_type = self.check_prec(Prec::Top, &def.r#type);
let def_expr = self.check_prec(Prec::Let, &def.expr);

let def_name = self.freshen_name(*def_name, body_expr);
let def_name = self.freshen_name(def.name, body_expr);
let def_name = self.push_local(def_name);
let body_expr = self.check_prec(Prec::Let, body_expr);
self.pop_local();
Expand All @@ -297,6 +297,30 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
self.scope.to_scope(body_expr),
)
}
core::Term::Letrec(_, defs, body_expr) => {
let initial_len = self.local_len();

// TODO: freshen names
let def_names: Vec<_> = defs.iter().map(|def| self.push_local(def.name)).collect();

let defs = self.scope.to_scope_from_iter(
Iterator::zip(def_names.iter(), defs.iter()).map(|(name, def)| {
let r#type = self.check(&def.r#type);
let expr = self.check(&def.expr);

LetDef {
pattern: name_to_pattern(*name),
r#type: Some(r#type),
expr,
}
}),
);

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

Term::Letrec((), defs, self.scope.to_scope(body_expr))
}
core::Term::FunLit(..) => {
let initial_local_len = self.local_len();
let mut params = Vec::new();
Expand Down Expand Up @@ -497,11 +521,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
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(_span, def, body_expr) => {
let def_type = self.check_prec(Prec::Top, &def.r#type);
let def_expr = self.check_prec(Prec::Let, &def.r#expr);

let def_name = self.freshen_name(*def_name, body_expr);
let def_name = self.freshen_name(def.name, body_expr);
let def_name = self.push_local(def_name);
let body_expr = self.synth_prec(Prec::Let, body_expr);
self.pop_local();
Expand All @@ -516,6 +540,30 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
self.scope.to_scope(body_expr),
)
}
core::Term::Letrec(_, defs, body_expr) => {
let initial_len = self.local_len();

// TODO: freshen names
let def_names: Vec<_> = defs.iter().map(|def| self.push_local(def.name)).collect();

let defs = self.scope.to_scope_from_iter(
Iterator::zip(def_names.iter(), defs.iter()).map(|(name, def)| {
let r#type = self.check(&def.r#type);
let expr = self.check(&def.expr);

LetDef {
pattern: name_to_pattern(*name),
r#type: Some(r#type),
expr,
}
}),
);

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

Term::Letrec((), defs, self.scope.to_scope(body_expr))
}
core::Term::Universe(_span) => Term::Universe(()),

core::Term::FunType(..) => {
Expand Down
Loading

0 comments on commit 74bac1b

Please sign in to comment.