Fixed desugar and made interpret

src/Desugar/Desugar.hs

@@ -68,7 +68,7 @@ desugarExp = \case
     -- EAbsS pat e -> EAbs (LIdent "$zz$") (ECase (EVar "$zz$") [Branch (desugarPattern pat) (desugarExp e)])
     ELet b e                      -> ELet (desugarBind b) (desugarExp e)
     ECase e br                    -> ECase (desugarExp e) (map desugarBranch br)
-    EAnn e t                      -> EAnn (desugarExp e) t
+    EAnn e t                      -> EAnn (desugarExp e) (desugarType t)
     EVarS (VSymbol (Symbol symb)) -> EVar (LIdent $ fixName symb)
     EVarS (VIdent (LIdent ident)) -> EVar $ LIdent $ fixName ident
     EVar i                        -> EVar i

test_program.crf

@@ -1,59 +1,52 @@
--- Peano naturals
+data Expr where
-data Nat where
+    EInt : Int -> Expr
-  Zero : Nat
+    EBool : Bool -> Expr
-  Succ : Nat -> Nat
+    EAdd : Expr -> Expr -> Expr
+    EAnd : Expr -> Expr -> Expr
 
--- Returns 10_000
+data Val where
-main = toInt (fromInt 10000)
+    VInt : Int -> Val
+    VBool : Bool -> Val
 
--- Peano arithmetic --
+data Eval where
+    Just : Val -> Eval
+    Nothing : Eval
 
--- Peano addition
+interp : Expr -> Eval
-add : Nat -> Nat -> Nat
+interp e = case e of
-add left right = case left of
+    EInt i => Just (VInt i)
-    Zero => right
+    EBool b => Just (VBool b)
-    Succ n => Succ (add n right)
+    EAdd e1 e2 => case interp e1 of
+        Just x => case x of
+            VInt i => case interp e2 of
+                Nothing => Nothing
+                Just y => case y of
+                    VInt j => Just (VInt (i + j))
+                    _ => Nothing
+            _ => Nothing
+        Nothing => Nothing
+    EAnd e1 e2 => case interp e1 of
+        Just x => case x of
+            VBool i => case interp e2 of
+                Just y => case y of
+                    VBool j => case i of 
+                        True => case j of
+                            True => Just (VBool True)
+                            _ => Just (VBool False)
+                        _ => Just (VBool False)
+                Nothing => Nothing
+            _ => Nothing
+        Nothing => Nothing
         
--- Peano multiplication
-mul : Nat -> Nat -> Nat
-mul left right = case right of
-    Zero => Zero
-    Succ n => add left (mul left n)
 
-eq : Nat -> Nat -> Nat
+readVal : Val -> Int
-eq a b = case a of
+readVal v = case v of
-    Zero => case b of 
+    VInt i => i
-        Zero => Succ Zero
+    VBool a => case a of
-        _    => Zero
+        True => 1
-    Succ n => case b of
+        False => 0
-        Zero => Zero
-        Succ m => eq n m
 
-less : Nat -> Nat -> Nat
+main = case interp (EAdd (EAdd (EInt 3) (EInt 5)) (EBool True)) of
-less a b = case a of
+    Nothing => (0 - 1)
-    Zero => case b of
+    Just x => case x of
-        Zero => Zero
-        Succ n => Succ Zero
-    Succ n => case b of
-        Zero => Zero
-        Succ m => less n m
 
-greater : Nat -> Nat -> Nat
-greater a b = case b of
-    Zero => case a of
-        Zero => Zero
-        Succ n => Succ Zero
-    Succ n => case a of
-        Zero => Zero
-        Succ m => less n m
-
--- Aux
-
-toInt : Nat -> Int
-toInt a = case a of
-    Succ n => 1 + toInt n
-    Zero => 0
-
-fromInt a = case a of
-    0 => Zero
-    n => Succ (fromInt (a - 1))