Merge branch 'main' of github.com:bachelor-group-66-systemf/churf

sample-programs/lambda_calculus.crf

@@ -0,0 +1,63 @@
+data Exp where
+    -- Integer for the variable name to be able to use (==)
+    -- as we do not have type classes.
+    EVar : Int -> Exp
+    EInt : Int -> Exp
+    EAbs : Int -> Exp -> Exp
+    EApp : Exp -> Exp -> Exp
+    EAdd : Exp -> Exp -> Exp
+
+data Pair a b where
+    Pair : a -> b -> Pair a b
+
+data Env where
+    Env : List (Pair Int Val) -> Env
+
+data Val where
+    VInt : Int -> Val
+    VClos : Env -> Int -> Exp -> Val
+
+data List a where
+    Nil : List a
+    Cons : a -> List a -> List a
+
+-- interp : Env -> Exp -> Val
+interp env exp = case exp of
+    EInt i => VInt i
+    EAdd e1 e2 => case interp env e1 of
+        VInt i => case interp env e2 of
+            VInt j => VInt (i + j)
+    EAbs ident expr => VClos env ident expr
+    EApp e1 e2 => case interp env e1 of
+        VClos closEnv ident exp => case interp env e2 of
+            v => interp (insert ident v closEnv) exp
+            -- Crash of incorrect program
+    EVar v => lookupVar v env
+
+-- lookupVar : Int -> Env -> Val
+lookupVar ident env = case env of
+    Env list => case list of
+        Cons a as => case a of
+            Pair identy val => case ident == identy of
+                True => val
+                False => lookupVar ident (Env as)
+        -- If the variable does not exist in
+        -- the context then we just crash the program
+
+-- insert : Int -> Val -> Env -> Env
+insert ident v env = case env of
+    Env list => Env (Cons (Pair ident v) list)
+
+-- eval : Val -> Int
+eval v = case v of
+    VInt i => i
+    -- Fail unless the final value is an integer
+
+-- expression : Exp
+expression = EApp (EAbs 0 (EAdd (EVar 0) (EInt 20))) (EInt 123)
+
+-- context : Env
+context = Env Nil
+
+-- main : Int
+main = eval (interp context expression)

src/Codegen/Emits.hs

@@ -320,7 +320,7 @@ emitECased t e cases = do
         emit $ Label lbl_failPos
     emitCases rt ty label stackPtr vs (Branch (PEnum (Ident "True$Bool"), t) exp) = do
         emitCases rt ty label stackPtr vs (Branch (PLit $ LInt 1, t) exp)
-    emitCases rt ty label stackPtr vs (Branch (PEnum (Ident "False$Bool"), _) exp) = do
+    emitCases rt ty label stackPtr vs (Branch (PEnum (Ident "False$Bool"), t) exp) = do
         emitCases rt ty label stackPtr vs (Branch (PLit (LInt 0), t) exp)
     emitCases rt ty label stackPtr vs br@(Branch (PEnum consId, _) exp) = do
         emit $ Comment "Penum"

src/Main.hs

@@ -58,6 +58,7 @@ flags =
     [ Option ['d'] ["debug"] (NoArg enableDebug) "Print debug messages."
     , Option ['t'] ["type-checker"] (ReqArg chooseTypechecker "bi/hm") "Choose type checker. Possible options are bi and hm"
     , Option ['m'] ["disable-gc"] (NoArg disableGC) "Disables the garbage collector and uses malloc instead."
+    , Option ['p'] ["disable-prelude"] (NoArg disablePrelude) "Do not include the prelude"
     , Option [] ["help"] (NoArg enableHelp) "Print this help message"
     ]
 
@@ -68,6 +69,7 @@ initOpts =
         , debug = False
         , gc = True
         , typechecker = Nothing
+        , preludeOpt = True
         }
 
 enableHelp :: Options -> Options
@@ -79,6 +81,9 @@ enableDebug opts = opts{debug = True}
 disableGC :: Options -> Options
 disableGC opts = opts{gc = False}
 
+disablePrelude :: Options -> Options
+disablePrelude opts = opts{preludeOpt = False}
+
 chooseTypechecker :: String -> Options -> Options
 chooseTypechecker s options = options{typechecker = tc}
   where
@@ -92,6 +97,7 @@ data Options = Options
     , debug       :: Bool
     , gc          :: Bool
     , typechecker :: Maybe TypeChecker
+    , preludeOpt     :: Bool
     }
 
 main' :: Options -> String -> IO ()
@@ -184,4 +190,10 @@ prelude =
           ".- : Int -> Int -> Int"
         , ".- x y = 0"
         , "\n"
+        , ".== : Int -> Int -> Bool"
+        , ".== a b = case a < b of"
+        , "    False => case b < a of"
+        , "        False => True"
+        , "        _ => False"
+        , "    False => False"
         ]

test_program.crf

@@ -1,52 +1,13 @@
-data Expr where
+data Two where
-    EInt : Int -> Expr
+    This : Two
-    EBool : Bool -> Expr
+    That : Two 
-    EAdd : Expr -> Expr -> Expr
-    EAnd : Expr -> Expr -> Expr
 
-data Val where
+main = reval (eval This)
-    VInt : Int -> Val
-    VBool : Bool -> Val
 
-data Eval where
+eval x = case x of
-    Just : Val -> Eval
+    That => That
-    Nothing : Eval
+    This => eval That
-
-interp : Expr -> Eval
-interp e = case e of
-    EInt i => Just (VInt i)
-    EBool b => Just (VBool b)
-    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
-        
-
-readVal : Val -> Int
-readVal v = case v of
-    VInt i => i
-    VBool a => case a of
-        True => 1
-        False => 0
-
-main = case interp (EAdd (EAdd (EInt 3) (EInt 5)) (EBool True)) of
-    Nothing => (0 - 1)
-    Just x => case x of
 
+reval x = case x of
+   This => 123 
+   That => 123