-- module m.hs
---------------
import Lex
import Parser
import Aux
import IO

type Env = [(String,Prog)]
getVal :: String -> Env -> Prog
getVal v [] = error ("Variable "++v++" not found in Environment")
getVal v ((w,p):e) = if (v==w) then p else (getVal v e)

eval :: Env -> Prog -> Prog
-- assumes that the program is well typed
-----------------------------------------------------------------------
eval e (Axiom a t) = (Axiom a t)
eval e (App (Axiom a t) n) = App (Axiom a t) (eval e n)
eval e (App(App (Axiom a t) n) m) = App(App (Axiom a t) (eval e n)) (eval e m)
eval e (App(App(App (Axiom a t) n) m) k) = 
	App(App(App (Axiom a t) (eval e n)) (eval e m)) (eval e k)
eval e (App(App(App(App (Axiom a t) n) m) k) p) = 
     App(App(App(App (Axiom a t) (eval e n)) (eval e m)) (eval e k)) (eval e p)
-----------------------------------------------------------------------

eval e Zero = Zero
eval e (Succ p) = Succ (eval e p)
-- to be able to normalize proofs we do not evaluate Plus:
eval e (Plus p q) = Plus (eval e p) (eval e q)
--eval e (Plus p Zero) = eval e p
--eval e (Plus p (Succ q)) = Succ (eval e (Plus p q))
--eval e (Plus p (Plus q r)) = eval e (Plus p (eval e (Plus q r)))
eval e (Var v) = eval e (getVal v e)
eval e (Abs x t p) = Abs x t p
eval e (App p q) = eval e (substP f x q) where (Abs x _ f) = eval e p
eval e (Fix f t p) = eval e (substP p f (Fix f t p))
eval e (PSum ps) = PSum (map (eval e) ps)
eval e (Proj k p) = nth k ps where (PSum ps) = eval e p
eval e (Casz t m v n) = case d of
				Zero -> eval e m
				Succ p -> eval ((v,p):e) n
				_ -> error ("EVAL Casz Type Error")
			where d = eval e t
eval _ p = error ("EVAL is not defined for program: "++(printP p))
--------------------------------------------------------------------------
injAxP :: [Prog] -> Prog -> Prog
-- injects axioms in place of variables, where AxName=VarName
injAxP ax Zero = Zero
injAxP ax (Succ p) = Succ (injAxP ax p)
injAxP ax (Plus p q) = Plus (injAxP ax p) (injAxP ax q)
injAxP ax (Var v) = getAxOrVar ax v
injAxP ax (Abs x t p) = Abs x (injAxT ax t) (injAxP ax p)
injAxP ax (App p q) = App (injAxP ax p) (injAxP ax q)
injAxP ax (Fix f t p) = Fix f (injAxT ax t) (injAxP ax p)
injAxP ax (PSum ps) = PSum (map (injAxP ax) ps)
injAxP ax (Proj k p) = Proj k (injAxP ax p)
injAxP ax (Casz t m v n) = Casz (injAxP ax t) (injAxP ax m) v (injAxP ax n)
injAxP _ p = error ("injAxP is not defined for program: "++(printP p))

getAxOrVar :: [Prog] -> String -> Prog
getAxOrVar [] v = Var v
getAxOrVar ((Axiom a t):ax) v = if (a==v) then (Axiom a t) 
				else getAxOrVar ax v
injAxT ax Nat = Nat
injAxT ax (TypeVar v) = TypeVar v
injAxT ax (Pred v qs) = Pred v (map (injAxP ax) qs)
injAxT ax (TArrow t1 t2) = TArrow (injAxT ax t1) (injAxT ax t2) 
injAxT ax (T_And ts) = T_And (map (injAxT ax) ts)
injAxT ax (T_Or ts) = T_Or (map (injAxT ax) ts)
injAxT ax (TUniv  x t) = TUniv x (injAxT ax t)
injAxT ax (T_Equal r q) = T_Equal (injAxP ax r) (injAxP ax q)
injAxT ax (T_Less r q) = T_Less (injAxP ax r) (injAxP ax q)
injAxT _ t = error ("injAxT not defined on type: "++(printT t))

--------------------------------------------------------------------------
ev :: String -> IO()
ev s = putStr (printP (eval [] (sp s)))

loadString :: String -> IO String
loadString fn = do h <- openFile fn ReadMode
		   c <- hGetContents h
		   putStr (c++"\n")
		   hClose h
		   return c

loadAxioms :: String -> IO [Prog]
loadAxioms fn = if (fn=="") then return []
		else do ax <- loadString fn
			return (getAx (lex1 ax))

loadProg :: String -> IO Prog
loadProg fn = do pg <- loadString fn
		 return (getProg (lex1 pg))

loadProg' :: String -> String -> IO Prog
loadProg' af pf = do	putStr "Loading Axioms ...\n"
			ax <- loadAxioms af
			putStr "Loading Program ...\n"
			pg <- loadProg pf
			return (injAxP ax pg)

pff :: String -> String -> IO()
pff af pf = do	p <- loadProg' af pf
		printProof p

nff :: String -> String -> IO()
nff af pf = do	p <- loadProg' af pf
		printProof (eval [] p)

pf :: String -> IO()
pf s = printProof (sp s)

nf :: String -> IO()
nf s = printProof (eval [] (sp s))

printProof :: Prog -> IO()
printProof p = putStr (snd (tp [] 0 "" p))