module Pages (input_page, help_page) where
import Text.XHtml
import Data.Maybe (fromMaybe, isJust)
import Paths (relativeURLOf)
-- The hackage URL of a package
hackage :: String -> URL
hackage pkgName = "http://hackage.haskell.org/cgi-bin/hackage-scripts/package/" ++ pkgName
-- Link text to url
at :: (HTML a) => a -> URL -> HotLink
text `at` url = hotlink url << text
page_template title_text content =
thehtml <<
[ header <<
[ thetitle << title_text
, thelink ! [rel "stylesheet", thetype "text/css", href (relativeURLOf "style.css")] << ""
, script ! [src "http://code.jquery.com/jquery-1.4.2.min.js", thetype "text/javascript"] << ""
, script ! [src (relativeURLOf "ui-tweaks.js"), thetype "text/javascript"] << ""
]
, body <<
[ thediv ! [identifier "header"] <<
[ h1 << "Haskell"
, h2 << title_text
]
, thediv ! [identifier "content"] << content
]
]
input_page :: [(String, String)] -> Html -> Html
input_page inputs additionalContent =
let title_text = "Automatic generation of free theorems"
in page_template title_text <<
[ p ! [identifier "help"] << "Help" `at` "?help"
, thediv <<
[ p << ("This tool allows to generate free theorems for sublanguages of Haskell. See the " +++ "help page" `at` "?help" +++ " for details.")
, p << ("The source is available at hackage as " +++ ("free-theorems-webui" `at` hackage "free-theorems-webui") +++ ". See also: " +++ ("free-theorems (library)" `at` hackage "free-theorems") +++ " and " +++ ("ftshell (shell interface)" `at` hackage "ftshell") +++ ".")
, p << ("You may also want to try the following related tools:" +++ ulist << [ li << "Automatically Generating Counterexamples to Naive Free Theorems" `at` "http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi"
, li << "Taming Selective Strictness" `at` "http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi"
])
]
, thediv <<
form ! [method "POST", theclass "float-container"] <<
[ thediv <<
[ p << "Please enter a (polymorphic) type, e.g. \"(a -> Bool) -> [a] -> [a]\" or simply \"filter\":"
, p << textfield' "type" ! [theclass "type", size "50", maxlength 1024]
, p << "Please choose a sublanguage of Haskell:"
, p << (check radioOption' { o_name = "model", o_value = "basic", o_label = "no bottoms (hence no general recursion and no selective strictness)" })
, p << ( radioOption' { o_name = "model", o_value = "fix" , o_label = "general recursion but no selective strictness" })
, p << ( radioOption' { o_name = "model", o_value = "seq" , o_label = "general recursion and selective strictness" })
, p << "Please choose a theorem style (without effect in the sublanguage with no bottoms):"
, p << (check radioOption' { o_name = "style", o_value = "eq" , o_label = "equational" })
, p << ( radioOption' { o_name = "style", o_value = "ineq" , o_label = "inequational" })
]
, thediv <<
[ p << "If you need additional declarations you can enter them here:"
, p << textarea' "xtraSrc"
]
, thediv ! [theclass "clear"] <<
[ submit "" "Generate"
, thespan <<
yesNoOption' { o_name = "hideTypeInstantiations", o_value = "yes", o_label = "hide type instantiations", o_title = "Hide type instantiations in theorems for better readability." }
, thespan <<
[ check radioOption' { o_name = "format", o_value = "html+png" , o_label = "PNG" , o_title = "Show result with graphical formulae" }
, radioOption' { o_name = "format", o_value = "html+text", o_label = "Plain", o_title = "Show result with plain text formulae" }
, radioOption' { o_name = "format", o_value = "tex" , o_label = "TeX" , o_title = "Export as TeX" }
, radioOption' { o_name = "format", o_value = "pdf" , o_label = "PDF" , o_title = "Export as PDF" }
] +++ " " +++ ("?" `at` "?help#format" ! [title "Help on output formats"])
]
]
, additionalContent
]
where
-- Define versions of all used input elements which
-- implicitly use the values from the "inputs" parameter.
-- This causes input elements to keep their values after form submission,
-- provided the result from getInputs is passed to this function.
radioOption' = radioOption { o_inputs = inputs }
yesNoOption' = yesNoOption { o_inputs = inputs }
textfield' name_ = (! [value $ fromMaybe "" $ lookup name_ inputs]) textfield name_
textarea' name_ = textarea ! [name name_] << (fromMaybe "" $ lookup name_ inputs)
data Option = Option { o_type :: String, o_name :: String, o_value :: String, o_label :: String, o_title :: String, o_checked :: Bool, o_inputs :: [(String, String)] }
check :: Option -> Option
check opt = opt { o_checked = True }
instance HTML Option where
toHtml (Option tp n v l t c inputs) =
toHtml (input ! attributes +++ label ! [thefor input_id] << l)
where attributes = [thetype tp, name n, value v, title t, identifier input_id] ++ if maybe c (v==) (lookup n inputs) then [checked] else []
input_id = n ++ "_" ++ v
yesNoOption = Option "checkbox" "" "" "" "" False []
radioOption = Option "radio" "" "" "" "" False []
help_page :: Html -> Html
help_page additionalContent =
let title_text = "Help on: Automatic generation of free theorems"
in page_template title_text <<
[ thediv << ("This is the help page for the " +++ "Free Theorem Generator" `at` "?" +++ ".")
, thediv <<
[ h3 << "Free Theorems"
, p << ("Free Theorems were first described in the paper " +++ "\"Theorems for free!\"" `at` "http://doi.acm.org/10.1145/99370.99404" +++ " by Philip Wadler. " +++
"Their special property is that they can be derived solely from the type of a function. The key idea is to interpret types as relations. " +++
"To reflect the structure of types, a relational action, which maps relations to a relation, is defined for every type constructor. " +++
"Using relational actions, a relation can be constructed for every type, and, by applying the definitions of these relational actions, free theorems are obtained.")
, p << ("General recursion and selective strictness weaken free theorems. " +++
"To show the influences caused by adding these constructs, several sublanguages of Haskell are supported in this tool. " +++
"The theoretical foundations are described in the paper " +++ "\"Free theorems in the presence of seq\"" `at` "http://doi.acm.org/10.1145/982962.964010" +++ " by Patricia Johann and Janis Voigtländer. " +++
"As motivated there, it is possible to derive both equational and inequational free theorems.")
]
, thediv <<
[ h3 << "Types"
, p << [ thespan << "Types can be entered in two ways, either with a name or without one. Examples would be "
, pre << "g :: forall b . (Int -> b -> b) -> b -> b"
, thespan << " or "
, pre << "[a] -> [a]"
]
, p << "It is also possible to simply enter the name of a predefined Haskell function (see the list given below). The tool knows about standard Haskell data types, type synonyms, and type classes (again, see the lists below)."
, p << "Additionally, T0 to T9 may be used as placeholders for arbitrary but fixed types."
]
, anchor ! [ identifier "format" ] << ""
, thediv <<
[ h3 << "Output formats"
, p << "The following output formats can be selected:"
, defList
[ ("PNG", "Result is displayed on webpage, formulae are rendered as PNG images — " +++ emphasize << "This is the default.")
, ("Plain", stringToHtml "Result is displayed on webpage, formulae are rendered as plain text.")
, ("TeX", "A TeX file is generated. You need " +++ "lambdaTeX.tex" `at` relativeURLOf "lambdaTeX.tex" +++ " (adapted from Patryk Zadarnowski) and pdflatex to get the same result as by selecting the 'PDF' option.")
, ("PDF", stringToHtml "A PDF file is generated.")
]
]
, additionalContent
]