> module Main where

> import System
> import System.IO
> import System.Console.Readline
> import Debug.Trace
> import Char
> import Monad
> import List
> import Ivor.TT

> import Logic
> import Parser

Add all the necessary data structures and definitions to the environment.
Also adds variables A-Z as axioms.

> initialise = do st <- foldM (\a b -> addAxiom a (name [b]) "*") emptyContext
>                          ['A'..'Z']
>                 st <- addData st "And (A:*)(B:*) : * = and_intro : (a:A)(b:B)(And A B)"
>                 st <- addData st $  "Or (A:*)(B:*) : * "++
>                                     "= or_intro_l : (a:A)(Or A B)" ++
>                                     "| or_intro_r : (b:B)(Or A B)"
> --              st <- addData st "Ex (A:*)(P:(a:A)*) : * = ex_intro : (x:A)(p:P x)(Ex A P)"
>                 st <- addData st "False : * =";
>                 st <- addData st "True : * = II : True";
>                 st <- addDef st (name "not") "[A:*](a:A)False"
>                 st <- addDef st (name "notElim") "[A:*][p:not A][pp:A](p pp)"
>                 return st

And and or introduction are straightforward refinements by their 
constructors. 

> inl, inr, and_intro :: Tactic
> inl = refine "or_intro_l" >+> keepSolving
> inr = refine "or_intro_r" >+> keepSolving
> and_intro = refine "and_intro" >+> keepSolving

(Not actually used yet)

> exists :: String -> Tactic
> exists tm = refine "exists" >->
>             fill tm

> false = (Name TypeCon (name "False"))

Not introduction needs to rewrite the goal to be in a suitable form
for introduction (not A is just A->False).

> notassume :: Tactic
> notassume = unfold (name "not") >+> intro 

Contradiction tactic works by claiming there is a contradiction, proving 
the goal by induction on this contradiction, then using notElim to
demonstrate that there is a contradiction. If the tactic doesn't work
with the premises one way, try them the other way.

> contradiction :: String -> String -> Tactic
> contradiction x y = claim (name "false") "False" >+>
>                     induction "false" >+>
>                     (try (fill $ x ++ " " ++ y)
>                           idTac
>                           (fill $ y ++ " " ++ x))

> ivor :: TTM a -> IO a
> ivor (Left err) = fail (show err)
> ivor (Right x) = return x

> main :: IO ()
> main = do ctxt <- ivor initialise
>           ctxt <- proveIt ctxt
>           tm <- ivor $ check ctxt "thm"
>           putStrLn "Proof complete. Proof term is:"
>           def <- ivor $ getDef ctxt (name "thm")
>           putStrLn $ show (eval ctxt def) ++ "\n"
>           main

> proveIt :: Context -> IO Context
> proveIt ctxt = 
>     do putStr "Enter a formula to prove (? at any time for help): "
>        hFlush stdout
>        formline <- readline ""
>        case formline of
>             Nothing -> proveIt ctxt
>             (Just form) -> do
>                when (form == "Quit") $ exitWith ExitSuccess
>                if (form == "?" || form == "") 
>                   then do fhelp
>                           proveIt ctxt
>                   else case parseFormula form of
>                            Failure err -> do 
>                              putStrLn err
>                              fhelp
>                              proveIt ctxt
>                            Success tm -> do 
>                              ctxt <- ivor $ theorem ctxt (name "thm") (mkTerm tm)
>                              doProof True (save ctxt)

> fhelp = do putStrLn "Syntax: Variables A-Z; connectives ~, /\\, \\/ and ->"
>            putStrLn "e.g. Try proving these (they are all provable!):"
>            putStrLn "\t(A -> B) -> A -> B"
>            putStrLn "\tA /\\ B -> B /\\ A"
>            putStrLn "\tA \\/ B -> B \\/ A"
>            putStrLn "\tA /\\ ~A -> C"
>            putStrLn "\t~(A /\\ ~A)"
>            putStrLn "\tA \\/ B -> C -> B \\/ (A /\\ C)"
>            putStrLn "\t~(A /\\ B) -> ~(B /\\ A)"
>            putStrLn "\t~(A \\/ B) -> ~(B \\/ A)"
>            putStrLn "\t(A \\/ ~A) -> ((A -> B) -> A) -> A"
>            putStrLn ""
>            putStrLn "type Quit to exit"
>            putStrLn ""

> commhelp = do putStrLn "Available commands (case sensitive):"
>               putStrLn "\tassume [optional name]\t\t(-> introduction)"
>               putStrLn "\tsplit\t\t\t\t(/\\ introduction)"
>               putStrLn "\tleft [optional name]\t\t(\\/ introduction)"
>               putStrLn "\tright [optional name]\t\t(\\/ introduction)"
>               putStrLn "\tnegate\t\t\t\t(~ introduction)"
>               putStrLn "\tapply [name]\t\t\t(-> elimination, or use a premise directly)"
>               putStrLn "\telim [name]\t\t\t(/\\ or \\/ elimination)"
>               putStrLn "\tcontradiction [name1] [name2]\t(~ elimination)"
>               putStrLn "\tundo\t\t\t\t(undo proof step)"

> completions = ["assume","split","left","right","negate",
>                "apply","elim","contradiction","undo"]

> commandComplete :: [String] -> String -> IO [String]
> commandComplete [] init = return []
> commandComplete (x:xs) init 
>     | (take (length init) x) == init = do rest <- commandComplete xs init
>                                           return (x:rest)
>     | otherwise = commandComplete xs init

> doProof showgoal ctxt 
>     | allSolved ctxt = ivor $ qed ctxt
>     | otherwise =
>         do ctxt <- ivor $ beta defaultGoal ctxt
>            when showgoal $ showGoal defaultGoal ctxt
>            names <- ivor $ getNames defaultGoal ctxt
>            setCompletionEntryFunction $
>                Just $ commandComplete (nub (completions++names))
>            line <- readline "Command> "
>            case line of
>               Nothing -> doProof showgoal ctxt
>               Just "?" -> do commhelp
>                              doProof False ctxt
>               Just inp -> do addHistory inp
>                              ctxt <- case runCmd inp ctxt of
>                                   Left err -> do putStrLn (show err)
>                                                  return ctxt
>                                   Right c -> return c
>                              ctxt <- ivor $ keepSolving defaultGoal ctxt
>                              doProof True ctxt

> runCmd cmd ctxtin = do 
>     let ctxt = save ctxtin
>     case (splitinput "" cmd) of
>            ("assume","") -> intro defaultGoal ctxt
>            ("assumption","") -> intro defaultGoal ctxt
>            ("assume",rest) -> introName (name rest) defaultGoal ctxt
>            ("elim",rest) -> induction rest defaultGoal ctxt
>            ("split",_) -> and_intro defaultGoal ctxt
>            ("left","") -> inl defaultGoal ctxt
>            ("right","") -> inr defaultGoal ctxt
>            ("left",n) -> (inl >+> beta >+> refine n) defaultGoal ctxt 
>            ("right",n) -> (inr >+> beta >+> refine n) defaultGoal ctxt 
>            ("apply",n) -> (refine n) defaultGoal ctxt
>            ("negate",n) -> notassume defaultGoal ctxt
>            ("contradiction",n) -> do (a,b) <- parsePair n
>                                      contradiction a b defaultGoal ctxt
>            ("undo",n) -> restore ctxtin
>            ("trace",_) -> traceTac defaultGoal ctxt
>            ("",_) -> idTac defaultGoal ctxt
>            _ -> fail "Unrecognised command"
>   where splitinput acc (' ':xs) = (acc,xs)
>         splitinput acc [] = (acc,"")
>         splitinput acc (x:xs) = splitinput (acc++[x]) xs
>         parsePair n = let ws = words n in
>                       if (length ws/=2) 
>                          then fail "contradiction needs two arguments"
>                          else return (ws!!0,ws!!1)

> showGoal goal ctxt 
>     | allSolved ctxt = putStrLn "No more goals"
>     | otherwise = do gd <- ivor $ goalData ctxt False goal
>                      let gctxt = bindings gd
>                      let gtype = goalType gd
>                      showBindings gctxt
>                      putStrLn $ "----"
>                      putStrLn $ lshow gtype ++ "\n"
>                      putStrLn $ showgoals ((numUnsolved ctxt)-1) ++ "\n"
>   where showgoals 0 = "No other goals"
>         showgoals 1 = "1 other goal to solve"
>         showgoals n = show n ++ " other goals to solve"

> getNames goal ctxt = do gd <- goalData ctxt False goal
>                         let gctxt = bindings gd
>                         return (map (show.fst) gctxt)

> showBindings [] = return ()
> showBindings ((n,ty):ts) = do showBindings ts
>                               putStrLn $ show n ++ " : " ++ lshow ty

(This probably gets precedences wrong, I didn't really think about it
properly. Patches welcome :))

> lshow t = tologic 10 $ view t
>  where
>    tologic x (Forall v ty sc) 
>        = bracket x 3 $ tologic 3 ty ++ " -> " ++ tologic 4 sc
>    tologic x (App (App (Name TypeCon n) a) b) 
>         | n == (name "And") 
>             = bracket x 1 $ tologic 1 a ++ " /\\ " ++ tologic 2 b
>         | n == (name "Or") 
>             = bracket x 2 $ tologic 2 a ++ " \\/ " ++ tologic 3 b
>    tologic x (Name TypeCon n) 
>         | n == (name "False") = "_|_"
>    tologic x (App (Name _ n) a)
>         | n == (name "not") 
>             = bracket x 1 $ "~" ++ tologic 1 a
>    tologic _ vt = show vt

>    bracket outer inner str | inner>=outer = "("++str++")"
>                            | otherwise = str