diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,31 @@ +The module free-theorems-seq-webui-0.1 provides the binary free-theorems-seq-webui.cgi. + +Installation can either be done with cabal (configure/build/install) or +runhaskell Setup.hs configure --user +runhaskell Setup.hs build +runhaskell Setup.hs install + +It is recommended to produce only a local build +and start the webinterface (using the local build) with + +$ ./test.sh + +then it runs under http://localhost:8002/ + +An online version of the webinterface is also found under + +http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi + +Enjoy. + + + +Acknowledgements. +================= + +Most of the webinterface' code (./src/polyseq-cgi.hs) and the script testcgi.py +are written by + +Joachim Breitner . + +Thanks! diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,5 @@ +#!/usr/bin/runhaskell + +import Distribution.Simple + +main = defaultMain diff --git a/free-theorems-seq-webui.cabal b/free-theorems-seq-webui.cabal new file mode 100644 --- /dev/null +++ b/free-theorems-seq-webui.cabal @@ -0,0 +1,42 @@ +name: free-theorems-seq-webui +version: 1.0 +license: PublicDomain +author: Daniel Seidel +maintainer: ds@iai.uni-bonn.de +synopsis: Taming Selective Strictness +description: + This package provides access to the functionality of + through a web interface. + . + An online version of the interface is running at . +category: Language +tested-with: GHC==7.0.1 +build-type: Simple +cabal-version: >= 1.6 + +extra-source-files: + testcgi.py + test.sh + src/TimeOut.hs + README + +executable free-theorems-seq-webui.cgi + main-is: + free-theorems-seq-webui.hs + build-depends: + cgi >= 3001.1.5.1 + , containers >= 0.1.0.1 + , free-theorems-seq == 0.1.* + , mtl >= 1.1.0.0 + , network >= 2.1.0.0 + , pretty == 1.* + , utf8-string >= 0.3.1.1 + , xhtml >= 3000.0.2.1 + if impl(ghc >= 6.10) + build-depends: + base >= 4 + , syb >= 0.1.0.0 + else + build-depends: + base >= 1 && < 4 + hs-source-dirs: src diff --git a/src/TimeOut.hs b/src/TimeOut.hs new file mode 100644 --- /dev/null +++ b/src/TimeOut.hs @@ -0,0 +1,35 @@ +module TimeOut where + +import Control.Concurrent +--import Distribution.Simple.Utils +watchdogIO :: (Show a) => + Int -- milliseconds + -> IO a -- expensive computation + -> IO a -- cheap computation + -> IO a +watchdogIO millis expensive cheap = + do mvar <- newEmptyMVar + tid1 <- forkIO $ do x <- expensive + (if (length (show x) >= 0) then x else x) `seq` putMVar mvar (Just x) + tid2 <- forkIO $ do threadDelay (millis * 1000) + putMVar mvar Nothing + res <- takeMVar mvar + case res of + Just x -> + do --info ("EXPENSIVE was used") + killThread tid2 --`catch` (\e -> warn (show e)) + return x + Nothing -> + do --info ("WATCHDOG after " ++ show millis ++ " milliseconds") + killThread tid1 --`catch` (\e -> warn (show e)) + cheap + +watchdog1 :: (Show a) => Int -> a -> IO (Maybe a) +watchdog1 millis x = + watchdogIO millis (return (Just x)) + (return Nothing) + +watchdog2 :: (Show a) => Int -> a -> IO (Maybe a) +watchdog2 millis x = + watchdogIO millis (x `seq` return (Just x)) + (return Nothing) diff --git a/src/free-theorems-seq-webui.hs b/src/free-theorems-seq-webui.hs new file mode 100644 --- /dev/null +++ b/src/free-theorems-seq-webui.hs @@ -0,0 +1,167 @@ +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 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 ft) + +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 paper " + +++ primHtmlChar "ldquo" + +++ hotlink "http://www.iai.uni-bonn.de/~jv/atps09.pdf" + << "Taming Selective Strictness" + +++ primHtmlChar "rdquo" + +++ " (ATPS'09) 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; }" + ] diff --git a/test.sh b/test.sh new file mode 100644 --- /dev/null +++ b/test.sh @@ -0,0 +1,2 @@ +#!/bin/bash +./testcgi.py ./dist/build/free-theorems-seq-webui.cgi/free-theorems-seq-webui.cgi diff --git a/testcgi.py b/testcgi.py new file mode 100644 --- /dev/null +++ b/testcgi.py @@ -0,0 +1,18 @@ +#!/usr/bin/python + +from BaseHTTPServer import HTTPServer +from CGIHTTPServer import CGIHTTPRequestHandler +import sys + +class MyRequestHandler(CGIHTTPRequestHandler): + def is_cgi(self): + self.cgi_info = ("","") + return True + + def translate_path(self, path): + return sys.argv[1] + + +server_address = ('', 8002) +http = HTTPServer(server_address, MyRequestHandler) +http.serve_forever()