diff options
author | Nadrieril Feneanar | 2019-08-20 14:10:54 +0200 |
---|---|---|
committer | GitHub | 2019-08-20 14:10:54 +0200 |
commit | 9470664a5e481c63fd96939e7b8986b8fe881dbe (patch) | |
tree | 13bab9e1145a8769b6dd4ca1d76d34af1ff6c12b /dhall/src/core | |
parent | 88ebc0f9d561a2541aad84a3152511a0439db8b4 (diff) | |
parent | caf36246a517b884d7cfcf7c31e1b5d8fce60dfa (diff) |
Merge pull request #104 from Nadrieril/rework-value
Rework Value
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/context.rs | 162 | ||||
-rw-r--r-- | dhall/src/core/mod.rs | 2 | ||||
-rw-r--r-- | dhall/src/core/thunk.rs | 414 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 686 | ||||
-rw-r--r-- | dhall/src/core/valuef.rs | 400 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 206 |
6 files changed, 842 insertions, 1028 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 9230a2e..2bf39c5 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -3,64 +3,56 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; -use crate::core::thunk::Thunk; use crate::core::value::Value; +use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::TypeError; -use crate::phase::{Type, Typed}; #[derive(Debug, Clone)] -enum CtxItem<T> { - Kept(AlphaVar, T), - Replaced(Thunk, T), +enum CtxItem { + Kept(AlphaVar, Value), + Replaced(Value), } #[derive(Debug, Clone)] -struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>); +pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>); -#[derive(Debug, Clone)] -pub(crate) struct NormalizationContext(Context<()>); - -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Context<Type>); - -impl<T> Context<T> { +impl TypecheckContext { pub fn new() -> Self { - Context(Rc::new(Vec::new())) + TypecheckContext(Rc::new(Vec::new())) } - pub fn insert_kept(&self, x: &Label, t: T) -> Self - where - T: Shift + Clone, - { + pub fn insert_type(&self, x: &Label, t: Value) -> Self { let mut vec = self.0.as_ref().clone(); vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); - Context(Rc::new(vec)) + TypecheckContext(Rc::new(vec)) } - pub fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self - where - T: Clone, - { + pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> { let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Replaced(th, t))); - Context(Rc::new(vec)) + vec.push((x.clone(), CtxItem::Replaced(e))); + Ok(TypecheckContext(Rc::new(vec))) } - pub fn lookup(&self, var: &V<Label>) -> Result<CtxItem<T>, V<Label>> - where - T: Clone + Shift, - { + pub fn lookup(&self, var: &V<Label>) -> Option<Value> { let mut var = var.clone(); let mut shift_map: HashMap<Label, _> = HashMap::new(); for (l, i) in self.0.iter().rev() { match var.over_binder(l) { - None => return Ok(i.under_multiple_binders(&shift_map)), + None => { + let i = i.under_multiple_binders(&shift_map); + return Some(match i { + CtxItem::Kept(newvar, t) => { + Value::from_valuef_and_type(ValueF::Var(newvar), t) + } + CtxItem::Replaced(v) => v, + }); + } Some(newvar) => var = newvar, }; if let CtxItem::Kept(_, _) = i { *shift_map.entry(l.clone()).or_insert(0) += 1; } } - // Free variable - Err(var) + // Unbound variable + None } /// Given a var that makes sense in the current context, map the given function in such a way /// that the passed variable always makes sense in the context of the passed item. @@ -69,11 +61,8 @@ impl<T> Context<T> { fn do_with_var<E>( &self, var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem<T>) -> Result<CtxItem<T>, E>, - ) -> Result<Self, E> - where - T: Clone, - { + mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>, + ) -> Result<Self, E> { let mut vec = Vec::new(); vec.reserve(self.0.len()); let mut var = var.clone(); @@ -91,16 +80,13 @@ impl<T> Context<T> { vec.push((l.clone(), (*i).clone())); } vec.reverse(); - Ok(Context(Rc::new(vec))) + Ok(TypecheckContext(Rc::new(vec))) } - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> - where - T: Clone + Shift, - { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { if delta < 0 { Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) } else { - Some(Context(Rc::new( + Some(TypecheckContext(Rc::new( self.0 .iter() .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) @@ -108,117 +94,51 @@ impl<T> Context<T> { ))) } } - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self - where - T: Clone + Subst<Typed>, - { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) .unwrap() } } -impl NormalizationContext { - pub fn new() -> Self { - NormalizationContext(Context::new()) - } - pub fn skip(&self, x: &Label) -> Self { - NormalizationContext(self.0.insert_kept(x, ())) - } - pub fn lookup(&self, var: &V<Label>) -> Value { - match self.0.lookup(var) { - Ok(CtxItem::Replaced(t, ())) => t.to_value(), - Ok(CtxItem::Kept(newvar, ())) => Value::Var(newvar.clone()), - Err(var) => Value::Var(AlphaVar::from_var(var)), - } - } -} - -impl TypecheckContext { - pub fn new() -> Self { - TypecheckContext(Context::new()) - } - pub fn insert_type(&self, x: &Label, t: Type) -> Self { - TypecheckContext(self.0.insert_kept(x, t)) - } - pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> { - Ok(TypecheckContext(self.0.insert_replaced( - x, - e.to_thunk(), - e.get_type()?.into_owned(), - ))) - } - pub fn lookup(&self, var: &V<Label>) -> Option<Typed> { - match self.0.lookup(var) { - Ok(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type( - Thunk::from_value(Value::Var(newvar.clone())), - t.clone(), - )), - Ok(CtxItem::Replaced(th, t)) => { - Some(Typed::from_thunk_and_type(th.clone(), t.clone())) - } - Err(_) => None, - } - } -} - -impl<T: Shift> Shift for CtxItem<T> { +impl Shift for CtxItem { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(match self { CtxItem::Kept(v, t) => { CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) } - CtxItem::Replaced(e, t) => { - CtxItem::Replaced(e.shift(delta, var)?, t.shift(delta, var)?) - } + CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), }) } } -impl<T: Clone + Shift> Shift for Context<T> { +impl Shift for TypecheckContext { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { self.shift(delta, var) } } -impl Shift for NormalizationContext { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(NormalizationContext(self.0.shift(delta, var)?)) - } -} - -impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<Value> for CtxItem { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { - CtxItem::Replaced(e, t) => CtxItem::Replaced( - e.subst_shift(var, val), - t.subst_shift(var, val), - ), + CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), CtxItem::Kept(v, t) => match v.shift(-1, var) { - None => { - CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val)) - } + None => CtxItem::Replaced(val.clone()), Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), }, } } } -impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<Value> for TypecheckContext { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { self.subst_shift(var, val) } } -impl Subst<Typed> for NormalizationContext { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - NormalizationContext(self.0.subst_shift(var, val)) - } -} - +/// Don't count contexts when comparing stuff. +/// This is dirty but needed. impl PartialEq for TypecheckContext { fn eq(&self, _: &Self) -> bool { - // don't count contexts when comparing stuff - // this is dirty but needed for now true } } diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs index 0667df8..08213f7 100644 --- a/dhall/src/core/mod.rs +++ b/dhall/src/core/mod.rs @@ -1,4 +1,4 @@ pub mod context; -pub mod thunk; pub mod value; +pub mod valuef; pub mod var; diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs deleted file mode 100644 index 54a5442..0000000 --- a/dhall/src/core/thunk.rs +++ /dev/null @@ -1,414 +0,0 @@ -use std::borrow::Cow; -use std::cell::{Ref, RefCell}; -use std::rc::Rc; - -use dhall_syntax::{Const, ExprF}; - -use crate::core::context::{NormalizationContext, TypecheckContext}; -use crate::core::value::Value; -use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{ - apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, -}; -use crate::phase::typecheck::type_of_const; -use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; - -#[derive(Debug, Clone, Copy)] -enum Marker { - /// Weak Head Normal Form, i.e. subexpressions may not be normalized - WHNF, - /// Normal form, i.e. completely normalized - NF, -} -use Marker::{NF, WHNF}; - -#[derive(Debug)] -enum ThunkInternal { - /// Non-normalized value alongside a normalization context - Unnormalized(NormalizationContext, InputSubExpr), - /// Partially normalized value whose subexpressions have been thunked (this is returned from - /// typechecking). Note that this is different from `Value::PartialExpr` because there is no - /// requirement of WHNF here. - PartialExpr(ExprF<Thunk, Normalized>), - /// Partially normalized value. - /// Invariant: if the marker is `NF`, the value must be fully normalized - Value(Marker, Value), -} - -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, -/// sharing computation automatically. -/// Uses a RefCell to share computation. -#[derive(Clone)] -pub struct Thunk(Rc<RefCell<ThunkInternal>>); - -/// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve -/// type information through the normalization phase. -#[derive(Debug, Clone)] -pub enum TypedThunk { - // Any value, along with (optionally) its type - Untyped(Thunk), - Typed(Thunk, Box<Type>), - // One of the base higher-kinded types. - // Used to avoid storing the same tower ot Type->Kind->Sort - // over and over again. Also enables having Sort as a value - // even though it doesn't itself have a type. - Const(Const), -} - -impl ThunkInternal { - fn into_thunk(self) -> Thunk { - Thunk(Rc::new(RefCell::new(self))) - } - - fn normalize_whnf(&mut self) { - match self { - ThunkInternal::Unnormalized(ctx, e) => { - *self = ThunkInternal::Value( - WHNF, - normalize_whnf(ctx.clone(), e.clone()), - ) - } - ThunkInternal::PartialExpr(e) => { - *self = - ThunkInternal::Value(WHNF, normalize_one_layer(e.clone())) - } - // Already at least in WHNF - ThunkInternal::Value(_, _) => {} - } - } - - fn normalize_nf(&mut self) { - match self { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) => { - self.normalize_whnf(); - self.normalize_nf(); - } - ThunkInternal::Value(m @ WHNF, v) => { - v.normalize_mut(); - *m = NF; - } - // Already in NF - ThunkInternal::Value(NF, _) => {} - } - } - - // Always use normalize_whnf before - fn as_whnf(&self) -> &Value { - match self { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) => unreachable!(), - ThunkInternal::Value(_, v) => v, - } - } - - // Always use normalize_nf before - fn as_nf(&self) -> &Value { - match self { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) - | ThunkInternal::Value(WHNF, _) => unreachable!(), - ThunkInternal::Value(NF, v) => v, - } - } -} - -impl Thunk { - pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { - ThunkInternal::Unnormalized(ctx, e).into_thunk() - } - - pub(crate) fn from_value(v: Value) -> Thunk { - ThunkInternal::Value(WHNF, v).into_thunk() - } - - pub(crate) fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk { - ThunkInternal::PartialExpr(e).into_thunk() - } - - // Normalizes contents to normal form; faster than `normalize_nf` if - // no one else shares this thunk - pub(crate) fn normalize_mut(&mut self) { - match Rc::get_mut(&mut self.0) { - // Mutate directly if sole owner - Some(refcell) => RefCell::get_mut(refcell).normalize_nf(), - // Otherwise mutate through the refcell - None => self.0.borrow_mut().normalize_nf(), - } - } - - fn do_normalize_whnf(&self) { - let borrow = self.0.borrow(); - match &*borrow { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) => { - drop(borrow); - self.0.borrow_mut().normalize_whnf(); - } - // Already at least in WHNF - ThunkInternal::Value(_, _) => {} - } - } - - fn do_normalize_nf(&self) { - let borrow = self.0.borrow(); - match &*borrow { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) - | ThunkInternal::Value(WHNF, _) => { - drop(borrow); - self.0.borrow_mut().normalize_nf(); - } - // Already in NF - ThunkInternal::Value(NF, _) => {} - } - } - - // WARNING: avoid normalizing any thunk while holding on to this ref - // or you could run into BorrowMut panics - pub(crate) fn normalize_nf(&self) -> Ref<Value> { - self.do_normalize_nf(); - Ref::map(self.0.borrow(), ThunkInternal::as_nf) - } - - // WARNING: avoid normalizing any thunk while holding on to this ref - // or you could run into BorrowMut panics - pub(crate) fn as_value(&self) -> Ref<Value> { - self.do_normalize_whnf(); - Ref::map(self.0.borrow(), ThunkInternal::as_whnf) - } - - pub(crate) fn to_value(&self) -> Value { - self.as_value().clone() - } - - pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) - } - - pub(crate) fn app_val(&self, val: Value) -> Value { - self.app_thunk(val.into_thunk()) - } - - pub(crate) fn app_thunk(&self, th: Thunk) -> Value { - apply_any(self.clone(), th) - } -} - -impl TypedThunk { - pub(crate) fn from_value(v: Value) -> TypedThunk { - TypedThunk::from_thunk(Thunk::from_value(v)) - } - - pub fn from_thunk(th: Thunk) -> TypedThunk { - TypedThunk::from_thunk_untyped(th) - } - - pub(crate) fn from_type(t: Type) -> TypedThunk { - t.into_typethunk() - } - - pub(crate) fn normalize_nf(&self) -> Value { - match self { - TypedThunk::Const(c) => Value::Const(*c), - TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { - thunk.normalize_nf().clone() - } - } - } - - pub(crate) fn to_typed(&self) -> Typed { - self.clone().into_typed() - } - - pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) - } - - pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - TypedThunk::Typed(th, Box::new(t)) - } - pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - TypedThunk::Untyped(th) - } - pub(crate) fn from_const(c: Const) -> Self { - TypedThunk::Const(c) - } - pub(crate) fn from_value_untyped(v: Value) -> Self { - TypedThunk::from_thunk_untyped(Thunk::from_value(v)) - } - - // TODO: Avoid cloning if possible - pub(crate) fn to_value(&self) -> Value { - match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), - TypedThunk::Const(c) => Value::Const(*c), - } - } - pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr_maybe_alpha(true) - } - pub(crate) fn to_thunk(&self) -> Thunk { - match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), - TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)), - } - } - pub(crate) fn to_type(&self) -> Type { - self.clone().into_typed().into_type() - } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_typethunk(self) - } - pub(crate) fn as_const(&self) -> Option<Const> { - // TODO: avoid clone - match &self.to_value() { - Value::Const(c) => Some(*c), - _ => None, - } - } - - pub(crate) fn normalize_mut(&mut self) { - match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { - th.normalize_mut() - } - TypedThunk::Const(_) => {} - } - } - - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { - match self { - TypedThunk::Untyped(_) => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), - TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), - } - } -} - -impl Shift for Thunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(self.0.borrow().shift(delta, var)?.into_thunk()) - } -} - -impl Shift for ThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - ThunkInternal::Unnormalized(ctx, e) => { - ThunkInternal::Unnormalized(ctx.shift(delta, var)?, e.clone()) - } - ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr( - e.traverse_ref_with_special_handling_of_binders( - |v| Ok(v.shift(delta, var)?), - |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - )?, - ), - ThunkInternal::Value(m, v) => { - ThunkInternal::Value(*m, v.shift(delta, var)?) - } - }) - } -} - -impl Shift for TypedThunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - TypedThunk::Untyped(th) => { - TypedThunk::Untyped(th.shift(delta, var)?) - } - TypedThunk::Typed(th, t) => TypedThunk::Typed( - th.shift(delta, var)?, - Box::new(t.shift(delta, var)?), - ), - TypedThunk::Const(c) => TypedThunk::Const(*c), - }) - } -} - -impl Subst<Typed> for Thunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - self.0.borrow().subst_shift(var, val).into_thunk() - } -} - -impl Subst<Typed> for ThunkInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized( - ctx.subst_shift(var, val), - e.clone(), - ), - ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr( - e.map_ref_with_special_handling_of_binders( - |v| v.subst_shift(var, val), - |x, v| { - v.subst_shift( - &var.under_binder(x), - &val.under_binder(x), - ) - }, - ), - ), - ThunkInternal::Value(_, v) => { - // The resulting value may not stay in normal form after substitution - ThunkInternal::Value(WHNF, v.subst_shift(var, val)) - } - } - } -} - -impl Subst<Typed> for TypedThunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - TypedThunk::Untyped(th) => { - TypedThunk::Untyped(th.subst_shift(var, val)) - } - TypedThunk::Typed(th, t) => TypedThunk::Typed( - th.subst_shift(var, val), - Box::new(t.subst_shift(var, val)), - ), - TypedThunk::Const(c) => TypedThunk::Const(*c), - } - } -} - -impl std::cmp::PartialEq for Thunk { - fn eq(&self, other: &Self) -> bool { - *self.as_value() == *other.as_value() - } -} -impl std::cmp::Eq for Thunk {} - -impl std::cmp::PartialEq for TypedThunk { - fn eq(&self, other: &Self) -> bool { - self.to_value() == other.to_value() - } -} -impl std::cmp::Eq for TypedThunk {} - -impl std::fmt::Debug for Thunk { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let b: &ThunkInternal = &self.0.borrow(); - match b { - ThunkInternal::Value(m, v) => { - f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() - } - ThunkInternal::PartialExpr(e) => { - f.debug_tuple("Thunk@PartialExpr").field(e).finish() - } - ThunkInternal::Unnormalized(ctx, e) => f - .debug_tuple("Thunk@Unnormalized") - .field(ctx) - .field(e) - .finish(), - } - } -} diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 61a8eea..0af7c8c 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,490 +1,272 @@ -use std::collections::HashMap; +use std::borrow::Cow; +use std::cell::{Ref, RefCell, RefMut}; +use std::rc::Rc; -use dhall_syntax::{ - rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; +use dhall_syntax::Const; -use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::normalize::{ - apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, -}; -use crate::phase::{Normalized, Typed}; +use crate::core::context::TypecheckContext; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; +use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{NormalizedSubExpr, Typed}; -/// A semantic value. The invariants ensure this value represents a Weak-Head -/// Normal Form (WHNF). This means that this first constructor is the first constructor of the -/// final Normal Form (NF). -/// This WHNF must be preserved by operations on `Value`s. In particular, `subst_shift` could break -/// the invariants so need to be careful to reevaluate as needed. -/// Subexpressions are Thunks, which are partially evaluated expressions that are normalized -/// on-demand. When all the Thunks in a Value are at least in WHNF, and recursively so, then the -/// Value is in NF. This is because WHNF ensures that we have the first constructor of the NF; so -/// if we have the first constructor of the NF at all levels, we actually have the NF. -/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence -/// (normalization). Equality will normalize only as needed. -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum Value { - /// Closures - Lam(AlphaLabel, TypedThunk, Thunk), - Pi(AlphaLabel, TypedThunk, TypedThunk), - // Invariant: the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec<Thunk>), +#[derive(Debug, Clone, Copy)] +enum Form { + /// No constraints; expression may not be normalized at all. + Unevaled, + /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may + /// not be normalized. This means that the first constructor of the contained ValueF is the first + /// constructor of the final Normal Form (NF). + WHNF, + /// Normal Form, i.e. completely normalized. + /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the + /// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so + /// if we have the first constructor of the NF at all levels, we actually have the NF. + NF, +} +use Form::{Unevaled, NF, WHNF}; - Var(AlphaVar), - Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), - EmptyOptionalLit(TypedThunk), - NEOptionalLit(Thunk), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypedThunk), - NEListLit(Vec<Thunk>), - RecordLit(HashMap<Label, Thunk>), - RecordType(HashMap<Label, TypedThunk>), - UnionType(HashMap<Label, Option<TypedThunk>>), - UnionConstructor(Label, HashMap<Label, Option<TypedThunk>>), - UnionLit(Label, Thunk, HashMap<Label, Option<TypedThunk>>), - // Invariant: this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec<InterpolatedTextContents<Thunk>>), - Equivalence(TypedThunk, TypedThunk), - // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF<Thunk, Normalized>), +#[derive(Debug)] +/// Partially normalized value. +/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form +/// Invariant: if `form` is `NF`, `value` must be fully normalized +struct ValueInternal { + form: Form, + value: ValueF, + ty: Option<Value>, } -impl Value { - pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_value(self) +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, +/// sharing computation automatically. Uses a RefCell to share computation. +/// Can optionally store a type from typechecking to preserve type information. +#[derive(Clone)] +pub struct Value(Rc<RefCell<ValueInternal>>); + +impl ValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_valuef(&self) -> &ValueF { + &self.value } - /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { - self.normalize_to_expr_maybe_alpha(false) - } - /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize - /// if alpha is `true` - pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - match self { - Value::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), - )), - Value::AppliedBuiltin(b, args) => { - let mut e = rc(ExprF::Builtin(*b)); - for v in args { - e = rc(ExprF::App( - e, - v.normalize_to_expr_maybe_alpha(alpha), - )); - } - e - } - Value::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), - )), - Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))), - Value::Const(c) => rc(ExprF::Const(*c)), - Value::BoolLit(b) => rc(ExprF::BoolLit(*b)), - Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - Value::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - Value::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), - n.normalize_to_expr_maybe_alpha(alpha), - )), - Value::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) - } - Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.normalize_to_expr_maybe_alpha(alpha), - )))), - Value::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter() - .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) - .collect(), - )), - Value::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) - .collect(), - )), - Value::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) - .collect(), - )), - Value::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(), - )), - Value::UnionConstructor(l, kts) => { - let kts = kts - .iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(); - rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) + fn normalize_whnf(&mut self) { + take_mut::take(self, |vint| match &vint.form { + Unevaled => ValueInternal { + form: WHNF, + value: normalize_whnf(vint.value), + ty: vint.ty, + }, + // Already in WHNF + WHNF | NF => vint, + }) + } + fn normalize_nf(&mut self) { + match self.form { + Unevaled => { + self.normalize_whnf(); + self.normalize_nf(); } - Value::UnionLit(l, v, kts) => rc(ExprF::App( - Value::UnionConstructor(l.clone(), kts.clone()) - .normalize_to_expr_maybe_alpha(alpha), - v.normalize_to_expr_maybe_alpha(alpha), - )), - Value::TextLit(elts) => { - use InterpolatedTextContents::{Expr, Text}; - rc(ExprF::TextLit( - elts.iter() - .map(|contents| match contents { - Expr(e) => { - Expr(e.normalize_to_expr_maybe_alpha(alpha)) - } - Text(s) => Text(s.clone()), - }) - .collect(), - )) + WHNF => { + self.value.normalize_mut(); + self.form = NF; } - Value::Equivalence(x, y) => rc(ExprF::BinOp( - dhall_syntax::BinOp::Equivalence, - x.normalize_to_expr_maybe_alpha(alpha), - y.normalize_to_expr_maybe_alpha(alpha), + // Already in NF + NF => {} + } + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, )), - Value::PartialExpr(e) => { - rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) - } } } +} - pub(crate) fn normalize_mut(&mut self) { - match self { - Value::Var(_) - | Value::Const(_) - | Value::BoolLit(_) - | Value::NaturalLit(_) - | Value::IntegerLit(_) - | Value::DoubleLit(_) => {} +impl Value { + pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { + ValueInternal { + form: Unevaled, + value: v, + ty: None, + } + .into_value() + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { + ValueInternal { + form: Unevaled, + value: v, + ty: Some(t), + } + .into_value() + } + pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { + Value::from_valuef_and_type(v, Value::from_const(Const::Type)) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => Value::from_valuef_untyped(ValueF::Const(c)), + } + } + pub fn const_type() -> Self { + Value::from_const(Const::Type) + } - Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => { - tth.normalize_mut(); - } + pub(crate) fn as_const(&self) -> Option<Const> { + match &*self.as_whnf() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } - Value::NEOptionalLit(th) => { - th.normalize_mut(); - } - Value::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - Value::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - Value::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - Value::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - Value::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - Value::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - Value::UnionType(kts) | Value::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - Value::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - Value::TextLit(elts) => { - for x in elts.iter_mut() { - use InterpolatedTextContents::{Expr, Text}; - match x { - Expr(n) => n.normalize_mut(), - Text(_) => {} - } - } - } - Value::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); + fn as_internal(&self) -> Ref<ValueInternal> { + self.0.borrow() + } + fn as_internal_mut(&self) -> RefMut<ValueInternal> { + self.0.borrow_mut() + } + /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an + /// unevaled PartialExpr. You probably want to use `as_whnf`. + fn as_valuef(&self) -> Ref<ValueF> { + Ref::map(self.as_internal(), ValueInternal::as_valuef) + } + /// This is what you want if you want to pattern-match on the value. + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_whnf(&self) -> Ref<ValueF> { + self.normalize_whnf(); + self.as_valuef() + } + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_nf(&self) -> Ref<ValueF> { + self.normalize_nf(); + self.as_valuef() + } + + // TODO: rename `normalize_to_expr` + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.as_whnf().normalize_to_expr() + } + // TODO: rename `normalize_to_expr_maybe_alpha` + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.as_whnf().normalize_to_expr_maybe_alpha(true) + } + /// TODO: cloning a valuef can often be avoided + pub(crate) fn to_whnf(&self) -> ValueF { + self.as_whnf().clone() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_value(self) + } + + /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. + fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { + match Rc::get_mut(&mut self.0) { + // Mutate directly if sole owner + Some(refcell) => f(RefCell::get_mut(refcell)), + // Otherwise mutate through the refcell + None => f(&mut self.as_internal_mut()), + } + } + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this. + pub(crate) fn normalize_mut(&mut self) { + self.mutate_internal(|vint| vint.normalize_nf()) + } + + pub(crate) fn normalize_whnf(&self) { + let borrow = self.as_internal(); + match borrow.form { + Unevaled => { + drop(borrow); + self.as_internal_mut().normalize_whnf(); } - Value::PartialExpr(e) => { - // TODO: need map_mut - e.map_ref(|v| { - v.normalize_nf(); - }); + // Already at least in WHNF + WHNF | NF => {} + } + } + pub(crate) fn normalize_nf(&self) { + let borrow = self.as_internal(); + match borrow.form { + Unevaled | WHNF => { + drop(borrow); + self.as_internal_mut().normalize_nf(); } + // Already in NF + NF => {} } } - /// Apply to a value - pub(crate) fn app(self, val: Value) -> Value { - self.app_val(val) + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - /// Apply to a value - pub(crate) fn app_val(self, val: Value) -> Value { - self.app_thunk(val.into_thunk()) + pub(crate) fn app_value(&self, th: Value) -> ValueF { + apply_any(self.clone(), th) } - /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> Value { - Thunk::from_value(self).app_thunk(th) + pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> { + Ok(Cow::Owned(self.as_internal().get_type()?.clone())) } +} - pub fn from_builtin(b: Builtin) -> Value { - Value::AppliedBuiltin(b, vec![]) +impl Shift for Value { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(Value(self.0.shift(delta, var)?)) } } -impl Shift for Value { +impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - Value::Lam(x, t, e) => Value::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( - *b, - args.iter() - .map(|v| Ok(v.shift(delta, var)?)) - .collect::<Result<_, _>>()?, - ), - Value::Pi(x, t, e) => Value::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - Value::Var(v) => Value::Var(v.shift(delta, var)?), - Value::Const(c) => Value::Const(*c), - Value::BoolLit(b) => Value::BoolLit(*b), - Value::NaturalLit(n) => Value::NaturalLit(*n), - Value::IntegerLit(n) => Value::IntegerLit(*n), - Value::DoubleLit(n) => Value::DoubleLit(*n), - Value::EmptyOptionalLit(tth) => { - Value::EmptyOptionalLit(tth.shift(delta, var)?) - } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.shift(delta, var)?) - } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.shift(delta, var)?) - } - Value::NEListLit(elts) => Value::NEListLit( - elts.iter() - .map(|v| Ok(v.shift(delta, var)?)) - .collect::<Result<_, _>>()?, - ), - Value::RecordLit(kvs) => Value::RecordLit( - kvs.iter() - .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) - .collect::<Result<_, _>>()?, - ), - Value::RecordType(kvs) => Value::RecordType( - kvs.iter() - .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) - .collect::<Result<_, _>>()?, - ), - Value::UnionType(kts) => Value::UnionType( - kts.iter() - .map(|(k, v)| { - Ok(( - k.clone(), - v.as_ref() - .map(|v| Ok(v.shift(delta, var)?)) - .transpose()?, - )) - }) - .collect::<Result<_, _>>()?, - ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( - x.clone(), - kts.iter() - .map(|(k, v)| { - Ok(( - k.clone(), - v.as_ref() - .map(|v| Ok(v.shift(delta, var)?)) - .transpose()?, - )) - }) - .collect::<Result<_, _>>()?, - ), - Value::UnionLit(x, v, kts) => Value::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.iter() - .map(|(k, v)| { - Ok(( - k.clone(), - v.as_ref() - .map(|v| Ok(v.shift(delta, var)?)) - .transpose()?, - )) - }) - .collect::<Result<_, _>>()?, - ), - Value::TextLit(elts) => Value::TextLit( - elts.iter() - .map(|contents| { - use InterpolatedTextContents::{Expr, Text}; - Ok(match contents { - Expr(th) => Expr(th.shift(delta, var)?), - Text(s) => Text(s.clone()), - }) - }) - .collect::<Result<_, _>>()?, - ), - Value::Equivalence(x, y) => { - Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) - } - Value::PartialExpr(e) => Value::PartialExpr( - e.traverse_ref_with_special_handling_of_binders( - |v| Ok(v.shift(delta, var)?), - |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - )?, - ), + Some(ValueInternal { + form: self.form, + value: self.value.shift(delta, var)?, + ty: self.ty.shift(delta, var)?, }) } } -impl Subst<Typed> for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - // Retry normalizing since substituting may allow progress - Value::AppliedBuiltin(b, args) => apply_builtin( - *b, - args.iter().map(|v| v.subst_shift(var, val)).collect(), - ), - // Retry normalizing since substituting may allow progress - Value::PartialExpr(e) => { - normalize_one_layer(e.map_ref_with_special_handling_of_binders( - |v| v.subst_shift(var, val), - |x, v| { - v.subst_shift( - &var.under_binder(x), - &val.under_binder(x), - ) - }, - )) - } - // Retry normalizing since substituting may allow progress - Value::TextLit(elts) => { - Value::TextLit(squash_textlit(elts.iter().map(|contents| { - use InterpolatedTextContents::{Expr, Text}; - match contents { - Expr(th) => Expr(th.subst_shift(var, val)), - Text(s) => Text(s.clone()), - } - }))) - } - Value::Lam(x, t, e) => Value::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - Value::Pi(x, t, e) => Value::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - Value::Var(v) if v == var => val.to_value(), - Value::Var(v) => Value::Var(v.shift(-1, var).unwrap()), - Value::Const(c) => Value::Const(*c), - Value::BoolLit(b) => Value::BoolLit(*b), - Value::NaturalLit(n) => Value::NaturalLit(*n), - Value::IntegerLit(n) => Value::IntegerLit(*n), - Value::DoubleLit(n) => Value::DoubleLit(*n), - Value::EmptyOptionalLit(tth) => { - Value::EmptyOptionalLit(tth.subst_shift(var, val)) - } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.subst_shift(var, val)) - } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.subst_shift(var, val)) - } - Value::NEListLit(elts) => Value::NEListLit( - elts.iter().map(|v| v.subst_shift(var, val)).collect(), - ), - Value::RecordLit(kvs) => Value::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) - .collect(), - ), - Value::RecordType(kvs) => Value::RecordType( - kvs.iter() - .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) - .collect(), - ), - Value::UnionType(kts) => Value::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) - }) - .collect(), - ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( - x.clone(), - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) - }) - .collect(), - ), - Value::UnionLit(x, v, kts) => Value::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) - }) - .collect(), - ), - Value::Equivalence(x, y) => Value::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), +impl Subst<Value> for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + Value(self.0.subst_shift(var, val)) + } +} + +impl Subst<Value> for ValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + ValueInternal { + // The resulting value may not stay in wnhf after substitution + form: Unevaled, + value: self.value.subst_shift(var, val), + ty: self.ty.subst_shift(var, val), } } } + +// TODO: use Rc comparison to shortcut on identical pointers +impl std::cmp::PartialEq for Value { + fn eq(&self, other: &Self) -> bool { + *self.as_whnf() == *other.as_whnf() + } +} +impl std::cmp::Eq for Value {} + +impl std::fmt::Debug for Value { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let vint: &ValueInternal = &self.as_internal(); + fmt.debug_tuple(&format!("Value@{:?}", &vint.form)) + .field(&vint.value) + .finish() + } +} diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs new file mode 100644 index 0000000..0c3058d --- /dev/null +++ b/dhall/src/core/valuef.rs @@ -0,0 +1,400 @@ +use std::collections::HashMap; + +use dhall_syntax::{ + rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, +}; + +use crate::core::value::Value; +use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::phase::normalize::OutputSubExpr; +use crate::phase::Normalized; + +/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are +/// normalized on-demand. +/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to +/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will +/// recursively normalize as needed. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ValueF { + /// Closures + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), + // Invariant: the evaluation must not be able to progress further. + AppliedBuiltin(Builtin, Vec<Value>), + + Var(AlphaVar), + Const(Const), + BoolLit(bool), + NaturalLit(Natural), + IntegerLit(Integer), + DoubleLit(NaiveDouble), + EmptyOptionalLit(Value), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Value), + NEListLit(Vec<Value>), + RecordLit(HashMap<Label, Value>), + RecordType(HashMap<Label, Value>), + UnionType(HashMap<Label, Option<Value>>), + UnionConstructor(Label, HashMap<Label, Option<Value>>), + UnionLit(Label, Value, HashMap<Label, Option<Value>>), + // Invariant: this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec<InterpolatedTextContents<Value>>), + Equivalence(Value, Value), + // Invariant: this must not contain a value captured by one of the variants above. + PartialExpr(ExprF<Value, Normalized>), +} + +impl ValueF { + pub(crate) fn into_value_untyped(self) -> Value { + Value::from_valuef_untyped(self) + } + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_valuef_and_type(self, t) + } + pub(crate) fn into_value_simple_type(self) -> Value { + Value::from_valuef_simple_type(self) + } + + /// Convert the value to a fully normalized syntactic expression + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + self.normalize_to_expr_maybe_alpha(false) + } + /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize + /// if alpha is `true` + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + match self { + ValueF::Lam(x, t, e) => rc(ExprF::Lam( + x.to_label_maybe_alpha(alpha), + t.normalize_to_expr_maybe_alpha(alpha), + e.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::AppliedBuiltin(b, args) => { + let mut e = rc(ExprF::Builtin(*b)); + for v in args { + e = rc(ExprF::App( + e, + v.normalize_to_expr_maybe_alpha(alpha), + )); + } + e + } + ValueF::Pi(x, t, e) => rc(ExprF::Pi( + x.to_label_maybe_alpha(alpha), + t.normalize_to_expr_maybe_alpha(alpha), + e.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))), + ValueF::Const(c) => rc(ExprF::Const(*c)), + ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueF::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::NEOptionalLit(n) => { + rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) + } + ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + n.normalize_to_expr_maybe_alpha(alpha), + )))), + ValueF::NEListLit(elts) => rc(ExprF::NEListLit( + elts.iter() + .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) + .collect(), + )), + ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| { + (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) + }) + .collect(), + )), + ValueF::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) + }) + .collect(), + )), + ValueF::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref().map(|v| { + v.normalize_to_expr_maybe_alpha(alpha) + }), + ) + }) + .collect(), + )), + ValueF::UnionConstructor(l, kts) => { + let kts = kts + .iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref().map(|v| { + v.normalize_to_expr_maybe_alpha(alpha) + }), + ) + }) + .collect(); + rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) + } + ValueF::UnionLit(l, v, kts) => rc(ExprF::App( + ValueF::UnionConstructor(l.clone(), kts.clone()) + .normalize_to_expr_maybe_alpha(alpha), + v.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::TextLit(elts) => { + use InterpolatedTextContents::{Expr, Text}; + rc(ExprF::TextLit( + elts.iter() + .map(|contents| match contents { + Expr(e) => { + Expr(e.normalize_to_expr_maybe_alpha(alpha)) + } + Text(s) => Text(s.clone()), + }) + .collect(), + )) + } + ValueF::Equivalence(x, y) => rc(ExprF::BinOp( + dhall_syntax::BinOp::Equivalence, + x.normalize_to_expr_maybe_alpha(alpha), + y.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::PartialExpr(e) => { + rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) + } + } + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueF::Var(_) + | ValueF::Const(_) + | ValueF::BoolLit(_) + | ValueF::NaturalLit(_) + | ValueF::IntegerLit(_) + | ValueF::DoubleLit(_) => {} + + ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueF::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueF::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueF::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueF::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueF::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueF::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueF::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueF::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueF::TextLit(elts) => { + for x in elts.iter_mut() { + use InterpolatedTextContents::{Expr, Text}; + match x { + Expr(n) => n.normalize_mut(), + Text(_) => {} + } + } + } + ValueF::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueF::PartialExpr(e) => { + // TODO: need map_mut + e.map_ref(|v| { + v.normalize_nf(); + }); + } + } + } + + /// Apply to a valuef + pub(crate) fn app(self, val: ValueF) -> ValueF { + self.app_valuef(val) + } + + /// Apply to a valuef + pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { + self.app_value(val.into_value_untyped()) + } + + /// Apply to a value + pub fn app_value(self, th: Value) -> ValueF { + Value::from_valuef_untyped(self).app_value(th) + } + + pub fn from_builtin(b: Builtin) -> ValueF { + ValueF::AppliedBuiltin(b, vec![]) + } +} + +impl Shift for ValueF { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(match self { + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.shift(delta, var)?) + } + ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.shift(delta, var)?) + } + ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + } + ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), + }) + } +} + +impl Subst<Value> for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) + } + ValueF::PartialExpr(e) => { + ValueF::PartialExpr(e.subst_shift(var, val)) + } + ValueF::TextLit(elts) => { + ValueF::TextLit(elts.subst_shift(var, val)) + } + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueF::Var(v) if v == var => val.to_whnf(), + ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.subst_shift(var, val)) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.subst_shift(var, val)) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.subst_shift(var, val)) + } + ValueF::RecordLit(kvs) => { + ValueF::RecordLit(kvs.subst_shift(var, val)) + } + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.subst_shift(var, val)) + } + ValueF::UnionType(kts) => { + ValueF::UnionType(kts.subst_shift(var, val)) + } + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueF::Equivalence(x, y) => ValueF::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs index 4ef1b93..ce4d137 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -2,17 +2,17 @@ use std::collections::HashMap; use dhall_syntax::{Label, V}; -/// Stores a pair of variables: a normal one and if relevant one +/// Stores a pair of variables: a normal one and one /// that corresponds to the alpha-normalized version of the first one. -/// Equality is up to alpha-equivalence. +/// Equality is up to alpha-equivalence (compares on the second one only). #[derive(Clone, Eq)] pub struct AlphaVar { normal: V<Label>, - alpha: Option<V<()>>, + alpha: V<()>, } // Exactly like a Label, but equality returns always true. -// This is so that Value equality is exactly alpha-equivalence. +// This is so that ValueF equality is exactly alpha-equivalence. #[derive(Clone, Eq)] pub struct AlphaLabel(Label); @@ -50,27 +50,22 @@ pub(crate) trait Shift: Sized { } } -pub(crate) trait Subst<T> { - fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self; +pub(crate) trait Subst<S> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self; } impl AlphaVar { pub(crate) fn to_var(&self, alpha: bool) -> V<Label> { - match (alpha, &self.alpha) { - (true, Some(x)) => V("_".into(), x.1), - _ => self.normal.clone(), - } - } - pub(crate) fn from_var(normal: V<Label>) -> Self { - AlphaVar { - normal, - alpha: None, + if alpha { + V("_".into(), self.alpha.1) + } else { + self.normal.clone() } } pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self { AlphaVar { normal, - alpha: Some(V((), alpha)), + alpha: V((), alpha), } } } @@ -92,31 +87,15 @@ impl Shift for AlphaVar { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(AlphaVar { normal: self.normal.shift(delta, &var.normal)?, - alpha: match (&self.alpha, &var.alpha) { - (Some(x), Some(v)) => Some(x.shift(delta, v)?), - _ => None, - }, + alpha: self.alpha.shift(delta, &var.alpha)?, }) } } -impl Shift for () { - fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> { - Some(()) - } -} - -impl<T> Subst<T> for () { - fn subst_shift(&self, _var: &AlphaVar, _val: &T) -> Self {} -} - +/// Equality up to alpha-equivalence impl std::cmp::PartialEq for AlphaVar { fn eq(&self, other: &Self) -> bool { - match (&self.alpha, &other.alpha) { - (Some(x), Some(y)) => x == y, - (None, None) => self.normal == other.normal, - _ => false, - } + self.alpha == other.alpha } } impl std::cmp::PartialEq for AlphaLabel { @@ -127,10 +106,7 @@ impl std::cmp::PartialEq for AlphaLabel { impl std::fmt::Debug for AlphaVar { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - match &self.alpha { - Some(a) => write!(f, "AlphaVar({}, {})", self.normal, a.1), - None => write!(f, "AlphaVar({}, free)", self.normal), - } + write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1) } } @@ -144,7 +120,7 @@ impl From<Label> for AlphaVar { fn from(x: Label) -> AlphaVar { AlphaVar { normal: V(x, 0), - alpha: Some(V((), 0)), + alpha: V((), 0), } } } @@ -175,3 +151,153 @@ impl From<AlphaLabel> for Label { x.0 } } +impl Shift for () { + fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> { + Some(()) + } +} + +impl<A: Shift, B: Shift> Shift for (A, B) { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some((self.0.shift(delta, var)?, self.1.shift(delta, var)?)) + } +} + +impl<T: Shift> Shift for Option<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(match self { + None => None, + Some(x) => Some(x.shift(delta, var)?), + }) + } +} + +impl<T: Shift> Shift for Box<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(Box::new(self.as_ref().shift(delta, var)?)) + } +} + +impl<T: Shift> Shift for std::rc::Rc<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?)) + } +} + +impl<T: Shift> Shift for std::cell::RefCell<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?)) + } +} + +impl<T: Shift, E: Clone> Shift for dhall_syntax::ExprF<T, E> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(self.traverse_ref_with_special_handling_of_binders( + |v| Ok(v.shift(delta, var)?), + |x, v| Ok(v.shift(delta, &var.under_binder(x))?), + )?) + } +} + +impl<T: Shift> Shift for Vec<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some( + self.iter() + .map(|v| Ok(v.shift(delta, var)?)) + .collect::<Result<_, _>>()?, + ) + } +} + +impl<K, T: Shift> Shift for HashMap<K, T> +where + K: Clone + std::hash::Hash + Eq, +{ + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some( + self.iter() + .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) + .collect::<Result<_, _>>()?, + ) + } +} + +impl<T: Shift> Shift for dhall_syntax::InterpolatedTextContents<T> { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + use dhall_syntax::InterpolatedTextContents::{Expr, Text}; + Some(match self { + Expr(x) => Expr(x.shift(delta, var)?), + Text(s) => Text(s.clone()), + }) + } +} + +impl<S> Subst<S> for () { + fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {} +} + +impl<S, A: Subst<S>, B: Subst<S>> Subst<S> for (A, B) { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + (self.0.subst_shift(var, val), self.1.subst_shift(var, val)) + } +} + +impl<S, T: Subst<S>> Subst<S> for Option<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.as_ref().map(|x| x.subst_shift(var, val)) + } +} + +impl<S, T: Subst<S>> Subst<S> for Box<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + Box::new(self.as_ref().subst_shift(var, val)) + } +} + +impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + std::rc::Rc::new(self.as_ref().subst_shift(var, val)) + } +} + +impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + std::cell::RefCell::new(self.borrow().subst_shift(var, val)) + } +} + +impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for dhall_syntax::ExprF<T, E> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.map_ref_with_special_handling_of_binders( + |v| v.subst_shift(var, val), + |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ) + } +} + +impl<S, T: Subst<S>> Subst<S> for Vec<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.iter().map(|v| v.subst_shift(var, val)).collect() + } +} + +impl<S, T: Subst<S>> Subst<S> for dhall_syntax::InterpolatedTextContents<T> { + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + use dhall_syntax::InterpolatedTextContents::{Expr, Text}; + match self { + Expr(x) => Expr(x.subst_shift(var, val)), + Text(s) => Text(s.clone()), + } + } +} + +impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T> +where + K: Clone + std::hash::Hash + Eq, +{ + fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { + self.iter() + .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) + .collect() + } +} |