diff options
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 69 |
1 files changed, 36 insertions, 33 deletions
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(); |