Small adjustment, forgotten patterns
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 16 Oct 2008 07:50:24 +0000 (07:50 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 16 Oct 2008 07:50:24 +0000 (07:50 +0000)
Expr.hs
polyfix-cgi.hs

diff --git a/Expr.hs b/Expr.hs
index cc155e7..b895827 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -26,7 +26,6 @@ data EVar = F
 
 data Expr
        = Var EVar
-       | TheOneFunc
        | App Expr Expr
        | Conc [Expr] -- Conc [] is Id
        | Lambda TypedExpr Expr
@@ -111,11 +110,13 @@ andEither lbe1 lbe2 e1 e2 | Just f1 <- arg1IsFunc lbe1
                          | otherwise
                           = AndEither lbe1 lbe2 (unTypeExpr e1) (unTypeExpr e2)
 
+arg1IsFunc :: LambdaBE -> Maybe TypedExpr
 arg1IsFunc (CurriedEquals t)    = Just $ TypedExpr (Conc []) (Arrow t t)
 arg1IsFunc (LambdaBE v1 v2 rel) | Just v1' <- defFor v1 rel
                                 = Just (lambda v2 v1')
                                | otherwise = Nothing
 
+arg2IsFunc :: LambdaBE -> Maybe TypedExpr
 arg2IsFunc (CurriedEquals t)    = Just $ TypedExpr (Conc []) (Arrow t t)
 arg2IsFunc (LambdaBE v1 v2 rel) | Just v2' <- defFor v2 rel
                                 = Just (lambda v1 v2')
@@ -263,7 +264,7 @@ app te1 te2 | otherwise                          = error $ "Type mismatch in app
 
 app' :: Expr -> Expr -> Expr
 app' Map (Conc []) = Conc []   -- map id = id
-app' ConstUnit v   = EUnit     -- id x   = x
+app' ConstUnit _   = EUnit     -- id x   = x
 app' (Conc []) v   = v         -- id x   = x
 app' f v           = App f v
 
@@ -286,6 +287,7 @@ conc x          y        = Conc ([x,y])
 
 -- Specialization of g'
 
+specialize :: BoolExpr -> BoolExpr
 specialize (TypeVarInst strict i be') = 
                replaceTermBE (Var (FromTypVar i)) (if strict then Conc [] else ConstUnit) .
                everywhere (mkT $ go) $
@@ -344,6 +346,7 @@ instance Show Expr where
                                   showsPrec 0 e1 .
                                   showString "," .
                                   showsPrec 0 e2
+       showsPrec _ EUnit         = showString "()"
        showsPrec _ Map           = showString "map"
        showsPrec d ConstUnit     = showParen (d>10) $ showString "const ()"
        showsPrec _ EitherMap     = showString "eitherMap"
@@ -417,7 +420,7 @@ instance Show BoolExpr where
                        show (2*i) ++
                        ", " ++
                        (if strict then "strict " else "(strict) ") ++
-                       "functions " ++
+                       "functions g" ++
                        show i ++
                        " :: t" ++
                        show (2*i-1) ++
index e27c4d4..e78ee05 100644 (file)
@@ -21,7 +21,6 @@ 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)
 
@@ -62,12 +61,16 @@ generateResult typeStr typ = askDiv typeStr noHtml +++
                        p << ("By disregarding the strictness conditions for the chosen "+++
                               "relations, the following term is a counter example:" +++
                               pre << ("f = " ++ res) ) +++
-                       p << ("Wheres the abstraced variables are chosen as follows:" +++
+                       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
-                                       (s,"")  -> s
-                                       (_,_:s) -> s
+                                       (t,"")  -> t
+                                       (_,_:t) -> t
                      (ds,es) = runChecks (parse properType >>= check)
                       [s]     = filterSignatures ds
                  in if null es
@@ -108,8 +111,6 @@ cgiMain = do
                        thespan ! [theclass "subtitle"] << "Counter Examples for Free Theorems"
                ) +++
                content +++
-               maindiv ( p << ("In the simplified theorems, the following custom haskell functions might appear:") +++
-                         pre << addDefs ) +++
                maindiv ( p << ("© 2008 Daniel Seidel und Joachim Breitner <" +++
                              hotlink "mailto:mail@joachim-breitner.de" << "mail@joachim-breitner.de" +++
                              ">")