Fix boolean beta reduce head

JonathanBrouwer · Sep 10, 2022 · a6c7100 · a6c7100
1 parent 8ec0c97
commit a6c7100
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 7 deletions.
diff --git a/lody/src/type_check/beta_eq.stx b/lody/src/type_check/beta_eq.stx
@@ -28,13 +28,13 @@ rules
   	expectBetaEq(
   		(scopePutSubst(s1, arg_name1, (empty_scope(), AlphaEqVars(arg_name1, arg_name2))), body1), 
   		(scopePutSubst(s2, arg_name2, (empty_scope(), AlphaEqVars(arg_name1, arg_name2))), body2)).
-  expectBetaEq((s1, FnDestruct(fn1, arg1)), (s2, FnDestruct(fn2, arg2))) :-
+  expectBetaEq_((s1, FnDestruct(fn1, arg1)), (s2, FnDestruct(fn2, arg2))) :-
   	expectBetaEq((s1, fn1), (s2, fn2)), expectBetaEq((s1, arg1), (s2, arg2)).
 
-  expectBetaEq((s1, BoolTrue()), (s2, BoolTrue())).
-  expectBetaEq((s1, BoolFalse()), (s2, BoolFalse())).
-  expectBetaEq((s1, BoolType()), (s2, BoolType())).
-  expectBetaEq((s1, BoolIf(c1, t1, e1)), (s2, BoolIf(c2, t2, e2))) :-
+  expectBetaEq_((s1, BoolTrue()), (s2, BoolTrue())).
+  expectBetaEq_((s1, BoolFalse()), (s2, BoolFalse())).
+  expectBetaEq_((s1, BoolType()), (s2, BoolType())).
+  expectBetaEq_((s1, BoolIf(c1, t1, e1)), (s2, BoolIf(c2, t2, e2))) :-
   	expectBetaEq((s1, c1), (s2, c2)),
   	expectBetaEq((s1, t1), (s2, t2)),
   	expectBetaEq((s1, e1), (s2, e2)).
@@ -65,7 +65,7 @@ rules
   betaReduceHead((s, e@BoolTrue())) = (s, e).
   betaReduceHead((s, e@BoolFalse())) = (s, e).
   betaReduceHead((s, e@BoolType())) = (s, e).
-  betaReduceHead((s, e@BoolIf(c, t, e))) = betaReduceHeadIf(s, betaReduceHead((s, c)), c, t, e).
+  betaReduceHead((s, BoolIf(c, t, e))) = betaReduceHeadIf(s, betaReduceHead((s, c)), c, t, e).
   betaReduceHeadIf : scope * (scope * Expr) * Expr * Expr * Expr -> (scope * Expr)
   betaReduceHeadIf(s, (_, BoolTrue()), _, t, _) = (s, t).
   betaReduceHeadIf(s, (_, BoolFalse()), _, _, e) = (s, e).

diff --git a/lody/test/typecheck_bools.spt b/lody/test/typecheck_bools.spt
@@ -28,4 +28,17 @@ test if var 2 [[
 \x: Bool.
 if x then Type else Type end
 ]]
-]] 0 errors run get-type on #1 to FnType("x", BoolType(), Type())
+]] 0 errors run get-type on #1 to FnType("x", BoolType(), Type())
+
+test and [[
+[[
+let and = \x: Bool. \y: Bool. if x then y else false end;
+and
+]]
+]] 0 errors run get-type on #1 to FnType("x", BoolType(), FnType("y", BoolType(), BoolType()))
+
+test bool decomp [[
+[[
+true : if true then Bool else Type end
+]]
+]] 0 errors run get-type on #1 to BoolType()