module Main where
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType')
import Language.Haskell.FreeTheorems.Variations.CounterExamples.ExFind (getForWebInterface)
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Common.AlgCommon(showTerm, showTrackContApplicationWithNames, showTrackContApplicationSolved, Term(Var), TermVar(..), assignTypeRelFuncs, prependRelFunc, renumberVariables, showFuncNames, showVarList, getTypeRelFuncNamesNonStrict, mapDisRelFuncsToNames)
import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
import Language.Haskell.FreeTheorems
( runChecks
, check
, filterSignatures
, prettyTheorem
, asTheorem
, interpret
, unfoldLifts
, prettyUnfoldedLift
, LanguageSubset(SubsetWithFix)
, TheoremType(EquationalTheorem)
, PrettyTheoremOption(OmitTypeInstantiations,OmitLanguageSubsets)
, specialise
, relationVariables
)
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 Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.TimeOut
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.FTSync
askDiv v e = maindiv << (
p << ( "Please enter a type. " +++
"You can prepend it with a list of type variables " +++
"that should not be considered for counterexample generation, e.g. " +++ primHtmlChar "ldquo" +++ tt << "a b. ((a,c) -> b) -> b" +++ primHtmlChar "rdquo" +++ "." +++
p << ( input ! [name "type", value v] +++ " " +++
submit "submit" "Generate" )) +++
e
)
askTypeForm = askDiv "[a] -> [a]" noHtml
typeError typeStr err = askDiv typeStr (
p << ("There was a problem parsing your type: " +++
pre << err )
)
generateResult typeStr typ =
do counter_example <- counter_exampleM
return (askDiv typeStr noHtml +++
maindiv << (
h3 << "The Free Theorem" +++
(case ft_full of
Left err -> p << "The full Free Theorem deriver failed:" +++
pre << err
Right s -> p << "The theorem generated for functions of the type" +++
pre << (termName ++ " :: " ++ dropedPreFix) +++
"is:" +++
pre << s
)) +++
maindiv << (
h3 << "The Counterexample" +++
( case counter_example of
Left err -> p << if err == "_timeOut"
then "Unfortunately the generator for the counterexample timed out. Time was restricted to 3 seconds." +++ ""
else (let nonstrict = getTypeRelFuncNamesNonStrict typ funcNames in
case nonstrict of
[] -> "No type variables were made available for consideration for counterexample generation." +++ ""
[x] -> "Even without strictness condition on " +++ tt << x +++ " the algorithm found no counterexample."
xs -> "Even without strictness conditions on " +++ tt <<showVarList xs +++ " the algorithm found no counterexample.")
Right result ->
let (term,trackCont,funcs) = result
names = mapDisRelFuncsToNames funcs drelNames varNames
nonstricts = getTypeRelFuncNamesNonStrict typ funcNames in
p << ((if length nonstricts == 1
then ("By disregarding the strictness condition on " +++ tt << showVarList nonstricts +++ " the theorem becomes wrong.")
else ("By disregarding the strictness conditions on " +++ tt << showVarList nonstricts +++ " the theorem becomes wrong.")) +++
" The term" +++
pre << tt << (termName ++ " = " ++ (showTerm.head.renumberVariables $ [term])) +++
"is a counterexample.") +++
p << ("By setting " +++ tt << "t1 = t2 = ... = ()" +++ " and" +++
pre << assignTypeRelFuncs typ funcNames) +++
p << ("the following would be a consequence of the thus " +++ primHtmlChar "ldquo" +++ "naivified" +++ primHtmlChar "rdquo" +++ " free theorem:" +++
pre << prependRelFunc funcNames (fst trackCont) ((showTrackContApplicationWithNames trackCont names (Var (TermVar 0))) ++ "\n\nwhere\n\n" ++ showFuncNames (zip (snd.unzip$names) (snd.unzip$funcs)))) +++
p << ("But this is wrong since with the above " +++ tt << termName +++ " it reduces to:" +++
pre << prependRelFunc funcNames (fst trackCont) (showTrackContApplicationSolved trackCont funcs term))
)))
where ft_full = let properType = termName ++ " :: " ++ case span (/='.') typeStr of
(t,"") -> t
(_,_:t) -> t
either = "data Either a b = Left a | Right b"
bool = "data Bool = False | True"
maybe = "data Maybe a = Nothing | Just a"
parse_input = unlines [either, bool, maybe, properType]
(ds,es) = runChecks (parse parse_input >>= check)
[s] = filterSignatures ds
in if null es
then case interpret ds (SubsetWithFix EquationalTheorem) s of
Nothing -> Left "interpret returned nothing"
Just i -> let i' = foldl specialise i (relationVariables i) in
Right $ render (prettyTheorem [OmitTypeInstantiations,OmitLanguageSubsets] (asTheorem i')) ++
case unfoldLifts ds i' of
[] -> ""
ls -> (if length ls == 1
then "\n\nThe structural lifting occuring therein is defined as follows:\n\n "
else "\n\nThe structural liftings occuring therein are defined as follows:\n\n") ++
unlines (map (render . prettyUnfoldedLift []) ls)
else Left (unlines (map render es))
counter_exampleM = do res <- liftIO (watchdog2 3000 (getForWebInterface typ))
return (case res of
Nothing -> Left "_timeOut"
Just x -> x)
dropedPreFix = let (prefix,typ) = break (=='.') typeStr in
if typ == [] then prefix else tail typ
main = runCGI (handleErrors cgiMain)
cgiMain = do
setHeader "Content-type" "text/html; charset=UTF-8"
mTypeStr <- getInput "type"
let content = case mTypeStr of
Nothing -> return askTypeForm
Just typeStr -> case parseType' typeStr of
Left err -> return (typeError typeStr err)
Right typ -> generateResult typeStr typ
con <- content
outputFPS $ fromString $ showHtml $
header (
thetitle << "Automatically Generating Counterexamples to Naive Free Theorems" +++
style ! [ thetype "text/css" ] << cdata cssStyle
) +++
body ( form ! [method "POST", action "#"] << (
thediv ! [theclass "top"] << (
thespan ! [theclass "title"] << "Haskell" +++
thespan ! [theclass "subtitle"] << "Automatically Generating Counterexamples to Naive Free Theorems"
) +++
maindiv ( p << ("This tool allows you to run the algorithm described in the paper "
+++ primHtmlChar "ldquo"
+++ hotlink "http://www.iai.uni-bonn.de/~jv/paper.pdf"
<< "Automatically Generating Counterexamples to Naive Free Theorems"
+++ primHtmlChar "rdquo"
+++ " (FLOPS'10) 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/polyseq.cgi" << "Taming Selective Strictness" +++ primHtmlChar "rdquo")
])) +++
con +++
maindiv ( p << ("The source code is available for " +++
hotlink "http://hackage.haskell.org/package/free-theorems-counterexamples" << "download" +++
".") +++
p << ("© 2010 Daniel Seidel <" +++ hotlink "mailto:ds@iai.uni-bonn.de" << "ds@iai.uni-bonn.de" +++ "> and Joachim Breitner <" +++
hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.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; }"
]