From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:35:54 +0000 Subject: Remove most reliance on types stored in Value --- dhall/src/semantics/tck/typecheck.rs | 56 ++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 25 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') 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) } -- cgit v1.2.3 From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:58:48 +0000 Subject: Remove move type propagation through Value --- dhall/src/semantics/tck/typecheck.rs | 42 +++++++++++------------------------- 1 file changed, 12 insertions(+), 30 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index ceb83de..810e483 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -183,11 +183,11 @@ fn type_one_layer( }; } - let ty = type_of_recordtype( + type_of_recordtype( span.clone(), kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), )?; - Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -247,22 +247,11 @@ fn type_one_layer( ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { - // Can't fail because uniontypes must have type Const(_). - let kt = scrut.get_type()?.as_const().unwrap(); - // The type of the field must be Const smaller than `kt`, thus the - // function type has type `kt`. - let pi_ty = Value::from_const(kt); - - Value::from_kind_and_type( - ValueKind::PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant( - scrut_nf, - ), - }, - pi_ty, - ) + Value::from_kind(ValueKind::PiClosure { + binder: Binder::new(x.clone()), + annot: ty.clone(), + closure: Closure::new_constant(scrut_nf), + }) } Some(None) => scrut_nf, None => return span_err("MissingUnionField"), @@ -386,11 +375,11 @@ fn type_one_layer( })?; // Construct the final record type - let ty = type_of_recordtype( + type_of_recordtype( span.clone(), kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), )?; - Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( @@ -685,12 +674,8 @@ fn type_one_layer( let mut kts = HashMap::new(); kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); - let output_type = Value::from_builtin(Builtin::List).app( - Value::from_kind_and_type( - ValueKind::RecordType(kts), - Value::from_const(Const::Type), - ), - ); + let output_type = Value::from_builtin(Builtin::List) + .app(Value::from_kind(ValueKind::RecordType(kts))); if let Some(annot) = annot { let annot_val = annot.eval(env.as_nzenv()); if output_type != annot_val { @@ -723,10 +708,7 @@ fn type_one_layer( }; } - Value::from_kind_and_type( - ValueKind::RecordType(new_kts), - record_type.get_type(env)?, - ) + Value::from_kind(ValueKind::RecordType(new_kts)) } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.get_type()?; -- cgit v1.2.3 From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:53:55 +0000 Subject: Remove most TyExpr from normalization --- dhall/src/semantics/tck/typecheck.rs | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 810e483..5b233f8 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -266,17 +266,10 @@ fn type_one_layer( let x_ty = x.get_type()?; if x_ty != t { return span_err(&format!( - "annot mismatch: ({} : {}) : {}", - x.to_expr_tyenv(env), - x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env), - t.to_tyexpr_tyenv(env).to_expr_tyenv(env) + "annot mismatch: {} != {}", + x_ty.to_expr_tyenv(env), + t.to_expr_tyenv(env) )); - // return span_err(format!( - // "annot mismatch: {} != {}", - // 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,)); } x_ty } -- cgit v1.2.3 From a709c65eb28f1b6a666f15bfc2255da7bc7105ab Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:38:37 +0000 Subject: Resolve variables alongside import resolution --- dhall/src/semantics/tck/typecheck.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 5b233f8..eb6a58c 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -43,7 +43,7 @@ fn function_check(a: Const, b: Const) -> Const { } } -fn mkerr(x: S) -> Result { +pub fn mkerr(x: S) -> Result { Err(TypeError::new(TypeMessage::Custom(x.to_string()))) } -- cgit v1.2.3 From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:58:28 +0000 Subject: Take Hir for typecheck --- dhall/src/semantics/tck/typecheck.rs | 60 +++++++++++++++++------------------- 1 file changed, 28 insertions(+), 32 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index eb6a58c..ac113cd 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,11 +5,11 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr, - TyExprKind, Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv, + TyExpr, TyExprKind, Type, Value, ValueKind, }; use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span, }; use crate::Normalized; @@ -115,8 +115,8 @@ fn type_one_layer( ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), ExprKind::Builtin(b) => { - let t_expr = type_of_builtin(*b); - let t_tyexpr = type_with(env, &t_expr)?; + let t_hir = type_of_builtin(*b); + let t_tyexpr = typecheck(&t_hir)?; t_tyexpr.eval(env.as_nzenv()) } ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), @@ -761,25 +761,16 @@ fn type_one_layer( } /// `type_with` typechecks an expressio in the provided environment. -pub(crate) fn type_with( - env: &TyEnv, - expr: &Expr, -) -> Result { - let (tyekind, ty) = match expr.as_ref() { - ExprKind::Var(var) => match env.lookup(&var) { - Some((v, ty)) => (TyExprKind::Var(v), Some(ty)), - None => { - return mkerr( - ErrorBuilder::new(format!("unbound variable `{}`", var)) - .span_err(expr.span(), "not found in this scope") - .format(), - ) - } - }, - ExprKind::Const(Const::Sort) => { +pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { + let (tyekind, ty) = match hir.kind() { + HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))), + HirKind::Expr(ExprKind::Var(_)) => { + unreachable!("Hir should contain no unresolved variables") + } + HirKind::Expr(ExprKind::Const(Const::Sort)) => { (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } - ExprKind::Embed(p) => { + HirKind::Expr(ExprKind::Embed(p)) => { let val = p.clone().into_value(); ( val.to_tyexpr_noenv().kind().clone(), @@ -787,7 +778,7 @@ pub(crate) fn type_with( ) // return Ok(p.clone().into_value().to_tyexpr_noenv()) } - ekind => { + HirKind::Expr(ekind) => { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot)?; @@ -805,7 +796,13 @@ pub(crate) fn type_with( } ExprKind::Let(binder, annot, val, body) => { let val = if let Some(t) = annot { - t.rewrap(ExprKind::Annot(val.clone(), t.clone())) + Hir::new( + HirKind::Expr(ExprKind::Annot( + val.clone(), + t.clone(), + )), + t.span(), + ) } else { val.clone() }; @@ -818,16 +815,16 @@ pub(crate) fn type_with( } _ => ekind.traverse_ref(|e| type_with(env, e))?, }; - return type_one_layer(env, ekind, expr.span()); + return type_one_layer(env, ekind, hir.span()); } }; - Ok(TyExpr::new(tyekind, ty, expr.span())) + Ok(TyExpr::new(tyekind, ty, hir.span())) } /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck(e: &Expr) -> Result { +pub(crate) fn typecheck(e: &Hir) -> Result { let res = type_with(&TyEnv::new(), e)?; // Ensure that the inferred type exists (i.e. this is not Sort) res.get_type()?; @@ -835,9 +832,8 @@ pub(crate) fn typecheck(e: &Expr) -> Result { } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. -pub(crate) fn typecheck_with( - expr: &Expr, - ty: Expr, -) -> Result { - typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty))) +pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { + let hir = + Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span()); + typecheck(&hir) } -- cgit v1.2.3 From f6732982c522dd579d378ab4820001d5ae107c43 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:18:32 +0000 Subject: Automate conversion between envs --- dhall/src/semantics/tck/typecheck.rs | 38 +++++++++++++++++------------------- 1 file changed, 18 insertions(+), 20 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index ac113cd..7f02832 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -73,11 +73,10 @@ fn type_one_layer( ExprKind::Lam(binder, annot, body) => { let body_ty = body.get_type()?; let body_ty = body_ty.to_tyexpr_tyenv( - &env.insert_type(&binder.clone(), annot.eval(env.as_nzenv())), + &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, Span::Artificial)? - .eval(env.as_nzenv()) + type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env) } ExprKind::Pi(_, annot, body) => { let ks = match annot.get_type()?.as_const() { @@ -117,7 +116,7 @@ fn type_one_layer( ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); let t_tyexpr = typecheck(&t_hir)?; - t_tyexpr.eval(env.as_nzenv()) + t_tyexpr.eval(env) } ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural), @@ -136,7 +135,7 @@ fn type_one_layer( text_type } ExprKind::EmptyListLit(t) => { - let t = t.eval(env.as_nzenv()); + let t = t.eval(env); match &*t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, @@ -242,7 +241,7 @@ fn type_one_layer( }, // TODO: branch here only when scrut.get_type() is a Const _ => { - let scrut_nf = scrut.eval(env.as_nzenv()); + let scrut_nf = scrut.eval(env); match scrut_nf.kind() { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > @@ -262,7 +261,7 @@ fn type_one_layer( } } ExprKind::Annot(x, t) => { - let t = t.eval(env.as_nzenv()); + let t = t.eval(env); let x_ty = x.get_type()?; if x_ty != t { return span_err(&format!( @@ -274,7 +273,7 @@ fn type_one_layer( x_ty } ExprKind::Assert(t) => { - let t = t.eval(env.as_nzenv()); + let t = t.eval(env); match &*t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => { @@ -315,7 +314,7 @@ fn type_one_layer( ); } - let arg_nf = arg.eval(env.as_nzenv()); + let arg_nf = arg.eval(env); closure.apply(arg_nf) } _ => return mkerr( @@ -380,11 +379,11 @@ fn type_one_layer( 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()) + type_one_layer(env, ekind, Span::Artificial)?.eval(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - let x_val = x.eval(env.as_nzenv()); - let y_val = y.eval(env.as_nzenv()); + let x_val = x.eval(env); + let y_val = y.eval(env); let kts_x = match x_val.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("RecordTypeMergeRequiresRecordType"), @@ -589,8 +588,7 @@ fn type_one_layer( } } - let type_annot = - type_annot.as_ref().map(|t| t.eval(env.as_nzenv())); + let type_annot = type_annot.as_ref().map(|t| t.eval(env)); match (inferred_type, type_annot) { (Some(t1), Some(t2)) => { if t1 != t2 { @@ -621,7 +619,7 @@ fn type_one_layer( annotation", ); }; - let annot_val = annot.eval(env.as_nzenv()); + let annot_val = annot.eval(env); let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; @@ -670,7 +668,7 @@ fn type_one_layer( let output_type = Value::from_builtin(Builtin::List) .app(Value::from_kind(ValueKind::RecordType(kts))); if let Some(annot) = annot { - let annot_val = annot.eval(env.as_nzenv()); + let annot_val = annot.eval(env); if output_type != annot_val { return span_err("Annotation mismatch"); } @@ -710,7 +708,7 @@ fn type_one_layer( _ => return span_err("ProjectionMustBeRecord"), }; - let selection_val = selection.eval(env.as_nzenv()); + let selection_val = selection.eval(env); let sel_kts = match selection_val.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), @@ -782,14 +780,14 @@ pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot)?; - let annot_nf = annot.eval(env.as_nzenv()); + let annot_nf = annot.eval(env); let body_env = env.insert_type(binder, annot_nf); let body = type_with(&body_env, body)?; ExprKind::Lam(binder.clone(), annot, body) } ExprKind::Pi(binder, annot, body) => { let annot = type_with(env, annot)?; - let annot_nf = annot.eval(env.as_nzenv()); + let annot_nf = annot.eval(env); let body_env = env.insert_type(binder, annot_nf); let body = type_with(&body_env, body)?; ExprKind::Pi(binder.clone(), annot, body) @@ -808,7 +806,7 @@ pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { }; let val = type_with(env, &val)?; let val_ty = val.get_type()?; - let val_nf = val.eval(&env.as_nzenv()); + let val_nf = val.eval(env); 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) -- cgit v1.2.3 From c3ed75dc4b354becac0821e4288105dc2a300c4c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 10 Feb 2020 19:14:07 +0000 Subject: Remove need for Embed This was an archaic leftover from copying the Haskell datatypes anyway --- dhall/src/semantics/tck/typecheck.rs | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7f02832..4e45637 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -761,21 +761,13 @@ fn type_one_layer( /// `type_with` typechecks an expressio in the provided environment. pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { let (tyekind, ty) = match hir.kind() { - HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))), + HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } - HirKind::Expr(ExprKind::Embed(p)) => { - 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()) - } HirKind::Expr(ekind) => { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { -- cgit v1.2.3 From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/semantics/tck/typecheck.rs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 4e45637..f9ff3d3 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -11,7 +11,6 @@ use crate::semantics::{ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span, }; -use crate::Normalized; fn type_of_recordtype<'a>( span: Span, @@ -51,7 +50,7 @@ pub fn mkerr(x: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind, + ekind: ExprKind, span: Span, ) -> Result { let span_err = |msg: &str| { @@ -66,9 +65,7 @@ fn type_one_layer( ExprKind::Import(..) => unreachable!( "There should remain no imports in a resolved expression" ), - ExprKind::Var(..) - | ExprKind::Const(Const::Sort) - | ExprKind::Embed(..) => unreachable!(), // Handled in type_with + ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with ExprKind::Lam(binder, annot, body) => { let body_ty = body.get_type()?; -- cgit v1.2.3 From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 19:04:44 +0000 Subject: Introduce LitKind to factor out common enum nodes --- dhall/src/semantics/tck/typecheck.rs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index f9ff3d3..c52cfda 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -9,7 +9,7 @@ use crate::semantics::{ TyExpr, TyExprKind, Type, Value, ValueKind, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, }; fn type_of_recordtype<'a>( @@ -115,10 +115,16 @@ fn type_one_layer( let t_tyexpr = typecheck(&t_hir)?; t_tyexpr.eval(env) } - ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), - ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural), - ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer), - ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double), + ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool), + ExprKind::Lit(LitKind::Natural(_)) => { + Value::from_builtin(Builtin::Natural) + } + ExprKind::Lit(LitKind::Integer(_)) => { + Value::from_builtin(Builtin::Integer) + } + ExprKind::Lit(LitKind::Double(_)) => { + Value::from_builtin(Builtin::Double) + } ExprKind::TextLit(interpolated) => { let text_type = Value::from_builtin(Builtin::Text); for contents in interpolated.iter() { -- cgit v1.2.3 From 7b649b8647c60f1c02050805520f307edff0a94f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 19:48:11 +0000 Subject: Only store type at root node in tyexpr --- dhall/src/semantics/tck/typecheck.rs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c52cfda..c854552 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv, - TyExpr, TyExprKind, Type, Value, ValueKind, + TyExpr, Type, Value, ValueKind, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -758,18 +758,22 @@ fn type_one_layer( } }; - Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span)) + Ok(TyExpr::new( + HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), + Some(ty), + span, + )) } /// `type_with` typechecks an expressio in the provided environment. pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { let (tyekind, ty) = match hir.kind() { - HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))), + HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { - (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) + (HirKind::Expr(ExprKind::Const(Const::Sort)), None) } HirKind::Expr(ekind) => { let ekind = match ekind { -- cgit v1.2.3 From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:17:41 +0000 Subject: Simplify conversions to/from TyExpr --- dhall/src/semantics/tck/typecheck.rs | 157 ++++++++++++++++------------------- 1 file changed, 70 insertions(+), 87 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c854552..794edcf 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -12,28 +12,6 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, }; -fn type_of_recordtype<'a>( - span: Span, - tys: impl Iterator>, -) -> Result { - let span_err = |msg: &str| { - mkerr( - ErrorBuilder::new(msg.to_string()) - .span_err(span.clone(), msg.to_string()) - .format(), - ) - }; - // An empty record type has type Type - let mut k = Const::Type; - for t in tys { - match t.get_type()?.as_const() { - Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), - } - } - Ok(Value::from_const(k)) -} - fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { Const::Type @@ -42,8 +20,19 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub fn mkerr(x: S) -> Result { - Err(TypeError::new(TypeMessage::Custom(x.to_string()))) +pub fn mkerr(msg: S) -> Result { + Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) +} + +pub fn mk_span_err( + span: &Span, + msg: S, +) -> Result { + mkerr( + ErrorBuilder::new(msg.to_string()) + .span_err(span.clone(), msg.to_string()) + .format(), + ) } /// When all sub-expressions have been typed, check the remaining toplevel @@ -53,13 +42,7 @@ fn type_one_layer( ekind: ExprKind, span: Span, ) -> Result { - let span_err = |msg: &str| { - mkerr( - ErrorBuilder::new(msg.to_string()) - .span_err(span.clone(), msg.to_string()) - .format(), - ) - }; + let span_err = |msg: &str| mk_span_err(&span, msg); let ty = match &ekind { ExprKind::Import(..) => unreachable!( @@ -68,10 +51,9 @@ fn type_one_layer( ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with ExprKind::Lam(binder, annot, body) => { - let body_ty = body.get_type()?; - let body_ty = body_ty.to_tyexpr_tyenv( + 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, Span::Artificial)?.eval(env) } @@ -157,19 +139,19 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - let t = x.get_type()?; - if t.get_type(env)?.as_const() != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidListType"); } + let t = x.get_type()?; Value::from_builtin(Builtin::List).app(t) } ExprKind::SomeLit(x) => { - let t = x.get_type()?; - if t.get_type(env)?.as_const() != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } + let t = x.get_type()?; Value::from_builtin(Builtin::Optional).app(t) } ExprKind::RecordLit(kvs) => { @@ -183,18 +165,23 @@ fn type_one_layer( } Entry::Vacant(e) => e.insert(v.get_type()?), }; + + // Check that the fields have a valid kind + match v.get_kind(env)? { + Some(_) => {} + None => return span_err("InvalidFieldType"), + } } - type_of_recordtype( - span.clone(), - kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), - )?; Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; let mut seen_fields = HashMap::new(); - for (x, _) in kts { + // An empty record type has type Type + let mut k = Const::Type; + + for (x, t) in kts { // Check for duplicated entries match seen_fields.entry(x.clone()) { Entry::Occupied(_) => { @@ -202,12 +189,15 @@ fn type_one_layer( } Entry::Vacant(e) => e.insert(()), }; + + // Check the type is a Const and compute final type + match t.get_type()?.as_const() { + Some(c) => k = max(k, c), + None => return span_err("InvalidFieldType"), + } } - type_of_recordtype( - span.clone(), - kts.iter().map(|(_, t)| Cow::Borrowed(t)), - )? + Value::from_const(k) } ExprKind::UnionType(kts) => { use std::collections::hash_map::Entry; @@ -337,9 +327,7 @@ fn type_one_layer( if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - 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) { + if y.get_kind(env)? != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.get_type()? != z.get_type()? { @@ -369,45 +357,44 @@ fn type_one_layer( Ok(r_t.clone()) })?; - // Construct the final record type - type_of_recordtype( - span.clone(), - kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), - )?; Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - x.get_type()?.to_tyexpr_tyenv(env), - y.get_type()?.to_tyexpr_tyenv(env), + x.get_type_tyexpr(env)?, + y.get_type_tyexpr(env)?, ); - type_one_layer(env, ekind, Span::Artificial)?.eval(env) + type_one_layer(env, ekind, span.clone())?.eval(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - let x_val = x.eval(env); - let y_val = y.eval(env); - let kts_x = match x_val.kind() { - ValueKind::RecordType(kts) => kts, - _ => return span_err("RecordTypeMergeRequiresRecordType"), - }; - let kts_y = match y_val.kind() { - ValueKind::RecordType(kts) => kts, - _ => return span_err("RecordTypeMergeRequiresRecordType"), - }; - for (k, tx) in kts_x { - if let Some(ty) = kts_y.get(k) { - type_one_layer( - env, - ExprKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - tx.to_tyexpr_tyenv(env), - ty.to_tyexpr_tyenv(env), - ), - Span::Artificial, - )?; + 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, "RecordTypeMergeRequiresRecordType"), + }; + let kts_y = match y.kind() { + ValueKind::RecordType(kts) => kts, + _ => return mk_span_err(span, "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 let xk = x.get_type()?.as_const().unwrap(); @@ -434,9 +421,7 @@ fn type_one_layer( if l.get_type()? != r.get_type()? { return span_err("EquivalenceTypeMismatch"); } - if l.get_type()?.to_tyexpr_tyenv(env).get_type()?.as_const() - != Some(Const::Type) - { + if l.get_kind(env)? != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -605,6 +590,9 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { + if record.get_kind(env)? != Some(Const::Type) { + return span_err("`toMap` only accepts records of type `Type`"); + } let record_t = record.get_type()?; let kts = match record_t.kind() { ValueKind::RecordType(kts) => kts, @@ -652,11 +640,6 @@ fn type_one_layer( annot_val } else { let entry_type = kts.iter().next().unwrap().1.clone(); - if entry_type.get_type(env)?.as_const() != Some(Const::Type) { - return span_err( - "`toMap` only accepts records of type `Type`", - ); - } for (_, t) in kts.iter() { if *t != entry_type { return span_err( -- cgit v1.2.3 From e25b67906ce68e8726e8139c1d1855f3ab2518ce Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:45:42 +0000 Subject: Rework annotation and Sort handling --- dhall/src/semantics/tck/typecheck.rs | 143 ++++++++++++++++++----------------- 1 file changed, 75 insertions(+), 68 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 794edcf..a4ab31f 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -24,13 +24,10 @@ pub fn mkerr(msg: S) -> Result { Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) } -pub fn mk_span_err( - span: &Span, - msg: S, -) -> Result { +pub fn mk_span_err(span: Span, msg: S) -> Result { mkerr( ErrorBuilder::new(msg.to_string()) - .span_err(span.clone(), msg.to_string()) + .span_err(span, msg.to_string()) .format(), ) } @@ -40,22 +37,25 @@ pub fn mk_span_err( fn type_one_layer( env: &TyEnv, ekind: ExprKind, + annot: Option, span: Span, ) -> Result { - let span_err = |msg: &str| mk_span_err(&span, msg); + let span_err = |msg: &str| mk_span_err(span.clone(), msg); let ty = match &ekind { ExprKind::Import(..) => unreachable!( "There should remain no imports in a resolved expression" ), - ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with + ExprKind::Var(..) + | ExprKind::Const(Const::Sort) + | 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, Span::Artificial)?.eval(env) + type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env) } ExprKind::Pi(_, annot, body) => { let ks = match annot.get_type()?.as_const() { @@ -253,18 +253,6 @@ fn type_one_layer( } // _ => span_err("NotARecord"), } } - ExprKind::Annot(x, t) => { - let t = t.eval(env); - let x_ty = x.get_type()?; - if x_ty != t { - return span_err(&format!( - "annot mismatch: {} != {}", - x_ty.to_expr_tyenv(env), - t.to_expr_tyenv(env) - )); - } - x_ty - } ExprKind::Assert(t) => { let t = t.eval(env); match &*t.kind() { @@ -365,7 +353,7 @@ fn type_one_layer( x.get_type_tyexpr(env)?, y.get_type_tyexpr(env)?, ); - type_one_layer(env, ekind, span.clone())?.eval(env) + type_one_layer(env, ekind, None, span.clone())?.eval(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { fn check_rectymerge( @@ -376,20 +364,25 @@ fn type_one_layer( ) -> Result<(), TypeError> { let kts_x = match x.kind() { ValueKind::RecordType(kts) => kts, - _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"), + _ => { + return mk_span_err( + span.clone(), + "RecordTypeMergeRequiresRecordType", + ) + } }; let kts_y = match y.kind() { ValueKind::RecordType(kts) => kts, - _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"), + _ => { + 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(), - )?; + check_rectymerge(span, env, tx.clone(), ty.clone())?; } } Ok(()) @@ -717,30 +710,38 @@ fn type_one_layer( let ty_field_default = type_one_layer( env, ExprKind::Field(ty.clone(), "default".into()), + None, span.clone(), )?; let ty_field_type = type_one_layer( env, ExprKind::Field(ty.clone(), "Type".into()), + None, span.clone(), )?; - let merge = type_one_layer( + return type_one_layer( env, ExprKind::BinOp( BinOp::RightBiasedRecordMerge, ty_field_default, compl.clone(), ), - span.clone(), - )?; - return type_one_layer( - env, - ExprKind::Annot(merge, ty_field_type), + Some(ty_field_type.eval(env)), span.clone(), ); } }; + if let Some(annot) = annot { + if ty != annot { + return span_err(&format!( + "annot mismatch: {} != {}", + ty.to_expr_tyenv(env), + annot.to_expr_tyenv(env) + )); + } + } + Ok(TyExpr::new( HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), Some(ty), @@ -748,72 +749,78 @@ fn type_one_layer( )) } -/// `type_with` typechecks an expressio in the provided environment. -pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result { - let (tyekind, ty) = match hir.kind() { - HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))), +/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation +/// to compare with. +pub(crate) fn type_with( + env: &TyEnv, + hir: &Hir, + annot: Option, +) -> Result { + match hir.kind() { + HirKind::Var(var) => Ok(TyExpr::new( + HirKind::Var(*var), + Some(env.lookup(var)), + hir.span(), + )), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { - (HirKind::Expr(ExprKind::Const(Const::Sort)), None) + mk_span_err(hir.span(), "Sort does not have a type") + } + HirKind::Expr(ExprKind::Annot(x, t)) => { + let t = match t.kind() { + HirKind::Expr(ExprKind::Const(Const::Sort)) => { + Value::from_const(Const::Sort) + } + _ => type_with(env, t, None)?.eval(env), + }; + type_with(env, x, Some(t)) } HirKind::Expr(ekind) => { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot)?; + let annot = type_with(env, annot, None)?; let annot_nf = annot.eval(env); let body_env = env.insert_type(binder, annot_nf); - let body = type_with(&body_env, body)?; + let body = type_with(&body_env, body, None)?; ExprKind::Lam(binder.clone(), annot, body) } ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot)?; + let annot = type_with(env, annot, None)?; let annot_nf = annot.eval(env); let body_env = env.insert_type(binder, annot_nf); - let body = type_with(&body_env, body)?; + let body = type_with(&body_env, body, None)?; ExprKind::Pi(binder.clone(), annot, body) } ExprKind::Let(binder, annot, val, body) => { - let val = if let Some(t) = annot { - Hir::new( - HirKind::Expr(ExprKind::Annot( - val.clone(), - t.clone(), - )), - t.span(), - ) + let val_annot = if let Some(t) = annot { + Some(type_with(env, t, None)?.eval(env)) } else { - val.clone() + None }; - let val = type_with(env, &val)?; + let val = type_with(env, &val, val_annot)?; let val_ty = val.get_type()?; let val_nf = val.eval(env); let body_env = env.insert_value(&binder, val_nf, val_ty); - let body = type_with(&body_env, body)?; + let body = type_with(&body_env, body, None)?; ExprKind::Let(binder.clone(), None, val, body) } - _ => ekind.traverse_ref(|e| type_with(env, e))?, + _ => ekind.traverse_ref(|e| type_with(env, e, None))?, }; - return type_one_layer(env, ekind, hir.span()); + type_one_layer(env, ekind, annot, hir.span()) } - }; - - Ok(TyExpr::new(tyekind, ty, hir.span())) + } } /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck(e: &Hir) -> Result { - let res = type_with(&TyEnv::new(), e)?; - // Ensure that the inferred type exists (i.e. this is not Sort) - res.get_type()?; - Ok(res) +pub(crate) fn typecheck(hir: &Hir) -> Result { + type_with(&TyEnv::new(), hir, None) } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { - let hir = - Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span()); - typecheck(&hir) + let ty = typecheck(&ty)?.eval(&TyEnv::new()); + type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3 From 350d1cf7d9c114b1334b2743071b0b99ea64c1ec Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:56:38 +0000 Subject: TyExpr always carries a type --- dhall/src/semantics/tck/typecheck.rs | 112 +++++++++++++++++------------------ 1 file changed, 55 insertions(+), 57 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a4ab31f..b3c9353 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -53,24 +53,24 @@ fn type_one_layer( 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) } ExprKind::Pi(_, annot, body) => { - let ks = match annot.get_type()?.as_const() { + let ks = match annot.ty().as_const() { Some(k) => k, _ => { return mkerr( ErrorBuilder::new(format!( "Invalid input type: `{}`", - annot.get_type()?.to_expr_tyenv(env), + annot.ty().to_expr_tyenv(env), )) .span_err( annot.span(), format!( "this has type: `{}`", - annot.get_type()?.to_expr_tyenv(env) + annot.ty().to_expr_tyenv(env) ), ) .help(format!( @@ -81,14 +81,14 @@ fn type_one_layer( ); } }; - let kt = match body.get_type()?.as_const() { + let kt = match body.ty().as_const() { Some(k) => k, _ => return span_err("Invalid output type"), }; Value::from_const(function_check(ks, kt)) } - ExprKind::Let(_, _, _, body) => body.get_type()?, + ExprKind::Let(_, _, _, body) => body.ty().clone(), ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), @@ -112,7 +112,7 @@ fn type_one_layer( for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { - if x.get_type()? != text_type { + if *x.ty() != text_type { return span_err("InvalidTextInterpolation"); } } @@ -121,7 +121,7 @@ fn type_one_layer( } ExprKind::EmptyListLit(t) => { let t = t.eval(env); - match &*t.kind() { + match t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, @@ -135,23 +135,23 @@ fn type_one_layer( let mut iter = xs.iter(); let x = iter.next().unwrap(); for y in iter { - if x.get_type()? != y.get_type()? { + if x.ty() != y.ty() { return span_err("InvalidListElement"); } } - if x.get_kind(env)? != Some(Const::Type) { + if x.get_kind(env) != Some(Const::Type) { return span_err("InvalidListType"); } - let t = x.get_type()?; + let t = x.ty().clone(); Value::from_builtin(Builtin::List).app(t) } ExprKind::SomeLit(x) => { - if x.get_kind(env)? != Some(Const::Type) { + if x.get_kind(env) != Some(Const::Type) { return span_err("InvalidOptionalType"); } - let t = x.get_type()?; + let t = x.ty().clone(); Value::from_builtin(Builtin::Optional).app(t) } ExprKind::RecordLit(kvs) => { @@ -163,11 +163,11 @@ fn type_one_layer( Entry::Occupied(_) => { return span_err("RecordTypeDuplicateField") } - Entry::Vacant(e) => e.insert(v.get_type()?), + Entry::Vacant(e) => e.insert(v.ty().clone()), }; // Check that the fields have a valid kind - match v.get_kind(env)? { + match v.get_kind(env) { Some(_) => {} None => return span_err("InvalidFieldType"), } @@ -191,7 +191,7 @@ fn type_one_layer( }; // Check the type is a Const and compute final type - match t.get_type()?.as_const() { + match t.ty().as_const() { Some(c) => k = max(k, c), None => return span_err("InvalidFieldType"), } @@ -206,7 +206,7 @@ fn type_one_layer( let mut k = None; for (x, t) in kts { if let Some(t) = t { - match (k, t.get_type()?.as_const()) { + match (k, t.ty().as_const()) { (None, Some(k2)) => k = Some(k2), (Some(k1), Some(k2)) if k1 == k2 => {} _ => return span_err("InvalidFieldType"), @@ -227,12 +227,12 @@ fn type_one_layer( Value::from_const(k) } ExprKind::Field(scrut, x) => { - match &*scrut.get_type()?.kind() { + match scrut.ty().kind() { ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => tth.clone(), None => return span_err("MissingRecordField"), }, - // TODO: branch here only when scrut.get_type() is a Const + // TODO: branch here only when scrut.ty() is a Const _ => { let scrut_nf = scrut.eval(env); match scrut_nf.kind() { @@ -255,7 +255,7 @@ fn type_one_layer( } ExprKind::Assert(t) => { let t = t.eval(env); - match &*t.kind() { + match t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => { return span_err("AssertMismatch") @@ -265,9 +265,9 @@ fn type_one_layer( t } ExprKind::App(f, arg) => { - match f.get_type()?.kind() { + match f.ty().kind() { ValueKind::PiClosure { annot, closure, .. } => { - if arg.get_type()? != *annot { + if arg.ty() != annot { return mkerr( ErrorBuilder::new(format!( "wrong type of function argument" @@ -283,13 +283,13 @@ fn type_one_layer( arg.span(), format!( "but this has type: {}", - arg.get_type()?.to_expr_tyenv(env), + arg.ty().to_expr_tyenv(env), ), ) .note(format!( "expected type `{}`\n found type `{}`", annot.to_expr_tyenv(env), - arg.get_type()?.to_expr_tyenv(env), + arg.ty().to_expr_tyenv(env), )) .format(), ); @@ -301,7 +301,7 @@ fn type_one_layer( _ => return mkerr( ErrorBuilder::new(format!( "expected function, found `{}`", - f.get_type()?.to_expr_tyenv(env) + f.ty().to_expr_tyenv(env) )) .span_err( f.span(), @@ -312,21 +312,21 @@ fn type_one_layer( } } ExprKind::BoolIf(x, y, z) => { - if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { + if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.get_kind(env)? != Some(Const::Type) { + if y.get_kind(env) != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } - if y.get_type()? != z.get_type()? { + if y.ty() != z.ty() { return span_err("IfBranchMismatch"); } - y.get_type()? + y.ty().clone() } ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => { - let x_type = x.get_type()?; - let y_type = y.get_type()?; + let x_type = x.ty(); + let y_type = y.ty(); // Extract the LHS record type let kts_x = match x_type.kind() { @@ -350,8 +350,8 @@ fn type_one_layer( ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - x.get_type_tyexpr(env)?, - y.get_type_tyexpr(env)?, + x.get_type_tyexpr(env), + y.get_type_tyexpr(env), ); type_one_layer(env, ekind, None, span.clone())?.eval(env) } @@ -390,13 +390,12 @@ fn type_one_layer( check_rectymerge(&span, env, x.eval(env), y.eval(env))?; // A RecordType's type is always a const - let xk = x.get_type()?.as_const().unwrap(); - let yk = y.get_type()?.as_const().unwrap(); + let xk = x.ty().as_const().unwrap(); + let yk = y.ty().as_const().unwrap(); Value::from_const(max(xk, yk)) } ExprKind::BinOp(BinOp::ListAppend, l, r) => { - let l_ty = l.get_type()?; - match &*l_ty.kind() { + match l.ty().kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, .. @@ -404,17 +403,17 @@ fn type_one_layer( _ => return span_err("BinOpTypeMismatch"), } - if l_ty != r.get_type()? { + if l.ty() != r.ty() { return span_err("BinOpTypeMismatch"); } - l_ty + l.ty().clone() } ExprKind::BinOp(BinOp::Equivalence, l, r) => { - if l.get_type()? != r.get_type()? { + if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } - if l.get_kind(env)? != Some(Const::Type) { + if l.get_kind(env) != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -436,24 +435,24 @@ fn type_one_layer( BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"), }); - if l.get_type()? != t { + if *l.ty() != t { return span_err("BinOpTypeMismatch"); } - if r.get_type()? != t { + if *r.ty() != t { return span_err("BinOpTypeMismatch"); } t } ExprKind::Merge(record, union, type_annot) => { - let record_type = record.get_type()?; + let record_type = record.ty(); let handlers = match record_type.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("Merge1ArgMustBeRecord"), }; - let union_type = union.get_type()?; + let union_type = union.ty(); let variants = match union_type.kind() { ValueKind::UnionType(kts) => Cow::Borrowed(kts), ValueKind::AppliedBuiltin(BuiltinClosure { @@ -583,10 +582,10 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { - if record.get_kind(env)? != Some(Const::Type) { + if record.get_kind(env) != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } - let record_t = record.get_type()?; + let record_t = record.ty(); let kts = match record_t.kind() { ValueKind::RecordType(kts) => kts, _ => { @@ -656,7 +655,7 @@ fn type_one_layer( } } ExprKind::Projection(record, labels) => { - let record_type = record.get_type()?; + let record_type = record.ty(); let kts = match record_type.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), @@ -681,7 +680,7 @@ fn type_one_layer( Value::from_kind(ValueKind::RecordType(new_kts)) } ExprKind::ProjectionByExpr(record, selection) => { - let record_type = record.get_type()?; + let record_type = record.ty(); let rec_kts = match record_type.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), @@ -742,9 +741,10 @@ fn type_one_layer( } } + // TODO: avoid retraversing Ok(TyExpr::new( HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), - Some(ty), + ty, span, )) } @@ -757,11 +757,9 @@ pub(crate) fn type_with( annot: Option, ) -> Result { match hir.kind() { - HirKind::Var(var) => Ok(TyExpr::new( - HirKind::Var(*var), - Some(env.lookup(var)), - hir.span(), - )), + HirKind::Var(var) => { + Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span())) + } HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } @@ -800,9 +798,9 @@ pub(crate) fn type_with( None }; let val = type_with(env, &val, val_annot)?; - let val_ty = val.get_type()?; let val_nf = val.eval(env); - let body_env = env.insert_value(&binder, val_nf, val_ty); + let body_env = + env.insert_value(&binder, val_nf, val.ty().clone()); let body = type_with(&body_env, body, None)?; ExprKind::Let(binder.clone(), None, val, body) } -- cgit v1.2.3 From 51cf6a28fa56031dbeae0ff378f0ef84eff7fd3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 14 Feb 2020 18:55:27 +0000 Subject: Oops --- dhall/src/semantics/tck/typecheck.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index b3c9353..377b97e 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -53,7 +53,7 @@ fn type_one_layer( 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) } @@ -139,7 +139,7 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - if x.get_kind(env) != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidListType"); } @@ -147,7 +147,7 @@ fn type_one_layer( Value::from_builtin(Builtin::List).app(t) } ExprKind::SomeLit(x) => { - if x.get_kind(env) != Some(Const::Type) { + if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } @@ -167,7 +167,7 @@ fn type_one_layer( }; // Check that the fields have a valid kind - match v.get_kind(env) { + match v.get_kind(env)? { Some(_) => {} None => return span_err("InvalidFieldType"), } @@ -315,7 +315,7 @@ fn type_one_layer( if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.get_kind(env) != Some(Const::Type) { + if y.get_kind(env)? != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.ty() != z.ty() { @@ -350,8 +350,8 @@ fn type_one_layer( ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( BinOp::RecursiveRecordTypeMerge, - x.get_type_tyexpr(env), - y.get_type_tyexpr(env), + x.get_type_tyexpr(env)?, + y.get_type_tyexpr(env)?, ); type_one_layer(env, ekind, None, span.clone())?.eval(env) } @@ -413,7 +413,7 @@ fn type_one_layer( if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } - if l.get_kind(env) != Some(Const::Type) { + if l.get_kind(env)? != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -582,7 +582,7 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { - if record.get_kind(env) != Some(Const::Type) { + if record.get_kind(env)? != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); -- cgit v1.2.3 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/tck/typecheck.rs | 118 ++++++++++++++++++++++------------- 1 file changed, 76 insertions(+), 42 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') 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 From 5057144ed99bc4e1a76a0840dd39fc1bd862665c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:10:52 +0000 Subject: Desugar Completion during resolution --- dhall/src/semantics/tck/typecheck.rs | 34 ++++++---------------------------- 1 file changed, 6 insertions(+), 28 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a8a2d95..36f7173 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -75,12 +75,14 @@ fn type_one_layer( let span_err = |msg: &str| mk_span_err(span.clone(), msg); let ty = match &ekind { - ExprKind::Import(..) => unreachable!( - "There should remain no imports in a resolved expression" - ), + ExprKind::Import(..) | ExprKind::Completion(..) => { + unreachable!("This case should have been handled in resolution") + } ExprKind::Var(..) | ExprKind::Const(Const::Sort) - | ExprKind::Annot(..) => unreachable!(), // Handled in type_with + | ExprKind::Annot(..) => { + unreachable!("This case should have been handled in type_with") + } ExprKind::Lam(binder, annot, body) => { if annot.ty().as_const().is_none() { @@ -739,30 +741,6 @@ fn type_one_layer( selection_val } - ExprKind::Completion(ty, compl) => { - let ty_field_default = type_one_layer( - env, - ExprKind::Field(ty.clone(), "default".into()), - None, - span.clone(), - )?; - let ty_field_type = type_one_layer( - env, - ExprKind::Field(ty.clone(), "Type".into()), - None, - span.clone(), - )?; - return type_one_layer( - env, - ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - ty_field_default, - compl.clone(), - ), - Some(ty_field_type.eval(env)), - span.clone(), - ); - } }; if let Some(annot) = annot { -- cgit v1.2.3 From aa867b21f57f9bef2ec2b9d8450736f9111189ee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:44:40 +0000 Subject: Introduce proper Type struct --- dhall/src/semantics/tck/typecheck.rs | 111 +++++++++++++++++++---------------- 1 file changed, 61 insertions(+), 50 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 36f7173..dd996ae 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -38,7 +38,8 @@ fn check_rectymerge( }; for (k, tx) in kts_x { if let Some(ty) = kts_y.get(k) { - check_rectymerge(span, env, tx.clone(), ty.clone())?; + // TODO: store Type in RecordType ? + check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?; } } Ok(()) @@ -105,7 +106,7 @@ fn type_one_layer( .format(), ); } - let body_env = env.insert_type(&binder, annot.eval(env)); + let body_env = env.insert_type(&binder, annot.eval_to_type(env)); if body.get_kind(&body_env)?.is_none() { return span_err("Invalid output type"); } @@ -117,7 +118,7 @@ fn type_one_layer( )), span.clone(), ) - .eval(env) + .eval_to_type(env) } ExprKind::Pi(_, annot, body) => { let ks = match annot.ty().as_const() { @@ -148,29 +149,29 @@ fn type_one_layer( _ => return span_err("Invalid output type"), }; - Value::from_const(function_check(ks, kt)) + Type::from_const(function_check(ks, kt)) } ExprKind::Let(_, _, _, body) => body.ty().clone(), - ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), - ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), + ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), + ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); let t_tyexpr = typecheck(&t_hir)?; - t_tyexpr.eval(env) + t_tyexpr.eval_to_type(env) } - ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool), + ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool), ExprKind::Lit(LitKind::Natural(_)) => { - Value::from_builtin(Builtin::Natural) + Type::from_builtin(Builtin::Natural) } ExprKind::Lit(LitKind::Integer(_)) => { - Value::from_builtin(Builtin::Integer) + Type::from_builtin(Builtin::Integer) } ExprKind::Lit(LitKind::Double(_)) => { - Value::from_builtin(Builtin::Double) + Type::from_builtin(Builtin::Double) } ExprKind::TextLit(interpolated) => { - let text_type = Value::from_builtin(Builtin::Text); + let text_type = Type::from_builtin(Builtin::Text); for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { @@ -182,7 +183,7 @@ fn type_one_layer( text_type } ExprKind::EmptyListLit(t) => { - let t = t.eval(env); + let t = t.eval_to_type(env); match t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, @@ -205,16 +206,16 @@ fn type_one_layer( return span_err("InvalidListType"); } - let t = x.ty().clone(); - Value::from_builtin(Builtin::List).app(t) + let t = x.ty().to_value(); + Value::from_builtin(Builtin::List).app(t).to_type() } ExprKind::SomeLit(x) => { if x.get_kind(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } - let t = x.ty().clone(); - Value::from_builtin(Builtin::Optional).app(t) + let t = x.ty().to_value(); + Value::from_builtin(Builtin::Optional).app(t).to_type() } ExprKind::RecordLit(kvs) => { use std::collections::hash_map::Entry; @@ -225,7 +226,7 @@ fn type_one_layer( Entry::Occupied(_) => { return span_err("RecordTypeDuplicateField") } - Entry::Vacant(e) => e.insert(v.ty().clone()), + Entry::Vacant(e) => e.insert(v.ty().to_value()), }; // Check that the fields have a valid kind @@ -235,7 +236,7 @@ fn type_one_layer( } } - Value::from_kind(ValueKind::RecordType(kts)) + Value::from_kind(ValueKind::RecordType(kts)).to_type() } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -259,7 +260,7 @@ fn type_one_layer( } } - Value::from_const(k) + Type::from_const(k) } ExprKind::UnionType(kts) => { use std::collections::hash_map::Entry; @@ -286,17 +287,17 @@ fn type_one_layer( // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Value::from_const(k) + Type::from_const(k) } ExprKind::Field(scrut, x) => { match scrut.ty().kind() { ValueKind::RecordType(kts) => match kts.get(&x) { - Some(tth) => tth.clone(), + Some(val) => val.clone().to_type(), None => return span_err("MissingRecordField"), }, // TODO: branch here only when scrut.ty() is a Const _ => { - let scrut_nf = scrut.eval(env); + let scrut_nf = scrut.eval_to_type(env); match scrut_nf.kind() { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > @@ -304,8 +305,11 @@ fn type_one_layer( Value::from_kind(ValueKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), - closure: Closure::new_constant(scrut_nf), + closure: Closure::new_constant( + scrut_nf.into_value(), + ), }) + .to_type() } Some(None) => scrut_nf, None => return span_err("MissingUnionField"), @@ -316,7 +320,7 @@ fn type_one_layer( } } ExprKind::Assert(t) => { - let t = t.eval(env); + let t = t.eval_to_type(env); match t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => { @@ -328,8 +332,9 @@ fn type_one_layer( } ExprKind::App(f, arg) => { match f.ty().kind() { + // TODO: store Type in closure ValueKind::PiClosure { annot, closure, .. } => { - if arg.ty() != annot { + if arg.ty().as_value() != annot { return mkerr( ErrorBuilder::new(format!( "wrong type of function argument" @@ -358,7 +363,7 @@ fn type_one_layer( } let arg_nf = arg.eval(env); - closure.apply(arg_nf) + closure.apply(arg_nf).to_type() } _ => return mkerr( ErrorBuilder::new(format!( @@ -407,7 +412,7 @@ fn type_one_layer( Ok(r_t.clone()) })?; - Value::from_kind(ValueKind::RecordType(kts)) + Value::from_kind(ValueKind::RecordType(kts)).to_type() } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?; @@ -420,15 +425,20 @@ fn type_one_layer( )), span.clone(), ) - .eval(env) + .eval_to_type(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - check_rectymerge(&span, env, x.eval(env), y.eval(env))?; + check_rectymerge( + &span, + env, + x.eval_to_type(env), + y.eval_to_type(env), + )?; // A RecordType's type is always a const let xk = x.ty().as_const().unwrap(); let yk = y.ty().as_const().unwrap(); - Value::from_const(max(xk, yk)) + Type::from_const(max(xk, yk)) } ExprKind::BinOp(BinOp::ListAppend, l, r) => { match l.ty().kind() { @@ -453,10 +463,10 @@ fn type_one_layer( return span_err("EquivalenceArgumentsMustBeTerms"); } - Value::from_const(Const::Type) + Type::from_const(Const::Type) } ExprKind::BinOp(o, l, r) => { - let t = Value::from_builtin(match o { + let t = Type::from_builtin(match o { BinOp::BoolAnd | BinOp::BoolOr | BinOp::BoolEQ @@ -507,7 +517,7 @@ fn type_one_layer( let mut inferred_type = None; for (x, handler_type) in handlers { - let handler_return_type = match variants.get(x) { + let handler_return_type: Type = match variants.get(x) { // Union alternative with type Some(Some(variant_type)) => match handler_type.kind() { ValueKind::PiClosure { closure, annot, .. } => { @@ -542,7 +552,7 @@ fn type_one_layer( } match closure.remove_binder() { - Ok(v) => v, + Ok(v) => v.to_type(), Err(()) => { return span_err( "MergeReturnTypeIsDependent", @@ -586,7 +596,7 @@ fn type_one_layer( } }, // Union alternative without type - Some(None) => handler_type.clone(), + Some(None) => handler_type.clone().to_type(), None => return span_err("MergeHandlerMissingVariant"), }; match &inferred_type { @@ -604,7 +614,7 @@ fn type_one_layer( } } - let type_annot = type_annot.as_ref().map(|t| t.eval(env)); + let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env)); match (inferred_type, type_annot) { (Some(t1), Some(t2)) => { if t1 != t2 { @@ -638,7 +648,7 @@ fn type_one_layer( annotation", ); }; - let annot_val = annot.eval(env); + let annot_val = annot.eval_to_type(env); let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; @@ -679,10 +689,11 @@ fn type_one_layer( let mut kts = HashMap::new(); kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); - let output_type = Value::from_builtin(Builtin::List) - .app(Value::from_kind(ValueKind::RecordType(kts))); + let output_type: Type = Value::from_builtin(Builtin::List) + .app(Value::from_kind(ValueKind::RecordType(kts))) + .to_type(); if let Some(annot) = annot { - let annot_val = annot.eval(env); + let annot_val = annot.eval_to_type(env); if output_type != annot_val { return span_err("Annotation mismatch"); } @@ -713,7 +724,7 @@ fn type_one_layer( }; } - Value::from_kind(ValueKind::RecordType(new_kts)) + Value::from_kind(ValueKind::RecordType(new_kts)).to_type() } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.ty(); @@ -722,7 +733,7 @@ fn type_one_layer( _ => return span_err("ProjectionMustBeRecord"), }; - let selection_val = selection.eval(env); + let selection_val = selection.eval_to_type(env); let sel_kts = match selection_val.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), @@ -781,9 +792,9 @@ pub(crate) fn type_with( HirKind::Expr(ExprKind::Annot(x, t)) => { let t = match t.kind() { HirKind::Expr(ExprKind::Const(Const::Sort)) => { - Value::from_const(Const::Sort) + Type::from_const(Const::Sort) } - _ => type_with(env, t, None)?.eval(env), + _ => type_with(env, t, None)?.eval_to_type(env), }; type_with(env, x, Some(t)) } @@ -791,21 +802,21 @@ pub(crate) fn type_with( let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot, None)?; - let annot_nf = annot.eval(env); + let annot_nf = annot.eval_to_type(env); let body_env = env.insert_type(binder, annot_nf); let body = type_with(&body_env, body, None)?; ExprKind::Lam(binder.clone(), annot, body) } ExprKind::Pi(binder, annot, body) => { let annot = type_with(env, annot, None)?; - let annot_nf = annot.eval(env); - let body_env = env.insert_type(binder, annot_nf); + let annot_val = annot.eval_to_type(env); + let body_env = env.insert_type(binder, annot_val); let body = type_with(&body_env, body, None)?; ExprKind::Pi(binder.clone(), annot, body) } ExprKind::Let(binder, annot, val, body) => { let val_annot = if let Some(t) = annot { - Some(type_with(env, t, None)?.eval(env)) + Some(type_with(env, t, None)?.eval_to_type(env)) } else { None }; @@ -831,6 +842,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result { /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { - let ty = typecheck(&ty)?.eval(&TyEnv::new()); + let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new()); type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3 From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:06:23 +0000 Subject: Start requiring Universe to build a Type --- dhall/src/semantics/tck/typecheck.rs | 263 ++++++++++++++--------------------- 1 file changed, 107 insertions(+), 156 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index dd996ae..1281045 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -15,8 +15,8 @@ use crate::syntax::{ fn check_rectymerge( span: &Span, env: &TyEnv, - x: Type, - y: Type, + x: Value, + y: Value, ) -> Result<(), TypeError> { let kts_x = match x.kind() { ValueKind::RecordType(kts) => kts, @@ -39,7 +39,7 @@ fn check_rectymerge( for (k, tx) in kts_x { if let Some(ty) = kts_y.get(k) { // TODO: store Type in RecordType ? - check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?; + check_rectymerge(span, env, tx.clone(), ty.clone())?; } } Ok(()) @@ -70,9 +70,8 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { fn type_one_layer( env: &TyEnv, ekind: ExprKind, - annot: Option, span: Span, -) -> Result { +) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); let ty = match &ekind { @@ -81,84 +80,19 @@ fn type_one_layer( } ExprKind::Var(..) | ExprKind::Const(Const::Sort) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) | ExprKind::Annot(..) => { unreachable!("This case should have been handled in type_with") } - ExprKind::Lam(binder, annot, body) => { - 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_to_type(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_to_type(env) - } - ExprKind::Pi(_, annot, body) => { - let ks = match annot.ty().as_const() { - Some(k) => k, - _ => { - 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 kt = match body.ty().as_const() { - Some(k) => k, - _ => return span_err("Invalid output type"), - }; - - Type::from_const(function_check(ks, kt)) - } - ExprKind::Let(_, _, _, body) => body.ty().clone(), - ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); let t_tyexpr = typecheck(&t_hir)?; - t_tyexpr.eval_to_type(env) + t_tyexpr.eval_to_type(env)? } ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool), ExprKind::Lit(LitKind::Natural(_)) => { @@ -183,7 +117,7 @@ fn type_one_layer( text_type } ExprKind::EmptyListLit(t) => { - let t = t.eval_to_type(env); + let t = t.eval_to_type(env)?; match t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, @@ -202,7 +136,7 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - if x.get_kind(env)? != Some(Const::Type) { + if x.ty().ty(env)? != Some(Const::Type) { return span_err("InvalidListType"); } @@ -210,7 +144,7 @@ fn type_one_layer( Value::from_builtin(Builtin::List).app(t).to_type() } ExprKind::SomeLit(x) => { - if x.get_kind(env)? != Some(Const::Type) { + if x.ty().ty(env)? != Some(Const::Type) { return span_err("InvalidOptionalType"); } @@ -230,7 +164,7 @@ fn type_one_layer( }; // Check that the fields have a valid kind - match v.get_kind(env)? { + match v.ty().ty(env)? { Some(_) => {} None => return span_err("InvalidFieldType"), } @@ -297,7 +231,7 @@ fn type_one_layer( }, // TODO: branch here only when scrut.ty() is a Const _ => { - let scrut_nf = scrut.eval_to_type(env); + let scrut_nf = scrut.eval(env); match scrut_nf.kind() { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > @@ -305,13 +239,11 @@ fn type_one_layer( Value::from_kind(ValueKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), - closure: Closure::new_constant( - scrut_nf.into_value(), - ), + closure: Closure::new_constant(scrut_nf), }) .to_type() } - Some(None) => scrut_nf, + Some(None) => scrut_nf.to_type(), None => return span_err("MissingUnionField"), }, _ => return span_err("NotARecord"), @@ -320,7 +252,7 @@ fn type_one_layer( } } ExprKind::Assert(t) => { - let t = t.eval_to_type(env); + let t = t.eval_to_type(env)?; match t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => { @@ -382,7 +314,7 @@ fn type_one_layer( if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.get_kind(env)? != Some(Const::Type) { + if y.ty().ty(env)? != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.ty() != z.ty() { @@ -415,25 +347,22 @@ fn type_one_layer( Value::from_kind(ValueKind::RecordType(kts)).to_type() } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?; + check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?; - Hir::new( + let hir = 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_to_type(env) + ); + let x_u = x.ty().ty_univ(env)?; + let y_u = y.ty().ty_univ(env)?; + Type::new(hir.eval(env), max(x_u, y_u)) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - check_rectymerge( - &span, - env, - x.eval_to_type(env), - y.eval_to_type(env), - )?; + check_rectymerge(&span, env, x.eval(env), y.eval(env))?; // A RecordType's type is always a const let xk = x.ty().as_const().unwrap(); @@ -459,7 +388,7 @@ fn type_one_layer( if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } - if l.get_kind(env)? != Some(Const::Type) { + if l.ty().ty(env)? != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -614,7 +543,10 @@ fn type_one_layer( } } - let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env)); + let type_annot = type_annot + .as_ref() + .map(|t| t.eval_to_type(env)) + .transpose()?; match (inferred_type, type_annot) { (Some(t1), Some(t2)) => { if t1 != t2 { @@ -628,7 +560,7 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { - if record.get_kind(env)? != Some(Const::Type) { + if record.ty().ty(env)? != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); @@ -648,7 +580,7 @@ fn type_one_layer( annotation", ); }; - let annot_val = annot.eval_to_type(env); + let annot_val = annot.eval_to_type(env)?; let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; @@ -693,7 +625,7 @@ fn type_one_layer( .app(Value::from_kind(ValueKind::RecordType(kts))) .to_type(); if let Some(annot) = annot { - let annot_val = annot.eval_to_type(env); + let annot_val = annot.eval_to_type(env)?; if output_type != annot_val { return span_err("Annotation mismatch"); } @@ -733,7 +665,7 @@ fn type_one_layer( _ => return span_err("ProjectionMustBeRecord"), }; - let selection_val = selection.eval_to_type(env); + let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { ValueKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), @@ -754,22 +686,7 @@ fn type_one_layer( } }; - if let Some(annot) = annot { - if ty != annot { - return span_err(&format!( - "annot mismatch: {} != {}", - ty.to_expr_tyenv(env), - annot.to_expr_tyenv(env) - )); - } - } - - // TODO: avoid retraversing - Ok(TyExpr::new( - HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), - ty, - span, - )) + Ok(ty) } /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation @@ -779,59 +696,93 @@ pub(crate) fn type_with( hir: &Hir, annot: Option, ) -> Result { - match hir.kind() { - HirKind::Var(var) => { - Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span())) - } + let tyexpr = match hir.kind() { + HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { - mk_span_err(hir.span(), "Sort does not have a type") + return mk_span_err(hir.span(), "Sort does not have a type") } HirKind::Expr(ExprKind::Annot(x, t)) => { let t = match t.kind() { HirKind::Expr(ExprKind::Const(Const::Sort)) => { Type::from_const(Const::Sort) } - _ => type_with(env, t, None)?.eval_to_type(env), + _ => type_with(env, t, None)?.eval_to_type(env)?, }; - type_with(env, x, Some(t)) + type_with(env, x, Some(t))? } - HirKind::Expr(ekind) => { - let ekind = match ekind { - ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot, None)?; - let annot_nf = annot.eval_to_type(env); - let body_env = env.insert_type(binder, annot_nf); - let body = type_with(&body_env, body, None)?; - ExprKind::Lam(binder.clone(), annot, body) - } - ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot, None)?; - let annot_val = annot.eval_to_type(env); - let body_env = env.insert_type(binder, annot_val); - let body = type_with(&body_env, body, None)?; - ExprKind::Pi(binder.clone(), annot, body) - } - ExprKind::Let(binder, annot, val, body) => { - let val_annot = if let Some(t) = annot { - Some(type_with(env, t, None)?.eval_to_type(env)) - } else { - None - }; - let val = type_with(env, &val, val_annot)?; - let val_nf = val.eval(env); - let body_env = - env.insert_value(&binder, val_nf, val.ty().clone()); - let body = type_with(&body_env, body, None)?; - ExprKind::Let(binder.clone(), None, val, body) - } - _ => ekind.traverse_ref(|e| type_with(env, e, None))?, + + HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { + let annot = type_with(env, annot, None)?; + let annot_nf = annot.eval_to_type(env)?; + let body_env = env.insert_type(binder, annot_nf); + let body = type_with(&body_env, body, None)?; + + let u_annot = annot.ty().as_const().unwrap(); + let u_body = match body.ty().ty(&body_env)? { + Some(k) => k, + _ => return mk_span_err(hir.span(), "Invalid output type"), }; - type_one_layer(env, ekind, annot, hir.span()) + let u = function_check(u_annot, u_body).to_universe(); + let ty_hir = Hir::new( + HirKind::Expr(ExprKind::Pi( + binder.clone(), + annot.to_hir(), + body.ty().to_hir(body_env.as_varenv()), + )), + hir.span(), + ); + let ty = Type::new(ty_hir.eval(env), u); + + TyExpr::from_hir(hir, ty) + } + HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { + let annot = type_with(env, annot, None)?; + let annot_val = annot.eval_to_type(env)?; + let body_env = env.insert_type(binder, annot_val); + let body = type_with(&body_env, body, None)?; + body.ensure_is_type(env)?; + + let ks = annot.ty().as_const().unwrap(); + let kt = body.ty().as_const().unwrap(); + let ty = Type::from_const(function_check(ks, kt)); + TyExpr::from_hir(hir, ty) + } + HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => { + let val_annot = annot + .as_ref() + .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?)) + .transpose()?; + let val = type_with(env, &val, val_annot)?; + let val_nf = val.eval(env); + let body_env = env.insert_value(&binder, val_nf, val.ty().clone()); + let body = type_with(&body_env, body, None)?; + let ty = body.ty().clone(); + TyExpr::from_hir(hir, ty) + } + HirKind::Expr(ekind) => { + let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?; + let ty = type_one_layer(env, ekind, hir.span())?; + TyExpr::from_hir(hir, ty) + } + }; + + if let Some(annot) = annot { + if *tyexpr.ty() != annot { + return mk_span_err( + hir.span(), + &format!( + "annot mismatch: {} != {}", + tyexpr.ty().to_expr_tyenv(env), + annot.to_expr_tyenv(env) + ), + ); } } + + Ok(tyexpr) } /// Typecheck an expression and return the expression annotated with types if type-checking @@ -842,6 +793,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result { /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { - let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new()); + let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3 From c451c18103b871e563b12c524bc3feec5451154c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:48:35 +0000 Subject: Avoid recomputing universes in tck --- dhall/src/semantics/tck/typecheck.rs | 73 ++++++++++++++++++++++-------------- 1 file changed, 45 insertions(+), 28 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 1281045..45b3168 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -136,24 +136,30 @@ fn type_one_layer( return span_err("InvalidListElement"); } } - if x.ty().ty(env)? != Some(Const::Type) { + if x.ty().ty().as_const() != Some(Const::Type) { return span_err("InvalidListType"); } let t = x.ty().to_value(); - Value::from_builtin(Builtin::List).app(t).to_type() + Value::from_builtin(Builtin::List) + .app(t) + .to_type(Const::Type) } ExprKind::SomeLit(x) => { - if x.ty().ty(env)? != Some(Const::Type) { + if x.ty().ty().as_const() != Some(Const::Type) { return span_err("InvalidOptionalType"); } let t = x.ty().to_value(); - Value::from_builtin(Builtin::Optional).app(t).to_type() + Value::from_builtin(Builtin::Optional) + .app(t) + .to_type(Const::Type) } ExprKind::RecordLit(kvs) => { use std::collections::hash_map::Entry; let mut kts = HashMap::new(); + // An empty record type has type Type + let mut k = Const::Type; for (x, v) in kvs { // Check for duplicated entries match kts.entry(x.clone()) { @@ -164,13 +170,13 @@ fn type_one_layer( }; // Check that the fields have a valid kind - match v.ty().ty(env)? { - Some(_) => {} + match v.ty().ty().as_const() { + Some(c) => k = max(k, c), None => return span_err("InvalidFieldType"), } } - Value::from_kind(ValueKind::RecordType(kts)).to_type() + Value::from_kind(ValueKind::RecordType(kts)).to_type(k) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -226,29 +232,31 @@ fn type_one_layer( ExprKind::Field(scrut, x) => { match scrut.ty().kind() { ValueKind::RecordType(kts) => match kts.get(&x) { - Some(val) => val.clone().to_type(), + Some(val) => Type::new_infer_universe(env, val.clone())?, None => return span_err("MissingRecordField"), }, - // TODO: branch here only when scrut.ty() is a Const - _ => { - let scrut_nf = scrut.eval(env); - match scrut_nf.kind() { + ValueKind::Const(_) => { + let scrut = scrut.eval_to_type(env)?; + match scrut.kind() { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { Value::from_kind(ValueKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), - closure: Closure::new_constant(scrut_nf), + closure: Closure::new_constant( + scrut.to_value(), + ), }) - .to_type() + .to_type(scrut.ty()) } - Some(None) => scrut_nf.to_type(), + Some(None) => scrut, None => return span_err("MissingUnionField"), }, _ => return span_err("NotARecord"), } - } // _ => span_err("NotARecord"), + } + _ => return span_err("NotARecord"), } } ExprKind::Assert(t) => { @@ -295,7 +303,7 @@ fn type_one_layer( } let arg_nf = arg.eval(env); - closure.apply(arg_nf).to_type() + Type::new_infer_universe(env, closure.apply(arg_nf))? } _ => return mkerr( ErrorBuilder::new(format!( @@ -314,7 +322,7 @@ fn type_one_layer( if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } - if y.ty().ty(env)? != Some(Const::Type) { + if y.ty().ty().as_const() != Some(Const::Type) { return span_err("IfBranchMustBeTerm"); } if y.ty() != z.ty() { @@ -344,7 +352,8 @@ fn type_one_layer( Ok(r_t.clone()) })?; - Value::from_kind(ValueKind::RecordType(kts)).to_type() + let u = max(x.ty().ty(), y.ty().ty()); + Value::from_kind(ValueKind::RecordType(kts)).to_type(u) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?; @@ -357,8 +366,8 @@ fn type_one_layer( )), span.clone(), ); - let x_u = x.ty().ty_univ(env)?; - let y_u = y.ty().ty_univ(env)?; + let x_u = x.ty().ty(); + let y_u = y.ty().ty(); Type::new(hir.eval(env), max(x_u, y_u)) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { @@ -388,7 +397,7 @@ fn type_one_layer( if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } - if l.ty().ty(env)? != Some(Const::Type) { + if l.ty().ty().as_const() != Some(Const::Type) { return span_err("EquivalenceArgumentsMustBeTerms"); } @@ -480,8 +489,11 @@ fn type_one_layer( ); } + // TODO: this actually doesn't check anything yet match closure.remove_binder() { - Ok(v) => v.to_type(), + Ok(v) => { + Type::new_infer_universe(env, v.clone())? + } Err(()) => { return span_err( "MergeReturnTypeIsDependent", @@ -525,7 +537,9 @@ fn type_one_layer( } }, // Union alternative without type - Some(None) => handler_type.clone().to_type(), + Some(None) => { + Type::new_infer_universe(env, handler_type.clone())? + } None => return span_err("MergeHandlerMissingVariant"), }; match &inferred_type { @@ -560,7 +574,7 @@ fn type_one_layer( } } ExprKind::ToMap(record, annot) => { - if record.ty().ty(env)? != Some(Const::Type) { + if record.ty().ty().as_const() != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); @@ -623,7 +637,7 @@ fn type_one_layer( kts.insert("mapValue".into(), entry_type); let output_type: Type = Value::from_builtin(Builtin::List) .app(Value::from_kind(ValueKind::RecordType(kts))) - .to_type(); + .to_type(Const::Type); if let Some(annot) = annot { let annot_val = annot.eval_to_type(env)?; if output_type != annot_val { @@ -656,7 +670,10 @@ fn type_one_layer( }; } - Value::from_kind(ValueKind::RecordType(new_kts)).to_type() + Type::new_infer_universe( + env, + Value::from_kind(ValueKind::RecordType(new_kts)), + )? } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.ty(); @@ -721,7 +738,7 @@ pub(crate) fn type_with( let body = type_with(&body_env, body, None)?; let u_annot = annot.ty().as_const().unwrap(); - let u_body = match body.ty().ty(&body_env)? { + let u_body = match body.ty().ty().as_const() { Some(k) => k, _ => return mk_span_err(hir.span(), "Invalid output type"), }; -- cgit v1.2.3 From 2f65c02a995f6b6d4c755197fc074782f6bb100d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:12:44 +0000 Subject: Rename TyExpr to Tir --- dhall/src/semantics/tck/typecheck.rs | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 45b3168..7bf15af 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,8 +5,8 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv, - TyExpr, Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv, + Type, Value, ValueKind, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -69,7 +69,7 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind, + ekind: ExprKind, span: Span, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); @@ -91,8 +91,7 @@ fn type_one_layer( ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); - let t_tyexpr = typecheck(&t_hir)?; - t_tyexpr.eval_to_type(env)? + typecheck(&t_hir)?.eval_to_type(env)? } ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool), ExprKind::Lit(LitKind::Natural(_)) => { @@ -712,9 +711,9 @@ pub(crate) fn type_with( env: &TyEnv, hir: &Hir, annot: Option, -) -> Result { - let tyexpr = match hir.kind() { - HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)), +) -> Result { + let tir = match hir.kind() { + HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } @@ -753,7 +752,7 @@ pub(crate) fn type_with( ); let ty = Type::new(ty_hir.eval(env), u); - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = type_with(env, annot, None)?; @@ -765,7 +764,7 @@ pub(crate) fn type_with( let ks = annot.ty().as_const().unwrap(); let kt = body.ty().as_const().unwrap(); let ty = Type::from_const(function_check(ks, kt)); - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => { let val_annot = annot @@ -777,39 +776,39 @@ pub(crate) fn type_with( let body_env = env.insert_value(&binder, val_nf, val.ty().clone()); let body = type_with(&body_env, body, None)?; let ty = body.ty().clone(); - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } HirKind::Expr(ekind) => { let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?; let ty = type_one_layer(env, ekind, hir.span())?; - TyExpr::from_hir(hir, ty) + Tir::from_hir(hir, ty) } }; if let Some(annot) = annot { - if *tyexpr.ty() != annot { + if *tir.ty() != annot { return mk_span_err( hir.span(), &format!( "annot mismatch: {} != {}", - tyexpr.ty().to_expr_tyenv(env), + tir.ty().to_expr_tyenv(env), annot.to_expr_tyenv(env) ), ); } } - Ok(tyexpr) + Ok(tir) } /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck(hir: &Hir) -> Result { +pub(crate) fn typecheck(hir: &Hir) -> Result { type_with(&TyEnv::new(), hir, None) } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. -pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { +pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/tck/typecheck.rs | 90 +++++++++++++++++------------------- 1 file changed, 43 insertions(+), 47 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7bf15af..42a9165 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,8 +5,8 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv, - Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, + NirKind, Tir, TyEnv, Type, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -15,11 +15,11 @@ use crate::syntax::{ fn check_rectymerge( span: &Span, env: &TyEnv, - x: Value, - y: Value, + x: Nir, + y: Nir, ) -> Result<(), TypeError> { let kts_x = match x.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return mk_span_err( span.clone(), @@ -28,7 +28,7 @@ fn check_rectymerge( } }; let kts_y = match y.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return mk_span_err( span.clone(), @@ -118,7 +118,7 @@ fn type_one_layer( ExprKind::EmptyListLit(t) => { let t = t.eval_to_type(env)?; match t.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. @@ -139,18 +139,16 @@ fn type_one_layer( return span_err("InvalidListType"); } - let t = x.ty().to_value(); - Value::from_builtin(Builtin::List) - .app(t) - .to_type(Const::Type) + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) } ExprKind::SomeLit(x) => { if x.ty().ty().as_const() != Some(Const::Type) { return span_err("InvalidOptionalType"); } - let t = x.ty().to_value(); - Value::from_builtin(Builtin::Optional) + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::Optional) .app(t) .to_type(Const::Type) } @@ -165,7 +163,7 @@ fn type_one_layer( Entry::Occupied(_) => { return span_err("RecordTypeDuplicateField") } - Entry::Vacant(e) => e.insert(v.ty().to_value()), + Entry::Vacant(e) => e.insert(v.ty().to_nir()), }; // Check that the fields have a valid kind @@ -175,7 +173,7 @@ fn type_one_layer( } } - Value::from_kind(ValueKind::RecordType(kts)).to_type(k) + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -230,21 +228,21 @@ fn type_one_layer( } ExprKind::Field(scrut, x) => { match scrut.ty().kind() { - ValueKind::RecordType(kts) => match kts.get(&x) { + NirKind::RecordType(kts) => match kts.get(&x) { Some(val) => Type::new_infer_universe(env, val.clone())?, None => return span_err("MissingRecordField"), }, - ValueKind::Const(_) => { + NirKind::Const(_) => { let scrut = scrut.eval_to_type(env)?; match scrut.kind() { - ValueKind::UnionType(kts) => match kts.get(x) { + NirKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { - Value::from_kind(ValueKind::PiClosure { + Nir::from_kind(NirKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), closure: Closure::new_constant( - scrut.to_value(), + scrut.to_nir(), ), }) .to_type(scrut.ty()) @@ -261,10 +259,8 @@ fn type_one_layer( ExprKind::Assert(t) => { let t = t.eval_to_type(env)?; match t.kind() { - ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(..) => { - return span_err("AssertMismatch") - } + NirKind::Equivalence(x, y) if x == y => {} + NirKind::Equivalence(..) => return span_err("AssertMismatch"), _ => return span_err("AssertMustTakeEquivalence"), } t @@ -272,8 +268,8 @@ fn type_one_layer( ExprKind::App(f, arg) => { match f.ty().kind() { // TODO: store Type in closure - ValueKind::PiClosure { annot, closure, .. } => { - if arg.ty().as_value() != annot { + NirKind::PiClosure { annot, closure, .. } => { + if arg.ty().as_nir() != annot { return mkerr( ErrorBuilder::new(format!( "wrong type of function argument" @@ -318,7 +314,7 @@ fn type_one_layer( } } ExprKind::BoolIf(x, y, z) => { - if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { + if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } if y.ty().ty().as_const() != Some(Const::Type) { @@ -336,12 +332,12 @@ fn type_one_layer( // Extract the LHS record type let kts_x = match x_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("MustCombineRecord"), }; // Extract the RHS record type let kts_y = match y_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("MustCombineRecord"), }; @@ -352,10 +348,10 @@ fn type_one_layer( })?; let u = max(x.ty().ty(), y.ty().ty()); - Value::from_kind(ValueKind::RecordType(kts)).to_type(u) + Nir::from_kind(NirKind::RecordType(kts)).to_type(u) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?; + check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; let hir = Hir::new( HirKind::Expr(ExprKind::BinOp( @@ -379,7 +375,7 @@ fn type_one_layer( } ExprKind::BinOp(BinOp::ListAppend, l, r) => { match l.ty().kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, .. }) => {} @@ -431,14 +427,14 @@ fn type_one_layer( ExprKind::Merge(record, union, type_annot) => { let record_type = record.ty(); let handlers = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("Merge1ArgMustBeRecord"), }; let union_type = union.ty(); let variants = match union_type.kind() { - ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::UnionType(kts) => Cow::Borrowed(kts), + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::Optional, args, .. @@ -457,7 +453,7 @@ fn type_one_layer( let handler_return_type: Type = match variants.get(x) { // Union alternative with type Some(Some(variant_type)) => match handler_type.kind() { - ValueKind::PiClosure { closure, annot, .. } => { + NirKind::PiClosure { closure, annot, .. } => { if variant_type != annot { return mkerr( ErrorBuilder::new(format!( @@ -578,7 +574,7 @@ fn type_one_layer( } let record_t = record.ty(); let kts = match record_t.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return span_err("The argument to `toMap` must be a record") } @@ -598,7 +594,7 @@ fn type_one_layer( let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; let arg = match annot_val.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. @@ -606,14 +602,14 @@ fn type_one_layer( _ => return span_err(err_msg), }; let kts = match arg.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err(err_msg), }; if kts.len() != 2 { return span_err(err_msg); } match kts.get(&"mapKey".into()) { - Some(t) if *t == Value::from_builtin(Builtin::Text) => {} + Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} _ => return span_err(err_msg), } match kts.get(&"mapValue".into()) { @@ -632,10 +628,10 @@ fn type_one_layer( } let mut kts = HashMap::new(); - kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text)); + kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); - let output_type: Type = Value::from_builtin(Builtin::List) - .app(Value::from_kind(ValueKind::RecordType(kts))) + let output_type: Type = Nir::from_builtin(Builtin::List) + .app(Nir::from_kind(NirKind::RecordType(kts))) .to_type(Const::Type); if let Some(annot) = annot { let annot_val = annot.eval_to_type(env)?; @@ -649,7 +645,7 @@ fn type_one_layer( ExprKind::Projection(record, labels) => { let record_type = record.ty(); let kts = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; @@ -671,19 +667,19 @@ fn type_one_layer( Type::new_infer_universe( env, - Value::from_kind(ValueKind::RecordType(new_kts)), + Nir::from_kind(NirKind::RecordType(new_kts)), )? } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.ty(); let rec_kts = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), }; -- cgit v1.2.3 From ebe43bd6f1fd6feb1564ab9837399de7808b67b5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:39:10 +0000 Subject: Borrow relevant Hir from Tir --- dhall/src/semantics/tck/typecheck.rs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 42a9165..0787b32 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -69,7 +69,7 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { /// layer. fn type_one_layer( env: &TyEnv, - ekind: ExprKind, + ekind: ExprKind>, span: Span, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); @@ -703,11 +703,11 @@ fn type_one_layer( /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation /// to compare with. -pub(crate) fn type_with( +pub(crate) fn type_with<'hir>( env: &TyEnv, - hir: &Hir, + hir: &'hir Hir, annot: Option, -) -> Result { +) -> Result, TypeError> { let tir = match hir.kind() { HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)), HirKind::Expr(ExprKind::Var(_)) => { @@ -799,12 +799,15 @@ pub(crate) fn type_with( /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck(hir: &Hir) -> Result { +pub(crate) fn typecheck<'hir>(hir: &'hir Hir) -> Result, TypeError> { type_with(&TyEnv::new(), hir, None) } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. -pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result { +pub(crate) fn typecheck_with<'hir>( + hir: &'hir Hir, + ty: Hir, +) -> Result, TypeError> { let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?; type_with(&TyEnv::new(), hir, Some(ty)) } -- cgit v1.2.3 From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 19:12:31 +0000 Subject: Avoid re-typechecking after import --- dhall/src/semantics/tck/typecheck.rs | 1 + 1 file changed, 1 insertion(+) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 0787b32..972326b 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -710,6 +710,7 @@ pub(crate) fn type_with<'hir>( ) -> Result, TypeError> { let tir = match hir.kind() { HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)), + HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } -- cgit v1.2.3