Skip to content

Commit

Permalink
Cleanup surface::elaboration
Browse files Browse the repository at this point in the history
  • Loading branch information
@Kmeakin
Kmeakin committed Feb 13, 2023
1 parent 3960a94 commit 49c2156
Show file tree
Hide file tree
Showing 14 changed files with 1,584 additions and 1,208 deletions.
374 changes: 361 additions & 13 deletions fathom/src/core.rs
View file

Large diffs are not rendered by default.

16 changes: 5 additions & 11 deletions fathom/src/core/binary.rs
View file
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
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

Large diffs are not rendered by default.

105 changes: 54 additions & 51 deletions fathom/src/core/semantics.rs
View file
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
6 changes: 6 additions & 0 deletions fathom/src/source.rs
View file
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

0 comments on commit 49c2156

Please sign in to comment.