Fixed some reviews

Going from the `ifte` way to the different rules would be better if `typecheck`
wouldn't have two responsibilities, to typecheck and to traverse the
AST looking for `Promise()`.

makam-spec/src/eval.makam

@@ -35,7 +35,7 @@ eval (ebinop E1 Op E2) V :-
   eval_binop Op V1 V2 V.
 
 eval_binop add (eint N1) (eint N2) (eint N) :- plus N1 N2 N.
-eval_binop sub (eint N1) (eint N2) (eint N) :- plus N2 N N1, if (lessthan N 0 true) then (log_error _ `no negatives allowed`, failure) else success.
+eval_binop sub (eint N1) (eint N2) (eint N) :- plus N2 N N1.
 eval_binop mul (eint N1) (eint N2) (eint N) :- mult N1 N2 N.
 
 eval_unop : unop -> expr -> expr -> prop.

makam-spec/src/examples.makam

@@ -1,12 +1,14 @@
 
 print "Simple example without let" ?
 
+print "Return 6" ?
 interpreter "
 (fun x => x + x) 3
 " V T ?
 
 print "Promises are check before running, assumes after" ?
 
+print "Typecheck fail" ?
 interpreter "
 let ( id = fun t => t ) in
 
@@ -15,6 +17,7 @@ Ifte( ( Promise(Bool -> Bool, id) ) true, 3, Promise(Num, true))
 )
 " V T ?
 
+print "Return 3" ?
 interpreter "
 let ( id = fun t => t ) in
 
@@ -23,6 +26,7 @@ Ifte( ( Promise(Bool -> Bool, id) ) true, 3, Assume(Num, true))
 )
 " V T ?
 
+print "Blame" ?
 interpreter "
 let ( id = fun t => t ) in
 
@@ -31,6 +35,7 @@ Ifte( ( Promise(Bool -> Bool, id) ) false, 3, Assume(Num, true))
 )
 " V T ?
 
+print "Return 5" ?
 interpreter "
 let ( id = fun t => t ) in
 
@@ -39,25 +44,29 @@ Ifte( ( Promise(Bool -> Bool, id) ) false, 3, Assume(Num, 5))
 )
 " V T ?
 
-
 print " We don't have let polymorphism (any) " ?
 
+print "Typecheck fail" ?
 interpreter "
 let (id = fun x => x) in
 Ifte(true, Promise(Num, id 3), Promise(Bool, id true))
 " V T ?
 
+print "Return 3" ?
 interpreter "
 let (id = fun x => x) in
 Ifte(true, Promise(Num, id 3), Assume(Bool, id true))
 " V T ?
 
+print "Return true" ?
 interpreter "
 let (id = fun x => x) in
 Ifte(false, Promise(Num, id 3), Assume(Bool, id true))
 " V T ?
 
 print "This is bad because order matters!!" ?
+
+print "Typecheck fail" ?
 interpreter "
 let (id = fun x => x) in
 Ifte(true, Assume(Bool, id true), Promise(Num, id 3))
@@ -65,6 +74,7 @@ Ifte(true, Assume(Bool, id true), Promise(Num, id 3))
 
 print "We can still use Assume(...)s" ?
 
+print "Return 3" ?
 interpreter "
 let (id = fun x => x) in
 Ifte(true, Promise( Num , id 3), Promise( Bool, Assume( Bool -> Bool , id ) true))

makam-spec/src/typecheck.makam

@@ -16,27 +16,35 @@ typecheck (lam (bind _ B)) (tarrow S T) :-
     ).
 
 typecheck (app A B) T :-
-    typecheck A ATy,
+    typecheck A (tarrow S T),
+    typecheck B S.
+typecheck (app A B) tdyn :-
+    typecheck A (tarrow S _),
     typecheck B BTy,
-    ifte (eq ATy (tarrow S T'))
+    not (eq S BTy).
-        (ifte (eq BTy S)
+typecheck (app A B) tdyn :-
-            (eq T' T)
+    typecheck A ATy,
-            (eq tdyn T))
+    not (eq ATy (tarrow _ _)),
-        (eq tdyn T).
+    typecheck B _.
 
 typecheck (eint _) tnum.
 typecheck (ebool _) tbool.
 typecheck (estr _) tstr.
 
 typecheck (ite C T E) Ty :-
-    typecheck C CTy,
+    typecheck C tbool,
+    typecheck T Ty,
+    typecheck E Ty.
+typecheck (ite C T E) tdyn :-
+    typecheck C tbool,
     typecheck T TTy,
     typecheck E ETy,
-    ifte (eq CTy tbool)
+    not (eq TTy ETy).
-        (ifte (eq TTy ETy)
+typecheck (ite C T E) tdyn :-
-            (eq Ty TTy)
+    typecheck C CTy,
-            (eq Ty tdyn))
+    not (eq Cty tbool),
-        (eq Ty tdyn).
+    typecheck T _,
+    typecheck E _.
 
 typecheck (eunop blame _) _.
     
@@ -44,19 +52,24 @@ typecheck (eunop isNum _) tbool.
 typecheck (eunop isBool _) tbool.
 typecheck (eunop isFun _) tbool.
 
-typecheck (ebinop A _ B) Ty :-
+typecheck (ebinop A _ B) tnum :-
-    typecheck A ATy,
+    typecheck A tnum,
-    typecheck B BTy,
+    typecheck B tnum.
-    ifte (eq ATy tnum)
+typecheck (ebinop A _ B) tdyn :-
-        (ifte (eq BTy tnum)
+    typecheck A tnum,
-            (eq Ty tnum)
+    typecheck B Bty,
-            (eq Ty tdyn))
+    not (eq Bty tnum).
-        (eq Ty tdyn).
+typecheck (ebinop A _ B) tdyn :-
+    typecheck A Aty,
+    not (eq Aty tnum),
+    typecheck B _.
 
-typecheck (promise Ty E) T :-
+typecheck (promise Ty E) Ty :-
-    ifte (typecheck E Ty)
+    typecheck E Ty.
-        (eq T Ty)
+typecheck (promise Ty E) _ :-
-        (and (log_error Ty `Couldnt check Promise(...)`) failure).
+    not (typecheck E Ty),
+    log_error Ty `Couldnt check Promise(...)`,
+    failure.
 
 (* The type of an Assume construct doesn't depend on the term *)
 typecheck (assume Ty _ E) Ty :-