nameme-cgi.hs

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