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