diff options
Diffstat (limited to 'dhall/src')
-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 | ||||
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 8 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 56 |
5 files changed, 88 insertions, 67 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(), } diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 1fc711c..b3e7895 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -104,16 +104,16 @@ impl TyEnv { &self.names } - pub fn insert_type(&self, x: &Label, t: Type) -> Self { + pub fn insert_type(&self, x: &Label, ty: Type) -> Self { TyEnv { names: self.names.insert(x), - items: self.items.insert_type(t), + items: self.items.insert_type(ty), } } - pub fn insert_value(&self, x: &Label, e: Value) -> Self { + pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self { TyEnv { names: self.names.insert(x), - items: self.items.insert_value(e), + items: self.items.insert_value(e, ty), } } pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index dd9a8fa..ceb83de 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -72,7 +72,9 @@ fn type_one_layer( ExprKind::Lam(binder, annot, body) => { let body_ty = body.get_type()?; - let body_ty = body_ty.to_tyexpr(env.as_varenv().insert()); + let body_ty = body_ty.to_tyexpr_tyenv( + &env.insert_type(&binder.clone(), annot.eval(env.as_nzenv())), + ); let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); type_one_layer(env, pi_ekind, Span::Artificial)? .eval(env.as_nzenv()) @@ -154,7 +156,7 @@ fn type_one_layer( } } let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Const::Type) { + if t.get_type(env)?.as_const() != Some(Const::Type) { return span_err("InvalidListType"); } @@ -162,7 +164,7 @@ fn type_one_layer( } ExprKind::SomeLit(x) => { let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Const::Type) { + if t.get_type(env)?.as_const() != Some(Const::Type) { return span_err("InvalidOptionalType"); } @@ -183,8 +185,7 @@ fn type_one_layer( let ty = type_of_recordtype( span.clone(), - kts.iter() - .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))), + kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), )?; Value::from_kind_and_type(ValueKind::RecordType(kts), ty) } @@ -278,13 +279,13 @@ fn type_one_layer( return span_err(&format!( "annot mismatch: ({} : {}) : {}", x.to_expr_tyenv(env), - x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env), - t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env) + x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env), + t.to_tyexpr_tyenv(env).to_expr_tyenv(env) )); // return span_err(format!( // "annot mismatch: {} != {}", - // x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env), - // t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env) + // x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env), + // t.to_tyexpr_tyenv(env).to_expr_tyenv(env) // )); // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,)); } @@ -352,10 +353,9 @@ fn type_one_layer( if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.get_type()?.get_type()?.as_const() != Some(Const::Type) { - return span_err("IfBranchMustBeTerm"); - } - if z.get_type()?.get_type()?.as_const() != Some(Const::Type) { + let y_ty = y.get_type()?; + let y_ty = y_ty.to_tyexpr_tyenv(env); + if y_ty.get_type()?.as_const() != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.get_type()? != z.get_type()? { @@ -388,16 +388,15 @@ fn type_one_layer( // Construct the final record type let ty = type_of_recordtype( span.clone(), - kts.iter() - .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))), + kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), )?; Value::from_kind_and_type(ValueKind::RecordType(kts), ty) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - x.get_type()?.to_tyexpr(env.as_varenv()), - y.get_type()?.to_tyexpr(env.as_varenv()), + x.get_type()?.to_tyexpr_tyenv(env), + y.get_type()?.to_tyexpr_tyenv(env), ); type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv()) } @@ -418,8 +417,8 @@ fn type_one_layer( env, ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - tx.to_tyexpr(env.as_varenv()), - ty.to_tyexpr(env.as_varenv()), + tx.to_tyexpr_tyenv(env), + ty.to_tyexpr_tyenv(env), ), Span::Artificial, )?; @@ -451,7 +450,9 @@ fn type_one_layer( if l.get_type()? != r.get_type()? { return span_err("EquivalenceTypeMismatch"); } - if l.get_type()?.get_type()?.as_const() != Some(Const::Type) { + if l.get_type()?.to_tyexpr_tyenv(env).get_type()?.as_const() + != Some(Const::Type) + { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -668,7 +669,7 @@ fn type_one_layer( annot_val } else { let entry_type = kts.iter().next().unwrap().1.clone(); - if entry_type.get_type()?.as_const() != Some(Const::Type) { + if entry_type.get_type(env)?.as_const() != Some(Const::Type) { return span_err( "`toMap` only accepts records of type `Type`", ); @@ -724,7 +725,7 @@ fn type_one_layer( Value::from_kind_and_type( ValueKind::RecordType(new_kts), - record_type.get_type()?, + record_type.get_type(env)?, ) } ExprKind::ProjectionByExpr(record, selection) => { @@ -804,7 +805,12 @@ pub(crate) fn type_with( (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } ExprKind::Embed(p) => { - return Ok(p.clone().into_value().to_tyexpr_noenv()) + let val = p.clone().into_value(); + ( + val.to_tyexpr_noenv().kind().clone(), + Some(val.get_type(&TyEnv::new())?), + ) + // return Ok(p.clone().into_value().to_tyexpr_noenv()) } ekind => { let ekind = match ekind { @@ -829,9 +835,9 @@ pub(crate) fn type_with( val.clone() }; let val = type_with(env, &val)?; - val.get_type()?; // Ensure val is not Sort + let val_ty = val.get_type()?; let val_nf = val.eval(&env.as_nzenv()); - let body_env = env.insert_value(&binder, val_nf); + let body_env = env.insert_value(&binder, val_nf, val_ty); let body = type_with(&body_env, body)?; ExprKind::Let(binder.clone(), None, val, body) } |