From 19c1a85db9cdf531cf6e782ef0252e0dbf202ab6 Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Thu, 19 Jan 2023 04:19:09 +0000 Subject: [PATCH] Lazy evaluation --- fathom/Cargo.toml | 2 +- fathom/src/core/binary.rs | 53 +-- fathom/src/core/prim.rs | 90 +++-- fathom/src/core/semantics.rs | 318 +++++++++++++----- fathom/src/driver.rs | 15 +- fathom/src/surface.rs | 2 +- fathom/src/surface/elaboration.rs | 118 ++++--- fathom/src/surface/elaboration/unification.rs | 93 +++-- 8 files changed, 459 insertions(+), 232 deletions(-) diff --git a/fathom/Cargo.toml b/fathom/Cargo.toml index 0c9be003b..c1f1f6603 100644 --- a/fathom/Cargo.toml +++ b/fathom/Cargo.toml @@ -27,7 +27,7 @@ lalrpop-util = "0.19.5" lasso = { version = "0.6.0", features = ["multi-threaded", "ahasher", "inline-more"] } levenshtein = "1.0.5" logos = "0.12" -once_cell = { version = "1.17.0", features = ["parking_lot"] } +once_cell = { version = "1.17.0", features = ["parking_lot"] } # TODO: remove once `std::cell::once_cell` is stabilized pretty = "0.11.2" rpds = "0.12.0" scoped-arena = "0.4.1" diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs index 661f014e6..958167723 100644 --- a/fathom/src/core/binary.rs +++ b/fathom/src/core/binary.rs @@ -7,7 +7,8 @@ use std::fmt::Debug; use std::slice::SliceIndex; use std::sync::Arc; -use crate::core::semantics::{self, ArcValue, Elim, Head, Value}; +use super::semantics::{EvalMode, LocalExprs}; +use crate::core::semantics::{self, ArcValue, Elim, Head, LazyValue, Value}; use crate::core::{Const, Item, Module, Prim, Term, UIntStyle}; use crate::env::{EnvLen, SharedEnv, UniqueEnv}; use crate::source::{Span, Spanned}; @@ -254,8 +255,8 @@ impl fmt::Display for BufferError { impl std::error::Error for BufferError {} pub struct Context<'arena, 'data> { - item_exprs: UniqueEnv>, - local_exprs: SharedEnv>, + item_exprs: UniqueEnv>, + local_exprs: LocalExprs<'arena>, initial_buffer: Buffer<'data>, pending_formats: Vec<(usize, ArcValue<'arena>)>, cached_refs: HashMap>>, @@ -283,7 +284,7 @@ impl<'arena, 'data> Context<'arena, 'data> { fn eval_env(&mut self) -> semantics::EvalEnv<'arena, '_> { let elim_env = semantics::ElimEnv::new(&self.item_exprs, [][..].into()); - semantics::EvalEnv::new(elim_env, &mut self.local_exprs) + semantics::EvalEnv::new(elim_env, &mut self.local_exprs).with_mode(EvalMode::Strict) } fn elim_env(&self) -> semantics::ElimEnv<'arena, '_> { @@ -295,7 +296,7 @@ impl<'arena, 'data> Context<'arena, 'data> { for item in module.items { match item { Item::Def { expr, .. } => { - let expr = self.eval_env().eval(expr); + let expr = self.eval_env().delay_or_eval(expr); self.item_exprs.push(expr); } } @@ -332,7 +333,7 @@ impl<'arena, 'data> Context<'arena, 'data> { let mut exprs = Vec::with_capacity(formats.len()); while let Some((format, next_formats)) = self.elim_env().split_telescope(formats) { - let expr = self.read_format(reader, &format)?; + let expr = LazyValue::eager(self.read_format(reader, &format)?); exprs.push(expr.clone()); formats = next_formats(expr); } @@ -343,8 +344,10 @@ impl<'arena, 'data> Context<'arena, 'data> { )) } Value::FormatCond(_label, format, cond) => { - let value = self.read_format(reader, format)?; - let cond_res = self.elim_env().apply_closure(cond, value.clone()); + let value = self.read_format(reader, &self.elim_env().force_lazy(format))?; + let cond_res = self + .elim_env() + .apply_closure(cond, LazyValue::eager(value.clone())); match cond_res.as_ref() { Value::ConstLit(Const::Bool(true)) => Ok(value), @@ -366,7 +369,7 @@ impl<'arena, 'data> Context<'arena, 'data> { while let Some((format, next_formats)) = self.elim_env().split_telescope(formats) { let mut reader = reader.clone(); - let expr = self.read_format(&mut reader, &format)?; + let expr = LazyValue::eager(self.read_format(&mut reader, &format)?); exprs.push(expr.clone()); formats = next_formats(expr); @@ -406,6 +409,8 @@ impl<'arena, 'data> Context<'arena, 'data> { ) -> Result, ReadError<'arena>> { use crate::core::semantics::Elim::FunApp; + let force = |expr| self.elim_env().force_lazy(expr); + match (prim, slice) { (Prim::FormatU8, []) => read_const(reader, span, read_u8, |num| Const::U8(num, UIntStyle::Decimal)), (Prim::FormatU16Be, []) => read_const(reader, span, read_u16be, |num| Const::U16(num, UIntStyle::Decimal)), @@ -425,22 +430,18 @@ 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::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::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::FormatRepeatLen8| Prim::FormatRepeatLen16 | Prim::FormatRepeatLen32 | Prim::FormatRepeatLen64, + [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, &force(len), &force(format)), + (Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, &force(format)), + (Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64, + [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader,&force(limit) , &force(format)), + (Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, &force(pos), &force(format)), + (Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(&force(format), &force(r#ref)), (Prim::FormatStreamPos, []) => read_stream_pos(reader, span), - (Prim::FormatSucceed, [_, FunApp(_, elem)]) => Ok(elem.clone()), + (Prim::FormatSucceed, [_, FunApp(_, elem)]) => Ok(force(elem)), (Prim::FormatFail, []) => Err(ReadError::ReadFailFormat(span)), - (Prim::FormatUnwrap, [_, FunApp(_, option)]) => match option.match_prim_spine() { - Some((Prim::OptionSome, [_, FunApp(_, elem)])) => Ok(elem.clone()), + (Prim::FormatUnwrap, [_, FunApp(_, option)]) => match force(option).match_prim_spine() { + Some((Prim::OptionSome, [_, FunApp(_, elem)])) => Ok(force(elem)), Some((Prim::OptionNone, [_])) => Err(ReadError::UnwrappedNone(span)), _ => Err(ReadError::InvalidValue(span)), }, @@ -464,7 +465,7 @@ impl<'arena, 'data> Context<'arena, 'data> { }; let elem_exprs = (0..len) - .map(|_| self.read_format(reader, elem_format)) + .map(|_| (self.read_format(reader, elem_format).map(LazyValue::eager))) .collect::>()?; Ok(Spanned::new(span, Arc::new(Value::ArrayLit(elem_exprs)))) @@ -481,7 +482,7 @@ impl<'arena, 'data> Context<'arena, 'data> { loop { match self.read_format(reader, elem_format) { Ok(elem) => { - elems.push(elem); + elems.push(LazyValue::eager(elem)); current_offset = reader.relative_offset(); } Err(ReadError::BufferError(_, BufferError::UnexpectedEndOfBuffer)) => { @@ -557,7 +558,7 @@ impl<'arena, 'data> Context<'arena, 'data> { fn lookup_ref<'context>( &'context self, pos: usize, - format: &ArcValue<'_>, + format: &ArcValue<'arena>, ) -> Option<&'context ParsedRef<'arena>> { // NOTE: The number of calls to `semantics::ConversionEnv::is_equal` // when looking up cached references is a bit of a pain. If this ever diff --git a/fathom/src/core/prim.rs b/fathom/src/core/prim.rs index e4e99808f..a4c126645 100644 --- a/fathom/src/core/prim.rs +++ b/fathom/src/core/prim.rs @@ -3,6 +3,7 @@ use std::sync::Arc; use fxhash::FxHashMap; use scoped_arena::Scope; +use super::semantics::{LazyValue, LocalExprs}; use crate::core::semantics::{ArcValue, Elim, ElimEnv, Head, Value}; use crate::core::{self, Const, Plicity, Prim, UIntStyle}; use crate::env::{self, SharedEnv, UniqueEnv}; @@ -508,8 +509,8 @@ struct EnvBuilder<'arena> { entries: FxHashMap)>, scope: &'arena Scope<'arena>, meta_exprs: UniqueEnv>>, - item_exprs: UniqueEnv>, - local_exprs: SharedEnv>, + item_exprs: UniqueEnv>, + local_exprs: LocalExprs<'arena>, } impl<'arena> EnvBuilder<'arena> { @@ -577,13 +578,13 @@ macro_rules! step { // TODO: Should we merge the spans of the param idents to produce the body span? macro_rules! const_step { ([$($param:ident : $Input:ident),*] => $body:expr) => { - step!(_, [$($param),*] => match ($($param.as_ref(),)*) { + step!(env, [$($param),*] => match ($(env.force_lazy($param).as_ref(),)*) { ($(Value::ConstLit(Const::$Input($param, ..)),)*) => Spanned::empty(Arc::new(Value::ConstLit($body))), _ => return None, }) }; ([$($param:ident , $style:ident : $Input:ident),*] => $body:expr) => { - step!(_, [$($param),*] => match ($($param.as_ref(),)*) { + step!(env, [$($param),*] => match ($(env.force_lazy($param).as_ref(),)*) { ($(Value::ConstLit(Const::$Input($param, $style)),)*) => Spanned::empty(Arc::new(Value::ConstLit($body))), _ => return None, }) @@ -611,21 +612,18 @@ pub fn repr(prim: Prim) -> Step { Prim::FormatF32Le => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F32Type, [])))), Prim::FormatF64Be => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F64Type, [])))), Prim::FormatF64Le => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F64Type, [])))), - Prim::FormatRepeatLen8 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array8Type, [len.clone(), env.format_repr(elem)])))), - Prim::FormatRepeatLen16 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array16Type, [len.clone(), env.format_repr(elem)])))), - Prim::FormatRepeatLen32 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array32Type, [len.clone(), env.format_repr(elem)])))), - Prim::FormatRepeatLen64 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array64Type, [len.clone(), env.format_repr(elem)])))), - Prim::FormatLimit8 => step!(env, [_, elem] => env.format_repr(elem)), - Prim::FormatLimit16 => step!(env, [_, elem] => env.format_repr(elem)), - Prim::FormatLimit32 => step!(env, [_, elem] => env.format_repr(elem)), - Prim::FormatLimit64 => step!(env, [_, elem] => env.format_repr(elem)), - Prim::FormatRepeatUntilEnd => step!(env, [elem] => Spanned::empty(Arc::new(Value::prim(Prim::ArrayType, [env.format_repr(elem)])))), - Prim::FormatLink => step!(_, [_, elem] => Spanned::empty(Arc::new(Value::prim(Prim::RefType, [elem.clone()])))), - Prim::FormatDeref => step!(env, [elem, _] => env.format_repr(elem)), + Prim::FormatRepeatLen8 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array8Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))), + Prim::FormatRepeatLen16 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array16Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))), + Prim::FormatRepeatLen32 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array32Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))), + Prim::FormatRepeatLen64 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array64Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))), + Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64 => step!(env, [_, elem] => env.format_repr(&env.force_lazy(elem))), + Prim::FormatRepeatUntilEnd => step!(env, [elem] => Spanned::empty(Arc::new(Value::prim(Prim::ArrayType, [env.format_repr(&env.force_lazy(elem))])))), + Prim::FormatLink => step!(env, [_, elem] => Spanned::empty(Arc::new(Value::prim(Prim::RefType, [env.force_lazy(elem)])))), + Prim::FormatDeref => step!(env, [elem, _] => env.format_repr(&env.force_lazy(elem))), Prim::FormatStreamPos => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::PosType, [])))), - Prim::FormatSucceed => step!(_, [elem, _] => elem.clone()), + Prim::FormatSucceed => step!(env, [elem, _] => env.force_lazy(elem)), Prim::FormatFail => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::VoidType, [])))), - Prim::FormatUnwrap => step!(_, [elem, _] => elem.clone()), + Prim::FormatUnwrap => step!(env, [elem, _] => env.force_lazy(elem)), Prim::ReportedError => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::ReportedError, [])))), _ => |_, _| None, } @@ -641,15 +639,49 @@ pub fn step(prim: Prim) -> Step { #[allow(unreachable_code)] Prim::Absurd => step!(_, [_, _] => panic!("Constructed an element of `Void`")), - Prim::FormatRepr => step!(env, [format] => env.format_repr(format)), + Prim::FormatRepr => step!(env, [format] => env.format_repr(&env.force_lazy(format))), Prim::BoolEq => const_step!([x: Bool, y: Bool] => Const::Bool(x == y)), Prim::BoolNeq => const_step!([x: Bool, y: Bool] => Const::Bool(x != y)), Prim::BoolNot => const_step!([x: Bool] => Const::Bool(bool::not(*x))), - Prim::BoolAnd => const_step!([x: Bool, y: Bool] => Const::Bool(*x && *y)), - Prim::BoolOr => const_step!([x: Bool, y: Bool] => Const::Bool(*x || *y)), Prim::BoolXor => const_step!([x: Bool, y: Bool] => Const::Bool(*x ^ *y)), + Prim::BoolAnd => |env: &ElimEnv, spine: &[Elim]| match spine { + [Elim::FunApp(_,x), Elim::FunApp(_, y)] => { + let x = env.force_lazy(x); + match x.as_ref() { + Value::ConstLit(Const::Bool(false)) => Some(x), + Value::ConstLit(Const::Bool(true)) => { + let y = env.force_lazy(y); + match y.as_ref() { + Value::ConstLit(Const::Bool(_)) => Some(y), + _ => None, + } + } + _ => None, + } + } + _ => None, + }, + + Prim::BoolOr => |env: &ElimEnv, spine: &[Elim]| match spine { + [Elim::FunApp(_,x), Elim::FunApp(_, y)] => { + let x = env.force_lazy(x); + match x.as_ref() { + Value::ConstLit(Const::Bool(true)) => Some(x), + Value::ConstLit(Const::Bool(false)) => { + let y = env.force_lazy(y); + match y.as_ref() { + Value::ConstLit(Const::Bool(_)) => Some(y), + _ => None, + } + } + _ => None, + } + } + _ => None, + }, + Prim::U8Eq => const_step!([x: U8, y: U8] => Const::Bool(x == y)), Prim::U8Neq => const_step!([x: U8, y: U8] => Const::Bool(x != y)), Prim::U8Gt => const_step!([x: U8, y: U8] => Const::Bool(x > y)), @@ -775,22 +807,20 @@ pub fn step(prim: Prim) -> Step { Prim::S64UAbs => const_step!([x: S64] => Const::U64(i64::unsigned_abs(*x), UIntStyle::Decimal)), Prim::OptionFold => step!(env, [_, _, on_none, on_some, option] => { - match option.match_prim_spine()? { + match env.force_lazy(option).match_prim_spine()? { (Prim::OptionSome, [_, Elim::FunApp(Plicity::Explicit, value)]) => { - env.fun_app(Plicity::Explicit, on_some.clone(), value.clone()) + env.fun_app(Plicity::Explicit, env.force_lazy(on_some), value) }, - (Prim::OptionNone, [_]) => on_none.clone(), + (Prim::OptionNone, [_]) => env.force_lazy(on_none), _ => return None, } }), Prim::Array8Find | Prim::Array16Find | Prim::Array32Find | Prim::Array64Find => { - step!(env, [_, elem_type, pred, array] => match array.as_ref() { + step!(env, [_, elem_type, pred, array] => match env.force_lazy(array).as_ref() { Value::ArrayLit(elems) => { for elem in elems { - match env.fun_app( - Plicity::Explicit, - pred.clone(), elem.clone()).as_ref() { + match env.fun_app(Plicity::Explicit, env.force_lazy(pred), elem).as_ref() { Value::ConstLit(Const::Bool(true)) => { return Some(Spanned::empty(Arc::new(Value::Stuck( Head::Prim(Prim::OptionSome), @@ -814,16 +844,16 @@ pub fn step(prim: Prim) -> Step { } Prim::Array8Index | Prim::Array16Index | Prim::Array32Index | Prim::Array64Index => { - step!(_, [_, _, index, array] => match array.as_ref() { + step!(env, [_, _, index, array] => match env.force_lazy(array).as_ref() { Value::ArrayLit(elems) => { - let index = match (index).as_ref() { + let index = match env.force_lazy(index).as_ref() { Value::ConstLit(Const::U8(index, _)) => Some(usize::from(*index)), Value::ConstLit(Const::U16(index, _)) => Some(usize::from(*index)), Value::ConstLit(Const::U32(index, _)) => usize::try_from(*index).ok(), Value::ConstLit(Const::U64(index, _)) => usize::try_from(*index).ok(), _ => return None, }?; - elems.get(index).cloned()? + env.force_lazy(elems.get(index)?) } _ => return None, }) diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 5be7f9dbe..3558f49f0 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -1,9 +1,11 @@ //! The semantics of the core language, implemented using [normalization by //! evaluation](https://en.wikipedia.org/wiki/Normalization_by_evaluation). +use std::cell::RefCell; use std::panic::panic_any; use std::sync::Arc; +use once_cell::sync::OnceCell; use scoped_arena::Scope; use crate::alloc::SliceVec; @@ -16,6 +18,15 @@ use crate::symbol::Symbol; /// the amount of sharing we can achieve during evaluation. pub type ArcValue<'arena> = Spanned>>; +pub type LocalExprs<'arena> = SharedEnv>; +pub type ItemExprs<'arena> = SliceEnv>; + +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum EvalMode { + Lazy, + Strict, +} + /// Values in weak-head-normal form, with bindings converted to closures. #[derive(Debug, Clone)] pub enum Value<'arena> { @@ -29,22 +40,27 @@ pub enum Value<'arena> { Universe, /// Dependent function types. - FunType(Plicity, Option, ArcValue<'arena>, Closure<'arena>), + FunType( + Plicity, + Option, + Arc>, // wrapped in `Arc` to keep size_of down + Closure<'arena>, + ), /// Function literals. FunLit(Plicity, Option, Closure<'arena>), /// Record types. RecordType(&'arena [Symbol], Telescope<'arena>), /// Record literals. - RecordLit(&'arena [Symbol], Vec>), + RecordLit(&'arena [Symbol], Vec>), /// Array literals. - ArrayLit(Vec>), + ArrayLit(Vec>), /// Record formats, consisting of a list of dependent formats. FormatRecord(&'arena [Symbol], Telescope<'arena>), /// Conditional format, consisting of a format and predicate. - FormatCond(Symbol, ArcValue<'arena>, Closure<'arena>), + FormatCond(Symbol, Arc>, Closure<'arena>), /// Overlap formats, consisting of a list of dependent formats, overlapping /// in memory. FormatOverlap(&'arena [Symbol], Telescope<'arena>), @@ -53,11 +69,58 @@ pub enum Value<'arena> { ConstLit(Const), } +/// Initialization operation for lazy values. +/// +/// We need to use a [defunctionalized] representation because Rust does not +/// allow closures of type `dyn (Clone + FnOnce() -> Arc)`. +/// +/// [defunctionalized]: https://en.wikipedia.org/wiki/Defunctionalization +#[derive(Clone, Debug)] +enum LazyInit<'arena> { + EvalTerm(LocalExprs<'arena>, &'arena Term<'arena>), + ApplyElim(Arc>, Arc>), +} + +#[derive(Debug, Clone)] +pub struct LazyValue<'arena> { + /// Initialization operation. Will be set to `None` if `cell` is forced. + init: RefCell>>, + /// A once-cell to hold the lazily initialized value. + cell: OnceCell>, +} + +impl<'arena> LazyValue<'arena> { + /// Eagerly construct the lazy value. + pub fn eager(value: ArcValue<'arena>) -> Self { + LazyValue { + init: RefCell::new(None), + cell: OnceCell::from(value), + } + } + + /// Create a delayed LazyValue which, when forced, will evaluate `term` in + /// `local_exprs` + pub fn delay(local_exprs: LocalExprs<'arena>, term: &'arena Term<'arena>) -> Self { + LazyValue { + init: RefCell::new(Some(LazyInit::EvalTerm(local_exprs, term))), + cell: OnceCell::new(), + } + } + + /// Lazily apply an elimination. + pub fn apply_elim(head: Arc>, elim: Elim<'arena>) -> Self { + LazyValue { + init: RefCell::new(Some(LazyInit::ApplyElim(head, Arc::new(elim)))), + cell: OnceCell::new(), + } + } +} + impl<'arena> Value<'arena> { pub fn prim(prim: Prim, params: impl IntoIterator>) -> Value<'arena> { let params = params .into_iter() - .map(|arg| Elim::FunApp(Plicity::Explicit, arg)) + .map(|arg| Elim::FunApp(Plicity::Explicit, LazyValue::eager(arg))) .collect(); Value::Stuck(Head::Prim(prim), params) } @@ -98,7 +161,7 @@ pub enum Head { #[derive(Debug, Clone)] pub enum Elim<'arena> { /// Function applications. - FunApp(Plicity, ArcValue<'arena>), + FunApp(Plicity, LazyValue<'arena>), /// Record projections. RecordProj(Symbol), /// Match on a constant. @@ -111,17 +174,14 @@ pub struct Closure<'arena> { /// Local environment where the closed [term][Self.term] is bound. A new /// entry will need to be pushed to this environment before evaluating the /// term. - local_exprs: SharedEnv>, + local_exprs: LocalExprs<'arena>, /// The term that is closed over. term: &'arena Term<'arena>, } impl<'arena> Closure<'arena> { /// Construct a closure. - pub fn new( - local_exprs: SharedEnv>, - term: &'arena Term<'arena>, - ) -> Closure<'arena> { + pub fn new(local_exprs: LocalExprs<'arena>, term: &'arena Term<'arena>) -> Closure<'arena> { Closure { local_exprs, term } } @@ -140,7 +200,7 @@ impl<'arena> Closure<'arena> { #[derive(Debug, Clone)] pub struct Telescope<'arena> { /// Local environment where the telescope's [terms][Self.terms] are bound. - local_exprs: SharedEnv>, + local_exprs: LocalExprs<'arena>, /// `Repr` should be applied to each term in the telescope. apply_repr: bool, /// The terms in the telescope. @@ -150,7 +210,7 @@ pub struct Telescope<'arena> { impl<'arena> Telescope<'arena> { /// Construct a telescope. pub fn new( - local_exprs: SharedEnv>, + local_exprs: LocalExprs<'arena>, terms: &'arena [Term<'arena>], ) -> Telescope<'arena> { Telescope { @@ -177,7 +237,7 @@ impl<'arena> Telescope<'arena> { /// The branches of a single-level pattern match. #[derive(Debug, Clone)] pub struct Branches<'arena, P> { - local_exprs: SharedEnv>, + local_exprs: LocalExprs<'arena>, pattern_branches: &'arena [(P, Term<'arena>)], default_branch: Option<(Option, &'arena Term<'arena>)>, } @@ -185,7 +245,7 @@ pub struct Branches<'arena, P> { impl<'arena, P> Branches<'arena, P> { /// Construct a single-level pattern match. pub fn new( - local_exprs: SharedEnv>, + local_exprs: LocalExprs<'arena>, pattern_branches: &'arena [(P, Term<'arena>)], default_branch: Option<(Option, &'arena Term<'arena>)>, ) -> Branches<'arena, P> { @@ -245,26 +305,43 @@ impl Error { /// Like the [`ElimEnv`], this allows for the running of computations, but /// also maintains a local environment, allowing for evaluation. pub struct EvalEnv<'arena, 'env> { + mode: EvalMode, elim_env: ElimEnv<'arena, 'env>, - local_exprs: &'env mut SharedEnv>, + local_exprs: &'env mut LocalExprs<'arena>, } impl<'arena, 'env> EvalEnv<'arena, 'env> { pub fn new( elim_env: ElimEnv<'arena, 'env>, - local_exprs: &'env mut SharedEnv>, + local_exprs: &'env mut LocalExprs<'arena>, ) -> EvalEnv<'arena, 'env> { EvalEnv { + mode: EvalMode::Lazy, elim_env, local_exprs, } } + pub fn with_mode(self, mode: EvalMode) -> Self { + Self { mode, ..self } + } + + pub fn delay_or_eval(&mut self, term: &'arena Term<'arena>) -> LazyValue<'arena> { + match self.mode { + EvalMode::Lazy => self.delay(term), + EvalMode::Strict => LazyValue::eager(self.eval(term)), + } + } + + pub fn delay(&self, term: &'arena Term<'arena>) -> LazyValue<'arena> { + LazyValue::delay(self.local_exprs.clone(), term) + } + fn quote_env(&self) -> QuoteEnv<'arena, 'env> { QuoteEnv::new(self.elim_env, self.local_exprs.len()) } - fn get_local_expr<'this: 'env>(&'this self, var: Index) -> &'env ArcValue<'arena> { + fn get_local_expr<'this: 'env>(&'this self, var: Index) -> &'env LazyValue<'arena> { let value = self.local_exprs.get_index(var); value.unwrap_or_else(|| panic_any(Error::UnboundLocalVar)) } @@ -287,21 +364,25 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { /// twitter thread](https://twitter.com/brendanzab/status/1423536653658771457)). pub fn eval(&mut self, term: &Term<'arena>) -> ArcValue<'arena> { match term { - Term::ItemVar(span, var) => { - Spanned::new(*span, Arc::clone(self.elim_env.get_item_expr(*var))) + Term::ItemVar(_, var) => { + let expr = self.elim_env.get_item_expr(*var); + self.elim_env.force_lazy(expr) } Term::MetaVar(span, var) => match self.elim_env.get_meta_expr(*var) { Some(value) => Spanned::new(*span, Arc::clone(value)), None => Spanned::new(*span, Arc::new(Value::meta_var(*var))), }, - Term::LocalVar(span, var) => Spanned::new(*span, Arc::clone(self.get_local_expr(*var))), + Term::LocalVar(_, var) => { + let expr = self.get_local_expr(*var); + self.elim_env.force_lazy(expr) + } Term::InsertedMeta(span, var, local_infos) => { 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); + let def_expr = self.delay_or_eval(def_expr); self.local_exprs.push(def_expr); let body_expr = self.eval(body_expr); self.local_exprs.pop(); @@ -315,7 +396,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Arc::new(Value::FunType( *plicity, *param_name, - self.eval(param_type), + Arc::new(self.delay_or_eval(param_type)), Closure::new(self.local_exprs.clone(), body_type), )), ), @@ -329,8 +410,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { ), Term::FunApp(span, plicity, head_expr, arg_expr) => { let head_expr = self.eval(head_expr); - let arg_expr = self.eval(arg_expr); - Spanned::merge(*span, self.elim_env.fun_app(*plicity, head_expr, arg_expr)) + let arg_expr = self.delay_or_eval(arg_expr); + Spanned::merge(*span, self.elim_env.fun_app(*plicity, head_expr, &arg_expr)) } Term::RecordType(span, labels, types) => { @@ -338,7 +419,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Spanned::new(*span, Arc::new(Value::RecordType(labels, types))) } Term::RecordLit(span, labels, exprs) => { - let exprs = exprs.iter().map(|expr| self.eval(expr)).collect(); + let exprs = exprs.iter().map(|expr| self.delay_or_eval(expr)).collect(); Spanned::new(*span, Arc::new(Value::RecordLit(labels, exprs))) } Term::RecordProj(span, head_expr, label) => { @@ -347,7 +428,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { } Term::ArrayLit(span, exprs) => { - let exprs = exprs.iter().map(|expr| self.eval(expr)).collect(); + let exprs = exprs.iter().map(|expr| self.delay_or_eval(expr)).collect(); Spanned::new(*span, Arc::new(Value::ArrayLit(exprs))) } @@ -356,7 +437,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Spanned::new(*span, Arc::new(Value::FormatRecord(labels, formats))) } Term::FormatCond(span, name, format, cond) => { - let format = self.eval(format); + let format = Arc::new(self.delay_or_eval(format)); let cond_expr = Closure::new(self.local_exprs.clone(), cond); Spanned::new(*span, Arc::new(Value::FormatCond(*name, format, cond_expr))) } @@ -386,10 +467,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { for (info, expr) in Iterator::zip(infos.iter(), self.local_exprs.iter()) { head_expr = match info { LocalInfo::Def => head_expr, - LocalInfo::Param => { - self.elim_env - .fun_app(Plicity::Explicit, head_expr, expr.clone()) - } + LocalInfo::Param => self.elim_env.fun_app(Plicity::Explicit, head_expr, expr), }; } head_expr @@ -402,13 +480,13 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { /// environment that would be needed for full evaluation. #[derive(Copy, Clone)] pub struct ElimEnv<'arena, 'env> { - item_exprs: &'env SliceEnv>, + item_exprs: &'env ItemExprs<'arena>, meta_exprs: &'env SliceEnv>>, } impl<'arena, 'env> ElimEnv<'arena, 'env> { pub fn new( - item_exprs: &'env SliceEnv>, + item_exprs: &'env ItemExprs<'arena>, meta_exprs: &'env SliceEnv>>, ) -> ElimEnv<'arena, 'env> { ElimEnv { @@ -417,10 +495,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { } } - pub fn eval_env( - &self, - local_exprs: &'env mut SharedEnv>, - ) -> EvalEnv<'arena, 'env> { + pub fn eval_env(&self, local_exprs: &'env mut LocalExprs<'arena>) -> EvalEnv<'arena, 'env> { EvalEnv::new(*self, local_exprs) } @@ -428,7 +503,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { ConversionEnv::new(*self, local_exprs) } - fn get_item_expr(&self, var: Level) -> &'env ArcValue<'arena> { + fn get_item_expr(&self, var: Level) -> &'env LazyValue<'arena> { let value = self.item_exprs.get_level(var); value.unwrap_or_else(|| panic_any(Error::UnboundItemVar)) } @@ -440,7 +515,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { /// Bring a value up-to-date with any new unification solutions that /// might now be present at the head of in the given value. - pub fn force(&self, value: &ArcValue<'arena>) -> ArcValue<'arena> { + pub fn force_metas(&self, value: &ArcValue<'arena>) -> ArcValue<'arena> { let mut forced_value = value.clone(); // Attempt to force metavariables until we don't see any more. while let Value::Stuck(Head::MetaVar(var), spine) = forced_value.as_ref() { @@ -456,11 +531,30 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { forced_value } + /// Force the evaluation of a lazy value. + pub fn force_lazy(&self, value: &LazyValue<'arena>) -> ArcValue<'arena> { + (value.cell) + .get_or_init(|| match value.init.replace(None) { + Some(LazyInit::EvalTerm(mut local_exprs, term)) => { + self.eval_env(&mut local_exprs).eval(term) + } + Some(LazyInit::ApplyElim(head, elim)) => match elim.as_ref() { + Elim::RecordProj(label) => self.record_proj(self.force_lazy(&head), *label), + Elim::FunApp(plicity, arg) => { + self.fun_app(*plicity, self.force_lazy(&head), arg) + } + Elim::ConstMatch(_) => todo!(), + }, + None => panic!("Lazy instance has previously been poisoned"), + }) + .clone() + } + /// Apply a closure to a value. pub fn apply_closure( &self, closure: &Closure<'arena>, - value: ArcValue<'arena>, + value: LazyValue<'arena>, ) -> ArcValue<'arena> { let mut local_exprs = closure.local_exprs.clone(); local_exprs.push(value); @@ -474,7 +568,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { mut telescope: Telescope<'arena>, ) -> Option<( ArcValue<'arena>, - impl FnOnce(ArcValue<'arena>) -> Telescope<'arena>, + impl FnOnce(LazyValue<'arena>) -> Telescope<'arena>, )> { let (term, terms) = telescope.terms.split_first()?; let mut env = self.eval_env(&mut telescope.local_exprs); @@ -518,18 +612,18 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { &self, arg_plicity: Plicity, mut head_expr: ArcValue<'arena>, - arg_expr: ArcValue<'arena>, + arg_expr: &LazyValue<'arena>, ) -> ArcValue<'arena> { match Arc::make_mut(&mut head_expr) { // Beta-reduction 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) + self.apply_closure(body_expr, arg_expr.clone()) } // The computation is stuck, preventing further reduction Value::Stuck(head, spine) => { - spine.push(Elim::FunApp(arg_plicity, arg_expr)); + spine.push(Elim::FunApp(arg_plicity, arg_expr.clone())); match head { Head::Prim(prim) => prim::step(*prim)(self, spine).unwrap_or(head_expr), _ => head_expr, @@ -543,12 +637,17 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { /// [beta-reduction] if possible. /// /// [beta-reduction]: https://ncatlab.org/nlab/show/beta-reduction - pub fn record_proj(&self, mut head_expr: ArcValue<'arena>, label: Symbol) -> ArcValue<'arena> { + pub fn record_proj( + &self, + mut head_expr: ArcValue<'arena>, // TODO: should `head_expr` be lazy? + label: Symbol, + ) -> ArcValue<'arena> { match Arc::make_mut(&mut head_expr) { // Beta-reduction Value::RecordLit(labels, exprs) => (labels.iter()) .position(|current_label| *current_label == label) .and_then(|expr_index| exprs.get(expr_index).cloned()) + .map(|lazy_value| self.force_lazy(&lazy_value)) .unwrap_or_else(|| panic_any(Error::InvalidRecordProj)), // The computation is stuck, preventing further reduction Value::Stuck(_, spine) => { @@ -580,7 +679,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { let mut local_exprs = branches.local_exprs.clone(); match branches.default_branch { Some((_, default_expr)) => { - local_exprs.push(head_expr); + local_exprs.push(LazyValue::eager(head_expr)); self.eval_env(&mut local_exprs).eval(default_expr) } None => panic_any(Error::MissingConstDefault), @@ -598,7 +697,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { /// Apply an expression to an elimination spine. fn apply_spine(&self, head_expr: ArcValue<'arena>, spine: &[Elim<'arena>]) -> ArcValue<'arena> { spine.iter().fold(head_expr, |head_expr, elim| match elim { - Elim::FunApp(plicity, arg_expr) => self.fun_app(*plicity, head_expr, arg_expr.clone()), + Elim::FunApp(plicity, arg_expr) => self.fun_app(*plicity, head_expr, arg_expr), Elim::RecordProj(label) => self.record_proj(head_expr, *label), Elim::ConstMatch(split) => self.const_match(head_expr, split.clone()), }) @@ -610,7 +709,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { Value::FormatRecord(labels, formats) | Value::FormatOverlap(labels, formats) => { Value::RecordType(labels, formats.clone().apply_repr()) } - Value::FormatCond(_, format, _) => return self.format_repr(format), + Value::FormatCond(_, format, _) => return self.format_repr(&self.force_lazy(format)), Value::Stuck(Head::Prim(prim), spine) => match prim::repr(*prim)(self, spine) { Some(r#type) => return r#type, None => Value::prim(Prim::FormatRepr, [format.clone()]), @@ -667,7 +766,7 @@ 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 value = self.elim_env.force(value); + let value = self.elim_env.force_metas(value); let span = value.span(); match value.as_ref() { Value::Stuck(head, spine) => spine.iter().fold( @@ -677,7 +776,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { span, *plicity, scope.to_scope(head_expr), - scope.to_scope(self.quote(scope, arg_expr)), + scope.to_scope(self.quote_lazy(scope, arg_expr)), ), Elim::RecordProj(label) => { Term::RecordProj(span, scope.to_scope(head_expr), *label) @@ -716,7 +815,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { span, *plicity, *param_name, - scope.to_scope(self.quote(scope, param_type)), + scope.to_scope(self.quote_lazy(scope, param_type)), self.quote_closure(scope, body_type), ), Value::FunLit(plicity, param_name, body_expr) => Term::FunLit( @@ -734,11 +833,11 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { Value::RecordLit(labels, exprs) => Term::RecordLit( span, scope.to_scope_from_iter(labels.iter().copied()), - scope.to_scope_from_iter(exprs.iter().map(|expr| self.quote(scope, expr))), + scope.to_scope_from_iter((exprs.iter()).map(|expr| self.quote_lazy(scope, expr))), ), Value::ArrayLit(exprs) => Term::ArrayLit( span, - scope.to_scope_from_iter(exprs.iter().map(|expr| self.quote(scope, expr))), + scope.to_scope_from_iter(exprs.iter().map(|expr| self.quote_lazy(scope, expr))), ), Value::FormatRecord(labels, formats) => Term::FormatRecord( @@ -749,7 +848,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { Value::FormatCond(label, format, cond) => Term::FormatCond( span, *label, - scope.to_scope(self.quote(scope, format)), + scope.to_scope(self.quote_lazy(scope, format)), self.quote_closure(scope, cond), ), Value::FormatOverlap(labels, formats) => Term::FormatOverlap( @@ -762,6 +861,14 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { } } + pub fn quote_lazy<'out_arena>( + &mut self, + scope: &'out_arena Scope<'out_arena>, + value: &LazyValue<'in_arena>, + ) -> Term<'out_arena> { + self.quote(scope, &self.elim_env.force_lazy(value)) + } + /// Quote an [elimination head][Head] back into a [term][Term]. fn quote_head<'out_arena>( &mut self, @@ -793,8 +900,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { scope: &'out_arena Scope<'out_arena>, closure: &Closure<'in_arena>, ) -> &'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)); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); + let value = self.elim_env.apply_closure(closure, var); self.push_local(); let term = self.quote(scope, &value); @@ -814,8 +923,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { let mut terms = SliceVec::new(scope, telescope.len()); while let Some((value, next_telescope)) = self.elim_env.split_telescope(telescope) { - let var = Arc::new(Value::local_var(self.local_exprs.next_level())); - telescope = next_telescope(Spanned::empty(var)); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); + telescope = next_telescope(var); terms.push(self.quote(scope, &value)); self.local_exprs.push(); } @@ -977,10 +1088,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { scope.to_scope(head_expr), scope.to_scope(self.unfold_metas(scope, arg_expr)), )), - TermOrValue::Value(head_expr) => { - let arg_expr = self.eval(arg_expr); - TermOrValue::Value(self.elim_env.fun_app(*plicity, head_expr, arg_expr)) - } + TermOrValue::Value(head_expr) => TermOrValue::Value(self.elim_env.fun_app( + *plicity, + head_expr, + &LazyValue::delay(self.local_exprs.clone(), arg_expr), + )), } } Term::RecordProj(span, head_expr, label) => { @@ -1024,9 +1136,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { scope: &'out_arena Scope<'out_arena>, term: &Term<'arena>, ) -> &'out_arena Term<'out_arena> { - let var = Arc::new(Value::local_var(self.local_exprs.len().next_level())); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.len().next_level(), + )))); - self.local_exprs.push(Spanned::empty(var)); + self.local_exprs.push(var); let term = self.unfold_metas(scope, term); self.local_exprs.pop(); @@ -1043,8 +1157,10 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { let terms = scope.to_scope_from_iter(terms.iter().map(|term| { let term = self.unfold_metas(scope, term); - let var = Arc::new(Value::local_var(self.local_exprs.len().next_level())); - self.local_exprs.push(Spanned::empty(var)); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.len().next_level(), + )))); + self.local_exprs.push(var); term })); @@ -1091,9 +1207,9 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { /// /// [computationally equal]: https://ncatlab.org/nlab/show/equality#computational_equality /// [eta-conversion]: https://ncatlab.org/nlab/show/eta-conversion - pub fn is_equal(&mut self, value0: &ArcValue<'_>, value1: &ArcValue<'_>) -> bool { - let value0 = self.elim_env.force(value0); - let value1 = self.elim_env.force(value1); + pub fn is_equal(&mut self, value0: &ArcValue<'arena>, value1: &ArcValue<'arena>) -> bool { + let value0 = self.elim_env.force_metas(value0); + let value1 = self.elim_env.force_metas(value1); match (value0.as_ref(), value1.as_ref()) { // `ReportedError`s result from errors that have already been @@ -1111,7 +1227,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { Value::FunType(plicity1, _, param_type1, body_type1), ) => { plicity0 == plicity1 - && self.is_equal(param_type0, param_type1) + && self.is_equal_lazy(param_type0, param_type1) && self.is_equal_closures(body_type0, body_type1) } (Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) => { @@ -1130,7 +1246,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { (Value::RecordLit(labels0, exprs0), Value::RecordLit(labels1, exprs1)) => { labels0 == labels1 && Iterator::zip(exprs0.iter(), exprs1.iter()) - .all(|(expr0, expr1)| self.is_equal(expr0, expr1)) + .all(|(expr0, expr1)| self.is_equal_lazy(expr0, expr1)) } (Value::RecordLit(labels, exprs), _) => { self.is_equal_record_lit(labels, exprs, &value1) @@ -1141,7 +1257,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { (Value::ArrayLit(exprs0), Value::ArrayLit(exprs1)) => { Iterator::zip(exprs0.iter(), exprs1.iter()) - .all(|(expr0, expr1)| self.is_equal(expr0, expr1)) + .all(|(expr0, expr1)| self.is_equal_lazy(expr0, expr1)) } (Value::FormatRecord(labels0, formats0), Value::FormatRecord(labels1, formats1)) @@ -1154,7 +1270,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { Value::FormatCond(label1, format1, cond1), ) => { label0 == label1 - && self.is_equal(format0, format1) + && self.is_equal_lazy(format0, format1) && self.is_equal_closures(cond0, cond1) } @@ -1164,13 +1280,24 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { } } + pub fn is_equal_lazy( + &mut self, + value0: &LazyValue<'arena>, + value1: &LazyValue<'arena>, + ) -> bool { + self.is_equal( + &self.elim_env.force_lazy(value0), + &self.elim_env.force_lazy(value1), + ) + } + /// Check that two elimination spines are equal. - pub fn is_equal_spines(&mut self, spine0: &[Elim<'_>], spine1: &[Elim<'_>]) -> bool { + pub fn is_equal_spines(&mut self, spine0: &[Elim<'arena>], spine1: &[Elim<'arena>]) -> bool { spine0.len() == spine1.len() && Iterator::zip(spine0.iter(), spine1.iter()).all(|(elim0, elim1)| { match (elim0, elim1) { (Elim::FunApp(plicity0, expr0), Elim::FunApp(plicity1, expr1)) => { - plicity0 == plicity1 && self.is_equal(expr0, expr1) + plicity0 == plicity1 && self.is_equal_lazy(expr0, expr1) } (Elim::RecordProj(label0), Elim::RecordProj(label1)) => label0 == label1, (Elim::ConstMatch(branches0), Elim::ConstMatch(branches1)) => { @@ -1182,8 +1309,14 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { } /// Check that two [closures][Closure] are equal. - pub fn is_equal_closures(&mut self, closure0: &Closure<'_>, closure1: &Closure<'_>) -> bool { - let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level()))); + pub fn is_equal_closures( + &mut self, + closure0: &Closure<'arena>, + closure1: &Closure<'arena>, + ) -> bool { + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); let value0 = self.elim_env.apply_closure(closure0, var.clone()); let value1 = self.elim_env.apply_closure(closure1, var); @@ -1197,8 +1330,8 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { /// Check that two [telescopes][Telescope] are equal. pub fn is_equal_telescopes( &mut self, - telescope0: &Telescope<'_>, - telescope1: &Telescope<'_>, + telescope0: &Telescope<'arena>, + telescope1: &Telescope<'arena>, ) -> bool { if telescope0.len() != telescope1.len() { return false; @@ -1217,7 +1350,9 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { return false; } - let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level()))); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); telescope0 = next_telescope0(var.clone()); telescope1 = next_telescope1(var); self.local_exprs.push(); @@ -1230,8 +1365,8 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { /// Check that two [constant branches][Branches] are equal. fn is_equal_branches( &mut self, - branches0: &Branches<'_, P>, - branches1: &Branches<'_, P>, + branches0: &Branches<'arena, P>, + branches1: &Branches<'arena, P>, ) -> bool { use SplitBranches::*; @@ -1267,11 +1402,13 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { fn is_equal_fun_lit( &mut self, plicity: Plicity, - body_expr: &Closure<'_>, - value: &ArcValue<'_>, + body_expr: &Closure<'arena>, + value: &ArcValue<'arena>, ) -> bool { - let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level()))); - let value = self.elim_env.fun_app(plicity, value.clone(), var.clone()); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); + let value = self.elim_env.fun_app(plicity, value.clone(), &var); let body_expr = self.elim_env.apply_closure(body_expr, var); self.push_local(); @@ -1289,12 +1426,12 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { fn is_equal_record_lit( &mut self, labels: &[Symbol], - exprs: &[ArcValue<'_>], - value: &ArcValue<'_>, + exprs: &[LazyValue<'arena>], + value: &ArcValue<'arena>, ) -> bool { Iterator::zip(labels.iter(), exprs.iter()).all(|(label, expr)| { let field_value = self.elim_env.record_proj(value.clone(), *label); - self.is_equal(expr, &field_value) + self.is_equal(&self.elim_env.force_lazy(expr), &field_value) }) } } @@ -1349,5 +1486,6 @@ mod tests { #[cfg(target_pointer_width = "64")] fn value_size() { assert_eq!(std::mem::size_of::(), 72); + assert_eq!(std::mem::size_of::(), 80); } } diff --git a/fathom/src/driver.rs b/fathom/src/driver.rs index 36fb4a94d..7a03a1fb5 100644 --- a/fathom/src/driver.rs +++ b/fathom/src/driver.rs @@ -7,6 +7,7 @@ use codespan_reporting::files::SimpleFiles; use codespan_reporting::term::termcolor::{BufferedStandardStream, ColorChoice, WriteColor}; use crate::core::binary::{self, BufferError, ReadError}; +use crate::core::semantics::EvalMode; use crate::files::{FileId, Files}; use crate::source::{ByteRange, ProgramSource, SourceTooBig, Span, MAX_SOURCE_LEN}; use crate::surface::elaboration::ItemEnv; @@ -264,8 +265,14 @@ impl<'surface, 'core> Driver<'surface, 'core> { return Status::Error; } - let term = context.eval_env().normalize(&self.core_scope, &term); - let r#type = context.eval_env().normalize(&self.core_scope, &r#type); + let term = context + .eval_env() + .with_mode(EvalMode::Strict) + .normalize(&self.core_scope, &term); + let r#type = context + .eval_env() + .with_mode(EvalMode::Strict) + .normalize(&self.core_scope, &r#type); self.surface_scope.reset(); // Reuse the surface scope for distillation let mut context = context.distillation_context(&self.surface_scope); @@ -443,8 +450,8 @@ impl<'surface, 'core> Driver<'surface, 'core> { fn read_error_to_diagnostic( &self, - err: ReadError<'_>, - context: &mut elaboration::Context, + err: ReadError<'core>, + context: &mut elaboration::Context<'core>, ) -> Diagnostic { match err { ReadError::ReadFailFormat(span) => Diagnostic::error() diff --git a/fathom/src/surface.rs b/fathom/src/surface.rs index 354a86c21..65c46b17d 100644 --- a/fathom/src/surface.rs +++ b/fathom/src/surface.rs @@ -93,7 +93,7 @@ pub enum Pattern { /// Boolean literal patterns BooleanLiteral(Range, bool), // TODO: Record literal patterns - // RecordLiteral(Range, &'arena [((Range, StringId), Pattern<'arena, Range>)]), + // RecordLiteral(Range, &'arena [((Range, Symbol), Pattern<'arena, Range>)]), } #[derive(Debug, Clone, Copy)] diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index cf4a19466..3e5bd6071 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -26,7 +26,7 @@ use std::sync::Arc; use scoped_arena::Scope; use crate::alloc::SliceVec; -use crate::core::semantics::{self, ArcValue, Head, Telescope, Value}; +use crate::core::semantics::{self, ArcValue, Head, LazyValue, LocalExprs, Telescope, Value}; use crate::core::{self, prim, Const, Plicity, Prim, UIntStyle}; use crate::env::{self, EnvLen, Level, SharedEnv, UniqueEnv}; use crate::files::FileId; @@ -48,7 +48,7 @@ pub struct ItemEnv<'arena> { /// Types of items. types: UniqueEnv>, /// Expressions of items. - exprs: UniqueEnv>, + exprs: UniqueEnv>, } impl<'arena> ItemEnv<'arena> { @@ -61,7 +61,7 @@ impl<'arena> ItemEnv<'arena> { } } - fn push_definition(&mut self, name: Symbol, r#type: ArcValue<'arena>, expr: ArcValue<'arena>) { + fn push_definition(&mut self, name: Symbol, r#type: ArcValue<'arena>, expr: LazyValue<'arena>) { self.names.push(name); self.types.push(r#type); self.exprs.push(expr); @@ -97,7 +97,7 @@ struct LocalEnv<'arena> { infos: UniqueEnv, /// Expressions that will be substituted for local variables during /// [evaluation][semantics::EvalEnv::eval]. - exprs: SharedEnv>, + exprs: LocalExprs<'arena>, } impl<'arena> LocalEnv<'arena> { @@ -124,22 +124,29 @@ impl<'arena> LocalEnv<'arena> { } /// Push a local definition onto the context. - fn push_def(&mut self, name: Option, expr: ArcValue<'arena>, r#type: ArcValue<'arena>) { + fn push_def( + &mut self, + name: Option, + expr: LazyValue<'arena>, + r#type: ArcValue<'arena>, + ) { self.names.push(name); - self.types.push(r#type); self.infos.push(core::LocalInfo::Def); + self.types.push(r#type); self.exprs.push(expr); } /// Push a local parameter onto the context. - fn push_param(&mut self, name: Option, r#type: ArcValue<'arena>) -> ArcValue<'arena> { + fn push_param(&mut self, name: Option, r#type: ArcValue<'arena>) -> LazyValue<'arena> { // An expression that refers to itself once it is pushed onto the local // expression environment. - let expr = Spanned::empty(Arc::new(Value::local_var(self.exprs.len().next_level()))); + let expr = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.exprs.len().next_level(), + )))); self.names.push(name); - self.types.push(r#type); self.infos.push(core::LocalInfo::Param); + self.types.push(r#type); self.exprs.push(expr.clone()); expr @@ -255,9 +262,9 @@ pub struct Context<'arena> { scope: &'arena Scope<'arena>, // Commonly used values, cached to increase sharing. - universe: ArcValue<'static>, - format_type: ArcValue<'static>, - bool_type: ArcValue<'static>, + universe: ArcValue<'arena>, + format_type: ArcValue<'arena>, + bool_type: ArcValue<'arena>, /// Primitive environment. prim_env: prim::Env<'arena>, @@ -418,7 +425,7 @@ impl<'arena> Context<'arena> { ) } - fn pretty_value(&self, value: &ArcValue<'_>) -> String { + fn pretty_value(&self, value: &ArcValue<'arena>) -> String { let term = self.quote_env().unfolding_metas().quote(self.scope, value); let surface_term = self.distillation_context(self.scope).check(&term); @@ -579,8 +586,8 @@ impl<'arena> Context<'arena> { to: &ArcValue<'arena>, ) -> core::Term<'arena> { let span = expr.span(); - let from = self.elim_env().force(from); - let to = self.elim_env().force(to); + let from = self.elim_env().force_metas(from); + let to = self.elim_env().force_metas(to); match (from.as_ref(), to.as_ref()) { // Coerce format descriptions to their representation types by @@ -638,7 +645,8 @@ impl<'arena> Context<'arena> { Item::Def(item) => { let (expr, r#type) = self.synth_fun_lit(item.range, item.params, item.expr, item.r#type); - let expr_value = self.eval_env().eval(&expr); + let expr = self.scope.to_scope(expr); + let expr_value = self.eval_env().delay(expr); let type_value = self.eval_env().eval(&r#type); self.item_env @@ -647,7 +655,7 @@ impl<'arena> Context<'arena> { items.push(core::Item::Def { label: item.label.1, r#type: self.scope.to_scope(r#type), - expr: self.scope.to_scope(expr), + expr, }); } Item::ReportedError(_) => {} @@ -894,7 +902,7 @@ impl<'arena> Context<'arena> { fn push_local_def( &mut self, pattern: CheckedPattern, - expr: ArcValue<'arena>, + expr: LazyValue<'arena>, r#type: ArcValue<'arena>, ) -> Option { let name = match pattern { @@ -921,7 +929,7 @@ impl<'arena> Context<'arena> { &mut self, pattern: CheckedPattern, r#type: ArcValue<'arena>, - ) -> (Option, ArcValue<'arena>) { + ) -> (Option, LazyValue<'arena>) { let name = match pattern { CheckedPattern::Binder(_, name) => Some(name), CheckedPattern::Placeholder(_) => None, @@ -966,7 +974,7 @@ impl<'arena> Context<'arena> { expected_type: &ArcValue<'arena>, ) -> core::Term<'arena> { let file_range = self.file_range(surface_term.range()); - let expected_type = self.elim_env().force(expected_type); + let expected_type = self.elim_env().force_metas(expected_type); match (surface_term, expected_type.as_ref()) { (Term::Paren(_, term), _) => self.check(term, &expected_type), @@ -974,7 +982,8 @@ impl<'arena> Context<'arena> { let (def_pattern, def_type, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type); let def_expr = self.check(def_expr, &def_type_value); - let def_expr_value = self.eval_env().eval(&def_expr); + let def_expr = self.scope.to_scope(def_expr); + let def_expr_value = self.eval_env().delay(def_expr); let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants let body_expr = self.check(body_expr, &expected_type); @@ -984,7 +993,7 @@ impl<'arena> Context<'arena> { file_range.into(), def_name, self.scope.to_scope(def_type), - self.scope.to_scope(def_expr), + def_expr, self.scope.to_scope(body_expr), ) } @@ -1043,8 +1052,9 @@ impl<'arena> Context<'arena> { let name_expr = Term::Name(expr_field.label.0, expr_field.label.1); let expr = expr_field.expr.as_ref().unwrap_or(&name_expr); let expr = self.check(expr, &r#type); - types = next_types(self.eval_env().eval(&expr)); - exprs.push(expr); + let expr = self.scope.to_scope(expr); + types = next_types(self.eval_env().delay(expr)); + exprs.push(expr.clone()); } core::Term::RecordLit(file_range.into(), labels, exprs.into()) @@ -1130,8 +1140,9 @@ impl<'arena> Context<'arena> { Option::zip(elem_exprs.next(), self.elim_env().split_telescope(types)) { let expr = self.check(elem_expr, &r#type); - types = next_types(self.eval_env().eval(&expr)); - exprs.push(expr); + let expr = self.scope.to_scope(expr); + types = next_types(self.eval_env().delay(expr)); + exprs.push(expr.clone()); } core::Term::RecordLit(file_range.into(), labels, exprs.into()) @@ -1165,7 +1176,10 @@ impl<'arena> Context<'arena> { } }; - let len = match len_value.map(|val| val.as_ref()) { + let len_value = len_value.map(|len_value| self.elim_env().force_lazy(len_value)); + let elem_type = self.elim_env().force_lazy(elem_type); + + let len = match len_value.as_ref().map(|val| val.as_ref()) { None => Some(elem_exprs.len() as u64), Some(Value::ConstLit(Const::U8(len, _))) => Some(*len as u64), Some(Value::ConstLit(Const::U16(len, _))) => Some(*len as u64), @@ -1181,20 +1195,20 @@ impl<'arena> Context<'arena> { Some(len) if elem_exprs.len() as u64 == len => core::Term::ArrayLit( file_range.into(), self.scope.to_scope_from_iter( - (elem_exprs.iter()).map(|elem_expr| self.check(elem_expr, elem_type)), + (elem_exprs.iter()).map(|elem_expr| self.check(elem_expr, &elem_type)), ), ), _ => { // Check the array elements anyway in order to report // any errors inside the literal as well. for elem_expr in *elem_exprs { - self.check(elem_expr, elem_type); + self.check(elem_expr, &elem_type); } self.push_message(Message::MismatchedArrayLength { range: file_range, found_len: elem_exprs.len(), - expected_len: self.pretty_value(len_value.unwrap()), + expected_len: self.pretty_value(&len_value.unwrap()), }); core::Term::Prim(file_range.into(), Prim::ReportedError) @@ -1275,17 +1289,18 @@ impl<'arena> Context<'arena> { ) -> (core::Term<'arena>, ArcValue<'arena>) { let file_range = self.file_range(range); while let Value::FunType(Plicity::Implicit, name, param_type, body_type) = - self.elim_env().force(&r#type).as_ref() + self.elim_env().force_metas(&r#type).as_ref() { let source = MetaSource::ImplicitArg(file_range, *name); - let arg_term = self.push_unsolved_term(source, param_type.clone()); - let arg_value = self.eval_env().eval(&arg_term); + let arg_term = self.push_unsolved_term(source, self.elim_env().force_lazy(param_type)); + let arg_term = self.scope.to_scope(arg_term); + let arg_value = self.eval_env().delay(arg_term); term = core::Term::FunApp( file_range.into(), Plicity::Implicit, self.scope.to_scope(term), - self.scope.to_scope(arg_term), + arg_term, ); r#type = self.elim_env().apply_closure(body_type, arg_value); } @@ -1376,7 +1391,8 @@ impl<'arena> Context<'arena> { let (def_pattern, def_type, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type); let def_expr = self.check(def_expr, &def_type_value); - let def_expr_value = self.eval_env().eval(&def_expr); + let def_expr = self.scope.to_scope(def_expr); + let def_expr_value = self.eval_env().delay(def_expr); let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); let (body_expr, body_type) = self.synth(body_expr); @@ -1386,7 +1402,7 @@ impl<'arena> Context<'arena> { file_range.into(), def_name, self.scope.to_scope(def_type), - self.scope.to_scope(def_expr), + def_expr, self.scope.to_scope(body_expr), ); @@ -1477,7 +1493,7 @@ impl<'arena> Context<'arena> { let (mut head_expr, mut head_type) = self.synth(head_expr); for arg in *args { - head_type = self.elim_env().force(&head_type); + head_type = self.elim_env().force_metas(&head_type); match arg.plicity { Plicity::Implicit => {} @@ -1524,14 +1540,15 @@ impl<'arena> Context<'arena> { let arg_range = arg.term.range(); head_range = ByteRange::merge(head_range, arg_range); - let arg_expr = self.check(&arg.term, param_type); - let arg_expr_value = self.eval_env().eval(&arg_expr); + let arg_expr = self.check(&arg.term, &self.elim_env().force_lazy(param_type)); + let arg_expr = self.scope.to_scope(arg_expr); + let arg_expr_value = self.eval_env().delay(arg_expr); head_expr = core::Term::FunApp( self.file_range(head_range).into(), arg.plicity, self.scope.to_scope(head_expr), - self.scope.to_scope(arg_expr), + arg_expr, ); head_type = self.elim_env().apply_closure(body_type, arg_expr_value); } @@ -1601,7 +1618,7 @@ impl<'arena> Context<'arena> { let (mut head_expr, mut head_type) = self.synth_and_insert_implicit_apps(head_expr); 'labels: for (label_range, proj_label) in *labels { - head_type = self.elim_env().force(&head_type); + head_type = self.elim_env().force_metas(&head_type); match (&head_expr, head_type.as_ref()) { // Ensure that the head of the projection is a record (_, Value::RecordType(labels, types)) => { @@ -1632,7 +1649,7 @@ impl<'arena> Context<'arena> { // looking for the field. let head_expr = head_expr_value.clone(); let expr = self.elim_env().record_proj(head_expr, label); - types = next_types(expr); + types = next_types(LazyValue::eager(expr)); } } // Couldn't find the field in the record type. @@ -1726,16 +1743,17 @@ impl<'arena> Context<'arena> { let file_range = self.file_range(range); match params.split_first() { Some((param, next_params)) => { - let body_type = self.elim_env().force(expected_type); + let body_type = self.elim_env().force_metas(expected_type); match body_type.as_ref() { Value::FunType(param_plicity, _, param_type, next_body_type) if param.plicity == *param_plicity => { let range = ByteRange::merge(param.pattern.range(), body_expr.range()); + let param_type = self.elim_env().force_lazy(param_type); let pattern = self.check_ann_pattern( ¶m.pattern, param.r#type.as_ref(), - param_type, + ¶m_type, ); let (name, arg_expr) = self.push_local_param(pattern, param_type.clone()); @@ -1756,7 +1774,9 @@ impl<'arena> Context<'arena> { Value::FunType(Plicity::Implicit, param_name, param_type, next_body_type) if param.plicity == Plicity::Explicit => { - let arg_expr = self.local_env.push_param(*param_name, param_type.clone()); + let arg_expr = self + .local_env + .push_param(*param_name, self.elim_env().force_lazy(param_type)); let body_type = self.elim_env().apply_closure(next_body_type, arg_expr); let body_expr = self.check_fun_lit(range, params, body_expr, &body_type); self.local_env.pop(); @@ -1857,8 +1877,8 @@ impl<'arena> Context<'arena> { // de-sugar into function application let (lhs_expr, lhs_type) = self.synth_and_insert_implicit_apps(lhs); let (rhs_expr, rhs_type) = self.synth_and_insert_implicit_apps(rhs); - let lhs_type = self.elim_env().force(&lhs_type); - let rhs_type = self.elim_env().force(&rhs_type); + let lhs_type = self.elim_env().force_metas(&lhs_type); + let rhs_type = self.elim_env().force_metas(&rhs_type); let operand_types = Option::zip(lhs_type.match_prim_spine(), rhs_type.match_prim_spine()); let (fun, body_type) = match (op, operand_types) { @@ -2200,7 +2220,7 @@ impl<'arena> Context<'arena> { let match_info = MatchInfo { range, scrutinee: self.synth_scrutinee(scrutinee_expr), - expected_type: self.elim_env().force(expected_type), + expected_type: self.elim_env().force_metas(expected_type), }; self.elab_match(&match_info, true, equations.iter()) @@ -2238,7 +2258,7 @@ impl<'arena> Context<'arena> { self.check_match_reachable(is_reachable, range); let def_name = Some(name); - let def_expr = self.eval_env().eval(match_info.scrutinee.expr); + let def_expr = self.eval_env().delay(match_info.scrutinee.expr); let def_type_value = match_info.scrutinee.r#type.clone(); let def_type = self.quote_env().quote(self.scope, &def_type_value); diff --git a/fathom/src/surface/elaboration/unification.rs b/fathom/src/surface/elaboration/unification.rs index 852c4e69a..b85a21658 100644 --- a/fathom/src/surface/elaboration/unification.rs +++ b/fathom/src/surface/elaboration/unification.rs @@ -21,7 +21,8 @@ use scoped_arena::Scope; use crate::alloc::SliceVec; use crate::core::semantics::{ - self, ArcValue, Branches, Closure, Elim, Head, SplitBranches, Telescope, Value, + self, ArcValue, Branches, Closure, Elim, Head, ItemExprs, LazyValue, SplitBranches, Telescope, + Value, }; use crate::core::{Prim, Term}; use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv, UniqueEnv}; @@ -164,7 +165,7 @@ pub struct Context<'arena, 'env> { /// each call to [`Context::solve`] in order to reuse previous allocations. renaming: &'env mut PartialRenaming, /// Item expressions. - item_exprs: &'env SliceEnv>, + item_exprs: &'env ItemExprs<'arena>, /// The length of the local environment. local_exprs: EnvLen, /// Solutions for metavariables. @@ -175,7 +176,7 @@ impl<'arena, 'env> Context<'arena, 'env> { pub fn new( scope: &'arena Scope<'arena>, renaming: &'env mut PartialRenaming, - item_exprs: &'env SliceEnv>, + item_exprs: &'env ItemExprs<'arena>, local_exprs: EnvLen, meta_exprs: &'env mut SliceEnv>>, ) -> Context<'arena, 'env> { @@ -203,8 +204,8 @@ impl<'arena, 'env> Context<'arena, 'env> { return Ok(()); } - let value0 = self.elim_env().force(value0); - let value1 = self.elim_env().force(value1); + let value0 = self.elim_env().force_metas(value0); + let value1 = self.elim_env().force_metas(value1); match (value0.as_ref(), value1.as_ref()) { // `ReportedError`s result from errors that have already been @@ -236,7 +237,7 @@ impl<'arena, 'env> Context<'arena, 'env> { Value::FunType(plicity0, _, param_type0, body_type0), Value::FunType(plicity1, _, param_type1, body_type1), ) if plicity0 == plicity1 => { - self.unify(param_type0, param_type1)?; + self.unify_lazy(param_type0, param_type1)?; self.unify_closures(body_type0, body_type1) } (Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) @@ -262,7 +263,7 @@ impl<'arena, 'env> Context<'arena, 'env> { return Err(Error::Mismatch); } for (expr0, expr1) in Iterator::zip(exprs0.iter(), exprs1.iter()) { - self.unify(expr0, expr1)?; + self.unify_lazy(expr0, expr1)?; } Ok(()) } @@ -273,7 +274,7 @@ impl<'arena, 'env> Context<'arena, 'env> { for (elem_expr0, elem_expr1) in Iterator::zip(elem_exprs0.iter(), elem_exprs1.iter()) { - self.unify(elem_expr0, elem_expr1)?; + self.unify_lazy(elem_expr0, elem_expr1)?; } Ok(()) } @@ -292,7 +293,7 @@ impl<'arena, 'env> Context<'arena, 'env> { if label0 != label1 { return Err(Error::Mismatch); } - self.unify(format0, format1)?; + self.unify_lazy(format0, format1)?; self.unify_closures(cond0, cond1) } @@ -309,6 +310,17 @@ impl<'arena, 'env> Context<'arena, 'env> { } } + pub fn unify_lazy( + &mut self, + value0: &LazyValue<'arena>, + value1: &LazyValue<'arena>, + ) -> Result<(), Error> { + self.unify( + &self.elim_env().force_lazy(value0), + &self.elim_env().force_lazy(value1), + ) + } + /// Unify two elimination spines. fn unify_spines( &mut self, @@ -323,7 +335,7 @@ impl<'arena, 'env> Context<'arena, 'env> { (Elim::FunApp(plicity0, arg_expr0), Elim::FunApp(plicity1, arg_expr1)) if plicity0 == plicity1 => { - self.unify(arg_expr0, arg_expr1)?; + self.unify_lazy(arg_expr0, arg_expr1)?; } (Elim::RecordProj(label0), Elim::RecordProj(label1)) if label0 == label1 => {} (Elim::ConstMatch(branches0), Elim::ConstMatch(branches1)) => { @@ -343,7 +355,9 @@ impl<'arena, 'env> Context<'arena, 'env> { closure0: &Closure<'arena>, closure1: &Closure<'arena>, ) -> Result<(), Error> { - let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level()))); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); let value0 = self.elim_env().apply_closure(closure0, var.clone()); let value1 = self.elim_env().apply_closure(closure1, var); @@ -377,7 +391,9 @@ impl<'arena, 'env> Context<'arena, 'env> { return Err(error); } - let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level()))); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); telescope0 = next_telescope0(var.clone()); telescope1 = next_telescope1(var); self.local_exprs.push(); @@ -433,8 +449,10 @@ impl<'arena, 'env> Context<'arena, 'env> { body_expr: &Closure<'arena>, value: &ArcValue<'arena>, ) -> Result<(), Error> { - let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level()))); - let value = self.elim_env().fun_app(plicity, value.clone(), var.clone()); + let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.local_exprs.next_level(), + )))); + let value = self.elim_env().fun_app(plicity, value.clone(), &var); let body_expr = self.elim_env().apply_closure(body_expr, var); self.local_exprs.push(); @@ -452,12 +470,12 @@ impl<'arena, 'env> Context<'arena, 'env> { fn unify_record_lit( &mut self, labels: &[Symbol], - exprs: &[ArcValue<'arena>], + exprs: &[LazyValue<'arena>], value: &ArcValue<'arena>, ) -> Result<(), Error> { for (label, expr) in Iterator::zip(labels.iter(), exprs.iter()) { let field_value = self.elim_env().record_proj(value.clone(), *label); - self.unify(expr, &field_value)?; + self.unify(&self.elim_env().force_lazy(expr), &field_value)?; } Ok(()) } @@ -499,14 +517,17 @@ impl<'arena, 'env> Context<'arena, 'env> { for elim in spine { match elim { - Elim::FunApp(_, arg_expr) => match self.elim_env().force(arg_expr).as_ref() { - Value::Stuck(Head::LocalVar(source_var), spine) - if spine.is_empty() && self.renaming.set_local(*source_var) => {} - Value::Stuck(Head::LocalVar(source_var), _) => { - return Err(SpineError::NonLinearSpine(*source_var)) + Elim::FunApp(_, arg_expr) => { + let arg_expr = self.elim_env().force_lazy(arg_expr); + match self.elim_env().force_metas(&arg_expr).as_ref() { + Value::Stuck(Head::LocalVar(source_var), spine) + if spine.is_empty() && self.renaming.set_local(*source_var) => {} + Value::Stuck(Head::LocalVar(source_var), _) => { + return Err(SpineError::NonLinearSpine(*source_var)) + } + _ => return Err(SpineError::NonLocalFunApp), } - _ => return Err(SpineError::NonLocalFunApp), - }, + } Elim::RecordProj(label) => return Err(SpineError::RecordProj(*label)), Elim::ConstMatch(_) => return Err(SpineError::ConstMatch), } @@ -541,7 +562,7 @@ impl<'arena, 'env> Context<'arena, 'env> { meta_var: Level, value: &ArcValue<'arena>, ) -> Result, RenameError> { - let val = self.elim_env().force(value); + let val = self.elim_env().force_metas(value); let span = val.span(); match val.as_ref() { Value::Stuck(head, spine) => { @@ -563,7 +584,7 @@ impl<'arena, 'env> Context<'arena, 'env> { span, *plicity, self.scope.to_scope(head_expr), - self.scope.to_scope(self.rename(meta_var, arg_expr)?), + self.scope.to_scope(self.rename_lazy(meta_var, arg_expr)?), ), Elim::RecordProj(label) => { Term::RecordProj(span, self.scope.to_scope(head_expr), *label) @@ -605,7 +626,7 @@ impl<'arena, 'env> Context<'arena, 'env> { Value::Universe => Ok(Term::Universe(span)), Value::FunType(plicity, param_name, param_type, body_type) => { - let param_type = self.rename(meta_var, param_type)?; + let param_type = self.rename_lazy(meta_var, param_type)?; let body_type = self.rename_closure(meta_var, body_type)?; Ok(Term::FunType( @@ -635,7 +656,7 @@ impl<'arena, 'env> Context<'arena, 'env> { Value::RecordLit(labels, exprs) => { let mut new_exprs = SliceVec::new(self.scope, exprs.len()); for expr in exprs { - new_exprs.push(self.rename(meta_var, expr)?); + new_exprs.push(self.rename_lazy(meta_var, expr)?); } Ok(Term::RecordLit(span, labels, new_exprs.into())) @@ -644,7 +665,7 @@ impl<'arena, 'env> Context<'arena, 'env> { Value::ArrayLit(elem_exprs) => { let mut new_elem_exprs = SliceVec::new(self.scope, elem_exprs.len()); for elem_expr in elem_exprs { - new_elem_exprs.push(self.rename(meta_var, elem_expr)?); + new_elem_exprs.push(self.rename_lazy(meta_var, elem_expr)?); } Ok(Term::ArrayLit(span, new_elem_exprs.into())) @@ -656,7 +677,7 @@ impl<'arena, 'env> Context<'arena, 'env> { Ok(Term::FormatRecord(span, labels, formats)) } Value::FormatCond(label, format, cond) => { - let format = self.rename(meta_var, format)?; + let format = self.rename_lazy(meta_var, format)?; let cond = self.rename_closure(meta_var, cond)?; Ok(Term::FormatCond( span, @@ -675,6 +696,14 @@ impl<'arena, 'env> Context<'arena, 'env> { } } + fn rename_lazy( + &mut self, + meta_var: Level, + value: &LazyValue<'arena>, + ) -> Result, RenameError> { + self.rename(meta_var, &self.elim_env().force_lazy(value)) + } + /// Rename a closure back into a [`Term`]. fn rename_closure( &mut self, @@ -747,8 +776,10 @@ impl PartialRenaming { self.target.clear(); } - fn next_local_var<'arena>(&self) -> ArcValue<'arena> { - Spanned::empty(Arc::new(Value::local_var(self.source.len().next_level()))) + fn next_local_var<'arena>(&self) -> LazyValue<'arena> { + LazyValue::eager(Spanned::empty(Arc::new(Value::local_var( + self.source.len().next_level(), + )))) } /// Set a local source variable to local target variable mapping, ensuring