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