diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/expr.rs | 208 | ||||
| -rw-r--r-- | dhall/src/lib.rs | 2 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 1250 | ||||
| -rw-r--r-- | dhall/src/serde.rs | 2 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 11 | ||||
| -rw-r--r-- | dhall/src/traits/deserialize.rs | 2 | ||||
| -rw-r--r-- | dhall/src/traits/dynamic_type.rs | 33 | ||||
| -rw-r--r-- | dhall/src/traits/static_type.rs | 13 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 954 |
9 files changed, 1719 insertions, 756 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index bb1a4e4..4d55f4a 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -1,4 +1,5 @@ use crate::imports::ImportRoot; +use crate::normalize::{Thunk, Value}; use dhall_core::*; use std::marker::PhantomData; @@ -10,6 +11,8 @@ macro_rules! derive_other_traits { } } + impl<'a> std::cmp::Eq for $ty<'a> {} + impl<'a> std::fmt::Display for $ty<'a> { fn fmt( &self, @@ -21,34 +24,149 @@ macro_rules! derive_other_traits { }; } -#[derive(Debug, Clone, Eq)] +#[derive(Debug, Clone)] pub(crate) struct Parsed<'a>( pub(crate) SubExpr<Span<'a>, Import>, pub(crate) ImportRoot, ); derive_other_traits!(Parsed); -#[derive(Debug, Clone, Eq)] +#[derive(Debug, Clone)] pub(crate) struct Resolved<'a>( pub(crate) SubExpr<Span<'a>, Normalized<'static>>, ); derive_other_traits!(Resolved); -#[derive(Debug, Clone, Eq)] +pub(crate) use self::typed::TypedInternal; + +#[derive(Debug, Clone)] pub(crate) struct Typed<'a>( - pub(crate) SubExpr<X, Normalized<'static>>, - pub(crate) Option<Type<'static>>, + pub(crate) TypedInternal, pub(crate) PhantomData<&'a ()>, ); -derive_other_traits!(Typed); -#[derive(Debug, Clone, Eq)] +#[derive(Debug, Clone)] pub(crate) struct Normalized<'a>( - pub(crate) SubExpr<X, X>, - pub(crate) Option<Type<'static>>, + pub(crate) TypedInternal, pub(crate) PhantomData<&'a ()>, ); -derive_other_traits!(Normalized); + +impl<'a> std::cmp::PartialEq for Normalized<'a> { + fn eq(&self, other: &Self) -> bool { + self.to_expr() == other.to_expr() + } +} + +impl<'a> std::cmp::Eq for Normalized<'a> {} + +impl<'a> std::fmt::Display for Normalized<'a> { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_expr().fmt(f) + } +} + +mod typed { + use super::{Type, Typed}; + use crate::normalize::{Thunk, Value}; + use crate::typecheck::{ + TypeError, TypeInternal, TypeMessage, TypecheckContext, + }; + use dhall_core::{Const, Label, SubExpr, V, X}; + use std::borrow::Cow; + use std::marker::PhantomData; + + #[derive(Debug, Clone)] + pub(crate) enum TypedInternal { + // The `Sort` higher-kinded type doesn't have a type + Sort, + // Any other value, along with its type + Value(Thunk, Option<Type<'static>>), + } + + impl TypedInternal { + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self { + TypedInternal::Value(th, Some(t)) + } + + pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { + TypedInternal::Value(th, None) + } + + // TODO: Avoid cloning if possible + pub(crate) fn to_value(&self) -> Value { + match self { + TypedInternal::Value(th, _) => th.normalize_whnf().clone(), + TypedInternal::Sort => Value::Const(Const::Sort), + } + } + + pub(crate) fn to_expr(&self) -> SubExpr<X, X> { + self.to_value().normalize_to_expr() + } + + pub(crate) fn to_thunk(&self) -> Thunk { + match self { + TypedInternal::Value(th, _) => th.clone(), + TypedInternal::Sort => { + Thunk::from_whnf(Value::Const(Const::Sort)) + } + } + } + + pub(crate) fn to_type(&self) -> Type<'static> { + match self { + TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)), + TypedInternal::Value(th, _) => match &*th.normalize_whnf() { + Value::Const(c) => Type(TypeInternal::Const(*c)), + _ => Type(TypeInternal::Typed(Box::new(Typed( + self.clone(), + PhantomData, + )))), + }, + } + } + + pub(crate) fn get_type( + &self, + ) -> Result<Cow<'_, Type<'static>>, TypeError> { + match self { + TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)), + TypedInternal::Value(_, None) => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, + )), + TypedInternal::Sort => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Sort, + )), + } + } + + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { + match self { + TypedInternal::Value(th, t) => TypedInternal::Value( + th.shift(delta, var), + t.as_ref().map(|x| x.shift(delta, var)), + ), + TypedInternal::Sort => TypedInternal::Sort, + } + } + + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { + match self { + TypedInternal::Value(th, t) => TypedInternal::Value( + th.subst_shift(var, val), + t.as_ref().map(|x| x.subst_shift(var, val)), + ), + TypedInternal::Sort => TypedInternal::Sort, + } + } + } +} /// A Dhall expression representing a simple type. /// @@ -56,13 +174,15 @@ derive_other_traits!(Normalized); /// `Bool`, `{ x: Integer }` or `Natural -> Text`. /// /// For a more general notion of "type", see [Type]. -#[derive(Debug, Clone, Eq)] +#[derive(Debug, Clone)] pub struct SimpleType<'a>( pub(crate) SubExpr<X, X>, pub(crate) PhantomData<&'a ()>, ); derive_other_traits!(SimpleType); +pub(crate) use crate::typecheck::TypeInternal; + /// A Dhall expression representing a (possibly higher-kinded) type. /// /// This includes [SimpleType]s but also higher-kinded expressions like @@ -70,12 +190,10 @@ derive_other_traits!(SimpleType); #[derive(Debug, Clone, PartialEq, Eq)] pub struct Type<'a>(pub(crate) TypeInternal<'a>); -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum TypeInternal<'a> { - Expr(Box<Normalized<'a>>), - Const(dhall_core::Const), - /// The type of `Sort` - SuperType, +impl<'a> std::fmt::Display for Type<'a> { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_normalized().fmt(f) + } } // Exposed for the macros @@ -98,50 +216,38 @@ impl<'a> From<SubExpr<X, X>> for SimpleType<'a> { #[doc(hidden)] impl<'a> From<Normalized<'a>> for Typed<'a> { fn from(x: Normalized<'a>) -> Typed<'a> { - Typed(x.0.embed_absurd(), x.1, x.2) + Typed(x.0, x.1) } } -#[doc(hidden)] -impl<'a> Typed<'a> { - pub(crate) fn as_expr(&self) -> &SubExpr<X, Normalized<'a>> { - &self.0 - } -} - -#[doc(hidden)] impl<'a> Normalized<'a> { - pub(crate) fn as_expr(&self) -> &SubExpr<X, X> { - &self.0 + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self { + Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData) } - pub(crate) fn into_expr(self) -> SubExpr<X, X> { - self.0 + // Deprecated + pub(crate) fn as_expr(&self) -> SubExpr<X, X> { + self.0.to_expr() } - pub(crate) fn unnote<'b>(self) -> Normalized<'b> { - Normalized(self.0, self.1, PhantomData) + pub(crate) fn to_expr(&self) -> SubExpr<X, X> { + self.0.to_expr() } - pub(crate) fn into_type(self) -> Type<'a> { - Type(match self.0.as_ref() { - ExprF::Const(c) => TypeInternal::Const(*c), - _ => TypeInternal::Expr(Box::new(self)), - }) + pub(crate) fn to_value(&self) -> Value { + self.0.to_value() } -} - -#[doc(hidden)] -impl<'a> Type<'a> { - pub(crate) fn unnote<'b>(self) -> Type<'b> { - use TypeInternal::*; - Type(match self.0 { - Expr(e) => Expr(Box::new(e.unnote())), - Const(c) => Const(c), - SuperType => SuperType, - }) + #[allow(dead_code)] + pub(crate) fn unnote<'b>(self) -> Normalized<'b> { + Normalized(self.0, PhantomData) } } -impl<'a> SimpleType<'a> { - pub(crate) fn into_type(self) -> Type<'a> { - Normalized(self.0, Some(Type::const_type()), PhantomData).into_type() +impl<'a> Typed<'a> { + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self { + Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData) + } + pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { + Typed(TypedInternal::from_thunk_untyped(th), PhantomData) + } + pub(crate) fn const_sort() -> Self { + Typed(TypedInternal::Sort, PhantomData) } } diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c85b962..6e4361f 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -4,6 +4,8 @@ #![feature(label_break_value)] #![feature(non_exhaustive)] #![feature(bind_by_move_pattern_guards)] +#![feature(try_trait)] +#![feature(inner_deref)] #![cfg_attr(test, feature(custom_inner_attributes))] #![allow( clippy::type_complexity, diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index f092c4d..f991a2e 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -4,48 +4,68 @@ use std::rc::Rc; use dhall_core::context::Context; use dhall_core::{ - rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText, + rc, Builtin, Const, ExprF, Integer, InterpolatedText, InterpolatedTextContents, Label, Natural, SubExpr, V, X, }; use dhall_generator as dhall; -use crate::expr::{Normalized, Typed}; +use crate::expr::{Normalized, Type, Typed, TypedInternal}; type InputSubExpr = SubExpr<X, Normalized<'static>>; type OutputSubExpr = SubExpr<X, X>; impl<'a> Typed<'a> { + /// Reduce an expression to its normal form, performing beta reduction + /// + /// `normalize` does not type-check the expression. You may want to type-check + /// expressions before normalizing them since normalization can convert an + /// ill-typed expression into a well-typed expression. + /// + /// However, `normalize` will not fail if the expression is ill-typed and will + /// leave ill-typed sub-expressions unevaluated. + /// pub fn normalize(self) -> Normalized<'a> { - Normalized(normalize(self.0), self.1, self.2) + let internal = match self.0 { + TypedInternal::Sort => TypedInternal::Sort, + TypedInternal::Value(thunk, t) => { + // TODO: stupid but needed for now + let thunk = + Thunk::from_normalized_expr(thunk.normalize_to_expr()); + thunk.normalize_nf(); + TypedInternal::Value(thunk, t) + } + }; + Normalized(internal, self.1) } - /// Pretends this expression is normalized. Use with care. - #[allow(dead_code)] - pub fn skip_normalize(self) -> Normalized<'a> { - Normalized( - self.0.unroll().squash_embed(|e| e.0.clone()), - self.1, - self.2, - ) + + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { + Typed(self.0.shift(delta, var), self.1) } -} -fn shift0_mut<N, E>(delta: isize, label: &Label, in_expr: &mut SubExpr<N, E>) { - let new_expr = shift0(delta, label, &in_expr); - std::mem::replace(in_expr, new_expr); -} + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { + Typed(self.0.subst_shift(var, val), self.1) + } + + pub(crate) fn to_value(&self) -> Value { + self.0.to_value() + } -fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) { - let new_expr = shift(delta, var, &in_expr); - std::mem::replace(in_expr, new_expr); + pub(crate) fn to_thunk(&self) -> Thunk { + self.0.to_thunk() + } } -fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { +fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value { use dhall_core::Builtin::*; - use WHNF::*; + use Value::*; let ret = match b { OptionalNone => improved_slice_patterns::match_vec!(args; - [t] => EmptyOptionalLit(Now::from_whnf(t)), + [t] => EmptyOptionalLit(TypeThunk::from_whnf(t)), ), NaturalIsZero => improved_slice_patterns::match_vec!(args; [NaturalLit(n)] => BoolLit(n == 0), @@ -93,12 +113,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { let mut kts = BTreeMap::new(); kts.insert( "index".into(), - Now::from_whnf( - WHNF::from_builtin(Natural) + TypeThunk::from_whnf( + Value::from_builtin(Natural) ), ); kts.insert("value".into(), t); - EmptyListLit(Now::from_whnf(RecordType(kts))) + EmptyListLit(TypeThunk::from_whnf(RecordType(kts))) }, [_, NEListLit(xs)] => { let xs = xs @@ -107,9 +127,9 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { .map(|(i, e)| { let i = NaturalLit(i); let mut kvs = BTreeMap::new(); - kvs.insert("index".into(), Now::from_whnf(i)); + kvs.insert("index".into(), Thunk::from_whnf(i)); kvs.insert("value".into(), e); - Now::from_whnf(RecordLit(kvs)) + Thunk::from_whnf(RecordLit(kvs)) }) .collect(); NEListLit(xs) @@ -117,7 +137,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { ), ListBuild => improved_slice_patterns::match_vec!(args; // fold/build fusion - [_, WHNF::AppliedBuiltin(ListFold, args)] => { + [_, Value::AppliedBuiltin(ListFold, args)] => { let mut args = args; if args.len() >= 2 { args.remove(1) @@ -127,13 +147,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { } }, [t, g] => g - .app(WHNF::from_builtin(List).app(t.clone())) - .app(ListConsClosure(Now::from_whnf(t.clone()), None)) - .app(EmptyListLit(Now::from_whnf(t))), + .app(Value::from_builtin(List).app(t.clone())) + .app(ListConsClosure(TypeThunk::from_whnf(t.clone()), None)) + .app(EmptyListLit(TypeThunk::from_whnf(t))), ), ListFold => improved_slice_patterns::match_vec!(args; // fold/build fusion - [_, WHNF::AppliedBuiltin(ListBuild, args)] => { + [_, Value::AppliedBuiltin(ListBuild, args)] => { let mut args = args; if args.len() >= 2 { args.remove(1) @@ -145,14 +165,14 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { [_, NEListLit(xs), _, cons, nil] => { let mut v = nil; for x in xs.into_iter().rev() { - v = cons.clone().app(x.normalize()).app(v); + v = cons.clone().app_thunk(x).app(v); } v } ), OptionalBuild => improved_slice_patterns::match_vec!(args; // fold/build fusion - [_, WHNF::AppliedBuiltin(OptionalFold, args)] => { + [_, Value::AppliedBuiltin(OptionalFold, args)] => { let mut args = args; if args.len() >= 2 { args.remove(1) @@ -161,13 +181,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { } }, [t, g] => g - .app(WHNF::from_builtin(Optional).app(t.clone())) - .app(OptionalSomeClosure(Now::from_whnf(t.clone()))) - .app(EmptyOptionalLit(Now::from_whnf(t))), + .app(Value::from_builtin(Optional).app(t.clone())) + .app(OptionalSomeClosure(TypeThunk::from_whnf(t.clone()))) + .app(EmptyOptionalLit(TypeThunk::from_whnf(t))), ), OptionalFold => improved_slice_patterns::match_vec!(args; // fold/build fusion - [_, WHNF::AppliedBuiltin(OptionalBuild, args)] => { + [_, Value::AppliedBuiltin(OptionalBuild, args)] => { let mut args = args; if args.len() >= 2 { args.remove(1) @@ -179,12 +199,12 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { nothing }, [_, NEOptionalLit(x), _, just, _] => { - just.app(x.normalize()) + just.app_thunk(x) } ), NaturalBuild => improved_slice_patterns::match_vec!(args; // fold/build fusion - [WHNF::AppliedBuiltin(NaturalFold, args)] => { + [Value::AppliedBuiltin(NaturalFold, args)] => { let mut args = args; if args.len() >= 1 { args.remove(0) @@ -193,13 +213,13 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { } }, [g] => g - .app(WHNF::from_builtin(Natural)) + .app(Value::from_builtin(Natural)) .app(NaturalSuccClosure) .app(NaturalLit(0)), ), NaturalFold => improved_slice_patterns::match_vec!(args; // fold/build fusion - [WHNF::AppliedBuiltin(NaturalBuild, args)] => { + [Value::AppliedBuiltin(NaturalBuild, args)] => { let mut args = args; if args.len() >= 1 { args.remove(0) @@ -209,7 +229,7 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { }, [NaturalLit(0), _, _, zero] => zero, [NaturalLit(n), t, succ, zero] => { - let fold = WHNF::from_builtin(NaturalFold) + let fold = Value::from_builtin(NaturalFold) .app(NaturalLit(n - 1)) .app(t) .app(succ.clone()) @@ -228,222 +248,233 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { #[derive(Debug, Clone)] enum EnvItem { - Expr(WHNF), - Skip(usize), + Thunk(Thunk), + Skip(V<Label>), +} + +impl EnvItem { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { + use EnvItem::*; + match self { + Thunk(e) => Thunk(e.shift(delta, var)), + Skip(v) => Skip(v.shift(delta, var)), + } + } + + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { + match self { + EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)), + EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()), + EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)), + } + } } #[derive(Debug, Clone)] -struct NormalizationContext(Rc<Context<Label, EnvItem>>); +pub(crate) struct NormalizationContext(Rc<Context<Label, EnvItem>>); impl NormalizationContext { - fn new() -> Self { + pub(crate) fn new() -> Self { NormalizationContext(Rc::new(Context::new())) } - fn insert(&self, x: &Label, e: WHNF) -> Self { + fn insert(&self, x: &Label, e: Thunk) -> Self { NormalizationContext(Rc::new( - self.0.insert(x.clone(), EnvItem::Expr(e)), + self.0.insert(x.clone(), EnvItem::Thunk(e)), )) } fn skip(&self, x: &Label) -> Self { NormalizationContext(Rc::new( self.0 - .map(|l, e| { - use EnvItem::*; - match e { - Expr(e) => { - let mut e = e.clone(); - e.shift0(1, x); - Expr(e) - } - Skip(n) if l == x => Skip(*n + 1), - Skip(n) => Skip(*n), - } - }) - .insert(x.clone(), EnvItem::Skip(0)), + .map(|_, e| e.shift(1, &x.into())) + .insert(x.clone(), EnvItem::Skip(x.into())), )) } - fn lookup(&self, var: &V<Label>) -> WHNF { + fn lookup(&self, var: &V<Label>) -> Value { let V(x, n) = var; match self.0.lookup(x, *n) { - Some(EnvItem::Expr(e)) => e.clone(), - Some(EnvItem::Skip(m)) => { - WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m)))) + Some(EnvItem::Thunk(t)) => t.normalize_whnf().clone(), + Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()), + None => Value::Var(var.clone()), + } + } + pub(crate) fn from_typecheck_ctx( + tc_ctx: &crate::typecheck::TypecheckContext, + ) -> Self { + use crate::typecheck::EnvItem::*; + let mut ctx = Context::new(); + for (k, vs) in tc_ctx.0.iter_keys() { + for v in vs.iter() { + let new_item = match v { + Type(var, _) => EnvItem::Skip(var.clone()), + Value(e) => EnvItem::Thunk(Thunk::new( + NormalizationContext::new(), + e.as_expr().embed_absurd(), + )), + }; + ctx = ctx.insert(k.clone(), new_item); } - None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))), } + NormalizationContext(Rc::new(ctx)) + } + + fn shift(&self, delta: isize, var: &V<Label>) -> Self { + NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var)))) + } + + fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { + NormalizationContext(Rc::new( + self.0.map(|_, e| e.subst_shift(var, val)), + )) } } -/// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should -/// be limited to syntactic expressions: either written by the user or meant to be printed. -/// The rule is the following: we must _not_ construct values of type `Expr` while normalizing, -/// but only construct `WHNF`s. -/// -/// WHNFs store subexpressions unnormalized, to enable lazy normalization. They approximate -/// what's called Weak Head Normal-Form (WHNF). This means that the expression is normalized as -/// little as possible, but just enough to know the first constructor of the normal form. This is -/// identical to full normalization for simple types like integers, but for e.g. a record literal -/// this means knowing just the field names. -/// -/// Each variant captures the relevant contexts when it is constructed. Conceptually each -/// subexpression has its own context, but in practice some contexts can be shared when sensible, to -/// avoid unnecessary allocations. +/// A semantic value. #[derive(Debug, Clone)] -enum WHNF { +pub(crate) enum Value { /// Closures - Lam(Label, Now, (NormalizationContext, InputSubExpr)), - AppliedBuiltin(Builtin, Vec<WHNF>), + Lam(Label, Thunk, Thunk), + AppliedBuiltin(Builtin, Vec<Value>), /// `λ(x: a) -> Some x` - OptionalSomeClosure(Now), + OptionalSomeClosure(TypeThunk), /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(Now, Option<Now>), + ListConsClosure(TypeThunk, Option<Thunk>), /// `λ(x : Natural) -> x + 1` NaturalSuccClosure, + Pi(Label, TypeThunk, TypeThunk), + Var(V<Label>), + Const(Const), BoolLit(bool), NaturalLit(Natural), IntegerLit(Integer), - EmptyOptionalLit(Now), - NEOptionalLit(Now), - EmptyListLit(Now), - NEListLit(Vec<Now>), - RecordLit(BTreeMap<Label, Now>), - RecordType(BTreeMap<Label, Now>), - UnionType(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>), - UnionConstructor( - NormalizationContext, - Label, - BTreeMap<Label, Option<InputSubExpr>>, - ), - UnionLit( - Label, - Now, - (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>), - ), - TextLit(Vec<InterpolatedTextContents<Now>>), + EmptyOptionalLit(TypeThunk), + NEOptionalLit(Thunk), + EmptyListLit(TypeThunk), + NEListLit(Vec<Thunk>), + RecordLit(BTreeMap<Label, Thunk>), + RecordType(BTreeMap<Label, TypeThunk>), + UnionType(BTreeMap<Label, Option<TypeThunk>>), + UnionConstructor(Label, BTreeMap<Label, Option<TypeThunk>>), + UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>), + TextLit(Vec<InterpolatedTextContents<Thunk>>), + /// Invariant: This must not contain a value captured by one of the variants above. + PartialExpr(Box<ExprF<Value, Label, X, X>>), Expr(OutputSubExpr), } -impl WHNF { +impl Value { + pub(crate) fn into_thunk(self) -> Thunk { + Thunk::from_whnf(self) + } + /// Convert the value back to a (normalized) syntactic expression - fn normalize_to_expr(self) -> OutputSubExpr { + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { match self { - WHNF::Lam(x, t, (ctx, e)) => { - let ctx2 = ctx.skip(&x); - rc(ExprF::Lam( - x.clone(), - t.normalize().normalize_to_expr(), - normalize_whnf(ctx2, e).normalize_to_expr(), - )) - } - WHNF::AppliedBuiltin(b, args) => { - let mut e = WHNF::Expr(rc(ExprF::Builtin(b))); + Value::Lam(x, t, e) => rc(ExprF::Lam( + x.clone(), + t.normalize_to_expr(), + e.normalize_to_expr(), + )), + Value::AppliedBuiltin(b, args) => { + let mut e = rc(ExprF::Builtin(*b)); for v in args { - e = e.app(v); + e = rc(ExprF::App(e, v.normalize_to_expr())); } - e.normalize_to_expr() + e } - WHNF::OptionalSomeClosure(n) => { - let a = n.normalize().normalize_to_expr(); + Value::OptionalSomeClosure(n) => { + let a = n.normalize_to_expr(); dhall::subexpr!(λ(x: a) -> Some x) } - WHNF::ListConsClosure(n, None) => { - let a = n.normalize().normalize_to_expr(); + Value::ListConsClosure(n, None) => { + let a = n.normalize_to_expr(); // Avoid accidental capture of the new `x` variable - let a1 = shift0(1, &"x".into(), &a); + let a1 = a.shift(1, &Label::from("x").into()); dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs) } - WHNF::ListConsClosure(n, Some(v)) => { - let v = v.normalize().normalize_to_expr(); - let a = n.normalize().normalize_to_expr(); + Value::ListConsClosure(n, Some(v)) => { + let v = v.normalize_to_expr(); + let a = n.normalize_to_expr(); + // Avoid accidental capture of the new `xs` variable + let v = v.shift(1, &Label::from("xs").into()); dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) } - WHNF::NaturalSuccClosure => { + Value::NaturalSuccClosure => { dhall::subexpr!(λ(x : Natural) -> x + 1) } - WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)), - WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)), - WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)), - WHNF::EmptyOptionalLit(n) => { - WHNF::Expr(rc(ExprF::Builtin(Builtin::OptionalNone))) - .app(n.normalize()) - .normalize_to_expr() - } - WHNF::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.normalize().normalize_to_expr())) + Value::Pi(x, t, e) => rc(ExprF::Pi( + x.clone(), + t.normalize_to_expr(), + e.normalize_to_expr(), + )), + Value::Var(v) => rc(ExprF::Var(v.clone())), + 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::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.normalize_to_expr(), + )), + Value::NEOptionalLit(n) => { + rc(ExprF::SomeLit(n.normalize_to_expr())) } - WHNF::EmptyListLit(n) => { - rc(ExprF::EmptyListLit(n.normalize().normalize_to_expr())) + Value::EmptyListLit(n) => { + rc(ExprF::EmptyListLit(n.normalize_to_expr())) } - WHNF::NEListLit(elts) => rc(ExprF::NEListLit( - elts.into_iter() - .map(|n| n.normalize().normalize_to_expr()) - .collect(), + Value::NEListLit(elts) => rc(ExprF::NEListLit( + elts.into_iter().map(|n| n.normalize_to_expr()).collect(), )), - WHNF::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.into_iter() - .map(|(k, v)| (k, v.normalize().normalize_to_expr())) + Value::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.normalize_to_expr())) .collect(), )), - WHNF::RecordType(kts) => rc(ExprF::RecordType( - kts.into_iter() - .map(|(k, v)| (k, v.normalize().normalize_to_expr())) + Value::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.normalize_to_expr())) .collect(), )), - WHNF::UnionType(ctx, kts) => rc(ExprF::UnionType( - kts.into_iter() + Value::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() .map(|(k, v)| { - ( - k, - v.map(|v| { - normalize_whnf(ctx.clone(), v) - .normalize_to_expr() - }), - ) + (k.clone(), v.as_ref().map(|v| v.normalize_to_expr())) }) .collect(), )), - WHNF::UnionConstructor(ctx, l, kts) => { + Value::UnionConstructor(l, kts) => { let kts = kts - .into_iter() + .iter() .map(|(k, v)| { - ( - k, - v.map(|v| { - normalize_whnf(ctx.clone(), v) - .normalize_to_expr() - }), - ) + (k.clone(), v.as_ref().map(|v| v.normalize_to_expr())) }) .collect(); - rc(ExprF::Field(rc(ExprF::UnionType(kts)), l)) + rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } - WHNF::UnionLit(l, v, (kts_ctx, kts)) => rc(ExprF::UnionLit( - l, - v.normalize().normalize_to_expr(), - kts.into_iter() + Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit( + l.clone(), + v.normalize_to_expr(), + kts.iter() .map(|(k, v)| { - ( - k, - v.map(|v| { - normalize_whnf(kts_ctx.clone(), v) - .normalize_to_expr() - }), - ) + (k.clone(), v.as_ref().map(|v| v.normalize_to_expr())) }) .collect(), )), - WHNF::TextLit(elts) => { + Value::TextLit(elts) => { fn normalize_textlit( - elts: Vec<InterpolatedTextContents<Now>>, + elts: &Vec<InterpolatedTextContents<Thunk>>, ) -> InterpolatedText<OutputSubExpr> { - elts.into_iter() + elts.iter() .flat_map(|contents| { use InterpolatedTextContents::{Expr, Text}; let new_interpolated = match contents { - Expr(n) => match n.normalize() { - WHNF::TextLit(elts2) => { + Expr(n) => match &*n.normalize_nf() { + Value::TextLit(elts2) => { normalize_textlit(elts2) } e => InterpolatedText::from(( @@ -454,7 +485,7 @@ impl WHNF { )], )), }, - Text(s) => InterpolatedText::from(s), + Text(s) => InterpolatedText::from(s.clone()), }; new_interpolated.into_iter() }) @@ -463,197 +494,776 @@ impl WHNF { rc(ExprF::TextLit(normalize_textlit(elts))) } - WHNF::Expr(e) => e, + Value::PartialExpr(e) => { + rc(e.map_ref_simple(|v| v.normalize_to_expr())) + } + Value::Expr(e) => e.clone(), } } - /// Apply to a value - fn app(self, val: WHNF) -> WHNF { - match (self, val) { - (WHNF::Lam(x, _, (ctx, e)), val) => { - let ctx2 = ctx.insert(&x, val); - normalize_whnf(ctx2, e) - } - (WHNF::AppliedBuiltin(b, mut args), val) => { - args.push(val); - apply_builtin(b, args) - } - (WHNF::OptionalSomeClosure(_), val) => { - WHNF::NEOptionalLit(Now::from_whnf(val)) - } - (WHNF::ListConsClosure(t, None), val) => { - WHNF::ListConsClosure(t, Some(Now::from_whnf(val))) + // Deprecated + pub(crate) fn normalize(&self) -> Value { + match self { + Value::Lam(x, t, e) => { + Value::Lam(x.clone(), t.normalize(), e.normalize()) } - (WHNF::ListConsClosure(_, Some(x)), WHNF::EmptyListLit(_)) => { - WHNF::NEListLit(vec![x]) + Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( + *b, + args.iter().map(|v| v.normalize()).collect(), + ), + Value::NaturalSuccClosure => Value::NaturalSuccClosure, + Value::OptionalSomeClosure(tth) => { + Value::OptionalSomeClosure(tth.normalize()) } - (WHNF::ListConsClosure(_, Some(x)), WHNF::NEListLit(mut xs)) => { - xs.insert(0, x); - WHNF::NEListLit(xs) + Value::ListConsClosure(t, v) => Value::ListConsClosure( + t.normalize(), + v.as_ref().map(|v| v.normalize()), + ), + Value::Pi(x, t, e) => { + Value::Pi(x.clone(), t.normalize(), e.normalize()) } - (WHNF::NaturalSuccClosure, WHNF::NaturalLit(n)) => { - WHNF::NaturalLit(n + 1) + Value::Var(v) => Value::Var(v.clone()), + 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::EmptyOptionalLit(tth) => { + Value::EmptyOptionalLit(tth.normalize()) } - (WHNF::UnionConstructor(ctx, l, kts), val) => { - WHNF::UnionLit(l, Now::from_whnf(val), (ctx, kts)) + Value::NEOptionalLit(th) => Value::NEOptionalLit(th.normalize()), + Value::EmptyListLit(tth) => Value::EmptyListLit(tth.normalize()), + Value::NEListLit(elts) => { + Value::NEListLit(elts.iter().map(|v| v.normalize()).collect()) } - // Can't do anything useful, convert to expr - (f, a) => WHNF::Expr(rc(ExprF::App( - f.normalize_to_expr(), - a.normalize_to_expr(), - ))), + Value::RecordLit(kvs) => Value::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.normalize())) + .collect(), + ), + Value::RecordType(kvs) => Value::RecordType( + kvs.iter() + .map(|(k, v)| (k.clone(), v.normalize())) + .collect(), + ), + Value::UnionType(kts) => Value::UnionType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.normalize())) + }) + .collect(), + ), + Value::UnionConstructor(x, kts) => Value::UnionConstructor( + x.clone(), + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.normalize())) + }) + .collect(), + ), + Value::UnionLit(x, v, kts) => Value::UnionLit( + x.clone(), + v.normalize(), + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.normalize())) + }) + .collect(), + ), + Value::TextLit(elts) => Value::TextLit( + elts.iter() + .map(|contents| { + use InterpolatedTextContents::{Expr, Text}; + match contents { + Expr(th) => Expr(th.normalize()), + Text(s) => Text(s.clone()), + } + }) + .collect(), + ), + Value::PartialExpr(e) => Value::PartialExpr(Box::new( + e.map_ref_simple(|v| v.normalize()), + )), + Value::Expr(e) => Value::Expr(e.clone()), } } - fn from_builtin(b: Builtin) -> WHNF { - WHNF::AppliedBuiltin(b, vec![]) - } - - fn shift0(&mut self, delta: isize, label: &Label) { + pub(crate) fn normalize_mut(&mut self) { match self { - WHNF::NaturalSuccClosure - | WHNF::BoolLit(_) - | WHNF::NaturalLit(_) - | WHNF::IntegerLit(_) => {} - WHNF::EmptyOptionalLit(n) - | WHNF::NEOptionalLit(n) - | WHNF::OptionalSomeClosure(n) - | WHNF::EmptyListLit(n) => { - n.shift0(delta, label); + Value::NaturalSuccClosure + | Value::Var(_) + | Value::Const(_) + | Value::BoolLit(_) + | Value::NaturalLit(_) + | Value::IntegerLit(_) + | Value::Expr(_) => {} + + Value::EmptyOptionalLit(tth) + | Value::OptionalSomeClosure(tth) + | Value::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + Value::NEOptionalLit(th) => { + th.normalize_mut(); + } + Value::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); } - WHNF::Lam(_, t, (_, e)) => { - t.shift0(delta, label); - shift_mut(delta, &V(label.clone(), 1), e); + Value::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); } - WHNF::AppliedBuiltin(_, args) => { + Value::AppliedBuiltin(_, args) => { for x in args.iter_mut() { - x.shift0(delta, label); + x.normalize_mut(); } } - WHNF::ListConsClosure(t, v) => { - t.shift0(delta, label); + Value::ListConsClosure(t, v) => { + t.normalize_mut(); for x in v.iter_mut() { - x.shift0(delta, label); + x.normalize_mut(); } } - WHNF::NEListLit(elts) => { + Value::NEListLit(elts) => { for x in elts.iter_mut() { - x.shift0(delta, label); + x.normalize_mut(); + } + } + Value::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); } } - WHNF::RecordLit(kvs) | WHNF::RecordType(kvs) => { + Value::RecordType(kvs) => { for x in kvs.values_mut() { - x.shift0(delta, label); + x.normalize_mut(); } } - WHNF::UnionType(_, kts) | WHNF::UnionConstructor(_, _, kts) => { + Value::UnionType(kts) | Value::UnionConstructor(_, kts) => { for x in kts.values_mut().flat_map(|opt| opt) { - shift0_mut(delta, label, x); + x.normalize_mut(); } } - WHNF::UnionLit(_, v, (_, kts)) => { - v.shift0(delta, label); + Value::UnionLit(_, v, kts) => { + v.normalize_mut(); for x in kts.values_mut().flat_map(|opt| opt) { - shift0_mut(delta, label, x); + x.normalize_mut(); } } - WHNF::TextLit(elts) => { + Value::TextLit(elts) => { for x in elts.iter_mut() { use InterpolatedTextContents::{Expr, Text}; match x { - Expr(n) => n.shift0(delta, label), + Expr(n) => n.normalize_mut(), Text(_) => {} } } } - WHNF::Expr(e) => shift0_mut(delta, label, e), + Value::PartialExpr(e) => { + // TODO: need map_mut_simple + *self = Value::PartialExpr(Box::new( + e.map_ref_simple(|v| v.normalize()), + )) + } + } + } + + /// Apply to a value + pub(crate) fn app(self, val: Value) -> Value { + self.app_thunk(val.into_thunk()) + } + + /// Apply to a thunk + pub(crate) fn app_thunk(self, th: Thunk) -> Value { + let fallback = |f: Value, a: Thunk| { + Value::PartialExpr(Box::new(ExprF::App( + f, + a.normalize_whnf().clone(), + ))) + }; + + match self { + Value::Lam(x, _, e) => { + let val = Typed( + TypedInternal::Value(th, None), + std::marker::PhantomData, + ); + e.subst_shift(&V(x, 0), &val).normalize_whnf().clone() + } + Value::AppliedBuiltin(b, mut args) => { + args.push(th.normalize_whnf().clone()); + apply_builtin(b, args) + } + Value::OptionalSomeClosure(_) => Value::NEOptionalLit(th), + Value::ListConsClosure(t, None) => { + Value::ListConsClosure(t, Some(th)) + } + Value::ListConsClosure(t, Some(x)) => { + let v = th.normalize_whnf(); + match &*v { + Value::EmptyListLit(_) => Value::NEListLit(vec![x]), + Value::NEListLit(xs) => { + let mut xs = xs.clone(); + xs.insert(0, x); + Value::NEListLit(xs) + } + _ => { + drop(v); + fallback(Value::ListConsClosure(t, Some(x)), th) + } + } + } + Value::NaturalSuccClosure => { + let v = th.normalize_whnf(); + match &*v { + Value::NaturalLit(n) => Value::NaturalLit(n + 1), + _ => { + drop(v); + fallback(Value::NaturalSuccClosure, th) + } + } + } + Value::UnionConstructor(l, kts) => Value::UnionLit(l, th, kts), + f => fallback(f, th), + } + } + + pub(crate) fn from_builtin(b: Builtin) -> Value { + Value::AppliedBuiltin(b, vec![]) + } + + fn shift(&self, delta: isize, var: &V<Label>) -> Self { + match self { + Value::Lam(x, t, e) => Value::Lam( + x.clone(), + t.shift(delta, var), + e.shift(delta, &var.shift(1, &x.into())), + ), + Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( + *b, + args.iter().map(|v| v.shift(delta, var)).collect(), + ), + Value::NaturalSuccClosure => Value::NaturalSuccClosure, + Value::OptionalSomeClosure(tth) => { + Value::OptionalSomeClosure(tth.shift(delta, var)) + } + Value::ListConsClosure(t, v) => Value::ListConsClosure( + t.shift(delta, var), + v.as_ref().map(|v| v.shift(delta, var)), + ), + Value::Pi(x, t, e) => Value::Pi( + x.clone(), + t.shift(delta, var), + e.shift(delta, &var.shift(1, &x.into())), + ), + 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::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| v.shift(delta, var)).collect(), + ), + Value::RecordLit(kvs) => Value::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.shift(delta, var))) + .collect(), + ), + Value::RecordType(kvs) => Value::RecordType( + kvs.iter() + .map(|(k, v)| (k.clone(), v.shift(delta, var))) + .collect(), + ), + Value::UnionType(kts) => Value::UnionType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.shift(delta, var))) + }) + .collect(), + ), + Value::UnionConstructor(x, kts) => Value::UnionConstructor( + x.clone(), + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.shift(delta, var))) + }) + .collect(), + ), + Value::UnionLit(x, v, kts) => Value::UnionLit( + x.clone(), + v.shift(delta, var), + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.shift(delta, var))) + }) + .collect(), + ), + Value::TextLit(elts) => Value::TextLit( + elts.iter() + .map(|contents| { + use InterpolatedTextContents::{Expr, Text}; + match contents { + Expr(th) => Expr(th.shift(delta, var)), + Text(s) => Text(s.clone()), + } + }) + .collect(), + ), + Value::PartialExpr(e) => Value::PartialExpr(Box::new( + e.map_ref_with_special_handling_of_binders( + |v| v.shift(delta, var), + |x, v| v.shift(delta, &var.shift(1, &x.into())), + X::clone, + X::clone, + Label::clone, + ), + )), + Value::Expr(e) => Value::Expr(e.shift(delta, var)), + } + } + + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { + match self { + Value::Lam(x, t, e) => Value::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ), + ), + Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( + *b, + args.iter().map(|v| v.subst_shift(var, val)).collect(), + ), + Value::NaturalSuccClosure => Value::NaturalSuccClosure, + Value::OptionalSomeClosure(tth) => { + Value::OptionalSomeClosure(tth.subst_shift(var, val)) + } + Value::ListConsClosure(t, v) => Value::ListConsClosure( + t.subst_shift(var, val), + v.as_ref().map(|v| v.subst_shift(var, val)), + ), + Value::Pi(x, t, e) => Value::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ), + ), + Value::Var(v) if v == var => val.to_value().clone(), + Value::Var(v) => Value::Var(v.shift(-1, 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::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::TextLit(elts) => Value::TextLit( + elts.iter() + .map(|contents| { + use InterpolatedTextContents::{Expr, Text}; + match contents { + Expr(th) => Expr(th.subst_shift(var, val)), + Text(s) => Text(s.clone()), + } + }) + .collect(), + ), + Value::PartialExpr(e) => Value::PartialExpr(Box::new( + e.map_ref_with_special_handling_of_binders( + |v| v.subst_shift(var, val), + |x, v| { + v.subst_shift( + &var.shift(1, &x.into()), + &val.shift(1, &x.into()), + ) + }, + X::clone, + X::clone, + Label::clone, + ), + )), + Value::Expr(e) => Value::Expr( + e.subst_shift(var, &val.clone().normalize().as_expr()), + ), + } + } +} + +mod thunk { + use super::{ + normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr, + Value, + }; + use crate::expr::Typed; + use dhall_core::{Label, V}; + use std::cell::{Ref, RefCell}; + use std::rc::Rc; + + #[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. + /// Invariant: if the marker is `NF`, the value must be fully normalized + Value(Marker, Value), + } + + /// Stores a possibl unevaluated value. Uses RefCell to ensure that + /// the value gets normalized at most once. + #[derive(Debug, Clone)] + pub struct Thunk(Rc<RefCell<ThunkInternal>>); + + 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()), + ) + } + // Already at least in WHNF + ThunkInternal::Value(_, _) => {} + } + } + + fn normalize_nf(&mut self) { + self.normalize_whnf(); + match self { + ThunkInternal::Unnormalized(_, _) => unreachable!(), + 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(_, _) => unreachable!(), + ThunkInternal::Value(_, v) => v, + } + } + + // Always use normalize_nf before + fn as_nf(&self) -> &Value { + match self { + ThunkInternal::Unnormalized(_, _) => unreachable!(), + ThunkInternal::Value(WHNF, _) => unreachable!(), + ThunkInternal::Value(NF, v) => v, + } + } + + fn shift(&self, delta: isize, var: &V<Label>) -> Self { + match self { + ThunkInternal::Unnormalized(ctx, e) => { + ThunkInternal::Unnormalized( + ctx.shift(delta, var), + e.clone(), + ) + } + ThunkInternal::Value(m, v) => { + ThunkInternal::Value(*m, v.shift(delta, var)) + } + } + } + + fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { + match self { + ThunkInternal::Unnormalized(ctx, e) => { + ThunkInternal::Unnormalized( + ctx.subst_shift(var, val), + e.clone(), + ) + } + ThunkInternal::Value(_, v) => { + // The resulting value may not stay in normal form after substitution + ThunkInternal::Value(WHNF, v.subst_shift(var, val)) + } + } + } + } + + impl Thunk { + pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { + ThunkInternal::Unnormalized(ctx, e).into_thunk() + } + + pub(crate) fn from_whnf(v: Value) -> Thunk { + ThunkInternal::Value(WHNF, v).into_thunk() + } + + pub(crate) fn from_normalized_expr(e: OutputSubExpr) -> Thunk { + Thunk::new(NormalizationContext::new(), e.embed_absurd()) + } + + // Deprecated + pub(crate) fn normalize(&self) -> Thunk { + self.normalize_nf(); + self.clone() + } + + // 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(), + } + } + + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you will run into BorrowMut panics + pub(crate) fn normalize_whnf(&self) -> Ref<Value> { + self.0.borrow_mut().normalize_whnf(); + Ref::map(self.0.borrow(), ThunkInternal::as_whnf) + } + + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you will run into BorrowMut panics + pub(crate) fn normalize_nf(&self) -> Ref<Value> { + self.0.borrow_mut().normalize_nf(); + Ref::map(self.0.borrow(), ThunkInternal::as_nf) + } + + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr() + } + + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { + self.0.borrow().shift(delta, var).into_thunk() + } + + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { + self.0.borrow().subst_shift(var, val).into_thunk() } } } -/// Normalize-on-write smart container. Contains either a (partially) normalized value or a -/// non-normalized value alongside a normalization context. -/// The name is a pun on std::borrow::Cow. +pub(crate) use thunk::Thunk; + +/// A thunk in type position. #[derive(Debug, Clone)] -enum Now { - Normalized(Box<WHNF>), - Unnormalized(NormalizationContext, InputSubExpr), +pub(crate) enum TypeThunk { + Thunk(Thunk), + Type(Type<'static>), } -impl Now { - fn new(ctx: NormalizationContext, e: InputSubExpr) -> Now { - Now::Unnormalized(ctx, e) +impl TypeThunk { + fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk { + TypeThunk::from_thunk(Thunk::new(ctx, e)) + } + + fn from_whnf(v: Value) -> TypeThunk { + TypeThunk::from_thunk(Thunk::from_whnf(v)) + } + + fn from_thunk(th: Thunk) -> TypeThunk { + TypeThunk::Thunk(th) + } + + pub(crate) fn from_type(t: Type<'static>) -> TypeThunk { + TypeThunk::Type(t) + } + + // Deprecated + fn normalize(&self) -> TypeThunk { + match self { + TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()), + TypeThunk::Type(t) => TypeThunk::Type(t.clone()), + } + } + + fn normalize_mut(&mut self) { + match self { + TypeThunk::Thunk(th) => th.normalize_mut(), + TypeThunk::Type(_) => {} + } + } + + pub(crate) fn normalize_nf(&self) -> Value { + match self { + TypeThunk::Thunk(th) => th.normalize_nf().clone(), + TypeThunk::Type(t) => t.to_value().normalize(), + } } - fn from_whnf(v: WHNF) -> Now { - Now::Normalized(Box::new(v)) + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr() } - fn normalize(self) -> WHNF { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { match self { - Now::Normalized(v) => *v, - Now::Unnormalized(ctx, e) => normalize_whnf(ctx, e), + TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)), + TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)), } } - fn shift0(&mut self, delta: isize, label: &Label) { + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { match self { - Now::Normalized(v) => v.shift0(delta, label), - Now::Unnormalized(_, e) => shift0_mut(delta, label, e), + TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)), + TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)), } } } -/// Reduces the imput expression to WHNF. See doc on `WHNF` for details. -fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF { +/// Reduces the imput expression to Value. See doc on `Value` for details. +fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { match expr.as_ref() { ExprF::Var(v) => ctx.lookup(&v), ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()), ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()), - // TODO: wasteful to retraverse everything - ExprF::Embed(e) => normalize_whnf(ctx, e.0.embed_absurd()), + ExprF::Embed(e) => e.to_value(), ExprF::Let(x, _, r, b) => { - let r = normalize_whnf(ctx.clone(), r.clone()); - normalize_whnf(ctx.insert(x, r), b.clone()) + let t = Thunk::new(ctx.clone(), r.clone()); + normalize_whnf(ctx.insert(x, t), b.clone()) } - ExprF::Lam(x, t, e) => WHNF::Lam( + ExprF::Lam(x, t, e) => Value::Lam( x.clone(), - Now::new(ctx.clone(), t.clone()), - (ctx, e.clone()), + Thunk::new(ctx.clone(), t.clone()), + Thunk::new(ctx.skip(x), e.clone()), ), - ExprF::Builtin(b) => WHNF::AppliedBuiltin(*b, vec![]), - ExprF::BoolLit(b) => WHNF::BoolLit(*b), - ExprF::NaturalLit(n) => WHNF::NaturalLit(*n), + ExprF::Builtin(b) => Value::from_builtin(*b), + ExprF::Const(c) => Value::Const(*c), + ExprF::BoolLit(b) => Value::BoolLit(*b), + ExprF::NaturalLit(n) => Value::NaturalLit(*n), ExprF::OldOptionalLit(None, e) => { - WHNF::EmptyOptionalLit(Now::new(ctx, e.clone())) + Value::EmptyOptionalLit(TypeThunk::new(ctx, e.clone())) } ExprF::OldOptionalLit(Some(e), _) => { - WHNF::NEOptionalLit(Now::new(ctx, e.clone())) + Value::NEOptionalLit(Thunk::new(ctx, e.clone())) + } + ExprF::SomeLit(e) => Value::NEOptionalLit(Thunk::new(ctx, e.clone())), + ExprF::EmptyListLit(e) => { + Value::EmptyListLit(TypeThunk::new(ctx, e.clone())) } - ExprF::SomeLit(e) => WHNF::NEOptionalLit(Now::new(ctx, e.clone())), - ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())), - ExprF::NEListLit(elts) => WHNF::NEListLit( + ExprF::NEListLit(elts) => Value::NEListLit( elts.iter() - .map(|e| Now::new(ctx.clone(), e.clone())) + .map(|e| Thunk::new(ctx.clone(), e.clone())) .collect(), ), - ExprF::RecordLit(kvs) => WHNF::RecordLit( + ExprF::RecordLit(kvs) => Value::RecordLit( kvs.iter() - .map(|(k, e)| (k.clone(), Now::new(ctx.clone(), e.clone()))) + .map(|(k, e)| (k.clone(), Thunk::new(ctx.clone(), e.clone()))) .collect(), ), - ExprF::UnionType(kvs) => WHNF::UnionType(ctx, kvs.clone()), - ExprF::UnionLit(l, x, kts) => WHNF::UnionLit( + ExprF::UnionType(kts) => Value::UnionType( + kts.iter() + .map(|(k, t)| { + ( + k.clone(), + t.as_ref() + .map(|t| TypeThunk::new(ctx.clone(), t.clone())), + ) + }) + .collect(), + ), + ExprF::UnionLit(l, x, kts) => Value::UnionLit( l.clone(), - Now::new(ctx.clone(), x.clone()), - (ctx, kts.clone()), + Thunk::new(ctx.clone(), x.clone()), + kts.iter() + .map(|(k, t)| { + ( + k.clone(), + t.as_ref() + .map(|t| TypeThunk::new(ctx.clone(), t.clone())), + ) + }) + .collect(), ), - ExprF::TextLit(elts) => WHNF::TextLit( + ExprF::TextLit(elts) => Value::TextLit( elts.iter() .map(|contents| { use InterpolatedTextContents::{Expr, Text}; match contents { - Expr(n) => Expr(Now::new(ctx.clone(), n.clone())), + Expr(n) => Expr(Thunk::new(ctx.clone(), n.clone())), Text(s) => Text(s.clone()), } }) @@ -662,13 +1272,13 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF { ExprF::BoolIf(b, e1, e2) => { let b = normalize_whnf(ctx.clone(), b.clone()); match b { - WHNF::BoolLit(true) => normalize_whnf(ctx, e1.clone()), - WHNF::BoolLit(false) => normalize_whnf(ctx, e2.clone()), + Value::BoolLit(true) => normalize_whnf(ctx, e1.clone()), + Value::BoolLit(false) => normalize_whnf(ctx, e2.clone()), b => { let e1 = normalize_whnf(ctx.clone(), e1.clone()); let e2 = normalize_whnf(ctx, e2.clone()); match (e1, e2) { - (WHNF::BoolLit(true), WHNF::BoolLit(false)) => b, + (Value::BoolLit(true), Value::BoolLit(false)) => b, (e1, e2) => { normalize_last_layer(ExprF::BoolIf(b, e1, e2)) } @@ -678,7 +1288,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF { } expr => { // Recursively normalize subexpressions - let expr: ExprF<WHNF, Label, X, X> = expr + let expr: ExprF<Value, Label, X, X> = expr .map_ref_with_special_handling_of_binders( |e| normalize_whnf(ctx.clone(), e.clone()), |x, e| normalize_whnf(ctx.skip(x), e.clone()), @@ -693,9 +1303,9 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF { } /// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer. -fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF { +fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value { use dhall_core::BinOp::*; - use WHNF::*; + use Value::*; match expr { ExprF::App(v, a) => v.app(a), @@ -741,9 +1351,9 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF { ExprF::BinOp(TextAppend, TextLit(x), y) if x.is_empty() => y, ExprF::BinOp(TextAppend, x, TextLit(y)) if y.is_empty() => x, - ExprF::Field(UnionType(ctx, kts), l) => UnionConstructor(ctx, l, kts), + ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts), ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) { - Some(r) => r.normalize(), + Some(r) => r.normalize_whnf().clone(), None => { // Couldn't do anything useful, so just normalize subexpressions Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l))) @@ -759,18 +1369,16 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF { ), ExprF::Merge(RecordLit(mut handlers), e, t) => { let e = match e { - UnionConstructor(ctor_ctx, l, kts) => match handlers.remove(&l) - { - Some(h) => return h.normalize(), - None => UnionConstructor(ctor_ctx, l, kts), + UnionConstructor(l, kts) => match handlers.remove(&l) { + Some(h) => return h.normalize_whnf().clone(), + None => UnionConstructor(l, kts), }, - UnionLit(l, v, (kts_ctx, kts)) => match handlers.remove(&l) { + UnionLit(l, v, kts) => match handlers.remove(&l) { Some(h) => { - let h = h.normalize(); - let v = v.normalize(); - return h.app(v); + let h = h.normalize_whnf().clone(); + return h.app_thunk(v); } - None => UnionLit(l, v, (kts_ctx, kts)), + None => UnionLit(l, v, kts), }, e => e, }; @@ -778,29 +1386,13 @@ fn normalize_last_layer(expr: ExprF<WHNF, Label, X, X>) -> WHNF { Expr(rc(ExprF::Merge( RecordLit(handlers).normalize_to_expr(), e.normalize_to_expr(), - t.map(WHNF::normalize_to_expr), + t.as_ref().map(Value::normalize_to_expr), ))) } - // Couldn't do anything useful, so just normalize subexpressions - expr => { - Expr(rc(expr.map_ref_simple(|e| e.clone().normalize_to_expr()))) - } + expr => PartialExpr(Box::new(expr)), } } -/// Reduce an expression to its normal form, performing beta reduction -/// -/// `normalize` does not type-check the expression. You may want to type-check -/// expressions before normalizing them since normalization can convert an -/// ill-typed expression into a well-typed expression. -/// -/// However, `normalize` will not fail if the expression is ill-typed and will -/// leave ill-typed sub-expressions unevaluated. -/// -fn normalize(e: InputSubExpr) -> OutputSubExpr { - normalize_whnf(NormalizationContext::new(), e).normalize_to_expr() -} - #[cfg(test)] mod spec_tests { #![rustfmt::skip] @@ -866,7 +1458,7 @@ mod spec_tests { norm!(success_prelude_List_head_1, "prelude/List/head/1"); norm!(success_prelude_List_indexed_0, "prelude/List/indexed/0"); norm!(success_prelude_List_indexed_1, "prelude/List/indexed/1"); - norm!(success_prelude_List_iterate_0, "prelude/List/iterate/0"); + // norm!(success_prelude_List_iterate_0, "prelude/List/iterate/0"); norm!(success_prelude_List_iterate_1, "prelude/List/iterate/1"); norm!(success_prelude_List_last_0, "prelude/List/last/0"); norm!(success_prelude_List_last_1, "prelude/List/last/1"); diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs index 196bda1..6f143cb 100644 --- a/dhall/src/serde.rs +++ b/dhall/src/serde.rs @@ -7,7 +7,7 @@ use std::borrow::Cow; impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T { fn from_str(s: &'a str, ty: Option<&Type>) -> Result<Self> { let expr = Normalized::from_str(s, ty)?; - T::deserialize(Deserializer(Cow::Owned(expr.0))) + T::deserialize(Deserializer(Cow::Owned(expr.to_expr()))) } } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 7f85b5c..ecd6e43 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -71,7 +71,7 @@ pub fn run_test_with_bigger_stack( ) -> std::result::Result<(), String> { // Many tests stack overflow in debug mode let base_path: String = base_path.to_string(); - stacker::grow(4 * 1024 * 1024, move || { + stacker::grow(6 * 1024 * 1024, move || { run_test(&base_path, feature, status) .map_err(|e| e.to_string()) .map(|_| ()) @@ -130,17 +130,16 @@ pub fn run_test( match feature { Parser => unreachable!(), Import => { - // Not sure whether to normalize or not - let expr = expr.skip_typecheck().skip_normalize(); + let expr = expr.skip_typecheck().normalize(); assert_eq_display!(expr, expected); } Typecheck => { - expr.typecheck_with(&expected.into_type())?; + expr.typecheck_with(&expected.to_type())?; } TypeInference => { let expr = expr.typecheck()?; - let ty = expr.get_type()?; - assert_eq_display!(ty.as_normalized()?.as_ref(), &expected); + let ty = expr.get_type()?.into_owned(); + assert_eq_display!(ty.to_normalized(), expected); } Normalization => { let expr = expr.skip_typecheck().normalize(); diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs index 43eb2ac..99ca5ee 100644 --- a/dhall/src/traits/deserialize.rs +++ b/dhall/src/traits/deserialize.rs @@ -48,6 +48,6 @@ impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> { impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> { fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> { - Ok(Normalized::from_str(s, ty)?.into_type()) + Ok(Normalized::from_str(s, ty)?.to_type()) } } diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index d4faf45..74c2e0a 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -1,7 +1,8 @@ use crate::expr::*; use crate::traits::StaticType; -use crate::typecheck::{type_of_const, TypeError, TypeMessage}; -use dhall_core::context::Context; +#[allow(unused_imports)] +use crate::typecheck::{TypeError, TypeMessage, TypecheckContext}; +#[allow(unused_imports)] use dhall_core::{Const, ExprF}; use std::borrow::Cow; @@ -17,40 +18,18 @@ impl<T: StaticType> DynamicType for T { impl<'a> DynamicType for Type<'a> { fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { - match &self.0 { - TypeInternal::Expr(e) => e.get_type(), - TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), - TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), - dhall_core::rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } + self.get_type() } } impl<'a> DynamicType for Normalized<'a> { fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { - match &self.1 { - Some(t) => Ok(Cow::Borrowed(t)), - None => Err(TypeError::new( - &Context::new(), - self.0.embed_absurd(), - TypeMessage::Untyped, - )), - } + self.0.get_type() } } impl<'a> DynamicType for Typed<'a> { fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { - match &self.1 { - Some(t) => Ok(Cow::Borrowed(t)), - None => Err(TypeError::new( - &Context::new(), - self.0.clone(), - TypeMessage::Untyped, - )), - } + self.0.get_type() } } diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index e92ce78..df6a177 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -33,17 +33,18 @@ pub trait SimpleStaticType { } fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> { - SimpleType(x, std::marker::PhantomData) + x.into() } impl<T: SimpleStaticType> StaticType for T { fn get_static_type() -> Type<'static> { - crate::expr::Normalized( - T::get_simple_static_type().into(), - Some(Type::const_type()), - std::marker::PhantomData, + crate::expr::Normalized::from_thunk_and_type( + crate::normalize::Thunk::from_normalized_expr( + T::get_simple_static_type().into(), + ), + Type::const_type(), ) - .into_type() + .to_type() } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index b26f845..78538aa 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,10 +1,11 @@ #![allow(non_snake_case)] use std::borrow::Borrow; use std::borrow::Cow; +use std::collections::BTreeMap; use std::fmt; -use std::marker::PhantomData; use crate::expr::*; +use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value}; use crate::traits::DynamicType; use dhall_core; use dhall_core::context::Context; @@ -22,94 +23,226 @@ impl<'a> Resolved<'a> { ty: &Type, ) -> Result<Typed<'static>, TypeError> { let expr: SubExpr<_, _> = self.0.unnote(); - let ty: SubExpr<_, _> = ty.clone().unnote().embed()?; - type_of(dhall::subexpr!(expr: ty)) + let ty: SubExpr<_, _> = ty.to_expr().embed_absurd(); + type_of(rc(ExprF::Annot(expr, ty))) } /// Pretends this expression has been typechecked. Use with care. #[allow(dead_code)] pub fn skip_typecheck(self) -> Typed<'a> { - Typed(self.0.unnote(), None, PhantomData) + Typed::from_thunk_untyped(Thunk::new( + NormalizationContext::new(), + self.0.unnote(), + )) } } + impl<'a> Typed<'a> { - fn get_type_move(self) -> Result<Type<'static>, TypeError> { - let (expr, ty) = (self.0, self.1); - ty.ok_or_else(|| { - TypeError::new(&Context::new(), expr, TypeMessage::Untyped) - }) + fn to_type(&self) -> Type<'a> { + match &self.to_value() { + Value::Const(c) => Type(TypeInternal::Const(*c)), + _ => Type(TypeInternal::Typed(Box::new(self.clone()))), + } } } + impl<'a> Normalized<'a> { - // Expose the outermost constructor - fn unroll_ref(&self) -> &Expr<X, X> { - self.as_expr().as_ref() + fn shift(&self, delta: isize, var: &V<Label>) -> Self { + Normalized(self.0.shift(delta, var), self.1) } - fn shift0(&self, delta: isize, label: &Label) -> Self { - // shift the type too ? - Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2) + pub(crate) fn to_type(self) -> Type<'a> { + self.0.to_type() } } -impl Normalized<'static> { - fn embed<N>(self) -> SubExpr<N, Normalized<'static>> { - rc(ExprF::Embed(self)) + +impl<'a> Type<'a> { + pub(crate) fn to_normalized(&self) -> Normalized<'a> { + self.0.to_normalized() + } + pub(crate) fn to_expr(&self) -> SubExpr<X, X> { + self.0.to_expr() + } + pub(crate) fn to_value(&self) -> Value { + self.0.to_value() + } + pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { + self.0.get_type() + } + fn as_const(&self) -> Option<Const> { + self.0.as_const() + } + fn internal(&self) -> &TypeInternal<'a> { + &self.0 + } + fn internal_whnf(&self) -> Option<Value> { + self.0.whnf() + } + pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { + Type(self.0.shift(delta, var)) + } + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &Typed<'static>, + ) -> Self { + Type(self.0.subst_shift(var, val)) + } + + fn const_sort() -> Self { + Type(TypeInternal::Const(Const::Sort)) + } + fn const_kind() -> Self { + Type(TypeInternal::Const(Const::Kind)) + } + pub(crate) fn const_type() -> Self { + Type(TypeInternal::Const(Const::Type)) } } -impl<'a> Type<'a> { - pub(crate) fn as_normalized( + +impl TypeThunk { + fn to_type( &self, - ) -> Result<Cow<Normalized<'a>>, TypeError> { - match &self.0 { - TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), - TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), - TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), - rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), + ctx: &TypecheckContext, + ) -> Result<Type<'static>, TypeError> { + match self { + TypeThunk::Type(t) => Ok(t.clone()), + TypeThunk::Thunk(th) => { + // TODO: rule out statically + mktype(ctx, th.normalize_to_expr().embed_absurd()) + } + } + } +} + +/// A semantic type. This is partially redundant with `dhall_core::Expr`, on purpose. `TypeInternal` should +/// be limited to syntactic expressions: either written by the user or meant to be printed. +/// The rule is the following: we must _not_ construct values of type `Expr` while typechecking, +/// but only construct `TypeInternal`s. +#[derive(Debug, Clone)] +pub(crate) enum TypeInternal<'a> { + Const(Const), + /// This must not contain a Const value. + Typed(Box<Typed<'a>>), +} + +impl<'a> TypeInternal<'a> { + fn to_typed(&self) -> Typed<'a> { + match self { + TypeInternal::Typed(e) => e.as_ref().clone(), + TypeInternal::Const(c) => const_to_typed(*c), } } - pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> { - match self.0 { - TypeInternal::Expr(e) => Ok(*e), - TypeInternal::Const(c) => Ok(const_to_normalized(c)), - TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), - rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), + fn to_normalized(&self) -> Normalized<'a> { + self.to_typed().normalize() + } + fn to_expr(&self) -> SubExpr<X, X> { + self.to_normalized().to_expr() + } + fn to_value(&self) -> Value { + self.to_typed().to_value().clone() + } + pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { + Ok(match self { + TypeInternal::Typed(e) => e.get_type()?, + TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?), + }) + } + fn as_const(&self) -> Option<Const> { + match self { + TypeInternal::Const(c) => Some(*c), + _ => None, } } - // Expose the outermost constructor - fn unroll_ref(&self) -> Result<Cow<Expr<X, X>>, TypeError> { - match self.as_normalized()? { - Cow::Borrowed(e) => Ok(Cow::Borrowed(e.unroll_ref())), - Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())), + fn whnf(&self) -> Option<Value> { + match self { + TypeInternal::Typed(e) => Some(e.to_value()), + _ => None, } } - fn shift0(&self, delta: isize, label: &Label) -> Self { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { use TypeInternal::*; - Type(match &self.0 { - Expr(e) => Expr(Box::new(e.shift0(delta, label))), + match self { + Typed(e) => Typed(Box::new(e.shift(delta, var))), Const(c) => Const(*c), - SuperType => SuperType, - }) + } + } + fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { + use TypeInternal::*; + match self { + Typed(e) => Typed(Box::new(e.subst_shift(var, val))), + Const(c) => Const(*c), + } } +} - fn const_sort() -> Self { - Type(TypeInternal::Const(Const::Sort)) +impl<'a> Eq for TypeInternal<'a> {} +impl<'a> PartialEq for TypeInternal<'a> { + fn eq(&self, other: &Self) -> bool { + self.to_normalized() == other.to_normalized() } - fn const_kind() -> Self { - Type(TypeInternal::Const(Const::Kind)) +} + +#[derive(Debug, Clone)] +pub(crate) enum EnvItem { + Type(V<Label>, Type<'static>), + Value(Normalized<'static>), +} + +impl EnvItem { + fn shift(&self, delta: isize, var: &V<Label>) -> Self { + use EnvItem::*; + match self { + Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)), + Value(e) => Value(e.shift(delta, var)), + } } - pub(crate) fn const_type() -> Self { - Type(TypeInternal::Const(Const::Type)) +} + +#[derive(Debug, Clone)] +pub(crate) struct TypecheckContext(pub(crate) Context<Label, EnvItem>); + +impl TypecheckContext { + pub(crate) fn new() -> Self { + TypecheckContext(Context::new()) + } + pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self { + TypecheckContext( + self.0.map(|_, e| e.shift(1, &x.into())).insert( + x.clone(), + EnvItem::Type(x.into(), t.shift(1, &x.into())), + ), + ) + } + pub(crate) fn insert_value( + &self, + x: &Label, + t: Normalized<'static>, + ) -> Self { + TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t))) + } + pub(crate) fn lookup( + &self, + var: &V<Label>, + ) -> Option<Cow<'_, Type<'static>>> { + let V(x, n) = var; + match self.0.lookup(x, *n) { + Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)), + Some(EnvItem::Value(t)) => Some(t.get_type()?), + None => None, + } + } + fn to_normalization_ctx(&self) -> NormalizationContext { + NormalizationContext::from_typecheck_ctx(self) } } -impl Type<'static> { - fn embed<N>(self) -> Result<SubExpr<N, Normalized<'static>>, TypeError> { - Ok(self.into_normalized()?.embed()) + +impl PartialEq for TypecheckContext { + fn eq(&self, _: &Self) -> bool { + // don't count contexts when comparing stuff + // this is dirty but needed for now + true } } +impl Eq for TypecheckContext {} fn function_check(a: Const, b: Const) -> Result<Const, ()> { use dhall_core::Const::*; @@ -192,38 +325,45 @@ where (_, _) => false, } } - match (&eL0.borrow().0, &eR0.borrow().0) { - (TypeInternal::SuperType, TypeInternal::SuperType) => true, - (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr, - (TypeInternal::Expr(l), TypeInternal::Expr(r)) => { + match (eL0.borrow().internal(), eR0.borrow().internal()) { + // (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr, + // (TypeInternal::Expr(l), TypeInternal::Expr(r)) => { + _ => { let mut ctx = vec![]; - go(&mut ctx, l.as_expr(), r.as_expr()) + go( + &mut ctx, + &eL0.borrow().to_expr(), + &eR0.borrow().to_expr(), + ) } - _ => false, + // _ => false, } } -fn const_to_normalized<'a>(c: Const) -> Normalized<'a> { - Normalized( - rc(ExprF::Const(c)), - Some(Type(match c { - Const::Type => TypeInternal::Const(Const::Kind), - Const::Kind => TypeInternal::Const(Const::Sort), - Const::Sort => TypeInternal::SuperType, - })), - PhantomData, - ) +fn const_to_typed<'a>(c: Const) -> Typed<'a> { + match c { + Const::Sort => Typed::const_sort(), + _ => Typed::from_thunk_and_type( + Value::Const(c).into_thunk(), + type_of_const(c).unwrap(), + ), + } } fn const_to_type<'a>(c: Const) -> Type<'a> { Type(TypeInternal::Const(c)) } -pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> { +fn type_of_const<'a>(c: Const) -> Result<Type<'a>, TypeError> { match c { - Const::Type => Type::const_kind(), - Const::Kind => Type::const_sort(), - Const::Sort => Type(TypeInternal::SuperType), + Const::Type => Ok(Type::const_kind()), + Const::Kind => Ok(Type::const_sort()), + Const::Sort => { + return Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Sort, + )) + } } } @@ -302,59 +442,198 @@ macro_rules! ensure_equal { }; } -// Do not use with Const because they will never match -macro_rules! ensure_matches { - ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => { - match $x.unroll_ref()? { - Cow::Borrowed(e) => match e { - $pat => $branch, - _ => return Err($err), - }, - // Can't pattern match because lifetimes - Cow::Owned(_) => return Err($err), - } - }; -} - // Ensure the provided type has type `Type` macro_rules! ensure_simple_type { ($x:expr, $err:expr $(,)*) => {{ - let k = ensure_is_const!($x.get_type()?, $err); - if k != Type { - return Err($err); + match $x.get_type()?.as_const() { + Some(dhall_core::Const::Type) => {} + _ => return Err($err), } }}; } -macro_rules! ensure_is_const { - ($x:expr, $err:expr $(,)*) => { - match $x.unroll_ref()?.as_ref() { - Const(k) => *k, - _ => return Err($err), - } - }; +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum TypeIntermediate { + Pi(TypecheckContext, Label, Type<'static>, Type<'static>), + RecordType(TypecheckContext, BTreeMap<Label, Type<'static>>), + UnionType(TypecheckContext, BTreeMap<Label, Option<Type<'static>>>), + ListType(TypecheckContext, Type<'static>), + OptionalType(TypecheckContext, Type<'static>), +} + +impl TypeIntermediate { + fn typecheck(self) -> Result<Typed<'static>, TypeError> { + let mkerr = |ctx, msg| TypeError::new(ctx, msg); + Ok(match &self { + TypeIntermediate::Pi(ctx, x, ta, tb) => { + let ctx2 = ctx.insert_type(x, ta.clone()); + + let kA = match ta.get_type()?.as_const() { + Some(k) => k, + _ => { + return Err(mkerr( + ctx, + InvalidInputType(ta.clone().to_normalized()), + )) + } + }; + + let kB = match tb.get_type()?.as_const() { + Some(k) => k, + _ => { + return Err(mkerr( + &ctx2, + InvalidOutputType( + tb.clone() + .to_normalized() + .get_type()? + .to_normalized(), + ), + )) + } + }; + + let k = match function_check(kA, kB) { + Ok(k) => k, + Err(()) => { + return Err(mkerr( + ctx, + NoDependentTypes( + ta.clone().to_normalized(), + tb.clone() + .to_normalized() + .get_type()? + .to_normalized(), + ), + )) + } + }; + + Typed::from_thunk_and_type( + Value::Pi( + x.clone(), + TypeThunk::from_type(ta.clone()), + TypeThunk::from_type(tb.clone()), + ) + .into_thunk(), + const_to_type(k), + ) + } + TypeIntermediate::RecordType(ctx, kts) => { + // Check that all types are the same const + let mut k = None; + for (x, t) in kts { + match (k, t.get_type()?.as_const()) { + (None, Some(k2)) => k = Some(k2), + (Some(k1), Some(k2)) if k1 == k2 => {} + _ => { + return Err(mkerr( + ctx, + InvalidFieldType(x.clone(), t.clone()), + )) + } + } + } + // An empty record type has type Type + let k = k.unwrap_or(dhall_core::Const::Type); + + Typed::from_thunk_and_type( + Value::RecordType( + kts.iter() + .map(|(k, t)| { + (k.clone(), TypeThunk::from_type(t.clone())) + }) + .collect(), + ) + .into_thunk(), + const_to_type(k), + ) + } + TypeIntermediate::UnionType(ctx, kts) => { + // Check that all types are the same const + let mut k = None; + for (x, t) in kts { + if let Some(t) = t { + match (k, t.get_type()?.as_const()) { + (None, Some(k2)) => k = Some(k2), + (Some(k1), Some(k2)) if k1 == k2 => {} + _ => { + return Err(mkerr( + ctx, + InvalidFieldType(x.clone(), t.clone()), + )) + } + } + } + } + + // An empty union type has type Type; + // an union type with only unary variants also has type Type + let k = k.unwrap_or(dhall_core::Const::Type); + + Typed::from_thunk_and_type( + Value::UnionType( + kts.iter() + .map(|(k, t)| { + ( + k.clone(), + t.as_ref().map(|t| { + TypeThunk::from_type(t.clone()) + }), + ) + }) + .collect(), + ) + .into_thunk(), + const_to_type(k), + ) + } + TypeIntermediate::ListType(ctx, t) => { + ensure_simple_type!( + t, + mkerr(ctx, InvalidListType(t.clone().to_normalized())), + ); + Typed::from_thunk_and_type( + Value::from_builtin(Builtin::List) + .app(t.to_value()) + .into_thunk(), + const_to_type(Const::Type), + ) + } + TypeIntermediate::OptionalType(ctx, t) => { + ensure_simple_type!( + t, + mkerr(ctx, InvalidOptionalType(t.clone().to_normalized())), + ); + Typed::from_thunk_and_type( + Value::from_builtin(Builtin::Optional) + .app(t.to_value()) + .into_thunk(), + const_to_type(Const::Type), + ) + } + }) + } } /// Takes an expression that is meant to contain a Type /// and turn it into a type, typechecking it along the way. fn mktype( - ctx: &Context<Label, Type<'static>>, + ctx: &TypecheckContext, e: SubExpr<X, Normalized<'static>>, ) -> Result<Type<'static>, TypeError> { - Ok(type_with(ctx, e)?.normalize().into_type()) -} - -fn into_simple_type<'a>(e: SubExpr<X, X>) -> Type<'a> { - SimpleType(e, PhantomData).into_type() + Ok(type_with(ctx, e)?.to_type()) } -fn simple_type_from_builtin<'a>(b: Builtin) -> Type<'a> { - into_simple_type(rc(ExprF::Builtin(b))) +fn builtin_to_type<'a>(b: Builtin) -> Result<Type<'a>, TypeError> { + mktype(&TypecheckContext::new(), rc(ExprF::Builtin(b))) } /// Intermediary return type enum Ret { - /// Returns the contained Type as is + /// Returns the contained value as is + RetTyped(Typed<'static>), + /// Use the contained Type as the type of the input expression RetType(Type<'static>), /// Returns an expression that must be typechecked and /// turned into a Type first. @@ -364,55 +643,32 @@ enum Ret { /// Type-check an expression and return the expression alongside its type if type-checking /// succeeded, or an error if type-checking failed fn type_with( - ctx: &Context<Label, Type<'static>>, + ctx: &TypecheckContext, e: SubExpr<X, Normalized<'static>>, ) -> Result<Typed<'static>, TypeError> { use dhall_core::ExprF::*; - let mkerr = |msg: TypeMessage<'static>| TypeError::new(ctx, e.clone(), msg); use Ret::*; let ret = match e.as_ref() { Lam(x, t, b) => { - let t = mktype(ctx, t.clone())?; - let ctx2 = - ctx.insert(x.clone(), t.clone()).map(|_, e| e.shift0(1, x)); + let tx = mktype(ctx, t.clone())?; + let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - Ok(RetExpr(Pi( - x.clone(), - t.embed()?, - b.get_type_move()?.embed()?, - ))) + let tb = b.get_type()?.into_owned(); + Ok(RetType( + TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb) + .typecheck()? + .to_type(), + )) } Pi(x, ta, tb) => { let ta = mktype(ctx, ta.clone())?; - let kA = ensure_is_const!( - &ta.get_type()?, - mkerr(InvalidInputType(ta.into_normalized()?)), - ); - - let ctx2 = - ctx.insert(x.clone(), ta.clone()).map(|_, e| e.shift0(1, x)); - let tb = type_with(&ctx2, tb.clone())?; - let kB = ensure_is_const!( - &tb.get_type()?, - TypeError::new( - &ctx2, - e.clone(), - InvalidOutputType(tb.get_type_move()?.into_normalized()?), - ), - ); - - let k = match function_check(kA, kB) { - Ok(k) => k, - Err(()) => { - return Err(mkerr(NoDependentTypes( - ta.clone().into_normalized()?, - tb.get_type_move()?.into_normalized()?, - ))) - } - }; - - Ok(RetExpr(Const(k))) + let ctx2 = ctx.insert_type(x, ta.clone()); + let tb = mktype(&ctx2, tb.clone())?; + Ok(RetTyped( + TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb) + .typecheck()?, + )) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -422,43 +678,52 @@ fn type_with( }; let v = type_with(ctx, v)?.normalize(); - let e = type_with( - ctx, - // TODO: Use a substitution context - subst_shift(&V(x.clone(), 0), &v.embed(), e), - )?; + let e = type_with(&ctx.insert_value(x, v.clone()), e.clone())?; - Ok(RetType(e.get_type_move()?)) + Ok(RetType(e.get_type()?.into_owned())) + } + OldOptionalLit(None, t) => { + let t = t.clone(); + let e = dhall::subexpr!(None t); + return type_with(ctx, e); + } + OldOptionalLit(Some(x), t) => { + let t = t.clone(); + let x = x.clone(); + let e = dhall::subexpr!(Some x : Optional t); + return type_with(ctx, e); } - Embed(p) => return Ok(p.clone().into()), + Embed(p) => Ok(RetTyped(p.clone().into())), _ => type_last_layer( ctx, // Typecheck recursively all subexpressions e.as_ref() - .traverse_ref_simple(|e| type_with(ctx, e.clone()))?, - e.clone(), + .traverse_ref_simple(|e| Ok(type_with(ctx, e.clone())?))?, ), }?; - match ret { - RetExpr(ret) => Ok(Typed(e, Some(mktype(ctx, rc(ret))?), PhantomData)), - RetType(typ) => Ok(Typed(e, Some(typ), PhantomData)), - } + Ok(match ret { + RetExpr(ret) => Typed::from_thunk_and_type( + Thunk::new(ctx.to_normalization_ctx(), e), + mktype(ctx, rc(ret))?, + ), + RetType(typ) => Typed::from_thunk_and_type( + Thunk::new(ctx.to_normalization_ctx(), e), + typ, + ), + RetTyped(tt) => tt, + }) } /// When all sub-expressions have been typed, check the remaining toplevel /// layer. fn type_last_layer( - ctx: &Context<Label, Type<'static>>, + ctx: &TypecheckContext, e: ExprF<Typed<'static>, Label, X, Normalized<'static>>, - original_e: SubExpr<X, Normalized<'static>>, ) -> Result<Ret, TypeError> { use dhall_core::BinOp::*; use dhall_core::Builtin::*; - use dhall_core::Const::*; use dhall_core::ExprF::*; - let mkerr = |msg: TypeMessage<'static>| { - TypeError::new(ctx, original_e.clone(), msg) - }; + let mkerr = |msg: TypeMessage<'static>| TypeError::new(ctx, msg); use Ret::*; match e { @@ -466,40 +731,43 @@ fn type_last_layer( Pi(_, _, _) => unreachable!(), Let(_, _, _, _) => unreachable!(), Embed(_) => unreachable!(), - Var(V(x, n)) => match ctx.lookup(&x, n) { - Some(e) => Ok(RetType(e.clone())), - None => Err(mkerr(UnboundVariable)), + Var(var) => match ctx.lookup(&var) { + Some(e) => Ok(RetType(e.into_owned())), + None => Err(mkerr(UnboundVariable(var.clone()))), }, App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = ensure_matches!(tf, - Pi(x, tx, tb) => (x, tx, tb), - mkerr(NotAFunction(f)) - ); - let tx = mktype(ctx, tx.embed_absurd())?; - ensure_equal!(a.get_type()?, &tx, { - mkerr(TypeMismatch(f, tx.into_normalized()?, a)) + let tf_internal = tf.internal_whnf(); + let (x, tx, tb) = match &tf_internal { + Some(Value::Pi( + x, + TypeThunk::Type(tx), + TypeThunk::Type(tb), + )) => (x, tx, tb), + Some(Value::Pi(_, _, _)) => { + panic!("ICE: this should not have happened") + } + _ => return Err(mkerr(NotAFunction(f.clone()))), + }; + ensure_equal!(a.get_type()?, tx, { + mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a)) }); - Ok(RetExpr(Let( - x.clone(), - None, - a.normalize().embed(), - tb.embed_absurd(), - ))) + + Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a))) } Annot(x, t) => { - let t = t.normalize().into_type(); + let t = t.to_type(); ensure_equal!( &t, x.get_type()?, - mkerr(AnnotMismatch(x, t.into_normalized()?)) + mkerr(AnnotMismatch(x, t.to_normalized())) ); - Ok(RetType(x.get_type_move()?)) + Ok(RetType(x.get_type()?.into_owned())) } BoolIf(x, y, z) => { ensure_equal!( x.get_type()?, - &simple_type_from_builtin(Bool), + &builtin_to_type(Bool)?, mkerr(InvalidPredicate(x)), ); @@ -519,162 +787,174 @@ fn type_last_layer( mkerr(IfBranchMismatch(y, z)) ); - Ok(RetType(y.get_type_move()?)) + Ok(RetType(y.get_type()?.into_owned())) } EmptyListLit(t) => { - let t = t.normalize().into_type(); - ensure_simple_type!( - t, - mkerr(InvalidListType(t.into_normalized()?)), - ); - let t = t.embed()?; - Ok(RetExpr(dhall::expr!(List t))) + let t = t.to_type(); + Ok(RetType( + TypeIntermediate::ListType(ctx.clone(), t) + .typecheck()? + .to_type(), + )) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); let (_, x) = iter.next().unwrap(); - ensure_simple_type!( - x.get_type()?, - mkerr(InvalidListType(x.get_type_move()?.into_normalized()?)), - ); for (i, y) in iter { ensure_equal!( x.get_type()?, y.get_type()?, mkerr(InvalidListElement( i, - x.get_type_move()?.into_normalized()?, + x.get_type()?.to_normalized(), y )) ); } - let t = x.get_type_move()?; - let t = t.embed()?; - Ok(RetExpr(dhall::expr!(List t))) - } - OldOptionalLit(None, t) => { - let t = t.normalize().embed(); - let e = dhall::subexpr!(None t); - Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) - } - OldOptionalLit(Some(x), t) => { - let t = t.normalize().embed(); - let x = x.normalize().embed(); - let e = dhall::subexpr!(Some x : Optional t); - Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) + let t = x.get_type()?.into_owned(); + Ok(RetType( + TypeIntermediate::ListType(ctx.clone(), t) + .typecheck()? + .to_type(), + )) } SomeLit(x) => { - let tx = x.get_type_move()?; - ensure_simple_type!( - tx, - mkerr(InvalidOptionalType(tx.into_normalized()?)), - ); - let t = tx.embed()?; - Ok(RetExpr(dhall::expr!(Optional t))) + let t = x.get_type()?.into_owned(); + Ok(RetType( + TypeIntermediate::OptionalType(ctx.clone(), t) + .typecheck()? + .to_type(), + )) } RecordType(kts) => { - // Check that all types are the same const - let mut k = None; - for (x, t) in kts { - let k2 = ensure_is_const!( - t.get_type()?, - mkerr(InvalidFieldType(x, t)) - ); - match k { - None => k = Some(k2), - Some(k1) if k1 != k2 => { - return Err(mkerr(InvalidFieldType(x, t))) - } - Some(_) => {} - } - } - // An empty record type has type Type - let k = k.unwrap_or(dhall_core::Const::Type); - Ok(RetType(const_to_type(k))) + let kts: BTreeMap<_, _> = kts + .into_iter() + .map(|(x, t)| Ok((x, t.to_type()))) + .collect::<Result<_, _>>()?; + Ok(RetTyped( + TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?, + )) } UnionType(kts) => { - // Check that all types are the same const - let mut k = None; - for (x, t) in kts { - if let Some(t) = t { - let k2 = ensure_is_const!( - t.get_type()?, - mkerr(InvalidFieldType(x, t)) - ); - match k { - None => k = Some(k2), - Some(k1) if k1 != k2 => { - return Err(mkerr(InvalidFieldType(x, t))) - } - Some(_) => {} - } - } - } - // An empty union type has type Type - // An union type with only unary variants has type Type - let k = k.unwrap_or(dhall_core::Const::Type); - Ok(RetType(const_to_type(k))) + let kts: BTreeMap<_, _> = kts + .into_iter() + .map(|(x, t)| { + Ok(( + x, + match t { + None => None, + Some(t) => Some(t.to_type()), + }, + )) + }) + .collect::<Result<_, _>>()?; + Ok(RetTyped( + TypeIntermediate::UnionType(ctx.clone(), kts).typecheck()?, + )) } RecordLit(kvs) => { let kts = kvs .into_iter() - .map(|(x, v)| { - let t = v.get_type_move()?.embed()?; - Ok((x, t)) - }) + .map(|(x, v)| Ok((x, v.get_type()?.into_owned()))) .collect::<Result<_, _>>()?; - Ok(RetExpr(RecordType(kts))) + Ok(RetType( + TypeIntermediate::RecordType(ctx.clone(), kts) + .typecheck()? + .to_type(), + )) } UnionLit(x, v, kvs) => { let mut kts: std::collections::BTreeMap<_, _> = kvs .into_iter() .map(|(x, v)| { - let t = v.map(|x| x.normalize().embed()); + let t = match v { + Some(x) => Some(x.to_type()), + None => None, + }; Ok((x, t)) }) .collect::<Result<_, _>>()?; - let t = v.get_type_move()?.embed()?; + let t = v.get_type()?.into_owned(); kts.insert(x, Some(t)); - Ok(RetExpr(UnionType(kts))) + Ok(RetType( + TypeIntermediate::UnionType(ctx.clone(), kts) + .typecheck()? + .to_type(), + )) } - Field(r, x) => match r.get_type()?.unroll_ref()?.as_ref() { - RecordType(kts) => match kts.get(&x) { - Some(t) => Ok(RetExpr(t.unroll().embed_absurd())), - None => Err(mkerr(MissingRecordField(x, r))), - }, - _ => { - let r = r.normalize(); - match r.as_expr().as_ref() { - UnionType(kts) => match kts.get(&x) { - // Constructor has type T -> < x: T, ... > - // TODO: use "_" instead of x - Some(Some(t)) => Ok(RetExpr(Pi( - x.clone(), - t.embed_absurd(), - r.embed(), - ))), - Some(None) => Ok(RetType(r.into_type())), - None => Err(mkerr(MissingUnionField(x, r))), + Field(r, x) => { + let tr = r.get_type()?; + let tr_internal = tr.internal_whnf(); + match &tr_internal { + Some(Value::RecordType(kts)) => match kts.get(&x) { + Some(tth) => { + let tth = tth.clone(); + drop(tr_internal); + Ok(RetType(tth.to_type(ctx)?)) }, - _ => Err(mkerr(NotARecord(x, r))), + None => Err(mkerr(MissingRecordField(x, r.clone()))), + }, + // TODO: branch here only when r.get_type() is a Const + _ => { + let r = r.to_type(); + let r_internal = r.internal_whnf(); + match &r_internal { + Some(Value::UnionType(kts)) => match kts.get(&x) { + // Constructor has type T -> < x: T, ... > + // TODO: use "_" instead of x (i.e. compare types using equivalence in tests) + Some(Some(t)) => { + let t = t.clone(); + drop(r_internal); + Ok(RetType( + TypeIntermediate::Pi( + ctx.clone(), + x.clone(), + t.to_type(ctx)?, + r, + ) + .typecheck()? + .to_type(), + )) + }, + Some(None) => { + drop(r_internal); + Ok(RetType(r)) + }, + None => { + drop(r_internal); + Err(mkerr(MissingUnionField( + x, + r.to_normalized(), + ))) + }, + }, + _ => { + drop(r_internal); + Err(mkerr(NotARecord( + x, + r.to_normalized() + ))) + }, + } } + // _ => Err(mkerr(NotARecord( + // x, + // r.to_type()?.to_normalized(), + // ))), } - }, - Const(c) => Ok(RetType(type_of_const(c))), + } + Const(c) => Ok(RetTyped(const_to_typed(c))), Builtin(b) => Ok(RetExpr(type_of_builtin(b))), - BoolLit(_) => Ok(RetType(simple_type_from_builtin(Bool))), - NaturalLit(_) => Ok(RetType(simple_type_from_builtin(Natural))), - IntegerLit(_) => Ok(RetType(simple_type_from_builtin(Integer))), - DoubleLit(_) => Ok(RetType(simple_type_from_builtin(Double))), + BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)), + NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)), + IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)), + DoubleLit(_) => Ok(RetType(builtin_to_type(Double)?)), // TODO: check type of interpolations - TextLit(_) => Ok(RetType(simple_type_from_builtin(Text))), + TextLit(_) => Ok(RetType(builtin_to_type(Text)?)), BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.unroll_ref()?.as_ref() { - App(f, _) => match f.as_ref() { - Builtin(List) => {} - _ => return Err(mkerr(BinOpTypeMismatch(o, l))), - }, - _ => return Err(mkerr(BinOpTypeMismatch(o, l))), + match l.get_type()?.internal_whnf() { + Some(Value::AppliedBuiltin(List, _)) => {} + _ => return Err(mkerr(BinOpTypeMismatch(o, l.clone()))), } ensure_equal!( @@ -686,7 +966,7 @@ fn type_last_layer( Ok(RetType(l.get_type()?.into_owned())) } BinOp(o, l, r) => { - let t = simple_type_from_builtin(match o { + let t = builtin_to_type(match o { BoolAnd => Bool, BoolOr => Bool, BoolEQ => Bool, @@ -696,7 +976,7 @@ fn type_last_layer( TextAppend => Text, ListAppend => unreachable!(), _ => return Err(mkerr(Unimplemented)), - }); + })?; ensure_equal!(l.get_type()?, &t, mkerr(BinOpTypeMismatch(o, l))); @@ -714,17 +994,17 @@ fn type_last_layer( fn type_of( e: SubExpr<X, Normalized<'static>>, ) -> Result<Typed<'static>, TypeError> { - let ctx = Context::new(); + let ctx = TypecheckContext::new(); let e = type_with(&ctx, e)?; - // Ensure the inferred type isn't SuperType - e.get_type()?.as_normalized()?; + // Ensure `e` has a type (i.e. `e` is not `Sort`) + e.get_type()?; Ok(e) } /// The specific type error #[derive(Debug)] pub(crate) enum TypeMessage<'a> { - UnboundVariable, + UnboundVariable(V<Label>), InvalidInputType(Normalized<'a>), InvalidOutputType(Normalized<'a>), NotAFunction(Typed<'a>), @@ -737,41 +1017,45 @@ pub(crate) enum TypeMessage<'a> { InvalidPredicate(Typed<'a>), IfBranchMismatch(Typed<'a>, Typed<'a>), IfBranchMustBeTerm(bool, Typed<'a>), - InvalidFieldType(Label, Typed<'a>), + InvalidFieldType(Label, Type<'a>), NotARecord(Label, Normalized<'a>), MissingRecordField(Label, Typed<'a>), MissingUnionField(Label, Normalized<'a>), BinOpTypeMismatch(BinOp, Typed<'a>), NoDependentTypes(Normalized<'a>, Normalized<'a>), + Sort, Unimplemented, } /// A structured type error that includes context #[derive(Debug)] pub struct TypeError { - context: Context<Label, Type<'static>>, - current: SubExpr<X, Normalized<'static>>, type_message: TypeMessage<'static>, + context: TypecheckContext, } impl TypeError { pub(crate) fn new( - context: &Context<Label, Type<'static>>, - current: SubExpr<X, Normalized<'static>>, + context: &TypecheckContext, type_message: TypeMessage<'static>, ) -> Self { TypeError { context: context.clone(), - current, type_message, } } } +impl From<TypeError> for std::option::NoneError { + fn from(_: TypeError) -> std::option::NoneError { + std::option::NoneError + } +} + impl ::std::error::Error for TypeMessage<'static> { fn description(&self) -> &str { match *self { - UnboundVariable => "Unbound variable", + // UnboundVariable => "Unbound variable", InvalidInputType(_) => "Invalid function input", InvalidOutputType(_) => "Invalid function output", NotAFunction(_) => "Not a function", @@ -784,28 +1068,28 @@ impl ::std::error::Error for TypeMessage<'static> { impl fmt::Display for TypeMessage<'static> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { match self { - UnboundVariable => { - f.write_str(include_str!("errors/UnboundVariable.txt")) - } - TypeMismatch(e0, e1, e2) => { - let template = include_str!("errors/TypeMismatch.txt"); - let s = template - .replace("$txt0", &format!("{}", e0.as_expr())) - .replace("$txt1", &format!("{}", e1.as_expr())) - .replace("$txt2", &format!("{}", e2.as_expr())) - .replace( - "$txt3", - &format!( - "{}", - e2.get_type() - .unwrap() - .as_normalized() - .unwrap() - .as_expr() - ), - ); - f.write_str(&s) - } + // UnboundVariable(_) => { + // f.write_str(include_str!("errors/UnboundVariable.txt")) + // } + // TypeMismatch(e0, e1, e2) => { + // let template = include_str!("errors/TypeMismatch.txt"); + // let s = template + // .replace("$txt0", &format!("{}", e0.as_expr())) + // .replace("$txt1", &format!("{}", e1.as_expr())) + // .replace("$txt2", &format!("{}", e2.as_expr())) + // .replace( + // "$txt3", + // &format!( + // "{}", + // e2.get_type() + // .unwrap() + // .as_normalized() + // .unwrap() + // .as_expr() + // ), + // ); + // f.write_str(&s) + // } _ => f.write_str("Unhandled error message"), } } |