diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 71 |
1 files changed, 58 insertions, 13 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 4c844ee..c881a9a 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,9 +4,11 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::Binder; -use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; +use crate::semantics::phase::normalize::{ + apply_any, normalize_tyexpr_whnf, normalize_whnf, +}; use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; -use crate::semantics::{type_of_builtin, TyExpr, TyExprKind}; +use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -47,6 +49,14 @@ pub(crate) enum Form { WHNF, } +/// An unevaluated subexpression +#[derive(Debug, Clone)] +pub(crate) struct Thunk { + env: NzEnv, + body: TyExpr, +} + +/// An unevaluated subexpression that takes an argument. #[derive(Debug, Clone)] pub(crate) enum Closure { /// Normal closure @@ -99,6 +109,8 @@ pub(crate) enum ValueKind<Value> { Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprKind<Value, Normalized>), + // Invariant: absent in whnf + Thunk(Thunk), } impl Value { @@ -120,6 +132,15 @@ impl Value { } .into_value() } + pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { + ValueInternal { + form: Unevaled, + kind: ValueKind::Thunk(Thunk::new(env, tye.clone())), + ty: tye.get_type().ok(), + span: tye.span().clone(), + } + .into_value() + } pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Value) -> Value { Value::new(v, Unevaled, t, Span::Artificial) } @@ -147,9 +168,7 @@ impl Value { pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { Value::from_kind_and_type( ValueKind::from_builtin_env(b, env.clone()), - crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) - .unwrap() - .normalize_whnf_noenv(), + typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(), ) } @@ -325,6 +344,7 @@ impl Value { v.to_tyexpr(venv), )) } + ValueKind::Thunk(th) => return th.to_tyexpr(venv), self_kind => { let self_kind = self_kind.map_ref(|v| v.to_tyexpr(venv)); let expr = match self_kind { @@ -333,7 +353,8 @@ impl Value { | ValueKind::PiClosure { .. } | ValueKind::AppliedBuiltin(..) | ValueKind::UnionConstructor(..) - | ValueKind::UnionLit(..) => unreachable!(), + | ValueKind::UnionLit(..) + | ValueKind::Thunk(..) => unreachable!(), ValueKind::Const(c) => ExprKind::Const(c), ValueKind::BoolLit(b) => ExprKind::BoolLit(b), ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n), @@ -501,6 +522,9 @@ impl ValueKind<Value> { ValueKind::PartialExpr(e) => { e.map_mut(Value::normalize_mut); } + ValueKind::Thunk(..) => { + unreachable!("Should only normalize_mut values in WHNF") + } } } @@ -553,6 +577,22 @@ impl<V> ValueKind<V> { } } +impl Thunk { + pub fn new(env: &NzEnv, body: TyExpr) -> Self { + Thunk { + env: env.clone(), + body, + } + } + + pub fn eval(&self) -> Value { + normalize_tyexpr_whnf(&self.body, &self.env) + } + pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + self.eval().to_tyexpr(venv) + } +} + impl Closure { pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self { Closure::Closure { @@ -572,11 +612,9 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { match self { Closure::Closure { env, body, .. } => { - body.normalize_whnf(&env.insert_value(val)) - } - Closure::ConstantClosure { env, body, .. } => { - body.normalize_whnf(env) + body.eval(&env.insert_value(val)) } + Closure::ConstantClosure { env, body, .. } => body.eval(env), } } fn apply_var(&self, var: NzVar) -> Value { @@ -588,9 +626,7 @@ impl Closure { ); self.apply(val) } - Closure::ConstantClosure { env, body, .. } => { - body.normalize_whnf(env) - } + Closure::ConstantClosure { env, body, .. } => body.eval(env), } } @@ -626,6 +662,15 @@ impl std::cmp::PartialEq for Value { } impl std::cmp::Eq for Value {} +impl std::cmp::PartialEq for Thunk { + fn eq(&self, _other: &Self) -> bool { + unreachable!( + "Trying to compare thunks but we should only compare WHNFs" + ) + } +} +impl std::cmp::Eq for Thunk {} + impl std::cmp::PartialEq for Closure { fn eq(&self, other: &Self) -> bool { let v = NzVar::fresh(); |