Minimalistic prover

1 files changed, 79 insertions, 46 deletions

diff --git a/Smurf.icl b/Smurf.icl
index 9afefb8..fa5cd00 100644
--- a/Smurf.icl
+++ b/Smurf.icl
@@ -3,6 +3,7 @@ implementation module Smurf
 from StdFunc import o, flip
 import StdArray
 import StdList
+import StdMisc
 import StdString
 import StdTuple
 import StdFile
@@ -20,19 +21,32 @@ import GenPrint
 import SmurfParse
 import LaTeX
 
-derive gEq Stm
-derive gPrint (,)
-
-(<+) infixr 5 :: a b -> String | toString a & toString b
-(<+) a b = toString a +++ toString b
+derive gEq Stm, Expr, State
+derive gPrint (,), Expr
 
 instance == Stm where == a b = a === b
+instance == Expr where == a b = a === b
+instance == State where == a b = a === b
 
 instance zero [a] where zero = []
 
+/// Utilities ...
+
+(<+) infixr 5 :: a b -> String | toString a & toString b
+(<+) a b = toString a +++ toString b
+
+instance toString Expr
+where
+	toString (Lit s)      = s
+	toString (Var v)      = "$" <+ v
+	toString (ECat a b)   = a <+ b
+	toString (EHead a)    = "hd(" <+ a <+ ")"
+	toString (ETail a)    = "tl(" <+ a <+ ")"
+	toString (EQuotify a) = "q(" <+ a <+ ")"
+
 instance toString Stm
 where
-    toString (Push s) = quotify s
+    toString (Push s) = toString $ quotify s
     toString Input = "i"
     toString Output = "o"
     toString Cat = "+"
@@ -47,7 +61,7 @@ instance toChar Stm where toChar stm = (toString stm).[0]
 
 instance fromChar Stm
 where
-	fromChar '"' = Push ""
+	fromChar '"' = Push $ Lit ""
 	fromChar 'i' = Input
 	fromChar 'o' = Output
 	fromChar '+' = Cat
@@ -86,7 +100,7 @@ where toString ts = concat $ intersperse "\n" $ map toString $ reverse ts
 
 instance toLaTeX Stm
 where
-	toLaTeX (Push s) = List [Command "StmPush" [], Raw "~", sToLaTeX s]
+	toLaTeX (Push s) = List [Command "StmPush" [], Raw "~", eToLaTeX s]
 	toLaTeX Input    = Command "StmInput" []
 	toLaTeX Output   = Command "StmOutput" []
 	toLaTeX Cat      = Command "StmCat" []
@@ -113,12 +127,12 @@ where
 			intersperse (Raw ",") (map assToLaTeX ass) ++
 			[Command "}" []])
 	where
-		assToLaTeX :: (String,String) -> LaTeX
+		assToLaTeX :: (Expr,Expr) -> LaTeX
 		assToLaTeX (var,val)
 			= List
-				[ sToLaTeX var
+				[ eToLaTeX var
 				, Command "mapsto" []
-				, sToLaTeX val
+				, eToLaTeX val
 				]
 
 instance toLaTeX State
@@ -146,12 +160,12 @@ where
 			, toLaTeX st2
 			]
 
-stackToLaTeX :: [String] -> LaTeX
-stackToLaTeX ss
-	= List $ intersperse (Text ":") (map sToLaTeX ss ++ [Command "Nil" []])
+stackToLaTeX :: Stack -> LaTeX
+stackToLaTeX es
+	= List $ intersperse (Text ":") (map eToLaTeX es ++ [Command "Nil" []])
 
-sToLaTeX :: String -> LaTeX
-sToLaTeX s = Command "texttt" [List [Raw "\"", Text s, Raw "\""]]
+eToLaTeX :: Expr -> LaTeX
+eToLaTeX e = Command "texttt" [List [Raw "\"", Text (toString e), Raw "\""]]
 
 instance toLaTeX DerivationTree
 where
@@ -187,6 +201,17 @@ where
 				[Get:_]     = "rgetns"
 				[Exec:_]    = "rexecns"
 
+/// End utilities
+
+instance +++ Expr
+where
+	(+++) (Lit s) (Lit t) = Lit $ s +++ t
+	(+++) a b             = ECat a b
+
+eToCharList :: Expr -> [Char]
+eToCharList (Lit s) = fromString s
+eToCharList _       = abort "unimplemented\n"
+
 run :: !Program State io (IO io) -> (Maybe State, io)
 run prog st io iofuncs
     # (mbProgSt, io) = step prog st io iofuncs
@@ -226,32 +251,36 @@ step [Get:p] st io _
     = (pop st.stack >>= \(var,stk) ->
         pure (p, { st & stack = push (get var st.store) stk }), io)
 step [Exec:p] st io _
-    = (pop st.stack >>= parse o fromString o fst >>= \p ->
+    = (pop st.stack >>= parse o eToCharList o fst >>= \p ->
         pure (p, zero), io)
 
-push :: String Stack -> Stack
+push :: Expr Stack -> Stack
 push s st = [s:st]
 
-pop :: Stack -> Maybe (String, Stack)
+pop :: Stack -> Maybe (Expr, Stack)
 pop [] = empty
 pop [s:ss] = pure (s, ss)
 
-head :: String -> Maybe String
-head "" = empty
-head s = pure $ s % (0,0)
+head :: Expr -> Maybe Expr
+head (Lit "") = empty
+head (Lit s) = pure $ Lit $ s % (0,0)
+head e = pure $ EHead e
 
-tail :: String -> Maybe String
-tail "" = empty
-tail s = pure $ s % (1, size s - 1)
+tail :: Expr -> Maybe Expr
+tail (Lit "") = empty
+tail (Lit s) = pure $ Lit $ s % (1, size s - 1)
+tail e = pure $ ETail e
 
-put :: String String Store -> Store
+put :: Expr Expr Store -> Store
 put var val store = [(var,val) : filter ((<>)var o fst) store]
 
-get :: String Store -> String
-get var store = case filter ((==)var o fst) store of [] = ""; [(_,val):_] = val
+get :: Expr Store -> Expr
+get var store = case filter ((==)var o fst) store of
+	[]          = Lit ""
+	[(_,val):_] = val
 
-quotify :: (String -> String)
-quotify = (flip (+++) "\"") o ((+++)"\"") o toString o quot o fromString
+quotify :: Expr -> Expr
+quotify (Lit s) = Lit $ flip (+++) "\"" $ (+++)"\"" $ toString $ quot $ fromString s
 where
     quot :: [Char] -> [Char]
     quot []        = []
@@ -261,27 +290,31 @@ where
     quot ['\t':cs] = ['\\':'t':quot cs]
     quot ['"':cs]  = ['\\':'"':quot cs]
     quot [c:cs]    = [c:quot cs]
+quotify e = EQuotify e
 
 listIO :: IO ListIO
 listIO = IO read write
 where
-	read :: ListIO -> (String, ListIO)
+	read :: ListIO -> (Expr, ListIO)
 	read io=:{input} = (hd input, { io & input=tl input })
 
-	write :: String ListIO -> ListIO
+	write :: Expr ListIO -> ListIO
 	write s io=:{output} = { io & output=output ++ [s] }
 
-tree :: !Program !State !ListIO (IO ListIO) -> Maybe DerivationTree
-tree pgm st io iof
-	# init              = (pgm, io.input, st)
-	# (mbPgmSt, io)     = step pgm st io iof
-	| isNothing mbPgmSt = empty
-	# (pgm, st)         = fromJust mbPgmSt
-	| isEmpty pgm       = pure [ init --> (io.input, io.output, st)
-	                           , ([],io.input,st) --> (io.input,[],st)
-	                           ]
-	# mbTree            = tree pgm st io iof
-	| isNothing mbTree  = empty
-	# tree              = fromJust mbTree
-	# [child=:(_ --> final):children] = fromJust mbTree
-	= pure [init --> final:child:children]
+prover :: ((Program, Stack, State) -> Maybe (Stack, Stack, State))
+	Program State ListIO (IO ListIO) -> Maybe DerivationTree
+prover assumptions pgm st io iof
+# init              = (pgm, io.input, st)
+# mbAssumption      = assumptions init
+| isJust mbAssumption
+	= Just [init --> fromJust mbAssumption]
+# (mbPgmSt, io)     = step pgm st io iof
+| isNothing mbPgmSt = empty
+# (pgm, st)         = fromJust mbPgmSt
+| isEmpty pgm       = pure [ init --> (io.input, io.output, st)
+                           , ([],io.input,st) --> (io.input,[],st)
+                           ]
+# mbTree            = prover assumptions pgm st io iof
+| isNothing mbTree  = empty
+# [child=:(_ --> final):children] = fromJust mbTree
+= pure [init --> final:child:children]