free-theorems-seq-webui (empty) → 1.0
raw patch · 7 files changed
+300/−0 lines, 7 filesdep +basedep +cgidep +containerssetup-changed
Dependencies added: base, cgi, containers, free-theorems-seq, mtl, network, pretty, syb, utf8-string, xhtml
Files
- README +31/−0
- Setup.hs +5/−0
- free-theorems-seq-webui.cabal +42/−0
- src/TimeOut.hs +35/−0
- src/free-theorems-seq-webui.hs +167/−0
- test.sh +2/−0
- testcgi.py +18/−0
+ README view
@@ -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 <mail@joachim-breitner.de>.++Thanks!
+ Setup.hs view
@@ -0,0 +1,5 @@+#!/usr/bin/runhaskell++import Distribution.Simple++main = defaultMain
+ free-theorems-seq-webui.cabal view
@@ -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 + <http://hackage.haskell.org/package/free-theorems-seq> through a web interface.+ .+ An online version of the interface is running at <http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi>.+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
+ src/TimeOut.hs view
@@ -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)
+ src/free-theorems-seq-webui.hs view
@@ -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 $+ -- ("<![CDATA[\n"++ + s+ -- ++ "\n]]>")++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; }"+ ]
+ test.sh view
@@ -0,0 +1,2 @@+#!/bin/bash+./testcgi.py ./dist/build/free-theorems-seq-webui.cgi/free-theorems-seq-webui.cgi
+ testcgi.py view
@@ -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()