{- 
   HTML pretty-printing for formulas and tableaux 

   Pedro Vasconcelos, 2010.
-}
module Markup where

import FOL
import Tableaux
import Text.Html
import Data.Tree
import Zipper
import Parser
import Util
import CSS
import Data.List(intersperse,span)


data Form = Form {
      form_script  :: String
    , form_tableau :: Tableau
    , form_status :: Status
    } deriving (Eq, Show, Read)


instance HTML Form where
    toHtml t = form![strAttr "id" "tableau",
                     action (form_script t ++ "#focus"), method "POST"] << 
                      [math << (fmap decorate
                                (addPaths 
                                 (form_tableau t))),
                       hiddenField "tableau" (quote (show (form_tableau t))),
                       hiddenField "status" (quote (show (form_status t))),
                       hiddenField "cmd" ""
                      ]


-- decorate a single tree node
decorate :: (AttrFormula,String) -> Html
decorate (f,p) = markup_path p $ toHtml f

markup_path :: String -> Html -> Html
markup_path [] html
    = thespan <<
      [ thespan![theclass "cursor"] << html
      , spaceHtml
      , button "b1" "Expand" ![onclick "move('x')"]
      , button "b2" "Resolve"![onclick "move('s')"]
      , anchor![name "focus"] << noHtml
      ]
markup_path p html = thespan![onclick ("move('"++p++"')")] << html



instance HTML AttrFormula where
    toHtml (AttrFormula f open uses)
        | not open = thespan![theclass "closed"] << toHtml f
        | uses>0   = toHtml f
        | otherwise= thespan![theclass "unused"] << toHtml f


instance HTML Formula where
    toHtml f = htmlFormula 0 f 

-- pretty-print a formula in Html
htmlFormula :: Int -> Formula -> Html
htmlFormula _  TT = toHtml "True"
htmlFormula _  FF = toHtml "False"
htmlFormula _ (Rel r ts) = htmlTerm (Fun r ts)
htmlFormula p (Forall x f)
    = htmlParen (p>10) $ 
      primHtml "&forall;" +++ htmlSym x +++ spaceHtml +++ htmlFormula 10 f
htmlFormula p (Exist x f)
    = htmlParen (p>10) $ 
      primHtml "&exist;" +++ htmlSym x +++ spaceHtml +++ htmlFormula 10 f
htmlFormula p (Not f)
    = htmlParen (p>10) $ primHtml "&not;" +++ htmlFormula 10 f
htmlFormula p (And f1 f2) 
    = htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "&and;" +++ htmlFormula 5 f2
htmlFormula p (Or f1 f2) 
    = htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "&or;" +++ htmlFormula 5 f2
htmlFormula p (Implies f1 f2)
    = htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "&rArr;" +++ htmlFormula 5 f2


htmlParen :: Bool -> Html -> Html
htmlParen True h  = toHtml "(" +++ h +++ toHtml ")"
htmlParen False h = h


htmlTerm :: Term -> Html
htmlTerm (Var x) = htmlSym x
htmlTerm (Fun f ts) 
    | null ts  = htmlSym f
    | otherwise = htmlSym f +++ toHtml "(" +++
                  concatHtml (intersperse (toHtml ",") (map htmlTerm ts))
                  +++ toHtml ")"

htmlSym :: String -> Html
htmlSym ""       = noHtml
htmlSym ('_':xs) = sub (htmlSym xs)
htmlSym xs = let (xs',xs'') = span (/='_') xs
             in toHtml xs' +++ htmlSym xs''



instance HTML a => HTML (Tree a) where
    toHtml (Node x []) = toHtml x
    toHtml t = mkconj (conj t) +++ mkdisj (disj t)
        where conj (Node x [t]) = x : conj t 
              conj (Node x ts)  = [x]
              disj (Node x [t]) = disj t
              disj (Node x ts)  = ts


mkconj :: HTML a => [a] -> Html
mkconj [] = noHtml
mkconj xs 
    = thediv![theclass "conj"] << (hs ++ [h])
      where hs = map (p.toHtml) (init xs)
            h = p![theclass "last"] << last xs


mkdisj :: HTML a => [Tree a] -> Html
mkdisj [] = noHtml
mkdisj ts = ulist![theclass "tree"] << (hs ++ [h])
      where hs = map (li.toHtml) (init ts)
            h = li![theclass "last"] << last ts


instance HTML a => HTML (TreeLoc a) where
    toHtml loc = concatHtml $ toForest $ fmap toHtml loc


-- miscelaneous Html tags
htmlpage b = [header << [css << cssText, script << jsText],
              body << b]


script code = Html [HtmlTag "SCRIPT" [strAttr "type" "text/javascript"] code]

css txt = style![thetype "text/css"] << txt

-- stylesheet url = thelink noHtml![rel "stylesheet", thetype "text/css", href url]

math = thediv![theclass "math"] 

-- conj = thediv![theclass "conj"]


button :: String -> String -> Html
button name value 
    = input![strAttr "type" "button",
             strAttr "name" name, 
             strAttr "id" name,
             strAttr "value" value] 


onclick :: String -> HtmlAttr
onclick = strAttr "onclick"

onload :: String -> HtmlAttr
onload = strAttr "onload"

inputField :: String -> Html
inputField name
    = input![strAttr "name" name, strAttr "id" name]


hiddenField :: String -> String -> Html
hiddenField name value
    = input![strAttr "type" "hidden", strAttr "name" name,  
             strAttr "id" name, strAttr "value" value]


-- auxiliary event-handling javascript code
jsText :: String
jsText 
    = unlines [""
              ,"function move(action)"
              , "{"
              ,"document.getElementById('cmd').value = action;"
              ,"document.getElementById('tableau').submit();"
              ,"}" 
              ,"function copy(ex)"
              , "{"
              , "document.getElementById('refute').value = document.getElementById(ex).value;"
              , "}"
              ]