summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/build.rs4
-rw-r--r--dhall/src/semantics/phase/normalize.rs32
-rw-r--r--dhall/src/semantics/tck/typecheck.rs69
-rw-r--r--dhall/src/tests.rs18
-rw-r--r--tests_buffer1
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 >
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 22:51:27 +0000