diff options
Diffstat (limited to 'dhall/src/semantics/nze')
| -rw-r--r-- | dhall/src/semantics/nze/env.rs | 23 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 8 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 60 |
3 files changed, 53 insertions, 38 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 0b22a8b..261e0b6 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, Value, ValueKind}; +use crate::semantics::{AlphaVar, Type, Value, ValueKind}; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) enum NzVar { @@ -11,9 +11,9 @@ pub(crate) enum NzVar { #[derive(Debug, Clone)] enum NzEnvItem { // Variable is bound with given type - Kept(Value), + Kept(Type), // Variable has been replaced by corresponding value - Replaced(Value), + Replaced(Value, Type), } #[derive(Debug, Clone)] @@ -49,28 +49,31 @@ impl NzEnv { NzEnv { items: Vec::new() } } - pub fn insert_type(&self, t: Value) -> Self { + pub fn insert_type(&self, ty: Type) -> Self { let mut env = self.clone(); - env.items.push(NzEnvItem::Kept(t)); + env.items.push(NzEnvItem::Kept(ty)); env } - pub fn insert_value(&self, e: Value) -> Self { + pub fn insert_value(&self, e: Value, ty: Type) -> Self { let mut env = self.clone(); - env.items.push(NzEnvItem::Replaced(e)); + env.items.push(NzEnvItem::Replaced(e, ty)); env } + pub fn insert_value_noty(&self, e: Value) -> Self { + let ty = e.get_type_not_sort(); + self.insert_value(e, ty) + } pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), - NzEnvItem::Replaced(x) => x.kind().clone(), + NzEnvItem::Replaced(x, _) => x.kind().clone(), } } pub fn lookup_ty(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) => ty.clone(), - NzEnvItem::Replaced(x) => x.get_type().unwrap(), + NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(), } } } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index a00b7ff..3a981f4 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -17,14 +17,14 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { closure.apply(a).to_whnf_check_type(ty) } ValueKind::AppliedBuiltin(closure) => { - closure.apply(a, f.get_type().unwrap(), ty) + closure.apply(a, f.get_type_not_sort(), ty) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), a, kts.clone(), uniont.clone(), - f.get_type().unwrap(), + f.get_type_not_sort(), ), _ => ValueKind::PartialExpr(ExprKind::App(f, a)), } @@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer( UnionType(kts) => Ret::ValueKind(UnionConstructor( l.clone(), kts.clone(), - v.get_type().unwrap(), + v.get_type_not_sort(), )), PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, @@ -536,7 +536,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - body.eval(&env.insert_value(val)).kind().clone() + body.eval(&env.insert_value_noty(val)).kind().clone() } TyExprKind::Expr(e) => { let ty = match tye.get_type() { diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 607aa0d..203b479 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -3,13 +3,11 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::lazy; -use crate::semantics::Binder; use crate::semantics::{ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, - TyEnv, + type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv, + NzVar, TyEnv, TyExpr, TyExprKind, VarEnv, }; -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, NaiveDouble, Natural, Span, @@ -119,11 +117,14 @@ impl Value { ) .into_value() } + pub(crate) fn const_kind() -> Value { + Value::from_const(Const::Kind) + } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal::from_thunk( Thunk::new(env, tye.clone()), - tye.get_type().ok(), + Some(Value::const_kind()), tye.span().clone(), ) .into_value() @@ -137,24 +138,31 @@ impl Value { let env = NzEnv::new(); ValueInternal::from_thunk( Thunk::from_partial_expr(env, e, ty.clone()), - Some(ty), + Some(Value::const_kind()), Span::Artificial, ) .into_value() } /// Make a Value from a ValueKind pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value() + ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial) + .into_value() } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); match c { - Const::Type => { - Value::from_kind_and_type(v, Value::from_const(Const::Kind)) - } - Const::Kind => { - Value::from_kind_and_type(v, Value::from_const(Const::Sort)) - } + Const::Type => ValueInternal::from_whnf( + v, + Some(Value::from_const(Const::Kind)), + Span::Artificial, + ) + .into_value(), + Const::Kind => ValueInternal::from_whnf( + v, + Some(Value::const_sort()), + Span::Artificial, + ) + .into_value(), Const::Sort => Value::const_sort(), } } @@ -226,14 +234,10 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let body_t = match &*self.get_type_not_sort().kind() { - ValueKind::PiClosure { annot, closure, .. } => { - v.check_type(annot); - closure.apply(v.clone()) - } - _ => unreachable!("Internal type error"), - }; - Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t) + Value::from_kind_and_type( + apply_any(self.clone(), v, &Value::const_kind()), + Value::const_kind(), + ) } /// In debug mode, panic if the provided type doesn't match the value's type. @@ -246,12 +250,16 @@ impl Value { // "Internal type error" // ); } - pub(crate) fn get_type(&self) -> Result<Value, TypeError> { + pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> { + let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv); + type_with(tyenv, &expr).unwrap().get_type() + } + pub(crate) fn get_type_noenv(&self) -> Result<Value, TypeError> { Ok(self.0.get_type()?.clone()) } /// When we know the value isn't `Sort`, this gets the type directly pub(crate) fn get_type_not_sort(&self) -> Value { - self.get_type() + self.get_type_noenv() .expect("Internal type error: value is `Sort` but shouldn't be") } @@ -366,6 +374,10 @@ impl Value { TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone()) } + pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { + let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv); + type_with(tyenv, &expr).unwrap() + } pub fn to_tyexpr_noenv(&self) -> TyExpr { self.to_tyexpr(VarEnv::new()) } @@ -522,7 +534,7 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { match self { Closure::Closure { env, body, .. } => { - body.eval(&env.insert_value(val)) + body.eval(&env.insert_value_noty(val)) } Closure::ConstantClosure { body, .. } => body.clone(), } |