77446938a0a07d968c3ca9af1e43e9243adfbdc6
[darcs-mirror-polyfix.git] / nameme-cgi.hs
1 module Main where
2
3 import ParseType (parseType')
4 import SimpleFT  (freeTheorem)
5 import ExFindExtended (getComplete')
6
7 import Network.CGI
8 import Data.ByteString.Lazy.UTF8 (fromString)
9 import Text.XHtml
10 import Control.Monad
11 import System.Random (randomRIO)
12 import Data.Maybe
13
14 main = runCGI (handleErrors cgiMain)
15
16 cgiMain = do
17         setHeader "Content-type" "text/xml; charset=UTF-8"
18         
19         mTypeStr <- getInput "type"
20
21         
22         let content = case mTypeStr of 
23                 Nothing      -> askTypeForm
24                 Just typeStr -> case parseType' typeStr of
25                         Left err  -> typeError typeStr err
26                         Right typ -> generateResult typeStr typ
27         
28         outputFPS $ fromString $ showHtml $
29                header (
30                 thetitle << "Name Me" +++
31                 style ! [ thetype "text/css" ] << cdata cssStyle
32                ) +++
33                body ( form ! [method "POST", action "#"] << (
34                 thediv ! [theclass "top"] << (
35                         thespan ! [theclass "title"] << "Name Me" +++
36                         thespan ! [theclass "subtitle"] << "Counter Examples for Free Theorems"
37                 ) +++
38                 content +++
39                 maindiv ( p << ("© 2008 Daniel Seidel und Joachim Breitner <" +++
40                               hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
41                               ">")
42                         )       
43                 ))
44
45 maindiv = thediv ! [theclass "main"]
46
47 cdata s = primHtml ("<![CDATA[\n"++ s ++ "\n]]>")
48
49 cssStyle = unlines 
50         [ "body { padding:0px; margin: 0px; }"
51         , "div.top { margin:0px; padding:10px; margin-bottom:20px;"
52         , "              background-color:#efefef;"
53         , "              border-bottom:1px solid black; }"
54         , "span.title { font-size:xx-large; font-weight:bold; }"
55         , "span.subtitle { padding-left:30px; font-size:large; }"
56         , "div.main { border:1px dotted black;"
57         , "                   padding:10px; margin:10px; }"
58         , "div.submain { padding:10px; margin:11px; }"
59         , "p.subtitle { font-size:large; font-weight:bold; }"
60         , "input.type { font-family:monospace; }"
61         , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }"
62         , "span.mono { font-family:monospace; }"
63         , "pre { margin:10px; margin-left:20px; padding:10px;"
64         , "          border:1px solid black; }"
65         , "textarea { margin:10px; margin-left:20px; padding:10px;  }"
66         , "p { text-align:justify; }"
67         ]
68
69
70 askTypeForm = maindiv << p << (
71         "Please enter a function type, prepended with a list of unpointed " +++
72         "type variables and a single dot." +++ br +++
73         input ! [name "type", value "a. (a -> b) -> b"] +++ " " +++
74         submit "submit" "Generate Free Theorem and counter example"
75         )
76
77 typeError typeStr err = maindiv << (
78         p << ("Please enter a function type, prepended with a list of unpointed " +++
79               "type variables and a single dot.") +++
80         p << (input ! [name "type", value typeStr] +++ " " +++
81               submit "submit" "Generate Free Theorem and counter example") +++
82         p << ("There was a problem parsing your type: " +++
83               pre << err )
84         )
85
86 generateResult typeStr typ = maindiv << (
87         "Please enter a function type, prepended with a list of unpointed " +++
88         "type variables and a single dot." +++ br +++
89         input ! [name "type", value typeStr] +++ " " +++
90         submit "submit" "Generate Free Theorem and counter example"
91         ) +++
92         maindiv << (
93         h3 << "The Free Theorem" +++
94         p << "For your type, the following Free Theorem holds:" +++
95         pre << (show (freeTheorem typ))
96         ) +++
97         maindiv << (
98         h3 << "The counter-example" +++
99         case getComplete' typ of 
100                 Left err -> p << "No term could be derived: " +++ err
101                 Right (res,used) ->
102                         p << ("By disregarding the strictness conditions for the pointed "+++
103                               "variables(?), the following term is a counter example:" +++
104                               pre << ("f = " ++ res) ) +++
105                         p << ("Wheres the abstraced variables are chosen as follows:" +++
106                               pre << used)
107         )
108
109