Name vars corresponding to daniels output, identify strict functions
[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 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