{-
  Tableaux theorem prover for first order logic

  Pedro Vasconcelos <pbv@dcc.fc.up.pt>, 2009--2010
-}
module Main where
import Text.Html
import Network.CGI
import FOL
import Tableaux
import Markup
import Examples
import Parser
import Zipper
import Util
import Control.Monad.State
import qualified Data.Map as Map

main :: IO ()
main = runCGI cgi_start

-- CGI entry point 
cgi_start = do opstart <- getInput "refute" -- parse a formula to refute
               case opstart of
                 Just txt -> cgi_refute (parseFormula txt)
                 Nothing -> -- fetch current tableau 
                            do script<-scriptName
                               cmds <- getInputWithDefault "cmd" ""
                               op1 <- getInput "tableau" 
                               op2 <- getInput "status" 
                               let optf = do t <- op1 
                                             s <- op2
                                             return (Form script 
                                                     (read $ unquote t) 
                                                     (read $ unquote s))
                               case optf of
                                 Just tf -> cgi_tableau tf cmds
                                 Nothing ->  do setHeader "Content-type" "text/html"
                                                output (renderHtml (greetings script))

cgi_refute (Left msg)
          = do setHeader "Content-type" "text/plain"
               output (show msg)
cgi_refute (Right f)
          = do script<-scriptName 
               cgi_tableau (Form script tableau initial_status) ""
    where tableau = newTableau (Not f)


cgi_tableau t cmds 
    = do setHeader "Content-type" "text/html"
         output (renderHtml (htmlpage << tableau_header t'))
    where t' =  foldl perform t cmds



perform :: Form -> Char -> Form
perform t 'u' = t { form_tableau = cursorUp (form_tableau t) }
perform t 'd' = t { form_tableau = cursorDown (form_tableau t) }
perform t 'l' = t { form_tableau = cursorLeft (form_tableau t) }
perform t 'r' = t { form_tableau = cursorRight (form_tableau t) }
perform t 'x' = let ft = form_tableau t
                    st = form_status t
                    (ft', st') = runState (expand ft) st
                in t { form_tableau=ft', form_status=st' }

perform t 's' = t { form_tableau=resolve (form_tableau t) }
perform t _   = t


getInputWithDefault :: MonadCGI m => String -> String -> m String
getInputWithDefault var def = do opt<-getInput var
                                 return (maybe def id opt)


tableau_header t
    = [h2 << "Instructions",
       form![action (form_script t), method "POST"] << ordList 
       [ primHtml "Use <EM>Expand</EM> to split a formula into sub components.",
         primHtml "Move the current focus node by clicking on sub-formulas.",
         primHtml "Use <EM>Resolve</EM> on an <EM>atomic</EM> formula to unify with another of inverted sign in the same branch (thus <EM>closing</EM> the branch).",
         toHtml "The proof is complete when all branches are closed, i.e. end in False.",
         ("To return to the start page, click " +++ submit "bt" "Restart")
       ],
       hr,
       p << math << t,
       hr,
       signature
      ]
             


-- startup page
-- allows typing in a formula or selecting an example
greetings script 
    = htmlpage << 
      [ h1 << "Welcome to the interactive tableaux prover",
        p << [ toHtml "This web page allows constructing proofs of ",
               toHtml "propositional and first-order logic sentences using ",
               toHtml "the method of semantic tableaux. To learn more about tableaux, check the ",
               anchor![href "http://en.wikipedia.org/wiki/Method_of_analytic_tableaux"] << "Wikipedia article."
             ],
      form![action script, method "POST"] << 
        [ p << "Please type in a formula to prove or choose an example from the list below.",
          p << [inputField "refute"![size "60"],  submit "bt" "Start"]
        , p << table << map make_example (zip [1..] examples)
        , hr
        , p << [ toHtml "This theorem prover is written in "
               , anchor![href "http://www.haskell.org"] << "Haskell;"
               , toHtml " the source code package is available in the "
               , anchor![href "http://hackage.haskell.org"] << "HackageDB site."
               ]
        , signature
        ]
      ]
    where
      -- n-th example            
      make_example (n,(txt,f))
          = tr << [td << input ![name "sel", thetype "radio", 
                                 value (show n), onclick cmd],
                   td << math << f,
                   td![align "right"] << primHtml txt,
                   hiddenField id (showFormula f)
                  ]
            
          where cmd = "copy('" ++ id ++ "')"
                id = "ex" ++ show n


signature =
    address << [toHtml "Pedro Vasconcelos <pbv@ncc.up.pt>",
                br,
                toHtml "LIACC, University of Porto, PORTUGAL"]