From c11d46956b972f06854e8a0fa3a2adb9ab979569 Mon Sep 17 00:00:00 2001
From: reijix <leon.vatthauer@fau.de>
Date: Thu, 1 Jun 2023 09:30:14 +0200
Subject: [PATCH] Defining project outline

---
 pcf.cabal        |  5 ++++
 src/Evaluator.hs | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
 src/Main.hs      |  5 ----
 src/Misc.hs      | 42 ++++++++++++++++++++++++++++++++
 src/Syntax.hs    | 45 ++++++++++++++++++++++++++++++++++
 src/Typecheck.hs |  3 +++
 6 files changed, 158 insertions(+), 5 deletions(-)
 create mode 100644 src/Evaluator.hs
 create mode 100644 src/Misc.hs
 create mode 100644 src/Syntax.hs
 create mode 100644 src/Typecheck.hs

diff --git a/pcf.cabal b/pcf.cabal
index d35d224..99b29fd 100644
--- a/pcf.cabal
+++ b/pcf.cabal
@@ -27,3 +27,8 @@ common shared
 executable pcf
   import:  shared
   main-is: Main.hs
+  other-modules: 
+    Syntax
+    Misc
+    Evaluator
+    Typecheck
diff --git a/src/Evaluator.hs b/src/Evaluator.hs
new file mode 100644
index 0000000..2584d7f
--- /dev/null
+++ b/src/Evaluator.hs
@@ -0,0 +1,63 @@
+module Evaluator where
+
+import Syntax
+import Misc
+
+-- small-step cbn semantics of PCF
+eval :: Term -> Term
+-- if-then-else
+eval (ITE T e2 e3) = e2
+eval (ITE F e2 e3) = e3
+eval (ITE e1 e2 e3) = ITE (eval e1) e2 e3
+
+-- arithmetic
+eval (ADD (Number n1) (Number n2)) = Number $ n1 + n2
+eval (ADD e1@(Number n1) e2) = ADD e1 (eval e2)
+eval (ADD e1 e2) = ADD (eval e1) e2
+eval (SUB (Number n1) (Number n2)) = Number $ n1 - n2
+eval (SUB e1@(Number n1) e2) = SUB e1 (eval e2)
+eval (SUB e1 e2) = SUB (eval e1) e2
+
+-- equality
+-- cases where both arguments are evaluated already
+eval (EQ (Number n1) (Number n2)) = if n1 == n2 then T else F
+eval (EQ T T) = T
+eval (EQ F F) = T
+eval (EQ T F) = F
+eval (EQ F T) = F
+-- left argument is evaluated, eval the right one
+eval (EQ e1@(Number n1) e2) = EQ e1 (eval e2)
+eval (EQ T e2) = EQ T (eval e2)
+eval (EQ F e2) = EQ F (eval e2)
+-- no argument is evaluated, eval the left one
+eval (EQ e1 e2) = EQ (eval e1) e2
+
+-- application
+-- beta reduction
+eval (App (Abs x p) q) = subst (\y -> if x == y then q else Var y) p
+-- fixpoint combinator
+eval (App Fix f) = App f (App Fix f)
+-- reduce lhs
+eval (App e1 e2) = App (eval e1) e2
+
+-- products
+eval (Fst (Pair t1 t2)) = t1
+eval (Fst t) = Fst (eval t)
+eval (Snd (Pair t1 t2)) = t2
+eval (Snd t) = Snd (eval t)
+
+-- sums and lists
+eval (Case (Inl t) t1 t2) = App t1 t
+eval (Case (Inr t) t1 t2) = App t2 t
+eval (Case Nil t1 t2) = t1
+eval (Case (Cons x xs) t1 t2) = App (App t2 x) xs
+eval (Case t1 t2 t3) = Case (eval t1) t2 t3
+
+-- Term is normalform
+eval e = e
+
+
+-- exhaustive evaluation
+evalStar :: Term -> Term
+evalStar e = if e == e' then e else evalStar e'
+    where e' = eval e
\ No newline at end of file
diff --git a/src/Main.hs b/src/Main.hs
index 4f50f14..7377992 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -1,10 +1,5 @@
 module Main where
 
-{- |
- Main entry point.
-
- The `, run` script will invoke this function.
--}
 main :: IO ()
 main = do
   print "Hello world"
diff --git a/src/Misc.hs b/src/Misc.hs
new file mode 100644
index 0000000..d1f8195
--- /dev/null
+++ b/src/Misc.hs
@@ -0,0 +1,42 @@
+module Misc where
+
+-- calculates free variables in a Term
+freeVars :: Term -> [Name]
+freeVars (Var x) = [x]
+freeVars (ITE e1 e2 e3) = freeVars e1 ++ freeVars e2 ++ freeVars e3
+freeVars (ADD e1 e2) = freeVars e1 ++ freeVars e2
+freeVars (SUB e1 e2) = freeVars e1 ++ freeVars e2
+freeVars (EQ e1 e2) = freeVars e1 ++ freeVars e2
+freeVars (App e1 e2) = freeVars e1 ++ freeVars e2
+freeVars (Abs x p) = filter (/= x) $ freeVars p
+freeVars _ = []
+
+-- infinite list of variable names (used for capture avoiding substitution)
+vars :: [Name]
+vars = ['v' : show n | n <- [1..]]
+
+-- capture-avoiding substitution
+subst :: (Name -> Term) -> Term -> Term
+subst o (Var x) = o x
+subst o (ITE e1 e2 e3) = ITE (subst o e1) (subst o e2) (subst o e3)
+subst o (Case e1 e2 e3) = Case (subst o e1) (subst o e2) (subst o e3)
+subst o (ADD e1 e2) = ADD (subst o e1) (subst o e2)
+subst o (SUB e1 e2) = SUB (subst o e1) (subst o e2)
+subst o (EQ e1 e2) = EQ (subst o e1) (subst o e2)
+subst o (App e1 e2) = App (subst o e1) (subst o e2)
+subst o (Cons e1 e2) = Cons (subst o e1) (subst o e2)
+subst o (Pair e1 e2) = Pair (subst o e1) (subst o e2)
+subst o (Fst e) = Fst (subst o e)
+subst o (Snd e) = Snd (subst o e)
+subst o (Inl e) = Inl (subst o e)
+subst o (Inr e) = Inr (subst o e)
+subst o e@(Abs x p) = Abs y (subst o' p)
+    where
+        y = if isFresh x then x else fromJust $ find isFresh vars
+        o' v
+            | v == x = Var y
+            | otherwise = o v
+        zs = map o $ freeVars e
+        isFresh :: Name -> Bool
+        isFresh e = not (any (elem e . freeVars) zs)
+subst o e = e -- Terms without freeVars
\ No newline at end of file
diff --git a/src/Syntax.hs b/src/Syntax.hs
new file mode 100644
index 0000000..bf17788
--- /dev/null
+++ b/src/Syntax.hs
@@ -0,0 +1,45 @@
+module Syntax where
+
+type Name = String
+
+data Term
+    = T | F
+    | ITE Term Term Term
+    | Number Int
+    | ADD Term Term
+    | SUB Term Term
+    | EQ Term Term
+    | Fst Term
+    | Snd Term
+    | Inl Term
+    | Inr Term
+    | Case Term Term Term
+    | Nil
+    | Cons Term Term
+    | Pair Term Term
+    | Var Name
+    | App Term Term
+    | Abs Name Term
+    | Fix
+    deriving (Eq)
+
+instance Show Term where
+    show T = "true"
+    show F = "false"
+    show (ITE t1 t2 t3) = "if (" ++ show t1 ++ ")\n  then (" ++ show t2 ++ ")\n  else (" ++ show t3 ++ ")"
+    show (Case t1 t2 t3) = "\n  case (" ++ show t1 ++ ") of\n    <0> => (" ++ show t2 ++ ");\n    <1> => (" ++ show t3 ++ ")"
+    show (ADD t1 t2) = "(" ++ show t1 ++ ") + (" ++ show t2 ++ ")"
+    show (SUB t1 t2) = "(" ++ show t1 ++ ") - (" ++ show t2 ++ ")"
+    show (EQ t1 t2) = "(" ++ show t1 ++ ") == (" ++ show t2 ++ ")"
+    show (Number n) = show n
+    show (Fst t) = "fst " ++ show t
+    show (Snd t) = "snd " ++ show t
+    show (Inl t) = "inl " ++ show t
+    show (Inr t) = "inr " ++ show t
+    show Nil = "[]"
+    show (Cons t1 t2) = "(" ++ show t1 ++ ") : (" ++ show t2 ++ ")"
+    show (Pair t1 t2) = "(" ++ show t1 ++ ", " ++ show t2 ++ ")"
+    show (Var n) = n
+    show (App t1 t2) = "(" ++ show t1 ++ ") " ++ show t2
+    show Fix = "Y"
+    show (Abs x p) = "\\" ++ x ++ ". " ++ show p
\ No newline at end of file
diff --git a/src/Typecheck.hs b/src/Typecheck.hs
new file mode 100644
index 0000000..ff8bc5e
--- /dev/null
+++ b/src/Typecheck.hs
@@ -0,0 +1,3 @@
+module Typecheck where
+
+import Syntax
\ No newline at end of file