diff options
Diffstat (limited to 'dhall/src')
| -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 | ||||
| -rw-r--r-- | dhall/src/error/mod.rs | 54 | ||||
| -rw-r--r-- | dhall/src/phase/mod.rs | 75 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 588 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 796 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 28 |
11 files changed, 1473 insertions, 1938 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() + } +} diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 8f6ff51..13a9d7e 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -3,8 +3,9 @@ use std::io::Error as IOError; use dhall_syntax::{BinOp, Import, Label, ParseError, V}; use crate::core::context::TypecheckContext; +use crate::core::value::Value; use crate::phase::resolve::ImportStack; -use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; +use crate::phase::NormalizedSubExpr; pub type Result<T> = std::result::Result<T, Error>; @@ -48,28 +49,27 @@ pub struct TypeError { #[derive(Debug)] pub(crate) enum TypeMessage { UnboundVariable(V<Label>), - InvalidInputType(Normalized), - InvalidOutputType(Normalized), - NotAFunction(Typed), - TypeMismatch(Typed, Normalized, Typed), - AnnotMismatch(Typed, Normalized), + InvalidInputType(Value), + InvalidOutputType(Value), + NotAFunction(Value), + TypeMismatch(Value, Value, Value), + AnnotMismatch(Value, Value), Untyped, - FieldCollision(Label), - InvalidListElement(usize, Normalized, Typed), - InvalidListType(Normalized), - InvalidOptionalType(Normalized), - InvalidPredicate(Typed), - IfBranchMismatch(Typed, Typed), - IfBranchMustBeTerm(bool, Typed), - InvalidFieldType(Label, Type), - NotARecord(Label, Normalized), - MustCombineRecord(Typed), - MissingRecordField(Label, Typed), - MissingUnionField(Label, Normalized), - BinOpTypeMismatch(BinOp, Typed), - InvalidTextInterpolation(Typed), - Merge1ArgMustBeRecord(Typed), - Merge2ArgMustBeUnion(Typed), + InvalidListElement(usize, Value, Value), + InvalidListType(Value), + InvalidOptionalType(Value), + InvalidPredicate(Value), + IfBranchMismatch(Value, Value), + IfBranchMustBeTerm(bool, Value), + InvalidFieldType(Label, Value), + NotARecord(Label, Value), + MustCombineRecord(Value), + MissingRecordField(Label, Value), + MissingUnionField(Label, Value), + BinOpTypeMismatch(BinOp, Value), + InvalidTextInterpolation(Value), + Merge1ArgMustBeRecord(Value), + Merge2ArgMustBeUnion(Value), MergeEmptyNeedsAnnotation, MergeHandlerMissingVariant(Label), MergeVariantMissingHandler(Label), @@ -79,14 +79,12 @@ pub(crate) enum TypeMessage { ProjectionMustBeRecord, ProjectionMissingEntry, Sort, - RecordMismatch(Typed, Typed), RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(Type), - RecordTypeMismatch(Type, Type, Type, Type), + RecordTypeMergeRequiresRecordType(Value), UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, Typed), - EquivalenceTypeMismatch(Typed, Typed), - AssertMismatch(Typed, Typed), + EquivalenceArgumentMustBeTerm(bool, Value), + EquivalenceTypeMismatch(Value, Value), + AssertMismatch(Value, Value), AssertMustTakeEquivalence, } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 778f990..1f7e5f0 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -4,8 +4,8 @@ use std::path::Path; use dhall_syntax::{Const, SubExpr}; -use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; +use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{EncodeError, Error, ImportError, TypeError}; @@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(TypedThunk); +pub struct Typed(Value); /// A normalized expression. /// @@ -41,8 +41,6 @@ pub struct Typed(TypedThunk); #[derive(Debug, Clone)] pub struct Normalized(Typed); -pub type Type = Typed; - impl Parsed { pub fn parse_file(f: &Path) -> Result<Parsed, Error> { parse::parse_file(f) @@ -71,15 +69,10 @@ impl Parsed { impl Resolved { pub fn typecheck(self) -> Result<Typed, TypeError> { - typecheck::typecheck(self) - } - pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> { - typecheck::typecheck_with(self, ty) + Ok(typecheck::typecheck(self.0)?.into_typed()) } - /// Pretends this expression has been typechecked. Use with care. - #[allow(dead_code)] - pub(crate) fn skip_typecheck(self) -> Typed { - typecheck::skip_typecheck(self) + pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> { + Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) } } @@ -97,58 +90,39 @@ impl Typed { Normalized(self) } - pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - Typed(TypedThunk::from_thunk_and_type(th, t)) - } - pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - Typed(TypedThunk::from_thunk_untyped(th)) - } pub(crate) fn from_const(c: Const) -> Self { - Typed(TypedThunk::from_const(c)) + Typed(Value::from_const(c)) } - pub fn from_value_untyped(v: Value) -> Self { - Typed(TypedThunk::from_value_untyped(v)) + pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { + Typed(Value::from_valuef_and_type(v, t.into_value())) } - pub(crate) fn from_typethunk(th: TypedThunk) -> Self { + pub(crate) fn from_value(th: Value) -> Self { Typed(th) } - - pub(crate) fn to_value(&self) -> Value { - self.0.to_value() + pub fn const_type() -> Self { + Typed::from_const(Const::Type) } + pub fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() } pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.0.to_expr_alpha() } - pub fn to_thunk(&self) -> Thunk { - self.0.to_thunk() - } - // Deprecated - pub fn to_type(&self) -> Type { - self.clone() + pub fn to_value(&self) -> Value { + self.0.clone() } - // Deprecated - pub(crate) fn into_type(self) -> Type { - self - } - pub(crate) fn into_typethunk(self) -> TypedThunk { + pub(crate) fn into_value(self) -> Value { self.0 } - pub(crate) fn to_normalized(&self) -> Normalized { - self.clone().normalize() - } - pub(crate) fn as_const(&self) -> Option<Const> { - self.0.as_const() - } pub(crate) fn normalize_mut(&mut self) { self.0.normalize_mut() } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { - self.0.get_type() + #[allow(dead_code)] + pub(crate) fn get_type(&self) -> Result<Cow<'_, Typed>, TypeError> { + Ok(Cow::Owned(self.0.get_type()?.into_owned().into_typed())) } } @@ -164,13 +138,6 @@ impl Normalized { pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.0.to_expr_alpha() } - #[allow(dead_code)] - pub(crate) fn to_type(&self) -> Type { - self.0.to_type() - } - pub(crate) fn to_value(&self) -> Value { - self.0.to_value() - } pub(crate) fn into_typed(self) -> Typed { self.0 } @@ -188,8 +155,8 @@ impl Shift for Normalized { } } -impl Subst<Typed> for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst<Value> for Typed { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { Typed(self.0.subst_shift(var, val)) } } @@ -234,7 +201,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.to_value() == other.to_value() + self.0 == other.0 } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index fd0197d..a379a4b 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,13 +5,11 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::context::NormalizationContext; -use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; +use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; -use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr}; -pub(crate) type InputSubExpr = ResolvedSubExpr; pub(crate) type OutputSubExpr = NormalizedSubExpr; // Ad-hoc macro to help construct closures @@ -22,67 +20,76 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - Value::Var(var).into_thunk() + ValueF::Var(var).into_value_untyped() }}; + // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - Value::Lam( + ValueF::Lam( Label::from(stringify!($var)).into(), - TypedThunk::from_thunk_untyped(make_closure!($($ty)*)), + make_closure!($($ty)*), make_closure!($($rest)*), - ).into_thunk() + ).into_value_untyped() + }; + (Natural) => { + ValueF::from_builtin(Builtin::Natural) + .into_value_simple_type() }; - (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() }; (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) - .app_thunk(make_closure!($($rest)*)) - .into_thunk() + ValueF::from_builtin(Builtin::List) + .app_value(make_closure!($($rest)*)) + .into_value_simple_type() }; - (Some $($rest:tt)*) => { - Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk() + (Some($($rest:tt)*)) => { + ValueF::NEOptionalLit(make_closure!($($rest)*)) + .into_value_untyped() }; (1 + $($rest:tt)*) => { - Value::PartialExpr(ExprF::BinOp( + ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Thunk::from_value(Value::NaturalLit(1)), - )).into_thunk() + Value::from_valuef_and_type( + ValueF::NaturalLit(1), + make_closure!(Natural) + ), + )).into_value_with_type( + make_closure!(Natural) + ) }; ([ $($head:tt)* ] # $($tail:tt)*) => { - Value::PartialExpr(ExprF::BinOp( + ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::ListAppend, - Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(), + ValueF::NEListLit(vec![make_closure!($($head)*)]) + .into_value_untyped(), make_closure!($($tail)*), - )).into_thunk() + )).into_value_untyped() }; } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { +pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { use dhall_syntax::Builtin::*; - use Value::*; + use ValueF::*; // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced. let ret = match (b, args.as_slice()) { - (OptionalNone, [t, r..]) => { - Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone())))) - } - (NaturalIsZero, [n, r..]) => match &*n.as_value() { + (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))), + (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), }, - (NaturalEven, [n, r..]) => match &*n.as_value() { + (NaturalEven, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), _ => Err(()), }, - (NaturalOdd, [n, r..]) => match &*n.as_value() { + (NaturalOdd, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), _ => Err(()), }, - (NaturalToInteger, [n, r..]) => match &*n.as_value() { + (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), _ => Err(()), }, - (NaturalShow, [n, r..]) => match &*n.as_value() { + (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), @@ -90,7 +97,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { - match (&*a.as_value(), &*b.as_value()) { + match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => { Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) } @@ -100,7 +107,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Err(()), } } - (IntegerShow, [n, r..]) => match &*n.as_value() { + (IntegerShow, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() @@ -111,18 +118,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { } _ => Err(()), }, - (IntegerToDouble, [n, r..]) => match &*n.as_value() { + (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), _ => Err(()), }, - (DoubleShow, [n, r..]) => match &*n.as_value() { + (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), )), _ => Err(()), }, - (TextShow, [v, r..]) => match &*v.as_value() { + (TextShow, [v, r..]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -156,41 +163,44 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { } _ => Err(()), }, - (ListLength, [_, l, r..]) => match &*l.as_value() { + (ListLength, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(_) => Ok((r, NaturalLit(0))), NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), _ => Err(()), }, - (ListHead, [_, l, r..]) => match &*l.as_value() { + (ListHead, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone()))) } _ => Err(()), }, - (ListLast, [_, l, r..]) => match &*l.as_value() { + (ListLast, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()))) } _ => Err(()), }, - (ListReverse, [_, l, r..]) => match &*l.as_value() { + (ListReverse, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))), NEListLit(xs) => { Ok((r, NEListLit(xs.iter().rev().cloned().collect()))) } _ => Err(()), }, - (ListIndexed, [_, l, r..]) => match &*l.as_value() { + (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(t) => { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedThunk::from_value(Value::from_builtin(Natural)), + Value::from_valuef_untyped(ValueF::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); - Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts))))) + Ok(( + r, + EmptyListLit(Value::from_valuef_untyped(RecordType(kts))), + )) } NEListLit(xs) => { let xs = xs @@ -199,105 +209,131 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { .map(|(i, e)| { let i = NaturalLit(i); let mut kvs = HashMap::new(); - kvs.insert("index".into(), Thunk::from_value(i)); + kvs.insert( + "index".into(), + Value::from_valuef_untyped(i), + ); kvs.insert("value".into(), e.clone()); - Thunk::from_value(RecordLit(kvs)) + Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); Ok((r, NEListLit(xs))) } _ => Err(()), }, - (ListBuild, [t, f, r..]) => match &*f.as_value() { + (ListBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion - Value::AppliedBuiltin(ListFold, args) => { + ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_value())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - f.app_val(Value::from_builtin(List).app_thunk(t.clone())) - .app_thunk({ - // Move `t` under new `x` variable - let t1 = t.under_binder(Label::from("x")); - make_closure!( - λ(x : #t) -> - λ(xs : List #t1) -> - [ var(x, 1) ] # var(xs, 0) - ) - }) - .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))), - )), + _ => { + let list_t = ValueF::from_builtin(List) + .app_value(t.clone()) + .into_value_simple_type(); + Ok(( + r, + f.app_value(list_t.clone()) + .app_value({ + // Move `t` under new `x` variable + let t1 = t.under_binder(Label::from("x")); + make_closure!( + λ(x : #t) -> + λ(xs : List #t1) -> + [ var(x, 1) ] # var(xs, 0) + ) + }) + .app_value( + EmptyListLit(t.clone()) + .into_value_with_type(list_t), + ), + )) + } }, - (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() { - EmptyListLit(_) => Ok((r, nil.to_value())), + (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { + EmptyListLit(_) => Ok((r, nil.to_whnf())), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { v = cons .clone() - .app_thunk(x.clone()) - .app_thunk(v) - .into_thunk(); + .app_value(x.clone()) + .app_value(v) + .into_value_untyped(); } - Ok((r, v.to_value())) + Ok((r, v.to_whnf())) } _ => Err(()), }, - (OptionalBuild, [t, f, r..]) => match &*f.as_value() { + (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion - Value::AppliedBuiltin(OptionalFold, args) => { + ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_value())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - f.app_val(Value::from_builtin(Optional).app_thunk(t.clone())) - .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0))) - .app_val(EmptyOptionalLit(TypedThunk::from_thunk( - t.clone(), - ))), - )), + _ => { + let optional_t = ValueF::from_builtin(Optional) + .app_value(t.clone()) + .into_value_simple_type(); + Ok(( + r, + f.app_value(optional_t.clone()) + .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0)))) + .app_value( + EmptyOptionalLit(t.clone()) + .into_value_with_type(optional_t), + ), + )) + } }, - (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() { - EmptyOptionalLit(_) => Ok((r, nothing.to_value())), - NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))), + (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { + EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), + NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), _ => Err(()), }, - (NaturalBuild, [f, r..]) => match &*f.as_value() { + (NaturalBuild, [f, r..]) => match &*f.as_whnf() { // fold/build fusion - Value::AppliedBuiltin(NaturalFold, args) => { + ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].to_value())) + Ok((r, args[0].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - f.app_val(Value::from_builtin(Natural)) - .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) - .app_val(NaturalLit(0)), - )), + _ => { + let nat_type = + ValueF::from_builtin(Natural).into_value_simple_type(); + Ok(( + r, + f.app_value(nat_type.clone()) + .app_value( + make_closure!(λ(x : Natural) -> 1 + var(x, 0)), + ) + .app_value( + NaturalLit(0).into_value_with_type(nat_type), + ), + )) + } }, - (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() { - NaturalLit(0) => Ok((r, zero.to_value())), + (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { + NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) + let fold = ValueF::from_builtin(NaturalFold) .app(NaturalLit(n - 1)) - .app_thunk(t.clone()) - .app_thunk(succ.clone()) - .app_thunk(zero.clone()); - Ok((r, succ.app_val(fold))) + .app_value(t.clone()) + .app_value(succ.clone()) + .app_value(zero.clone()) + .into_value_with_type(t.clone()); + Ok((r, succ.app_value(fold))) } _ => Err(()), }, @@ -307,7 +343,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { Ok((unconsumed_args, mut v)) => { let n_consumed_args = args.len() - unconsumed_args.len(); for x in args.into_iter().skip(n_consumed_args) { - v = v.app_thunk(x); + v = v.app_value(x); } v } @@ -315,22 +351,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { } } -pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value { - let fallback = |f: Thunk, a: Thunk| Value::PartialExpr(ExprF::App(f, a)); +pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { + let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)); - let f_borrow = f.as_value(); + let f_borrow = f.as_whnf(); match &*f_borrow { - Value::Lam(x, _, e) => { - let val = Typed::from_thunk_untyped(a); - e.subst_shift(&x.into(), &val).to_value() - } - Value::AppliedBuiltin(b, args) => { + ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(), + ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args) } - Value::UnionConstructor(l, kts) => { - Value::UnionLit(l.clone(), a, kts.clone()) + ValueF::UnionConstructor(l, kts) => { + ValueF::UnionLit(l.clone(), a, kts.clone()) } _ => { drop(f_borrow); @@ -340,23 +373,23 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value { } pub(crate) fn squash_textlit( - elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>, -) -> Vec<InterpolatedTextContents<Thunk>> { + elts: impl Iterator<Item = InterpolatedTextContents<Value>>, +) -> Vec<InterpolatedTextContents<Value>> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>, + elts: impl Iterator<Item = InterpolatedTextContents<Value>>, crnt_str: &mut String, - ret: &mut Vec<InterpolatedTextContents<Thunk>>, + ret: &mut Vec<InterpolatedTextContents<Value>>, ) { for contents in elts { match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_value(); + let e_borrow = e.as_whnf(); match &*e_borrow { - Value::TextLit(elts2) => { + ValueF::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) } _ => { @@ -381,32 +414,6 @@ pub(crate) fn squash_textlit( ret } -/// Reduces the imput expression to a Value. Evaluates as little as possible. -pub(crate) fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { - match expr.as_ref() { - ExprF::Embed(e) => return e.to_value(), - ExprF::Var(v) => return ctx.lookup(v), - _ => {} - } - - // Thunk subexpressions - let expr: ExprF<Thunk, Normalized> = - expr.as_ref().map_ref_with_special_handling_of_binders( - |e| Thunk::new(ctx.clone(), e.clone()), - |x, e| Thunk::new(ctx.skip(x), e.clone()), - ); - - normalize_one_layer(expr) -} - -// Small helper enum to avoid repetition -enum Ret<'a> { - Value(Value), - Thunk(Thunk), - ThunkRef(&'a Thunk), - Expr(ExprF<Thunk, Normalized>), -} - /// Performs an intersection of two HashMaps. /// /// # Arguments @@ -441,60 +448,6 @@ where kvs } -/// Performs an outer join of two HashMaps. -/// -/// # Arguments -/// -/// * `ft` - Will convert the values of the first map -/// into the target value. -/// -/// * `fu` - Will convert the values of the second map -/// into the target value. -/// -/// * `fktu` - Will convert the key and values from both maps -/// into the target type. -/// -/// # Description -/// -/// If the key is present in both maps then the final value for -/// that key is computed via the `fktu` function. Otherwise, the -/// final value will be calculated by either the `ft` or `fu` value -/// depending on which map the key is present in. -/// -/// The final map will contain all keys from the two input maps with -/// also values computed as per above. -pub(crate) fn outer_join<K, T, U, V>( - mut ft: impl FnMut(&T) -> V, - mut fu: impl FnMut(&U) -> V, - mut fktu: impl FnMut(&K, &T, &U) -> V, - map1: &HashMap<K, T>, - map2: &HashMap<K, U>, -) -> HashMap<K, V> -where - K: std::hash::Hash + Eq + Clone, -{ - let mut kvs = HashMap::new(); - - for (k1, t) in map1 { - let v = if let Some(u) = map2.get(k1) { - // The key exists in both maps - // so use all values for computation - fktu(k1, t, u) - } else { - // Key only exists in map1 - ft(t) - }; - kvs.insert(k1.clone(), v); - } - - for (k1, u) in map2 { - // Insert if key was missing in map1 - kvs.entry(k1.clone()).or_insert(fu(u)); - } - - kvs -} - pub(crate) fn merge_maps<K, V>( map1: &HashMap<K, V>, map2: &HashMap<K, V>, @@ -520,82 +473,90 @@ where kvs } -fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> { +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueF(ValueF), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF<Value, Normalized>), +} + +fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use Value::{ + use ValueF::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_value(); - let y_borrow = y.as_value(); + let x_borrow = x.as_whnf(); + let y_borrow = y.as_whnf(); Some(match (o, &*x_borrow, &*y_borrow) { - (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y), - (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x), - (BoolAnd, BoolLit(false), _) => Ret::Value(BoolLit(false)), - (BoolAnd, _, BoolLit(false)) => Ret::Value(BoolLit(false)), - (BoolAnd, _, _) if x == y => Ret::ThunkRef(x), - (BoolOr, BoolLit(true), _) => Ret::Value(BoolLit(true)), - (BoolOr, _, BoolLit(true)) => Ret::Value(BoolLit(true)), - (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y), - (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x), - (BoolOr, _, _) if x == y => Ret::ThunkRef(x), - (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y), - (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x), - (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x == y)), - (BoolEQ, _, _) if x == y => Ret::Value(BoolLit(true)), - (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y), - (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x), - (BoolNE, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x != y)), - (BoolNE, _, _) if x == y => Ret::Value(BoolLit(false)), - - (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x), + (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), + (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), + (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)), + (BoolAnd, _, _) if x == y => Ret::ValueRef(x), + (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)), + (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), + (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolOr, _, _) if x == y => Ret::ValueRef(x), + (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), + (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), + (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)), + (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), + (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)), + (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)), + + (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), + (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::Value(NaturalLit(x + y)) + Ret::ValueF(NaturalLit(x + y)) } - (NaturalTimes, NaturalLit(0), _) => Ret::Value(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => Ret::Value(NaturalLit(0)), - (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y), - (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x), + (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), + (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::Value(NaturalLit(x * y)) + Ret::ValueF(NaturalLit(x * y)) } - (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => { - Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) - } + (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), + (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit( + xs.iter().chain(ys.iter()).cloned().collect(), + )), - (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::Value(TextLit( + (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), + (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), + (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit( squash_textlit(x.iter().chain(y.iter()).cloned()), )), (TextAppend, TextLit(x), _) => { use std::iter::once; let y = InterpolatedTextContents::Expr(y.clone()); - Ret::Value(TextLit(squash_textlit( + Ret::ValueF(TextLit(squash_textlit( x.iter().cloned().chain(once(y)), ))) } (TextAppend, _, TextLit(y)) => { use std::iter::once; let x = InterpolatedTextContents::Expr(x.clone()); - Ret::Value(TextLit(squash_textlit( + Ret::ValueF(TextLit(squash_textlit( once(x).chain(y.iter().cloned()), ))) } (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ThunkRef(x) + Ret::ValueRef(x) } (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ThunkRef(y) + Ret::ValueRef(y) } (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let mut kvs = kvs2.clone(); @@ -603,54 +564,53 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> { // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v.clone()); } - Ret::Value(RecordLit(kvs)) + Ret::ValueF(RecordLit(kvs)) } (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ThunkRef(x) + Ret::ValueRef(x) } (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ThunkRef(y) + Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Thunk::from_partial_expr(ExprF::BinOp( + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), - )) + ))) }); - Ret::Value(RecordLit(kvs)) + Ret::ValueF(RecordLit(kvs)) } (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => { - Ret::ThunkRef(x) + Ret::ValueRef(x) } (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => { - Ret::ThunkRef(y) + Ret::ValueRef(y) } (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp( + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( RecursiveRecordTypeMerge, - v1.to_thunk(), - v2.to_thunk(), + v1.clone(), + v2.clone(), ))) }); - Ret::Value(RecordType(kvs)) + Ret::ValueF(RecordType(kvs)) } - (Equivalence, _, _) => Ret::Value(Value::Equivalence( - TypedThunk::from_thunk(x.clone()), - TypedThunk::from_thunk(y.clone()), - )), + (Equivalence, _, _) => { + Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone())) + } _ => return None, }) } -pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { - use Value::{ +pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { + use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor, UnionLit, UnionType, @@ -662,36 +622,25 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { ), ExprF::Embed(_) => unreachable!(), ExprF::Var(_) => unreachable!(), - ExprF::Annot(x, _) => Ret::Thunk(x), + ExprF::Annot(x, _) => Ret::Value(x), ExprF::Assert(_) => Ret::Expr(expr), - ExprF::Lam(x, t, e) => { - Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e)) - } - ExprF::Pi(x, t, e) => Ret::Value(Pi( - x.into(), - TypedThunk::from_thunk(t), - TypedThunk::from_thunk(e), - )), - ExprF::Let(x, _, v, b) => { - let v = Typed::from_thunk_untyped(v); - Ret::Thunk(b.subst_shift(&x.into(), &v)) - } - ExprF::App(v, a) => Ret::Value(v.app_thunk(a)), - ExprF::Builtin(b) => Ret::Value(Value::from_builtin(b)), - ExprF::Const(c) => Ret::Value(Value::Const(c)), - ExprF::BoolLit(b) => Ret::Value(BoolLit(b)), - ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)), - ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)), - ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)), - ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)), + ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)), + ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)), + ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)), + ExprF::App(v, a) => Ret::ValueF(v.app_value(a)), + ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)), + ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)), + ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)), + ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)), + ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)), + ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)), + ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)), ExprF::EmptyListLit(ref t) => { // Check if the type is of the form `List x` - let t_borrow = t.as_value(); + let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::Value(EmptyListLit(TypedThunk::from_thunk( - args[0].clone(), - ))) + Ret::ValueF(EmptyListLit(args[0].clone())) } _ => { drop(t_borrow); @@ -700,43 +649,39 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } } ExprF::NEListLit(elts) => { - Ret::Value(NEListLit(elts.into_iter().collect())) + Ret::ValueF(NEListLit(elts.into_iter().collect())) } ExprF::RecordLit(kvs) => { - Ret::Value(RecordLit(kvs.into_iter().collect())) + Ret::ValueF(RecordLit(kvs.into_iter().collect())) + } + ExprF::RecordType(kts) => { + Ret::ValueF(RecordType(kts.into_iter().collect())) + } + ExprF::UnionType(kts) => { + Ret::ValueF(UnionType(kts.into_iter().collect())) } - ExprF::RecordType(kts) => Ret::Value(RecordType( - kts.into_iter() - .map(|(k, t)| (k, TypedThunk::from_thunk(t))) - .collect(), - )), - ExprF::UnionType(kts) => Ret::Value(UnionType( - kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t)))) - .collect(), - )), ExprF::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); // Simplify bare interpolation if let [Expr(th)] = elts.as_slice() { - Ret::Thunk(th.clone()) + Ret::Value(th.clone()) } else { - Ret::Value(TextLit(elts)) + Ret::ValueF(TextLit(elts)) } } ExprF::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_value(); + let b_borrow = b.as_whnf(); match &*b_borrow { - BoolLit(true) => Ret::ThunkRef(e1), - BoolLit(false) => Ret::ThunkRef(e2), + BoolLit(true) => Ret::ValueRef(e1), + BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_value(); - let e2_borrow = e2.as_value(); + let e1_borrow = e1.as_whnf(); + let e2_borrow = e2.as_whnf(); match (&*e1_borrow, &*e2_borrow) { // Simplify `if b then True else False` - (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b), - _ if e1 == e2 => Ret::ThunkRef(e1), + (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), + _ if e1 == e2 => Ret::ValueRef(e1), _ => { drop(b_borrow); drop(e1_borrow); @@ -753,12 +698,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { }, ExprF::Projection(_, ref ls) if ls.is_empty() => { - Ret::Value(RecordLit(HashMap::new())) + Ret::ValueF(RecordLit(HashMap::new())) } ExprF::Projection(ref v, ref ls) => { - let v_borrow = v.as_value(); + let v_borrow = v.as_whnf(); match &*v_borrow { - RecordLit(kvs) => Ret::Value(RecordLit( + RecordLit(kvs) => Ret::ValueF(RecordLit( ls.iter() .filter_map(|l| { kvs.get(l).map(|x| (l.clone(), x.clone())) @@ -772,17 +717,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } } ExprF::Field(ref v, ref l) => { - let v_borrow = v.as_value(); + let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Thunk(r.clone()), + Some(r) => Ret::Value(r.clone()), None => { drop(v_borrow); Ret::Expr(expr) } }, UnionType(kts) => { - Ret::Value(UnionConstructor(l.clone(), kts.clone())) + Ret::ValueF(UnionConstructor(l.clone(), kts.clone())) } _ => { drop(v_borrow); @@ -792,11 +737,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } ExprF::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_value(); - let variant_borrow = variant.as_value(); + let handlers_borrow = handlers.as_whnf(); + let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { - Some(h) => Ret::Thunk(h.clone()), + Some(h) => Ret::Value(h.clone()), None => { drop(handlers_borrow); drop(variant_borrow); @@ -804,7 +749,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.app_thunk(v.clone())), + Some(h) => Ret::ValueF(h.app_value(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); @@ -821,9 +766,22 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { }; match ret { - Ret::Value(v) => v, - Ret::Thunk(th) => th.to_value(), - Ret::ThunkRef(th) => th.to_value(), - Ret::Expr(expr) => Value::PartialExpr(expr), + Ret::ValueF(v) => v, + Ret::Value(th) => th.as_whnf().clone(), + Ret::ValueRef(th) => th.as_whnf().clone(), + Ret::Expr(expr) => ValueF::PartialExpr(expr), + } +} + +/// Normalize a ValueF into WHNF +pub(crate) fn normalize_whnf(v: ValueF) -> ValueF { + match v { + ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args), + ValueF::PartialExpr(e) => normalize_one_layer(e), + ValueF::TextLit(elts) => { + ValueF::TextLit(squash_textlit(elts.into_iter())) + } + // All other cases are already in WHNF + v => v, } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 56fb5ed..c47eb78 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1,33 +1,29 @@ +use std::cmp::max; use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr, }; -use crate::core::context::{NormalizationContext, TypecheckContext}; -use crate::core::thunk::{Thunk, TypedThunk}; +use crate::core::context::TypecheckContext; use crate::core::value::Value; +use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::{Normalized, Resolved, Type, Typed}; +use crate::phase::Normalized; fn tck_pi_type( ctx: &TypecheckContext, x: Label, - tx: Type, - te: Type, -) -> Result<Typed, TypeError> { + tx: Value, + te: Value, +) -> Result<Value, TypeError> { use crate::error::TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - ctx, - InvalidInputType(tx.to_normalized()), - )) - } + _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { @@ -35,68 +31,58 @@ fn tck_pi_type( _ => { return Err(TypeError::new( &ctx2, - InvalidOutputType(te.get_type()?.to_normalized()), + InvalidOutputType(te.get_type()?.into_owned()), )) } }; let k = function_check(ka, kb); - Ok(Typed::from_thunk_and_type( - Value::Pi( - x.into(), - TypedThunk::from_type(tx), - TypedThunk::from_type(te), - ) - .into_thunk(), - Type::from_const(k), + Ok(Value::from_valuef_and_type( + ValueF::Pi(x.into(), tx, te), + Value::from_const(k), )) } fn tck_record_type( ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, Type), TypeError>>, -) -> Result<Typed, TypeError> { + kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>, +) -> Result<Value, TypeError> { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); - // Check that all types are the same const - let mut k = None; + // An empty record type has type Type + let mut k = Const::Type; for e in kts { let (x, t) = e?; - match (k, t.get_type()?.as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x.clone(), t.clone()), - )) - } + // Construct the union of the contained `Const`s + match t.get_type()?.as_const() { + Some(k2) => k = max(k, k2), + None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), } - let entry = new_kts.entry(x.clone()); + // Check for duplicated entries + let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { return Err(TypeError::new(ctx, RecordTypeDuplicateField)) } - Entry::Vacant(_) => { - entry.or_insert_with(|| TypedThunk::from_type(t.clone())) - } + Entry::Vacant(_) => entry.or_insert_with(|| t), }; } - // An empty record type has type Type - let k = k.unwrap_or(dhall_syntax::Const::Type); - Ok(Typed::from_thunk_and_type( - Value::RecordType(new_kts).into_thunk(), - Type::from_const(k), + Ok(Value::from_valuef_and_type( + ValueF::RecordType(new_kts), + Value::from_const(k), )) } -fn tck_union_type( +fn tck_union_type<Iter>( ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, Option<Type>), TypeError>>, -) -> Result<Typed, TypeError> { + kts: Iter, +) -> Result<Value, TypeError> +where + Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>, +{ use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -111,46 +97,42 @@ fn tck_union_type( _ => { return Err(TypeError::new( ctx, - InvalidFieldType(x.clone(), t.clone()), + InvalidFieldType(x, t.clone()), )) } } } - let entry = new_kts.entry(x.clone()); + let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { return Err(TypeError::new(ctx, UnionTypeDuplicateField)) } - Entry::Vacant(_) => entry.or_insert_with(|| { - t.as_ref().map(|t| TypedThunk::from_type(t.clone())) - }), + Entry::Vacant(_) => entry.or_insert_with(|| t), }; } // An empty union type has type Type; // an union type with only unary variants also has type Type - let k = k.unwrap_or(dhall_syntax::Const::Type); + let k = k.unwrap_or(Const::Type); - Ok(Typed::from_thunk_and_type( - Value::UnionType(new_kts).into_thunk(), - Type::from_const(k), + Ok(Value::from_valuef_and_type( + ValueF::UnionType(new_kts), + Value::from_const(k), )) } fn function_check(a: Const, b: Const) -> Const { - use dhall_syntax::Const::Type; - use std::cmp::max; - if b == Type { - Type + if b == Const::Type { + Const::Type } else { max(a, b) } } -pub(crate) fn type_of_const(c: Const) -> Result<Type, TypeError> { +pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> { match c { - Const::Type => Ok(Type::from_const(Const::Kind)), - Const::Kind => Ok(Type::from_const(Const::Sort)), + Const::Type => Ok(Value::from_const(Const::Kind)), + Const::Kind => Ok(Value::from_const(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } @@ -298,25 +280,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { } } -/// Takes an expression that is meant to contain a Type -/// and turn it into a type, typechecking it along the way. -pub(crate) fn mktype( - ctx: &TypecheckContext, - e: SubExpr<Normalized>, -) -> Result<Type, TypeError> { - Ok(type_with(ctx, e)?.to_type()) -} - -pub(crate) fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> { - mktype(&TypecheckContext::new(), SubExpr::from_builtin(b)) -} - -/// Intermediary return type -enum Ret { - /// Returns the contained value as is - RetWhole(Typed), - /// Use the contained Type as the type of the input expression - RetTypeOnly(Type), +// TODO: this can't fail in practise +pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> { + type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } /// Type-check an expression and return the expression alongside its type if type-checking @@ -326,28 +292,23 @@ enum Ret { fn type_with( ctx: &TypecheckContext, e: SubExpr<Normalized>, -) -> Result<Typed, TypeError> { +) -> Result<Value, TypeError> { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; - use Ret::*; Ok(match e.as_ref() { Lam(x, t, b) => { - let tx = mktype(ctx, t.clone())?; + let tx = type_with(ctx, t.clone())?; let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - let v = Value::Lam( - x.clone().into(), - TypedThunk::from_type(tx.clone()), - b.to_thunk(), - ); + let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone()); let tb = b.get_type()?.into_owned(); - let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type(); - Typed::from_thunk_and_type(Thunk::from_value(v), t) + let t = tck_pi_type(ctx, x.clone(), tx, tb)?; + Value::from_valuef_and_type(v, t) } Pi(x, ta, tb) => { - let ta = mktype(ctx, ta.clone())?; + let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(x, ta.clone()); - let tb = mktype(&ctx2, tb.clone())?; + let tb = type_with(&ctx2, tb.clone())?; return tck_pi_type(ctx, x.clone(), ta, tb); } Let(x, t, v, e) => { @@ -360,9 +321,9 @@ fn type_with( let v = type_with(ctx, v)?; return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); } - Embed(p) => p.clone().into_typed(), + Embed(p) => p.clone().into_typed().into_value(), Var(var) => match ctx.lookup(&var) { - Some(typed) => typed, + Some(typed) => typed.clone(), None => { return Err(TypeError::new( ctx, @@ -370,24 +331,13 @@ fn type_with( )) } }, - _ => { + e => { // Typecheck recursively all subexpressions - let expr = - e.as_ref().traverse_ref_with_special_handling_of_binders( - |e| type_with(ctx, e.clone()), - |_, _| unreachable!(), - )?; - let ret = type_last_layer(ctx, &expr)?; - match ret { - RetTypeOnly(typ) => { - let expr = expr.map_ref(|typed| typed.to_thunk()); - Typed::from_thunk_and_type( - Thunk::from_partial_expr(expr), - typ, - ) - } - RetWhole(tt) => tt, - } + let expr = e.traverse_ref_with_special_handling_of_binders( + |e| type_with(ctx, e.clone()), + |_, _| unreachable!(), + )?; + type_last_layer(ctx, expr)? } }) } @@ -396,17 +346,25 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF<Typed, Normalized>, -) -> Result<Ret, TypeError> { + e: ExprF<Value, Normalized>, +) -> Result<Value, TypeError> { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; use dhall_syntax::Builtin::*; use dhall_syntax::Const::Type; use dhall_syntax::ExprF::*; + let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); + + /// Intermediary return type + enum Ret { + /// Returns the contained value as is + RetWhole(Value), + /// Returns the input expression `e` with the contained value as its type + RetTypeOnly(Value), + } use Ret::*; - let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg); - match e { + let ret = match &e { Import(_) => unreachable!( "There should remain no imports in a resolved expression" ), @@ -415,456 +373,296 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &tf.to_value() { - Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()), - _ => return Err(mkerr(NotAFunction(f.clone()))), + let tf_borrow = tf.as_whnf(); + let (x, tx, tb) = match &*tf_borrow { + ValueF::Pi(x, tx, tb) => (x, tx, tb), + _ => return mkerr(NotAFunction(f.clone())), }; - if a.get_type()?.as_ref() != &tx { - return Err(mkerr(TypeMismatch( - f.clone(), - tx.to_normalized(), - a.clone(), - ))); + if a.get_type()?.as_ref() != tx { + return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } - Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) + RetTypeOnly(tb.subst_shift(&x.into(), a)) } Annot(x, t) => { - let t = t.to_type(); - if &t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized()))); + if t != x.get_type()?.as_ref() { + return mkerr(AnnotMismatch(x.clone(), t.clone())); } - Ok(RetTypeOnly(x.get_type()?.into_owned())) + RetTypeOnly(x.get_type()?.into_owned()) } Assert(t) => { - match t.to_value() { - Value::Equivalence(ref x, ref y) if x == y => {} - Value::Equivalence(x, y) => { - return Err(mkerr(AssertMismatch( - x.to_typed(), - y.to_typed(), - ))) + match &*t.as_whnf() { + ValueF::Equivalence(x, y) if x == y => {} + ValueF::Equivalence(x, y) => { + return mkerr(AssertMismatch(x.clone(), y.clone())) } - _ => return Err(mkerr(AssertMustTakeEquivalence)), + _ => return mkerr(AssertMustTakeEquivalence), } - Ok(RetTypeOnly(t.to_type())) + RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { if x.get_type()?.as_ref() != &builtin_to_type(Bool)? { - return Err(mkerr(InvalidPredicate(x.clone()))); + return mkerr(InvalidPredicate(x.clone())); } if y.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(IfBranchMustBeTerm(true, y.clone()))); + return mkerr(IfBranchMustBeTerm(true, y.clone())); } if z.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(IfBranchMustBeTerm(false, z.clone()))); + return mkerr(IfBranchMustBeTerm(false, z.clone())); } if y.get_type()? != z.get_type()? { - return Err(mkerr(IfBranchMismatch(y.clone(), z.clone()))); + return mkerr(IfBranchMismatch(y.clone(), z.clone())); } - Ok(RetTypeOnly(y.get_type()?.into_owned())) + RetTypeOnly(y.get_type()?.into_owned()) } EmptyListLit(t) => { - let t = t.to_type(); - match &t.to_value() { - Value::AppliedBuiltin(dhall_syntax::Builtin::List, args) + match &*t.as_whnf() { + ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} - _ => { - return Err(TypeError::new( - ctx, - InvalidListType(t.to_normalized()), - )) - } + _ => return mkerr(InvalidListType(t.clone())), } - Ok(RetTypeOnly(t)) + RetTypeOnly(t.clone()) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, x) = iter.next().unwrap(); for (i, y) in iter { if x.get_type()? != y.get_type()? { - return Err(mkerr(InvalidListElement( + return mkerr(InvalidListElement( i, - x.get_type()?.to_normalized(), + x.get_type()?.into_owned(), y.clone(), - ))); + )); } } let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new( - ctx, - InvalidListType(t.to_normalized()), - )); + return mkerr(InvalidListType(t.into_owned())); } - Ok(RetTypeOnly( - Typed::from_thunk_and_type( - Value::from_builtin(dhall_syntax::Builtin::List) - .app(t.to_value()) - .into_thunk(), - Typed::from_const(Type), - ) - .to_type(), + RetTypeOnly(Value::from_valuef_and_type( + ValueF::from_builtin(dhall_syntax::Builtin::List) + .app_value(t.into_owned()), + Value::from_const(Type), )) } SomeLit(x) => { let t = x.get_type()?.into_owned(); if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new( - ctx, - InvalidOptionalType(t.to_normalized()), - )); + return mkerr(InvalidOptionalType(t)); } - Ok(RetTypeOnly( - Typed::from_thunk_and_type( - Value::from_builtin(dhall_syntax::Builtin::Optional) - .app(t.to_value()) - .into_thunk(), - Typed::from_const(Type).into_type(), - ) - .to_type(), + RetTypeOnly(Value::from_valuef_and_type( + ValueF::from_builtin(dhall_syntax::Builtin::Optional) + .app_value(t), + Value::from_const(Type), )) } - RecordType(kts) => Ok(RetWhole(tck_record_type( + RecordType(kts) => RetWhole(tck_record_type( ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))), - )?)), - UnionType(kts) => Ok(RetWhole(tck_union_type( + kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), + )?), + UnionType(kts) => RetWhole(tck_union_type( ctx, - kts.iter() - .map(|(x, t)| Ok((x.clone(), t.as_ref().map(|t| t.to_type())))), - )?)), - RecordLit(kvs) => Ok(RetTypeOnly( - tck_record_type( - ctx, - kvs.iter() - .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), - )? - .into_type(), - )), + kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), + )?), + RecordLit(kvs) => RetTypeOnly(tck_record_type( + ctx, + kvs.iter() + .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), + )?), Field(r, x) => { - match &r.get_type()?.to_value() { - Value::RecordType(kts) => match kts.get(&x) { + match &*r.get_type()?.as_whnf() { + ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { - Ok(RetTypeOnly(tth.to_type())) + RetTypeOnly(tth.clone()) }, - None => Err(mkerr(MissingRecordField(x.clone(), - r.clone()))), + None => return mkerr(MissingRecordField(x.clone(), + r.clone())), }, // TODO: branch here only when r.get_type() is a Const _ => { - let r = r.to_type(); - match &r.to_value() { - Value::UnionType(kts) => match kts.get(&x) { + match &*r.as_whnf() { + ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - // TODO: avoid capture - Ok(RetTypeOnly( + RetTypeOnly( tck_pi_type( ctx, "_".into(), - t.to_type(), - r.clone(), - )?.to_type() - )) + t.clone(), + r.under_binder(Label::from("_")), + )? + ) }, Some(None) => { - Ok(RetTypeOnly(r.clone())) + RetTypeOnly(r.clone()) }, None => { - Err(mkerr(MissingUnionField( + return mkerr(MissingUnionField( x.clone(), - r.to_normalized(), - ))) + r.clone(), + )) }, }, _ => { - Err(mkerr(NotARecord( + return mkerr(NotARecord( x.clone(), - r.to_normalized() - ))) + r.clone() + )) }, } } - // _ => Err(mkerr(NotARecord( + // _ => mkerr(NotARecord( // x, - // r.to_type()?.to_normalized(), - // ))), + // r?, + // )), } } - Const(c) => Ok(RetWhole(Typed::from_const(*c))), - Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)), - BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), - NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), - IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), - DoubleLit(_) => Ok(RetTypeOnly(builtin_to_type(Double)?)), + Const(c) => RetWhole(Value::from_const(*c)), + Builtin(b) => RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?), + BoolLit(_) => RetTypeOnly(builtin_to_type(Bool)?), + NaturalLit(_) => RetTypeOnly(builtin_to_type(Natural)?), + IntegerLit(_) => RetTypeOnly(builtin_to_type(Integer)?), + DoubleLit(_) => RetTypeOnly(builtin_to_type(Double)?), TextLit(interpolated) => { let text_type = builtin_to_type(Text)?; for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { if x.get_type()?.as_ref() != &text_type { - return Err(mkerr(InvalidTextInterpolation(x.clone()))); + return mkerr(InvalidTextInterpolation(x.clone())); } } } - Ok(RetTypeOnly(text_type)) + RetTypeOnly(text_type) } BinOp(RightBiasedRecordMerge, l, r) => { use crate::phase::normalize::merge_maps; let l_type = l.get_type()?; - let l_kind = l_type.get_type()?; let r_type = r.get_type()?; - let r_kind = r_type.get_type()?; - - // Check the equality of kinds. - // This is to disallow expression such as: - // "{ x = Text } // { y = 1 }" - if l_kind != r_kind { - return Err(mkerr(RecordMismatch(l.clone(), r.clone()))); - } // Extract the LHS record type - let kts_x = match l_type.to_value() { - Value::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(l.clone()))), + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { + ValueF::RecordType(kts) => kts, + _ => return mkerr(MustCombineRecord(l.clone())), }; // Extract the RHS record type - let kts_y = match r_type.to_value() { - Value::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(r.clone()))), + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { + ValueF::RecordType(kts) => kts, + _ => return mkerr(MustCombineRecord(r.clone())), }; // Union the two records, prefering // the values found in the RHS. - let kts = merge_maps(&kts_x, &kts_y, |_, r_t| r_t.clone()); + let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union - Ok(RetTypeOnly( - tck_record_type( - ctx, - kts.iter().map(|(x, v)| Ok((x.clone(), v.to_type()))), - )? - .into_type(), - )) - } - BinOp(RecursiveRecordMerge, l, r) => { - // A recursive function to dig down into - // records of records when merging. - fn combine_record_types( - ctx: &TypecheckContext, - kts_l: HashMap<Label, TypedThunk>, - kts_r: HashMap<Label, TypedThunk>, - ) -> Result<Typed, TypeError> { - use crate::phase::normalize::outer_join; - - // If the Label exists for both records and Type for the values - // are records themselves, then we hit the recursive case. - // Otherwise we have a field collision. - let combine = |k: &Label, - inner_l: &TypedThunk, - inner_r: &TypedThunk| - -> Result<Typed, TypeError> { - match (inner_l.to_value(), inner_r.to_value()) { - ( - Value::RecordType(inner_l_kvs), - Value::RecordType(inner_r_kvs), - ) => { - combine_record_types(ctx, inner_l_kvs, inner_r_kvs) - } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; - - let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join( - |l| Ok(l.to_type()), - |r| Ok(r.to_type()), - |k: &Label, l: &TypedThunk, r: &TypedThunk| { - combine(k, l, r) - }, - &kts_l, - &kts_r, - ); - - Ok(tck_record_type( - ctx, - kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )? - .into_type()) - }; - - let l_type = l.get_type()?; - let l_kind = l_type.get_type()?; - let r_type = r.get_type()?; - let r_kind = r_type.get_type()?; - - // Check the equality of kinds. - // This is to disallow expression such as: - // "{ x = Text } // { y = 1 }" - if l_kind != r_kind { - return Err(mkerr(RecordMismatch(l.clone(), r.clone()))); - } - - // Extract the LHS record type - let kts_x = match l_type.to_value() { - Value::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(l.clone()))), - }; - - // Extract the RHS record type - let kts_y = match r_type.to_value() { - Value::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(r.clone()))), - }; - - combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r)) + RetTypeOnly(tck_record_type( + ctx, + kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), + )?) } + BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( + ctx, + ExprF::BinOp( + RecursiveRecordTypeMerge, + l.get_type()?.into_owned(), + r.get_type()?.into_owned(), + ), + )?), BinOp(RecursiveRecordTypeMerge, l, r) => { - // A recursive function to dig down into - // records of records when merging. - fn combine_record_types( - ctx: &TypecheckContext, - kts_l: HashMap<Label, TypedThunk>, - kts_r: HashMap<Label, TypedThunk>, - ) -> Result<Typed, TypeError> { - use crate::phase::normalize::intersection_with_key; - - // If the Label exists for both records and Type for the values - // are records themselves, then we hit the recursive case. - // Otherwise we have a field collision. - let combine = |k: &Label, - kts_l_inner: &TypedThunk, - kts_r_inner: &TypedThunk| - -> Result<Typed, TypeError> { - match (kts_l_inner.to_value(), kts_r_inner.to_value()) { - ( - Value::RecordType(kvs_l_inner), - Value::RecordType(kvs_r_inner), - ) => { - combine_record_types(ctx, kvs_l_inner, kvs_r_inner) - } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; - - let kts = intersection_with_key( - |k: &Label, l: &TypedThunk, r: &TypedThunk| { - combine(k, l, r) - }, - &kts_l, - &kts_r, - ); - - Ok(tck_record_type( - ctx, - kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )? - .into_type()) - }; + use crate::phase::normalize::intersection_with_key; // Extract the Const of the LHS - let k_l = match l.get_type()?.to_value() { - Value::Const(k) => k, + let k_l = match l.get_type()?.as_const() { + Some(k) => k, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - l.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } }; // Extract the Const of the RHS - let k_r = match r.get_type()?.to_value() { - Value::Const(k) => k, + let k_r = match r.get_type()?.as_const() { + Some(k) => k, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - r.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } }; - // Const values must match for the Records - let k = if k_l == k_r { - k_l - } else { - return Err(mkerr(RecordTypeMismatch( - Typed::from_const(k_l), - Typed::from_const(k_r), - l.clone(), - r.clone(), - ))); - }; + let k = max(k_l, k_r); // Extract the LHS record type - let kts_x = match l.to_value() { - Value::RecordType(kts) => kts, + let borrow_l = l.as_whnf(); + let kts_x = match &*borrow_l { + ValueF::RecordType(kts) => kts, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - l.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } }; // Extract the RHS record type - let kts_y = match r.to_value() { - Value::RecordType(kts) => kts, + let borrow_r = r.as_whnf(); + let kts_y = match &*borrow_r { + ValueF::RecordType(kts) => kts, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - r.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } }; // Ensure that the records combine without a type error - // and if not output the final Const value. - combine_record_types(ctx, kts_x, kts_y) - .and(Ok(RetTypeOnly(Typed::from_const(k)))) + let kts = intersection_with_key( + // If the Label exists for both records, then we hit the recursive case. + |_: &Label, l: &Value, r: &Value| { + type_last_layer( + ctx, + ExprF::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + ), + ) + }, + kts_x, + kts_y, + ); + tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?; + + RetTypeOnly(Value::from_const(k)) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.to_value() { - Value::AppliedBuiltin(List, _) => {} - _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), + match &*l.get_type()?.as_whnf() { + ValueF::AppliedBuiltin(List, _) => {} + _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } if l.get_type()? != r.get_type()? { - return Err(mkerr(BinOpTypeMismatch(*o, r.clone()))); + return mkerr(BinOpTypeMismatch(*o, r.clone())); } - Ok(RetTypeOnly(l.get_type()?.into_owned())) + RetTypeOnly(l.get_type()?.into_owned()) } BinOp(Equivalence, l, r) => { if l.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(EquivalenceArgumentMustBeTerm( - true, - l.clone(), - ))); + return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); } if r.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(EquivalenceArgumentMustBeTerm( - false, - r.clone(), - ))); + return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); } if l.get_type()? != r.get_type()? { - return Err(mkerr(EquivalenceTypeMismatch( - r.clone(), - l.clone(), - ))); + return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); } - Ok(RetTypeOnly(Typed::from_const(Type).into_type())) + RetTypeOnly(Value::from_const(Type)) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -884,140 +682,136 @@ fn type_last_layer( })?; if l.get_type()?.as_ref() != &t { - return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))); + return mkerr(BinOpTypeMismatch(*o, l.clone())); } if r.get_type()?.as_ref() != &t { - return Err(mkerr(BinOpTypeMismatch(*o, r.clone()))); + return mkerr(BinOpTypeMismatch(*o, r.clone())); } - Ok(RetTypeOnly(t)) + RetTypeOnly(t) } Merge(record, union, type_annot) => { - let handlers = match record.get_type()?.to_value() { - Value::RecordType(kts) => kts, - _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let handlers = match &*record_borrow { + ValueF::RecordType(kts) => kts, + _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), }; - let variants = match union.get_type()?.to_value() { - Value::UnionType(kts) => kts, - _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), + let union_type = union.get_type()?; + let union_borrow = union_type.as_whnf(); + let variants = match &*union_borrow { + ValueF::UnionType(kts) => kts, + _ => return mkerr(Merge2ArgMustBeUnion(union.clone())), }; let mut inferred_type = None; - for (x, handler) in handlers.iter() { - let handler_return_type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => { - let variant_type = variant_type.to_type(); - let handler_type = handler.to_type(); - let (x, tx, tb) = match &handler_type.to_value() { - Value::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) + for (x, handler_type) in handlers { + let handler_return_type = + match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => { + let handler_type_borrow = handler_type.as_whnf(); + let (x, tx, tb) = match &*handler_type_borrow { + ValueF::Pi(x, tx, tb) => (x, tx, tb), + _ => { + return mkerr(NotAFunction( + handler_type.clone(), + )) + } + }; + + if variant_type != tx { + return mkerr(TypeMismatch( + handler_type.clone(), + tx.clone(), + variant_type.clone(), + )); } - _ => return Err(mkerr(NotAFunction(handler_type))), - }; - - if &variant_type != &tx { - return Err(mkerr(TypeMismatch( - handler_type, - tx.to_normalized(), - variant_type, - ))); - } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { - Some(x) => x, - None => { - return Err(mkerr( + // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. + match tb.over_binder(x) { + Some(x) => x, + None => return mkerr( MergeHandlerReturnTypeMustNotBeDependent, - )) + ), } } - } - // Union alternative without type - Some(None) => handler.to_type(), - None => { - return Err(mkerr(MergeHandlerMissingVariant( - x.clone(), - ))) - } - }; + // Union alternative without type + Some(None) => handler_type.clone(), + None => { + return mkerr(MergeHandlerMissingVariant(x.clone())) + } + }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { if t != &handler_return_type { - return Err(mkerr(MergeHandlerTypeMismatch)); + return mkerr(MergeHandlerTypeMismatch); } } } } for x in variants.keys() { if !handlers.contains_key(x) { - return Err(mkerr(MergeVariantMissingHandler(x.clone()))); + return mkerr(MergeVariantMissingHandler(x.clone())); } } match (inferred_type, type_annot) { (Some(ref t1), Some(t2)) => { - let t2 = t2.to_type(); - if t1 != &t2 { - return Err(mkerr(MergeAnnotMismatch)); + if t1 != t2 { + return mkerr(MergeAnnotMismatch); } - Ok(RetTypeOnly(t2)) + RetTypeOnly(t2.clone()) } - (Some(t), None) => Ok(RetTypeOnly(t)), - (None, Some(t)) => Ok(RetTypeOnly(t.to_type())), - (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)), + (Some(t), None) => RetTypeOnly(t), + (None, Some(t)) => RetTypeOnly(t.clone()), + (None, None) => return mkerr(MergeEmptyNeedsAnnotation), } } Projection(record, labels) => { - let trecord = record.get_type()?; - let kts = match trecord.to_value() { - Value::RecordType(kts) => kts, - _ => return Err(mkerr(ProjectionMustBeRecord)), + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let kts = match &*record_borrow { + ValueF::RecordType(kts) => kts, + _ => return mkerr(ProjectionMustBeRecord), }; let mut new_kts = HashMap::new(); for l in labels { match kts.get(l) { - None => return Err(mkerr(ProjectionMissingEntry)), + None => return mkerr(ProjectionMissingEntry), Some(t) => new_kts.insert(l.clone(), t.clone()), }; } - Ok(RetTypeOnly( - Typed::from_thunk_and_type( - Value::RecordType(new_kts).into_thunk(), - trecord.get_type()?.into_owned(), - ) - .to_type(), + RetTypeOnly(Value::from_valuef_and_type( + ValueF::RecordType(new_kts), + record_type.get_type()?.into_owned(), )) } - } + }; + + Ok(match ret { + RetTypeOnly(typ) => { + Value::from_valuef_and_type(ValueF::PartialExpr(e), typ) + } + RetWhole(v) => v, + }) } -/// `typeOf` is the same as `type_with` with an empty context, meaning that the +/// `type_of` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -fn type_of(e: SubExpr<Normalized>) -> Result<Typed, TypeError> { - let ctx = TypecheckContext::new(); - let e = type_with(&ctx, e)?; - // Ensure `e` has a type (i.e. `e` is not `Sort`) - e.get_type()?; - Ok(e) +pub(crate) fn typecheck(e: SubExpr<Normalized>) -> Result<Value, TypeError> { + type_with(&TypecheckContext::new(), e) } -pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> { - type_of(e.0) -} - -pub(crate) fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> { - let expr: SubExpr<_> = e.0; - let ty: SubExpr<_> = ty.to_expr(); - type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) -} -pub(crate) fn skip_typecheck(e: Resolved) -> Typed { - Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0)) +pub(crate) fn typecheck_with( + expr: SubExpr<Normalized>, + ty: SubExpr<Normalized>, +) -> Result<Value, TypeError> { + typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index d269523..be4805d 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -169,7 +169,7 @@ pub fn run_test( let expected_file_path = base_path + "B.dhall"; let expected = parse_file_str(&expected_file_path)? .resolve()? - .skip_typecheck() + .typecheck()? .normalize(); match feature { @@ -177,24 +177,23 @@ pub fn run_test( unreachable!() } Import => { - let expr = expr.skip_typecheck().normalize(); + let expr = expr.typecheck()?.normalize(); assert_eq_display!(expr, expected); } Typecheck => { - expr.typecheck_with(&expected.to_type())?; + expr.typecheck_with(&expected.into_typed())?.get_type()?; } TypeInference => { let expr = expr.typecheck()?; - let ty = expr.get_type()?.into_owned(); - assert_eq_display!(ty.to_normalized(), expected); + let ty = expr.get_type()?.into_owned().normalize(); + assert_eq_display!(ty, expected); } Normalization => { - let expr = expr.skip_typecheck().normalize(); + let expr = expr.typecheck()?.normalize(); assert_eq_display!(expr, expected); } AlphaNormalization => { - let expr = - expr.skip_typecheck().normalize().to_expr_alpha(); + let expr = expr.typecheck()?.normalize().to_expr_alpha(); assert_eq_display!(expr, expected.to_expr()); } } @@ -226,10 +225,15 @@ pub fn run_test( } Normalization | AlphaNormalization => unreachable!(), Typecheck | TypeInference => { - parse_file_str(&file_path)? - .skip_resolve()? - .typecheck() - .unwrap_err(); + let res = + parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + match res { + Err(_) => {} + // If e did typecheck, check that it doesn't have a type + Ok(e) => { + e.get_type().unwrap_err(); + } + } } } } |