diff options
| -rw-r--r-- | dhall/build.rs | 4 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 32 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 69 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 18 | ||||
| -rw-r--r-- | tests_buffer | 1 |
5 files changed, 59 insertions, 65 deletions
diff --git a/dhall/build.rs b/dhall/build.rs index c95a26d..cc94f5e 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -339,6 +339,8 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/CompletionWithWrongDefaultType" || path == "unit/CompletionWithWrongFieldName" || path == "unit/CompletionWithWrongOverridenType" + // TODO: enable free variable checking + || path == "unit/MergeHandlerFreeVar" }), input_type: FileType::Text, output_type: None, @@ -367,6 +369,8 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/CompletionWithWrongDefaultType" || path == "unit/CompletionWithWrongFieldName" || path == "unit/CompletionWithWrongOverridenType" + // TODO: enable free variable checking + || path == "unit/MergeHandlerFreeVar" }), input_type: FileType::Text, output_type: None, diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 532dae3..f4e4099 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::{NzVar, QuoteEnv}; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{ builtin_to_value_env, const_to_value, rc, }; @@ -855,30 +855,14 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec<NzEnvItem>, - vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { - items: Vec::new(), - vars: QuoteEnv::new(), - } + NzEnv { items: Vec::new() } } pub fn construct(items: Vec<NzEnvItem>) -> Self { - let vars = QuoteEnv::construct( - items - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(), - ); - NzEnv { items, vars } - } - pub fn as_quoteenv(&self) -> QuoteEnv { - self.vars + NzEnv { items } } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -887,7 +871,6 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); - env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { @@ -897,16 +880,9 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); - let var_idx = self.items[..idx] - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(var_idx)), + ValueKind::Var(var.clone(), NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 1b8f261..a83f175 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -44,7 +44,7 @@ impl TyEnv { } } pub fn as_quoteenv(&self) -> QuoteEnv { - self.items.as_quoteenv() + self.names.as_quoteenv() } pub fn as_nzenv(&self) -> &NzEnv { &self.items @@ -70,9 +70,6 @@ impl TyEnv { let ty = self.items.lookup_val(&var).get_type().unwrap(); Some((TyExprKind::Var(var), ty)) } - pub fn size(&self) -> usize { - self.names.size() - } } fn type_of_recordtype<'a>( @@ -312,33 +309,24 @@ fn type_one_layer( let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); match &*tf_borrow { - // ValueKind::PiClosure { annot, closure, .. } => (annot, closure), - ValueKind::PiClosure { - annot: _expected_arg_ty, - closure: ty_closure, - .. - } => { - // if arg.get_type()? != *expected_arg_ty { - // return mkerr(format!( - // "function annot mismatch: {:?}, {:?}", - // arg.get_type()?, - // expected_arg_ty - // )); - // } + ValueKind::PiClosure { annot, closure, .. } => { + if arg.get_type()? != *annot { + // return mkerr(format!("function annot mismatch")); + return mkerr(format!( + "function annot mismatch: ({} : {}) : {}", + arg.to_expr_tyenv(env), + arg.get_type()? + .to_tyexpr(env.as_quoteenv()) + .to_expr_tyenv(env), + annot + .to_tyexpr(env.as_quoteenv()) + .to_expr_tyenv(env), + )); + } let arg_nf = arg.normalize_whnf(env.as_nzenv()); - ty_closure.apply(arg_nf) + closure.apply(arg_nf) } - // ValueKind::Pi(_, _expected_arg_ty, body) => { - // // if arg.get_type()? != *tx { - // // return mkerr("TypeMismatch"); - // // } - - // let arg_nf = arg.normalize_whnf(env.as_nzenv()); - // let ret = body.subst_shift(&AlphaVar::default(), &arg_nf); - // ret.normalize_nf(); - // ret - // } _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)), } } @@ -404,14 +392,29 @@ fn type_one_layer( ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { let x_val = x.normalize_whnf(env.as_nzenv()); let y_val = y.normalize_whnf(env.as_nzenv()); - match &*x_val.as_whnf() { - ValueKind::RecordType(_) => {} + let x_val_borrow = x_val.as_whnf(); + let y_val_borrow = y_val.as_whnf(); + let kts_x = match &*x_val_borrow { + ValueKind::RecordType(kts) => kts, _ => return mkerr("RecordTypeMergeRequiresRecordType"), - } - match &*y_val.as_whnf() { - ValueKind::RecordType(_) => {} + }; + let kts_y = match &*y_val_borrow { + ValueKind::RecordType(kts) => kts, _ => return mkerr("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(env.as_quoteenv()), + ty.to_tyexpr(env.as_quoteenv()), + ), + )?; + } } + // A RecordType's type is always a const let xk = x.get_type()?.as_const().unwrap(); let yk = y.get_type()?.as_const().unwrap(); diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 971c48d..1c687f6 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -193,13 +193,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + // let mut res = + // parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + // if let Ok(e) = &res { + // // If e did typecheck, check that get_type fails + // res = e.get_type(); + // } + // res.unwrap_err(); + + let res = crate::semantics::tck::typecheck::typecheck( + &parse_file_str(&file_path)?.skip_resolve()?.to_expr(), + ); if let Ok(e) = &res { // If e did typecheck, check that get_type fails - res = e.get_type(); + e.get_type().unwrap_err(); + } else { + res.unwrap_err(); } - res.unwrap_err(); } // Checks the output of the type error against a text file. If the text file doesn't exist, // we instead write to it the output we got. This makes it easy to update those files: just diff --git a/tests_buffer b/tests_buffer index e5e1705..34210a9 100644 --- a/tests_buffer +++ b/tests_buffer @@ -49,6 +49,7 @@ success/ somehow test types added to the Foo/build closures λ(x : ∀(a : Type) → a) → x let X = 0 in λ(T : Type) → λ(x : T) → 1 + (λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > |