XGitUrl: https://git.nomeata.de/?p=darcsmirrorpolyfix.git;a=blobdiff_plain;f=polyfixcgi.hs;h=e78ee05f78b6628ec88d9fef87391c656b25299d;hp=274864124d038c685ddb198a83522c953f17083c;hb=0840d64fae731a7f97d22a92821c1ef3088bc51a;hpb=5ce7f1a415908442c5d01f5b9d3e4ba3721f3147
diff git a/polyfixcgi.hs b/polyfixcgi.hs
index 2748641..e78ee05 100644
 a/polyfixcgi.hs
+++ b/polyfixcgi.hs
@@ 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 etareduction, this theorem can be written as:" +++
+ pre << show ft_simple +++
+ p << "Further specializing all types to (), all strict functions to id and all nonstrict functions to const (), this theorem can be written as:" +++
+ pre << show (specialize ft_simple)
+ ) +++
+ maindiv << (
+ h3 << "The counterexample" +++
+ 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 { textalign: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 etareduction, this theorem can be written as:" +++
 pre << show ft_simple +++
 p << "Further specializing all types to (), all strict functions to id and all nonstrict functions to const (), this theorem can be written as:" +++
 pre << show (specialize ft_simple)
 ) +++
 maindiv << (
 h3 << "The counterexample" +++
 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"
+ ]