Minimalistic prover

8 files changed, 192 insertions, 62 deletions

diff --git a/.gitignore b/.gitignore
index 1eabc20..f4c8bfe 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,6 +3,7 @@
 *.out
 run
 tree
+proof
 
 # Directory used to store object files, abc files and assembly files
 Clean System Files/
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)
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]
diff --git a/SmurfParse.icl b/SmurfParse.icl
index 71bfc34..81f6c2f 100644
--- a/SmurfParse.icl
+++ b/SmurfParse.icl
@@ -16,7 +16,7 @@ import Smurf
 
 parse :: ![Char] -> Maybe Program
 parse []       = pure []
-parse ['"':cs] = parseString cs >>= \(s,cs`) -> append (Push s) $ parse cs`
+parse ['"':cs] = parseString cs >>= \(s,cs`) -> append (Push $ Lit s) $ parse cs`
 parse ['i':cs] = apparse Input cs
 parse ['o':cs] = apparse Output cs
 parse ['+':cs] = apparse Cat cs
diff --git a/proof.icl b/proof.icl
new file mode 100644
index 0000000..3ea9b1a
--- /dev/null
+++ b/proof.icl
@@ -0,0 +1,18 @@
+module proof
+
+import StdEnv, StdDebug
+
+from Data.Func import $
+import Data.Maybe
+
+import Smurf, SmurfParse
+
+Start = toString (devtree ass) +++ "\n"
+where
+	ass (pgm, ip, st)
+		| pgm == [Tail,Tail] && st.stack == [Lit "bcd"]
+			= Just ([], [], {st & stack=[Lit "d"]})
+		= Nothing
+	pgm = fromJust $ parse ['ittt']
+	devtree ass
+		= fromJust (prover ass pgm zero { zero & input = [Lit "abcd"] } listIO)
diff --git a/proof.prj b/proof.prj
new file mode 100644
index 0000000..0519a34
--- /dev/null
+++ b/proof.prj
@@ -0,0 +1,61 @@
+Version: 1.4
+Global
+	ProjectRoot:	.
+	Target:	StdEnv
+	Exec:	{Project}/proof
+	CodeGen
+		CheckStacks:	False
+		CheckIndexes:	True
+	Application
+		HeapSize:	2097152
+		StackSize:	512000
+		ExtraMemory:	8192
+		IntialHeapSize:	204800
+		HeapSizeMultiplier:	4096
+		ShowExecutionTime:	False
+		ShowGC:	False
+		ShowStackSize:	False
+		MarkingCollector:	False
+		DisableRTSFlags:	False
+		StandardRuntimeEnv:	True
+		Profile
+			Memory:	False
+			MemoryMinimumHeapSize:	0
+			Time:	False
+			Stack:	False
+		Output
+			Output:	BasicValuesOnly
+			Font:	Monaco
+			FontSize:	9
+			WriteStdErr:	False
+	Link
+		LinkMethod:	Static
+		GenerateRelocations:	False
+		GenerateSymbolTable:	False
+		GenerateLinkMap:	False
+		LinkResources:	False
+		ResourceSource:	
+		GenerateDLL:	False
+		ExportedNames:	
+	Paths
+		Path:	{Project}/
+		Path:	{Application}/lib/Generics/
+		Path:	{Application}/lib/StdLib/
+		Path:	{Application}/lib/clean-platform/OS-Independent/
+		Path:	{Application}/lib/clean-platform/OS-Linux-64/
+	Precompile:	
+	Postlink:	
+MainModule
+	Name:	proof
+	Dir:	{Project}
+	Compiler
+		NeverMemoryProfile:	False
+		NeverTimeProfile:	False
+		StrictnessAnalysis:	True
+		ListTypes:	StrictExportTypes
+		ListAttributes:	True
+		Warnings:	True
+		Verbose:	True
+		ReadableABC:	False
+		ReuseUniqueNodes:	True
+		Fusion:	False
diff --git a/run.icl b/run.icl
index 64ef079..385d987 100644
--- a/run.icl
+++ b/run.icl
@@ -17,6 +17,11 @@ import SmurfParse
 derive gEq SmurfOpt
 instance == SmurfOpt where == a b = a === b
 
+instance <<< Expr
+where
+	(<<<) f (Lit s) = f <<< s
+	// TODO Rest unimplemented for now
+
 Start :: *World -> *World
 Start w
 // Options
@@ -25,7 +30,7 @@ Start w
 | errs <> [] = error errs w
 # breakstms
 	= if (isMember BreakAll opts)
-		[Push "", Input, Output, Cat, Head, Tail, Quotify, Put, Get, Exec]
+		[Push (Lit ""), Input, Output, Cat, Head, Tail, Quotify, Put, Get, Exec]
 		[fromChar c \\ (Break c) <- opts]
 # inputs = [f \\ (IFile f) <- opts]
 | length inputs <> 1 = error ["Exactly one input file required"] w
@@ -61,18 +66,18 @@ where
 	where
 		isBrk :: Program -> Bool
 		isBrk [] = False
-		isBrk [(Push _):_] = isMember (Push "") brk
+		isBrk [(Push _):_] = isMember (Push (Lit "")) brk
 		isBrk [stm:_] = isMember stm brk
 
 		iofunc :: *IO *File
 		iofunc = IO read show
 		where
-			read :: *File -> *(String, *File)
+			read :: *File -> *(Expr, *File)
 			read f
 				# (s, f) = freadline f
-				= (s % (0, size s - 2), f)
+				= (Lit (s % (0, size s - 2)), f)
 
-			show :: String *File -> *File
+			show :: Expr *File -> *File
 			show s f = f <<< s
 
 	options = [ Option ['i'] ["infile"]
diff --git a/tree.icl b/tree.icl
index f895c89..5472b40 100644
--- a/tree.icl
+++ b/tree.icl
@@ -20,7 +20,7 @@ Start w
 # tree       = trace (toString tree +++ "\n") tree
 = toString (toLaTeX tree)
 where
-	devtree pgm = fromJust (tree pgm zero { zero & input = [""] } listIO)
+	devtree pgm = fromJust (tree pgm zero { zero & input = [Lit ""] } listIO)
 
 	readFile :: !*File -> *(!String, !*File)
 	readFile f