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
35
36
37
38
39
40
41
42
43
44
45
|
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 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
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
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'])
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
# (end,f) = fend f
| end = ("", f)
# (s,f) = freadline f
# (ss,f) = readFile f
= (s +++ ss, f)
|
