Skip to content

Cleanup surface::elaboration #495

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Cleanup surface::elaboration #495

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
383 changes: 364 additions & 19 deletions fathom/src/core.rs
View file
Open in desktop

Large diffs are not rendered by default.

16 changes: 5 additions & 11 deletions fathom/src/core/binary.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,15 +425,11 @@ impl<'arena, 'data> Context<'arena, 'data> {
(Prim::FormatF32Le, []) => read_const(reader, span, read_f32le, Const::F32),
(Prim::FormatF64Be, []) => read_const(reader, span, read_f64be, Const::F64),
(Prim::FormatF64Le, []) => read_const(reader, span, read_f64le, Const::F64),
(Prim::FormatRepeatLen8, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen16, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen32, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen64, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatLen8 | Prim::FormatRepeatLen16 | Prim::FormatRepeatLen32 | Prim::FormatRepeatLen64,
[FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
(Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, format),
(Prim::FormatLimit8, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
(Prim::FormatLimit16, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
(Prim::FormatLimit32, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
(Prim::FormatLimit64, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
(Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64,
[FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
(Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, pos, format),
(Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(format, r#ref),
(Prim::FormatStreamPos, []) => read_stream_pos(reader, span),
Expand Down Expand Up @@ -642,9 +638,7 @@ fn read_s8(reader: &mut BufferReader<'_>) -> Result<i8, BufferError> {
/// Generates a function that reads a multi-byte primitive.
macro_rules! read_multibyte_prim {
($read_multibyte_prim:ident, $from_bytes:ident, $T:ident) => {
fn $read_multibyte_prim<'data>(
reader: &mut BufferReader<'data>,
) -> Result<$T, BufferError> {
fn $read_multibyte_prim(reader: &mut BufferReader) -> Result<$T, BufferError> {
Ok($T::$from_bytes(*reader.read_byte_array()?))
}
};
Expand Down
6 changes: 3 additions & 3 deletions fathom/src/core/pretty.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,17 +143,17 @@ impl<'arena> Context {
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),
self.ann_pattern(Prec::Top, def.name, &def.r#type),
RcDoc::space(),
RcDoc::text("="),
RcDoc::softline(),
self.term_prec(Prec::Let, def_expr),
self.term_prec(Prec::Let, &def.expr),
RcDoc::text(";"),
])
.group(),
Expand Down
656 changes: 283 additions & 373 deletions fathom/src/core/prim.rs
View file
Open in desktop

Large diffs are not rendered by default.

105 changes: 54 additions & 51 deletions fathom/src/core/semantics.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ use std::sync::Arc;

use scoped_arena::Scope;

use super::{Builder, LetDef};
use crate::alloc::SliceVec;
use crate::core::{prim, Const, LocalInfo, Plicity, Prim, Term};
use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv};
Expand Down Expand Up @@ -300,8 +301,8 @@ 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();
Expand Down Expand Up @@ -667,21 +668,17 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
// NOTE: this copies more than is necessary when `'in_arena == 'out_arena`:
// for example when copying label slices.

let builder = Builder::new(scope);
let value = self.elim_env.force(value);
let span = value.span();
match value.as_ref() {
Value::Stuck(head, spine) => spine.iter().fold(
self.quote_head(scope, span, head),
|head_expr, elim| match elim {
Elim::FunApp(plicity, arg_expr) => Term::FunApp(
span,
*plicity,
scope.to_scope(head_expr),
scope.to_scope(self.quote(scope, arg_expr)),
),
Elim::RecordProj(label) => {
Term::RecordProj(span, scope.to_scope(head_expr), *label)
Elim::FunApp(plicity, arg_expr) => {
builder.fun_app(span, *plicity, head_expr, self.quote(scope, arg_expr))
}
Elim::RecordProj(label) => builder.record_proj(span, head_expr, *label),
Elim::ConstMatch(branches) => {
let mut branches = branches.clone();
let mut pattern_branches = SliceVec::new(scope, branches.num_patterns());
Expand All @@ -699,9 +696,9 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
}
};

Term::ConstMatch(
builder.const_match(
span,
scope.to_scope(head_expr),
head_expr,
pattern_branches.into(),
default_branch
.map(|(name, expr)| (name, self.quote_closure(scope, &expr))),
Expand All @@ -712,20 +709,19 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {

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

Value::FunType(plicity, param_name, param_type, body_type) => Term::FunType(
Value::FunType(plicity, param_name, param_type, body_type) => builder.fun_type(
span,
*plicity,
*param_name,
scope.to_scope(self.quote(scope, param_type)),
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, body_expr) => builder.fun_lit(
span,
*plicity,
*param_name,
self.quote_closure(scope, body_expr),
),

Value::RecordType(labels, types) => Term::RecordType(
span,
scope.to_scope_from_iter(labels.iter().copied()),
Expand All @@ -746,10 +742,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
scope.to_scope_from_iter(labels.iter().copied()),
self.quote_telescope(scope, formats),
),
Value::FormatCond(label, format, cond) => Term::FormatCond(
Value::FormatCond(label, format, cond) => builder.format_cond(
span,
*label,
scope.to_scope(self.quote(scope, format)),
self.quote(scope, format),
self.quote_closure(scope, cond),
),
Value::FormatOverlap(labels, formats) => Term::FormatOverlap(
Expand Down Expand Up @@ -792,15 +788,15 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
&mut self,
scope: &'out_arena Scope<'out_arena>,
closure: &Closure<'in_arena>,
) -> &'out_arena Term<'out_arena> {
) -> Term<'out_arena> {
let var = Arc::new(Value::local_var(self.local_exprs.next_level()));
let value = self.elim_env.apply_closure(closure, Spanned::empty(var));

self.push_local();
let term = self.quote(scope, &value);
self.pop_local();

scope.to_scope(term)
term
}

/// Quote a [telescope][Telescope] back into a slice of [terms][Term].
Expand Down Expand Up @@ -848,6 +844,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
scope: &'out_arena Scope<'out_arena>,
term: &Term<'arena>,
) -> Term<'out_arena> {
let builder = Builder::new(scope);

match term {
Term::ItemVar(span, var) => Term::ItemVar(*span, *var),
Term::LocalVar(span, var) => Term::LocalVar(*span, *var),
Expand All @@ -871,29 +869,31 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
Term::InsertedMeta(*span, *var, infos)
}
},
Term::Ann(span, expr, r#type) => Term::Ann(
Term::Ann(span, expr, r#type) => builder.ann(
*span,
scope.to_scope(self.unfold_metas(scope, expr)),
scope.to_scope(self.unfold_metas(scope, r#type)),
self.unfold_metas(scope, expr),
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) => builder.r#let(
*span,
*def_name,
scope.to_scope(self.unfold_metas(scope, def_type)),
scope.to_scope(self.unfold_metas(scope, def_expr)),
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::Universe(span) => Term::Universe(*span),

Term::FunType(span, plicity, param_name, param_type, body_type) => Term::FunType(
Term::FunType(span, plicity, param_name, param_type, body_type) => builder.fun_type(
*span,
*plicity,
*param_name,
scope.to_scope(self.unfold_metas(scope, param_type)),
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, body_expr) => builder.fun_lit(
*span,
*plicity,
*param_name,
Expand Down Expand Up @@ -921,10 +921,10 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
scope.to_scope_from_iter(labels.iter().copied()),
self.unfold_telescope_metas(scope, formats),
),
Term::FormatCond(span, name, format, pred) => Term::FormatCond(
Term::FormatCond(span, name, format, pred) => builder.format_cond(
*span,
*name,
scope.to_scope(self.unfold_metas(scope, format)),
self.unfold_metas(scope, format),
self.unfold_bound_metas(scope, pred),
),
Term::FormatOverlap(span, labels, formats) => Term::FormatOverlap(
Expand All @@ -945,6 +945,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
scope: &'out_arena Scope<'out_arena>,
term: &Term<'arena>,
) -> TermOrValue<'arena, 'out_arena> {
let builder = Builder::new(scope);

// Recurse to find the head of an elimination, checking if it's a
// metavariable. If so, check if it has a solution, and then apply
// eliminations to the solution in turn on our way back out.
Expand All @@ -971,11 +973,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {

Term::FunApp(span, plicity, head_expr, arg_expr) => {
match self.unfold_meta_var_spines(scope, head_expr) {
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::FunApp(
TermOrValue::Term(head_expr) => TermOrValue::Term(builder.fun_app(
*span,
*plicity,
scope.to_scope(head_expr),
scope.to_scope(self.unfold_metas(scope, arg_expr)),
head_expr,
self.unfold_metas(scope, arg_expr),
)),
TermOrValue::Value(head_expr) => {
let arg_expr = self.eval(arg_expr);
Expand All @@ -985,28 +987,29 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
}
Term::RecordProj(span, head_expr, label) => {
match self.unfold_meta_var_spines(scope, head_expr) {
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::RecordProj(
*span,
scope.to_scope(head_expr),
*label,
)),
TermOrValue::Term(head_expr) => {
TermOrValue::Term(builder.record_proj(*span, head_expr, *label))
}
TermOrValue::Value(head_expr) => {
TermOrValue::Value(self.elim_env.record_proj(head_expr, *label))
}
}
}
Term::ConstMatch(span, head_expr, branches, default_branch) => {
match self.unfold_meta_var_spines(scope, head_expr) {
TermOrValue::Term(head_expr) => TermOrValue::Term(Term::ConstMatch(
*span,
scope.to_scope(head_expr),
scope.to_scope_from_iter(
(branches.iter())
.map(|(r#const, expr)| (*r#const, self.unfold_metas(scope, expr))),
TermOrValue::Term(head_expr) => TermOrValue::Term(
builder.const_match(
*span,
head_expr,
scope.to_scope_from_iter(
branches.iter().map(|(r#const, expr)| {
(*r#const, self.unfold_metas(scope, expr))
}),
),
default_branch
.map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
),
default_branch
.map(|(name, expr)| (name, self.unfold_bound_metas(scope, expr))),
)),
),
TermOrValue::Value(head_expr) => {
let branches =
Branches::new(self.local_exprs.clone(), branches, *default_branch);
Expand All @@ -1023,14 +1026,14 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
&mut self,
scope: &'out_arena Scope<'out_arena>,
term: &Term<'arena>,
) -> &'out_arena Term<'out_arena> {
) -> Term<'out_arena> {
let var = Arc::new(Value::local_var(self.local_exprs.len().next_level()));

self.local_exprs.push(Spanned::empty(var));
let term = self.unfold_metas(scope, term);
self.local_exprs.pop();

scope.to_scope(term)
term
}

fn unfold_telescope_metas<'out_arena>(
Expand Down
35 changes: 23 additions & 12 deletions fathom/src/env.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,16 @@ impl Index {
pub const fn prev(self) -> Index {
Index(self.0 + 1)
}

/// An iterator over indices, listed from the most recently bound.
pub fn iter() -> impl Iterator<Item = Self> {
(0..).map(Self)
}

/// An iterator over indices, listed from `self`
pub fn iter_from(self) -> impl Iterator<Item = Self> {
(self.0..).map(Self)
}
}

impl fmt::Debug for Index {
Expand All @@ -70,11 +80,6 @@ impl fmt::Display for Index {
}
}

/// An iterator over indices, listed from the most recently bound.
pub fn indices() -> impl Iterator<Item = Index> {
(0..).map(Index)
}

/// A de Bruijn level, which represents a variable by counting the number of
/// binders between the binder that introduced the variable and the start of the
/// environment. For example:
Expand All @@ -101,6 +106,16 @@ impl Level {
pub const fn next(self) -> Level {
Level(self.0 + 1)
}

/// An iterator over levels, listed from the least recently bound.
pub fn iter() -> impl Iterator<Item = Self> {
(0..).map(Self)
}

/// An iterator over levels, listed from `self`
pub fn iter_from(self) -> impl Iterator<Item = Self> {
(self.0..).map(Self)
}
}

impl fmt::Debug for Level {
Expand All @@ -117,11 +132,6 @@ impl fmt::Display for Level {
}
}

/// An iterator over levels, listed from the least recently bound.
pub fn levels() -> impl Iterator<Item = Level> {
(0..).map(Level)
}

/// The length of an environment.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
pub struct EnvLen(RawVar);
Expand Down Expand Up @@ -270,11 +280,12 @@ impl<Entry> SliceEnv<Entry> {

impl<Entry: PartialEq> SliceEnv<Entry> {
pub fn elem_level(&self, entry: &Entry) -> Option<Level> {
Iterator::zip(levels(), self.iter()).find_map(|(var, e)| (entry == e).then_some(var))
Iterator::zip(Level::iter(), self.iter()).find_map(|(var, e)| (entry == e).then_some(var))
}

pub fn elem_index(&self, entry: &Entry) -> Option<Index> {
Iterator::zip(indices(), self.iter().rev()).find_map(|(var, e)| (entry == e).then_some(var))
Iterator::zip(Index::iter(), self.iter().rev())
.find_map(|(var, e)| (entry == e).then_some(var))
}
}

Expand Down
6 changes: 6 additions & 0 deletions fathom/src/source.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -162,6 +162,12 @@ impl fmt::Debug for ByteRange {
}
}

impl From<(BytePos, BytePos)> for ByteRange {
fn from((start, end): (BytePos, BytePos)) -> Self {
Self { start, end }
}
}

impl ByteRange {
pub fn new(start: BytePos, end: BytePos) -> ByteRange {
ByteRange { start, end }
Expand Down
Loading