From 5f0d69671b44ba1dff6becb9ebc7f6e74241e3e2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 18:14:55 +0200 Subject: Remove dead code --- serde_dhall/src/lib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'serde_dhall') diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index 71674a9..f400206 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -168,7 +168,8 @@ pub mod value { } pub(crate) fn make_optional_type(t: Value) -> Self { Self::from_dhall_value( - DhallValue::from_builtin(Builtin::Optional).app_thunk(t.to_thunk()), + DhallValue::from_builtin(Builtin::Optional) + .app_thunk(t.to_thunk()), ) } pub(crate) fn make_list_type(t: Value) -> Self { -- cgit v1.3.1 From 45fb07f74f19919f742be6fe7793dc72d4022f26 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 19:16:40 +0200 Subject: Try to minimize untyped TypedThunks --- dhall/src/core/thunk.rs | 13 +++++------ dhall/src/phase/mod.rs | 7 ++++-- dhall/src/phase/normalize.rs | 54 +++++++++++++++++++++++++------------------- serde_dhall/src/lib.rs | 24 ++++++++++++-------- 4 files changed, 57 insertions(+), 41 deletions(-) (limited to 'serde_dhall') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 87541d3..5f96ec8 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -182,11 +182,7 @@ impl Thunk { 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) + TypedThunk::from_thunk_untyped(Thunk::from_value(v)) } pub(crate) fn from_type(t: Type) -> TypedThunk { @@ -216,14 +212,17 @@ impl TypedThunk { pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { TypedThunk::Typed(th, Box::new(t)) } + pub fn from_thunk_simple_type(th: Thunk) -> Self { + TypedThunk::from_thunk_and_type(th, Type::const_type()) + } 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)) + pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self { + TypedThunk::from_thunk_and_type(Thunk::from_value(v), t) } // TODO: Avoid cloning if possible diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 5a6d4db..adf749c 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -101,12 +101,15 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(TypedThunk::from_const(c)) } - pub fn from_value_untyped(v: Value) -> Self { - Typed(TypedThunk::from_value_untyped(v)) + pub fn from_value_and_type(v: Value, t: Type) -> Self { + Typed(TypedThunk::from_value_and_type(v, t)) } pub(crate) fn from_typethunk(th: TypedThunk) -> Self { Typed(th) } + pub fn const_type() -> Self { + Typed::from_const(Const::Type) + } pub(crate) fn to_value(&self) -> Value { self.0.to_value() diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 2a2bf3e..02b705d 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -22,10 +22,13 @@ macro_rules! make_closure { ); Value::Var(var).into_thunk() }}; + // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { Value::Lam( Label::from(stringify!($var)).into(), - TypedThunk::from_thunk_untyped(make_closure!($($ty)*)), + TypedThunk::from_thunk_simple_type( + make_closure!($($ty)*), + ), make_closure!($($rest)*), ).into_thunk() }; @@ -61,9 +64,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { // 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())))) - } + (OptionalNone, [t, r..]) => Ok(( + r, + EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())), + )), (NaturalIsZero, [n, r..]) => match &*n.as_value() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), @@ -228,7 +232,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { [ var(x, 1) ] # var(xs, 0) ) }) - .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))), + .app_val(EmptyListLit(TypedThunk::from_thunk_simple_type( + t.clone(), + ))), )), }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() { @@ -260,9 +266,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { 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(), - ))), + .app_val(EmptyOptionalLit( + TypedThunk::from_thunk_simple_type(t.clone()), + )), )), }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() { @@ -611,18 +617,20 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp( - RecursiveRecordTypeMerge, - v1.to_thunk(), - v2.to_thunk(), - ))) + TypedThunk::from_thunk_untyped(Thunk::from_partial_expr( + ExprF::BinOp( + RecursiveRecordTypeMerge, + v1.to_thunk(), + v2.to_thunk(), + ), + )) }); Ret::Value(RecordType(kvs)) } (Equivalence, _, _) => Ret::Value(Value::Equivalence( - TypedThunk::from_thunk(x.clone()), - TypedThunk::from_thunk(y.clone()), + TypedThunk::from_thunk_simple_type(x.clone()), + TypedThunk::from_thunk_simple_type(y.clone()), )), _ => return None, @@ -645,12 +653,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { ExprF::Annot(x, _) => Ret::Thunk(x), ExprF::Assert(_) => Ret::Expr(expr), ExprF::Lam(x, t, e) => { - Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e)) + Ret::Value(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e)) } ExprF::Pi(x, t, e) => Ret::Value(Pi( x.into(), - TypedThunk::from_thunk(t), - TypedThunk::from_thunk(e), + TypedThunk::from_thunk_untyped(t), + TypedThunk::from_thunk_untyped(e), )), ExprF::Let(x, _, v, b) => { let v = Typed::from_thunk_untyped(v); @@ -669,9 +677,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { let t_borrow = t.as_value(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::Value(EmptyListLit(TypedThunk::from_thunk( - args[0].clone(), - ))) + Ret::Value(EmptyListLit( + TypedThunk::from_thunk_simple_type(args[0].clone()), + )) } _ => { drop(t_borrow); @@ -687,12 +695,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { } ExprF::RecordType(kts) => Ret::Value(RecordType( kts.into_iter() - .map(|(k, t)| (k, TypedThunk::from_thunk(t))) + .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t))) .collect(), )), ExprF::UnionType(kts) => Ret::Value(UnionType( kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t)))) + .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t)))) .collect(), )), ExprF::TextLit(elts) => { diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index f400206..a277977 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -160,20 +160,21 @@ pub mod value { self.0.to_type() } - pub(crate) fn from_dhall_value(v: DhallValue) -> Self { - Value(Typed::from_value_untyped(v)) + /// Assumes that the given value has type `Type`. + pub(crate) fn make_simple_type(v: DhallValue) -> Self { + Value(Typed::from_value_and_type(v, Type::const_type())) } pub(crate) fn make_builtin_type(b: Builtin) -> Self { - Self::from_dhall_value(DhallValue::from_builtin(b)) + Self::make_simple_type(DhallValue::from_builtin(b)) } pub(crate) fn make_optional_type(t: Value) -> Self { - Self::from_dhall_value( + Self::make_simple_type( DhallValue::from_builtin(Builtin::Optional) .app_thunk(t.to_thunk()), ) } pub(crate) fn make_list_type(t: Value) -> Self { - Self::from_dhall_value( + Self::make_simple_type( DhallValue::from_builtin(Builtin::List).app_thunk(t.to_thunk()), ) } @@ -182,9 +183,9 @@ pub mod value { pub fn make_record_type( kts: impl Iterator, ) -> Self { - Self::from_dhall_value(DhallValue::RecordType( + Self::make_simple_type(DhallValue::RecordType( kts.map(|(k, t)| { - (k.into(), TypedThunk::from_thunk(t.to_thunk())) + (k.into(), TypedThunk::from_thunk_simple_type(t.to_thunk())) }) .collect(), )) @@ -193,9 +194,14 @@ pub mod value { pub fn make_union_type( kts: impl Iterator)>, ) -> Self { - Self::from_dhall_value(DhallValue::UnionType( + Self::make_simple_type(DhallValue::UnionType( kts.map(|(k, t)| { - (k.into(), t.map(|t| TypedThunk::from_thunk(t.to_thunk()))) + ( + k.into(), + t.map(|t| { + TypedThunk::from_thunk_simple_type(t.to_thunk()) + }), + ) }) .collect(), )) -- cgit v1.3.1 From e0f5216215ccb7a4df85d80e11dd265cdb52a44f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 19:47:36 +0200 Subject: s/Value/ValueF/ --- dhall/src/core/context.rs | 4 +- dhall/src/core/thunk.rs | 90 ++++++++-------- dhall/src/core/value.rs | 212 ++++++++++++++++++------------------ dhall/src/core/var.rs | 2 +- dhall/src/phase/mod.rs | 12 +-- dhall/src/phase/normalize.rs | 250 ++++++++++++++++++++++--------------------- dhall/src/phase/typecheck.rs | 110 +++++++++---------- serde_dhall/src/lib.rs | 4 +- 8 files changed, 345 insertions(+), 339 deletions(-) (limited to 'serde_dhall') diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index cc25749..b1fbde9 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; use crate::core::thunk::Thunk; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::TypeError; use crate::phase::{Type, Typed}; @@ -44,7 +44,7 @@ impl TypecheckContext { let i = i.under_multiple_binders(&shift_map); let (th, t) = match i { CtxItem::Kept(newvar, t) => { - (Value::Var(newvar).into_thunk(), t) + (ValueF::Var(newvar).into_thunk(), t) } CtxItem::Replaced(th, t) => (th, t), }; diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 5f96ec8..cf7c097 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -5,7 +5,7 @@ use std::rc::Rc; use dhall_syntax::{Const, ExprF}; use crate::core::context::TypecheckContext; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; @@ -24,12 +24,12 @@ use Marker::{NF, WHNF}; #[derive(Debug)] enum ThunkInternal { /// 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 + /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no /// requirement of WHNF here. PartialExpr(ExprF), /// Partially normalized value. /// Invariant: if the marker is `NF`, the value must be fully normalized - Value(Marker, Value), + ValueF(Marker, ValueF), } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -61,10 +61,10 @@ impl ThunkInternal { match self { ThunkInternal::PartialExpr(e) => { *self = - ThunkInternal::Value(WHNF, normalize_one_layer(e.clone())) + ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone())) } // Already at least in WHNF - ThunkInternal::Value(_, _) => {} + ThunkInternal::ValueF(_, _) => {} } } @@ -74,37 +74,37 @@ impl ThunkInternal { self.normalize_whnf(); self.normalize_nf(); } - ThunkInternal::Value(m @ WHNF, v) => { + ThunkInternal::ValueF(m @ WHNF, v) => { v.normalize_mut(); *m = NF; } // Already in NF - ThunkInternal::Value(NF, _) => {} + ThunkInternal::ValueF(NF, _) => {} } } // Always use normalize_whnf before - fn as_whnf(&self) -> &Value { + fn as_whnf(&self) -> &ValueF { match self { ThunkInternal::PartialExpr(_) => unreachable!(), - ThunkInternal::Value(_, v) => v, + ThunkInternal::ValueF(_, v) => v, } } // Always use normalize_nf before - fn as_nf(&self) -> &Value { + fn as_nf(&self) -> &ValueF { match self { - ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => { + ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { unreachable!() } - ThunkInternal::Value(NF, v) => v, + ThunkInternal::ValueF(NF, v) => v, } } } impl Thunk { - pub(crate) fn from_value(v: Value) -> Thunk { - ThunkInternal::Value(WHNF, v).into_thunk() + pub(crate) fn from_valuef(v: ValueF) -> Thunk { + ThunkInternal::ValueF(WHNF, v).into_thunk() } pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { @@ -130,38 +130,38 @@ impl Thunk { self.0.borrow_mut().normalize_whnf(); } // Already at least in WHNF - ThunkInternal::Value(_, _) => {} + ThunkInternal::ValueF(_, _) => {} } } fn do_normalize_nf(&self) { let borrow = self.0.borrow(); match &*borrow { - ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => { + ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { drop(borrow); self.0.borrow_mut().normalize_nf(); } // Already in NF - ThunkInternal::Value(NF, _) => {} + ThunkInternal::ValueF(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 { + pub(crate) fn normalize_nf(&self) -> Ref { 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 { + pub(crate) fn as_valuef(&self) -> Ref { 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 to_valuef(&self) -> ValueF { + self.as_valuef().clone() } pub(crate) fn normalize_to_expr_maybe_alpha( @@ -171,27 +171,27 @@ impl Thunk { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app_val(&self, val: Value) -> Value { + pub(crate) fn app_val(&self, val: ValueF) -> ValueF { self.app_thunk(val.into_thunk()) } - pub(crate) fn app_thunk(&self, th: Thunk) -> Value { + pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF { apply_any(self.clone(), th) } } impl TypedThunk { - pub(crate) fn from_value(v: Value) -> TypedThunk { - TypedThunk::from_thunk_untyped(Thunk::from_value(v)) + pub(crate) fn from_valuef(v: ValueF) -> TypedThunk { + TypedThunk::from_thunk_untyped(Thunk::from_valuef(v)) } pub(crate) fn from_type(t: Type) -> TypedThunk { t.into_typethunk() } - pub(crate) fn normalize_nf(&self) -> Value { + pub(crate) fn normalize_nf(&self) -> ValueF { match self { - TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Const(c) => ValueF::Const(*c), TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { thunk.normalize_nf().clone() } @@ -221,27 +221,29 @@ impl TypedThunk { pub(crate) fn from_const(c: Const) -> Self { TypedThunk::Const(c) } - pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self { - TypedThunk::from_thunk_and_type(Thunk::from_value(v), t) + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + TypedThunk::from_thunk_and_type(Thunk::from_valuef(v), t) } // TODO: Avoid cloning if possible - pub(crate) fn to_value(&self) -> Value { + pub(crate) fn to_valuef(&self) -> ValueF { match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), - TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { + th.to_valuef() + } + TypedThunk::Const(c) => ValueF::Const(*c), } } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr() + self.to_valuef().normalize_to_expr() } pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr_maybe_alpha(true) + self.to_valuef().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)), + TypedThunk::Const(c) => Thunk::from_valuef(ValueF::Const(*c)), } } pub(crate) fn to_type(&self) -> Type { @@ -252,8 +254,8 @@ impl TypedThunk { } pub(crate) fn as_const(&self) -> Option { // TODO: avoid clone - match &self.to_value() { - Value::Const(c) => Some(*c), + match &self.to_valuef() { + ValueF::Const(c) => Some(*c), _ => None, } } @@ -294,8 +296,8 @@ impl Shift for ThunkInternal { |x, v| Ok(v.shift(delta, &var.under_binder(x))?), )?, ), - ThunkInternal::Value(m, v) => { - ThunkInternal::Value(*m, v.shift(delta, var)?) + ThunkInternal::ValueF(m, v) => { + ThunkInternal::ValueF(*m, v.shift(delta, var)?) } }) } @@ -336,9 +338,9 @@ impl Subst for ThunkInternal { }, ), ), - ThunkInternal::Value(_, v) => { + ThunkInternal::ValueF(_, v) => { // The resulting value may not stay in normal form after substitution - ThunkInternal::Value(WHNF, v.subst_shift(var, val)) + ThunkInternal::ValueF(WHNF, v.subst_shift(var, val)) } } } @@ -361,14 +363,14 @@ impl Subst for TypedThunk { impl std::cmp::PartialEq for Thunk { fn eq(&self, other: &Self) -> bool { - *self.as_value() == *other.as_value() + *self.as_valuef() == *other.as_valuef() } } impl std::cmp::Eq for Thunk {} impl std::cmp::PartialEq for TypedThunk { fn eq(&self, other: &Self) -> bool { - self.to_value() == other.to_value() + self.to_valuef() == other.to_valuef() } } impl std::cmp::Eq for TypedThunk {} @@ -377,7 +379,7 @@ 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) => { + ThunkInternal::ValueF(m, v) => { f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() } ThunkInternal::PartialExpr(e) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index d3d017d..0f2ef00 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -15,16 +15,16 @@ use crate::phase::{Normalized, 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 +/// This WHNF must be preserved by operations on `ValueF`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 +/// on-demand. When all the Thunks 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. /// 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 { +pub enum ValueF { /// Closures Lam(AlphaLabel, TypedThunk, Thunk), Pi(AlphaLabel, TypedThunk, TypedThunk), @@ -55,9 +55,9 @@ pub enum Value { PartialExpr(ExprF), } -impl Value { +impl ValueF { pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_value(self) + Thunk::from_valuef(self) } /// Convert the value to a fully normalized syntactic expression @@ -71,12 +71,12 @@ impl Value { alpha: bool, ) -> OutputSubExpr { match self { - Value::Lam(x, t, e) => rc(ExprF::Lam( + 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), )), - Value::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(b, args) => { let mut e = rc(ExprF::Builtin(*b)); for v in args { e = rc(ExprF::App( @@ -86,48 +86,48 @@ impl Value { } e } - Value::Pi(x, t, e) => rc(ExprF::Pi( + 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), )), - 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( + 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), )), - Value::NEOptionalLit(n) => { + ValueF::NEOptionalLit(n) => { rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) } - Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + ValueF::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( + ValueF::NEListLit(elts) => rc(ExprF::NEListLit( elts.iter() .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) .collect(), )), - Value::RecordLit(kvs) => rc(ExprF::RecordLit( + ValueF::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( + ValueF::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( + ValueF::UnionType(kts) => rc(ExprF::UnionType( kts.iter() .map(|(k, v)| { ( @@ -139,7 +139,7 @@ impl Value { }) .collect(), )), - Value::UnionConstructor(l, kts) => { + ValueF::UnionConstructor(l, kts) => { let kts = kts .iter() .map(|(k, v)| { @@ -153,12 +153,12 @@ impl Value { .collect(); rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } - Value::UnionLit(l, v, kts) => rc(ExprF::App( - Value::UnionConstructor(l.clone(), kts.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), )), - Value::TextLit(elts) => { + ValueF::TextLit(elts) => { use InterpolatedTextContents::{Expr, Text}; rc(ExprF::TextLit( elts.iter() @@ -171,12 +171,12 @@ impl Value { .collect(), )) } - Value::Equivalence(x, y) => rc(ExprF::BinOp( + 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), )), - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } @@ -184,60 +184,60 @@ impl Value { pub(crate) fn normalize_mut(&mut self) { match self { - Value::Var(_) - | Value::Const(_) - | Value::BoolLit(_) - | Value::NaturalLit(_) - | Value::IntegerLit(_) - | Value::DoubleLit(_) => {} + ValueF::Var(_) + | ValueF::Const(_) + | ValueF::BoolLit(_) + | ValueF::NaturalLit(_) + | ValueF::IntegerLit(_) + | ValueF::DoubleLit(_) => {} - Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => { + ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { tth.normalize_mut(); } - Value::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th) => { th.normalize_mut(); } - Value::Lam(_, t, e) => { + ValueF::Lam(_, t, e) => { t.normalize_mut(); e.normalize_mut(); } - Value::Pi(_, t, e) => { + ValueF::Pi(_, t, e) => { t.normalize_mut(); e.normalize_mut(); } - Value::AppliedBuiltin(_, args) => { + ValueF::AppliedBuiltin(_, args) => { for x in args.iter_mut() { x.normalize_mut(); } } - Value::NEListLit(elts) => { + ValueF::NEListLit(elts) => { for x in elts.iter_mut() { x.normalize_mut(); } } - Value::RecordLit(kvs) => { + ValueF::RecordLit(kvs) => { for x in kvs.values_mut() { x.normalize_mut(); } } - Value::RecordType(kvs) => { + ValueF::RecordType(kvs) => { for x in kvs.values_mut() { x.normalize_mut(); } } - Value::UnionType(kts) | Value::UnionConstructor(_, kts) => { + ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - Value::UnionLit(_, v, kts) => { + ValueF::UnionLit(_, v, kts) => { v.normalize_mut(); for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - Value::TextLit(elts) => { + ValueF::TextLit(elts) => { for x in elts.iter_mut() { use InterpolatedTextContents::{Expr, Text}; match x { @@ -246,11 +246,11 @@ impl Value { } } } - Value::Equivalence(x, y) => { + ValueF::Equivalence(x, y) => { x.normalize_mut(); y.normalize_mut(); } - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { // TODO: need map_mut e.map_ref(|v| { v.normalize_nf(); @@ -260,75 +260,75 @@ impl Value { } /// Apply to a value - pub(crate) fn app(self, val: Value) -> Value { + pub(crate) fn app(self, val: ValueF) -> ValueF { self.app_val(val) } /// Apply to a value - pub(crate) fn app_val(self, val: Value) -> Value { + pub(crate) fn app_val(self, val: ValueF) -> ValueF { self.app_thunk(val.into_thunk()) } /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> Value { - Thunk::from_value(self).app_thunk(th) + pub fn app_thunk(self, th: Thunk) -> ValueF { + Thunk::from_valuef(self).app_thunk(th) } - pub fn from_builtin(b: Builtin) -> Value { - Value::AppliedBuiltin(b, vec![]) + pub fn from_builtin(b: Builtin) -> ValueF { + ValueF::AppliedBuiltin(b, vec![]) } } -impl Shift for Value { +impl Shift for ValueF { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - Value::Lam(x, t, e) => Value::Lam( + ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.shift(delta, var)?, e.shift(delta, &var.under_binder(x))?, ), - Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( + ValueF::AppliedBuiltin(b, args) => ValueF::AppliedBuiltin( *b, args.iter() .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::Pi(x, t, e) => Value::Pi( + ValueF::Pi(x, t, e) => ValueF::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)?) + 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)?) } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.shift(delta, var)?) + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.shift(delta, var)?) + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) } - Value::NEListLit(elts) => Value::NEListLit( + ValueF::NEListLit(elts) => ValueF::NEListLit( elts.iter() .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::RecordLit(kvs) => Value::RecordLit( + ValueF::RecordLit(kvs) => ValueF::RecordLit( kvs.iter() .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) .collect::>()?, ), - Value::RecordType(kvs) => Value::RecordType( + ValueF::RecordType(kvs) => ValueF::RecordType( kvs.iter() .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) .collect::>()?, ), - Value::UnionType(kts) => Value::UnionType( + ValueF::UnionType(kts) => ValueF::UnionType( kts.iter() .map(|(k, v)| { Ok(( @@ -340,7 +340,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( + ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( x.clone(), kts.iter() .map(|(k, v)| { @@ -353,7 +353,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::UnionLit(x, v, kts) => Value::UnionLit( + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.shift(delta, var)?, kts.iter() @@ -367,7 +367,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::TextLit(elts) => Value::TextLit( + ValueF::TextLit(elts) => ValueF::TextLit( elts.iter() .map(|contents| { use InterpolatedTextContents::{Expr, Text}; @@ -378,10 +378,10 @@ impl Shift for Value { }) .collect::>()?, ), - Value::Equivalence(x, y) => { - Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) } - Value::PartialExpr(e) => Value::PartialExpr( + ValueF::PartialExpr(e) => ValueF::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))?), @@ -391,16 +391,16 @@ impl Shift for Value { } } -impl Subst for Value { +impl Subst for ValueF { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { // Retry normalizing since substituting may allow progress - Value::AppliedBuiltin(b, args) => apply_builtin( + ValueF::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) => { + ValueF::PartialExpr(e) => { normalize_one_layer(e.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), |x, v| { @@ -412,8 +412,8 @@ impl Subst for Value { )) } // Retry normalizing since substituting may allow progress - Value::TextLit(elts) => { - Value::TextLit(squash_textlit(elts.iter().map(|contents| { + ValueF::TextLit(elts) => { + ValueF::TextLit(squash_textlit(elts.iter().map(|contents| { use InterpolatedTextContents::{Expr, Text}; match contents { Expr(th) => Expr(th.subst_shift(var, val)), @@ -421,53 +421,53 @@ impl Subst for Value { } }))) } - Value::Lam(x, t, e) => Value::Lam( + 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)), ), - Value::Pi(x, t, e) => Value::Pi( + 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)), ), - 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)) + ValueF::Var(v) if v == var => val.to_valuef(), + 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)) } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.subst_shift(var, val)) + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.subst_shift(var, val)) } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.subst_shift(var, val)) + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.subst_shift(var, val)) } - Value::NEListLit(elts) => Value::NEListLit( + ValueF::NEListLit(elts) => ValueF::NEListLit( elts.iter().map(|v| v.subst_shift(var, val)).collect(), ), - Value::RecordLit(kvs) => Value::RecordLit( + ValueF::RecordLit(kvs) => ValueF::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) .collect(), ), - Value::RecordType(kvs) => Value::RecordType( + ValueF::RecordType(kvs) => ValueF::RecordType( kvs.iter() .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) .collect(), ), - Value::UnionType(kts) => Value::UnionType( + ValueF::UnionType(kts) => ValueF::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( + ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( x.clone(), kts.iter() .map(|(k, v)| { @@ -475,7 +475,7 @@ impl Subst for Value { }) .collect(), ), - Value::UnionLit(x, v, kts) => Value::UnionLit( + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.subst_shift(var, val), kts.iter() @@ -484,7 +484,7 @@ impl Subst for Value { }) .collect(), ), - Value::Equivalence(x, y) => Value::Equivalence( + 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 becd653..296e968 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -12,7 +12,7 @@ pub struct AlphaVar { } // 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); diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index adf749c..7e74f95 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -5,7 +5,7 @@ use std::path::Path; use dhall_syntax::{Const, SubExpr}; use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{EncodeError, Error, ImportError, TypeError}; @@ -101,8 +101,8 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(TypedThunk::from_const(c)) } - pub fn from_value_and_type(v: Value, t: Type) -> Self { - Typed(TypedThunk::from_value_and_type(v, t)) + pub fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + Typed(TypedThunk::from_valuef_and_type(v, t)) } pub(crate) fn from_typethunk(th: TypedThunk) -> Self { Typed(th) @@ -111,8 +111,8 @@ impl Typed { Typed::from_const(Const::Type) } - pub(crate) fn to_value(&self) -> Value { - self.0.to_value() + pub(crate) fn to_valuef(&self) -> ValueF { + self.0.to_valuef() } pub fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() @@ -229,7 +229,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.to_valuef() == other.to_valuef() } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 02b705d..da54726 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -6,7 +6,7 @@ use dhall_syntax::{ }; use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr, Typed}; @@ -20,11 +20,11 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - Value::Var(var).into_thunk() + ValueF::Var(var).into_thunk() }}; // 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_simple_type( make_closure!($($ty)*), @@ -32,35 +32,35 @@ macro_rules! make_closure { make_closure!($($rest)*), ).into_thunk() }; - (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() }; + (Natural) => { ValueF::from_builtin(Builtin::Natural).into_thunk() }; (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) + ValueF::from_builtin(Builtin::List) .app_thunk(make_closure!($($rest)*)) .into_thunk() }; (Some $($rest:tt)*) => { - Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk() + ValueF::NEOptionalLit(make_closure!($($rest)*)).into_thunk() }; (1 + $($rest:tt)*) => { - Value::PartialExpr(ExprF::BinOp( + ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Thunk::from_value(Value::NaturalLit(1)), + Thunk::from_valuef(ValueF::NaturalLit(1)), )).into_thunk() }; ([ $($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_thunk(), make_closure!($($tail)*), )).into_thunk() }; } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { +pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> 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()) { @@ -68,23 +68,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { r, EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())), )), - (NaturalIsZero, [n, r..]) => match &*n.as_value() { + (NaturalIsZero, [n, r..]) => match &*n.as_valuef() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), }, - (NaturalEven, [n, r..]) => match &*n.as_value() { + (NaturalEven, [n, r..]) => match &*n.as_valuef() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), _ => Err(()), }, - (NaturalOdd, [n, r..]) => match &*n.as_value() { + (NaturalOdd, [n, r..]) => match &*n.as_valuef() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), _ => Err(()), }, - (NaturalToInteger, [n, r..]) => match &*n.as_value() { + (NaturalToInteger, [n, r..]) => match &*n.as_valuef() { NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), _ => Err(()), }, - (NaturalShow, [n, r..]) => match &*n.as_value() { + (NaturalShow, [n, r..]) => match &*n.as_valuef() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), @@ -92,7 +92,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { - match (&*a.as_value(), &*b.as_value()) { + match (&*a.as_valuef(), &*b.as_valuef()) { (NaturalLit(a), NaturalLit(b)) => { Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) } @@ -102,7 +102,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { _ => Err(()), } } - (IntegerShow, [n, r..]) => match &*n.as_value() { + (IntegerShow, [n, r..]) => match &*n.as_valuef() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() @@ -113,18 +113,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { } _ => Err(()), }, - (IntegerToDouble, [n, r..]) => match &*n.as_value() { + (IntegerToDouble, [n, r..]) => match &*n.as_valuef() { IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), _ => Err(()), }, - (DoubleShow, [n, r..]) => match &*n.as_value() { + (DoubleShow, [n, r..]) => match &*n.as_valuef() { 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_valuef() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -158,41 +158,41 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { } _ => Err(()), }, - (ListLength, [_, l, r..]) => match &*l.as_value() { + (ListLength, [_, l, r..]) => match &*l.as_valuef() { 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_valuef() { 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_valuef() { 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_valuef() { 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_valuef() { EmptyListLit(t) => { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedThunk::from_value(Value::from_builtin(Natural)), + TypedThunk::from_valuef(ValueF::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); - Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts))))) + Ok((r, EmptyListLit(TypedThunk::from_valuef(RecordType(kts))))) } NEListLit(xs) => { let xs = xs @@ -201,20 +201,20 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> 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(), Thunk::from_valuef(i)); kvs.insert("value".into(), e.clone()); - Thunk::from_value(RecordLit(kvs)) + Thunk::from_valuef(RecordLit(kvs)) }) .collect(); Ok((r, NEListLit(xs))) } _ => Err(()), }, - (ListBuild, [t, f, r..]) => match &*f.as_value() { + (ListBuild, [t, f, r..]) => match &*f.as_valuef() { // 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_valuef())) } else { // Do we really need to handle this case ? unimplemented!() @@ -222,7 +222,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { } _ => Ok(( r, - f.app_val(Value::from_builtin(List).app_thunk(t.clone())) + f.app_val(ValueF::from_builtin(List).app_thunk(t.clone())) .app_thunk({ // Move `t` under new `x` variable let t1 = t.under_binder(Label::from("x")); @@ -237,8 +237,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { ))), )), }, - (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() { - EmptyListLit(_) => Ok((r, nil.to_value())), + (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() { + EmptyListLit(_) => Ok((r, nil.to_valuef())), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { @@ -248,15 +248,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { .app_thunk(v) .into_thunk(); } - Ok((r, v.to_value())) + Ok((r, v.to_valuef())) } _ => Err(()), }, - (OptionalBuild, [t, f, r..]) => match &*f.as_value() { + (OptionalBuild, [t, f, r..]) => match &*f.as_valuef() { // 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_valuef())) } else { // Do we really need to handle this case ? unimplemented!() @@ -264,23 +264,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { } _ => Ok(( r, - f.app_val(Value::from_builtin(Optional).app_thunk(t.clone())) + f.app_val(ValueF::from_builtin(Optional).app_thunk(t.clone())) .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0))) .app_val(EmptyOptionalLit( TypedThunk::from_thunk_simple_type(t.clone()), )), )), }, - (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() { - EmptyOptionalLit(_) => Ok((r, nothing.to_value())), - NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))), - _ => Err(()), - }, - (NaturalBuild, [f, r..]) => match &*f.as_value() { + (OptionalFold, [_, v, _, just, nothing, r..]) => { + match &*v.as_valuef() { + EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())), + NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))), + _ => Err(()), + } + } + (NaturalBuild, [f, r..]) => match &*f.as_valuef() { // 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_valuef())) } else { // Do we really need to handle this case ? unimplemented!() @@ -288,15 +290,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { } _ => Ok(( r, - f.app_val(Value::from_builtin(Natural)) + f.app_val(ValueF::from_builtin(Natural)) .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) .app_val(NaturalLit(0)), )), }, - (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_valuef() { + NaturalLit(0) => Ok((r, zero.to_valuef())), 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()) @@ -319,22 +321,22 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> 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: Thunk, a: Thunk) -> ValueF { + let fallback = |f: Thunk, a: Thunk| ValueF::PartialExpr(ExprF::App(f, a)); - let f_borrow = f.as_value(); + let f_borrow = f.as_valuef(); match &*f_borrow { - Value::Lam(x, _, e) => { + ValueF::Lam(x, _, e) => { let val = Typed::from_thunk_untyped(a); - e.subst_shift(&x.into(), &val).to_value() + e.subst_shift(&x.into(), &val).to_valuef() } - Value::AppliedBuiltin(b, args) => { + 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); @@ -358,9 +360,9 @@ pub(crate) fn squash_textlit( match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_value(); + let e_borrow = e.as_valuef(); match &*e_borrow { - Value::TextLit(elts2) => { + ValueF::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) } _ => { @@ -387,7 +389,7 @@ pub(crate) fn squash_textlit( // Small helper enum to avoid repetition enum Ret<'a> { - Value(Value), + ValueF(ValueF), Thunk(Thunk), ThunkRef(&'a Thunk), Expr(ExprF), @@ -512,67 +514,67 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { 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_valuef(); + let y_borrow = y.as_valuef(); 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, BoolLit(false), _) => Ret::ValueF(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => Ret::ValueF(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(true), _) => Ret::ValueF(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => Ret::ValueF(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)), + (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => Ret::ValueF(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)), + (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)), + (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)), (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y), (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(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(0), _) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y), (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(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, 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), 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()), ))) } @@ -589,7 +591,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { // 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() => { @@ -606,7 +608,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { v2.clone(), )) }); - Ret::Value(RecordLit(kvs)) + Ret::ValueF(RecordLit(kvs)) } (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => { @@ -625,10 +627,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { ), )) }); - Ret::Value(RecordType(kvs)) + Ret::ValueF(RecordType(kvs)) } - (Equivalence, _, _) => Ret::Value(Value::Equivalence( + (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence( TypedThunk::from_thunk_simple_type(x.clone()), TypedThunk::from_thunk_simple_type(y.clone()), )), @@ -637,8 +639,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { }) } -pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { - use Value::{ +pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { + use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor, UnionLit, UnionType, @@ -653,9 +655,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { ExprF::Annot(x, _) => Ret::Thunk(x), ExprF::Assert(_) => Ret::Expr(expr), ExprF::Lam(x, t, e) => { - Ret::Value(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e)) + Ret::ValueF(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e)) } - ExprF::Pi(x, t, e) => Ret::Value(Pi( + ExprF::Pi(x, t, e) => Ret::ValueF(Pi( x.into(), TypedThunk::from_thunk_untyped(t), TypedThunk::from_thunk_untyped(e), @@ -664,20 +666,20 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { 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::App(v, a) => Ret::ValueF(v.app_thunk(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_valuef(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::Value(EmptyListLit( + Ret::ValueF(EmptyListLit( TypedThunk::from_thunk_simple_type(args[0].clone()), )) } @@ -688,17 +690,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> 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::Value(RecordType( + ExprF::RecordType(kts) => Ret::ValueF(RecordType( kts.into_iter() .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t))) .collect(), )), - ExprF::UnionType(kts) => Ret::Value(UnionType( + ExprF::UnionType(kts) => Ret::ValueF(UnionType( kts.into_iter() .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t)))) .collect(), @@ -710,17 +712,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { if let [Expr(th)] = elts.as_slice() { Ret::Thunk(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_valuef(); match &*b_borrow { BoolLit(true) => Ret::ThunkRef(e1), BoolLit(false) => Ret::ThunkRef(e2), _ => { - let e1_borrow = e1.as_value(); - let e2_borrow = e2.as_value(); + let e1_borrow = e1.as_valuef(); + let e2_borrow = e2.as_valuef(); match (&*e1_borrow, &*e2_borrow) { // Simplify `if b then True else False` (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b), @@ -741,12 +743,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> 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_valuef(); 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())) @@ -760,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { } } ExprF::Field(ref v, ref l) => { - let v_borrow = v.as_value(); + let v_borrow = v.as_valuef(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Thunk(r.clone()), @@ -770,7 +772,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { } }, UnionType(kts) => { - Ret::Value(UnionConstructor(l.clone(), kts.clone())) + Ret::ValueF(UnionConstructor(l.clone(), kts.clone())) } _ => { drop(v_borrow); @@ -780,8 +782,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { } ExprF::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_value(); - let variant_borrow = variant.as_value(); + let handlers_borrow = handlers.as_valuef(); + let variant_borrow = variant.as_valuef(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { Some(h) => Ret::Thunk(h.clone()), @@ -792,7 +794,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> 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_thunk(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); @@ -809,9 +811,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> 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::Thunk(th) => th.to_valuef(), + Ret::ThunkRef(th) => th.to_valuef(), + Ret::Expr(expr) => ValueF::PartialExpr(expr), } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index dd6da70..8d7a3bc 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -6,7 +6,7 @@ use dhall_syntax::{ use crate::core::context::TypecheckContext; use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::{Normalized, Resolved, Type, Typed}; @@ -43,7 +43,7 @@ fn tck_pi_type( let k = function_check(ka, kb); Ok(Typed::from_thunk_and_type( - Value::Pi( + ValueF::Pi( x.into(), TypedThunk::from_type(tx), TypedThunk::from_type(te), @@ -88,7 +88,7 @@ fn tck_record_type( let k = k.unwrap_or(dhall_syntax::Const::Type); Ok(Typed::from_thunk_and_type( - Value::RecordType(new_kts).into_thunk(), + ValueF::RecordType(new_kts).into_thunk(), Type::from_const(k), )) } @@ -132,7 +132,7 @@ fn tck_union_type( let k = k.unwrap_or(dhall_syntax::Const::Type); Ok(Typed::from_thunk_and_type( - Value::UnionType(new_kts).into_thunk(), + ValueF::UnionType(new_kts).into_thunk(), Type::from_const(k), )) } @@ -335,14 +335,14 @@ fn type_with( let tx = mktype(ctx, t.clone())?; let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - let v = Value::Lam( + let v = ValueF::Lam( x.clone().into(), TypedThunk::from_type(tx.clone()), b.to_thunk(), ); 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) + Typed::from_thunk_and_type(Thunk::from_valuef(v), t) } Pi(x, ta, tb) => { let ta = mktype(ctx, ta.clone())?; @@ -415,8 +415,10 @@ 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()), + let (x, tx, tb) = match &tf.to_valuef() { + ValueF::Pi(x, tx, tb) => { + (x.clone(), tx.to_type(), tb.to_type()) + } _ => return Err(mkerr(NotAFunction(f.clone()))), }; if a.get_type()?.as_ref() != &tx { @@ -437,9 +439,9 @@ fn type_last_layer( Ok(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) => { + match t.to_valuef() { + ValueF::Equivalence(ref x, ref y) if x == y => {} + ValueF::Equivalence(x, y) => { return Err(mkerr(AssertMismatch( x.to_typed(), y.to_typed(), @@ -470,8 +472,8 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.to_type(); - match &t.to_value() { - Value::AppliedBuiltin(dhall_syntax::Builtin::List, args) + match &t.to_valuef() { + ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} _ => { return Err(TypeError::new( @@ -504,8 +506,8 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_thunk_and_type( - Value::from_builtin(dhall_syntax::Builtin::List) - .app(t.to_value()) + ValueF::from_builtin(dhall_syntax::Builtin::List) + .app(t.to_valuef()) .into_thunk(), Typed::from_const(Type), ) @@ -523,8 +525,8 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_thunk_and_type( - Value::from_builtin(dhall_syntax::Builtin::Optional) - .app(t.to_value()) + ValueF::from_builtin(dhall_syntax::Builtin::Optional) + .app(t.to_valuef()) .into_thunk(), Typed::from_const(Type).into_type(), ) @@ -549,8 +551,8 @@ fn type_last_layer( .into_type(), )), Field(r, x) => { - match &r.get_type()?.to_value() { - Value::RecordType(kts) => match kts.get(&x) { + match &r.get_type()?.to_valuef() { + ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { Ok(RetTypeOnly(tth.to_type())) }, @@ -560,8 +562,8 @@ fn type_last_layer( // 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.to_valuef() { + ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { Ok(RetTypeOnly( @@ -631,14 +633,14 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_value() { - Value::RecordType(kts) => kts, + let kts_x = match l_type.to_valuef() { + ValueF::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, + let kts_y = match r_type.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -672,10 +674,10 @@ fn type_last_layer( inner_l: &TypedThunk, inner_r: &TypedThunk| -> Result { - match (inner_l.to_value(), inner_r.to_value()) { + match (inner_l.to_valuef(), inner_r.to_valuef()) { ( - Value::RecordType(inner_l_kvs), - Value::RecordType(inner_r_kvs), + ValueF::RecordType(inner_l_kvs), + ValueF::RecordType(inner_r_kvs), ) => { combine_record_types(ctx, inner_l_kvs, inner_r_kvs) } @@ -715,14 +717,14 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_value() { - Value::RecordType(kts) => kts, + let kts_x = match l_type.to_valuef() { + ValueF::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, + let kts_y = match r_type.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -745,10 +747,10 @@ fn type_last_layer( kts_l_inner: &TypedThunk, kts_r_inner: &TypedThunk| -> Result { - match (kts_l_inner.to_value(), kts_r_inner.to_value()) { + match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { ( - Value::RecordType(kvs_l_inner), - Value::RecordType(kvs_r_inner), + ValueF::RecordType(kvs_l_inner), + ValueF::RecordType(kvs_r_inner), ) => { combine_record_types(ctx, kvs_l_inner, kvs_r_inner) } @@ -774,8 +776,8 @@ fn type_last_layer( }; // 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()?.to_valuef() { + ValueF::Const(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -784,8 +786,8 @@ fn type_last_layer( }; // 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()?.to_valuef() { + ValueF::Const(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -806,8 +808,8 @@ fn type_last_layer( }; // Extract the LHS record type - let kts_x = match l.to_value() { - Value::RecordType(kts) => kts, + let kts_x = match l.to_valuef() { + ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -816,8 +818,8 @@ fn type_last_layer( }; // Extract the RHS record type - let kts_y = match r.to_value() { - Value::RecordType(kts) => kts, + let kts_y = match r.to_valuef() { + ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -831,8 +833,8 @@ fn type_last_layer( .and(Ok(RetTypeOnly(Typed::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.to_value() { - Value::AppliedBuiltin(List, _) => {} + match l.get_type()?.to_valuef() { + ValueF::AppliedBuiltin(List, _) => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), } @@ -893,13 +895,13 @@ fn type_last_layer( Ok(RetTypeOnly(t)) } Merge(record, union, type_annot) => { - let handlers = match record.get_type()?.to_value() { - Value::RecordType(kts) => kts, + let handlers = match record.get_type()?.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), }; - let variants = match union.get_type()?.to_value() { - Value::UnionType(kts) => kts, + let variants = match union.get_type()?.to_valuef() { + ValueF::UnionType(kts) => kts, _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), }; @@ -910,8 +912,8 @@ fn type_last_layer( 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) => { + let (x, tx, tb) = match &handler_type.to_valuef() { + ValueF::Pi(x, tx, tb) => { (x.clone(), tx.to_type(), tb.to_type()) } _ => return Err(mkerr(NotAFunction(handler_type))), @@ -973,8 +975,8 @@ fn type_last_layer( } Projection(record, labels) => { let trecord = record.get_type()?; - let kts = match trecord.to_value() { - Value::RecordType(kts) => kts, + let kts = match trecord.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(ProjectionMustBeRecord)), }; @@ -988,7 +990,7 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_thunk_and_type( - Value::RecordType(new_kts).into_thunk(), + ValueF::RecordType(new_kts).into_thunk(), trecord.get_type()?.into_owned(), ) .to_type(), diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index a277977..49fd40e 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -125,7 +125,7 @@ pub use value::Value; // A Dhall value. pub mod value { use dhall::core::thunk::{Thunk, TypedThunk}; - use dhall::core::value::Value as DhallValue; + use dhall::core::value::ValueF as DhallValue; use dhall::phase::{NormalizedSubExpr, Parsed, Type, Typed}; use dhall_syntax::Builtin; @@ -162,7 +162,7 @@ pub mod value { /// Assumes that the given value has type `Type`. pub(crate) fn make_simple_type(v: DhallValue) -> Self { - Value(Typed::from_value_and_type(v, Type::const_type())) + Value(Typed::from_valuef_and_type(v, Type::const_type())) } pub(crate) fn make_builtin_type(b: Builtin) -> Self { Self::make_simple_type(DhallValue::from_builtin(b)) -- cgit v1.3.1 From 6753a1f97bb674d91dd4d42f2ddb25a8119e070d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 17 Aug 2019 19:00:43 +0200 Subject: s/Thunk/Value/ --- dhall/src/core/context.rs | 14 +- dhall/src/core/mod.rs | 2 +- dhall/src/core/thunk.rs | 406 ------------------------ dhall/src/core/value.rs | 723 ++++++++++++++++++++++--------------------- dhall/src/core/valuef.rs | 405 ++++++++++++++++++++++++ dhall/src/phase/mod.rs | 26 +- dhall/src/phase/normalize.rs | 208 +++++++------ dhall/src/phase/typecheck.rs | 68 ++-- serde_dhall/src/lib.rs | 17 +- 9 files changed, 936 insertions(+), 933 deletions(-) delete mode 100644 dhall/src/core/thunk.rs create mode 100644 dhall/src/core/valuef.rs (limited to 'serde_dhall') diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index b1fbde9..e1a23a9 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -3,8 +3,8 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; -use crate::core::thunk::Thunk; -use crate::core::value::ValueF; +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}; @@ -12,7 +12,7 @@ use crate::phase::{Type, Typed}; #[derive(Debug, Clone)] enum CtxItem { Kept(AlphaVar, Type), - Replaced(Thunk, Type), + Replaced(Value, Type), } #[derive(Debug, Clone)] @@ -31,7 +31,7 @@ impl TypecheckContext { let mut vec = self.0.as_ref().clone(); vec.push(( x.clone(), - CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()), + CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()), )); Ok(TypecheckContext(Rc::new(vec))) } @@ -44,11 +44,11 @@ impl TypecheckContext { let i = i.under_multiple_binders(&shift_map); let (th, t) = match i { CtxItem::Kept(newvar, t) => { - (ValueF::Var(newvar).into_thunk(), t) + (ValueF::Var(newvar).into_value(), t) } CtxItem::Replaced(th, t) => (th, t), }; - return Some(Typed::from_thunk_and_type(th, t)); + return Some(Typed::from_value_and_type(th, t)); } Some(newvar) => var = newvar, }; @@ -133,7 +133,7 @@ impl Subst for CtxItem { ), CtxItem::Kept(v, t) => match v.shift(-1, var) { None => { - CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val)) + CtxItem::Replaced(val.to_value(), t.subst_shift(var, val)) } Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), }, 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 325a410..0000000 --- a/dhall/src/core/thunk.rs +++ /dev/null @@ -1,406 +0,0 @@ -use std::borrow::Cow; -use std::cell::{Ref, RefCell, RefMut}; -use std::rc::Rc; - -use dhall_syntax::{Const, ExprF}; - -use crate::core::context::TypecheckContext; -use crate::core::value::ValueF; -use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_one_layer, 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, Clone)] -enum ThunkInternal { - /// Partially normalized value whose subexpressions have been thunked (this is returned from - /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no - /// requirement of WHNF here. - PartialExpr(ExprF), - /// Partially normalized value. - /// Invariant: if the marker is `NF`, the value must be fully normalized - ValueF(Marker, ValueF), -} - -#[derive(Debug)] -struct TypedThunkInternal { - internal: ThunkInternal, - typ: Option, -} - -/// 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 the typechecking phase to preserve type information through -/// the normalization phase. -#[derive(Clone)] -pub struct Thunk(Rc>); - -#[derive(Debug, Clone)] -pub struct TypedThunk(Thunk); - -impl ThunkInternal { - fn into_thunk(self, t: Option) -> Thunk { - TypedThunkInternal { - internal: self, - typ: t, - } - .into_thunk() - } - - fn normalize_whnf(&mut self) { - match self { - ThunkInternal::PartialExpr(e) => { - *self = - ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone())) - } - // Already at least in WHNF - ThunkInternal::ValueF(_, _) => {} - } - } - - fn normalize_nf(&mut self) { - match self { - ThunkInternal::PartialExpr(_) => { - self.normalize_whnf(); - self.normalize_nf(); - } - ThunkInternal::ValueF(m @ WHNF, v) => { - v.normalize_mut(); - *m = NF; - } - // Already in NF - ThunkInternal::ValueF(NF, _) => {} - } - } - - // Always use normalize_whnf before - fn as_whnf(&self) -> &ValueF { - match self { - ThunkInternal::PartialExpr(_) => unreachable!(), - ThunkInternal::ValueF(_, v) => v, - } - } - - // Always use normalize_nf before - fn as_nf(&self) -> &ValueF { - match self { - ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { - unreachable!() - } - ThunkInternal::ValueF(NF, v) => v, - } - } -} - -impl TypedThunkInternal { - fn into_thunk(self) -> Thunk { - Thunk(Rc::new(RefCell::new(self))) - } - fn as_internal(&self) -> &ThunkInternal { - &self.internal - } - fn as_internal_mut(&mut self) -> &mut ThunkInternal { - &mut self.internal - } - - fn get_type(&self) -> Result { - match &self.typ { - Some(t) => Ok(t.clone()), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - } - } -} - -impl Thunk { - pub(crate) fn from_valuef(v: ValueF) -> Thunk { - ThunkInternal::ValueF(WHNF, v).into_thunk(None) - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Thunk { - ThunkInternal::ValueF(WHNF, v).into_thunk(Some(t)) - } - pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { - ThunkInternal::PartialExpr(e).into_thunk(None) - } - pub(crate) fn with_type(self, t: Type) -> Thunk { - self.as_internal().clone().into_thunk(Some(t)) - } - - /// Mutates the contents. If no one else shares this thunk, - /// mutates directly, thus avoiding a RefCell lock. - fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedThunkInternal)) { - 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_tinternal_mut()), - } - } - - /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this thunk - pub(crate) fn normalize_mut(&mut self) { - self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) - } - - fn as_tinternal(&self) -> Ref { - self.0.borrow() - } - fn as_tinternal_mut(&mut self) -> RefMut { - self.0.borrow_mut() - } - fn as_internal(&self) -> Ref { - Ref::map(self.as_tinternal(), TypedThunkInternal::as_internal) - } - fn as_internal_mut(&self) -> RefMut { - RefMut::map(self.0.borrow_mut(), TypedThunkInternal::as_internal_mut) - } - - fn do_normalize_whnf(&self) { - let borrow = self.as_internal(); - match &*borrow { - ThunkInternal::PartialExpr(_) => { - drop(borrow); - self.as_internal_mut().normalize_whnf(); - } - // Already at least in WHNF - ThunkInternal::ValueF(_, _) => {} - } - } - - fn do_normalize_nf(&self) { - let borrow = self.as_internal(); - match &*borrow { - ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { - drop(borrow); - self.as_internal_mut().normalize_nf(); - } - // Already in NF - ThunkInternal::ValueF(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 { - self.do_normalize_nf(); - Ref::map(self.as_internal(), 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_valuef(&self) -> Ref { - self.do_normalize_whnf(); - Ref::map(self.as_internal(), ThunkInternal::as_whnf) - } - - pub(crate) fn to_valuef(&self) -> ValueF { - self.as_valuef().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: ValueF) -> ValueF { - self.app_thunk(val.into_thunk()) - } - - pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF { - apply_any(self.clone(), th) - } - - pub(crate) fn get_type(&self) -> Result, TypeError> { - Ok(Cow::Owned(self.as_tinternal().get_type()?)) - } -} - -impl TypedThunk { - pub(crate) fn from_valuef(v: ValueF) -> TypedThunk { - TypedThunk::from_thunk_untyped(Thunk::from_valuef(v)) - } - - pub(crate) fn from_type(t: Type) -> TypedThunk { - t.into_typethunk() - } - - pub(crate) fn normalize_nf(&self) -> ValueF { - self.0.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(th.with_type(t)) - } - pub fn from_thunk_simple_type(th: Thunk) -> Self { - TypedThunk::from_thunk_and_type(th, Type::const_type()) - } - pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - TypedThunk(th) - } - pub(crate) fn from_const(c: Const) -> Self { - match type_of_const(c) { - Ok(t) => TypedThunk::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => TypedThunk::from_valuef(ValueF::Const(c)), - } - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { - TypedThunk(Thunk::from_valuef_and_type(v, t)) - } - - pub(crate) fn to_valuef(&self) -> ValueF { - self.0.to_valuef() - } - pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_valuef().normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_valuef().normalize_to_expr_maybe_alpha(true) - } - pub(crate) fn to_thunk(&self) -> Thunk { - self.0.clone() - } - 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 { - // TODO: avoid clone - match &self.to_valuef() { - ValueF::Const(c) => Some(*c), - _ => None, - } - } - - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() - } - - pub(crate) fn get_type(&self) -> Result, TypeError> { - self.0.get_type() - } -} - -impl Shift for Thunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Thunk(self.0.shift(delta, var)?)) - } -} - -impl Shift for ThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ThunkInternal::PartialExpr(e) => { - ThunkInternal::PartialExpr(e.shift(delta, var)?) - } - ThunkInternal::ValueF(m, v) => { - ThunkInternal::ValueF(*m, v.shift(delta, var)?) - } - }) - } -} - -impl Shift for TypedThunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedThunk(self.0.shift(delta, var)?)) - } -} - -impl Shift for TypedThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedThunkInternal { - internal: self.internal.shift(delta, var)?, - typ: self.typ.shift(delta, var)?, - }) - } -} - -impl Subst for Thunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Thunk(self.0.subst_shift(var, val)) - } -} - -impl Subst for ThunkInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - ThunkInternal::PartialExpr(e) => { - ThunkInternal::PartialExpr(e.subst_shift(var, val)) - } - ThunkInternal::ValueF(_, v) => { - // The resulting value may not stay in normal form after substitution - ThunkInternal::ValueF(WHNF, v.subst_shift(var, val)) - } - } - } -} - -impl Subst for TypedThunkInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypedThunkInternal { - internal: self.internal.subst_shift(var, val), - typ: self.typ.subst_shift(var, val), - } - } -} - -impl Subst for TypedThunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypedThunk(self.0.subst_shift(var, val)) - } -} - -impl std::cmp::PartialEq for Thunk { - fn eq(&self, other: &Self) -> bool { - *self.as_valuef() == *other.as_valuef() - } -} -impl std::cmp::Eq for Thunk {} - -impl std::cmp::PartialEq for TypedThunk { - fn eq(&self, other: &Self) -> bool { - self.to_valuef() == other.to_valuef() - } -} -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.as_internal(); - match b { - ThunkInternal::ValueF(m, v) => { - f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() - } - ThunkInternal::PartialExpr(e) => { - f.debug_tuple("Thunk@PartialExpr").field(e).finish() - } - } - } -} diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index da70118..5c29bf0 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,405 +1,406 @@ -use std::collections::HashMap; - -use dhall_syntax::{ - rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -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}; - -/// 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 `ValueF`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 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. -/// 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 ValueF { - /// Closures - Lam(AlphaLabel, TypedThunk, Thunk), - Pi(AlphaLabel, TypedThunk, TypedThunk), - // Invariant: the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec), - - 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), - RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), - // Invariant: this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(TypedThunk, TypedThunk), - // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), +use std::borrow::Cow; +use std::cell::{Ref, RefCell, RefMut}; +use std::rc::Rc; + +use dhall_syntax::{Const, ExprF}; + +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_one_layer, 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}; -impl ValueF { - pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_valuef(self) - } +#[derive(Debug, Clone)] +enum ValueInternal { + /// Partially normalized value whose subexpressions have been thunked (this is returned from + /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no + /// requirement of WHNF here. + PartialExpr(ExprF), + /// Partially normalized value. + /// Invariant: if the marker is `NF`, the value must be fully normalized + ValueF(Marker, ValueF), +} - /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { - self.normalize_to_expr_maybe_alpha(false) +#[derive(Debug)] +struct TypedValueInternal { + internal: ValueInternal, + typ: Option, +} + +/// 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 through +/// normalization. +#[derive(Clone)] +pub struct Value(Rc>); + +#[derive(Debug, Clone)] +pub struct TypedValue(Value); + +impl ValueInternal { + fn into_value(self, t: Option) -> Value { + TypedValueInternal { + internal: self, + typ: t, + } + .into_value() } - /// 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 { + + fn normalize_whnf(&mut self) { 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 + ValueInternal::PartialExpr(e) => { + *self = + ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone())) } - 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))) + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} + } + } + + fn normalize_nf(&mut self) { + match self { + ValueInternal::PartialExpr(_) => { + self.normalize_whnf(); + self.normalize_nf(); } - 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())) + ValueInternal::ValueF(m @ WHNF, v) => { + v.normalize_mut(); + *m = NF; } - 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(), - )) + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } + } + + // Always use normalize_whnf before + fn as_whnf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) => unreachable!(), + ValueInternal::ValueF(_, v) => v, + } + } + + // Always use normalize_nf before + fn as_nf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + unreachable!() } - 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), + ValueInternal::ValueF(NF, v) => v, + } + } +} + +impl TypedValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_internal(&self) -> &ValueInternal { + &self.internal + } + fn as_internal_mut(&mut self) -> &mut ValueInternal { + &mut self.internal + } + + fn get_type(&self) -> Result { + match &self.typ { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, )), - ValueF::PartialExpr(e) => { - rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) - } } } +} +impl Value { + pub(crate) fn from_valuef(v: ValueF) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(None) + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(Some(t)) + } + pub(crate) fn from_partial_expr(e: ExprF) -> Value { + ValueInternal::PartialExpr(e).into_value(None) + } + pub(crate) fn with_type(self, t: Type) -> Value { + self.as_internal().clone().into_value(Some(t)) + } + + /// Mutates the contents. If no one else shares this thunk, + /// mutates directly, thus avoiding a RefCell lock. + fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedValueInternal)) { + 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_tinternal_mut()), + } + } + + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this thunk 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(); - } + self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) + } - 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(); - }); - } + fn as_tinternal(&self) -> Ref { + self.0.borrow() + } + fn as_tinternal_mut(&mut self) -> RefMut { + self.0.borrow_mut() + } + fn as_internal(&self) -> Ref { + Ref::map(self.as_tinternal(), TypedValueInternal::as_internal) + } + fn as_internal_mut(&self) -> RefMut { + RefMut::map(self.0.borrow_mut(), TypedValueInternal::as_internal_mut) + } + + fn do_normalize_whnf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) => { + drop(borrow); + self.as_internal_mut().normalize_whnf(); + } + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} } } - /// Apply to a value - pub(crate) fn app(self, val: ValueF) -> ValueF { - self.app_val(val) + fn do_normalize_nf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + drop(borrow); + self.as_internal_mut().normalize_nf(); + } + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } } - /// Apply to a value - pub(crate) fn app_val(self, val: ValueF) -> ValueF { - self.app_thunk(val.into_thunk()) + // 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 { + self.do_normalize_nf(); + Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> ValueF { - Thunk::from_valuef(self).app_thunk(th) + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you could run into BorrowMut panics + pub(crate) fn as_valuef(&self) -> Ref { + self.do_normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_whnf) } - pub fn from_builtin(b: Builtin) -> ValueF { - ValueF::AppliedBuiltin(b, vec![]) + pub(crate) fn to_valuef(&self) -> ValueF { + self.as_valuef().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_valuef(&self, val: ValueF) -> ValueF { + self.app_value(val.into_value()) + } + + pub(crate) fn app_value(&self, th: Value) -> ValueF { + apply_any(self.clone(), th) + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + Ok(Cow::Owned(self.as_tinternal().get_type()?)) } } -impl Shift for ValueF { +impl TypedValue { + pub(crate) fn from_valuef(v: ValueF) -> TypedValue { + TypedValue::from_value_untyped(Value::from_valuef(v)) + } + + pub(crate) fn from_type(t: Type) -> TypedValue { + t.into_typedvalue() + } + + pub(crate) fn normalize_nf(&self) -> ValueF { + self.0.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_value_and_type(th: Value, t: Type) -> Self { + TypedValue(th.with_type(t)) + } + pub fn from_value_simple_type(th: Value) -> Self { + TypedValue::from_value_and_type(th, Type::const_type()) + } + pub(crate) fn from_value_untyped(th: Value) -> Self { + TypedValue(th) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => TypedValue::from_valuef(ValueF::Const(c)), + } + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + TypedValue(Value::from_valuef_and_type(v, t)) + } + + pub(crate) fn to_valuef(&self) -> ValueF { + self.0.to_valuef() + } + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr() + } + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr_maybe_alpha(true) + } + pub(crate) fn to_value(&self) -> Value { + self.0.clone() + } + pub(crate) fn to_type(&self) -> Type { + self.clone().into_typed().into_type() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_typedvalue(self) + } + pub(crate) fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_valuef() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } + + pub(crate) fn normalize_mut(&mut self) { + self.0.normalize_mut() + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + self.0.get_type() + } +} + +impl Shift for Value { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(Value(self.0.shift(delta, var)?)) + } +} + +impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { 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)?) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.shift(delta, var)?) } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.shift(delta, var)?) + ValueInternal::ValueF(m, v) => { + ValueInternal::ValueF(*m, v.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 for ValueF { +impl Shift for TypedValue { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValue(self.0.shift(delta, var)?)) + } +} + +impl Shift for TypedValueInternal { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValueInternal { + internal: self.internal.shift(delta, var)?, + typ: self.typ.shift(delta, var)?, + }) + } +} + +impl Subst for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + Value(self.0.subst_shift(var, val)) + } +} + +impl Subst for ValueInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - // Retry normalizing since substituting may allow progress - ValueF::AppliedBuiltin(b, args) => { - apply_builtin(*b, args.subst_shift(var, val)) - } - // Retry normalizing since substituting may allow progress - ValueF::PartialExpr(e) => { - normalize_one_layer(e.subst_shift(var, val)) - } - // Retry normalizing since substituting may allow progress - ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( - elts.iter().map(|contents| contents.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_valuef(), - 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)) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.subst_shift(var, val)) } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.subst_shift(var, val)) + ValueInternal::ValueF(_, v) => { + // The resulting value may not stay in normal form after substitution + ValueInternal::ValueF(WHNF, v.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)) + } + } +} + +impl Subst for TypedValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValueInternal { + internal: self.internal.subst_shift(var, val), + typ: self.typ.subst_shift(var, val), + } + } +} + +impl Subst for TypedValue { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValue(self.0.subst_shift(var, val)) + } +} + +impl std::cmp::PartialEq for Value { + fn eq(&self, other: &Self) -> bool { + *self.as_valuef() == *other.as_valuef() + } +} +impl std::cmp::Eq for Value {} + +impl std::cmp::PartialEq for TypedValue { + fn eq(&self, other: &Self) -> bool { + self.to_valuef() == other.to_valuef() + } +} +impl std::cmp::Eq for TypedValue {} + +impl std::fmt::Debug for Value { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let b: &ValueInternal = &self.as_internal(); + match b { + ValueInternal::ValueF(m, v) => { + f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish() } - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + ValueInternal::PartialExpr(e) => { + f.debug_tuple("Value@PartialExpr").field(e).finish() } - 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/valuef.rs b/dhall/src/core/valuef.rs new file mode 100644 index 0000000..bea2e2e --- /dev/null +++ b/dhall/src/core/valuef.rs @@ -0,0 +1,405 @@ +use std::collections::HashMap; + +use dhall_syntax::{ + rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, +}; + +use crate::core::value::{TypedValue, Value}; +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}; + +/// 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 `ValueF`s. In particular, `subst_shift` could break +/// the invariants so need to be careful to reevaluate as needed. +/// Subexpressions are Values, which are partially evaluated expressions that are normalized +/// on-demand. 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. +/// 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 ValueF { + /// Closures + Lam(AlphaLabel, TypedValue, Value), + Pi(AlphaLabel, TypedValue, TypedValue), + // Invariant: the evaluation must not be able to progress further. + AppliedBuiltin(Builtin, Vec), + + Var(AlphaVar), + Const(Const), + BoolLit(bool), + NaturalLit(Natural), + IntegerLit(Integer), + DoubleLit(NaiveDouble), + EmptyOptionalLit(TypedValue), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(TypedValue), + NEListLit(Vec), + RecordLit(HashMap), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(TypedValue, TypedValue), + // Invariant: this must not contain a value captured by one of the variants above. + PartialExpr(ExprF), +} + +impl ValueF { + pub(crate) fn into_value(self) -> Value { + Value::from_valuef(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 value + pub(crate) fn app(self, val: ValueF) -> ValueF { + self.app_valuef(val) + } + + /// Apply to a value + pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { + self.app_value(val.into_value()) + } + + /// Apply to a thunk + pub fn app_value(self, th: Value) -> ValueF { + Value::from_valuef(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 { + 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 for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + match self { + // Retry normalizing since substituting may allow progress + ValueF::AppliedBuiltin(b, args) => { + apply_builtin(*b, args.subst_shift(var, val)) + } + // Retry normalizing since substituting may allow progress + ValueF::PartialExpr(e) => { + normalize_one_layer(e.subst_shift(var, val)) + } + // Retry normalizing since substituting may allow progress + ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( + elts.iter().map(|contents| contents.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_valuef(), + 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/phase/mod.rs b/dhall/src/phase/mod.rs index 7e74f95..c18f976 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::ValueF; +use crate::core::value::{TypedValue, 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(TypedValue); /// A normalized expression. /// @@ -92,19 +92,19 @@ 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_value_and_type(th: Value, t: Type) -> Self { + Typed(TypedValue::from_value_and_type(th, t)) } - pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - Typed(TypedThunk::from_thunk_untyped(th)) + pub(crate) fn from_value_untyped(th: Value) -> Self { + Typed(TypedValue::from_value_untyped(th)) } pub(crate) fn from_const(c: Const) -> Self { - Typed(TypedThunk::from_const(c)) + Typed(TypedValue::from_const(c)) } pub fn from_valuef_and_type(v: ValueF, t: Type) -> Self { - Typed(TypedThunk::from_valuef_and_type(v, t)) + Typed(TypedValue::from_valuef_and_type(v, t)) } - pub(crate) fn from_typethunk(th: TypedThunk) -> Self { + pub(crate) fn from_typedvalue(th: TypedValue) -> Self { Typed(th) } pub fn const_type() -> Self { @@ -120,8 +120,8 @@ impl Typed { pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.0.to_expr_alpha() } - pub fn to_thunk(&self) -> Thunk { - self.0.to_thunk() + pub fn to_value(&self) -> Value { + self.0.to_value() } // Deprecated pub fn to_type(&self) -> Type { @@ -131,7 +131,7 @@ impl Typed { pub(crate) fn into_type(self) -> Type { self } - pub(crate) fn into_typethunk(self) -> TypedThunk { + pub(crate) fn into_typedvalue(self) -> TypedValue { self.0 } pub(crate) fn to_normalized(&self) -> Normalized { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index da54726..93f2528 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,8 +5,8 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::ValueF; +use crate::core::value::{TypedValue, Value}; +use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr, Typed}; @@ -20,45 +20,45 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - ValueF::Var(var).into_thunk() + ValueF::Var(var).into_value() }}; // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { ValueF::Lam( Label::from(stringify!($var)).into(), - TypedThunk::from_thunk_simple_type( + TypedValue::from_value_simple_type( make_closure!($($ty)*), ), make_closure!($($rest)*), - ).into_thunk() + ).into_value() }; - (Natural) => { ValueF::from_builtin(Builtin::Natural).into_thunk() }; + (Natural) => { ValueF::from_builtin(Builtin::Natural).into_value() }; (List $($rest:tt)*) => { ValueF::from_builtin(Builtin::List) - .app_thunk(make_closure!($($rest)*)) - .into_thunk() + .app_value(make_closure!($($rest)*)) + .into_value() }; (Some $($rest:tt)*) => { - ValueF::NEOptionalLit(make_closure!($($rest)*)).into_thunk() + ValueF::NEOptionalLit(make_closure!($($rest)*)).into_value() }; (1 + $($rest:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Thunk::from_valuef(ValueF::NaturalLit(1)), - )).into_thunk() + Value::from_valuef(ValueF::NaturalLit(1)), + )).into_value() }; ([ $($head:tt)* ] # $($tail:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::ListAppend, - ValueF::NEListLit(vec![make_closure!($($head)*)]).into_thunk(), + ValueF::NEListLit(vec![make_closure!($($head)*)]).into_value(), make_closure!($($tail)*), - )).into_thunk() + )).into_value() }; } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { +pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { use dhall_syntax::Builtin::*; use ValueF::*; @@ -66,7 +66,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { let ret = match (b, args.as_slice()) { (OptionalNone, [t, r..]) => Ok(( r, - EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())), + EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())), )), (NaturalIsZero, [n, r..]) => match &*n.as_valuef() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), @@ -189,10 +189,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedThunk::from_valuef(ValueF::from_builtin(Natural)), + TypedValue::from_valuef(ValueF::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); - Ok((r, EmptyListLit(TypedThunk::from_valuef(RecordType(kts))))) + Ok((r, EmptyListLit(TypedValue::from_valuef(RecordType(kts))))) } NEListLit(xs) => { let xs = xs @@ -201,9 +201,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { .map(|(i, e)| { let i = NaturalLit(i); let mut kvs = HashMap::new(); - kvs.insert("index".into(), Thunk::from_valuef(i)); + kvs.insert("index".into(), Value::from_valuef(i)); kvs.insert("value".into(), e.clone()); - Thunk::from_valuef(RecordLit(kvs)) + Value::from_valuef(RecordLit(kvs)) }) .collect(); Ok((r, NEListLit(xs))) @@ -222,8 +222,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => Ok(( r, - f.app_val(ValueF::from_builtin(List).app_thunk(t.clone())) - .app_thunk({ + f.app_valuef(ValueF::from_builtin(List).app_value(t.clone())) + .app_value({ // Move `t` under new `x` variable let t1 = t.under_binder(Label::from("x")); make_closure!( @@ -232,9 +232,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { [ var(x, 1) ] # var(xs, 0) ) }) - .app_val(EmptyListLit(TypedThunk::from_thunk_simple_type( - t.clone(), - ))), + .app_valuef(EmptyListLit( + TypedValue::from_value_simple_type(t.clone()), + )), )), }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() { @@ -244,9 +244,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { 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(); } Ok((r, v.to_valuef())) } @@ -264,17 +264,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => Ok(( r, - f.app_val(ValueF::from_builtin(Optional).app_thunk(t.clone())) - .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0))) - .app_val(EmptyOptionalLit( - TypedThunk::from_thunk_simple_type(t.clone()), - )), + f.app_valuef( + ValueF::from_builtin(Optional).app_value(t.clone()), + ) + .app_value(make_closure!(λ(x: #t) -> Some var(x, 0))) + .app_valuef(EmptyOptionalLit( + TypedValue::from_value_simple_type(t.clone()), + )), )), }, (OptionalFold, [_, v, _, just, nothing, r..]) => { match &*v.as_valuef() { EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())), - NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))), + NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), _ => Err(()), } } @@ -290,9 +292,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => Ok(( r, - f.app_val(ValueF::from_builtin(Natural)) - .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) - .app_val(NaturalLit(0)), + f.app_valuef(ValueF::from_builtin(Natural)) + .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app_valuef(NaturalLit(0)), )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() { @@ -300,10 +302,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { NaturalLit(n) => { 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()); + Ok((r, succ.app_valuef(fold))) } _ => Err(()), }, @@ -313,7 +315,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { 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 } @@ -321,13 +323,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } } -pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF { - let fallback = |f: Thunk, a: Thunk| ValueF::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_valuef(); match &*f_borrow { ValueF::Lam(x, _, e) => { - let val = Typed::from_thunk_untyped(a); + let val = Typed::from_value_untyped(a); e.subst_shift(&x.into(), &val).to_valuef() } ValueF::AppliedBuiltin(b, args) => { @@ -346,15 +348,15 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF { } pub(crate) fn squash_textlit( - elts: impl Iterator>, -) -> Vec> { + elts: impl Iterator>, +) -> Vec> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator>, + elts: impl Iterator>, crnt_str: &mut String, - ret: &mut Vec>, + ret: &mut Vec>, ) { for contents in elts { match contents { @@ -390,9 +392,9 @@ pub(crate) fn squash_textlit( // Small helper enum to avoid repetition enum Ret<'a> { ValueF(ValueF), - Thunk(Thunk), - ThunkRef(&'a Thunk), - Expr(ExprF), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF), } /// Performs an intersection of two HashMaps. @@ -508,7 +510,7 @@ where kvs } -fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { +fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, @@ -521,46 +523,46 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { let x_borrow = x.as_valuef(); let y_borrow = y.as_valuef(); Some(match (o, &*x_borrow, &*y_borrow) { - (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y), - (BoolAnd, _, BoolLit(true)) => 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::ThunkRef(x), + (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::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), + (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::ThunkRef(y), - (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x), + (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::ThunkRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x), + (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), + (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { Ret::ValueF(NaturalLit(x + y)) } (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)), (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), - (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y), - (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x), + (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), + (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { Ret::ValueF(NaturalLit(x * y)) } - (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x), + (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), _) 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()), )), @@ -580,10 +582,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (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(); @@ -595,14 +597,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (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_partial_expr(ExprF::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), @@ -612,18 +614,18 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (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_untyped(Thunk::from_partial_expr( + TypedValue::from_value_untyped(Value::from_partial_expr( ExprF::BinOp( RecursiveRecordTypeMerge, - v1.to_thunk(), - v2.to_thunk(), + v1.to_value(), + v2.to_value(), ), )) }); @@ -631,15 +633,15 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { } (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence( - TypedThunk::from_thunk_simple_type(x.clone()), - TypedThunk::from_thunk_simple_type(y.clone()), + TypedValue::from_value_simple_type(x.clone()), + TypedValue::from_value_simple_type(y.clone()), )), _ => return None, }) } -pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { +pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, @@ -652,21 +654,21 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { ), 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::ValueF(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e)) + Ret::ValueF(Lam(x.into(), TypedValue::from_value_untyped(t), e)) } ExprF::Pi(x, t, e) => Ret::ValueF(Pi( x.into(), - TypedThunk::from_thunk_untyped(t), - TypedThunk::from_thunk_untyped(e), + TypedValue::from_value_untyped(t), + TypedValue::from_value_untyped(e), )), ExprF::Let(x, _, v, b) => { - let v = Typed::from_thunk_untyped(v); - Ret::Thunk(b.subst_shift(&x.into(), &v)) + let v = Typed::from_value_untyped(v); + Ret::Value(b.subst_shift(&x.into(), &v)) } - ExprF::App(v, a) => Ret::ValueF(v.app_thunk(a)), + 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)), @@ -680,7 +682,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { Ret::ValueF(EmptyListLit( - TypedThunk::from_thunk_simple_type(args[0].clone()), + TypedValue::from_value_simple_type(args[0].clone()), )) } _ => { @@ -697,12 +699,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { } ExprF::RecordType(kts) => Ret::ValueF(RecordType( kts.into_iter() - .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t))) + .map(|(k, t)| (k, TypedValue::from_value_untyped(t))) .collect(), )), ExprF::UnionType(kts) => Ret::ValueF(UnionType( kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t)))) + .map(|(k, t)| (k, t.map(|t| TypedValue::from_value_untyped(t)))) .collect(), )), ExprF::TextLit(elts) => { @@ -710,7 +712,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { 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::ValueF(TextLit(elts)) } @@ -718,15 +720,15 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { ExprF::BoolIf(ref b, ref e1, ref e2) => { let b_borrow = b.as_valuef(); 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_valuef(); let e2_borrow = e2.as_valuef(); 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); @@ -765,7 +767,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { let v_borrow = v.as_valuef(); 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) @@ -786,7 +788,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { let variant_borrow = variant.as_valuef(); 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); @@ -794,7 +796,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::ValueF(h.app_thunk(v.clone())), + Some(h) => Ret::ValueF(h.app_value(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); @@ -812,8 +814,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { match ret { Ret::ValueF(v) => v, - Ret::Thunk(th) => th.to_valuef(), - Ret::ThunkRef(th) => th.to_valuef(), + Ret::Value(th) => th.to_valuef(), + Ret::ValueRef(th) => th.to_valuef(), Ret::Expr(expr) => ValueF::PartialExpr(expr), } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 8d7a3bc..4154afe 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -5,8 +5,8 @@ use dhall_syntax::{ }; use crate::core::context::TypecheckContext; -use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::ValueF; +use crate::core::value::{TypedValue, Value}; +use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::{Normalized, Resolved, Type, Typed}; @@ -42,13 +42,13 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Typed::from_thunk_and_type( + Ok(Typed::from_value_and_type( ValueF::Pi( x.into(), - TypedThunk::from_type(tx), - TypedThunk::from_type(te), + TypedValue::from_type(tx), + TypedValue::from_type(te), ) - .into_thunk(), + .into_value(), Type::from_const(k), )) } @@ -80,15 +80,15 @@ fn tck_record_type( return Err(TypeError::new(ctx, RecordTypeDuplicateField)) } Entry::Vacant(_) => { - entry.or_insert_with(|| TypedThunk::from_type(t.clone())) + entry.or_insert_with(|| TypedValue::from_type(t.clone())) } }; } // An empty record type has type Type let k = k.unwrap_or(dhall_syntax::Const::Type); - Ok(Typed::from_thunk_and_type( - ValueF::RecordType(new_kts).into_thunk(), + Ok(Typed::from_value_and_type( + ValueF::RecordType(new_kts).into_value(), Type::from_const(k), )) } @@ -122,7 +122,7 @@ fn tck_union_type( return Err(TypeError::new(ctx, UnionTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| { - t.as_ref().map(|t| TypedThunk::from_type(t.clone())) + t.as_ref().map(|t| TypedValue::from_type(t.clone())) }), }; } @@ -131,8 +131,8 @@ fn tck_union_type( // an union type with only unary variants also has type Type let k = k.unwrap_or(dhall_syntax::Const::Type); - Ok(Typed::from_thunk_and_type( - ValueF::UnionType(new_kts).into_thunk(), + Ok(Typed::from_value_and_type( + ValueF::UnionType(new_kts).into_value(), Type::from_const(k), )) } @@ -337,12 +337,12 @@ fn type_with( let b = type_with(&ctx2, b.clone())?; let v = ValueF::Lam( x.clone().into(), - TypedThunk::from_type(tx.clone()), - b.to_thunk(), + TypedValue::from_type(tx.clone()), + b.to_value(), ); 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_valuef(v), t) + Typed::from_value_and_type(Value::from_valuef(v), t) } Pi(x, ta, tb) => { let ta = mktype(ctx, ta.clone())?; @@ -380,9 +380,9 @@ fn type_with( 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), + let expr = expr.map_ref(|typed| typed.to_value()); + Typed::from_value_and_type( + Value::from_partial_expr(expr), typ, ) } @@ -505,10 +505,10 @@ fn type_last_layer( } Ok(RetTypeOnly( - Typed::from_thunk_and_type( + Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) .app(t.to_valuef()) - .into_thunk(), + .into_value(), Typed::from_const(Type), ) .to_type(), @@ -524,10 +524,10 @@ fn type_last_layer( } Ok(RetTypeOnly( - Typed::from_thunk_and_type( + Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) .app(t.to_valuef()) - .into_thunk(), + .into_value(), Typed::from_const(Type).into_type(), ) .to_type(), @@ -662,8 +662,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { use crate::phase::normalize::outer_join; @@ -671,8 +671,8 @@ fn type_last_layer( // 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| + inner_l: &TypedValue, + inner_r: &TypedValue| -> Result { match (inner_l.to_valuef(), inner_r.to_valuef()) { ( @@ -690,7 +690,7 @@ fn type_last_layer( let kts: HashMap> = outer_join( |l| Ok(l.to_type()), |r| Ok(r.to_type()), - |k: &Label, l: &TypedThunk, r: &TypedThunk| { + |k: &Label, l: &TypedValue, r: &TypedValue| { combine(k, l, r) }, &kts_l, @@ -735,8 +735,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { use crate::phase::normalize::intersection_with_key; @@ -744,8 +744,8 @@ fn type_last_layer( // 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| + kts_l_inner: &TypedValue, + kts_r_inner: &TypedValue| -> Result { match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { ( @@ -761,7 +761,7 @@ fn type_last_layer( }; let kts = intersection_with_key( - |k: &Label, l: &TypedThunk, r: &TypedThunk| { + |k: &Label, l: &TypedValue, r: &TypedValue| { combine(k, l, r) }, &kts_l, @@ -989,8 +989,8 @@ fn type_last_layer( } Ok(RetTypeOnly( - Typed::from_thunk_and_type( - ValueF::RecordType(new_kts).into_thunk(), + Typed::from_value_and_type( + ValueF::RecordType(new_kts).into_value(), trecord.get_type()?.into_owned(), ) .to_type(), diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index 49fd40e..48f311e 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -124,8 +124,9 @@ pub use value::Value; // A Dhall value. pub mod value { - use dhall::core::thunk::{Thunk, TypedThunk}; - use dhall::core::value::ValueF as DhallValue; + use dhall::core::value::TypedValue as TypedThunk; + use dhall::core::value::Value as Thunk; + use dhall::core::valuef::ValueF as DhallValue; use dhall::phase::{NormalizedSubExpr, Parsed, Type, Typed}; use dhall_syntax::Builtin; @@ -153,8 +154,8 @@ pub mod value { pub(crate) fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() } - pub(crate) fn to_thunk(&self) -> Thunk { - self.0.to_thunk() + pub(crate) fn to_value(&self) -> Thunk { + self.0.to_value() } pub(crate) fn to_type(&self) -> Type { self.0.to_type() @@ -170,12 +171,12 @@ pub mod value { pub(crate) fn make_optional_type(t: Value) -> Self { Self::make_simple_type( DhallValue::from_builtin(Builtin::Optional) - .app_thunk(t.to_thunk()), + .app_value(t.to_value()), ) } pub(crate) fn make_list_type(t: Value) -> Self { Self::make_simple_type( - DhallValue::from_builtin(Builtin::List).app_thunk(t.to_thunk()), + DhallValue::from_builtin(Builtin::List).app_value(t.to_value()), ) } // Made public for the StaticType derive macro @@ -185,7 +186,7 @@ pub mod value { ) -> Self { Self::make_simple_type(DhallValue::RecordType( kts.map(|(k, t)| { - (k.into(), TypedThunk::from_thunk_simple_type(t.to_thunk())) + (k.into(), TypedThunk::from_value_simple_type(t.to_value())) }) .collect(), )) @@ -199,7 +200,7 @@ pub mod value { ( k.into(), t.map(|t| { - TypedThunk::from_thunk_simple_type(t.to_thunk()) + TypedThunk::from_value_simple_type(t.to_value()) }), ) }) -- cgit v1.3.1 From 26a1fd0f0861038a76a0f9b09eaef16d808d4139 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 21:52:26 +0200 Subject: Use TypedValue instead of Typed in normalize and typecheck Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized --- dhall/src/core/context.rs | 29 ++-- dhall/src/core/value.rs | 48 +++--- dhall/src/core/valuef.rs | 6 +- dhall/src/error/mod.rs | 55 +++--- dhall/src/phase/mod.rs | 51 ++---- dhall/src/phase/normalize.rs | 6 +- dhall/src/phase/typecheck.rs | 392 +++++++++++++++++++------------------------ dhall/src/tests.rs | 2 +- serde_dhall/src/lib.rs | 10 +- 9 files changed, 260 insertions(+), 339 deletions(-) (limited to 'serde_dhall') diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index e1a23a9..851e4c4 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -3,16 +3,15 @@ use std::rc::Rc; use dhall_syntax::{Label, V}; -use crate::core::value::Value; +use crate::core::value::{TypedValue, 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 { - Kept(AlphaVar, Type), - Replaced(Value, Type), + Kept(AlphaVar, TypedValue), + Replaced(Value, TypedValue), } #[derive(Debug, Clone)] @@ -22,12 +21,16 @@ impl TypecheckContext { pub fn new() -> Self { TypecheckContext(Rc::new(Vec::new())) } - pub fn insert_type(&self, x: &Label, t: Type) -> Self { + pub fn insert_type(&self, x: &Label, t: TypedValue) -> Self { let mut vec = self.0.as_ref().clone(); vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); TypecheckContext(Rc::new(vec)) } - pub fn insert_value(&self, x: &Label, e: Typed) -> Result { + pub fn insert_value( + &self, + x: &Label, + e: TypedValue, + ) -> Result { let mut vec = self.0.as_ref().clone(); vec.push(( x.clone(), @@ -35,7 +38,7 @@ impl TypecheckContext { )); Ok(TypecheckContext(Rc::new(vec))) } - pub fn lookup(&self, var: &V