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)