diff options
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 118 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/nzexpr.rs | 34 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 15 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 18 | ||||
| -rw-r--r-- | tests_buffer | 1 |
5 files changed, 69 insertions, 117 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 35913cf..42da653 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -303,7 +303,9 @@ impl Value { } => TyExprKind::Expr(ExprKind::Lam( binder.to_label(), annot.to_tyexpr(qenv), - closure.normalize().to_tyexpr(qenv.insert()), + closure + .apply_var(NzVar::new(qenv.size())) + .to_tyexpr(qenv.insert()), )), ValueKind::PiClosure { binder, @@ -312,7 +314,9 @@ impl Value { } => TyExprKind::Expr(ExprKind::Pi( binder.to_label(), annot.to_tyexpr(qenv), - closure.normalize().to_tyexpr(qenv.insert()), + closure + .apply_var(NzVar::new(qenv.size())) + .to_tyexpr(qenv.insert()), )), ValueKind::AppliedBuiltin(b, args, types) => { TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold( @@ -692,120 +696,17 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { self.body.normalize_whnf(&self.env.insert_value(val)) } - pub fn apply_fresh(&self, env: QuoteEnv) -> Value { + pub fn apply_var(&self, var: NzVar) -> Value { let val = Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), NzVar::new(env.size())), + ValueKind::Var(AlphaVar::default(), var), self.arg_ty.clone(), ); self.apply(val) } - pub fn normalize(&self) -> Value { - self.body - .normalize_whnf(&self.env.insert_type(self.arg_ty.clone())) - } } /// Compare two values for equality modulo alpha/beta-equivalence. // TODO: use Rc comparison to shortcut on identical pointers -fn equiv(val1: &Value, val2: &Value) -> bool { - struct ValueWithEnv<'v> { - val: &'v Value, - env: QuoteEnv, - } - impl<'v> PartialEq for ValueWithEnv<'v> { - fn eq(&self, other: &ValueWithEnv<'v>) -> bool { - equiv_with_env(self.env, self.val, other.env, other.val) - } - } - // Push the given context into every subnode of the ValueKind. That way, normal equality of the - // resulting value will take into account the context. - fn push_context<'v>( - env: QuoteEnv, - kind: &'v ValueKind<Value>, - ) -> ValueKind<ValueWithEnv<'v>> { - kind.map_ref_with_special_handling_of_binders( - |val| ValueWithEnv { val, env }, - |_, _, val| ValueWithEnv { - val, - env: env.insert(), - }, - ) - } - - fn equiv_with_env<'v>( - env1: QuoteEnv, - val1: &'v Value, - env2: QuoteEnv, - val2: &'v Value, - ) -> bool { - use ValueKind::Var; - let kind1 = val1.as_whnf(); - let kind2 = val2.as_whnf(); - match (&*kind1, &*kind2) { - (Var(_, v1), Var(_, v2)) => { - v1 == v2 - // match (env1.lookup(v1), env2.lookup(v2)) { - // // Both vars were found in the environment, check they point to the same - // // binder. - // // Does that even make any sense with an incomplete environment ? - // // I have no clue what I'm doing anymore. - // (Some(i), Some(j)) => i == j, - // // Both vars point to outside the environment ???? - // // (None, None) => v1 == v2, - // _ => false, - // } - } - // (Var(_, v1), Var(_, v2)) => env1.lookup(v1) == env2.lookup(v2), - ( - ValueKind::LamClosure { - annot: a1, - closure: cl1, - .. - }, - ValueKind::LamClosure { - annot: a2, - closure: cl2, - .. - }, - ) => { - equiv_with_env(env1, a1, env2, a2) - && equiv_with_env( - env1.insert(), - &cl1.apply_fresh(env1), - env2.insert(), - &cl2.apply_fresh(env2), - ) - } - ( - ValueKind::PiClosure { - annot: a1, - closure: cl1, - .. - }, - ValueKind::PiClosure { - annot: a2, - closure: cl2, - .. - }, - ) => { - equiv_with_env(env1, a1, env2, a2) - && equiv_with_env( - env1.insert(), - &cl1.apply_fresh(env1), - env2.insert(), - &cl2.apply_fresh(env2), - ) - } - (k1, k2) => push_context(env1, k1) == push_context(env2, k2), - } - } - - // TODO: need to use ambiant env instead of creating new one - // Might be possible to generate free variables differently to avoid this - equiv_with_env(QuoteEnv::new(), val1, QuoteEnv::new(), val2) -} - -// TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { *self.as_whnf() == *other.as_whnf() @@ -815,7 +716,8 @@ impl std::cmp::Eq for Value {} impl std::cmp::PartialEq for Closure { fn eq(&self, other: &Self) -> bool { - self.normalize() == other.normalize() + let v = NzVar::fresh(); + self.apply_var(v) == other.apply_var(v) } } impl std::cmp::Eq for Closure {} diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 33fdde3..6559082 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -81,10 +81,12 @@ pub(crate) struct QuoteEnv { size: usize, } -// Reverse-debruijn index: counts number of binders from the bottom of the stack. #[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub(crate) struct NzVar { - idx: usize, +pub(crate) enum NzVar { + /// Reverse-debruijn index: counts number of binders from the bottom of the stack. + Bound(usize), + /// Fake fresh variable generated for expression equality checking. + Fresh(usize), } // TODO: temporary hopefully // impl std::cmp::PartialEq for NzVar { @@ -207,7 +209,9 @@ impl NzEnv { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(ty) => NzExpr::new( - NzExprKind::Var { var: NzVar { idx } }, + NzExprKind::Var { + var: NzVar::new(idx), + }, Some(ty.clone()), ), NzEnvItem::Replaced(x) => x.clone(), @@ -235,18 +239,32 @@ impl QuoteEnv { self.lookup_fallible(var).unwrap() } pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> { - let idx = self.size.checked_sub(var.idx + 1)?; + let idx = self.size.checked_sub(var.idx() + 1)?; Some(AlphaVar::new(V((), idx))) } } impl NzVar { pub fn new(idx: usize) -> Self { - NzVar { idx } + NzVar::Bound(idx) + } + pub fn fresh() -> Self { + use std::sync::atomic::{AtomicUsize, Ordering}; + // Global counter to ensure uniqueness of the generated id. + static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0); + let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); + NzVar::Fresh(id) } pub fn shift(&self, delta: isize) -> Self { - NzVar { - idx: (self.idx as isize + delta) as usize, + NzVar::new((self.idx() as isize + delta) as usize) + } + // Panics on a fresh variable. + pub fn idx(&self) -> usize { + match self { + NzVar::Bound(i) => *i, + NzVar::Fresh(_) => panic!( + "Trying to use a fresh variable outside of equality checking" + ), } } } diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index a42265d..9e8dc47 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -12,7 +12,7 @@ use crate::syntax::{ExprKind, Label, Span, V}; pub(crate) type Type = Value; // An expression with inferred types at every node and resolved variables. -#[derive(Debug, Clone)] +#[derive(Clone)] pub(crate) struct TyExpr { kind: Box<TyExprKind>, ty: Option<Type>, @@ -114,3 +114,16 @@ fn tyexpr_to_expr<'a>( } }) } + +impl std::fmt::Debug for TyExpr { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mut x = fmt.debug_struct("TyExpr"); + x.field("kind", self.kind()); + if let Some(ty) = self.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } +} diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 88c09cc..971c48d 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -164,6 +164,7 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; // let ty = tyexpr.get_type()?.to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); let ty = crate::semantics::tck::typecheck::typecheck(&expr)? .get_type()? @@ -173,6 +174,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { }); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); + // + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let ty = crate::semantics::tck::typecheck::typecheck(&expr)? + // .get_type()?; + // let expected = parse_file_str(&expected_file_path)?.to_expr(); + // let expected = crate::semantics::tck::typecheck::typecheck(&expected)? + // .normalize_whnf_noenv(); + // // if ty != expected { + // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // }), expected.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // })) + // // } + // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { let mut res = diff --git a/tests_buffer b/tests_buffer index 225fc98..a872503 100644 --- a/tests_buffer +++ b/tests_buffer @@ -47,6 +47,7 @@ success/ somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases somehow test types added to the Foo/build closures + λ(x : ∀(a : Type) → a) → x failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > |