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)