section 4. arithHEADmain

1 files changed, 59 insertions, 0 deletions

diff --git a/arith/Core.hs b/arith/Core.hs
new file mode 100644
index 0000000..acec5b4
--- /dev/null
+++ b/arith/Core.hs
@@ -0,0 +1,59 @@
+module Core
+    ( Term(..)
+    , isNumericVal
+    , isVal
+    , eval
+    ) where
+
+data Term = TmTrue
+          | TmFalse
+          | TmIf Term Term Term
+          | TmZero
+          | TmSucc Term
+          | TmPred Term
+          | TmIsZero Term
+
+instance Show Term where
+    show TmTrue          = "true"
+    show TmFalse         = "false"
+    show (TmIf t1 t2 t3) = "if " ++ show t1 ++ " then " ++ show t2 ++ " else " ++ show t3
+    show TmZero          = "0"
+    show (TmSucc t)      = "succ " ++ show t
+    show (TmPred t)      = "pred " ++ show t
+    show (TmIsZero t)    = "iszero " ++ show t
+
+isNumericVal :: Term -> Bool
+isNumericVal TmZero      = True
+isNumericVal (TmSucc t1) = isNumericVal t1
+isNumericVal _           = False
+
+isVal :: Term -> Bool
+isVal TmTrue  = True
+isVal TmFalse = True
+isVal t       = isNumericVal t
+
+eval1 :: Term -> Maybe Term
+eval1 (TmIf TmTrue  t2 t3) = Just t2
+eval1 (TmIf TmFalse t2 t3) = Just t3
+eval1 (TmIf t1      t2 t3) = do
+    t1' <- eval1 t1
+    return $ TmIf t1' t2 t3
+eval1 (TmSucc t1) = do
+    t1' <- eval1 t1
+    return $ TmSucc t1'
+eval1 (TmPred TmZero)                          = Just $ TmZero
+eval1 (TmPred (TmSucc nv1)) | isNumericVal nv1 = Just nv1
+eval1 (TmPred t1)                              = do
+    t1' <- eval1 t1
+    return $ TmPred t1'
+eval1 (TmIsZero TmZero)                          = Just $ TmTrue
+eval1 (TmIsZero (TmSucc nv1)) | isNumericVal nv1 = Just $ TmFalse
+eval1 (TmIsZero t1)                              = do
+    t1' <- eval1 t1
+    return $ TmIsZero t1'
+eval1 _ = Nothing
+
+eval :: Term -> Term
+eval t = case eval1 t of
+    Just t' -> eval t'
+    Nothing -> t