Rename to PolyFix
authorJoachim Breitner <mail@joachim-breitner.de>
Wed, 15 Oct 2008 15:03:52 +0000 (15:03 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Wed, 15 Oct 2008 15:03:52 +0000 (15:03 +0000)
nameme-cgi.hs [deleted file]
polyfix-cgi.hs [new file with mode: 0644]

diff --git a/nameme-cgi.hs b/nameme-cgi.hs
deleted file mode 100644 (file)
index e8311f9..0000000
+++ /dev/null
@@ -1,140 +0,0 @@
-module Main where
-
-import ParseType (parseType')
-import SimpleFT  (freeTheorem)
-import Expr (specialize)
-import ExFindExtended (getComplete')
-import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
-import Language.Haskell.FreeTheorems
-       ( runChecks
-       , check
-       , filterSignatures
-       , prettyTheorem
-       , asTheorem
-       , interpret
-       , unfoldLifts
-       , prettyUnfoldedLift
-       , LanguageSubset(BasicSubset)
-       )
-
-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)
-
-main = runCGI (handleErrors cgiMain)
-
-cgiMain = do
-       setHeader "Content-type" "text/xml; charset=UTF-8"
-       
-       mTypeStr <- getInput "type"
-
-       
-       let content = case mTypeStr of 
-               Nothing      -> askTypeForm
-                Just typeStr -> case parseType' typeStr of
-                       Left err  -> typeError typeStr err
-                       Right typ -> generateResult typeStr typ
-       
-       outputFPS $ fromString $ showHtml $
-              header (
-               thetitle << "Name Me" +++
-               style ! [ thetype "text/css" ] << cdata cssStyle
-              ) +++
-              body ( form ! [method "POST", action "#"] << (
-               thediv ! [theclass "top"] << (
-                       thespan ! [theclass "title"] << "Name Me" +++
-                       thespan ! [theclass "subtitle"] << "Counter Examples for Free Theorems"
-               ) +++
-               content +++
-               maindiv ( p << ("© 2008 Daniel Seidel und Joachim Breitner <" +++
-                             hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
-                             ">")
-                       )       
-               ))
-
-maindiv = thediv ! [theclass "main"]
-
-cdata s = primHtml ("<![CDATA[\n"++ s ++ "\n]]>")
-
-cssStyle = unlines 
-        [ "body { padding:0px; margin: 0px; }"
-        , "div.top { margin:0px; padding:10px; margin-bottom:20px;"
-        , "              background-color:#efefef;"
-        , "              border-bottom:1px solid black; }"
-        , "span.title { font-size:xx-large; font-weight:bold; }"
-        , "span.subtitle { padding-left:30px; font-size:large; }"
-        , "div.main { border:1px dotted black;"
-        , "                   padding:10px; margin:10px; }"
-        , "div.submain { padding:10px; margin:11px; }"
-        , "p.subtitle { font-size:large; font-weight:bold; }"
-        , "input.type { font-family:monospace; }"
-        , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }"
-        , "span.mono { font-family:monospace; }"
-        , "pre { margin:10px; margin-left:20px; padding:10px;"
-        , "          border:1px solid black; }"
-        , "textarea { margin:10px; margin-left:20px; padding:10px;  }"
-        , "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
-       
diff --git a/polyfix-cgi.hs b/polyfix-cgi.hs
new file mode 100644 (file)
index 0000000..2748641
--- /dev/null
@@ -0,0 +1,140 @@
+module Main where
+
+import ParseType (parseType')
+import SimpleFT  (freeTheorem)
+import Expr (specialize)
+import ExFindExtended (getComplete')
+import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
+import Language.Haskell.FreeTheorems
+       ( runChecks
+       , check
+       , filterSignatures
+       , prettyTheorem
+       , asTheorem
+       , interpret
+       , unfoldLifts
+       , prettyUnfoldedLift
+       , LanguageSubset(BasicSubset)
+       )
+
+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)
+
+main = runCGI (handleErrors cgiMain)
+
+cgiMain = do
+       setHeader "Content-type" "text/xml; charset=UTF-8"
+       
+       mTypeStr <- getInput "type"
+
+       
+       let content = case mTypeStr of 
+               Nothing      -> askTypeForm
+                Just typeStr -> case parseType' typeStr of
+                       Left err  -> typeError typeStr err
+                       Right typ -> generateResult typeStr typ
+       
+       outputFPS $ fromString $ showHtml $
+              header (
+               thetitle << "PolyFix" +++
+               style ! [ thetype "text/css" ] << cdata cssStyle
+              ) +++
+              body ( form ! [method "POST", action "#"] << (
+               thediv ! [theclass "top"] << (
+                       thespan ! [theclass "title"] << "PolyFix" +++
+                       thespan ! [theclass "subtitle"] << "Counter Examples for Free Theorems"
+               ) +++
+               content +++
+               maindiv ( p << ("© 2008 Daniel Seidel und Joachim Breitner <" +++
+                             hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
+                             ">")
+                       )       
+               ))
+
+maindiv = thediv ! [theclass "main"]
+
+cdata s = primHtml ("<![CDATA[\n"++ s ++ "\n]]>")
+
+cssStyle = unlines 
+        [ "body { padding:0px; margin: 0px; }"
+        , "div.top { margin:0px; padding:10px; margin-bottom:20px;"
+        , "              background-color:#efefef;"
+        , "              border-bottom:1px solid black; }"
+        , "span.title { font-size:xx-large; font-weight:bold; }"
+        , "span.subtitle { padding-left:30px; font-size:large; }"
+        , "div.main { border:1px dotted black;"
+        , "                   padding:10px; margin:10px; }"
+        , "div.submain { padding:10px; margin:11px; }"
+        , "p.subtitle { font-size:large; font-weight:bold; }"
+        , "input.type { font-family:monospace; }"
+        , "input[type=\"submit\"] { font-family:monospace; background-color:#efefef; }"
+        , "span.mono { font-family:monospace; }"
+        , "pre { margin:10px; margin-left:20px; padding:10px;"
+        , "          border:1px solid black; }"
+        , "textarea { margin:10px; margin-left:20px; padding:10px;  }"
+        , "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
+