module Main where import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq (getForWebInterface) import Language.Haskell.FreeTheorems.Variations.PolySeq.Highlight(highlight) import Network.CGI import Data.ByteString.Lazy.UTF8 (fromString) import Text.XHtml import Control.Monad import Data.Maybe import Text.PrettyPrint.HughesPJ (render) import qualified Data.Map as M import Data.Generics import TimeOut askDiv v e = maindiv << ( p << ("To get a quick impression about the influence of strictness, toggle the let expressions between strict " +++ tt << "let!" +++ " and non-strict " +++ tt << "let" +++ ".") +++ p << ( "You can also enter your own term, " +++ "e.g. " +++ primHtmlChar "ldquo" +++ tt << "/\\a.\\x::a.\\f::forall b.b->Int.seq f_{Int} (f_{a} x)" +++ primHtmlChar "rdquo" +++ " or " +++ primHtmlChar "ldquo" +++ tt << "\\x::a.[]_{Int}" +++ primHtmlChar "rdquo" +++ "." +++ p << ("Note that recursive let expressions are not allowed.") +++ p << (textarea ! [name "term", cols "80", rows "11"] << v +++ submit "submit" "Generate" )) +++ e ) askTypeForm = askDiv ("\\c :: a -> b -> a.\n" ++ " let c' = c in\n" ++ " fix (\\h :: a -> [b] -> a.\n" ++ " \\n :: a. \\ys :: [b].\n" ++ " let! z = c' n in\n" ++ " case ys of {\n" ++ " [] -> n;\n" ++ " x:xs -> let! xs' = xs in\n" ++ " let! x' = x in\n" ++ " let n' = c' n x' in\n" ++ " h n' xs'})") noHtml -- ("/\\a.\\p::a->Bool.\n" ++ -- " let p' = p in \n" ++ -- " (fix \n" ++ -- " (\\f::[a]->[a]. \\ys::[a].\n" ++ -- " case ys of {[] -> []_{a};\n" ++ -- " x:xs-> let! x' = x in \n" ++ -- " if p x then\n" ++ -- " (let! xs' = xs in x):(f xs)\n" ++ -- " else f xs\n" ++ -- " }))") noHtml --generateResult :: (MonadIO t) => [Char] -> t Html generateResult termStr = do run_algorithm <- run_algorithmM return(askDiv termStr noHtml +++ maindiv << (case run_algorithm of Left (err,msg) -> p << case err of "TimeOut" -> msg +++ "" "ParseError" -> "A parse error occured:" +++ pre << msg "NotTypable" -> "The term" +++ pre << tt << msg +++ "is not typable." Right result -> let (term,constraint,typ,normalFT,minTypeFTList) = result l = length minTypeFTList in p << "The term" +++ pre << tt << term +++ -- p << "can be typed to " +++ tt << typ +++ -- p << "if the constraint " +++ -- pre << tt << constraint +++ "is satisfied, which leads to the optimal type(s)" +++ p << (if l > 1 then "can be typed to the minimal types" +++ (if l == 2 then printTypeAndFT (head minTypeFTList) +++ "and" else (foldr (\x y -> y +++ (printTypeAndFT x) +++ ",") (""+++"") (init $ minTypeFTList)) +++ " and") +++ printTypeAndFT (last minTypeFTList) else "can be typed to the minimal type" +++ printTypeAndFT (head minTypeFTList)) +++ p << "The normal free theorem for the type without annotations would be:" +++ pre << tt << (highlight $ neq2eq normalFT))) where run_algorithmM = do res <- liftIO (watchdog2 3000 (getForWebInterface termStr)) return (case res of Nothing -> Left ("TimeOut","Unfortunately the generator the type generator timed out. Time was restricted to 3 seconds.") Just x -> x) printTypeAndFT (tau,ft) = p << pre << tt << tau +++ p << "with the free theorem" +++ pre << tt << (highlight $ neq2eq ft) neq2eq ('/':'=':s) = neq2eq ('=':s) neq2eq (x:xs) = x : neq2eq xs neq2eq [] = [] main = runCGI (handleErrors cgiMain) --cgiMain :: CGI CGIResult cgiMain = do setHeader "Content-type" "text/html; charset=UTF-8" mTypeStr <- getInput "term" let content = case mTypeStr of Nothing -> return askTypeForm Just typeStr -> generateResult typeStr con <- content outputFPS $ fromString $ showHtml $ header ( thetitle << "Taming Selective Strictness" +++ style ! [ thetype "text/css" ] << cdata cssStyle ) +++ body ( form ! [method "POST", action "#"] << ( thediv ! [theclass "top"] << ( thespan ! [theclass "title"] << "Haskell" +++ thespan ! [theclass "subtitle"] << "Taming Selective Strictness" ) +++ maindiv ( p << ("This tool allows you to experiment with the method described in the article " +++ primHtmlChar "ldquo" +++ hotlink "http://www.iai.uni-bonn.de/~jv/acta.pdf" << "Refined Typing to Localize the Impact of Forced Strictness on Free Theorems" +++ primHtmlChar "rdquo" +++ " (Acta Informatica, to appear) by Daniel Seidel and " +++ hotlink "http://www.iai.uni-bonn.de/~jv" << (toHtml "Janis Voigtländer") +++ ".") +++ p << ("You may also want to try the following related tools:" +++ ulist << [ li << (--primHtmlChar "ldquo" +++ hotlink "http://www-ps.iai.uni-bonn.de/ft" << "Automatic Generation of Free Theorems" -- +++ primHtmlChar "rdquo" ) , li << (--primHtmlChar "ldquo" +++ hotlink "http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi" << "Automatically Generating Counterexamples to Naive Free Theorems" -- +++ primHtmlChar "rdquo" ) ])) +++ con +++ maindiv ( p << ("You can download the source code of " +++ hotlink "http://hackage.haskell.org/package/free-theorems-seq" << "the underlying library" +++ " and of " +++ hotlink "http://hackage.haskell.org/package/free-theorems-seq-webui" << "the webinterface" +++ " itself.") +++ p << ("© 2009-2011 Daniel Seidel <" +++ hotlink "mailto:ds@iai.uni-bonn.de" << "ds@iai.uni-bonn.de" +++ ">") ) )) maindiv = thediv ! [theclass "main"] cdata s = primHtml $ -- ("") cssStyle = unlines [ "body { padding:0px; margin: 0px; }" , "div.top { margin:0px; padding:10px; margin-bottom:20px;" , " background-color:#efefef;" , " border-bottom:1px solid black; }" , "span.title { font-size:xx-large; font-weight:bold; }" , "span.subtitle { padding-left:30px; font-size:large; }" , "div.main { border:1px dotted black;" , " padding:10px; margin:10px; }" , "div.submain { padding:10px; margin:11px; }" , "p.subtitle { font-size:large; font-weight:bold; }" , "input.type { font-family:monospace; }" , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }" , "span.mono { font-family:monospace; }" , "pre { margin:10px; margin-left:20px; padding:10px;" , " border:1px solid black; }" , "textarea { margin:10px; margin-left:20px; padding:10px; }" , "p { text-align:justify; }" ]