From a6c71001e32fa6aab5797d62555b98f86b7fe240 Mon Sep 17 00:00:00 2001
From: jonathan <jonathantbrouwer@gmail.com>
Date: Sat, 10 Sep 2022 12:16:58 +0200
Subject: [PATCH] Fix boolean beta reduce head

---
 lody/src/type_check/beta_eq.stx | 12 ++++++------
 lody/test/typecheck_bools.spt   | 15 ++++++++++++++-
 2 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/lody/src/type_check/beta_eq.stx b/lody/src/type_check/beta_eq.stx
index 6c4e5d7..474a3c7 100644
--- 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
index 8f0879c..04412aa 100644
--- 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())
\ No newline at end of file
+]] 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()
\ No newline at end of file