{-
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 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 "∀" +++ htmlSym x +++ spaceHtml +++ htmlFormula 10 f
htmlFormula p (Exist x f)
= htmlParen (p>10) $
primHtml "∃" +++ htmlSym x +++ spaceHtml +++ htmlFormula 10 f
htmlFormula p (Not f)
= htmlParen (p>10) $ primHtml "¬" +++ htmlFormula 10 f
htmlFormula p (And f1 f2)
= htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "∧" +++ htmlFormula 5 f2
htmlFormula p (Or f1 f2)
= htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "∨" +++ htmlFormula 5 f2
htmlFormula p (Implies f1 f2)
= htmlParen (p>=5) $ htmlFormula 5 f1 +++ primHtml "⇒" +++ 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;"
, "}"
]