polyfix-cgi.hs

   1 module Main where
   2
   3 import ParseType (parseType')
   4 import SimpleFT  (freeTheorem)
   5 import Expr (specialize)
   6 import ExFindExtended (getComplete')
   7 import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
   8 import Language.Haskell.FreeTheorems
   9         ( runChecks
  10         , check
  11         , filterSignatures
  12         , prettyTheorem
  13         , asTheorem
  14         , interpret
  15         , unfoldLifts
  16         , prettyUnfoldedLift
  17         , LanguageSubset(BasicSubset)
  18         )
  19
  20 import Network.CGI
  21 import Data.ByteString.Lazy.UTF8 (fromString)
  22 import Text.XHtml
  23 import Control.Monad
  24 import Data.Maybe
  25 import Text.PrettyPrint.HughesPJ (render)
  26
  27 askDiv v e =  maindiv << (
  28         p << ( "Please enter a function type, prepended with a list of type variables, " +++
  29                "whose relations should be allowed to be nonstrict, and a single dot.") +++            p << ( input ! [name "type", value v] +++ " " +++
  30                submit "submit" "Generate Free Theorem and counter example" ) +++
  31         e
  32         )
  33
  34
  35 askTypeForm = askDiv "a. (a -> b) -> b" noHtml
  36
  37 typeError typeStr err = askDiv typeStr (
  38         p << ("There was a problem parsing your type: " +++
  39               pre << err )
  40         )
  41
  42 generateResult typeStr typ = askDiv typeStr noHtml +++
  43         maindiv << (
  44         h3 << "The Free Theorem" +++
  45         (case ft_full of
  46                 Left err -> p << "The full Free Theorem deriver failed:" +++
  47                             pre << err
  48                 Right s  -> p << "For your type, the following Free Theorem holds:" +++
  49                             pre << s
  50         ) +++
  51         p << "Specializing relations to functions, canceling irrelvant terms and eta-reduction, this theorem can be written as:" +++
  52         pre << show ft_simple +++
  53         p << "Further specializing all types to (), all strict functions to id and all non-strict functions to const (), this theorem can be written as:" +++
  54         pre << show (specialize ft_simple)
  55         ) +++
  56         maindiv << (
  57         h3 << "The counter-example" +++
  58         case counter_example of
  59                 Left err -> p << "No term could be derived: " +++ pre << err
  60                 Right (res,used) ->
  61                         p << ("By disregarding the strictness conditions for the chosen "+++
  62                               "relations, the following term is a counter example:" +++
  63                               pre << ("f = " ++ res) ) +++
  64                         p << ("Whereas the abstraced variables are chosen as follows:" +++
  65                               pre << used)
  66         ) +++
  67         maindiv ( p << ("In the simplified theorems, the following custom haskell " +++
  68                         "functions might appear:") +++
  69                   pre << addDefs
  70         )
  71   where ft_full = let properType = "f :: " ++ case span (/='.') typeStr of
  72                                        (t,"")  -> t
  73                                        (_,_:t) -> t
  74                       (ds,es) = runChecks (parse properType >>= check)
  75                       [s]     = filterSignatures ds
  76                   in if null es
  77                      then case interpret [] BasicSubset s of
  78                         Nothing -> Left "interpret returned nothing"
  79                         Just i  -> Right $ render (prettyTheorem [] (asTheorem i)) ++
  80                               case unfoldLifts [] i of
  81                                 [] -> ""
  82                                 ls -> "\n\nWhereas the occuring lifts are defined as:\n\n "++
  83                                       unlines (map (render . prettyUnfoldedLift []) ls)
  84                      else Left (unlines (map render es))
  85
  86         ft_simple = freeTheorem typ
  87         counter_example = getComplete' typ
  88
  89 main = runCGI (handleErrors cgiMain)
  90
  91 cgiMain = do
  92         setHeader "Content-type" "text/xml; charset=UTF-8"
  93
  94         mTypeStr <- getInput "type"
  95
  96
  97         let content = case mTypeStr of
  98                 Nothing      -> askTypeForm
  99                 Just typeStr -> case parseType' typeStr of
 100                         Left err  -> typeError typeStr err
 101                         Right typ -> generateResult typeStr typ
 102
 103         outputFPS $ fromString $ showHtml $
 104                header (
 105                 thetitle << "PolyFix" +++
 106                 style ! [ thetype "text/css" ] << cdata cssStyle
 107                ) +++
 108                body ( form ! [method "POST", action "#"] << (
 109                 thediv ! [theclass "top"] << (
 110                         thespan ! [theclass "title"] << "PolyFix" +++
 111                         thespan ! [theclass "subtitle"] << "Counter Examples for Free Theorems"
 112                 ) +++
 113                 content +++
 114                 maindiv ( p << ("© 2008 Daniel Seidel und Joachim Breitner <" +++
 115                               hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
 116                               ">")
 117                         )
 118                 ))
 119
 120 maindiv = thediv ! [theclass "main"]
 121
 122 cdata s = primHtml ("<![CDATA[\n"++ s ++ "\n]]>")
 123
 124 cssStyle = unlines
 125         [ "body { padding:0px; margin: 0px; }"
 126         , "div.top { margin:0px; padding:10px; margin-bottom:20px;"
 127         , "              background-color:#efefef;"
 128         , "              border-bottom:1px solid black; }"
 129         , "span.title { font-size:xx-large; font-weight:bold; }"
 130         , "span.subtitle { padding-left:30px; font-size:large; }"
 131         , "div.main { border:1px dotted black;"
 132         , "                   padding:10px; margin:10px; }"
 133         , "div.submain { padding:10px; margin:11px; }"
 134         , "p.subtitle { font-size:large; font-weight:bold; }"
 135         , "input.type { font-family:monospace; }"
 136         , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }"
 137         , "span.mono { font-family:monospace; }"
 138         , "pre { margin:10px; margin-left:20px; padding:10px;"
 139         , "          border:1px solid black; }"
 140         , "textarea { margin:10px; margin-left:20px; padding:10px;  }"
 141         , "p { text-align:justify; }"
 142         ]
 143
 144 addDefs = unlines
 145         [ "allZipWith :: (a -> b -> Bool) -> [a] -> [b] -> Bool"
 146         , "allZipWith p [] [] = True"
 147         , "allZipWith p [] _  = False"
 148         , "allZipWith p _  [] = False"
 149         , "allZipWith p (x:xs) (y:ys) = p x y && allZipWith p xs ys"
 150         , ""
 151         , "eitherMap :: (a -> b) -> (c -> d) -> Either a c -> Either b d"
 152         , "eitherMap f1 f2 (Left v)  = Left (f1 v)"
 153         , "eitherMap f1 f2 (Right v) = Right (f2 v)"
 154         , ""
 155         , "andEither :: (a -> b -> Bool) -> (c -> d -> Bool) -> Either a c -> Bool"
 156         , "andEither p1 p2 (Left v1)  (Left v2)  = p1 v1 v2"
 157         , "andEither p1 p2 (Right v1) (Right v2) = p2 v1 v2"
 158         , "andEither _  _  _          _          = False"
 159         ]