Some fixes

1 files changed, 18 insertions, 7 deletions

diff --git a/proof.icl b/proof.icl
index a836190..33cc3d2 100644
--- a/proof.icl
+++ b/proof.icl
@@ -8,11 +8,16 @@ import Data.Maybe
 import Smurf, SmurfParse, LaTeX
 
 Start w //= trigger
-# (_,f,w)    = fopen "reverse-ward.smf" FReadText w
-# (pgm,f)    = readFile f
-# (ok,w)     = fclose f w
-# (Just pgm) = parse [c \\ c <-: pgm]
-# tree       = devtree ass pgm
+//# (_,f,w)    = fopen "reverse-ward.smf" FReadText w
+//# (pgm,f)    = readFile f
+//# (ok,w)     = fclose f w
+//# (Just pgm) = parse [c \\ c <-: pgm]
+//# tree       = devtree ass pgm zero {zero & input=[Lit "cs"]}
+// ---
+# tree       = devtree assbs innerpgm {zero & stack=[Var "s", ECat (Lit "c") (Var "t")]} zero
+// ---
+//# tree       = devtree assbs innerpgm {zero & stack=[Var "s", ECat (Lit "c") (Var "t")]} zero
+// ---
 # tree       = trace (toString tree +++ "\n") tree
 = toString (toLaTeX tree)
 where
@@ -21,9 +26,15 @@ where
 	| pgm == trigger = Just ([], [ECat (Var "s^R") (Lit x)], zero)
 	ass (pgm, ip, st) = Nothing
 
+	assbs :: (Program, Stack, State) -> Maybe (Stack, Stack, State)
+	assbs (pgm, [], {stack=[ECat (Lit "c") (ECat (Var "s") (Lit "")),ECat (Var "t") (Lit "")]})
+	| pgm == innerpgm = Just ([], [ECat (Var "t^R") (ECat (Lit "c") (Var "s"))], zero)
+	assbs _ = Nothing
+
 	trigger = fromJust (parse ['""\"\\\"u\\\"p\\\"v\\\"p\\\"w\\\"p\\\"w\\\"gh\\\"v\\\"g+\\\"v\\\"p\\\"w\\\"gt\\\"w\\\"p\\\"w\\\"g\\\"v\\\"gq\\\"o\\\"+\\\"w\\\"gq\\\"v\\\"gq\\\"u\\\"gq++\\\"u\\\"g+\\\"w\\\"gp\\\"\\\"pgx\"\"u\"p\"v\"p\"w\"p\"w\"gh\"v\"g+\"v\"p\"w\"gt\"w\"p\"w\"g\"v\"gq\"o\"+\"w\"gq\"v\"gq\"u\"gq++\"u\"g+\"w\"gp\"\"pgx'])
-	devtree ass pgm
-		= fromJust (prover ass pgm zero { zero & input = [ECat (Lit "c") (Var "s")] } listIO)
+	innerpgm = fromJust (parse ['\"\\\"u\\\"p\\\"v\\\"p\\\"w\\\"p\\\"w\\\"gh\\\"v\\\"g+\\\"v\\\"p\\\"w\\\"gt\\\"w\\\"p\\\"w\\\"g\\\"v\\\"gq\\\"o\\\"+\\\"w\\\"gq\\\"v\\\"gq\\\"u\\\"gq++\\\"u\\\"g+\\\"w\\\"gp\\\"\\\"pgx\"\"u\"p\"v\"p\"w\"p\"w\"gh\"v\"g+\"v\"p\"w\"gt\"w\"p\"w\"g\"v\"gq\"o\"+\"w\"gq\"v\"gq\"u\"gq++\"u\"g+\"w\"gp\"\"pgx'])
+	devtree ass pgm state io
+		= fromJust (prover ass pgm state io listIO)
 	
 	readFile :: !*File -> *(!String, !*File)
 	readFile f