Minimalistic prover

1 files changed, 21 insertions, 9 deletions

diff --git a/Smurf.dcl b/Smurf.dcl
index 53ab797..2c4fd1b 100644
--- a/Smurf.dcl
+++ b/Smurf.dcl
@@ -8,36 +8,46 @@ from StdOverloaded import
 
 from GenEq import generic gEq
 
-from Data.Maybe import ::Maybe
+from Data.Maybe import ::Maybe(Nothing)
 
 from LaTeX import class toLaTeX
 
-:: Stm = Push String
+:: Expr = Lit String
+        | Var String
+        | ECat Expr Expr
+        | EHead Expr
+        | ETail Expr
+        | EQuotify Expr
+
+:: Stm = Push Expr
        | Input | Output
        | Cat | Head | Tail | Quotify
        | Put | Get | Exec
 
 :: Program :== [Stm]
 
-:: Stack :== [String]
-:: Store :== [(String, String)]
+:: Stack :== [Expr]
+:: Store :== [(Expr, Expr)]
 
 :: State = { stack :: Stack
            , store :: Store
            }
 
-:: IO io = IO (io -> .(String, io)) (String io -> io)
+:: IO io = IO (io -> .(Expr, io)) (Expr io -> io)
 
-:: ListIO = { input  :: [String]
-            , output :: [String]
+:: ListIO = { input  :: [Expr]
+            , output :: [Expr]
             }
 
 :: Transition = (-->) infix 1 (Program, Stack, State) (Stack, Stack, State)
 :: DerivationTree :== [Transition]
 
-derive gEq Stm
+derive gEq Stm, Expr, State
 
 instance == Stm
+instance == Expr
+instance == State
+
 instance toString Stm
 instance toChar Stm
 instance fromChar Stm
@@ -57,4 +67,6 @@ step :: !Program State u:io u:(IO u:io) -> u:(Maybe (!Program, State), u:io)
 run :: !Program State io (IO io) -> (Maybe State, io)
 
 listIO :: IO ListIO
-tree :: !Program !State !ListIO (IO ListIO) -> Maybe DerivationTree
+prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State))
+	Program State ListIO (IO ListIO) -> Maybe DerivationTree
+tree :== prover (\_ -> Nothing)