From d65d639ff93691adbf0a208edb99736003bc64bd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:05:26 +0000 Subject: Factor some tck code to avoid needing get_type_tyexpr --- dhall/src/semantics/hir.rs | 4 +- dhall/src/semantics/nze/normalize.rs | 2 +- dhall/src/semantics/nze/value.rs | 4 +- dhall/src/semantics/tck/tyexpr.rs | 12 ++-- dhall/src/semantics/tck/typecheck.rs | 118 ++++++++++++++++++++++------------- 5 files changed, 88 insertions(+), 52 deletions(-) (limited to 'dhall') diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs index e4e2a5f..42f151e 100644 --- a/dhall/src/semantics/hir.rs +++ b/dhall/src/semantics/hir.rs @@ -76,8 +76,8 @@ impl Hir { } /// Eval the Hir. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: &NzEnv) -> Value { - Value::new_thunk(env.clone(), self.clone()) + pub fn eval(&self, env: impl Into) -> Value { + Value::new_thunk(env.into(), self.clone()) } /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as /// needed on demand. diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 4111190..c8dd5ae 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -475,7 +475,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { } HirKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - body.eval(&env.insert_value(val, ())).kind().clone() + body.eval(env.insert_value(val, ())).kind().clone() } HirKind::Expr(e) => { let e = e.map_ref(|hir| hir.eval(env)); diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 0603fb5..3a5b5b5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -87,7 +87,7 @@ pub(crate) enum ValueKind { UnionLit(Label, Value, HashMap>), TextLit(TextLit), Equivalence(Value, Value), - /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? + /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. PartialExpr(ExprKind), } @@ -387,7 +387,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(val, ())) } Closure::ConstantClosure { body, .. } => body.clone(), } diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index c7b8009..dfb4397 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -26,13 +26,15 @@ impl TyExpr { pub fn ty(&self) -> &Type { &self.ty } - pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result { - Ok(self.ty().to_hir(env.as_varenv()).typecheck(env)?) - } /// Get the kind (the type of the type) of this value // TODO: avoid recomputing so much pub fn get_kind(&self, env: &TyEnv) -> Result, TypeError> { - Ok(self.get_type_tyexpr(env)?.ty().as_const()) + Ok(self + .ty() + .to_hir(env.as_varenv()) + .typecheck(env)? + .ty() + .as_const()) } pub fn to_hir(&self) -> Hir { @@ -48,7 +50,7 @@ impl TyExpr { /// Eval the TyExpr. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: impl Into) -> Value { - self.as_hir().eval(&env.into()) + self.as_hir().eval(env.into()) } /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as /// needed on demand. diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 377b97e..a8a2d95 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -12,6 +12,38 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, }; +fn check_rectymerge( + span: &Span, + env: &TyEnv, + x: Type, + y: Type, +) -> Result<(), TypeError> { + let kts_x = match x.kind() { + ValueKind::RecordType(kts) => kts, + _ => { + return mk_span_err( + span.clone(), + "RecordTypeMergeRequiresRecordType", + ) + } + }; + let kts_y = match y.kind() { + ValueKind::RecordType(kts) => kts, + _ => { + return mk_span_err( + span.clone(), + "RecordTypeMergeRequiresRecordType", + ) + } + }; + for (k, tx) in kts_x { + if let Some(ty) = kts_y.get(k) { + check_rectymerge(span, env, tx.clone(), ty.clone())?; + } + } + Ok(()) +} + fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { Const::Type @@ -51,11 +83,39 @@ fn type_one_layer( | ExprKind::Annot(..) => unreachable!(), // Handled in type_with ExprKind::Lam(binder, annot, body) => { - let body_ty = body.get_type_tyexpr( - &env.insert_type(&binder.clone(), annot.eval(env)), - )?; - let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); - type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env) + if annot.ty().as_const().is_none() { + return mkerr( + ErrorBuilder::new(format!( + "Invalid input type: `{}`", + annot.ty().to_expr_tyenv(env), + )) + .span_err( + annot.span(), + format!( + "this has type: `{}`", + annot.ty().to_expr_tyenv(env) + ), + ) + .help(format!( + "The input type of a function must have type `Type`, \ + `Kind` or `Sort`", + )) + .format(), + ); + } + let body_env = env.insert_type(&binder, annot.eval(env)); + if body.get_kind(&body_env)?.is_none() { + return span_err("Invalid output type"); + } + Hir::new( + HirKind::Expr(ExprKind::Pi( + binder.clone(), + annot.to_hir(), + body.ty().to_hir(body_env.as_varenv()), + )), + span.clone(), + ) + .eval(env) } ExprKind::Pi(_, annot, body) => { let ks = match annot.ty().as_const() { @@ -348,45 +408,19 @@ fn type_one_layer( Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - let ekind = ExprKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - x.get_type_tyexpr(env)?, - y.get_type_tyexpr(env)?, - ); - type_one_layer(env, ekind, None, span.clone())?.eval(env) + check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?; + + Hir::new( + HirKind::Expr(ExprKind::BinOp( + BinOp::RecursiveRecordTypeMerge, + x.ty().to_hir(env.as_varenv()), + y.ty().to_hir(env.as_varenv()), + )), + span.clone(), + ) + .eval(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - fn check_rectymerge( - span: &Span, - env: &TyEnv, - x: Type, - y: Type, - ) -> Result<(), TypeError> { - let kts_x = match x.kind() { - ValueKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - let kts_y = match y.kind() { - ValueKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - for (k, tx) in kts_x { - if let Some(ty) = kts_y.get(k) { - check_rectymerge(span, env, tx.clone(), ty.clone())?; - } - } - Ok(()) - } check_rectymerge(&span, env, x.eval(env), y.eval(env))?; // A RecordType's type is always a const -- cgit v1.2.3