diff options
| author | Nadrieril | 2019-05-05 00:43:41 +0200 |
|---|---|---|
| committer | Nadrieril | 2019-05-05 00:43:41 +0200 |
| commit | 8e4182f26b20b28f60fb0c21b3e08e19314de9a0 (patch) | |
| tree | afcb15e7567275b0af228099e60e1a7adc50be57 /dhall/src/typecheck.rs | |
| parent | dadcd9aa595bf3f469514ccb586eace61a9c6b03 (diff) | |
Make Value equality be alpha-equivalence
Closes #66, #65
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/typecheck.rs | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 8137417..2b87bd2 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -243,8 +243,7 @@ where T: Borrow<Type>, U: Borrow<Type>, { - eL0.borrow().to_value().normalize_to_expr_maybe_alpha(true) - == eR0.borrow().to_value().normalize_to_expr_maybe_alpha(true) + eL0.borrow().to_value() == eR0.borrow().to_value() } fn const_to_typed(c: Const) -> Typed { @@ -352,9 +351,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> { forall (nothing: optional) -> optional ), - // TODO: alpha-equivalence in type-inference tests OptionalNone => dhall::expr!( - forall (A: Type) -> Optional A + forall (a: Type) -> Optional a ), } } @@ -436,7 +434,7 @@ impl TypeIntermediate { Typed::from_thunk_and_type( Value::Pi( - x.clone(), + x.clone().into(), TypeThunk::from_type(ta.clone()), TypeThunk::from_type(tb.clone()), ) @@ -823,12 +821,11 @@ fn type_last_layer( match &r.internal_whnf() { Some(Value::UnionType(kts)) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > - // TODO: use "_" instead of x (i.e. compare types using equivalence in tests) Some(Some(t)) => { Ok(RetType( TypeIntermediate::Pi( ctx.clone(), - x.clone(), + "_".into(), t.to_type(ctx)?, r.clone(), ) |