Remove TypSamples
[darcs-mirror-polyfix.git] / polyfix-cgi.hs
index 2748641..e78ee05 100644 (file)
@@ -21,10 +21,71 @@ import Network.CGI
 import Data.ByteString.Lazy.UTF8 (fromString)
 import Text.XHtml
 import Control.Monad
-import System.Random (randomRIO)
 import Data.Maybe
 import Text.PrettyPrint.HughesPJ (render)
 
+askDiv v e =  maindiv << (
+       p << ( "Please enter a function type, prepended with a list of type variables, " +++
+              "whose relations should be allowed to be nonstrict, and a single dot.") +++            p << ( input ! [name "type", value v] +++ " " +++
+              submit "submit" "Generate Free Theorem and counter example" ) +++
+       e
+       )
+
+
+askTypeForm = askDiv "a. (a -> b) -> b" noHtml
+
+typeError typeStr err = askDiv typeStr (
+       p << ("There was a problem parsing your type: " +++
+             pre << err )
+       )
+
+generateResult typeStr typ = askDiv typeStr noHtml +++
+       maindiv << (
+       h3 << "The Free Theorem" +++
+       (case ft_full of
+               Left err -> p << "The full Free Theorem deriver failed:" +++
+                            pre << err
+                Right s  -> p << "For your type, the following Free Theorem holds:" +++
+                           pre << s
+       ) +++
+       p << "Specializing relations to functions, canceling irrelvant terms and eta-reduction, this theorem can be written as:" +++
+       pre << show ft_simple +++
+       p << "Further specializing all types to (), all strict functions to id and all non-strict functions to const (), this theorem can be written as:" +++
+       pre << show (specialize ft_simple)
+       ) +++
+       maindiv << (
+       h3 << "The counter-example" +++
+       case counter_example of 
+               Left err -> p << "No term could be derived: " +++ pre << err
+               Right (res,used) ->
+                       p << ("By disregarding the strictness conditions for the chosen "+++
+                              "relations, the following term is a counter example:" +++
+                              pre << ("f = " ++ res) ) +++
+                       p << ("Whereas the abstraced variables are chosen as follows:" +++
+                              pre << used)
+       ) +++
+       maindiv ( p << ("In the simplified theorems, the following custom haskell " +++
+                        "functions might appear:") +++
+                 pre << addDefs
+       )
+  where ft_full = let properType = "f :: " ++ case span (/='.') typeStr of
+                                       (t,"")  -> t
+                                       (_,_:t) -> t
+                     (ds,es) = runChecks (parse properType >>= check)
+                      [s]     = filterSignatures ds
+                 in if null es
+                     then case interpret [] BasicSubset s of
+                       Nothing -> Left "interpret returned nothing"
+                       Just i  -> Right $ render (prettyTheorem [] (asTheorem i)) ++
+                             case unfoldLifts [] i of
+                               [] -> ""
+                               ls -> "\n\nWhereas the occuring lifts are defined as:\n\n "++
+                                     unlines (map (render . prettyUnfoldedLift []) ls)
+                     else Left (unlines (map render es))
+                   
+       ft_simple = freeTheorem typ
+        counter_example = getComplete' typ
+       
 main = runCGI (handleErrors cgiMain)
 
 cgiMain = do
@@ -80,61 +141,19 @@ cssStyle = unlines
         , "p { text-align:justify; }"
         ]
 
-askDiv v e =  maindiv << (
-       p << ( "Please enter a function type, prepended with a list of type variables, " +++
-              "whose relations should be allowed to be nonstrict, and a single dot.") +++            p << ( input ! [name "type", value v] +++ " " +++
-              submit "submit" "Generate Free Theorem and counter example" ) +++
-       e
-       )
-
-
-askTypeForm = askDiv "a. (a -> b) -> b" noHtml
-
-typeError typeStr err = askDiv typeStr (
-       p << ("There was a problem parsing your type: " +++
-             pre << err )
-       )
-
-generateResult typeStr typ = askDiv typeStr noHtml +++
-       maindiv << (
-       h3 << "The Free Theorem" +++
-       (case ft_full of
-               Left err -> p << "The full Free Theorem deriver failed:" +++
-                            pre << err
-                Right s  -> p << "For your type, the following Free Theorem holds:" +++
-                           pre << s
-       ) +++
-       p << "Specializing relations to functions, canceling irrelvant terms and eta-reduction, this theorem can be written as:" +++
-       pre << show ft_simple +++
-       p << "Further specializing all types to (), all strict functions to id and all non-strict functions to const (), this theorem can be written as:" +++
-       pre << show (specialize ft_simple)
-       ) +++
-       maindiv << (
-       h3 << "The counter-example" +++
-       case counter_example of 
-               Left err -> p << "No term could be derived: " +++ pre << err
-               Right (res,used) ->
-                       p << ("By disregarding the strictness conditions for the pointed "+++
-                              "variables(?), the following term is a counter example:" +++
-                              pre << ("f = " ++ res) ) +++
-                       p << ("Wheres the abstraced variables are chosen as follows:" +++
-                              pre << used)
-       )
-  where ft_full = let properType = "f :: " ++ case span (/='.') typeStr of
-                                       (s,"")  -> s
-                                       (_,_:s) -> s
-                     (ds,es) = runChecks (parse properType >>= check)
-                      [s]     = filterSignatures ds
-                 in if null es
-                     then case interpret [] BasicSubset s of
-                       Nothing -> Left "interpret returned nothing"
-                       Just i  -> Right $ render (prettyTheorem [] (asTheorem i)) ++
-                             case unfoldLifts [] i of
-                               [] -> ""
-                               ls -> "\n\nWhereas the occuring lifts are defined as:\n\n "++
-                                     unlines (map (render . prettyUnfoldedLift []) ls)
-                     else Left (unlines (map render es))
-                   
-       ft_simple = freeTheorem typ
-        counter_example = getComplete' typ
-       
+addDefs = unlines 
+       [ "allZipWith :: (a -> b -> Bool) -> [a] -> [b] -> Bool"
+       , "allZipWith p [] [] = True"
+       , "allZipWith p [] _  = False"
+       , "allZipWith p _  [] = False"
+       , "allZipWith p (x:xs) (y:ys) = p x y && allZipWith p xs ys"
+       , ""
+       , "eitherMap :: (a -> b) -> (c -> d) -> Either a c -> Either b d"
+       , "eitherMap f1 f2 (Left v)  = Left (f1 v)"
+       , "eitherMap f1 f2 (Right v) = Right (f2 v)"
+       , ""
+       , "andEither :: (a -> b -> Bool) -> (c -> d -> Bool) -> Either a c -> Bool"
+       , "andEither p1 p2 (Left v1)  (Left v2)  = p1 v1 v2"
+       , "andEither p1 p2 (Right v1) (Right v2) = p2 v1 v2"
+       , "andEither _  _  _          _          = False"
+       ]