1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
module proof
import StdEnv, StdDebug
from Data.Func import $
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
# tree = trace (toString tree +++ "\n") tree
= toString (toLaTeX tree)
where
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)
|
