diff options
Diffstat (limited to 'dhall/src/semantics/tck')
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 22 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 31 |
2 files changed, 28 insertions, 25 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 5492b8b..0a27f32 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -49,6 +49,9 @@ impl TyExpr { pub fn kind(&self) -> &TyExprKind { &*self.kind } + pub fn span(&self) -> &Span { + &self.span + } pub fn get_type(&self) -> Result<Type, TypeError> { match &self.ty { Some(t) => Ok(t.clone()), @@ -69,17 +72,18 @@ impl TyExpr { tyexpr_to_expr(self, opts, &mut env) } - pub fn normalize_whnf(&self, env: &NzEnv) -> Value { - normalize_tyexpr_whnf(self, env) - } - pub fn normalize_whnf_noenv(&self) -> Value { - self.normalize_whnf(&NzEnv::new()) + /// Eval the TyExpr. It will actually get evaluated only as needed on demand. + pub fn eval(&self, env: &NzEnv) -> Value { + Value::new_thunk(env, self.clone()) } - pub fn normalize_nf(&self, env: &NzEnv) -> Value { - self.normalize_whnf(env) + /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as + /// needed on demand. + pub fn eval_closed_expr(&self) -> Value { + self.eval(&NzEnv::new()) } - pub fn normalize_nf_noenv(&self) -> Value { - self.normalize_nf(&NzEnv::new()) + /// Eval a closed TyExpr fully and recursively; + pub fn rec_eval_closed_expr(&self) -> Value { + normalize_tyexpr_whnf(self, &NzEnv::new()) } } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index bc1c87f..d741b40 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -74,7 +74,7 @@ fn type_one_layer( ExprKind::Builtin(b) => { let t_expr = type_of_builtin(*b); let t_tyexpr = type_with(env, &t_expr)?; - t_tyexpr.normalize_whnf(env.as_nzenv()) + t_tyexpr.eval(env.as_nzenv()) } ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural), @@ -93,7 +93,7 @@ fn type_one_layer( text_type } ExprKind::EmptyListLit(t) => { - let t = t.normalize_nf(env.as_nzenv()); + let t = t.eval(env.as_nzenv()); match &*t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, @@ -196,7 +196,7 @@ fn type_one_layer( }, // TODO: branch here only when scrut.get_type() is a Const _ => { - let scrut_nf = scrut.normalize_nf(env.as_nzenv()); + let scrut_nf = scrut.eval(env.as_nzenv()); let scrut_nf_borrow = scrut_nf.kind(); match &*scrut_nf_borrow { ValueKind::UnionType(kts) => match kts.get(x) { @@ -224,7 +224,7 @@ fn type_one_layer( } } ExprKind::Annot(x, t) => { - let t = t.normalize_whnf(env.as_nzenv()); + let t = t.eval(env.as_nzenv()); let x_ty = x.get_type()?; if x_ty != t { return mkerr(format!( @@ -243,7 +243,7 @@ fn type_one_layer( x_ty } ExprKind::Assert(t) => { - let t = t.normalize_whnf(env.as_nzenv()); + let t = t.eval(env.as_nzenv()); match &*t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), @@ -268,7 +268,7 @@ fn type_one_layer( )); } - let arg_nf = arg.normalize_nf(env.as_nzenv()); + let arg_nf = arg.eval(env.as_nzenv()); closure.apply(arg_nf) } _ => return mkerr(format!("apply to not Pi")), @@ -329,11 +329,11 @@ fn type_one_layer( ); let ty = type_one_layer(env, &ekind)?; TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial) - .normalize_nf(env.as_nzenv()) + .eval(env.as_nzenv()) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - let x_val = x.normalize_whnf(env.as_nzenv()); - let y_val = y.normalize_whnf(env.as_nzenv()); + let x_val = x.eval(env.as_nzenv()); + let y_val = y.eval(env.as_nzenv()); let x_val_borrow = x_val.kind(); let y_val_borrow = y_val.kind(); let kts_x = match &*x_val_borrow { @@ -478,9 +478,8 @@ fn type_one_layer( } } - let type_annot = type_annot - .as_ref() - .map(|t| t.normalize_whnf(env.as_nzenv())); + let type_annot = + type_annot.as_ref().map(|t| t.eval(env.as_nzenv())); match (inferred_type, type_annot) { (Some(t1), Some(t2)) => { if t1 != t2 { @@ -542,7 +541,7 @@ pub(crate) fn type_with( }, ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot)?; - let annot_nf = annot.normalize_nf(env.as_nzenv()); + let annot_nf = annot.eval(env.as_nzenv()); let body_env = env.insert_type(&binder, annot_nf.clone()); let body = type_with(&body_env, body)?; let body_ty = body.get_type()?; @@ -555,7 +554,7 @@ pub(crate) fn type_with( Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?), Span::Artificial, ); - let ty = ty.normalize_whnf(env.as_nzenv()); + let ty = ty.eval(env.as_nzenv()); ( TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), Some(ty), @@ -563,7 +562,7 @@ pub(crate) fn type_with( } ExprKind::Pi(binder, annot, body) => { let annot = type_with(env, annot)?; - let annot_nf = annot.normalize_whnf(env.as_nzenv()); + let annot_nf = annot.eval(env.as_nzenv()); let body = type_with(&env.insert_type(binder, annot_nf.clone()), body)?; let ty = type_of_function(annot.get_type()?, body.get_type()?)?; @@ -580,7 +579,7 @@ pub(crate) fn type_with( }; let val = type_with(env, &val)?; - let val_nf = val.normalize_nf(&env.as_nzenv()); + let val_nf = val.eval(&env.as_nzenv()); let body = type_with(&env.insert_value(&binder, val_nf), body)?; let body_ty = body.get_type().ok(); ( |