diff options
Diffstat (limited to 'proof.icl')
| -rw-r--r-- | proof.icl | 34 |
1 files changed, 25 insertions, 9 deletions
@@ -5,14 +5,30 @@ import StdEnv, StdDebug from Data.Func import $ import Data.Maybe -import Smurf, SmurfParse +import Smurf, SmurfParse, LaTeX -Start = toString (devtree ass) +++ "\n" +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 +# tree = trace (toString tree +++ "\n") tree += toString (toLaTeX tree) 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) + ass :: (Program, Stack, State) -> Maybe (Stack, Stack, State) + ass (pgm, [], {stack=[Var "s":Lit x:[]], store=[]}) + | pgm == trigger = Just ([], [ECat (Var "s^R") (Lit x)], zero) + ass (pgm, ip, st) = 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) + + readFile :: !*File -> *(!String, !*File) + readFile f + # (end,f) = fend f + | end = ("", f) + # (s,f) = freadline f + # (ss,f) = readFile f + = (s +++ ss, f) |