Before Lambda untyping

diff --git a/ExFindExtended.hs b/ExFindExtended.hs
index f648a25..7da129a 100644 (file)
--- a/ExFindExtended.hs
+++ b/ExFindExtended.hs
@@ -1,4 +1,4 @@
-module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,getComplete',getCompleteRaw,getWithDebug,getIt) where
+module ExFindExtended (TypVar(..),Typ(..),TermVar(..),Term,TermCont,TermPlus,PlusElem(..),AbsTerm(..),testTerm,getTerm,getComplete,showTerm,showUsedTermCont,getCompleteRaw,getWithDebug,getIt) where
 
 import Prelude hiding (Either(..))
 import qualified Prelude as E (Either(..))
@@ -998,12 +998,6 @@ getComplete tau = do {printTyp tau;
                                                }
                     }
 
-getComplete' :: Typ -> E.Either String (String, String)
-getComplete' tau = case getCompleteRaw tau of 
-                     E.Left err          -> E.Left err
-                     E.Right (result)    -> E.Right (showTerm (fst result),
-                                                      uncurry showUsedTermCont result)
-
 getCompleteRaw :: Typ -> E.Either String (Term,TermCont)
 getCompleteRaw tau = case runM $ alg emptyCont tau emptyTermCont of
                      Nothing             -> E.Left "No Term."

diff --git a/Expr.hs b/Expr.hs
index 17dba20..6d76000 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -31,7 +31,9 @@ data Expr
        | Lambda TypedExpr Expr
        | Pair Expr Expr
        | Map
-       | ConstUnit
+       | Const Expr
+       | ELeft Expr
+       | ERight Expr
        | CaseUnit Expr Expr
        | EitherMap
        | EUnit
@@ -63,6 +65,7 @@ equal' :: Expr -> Expr -> BoolExpr
 equal' e1 e2  | (Just (lf,lv)) <- isFunctionApplication e1
               , (Just (rf,rv)) <- isFunctionApplication e2
               , lv == rv 
+             , False
                                         = equal' lf rf
              -- This makes it return True...
              | e1 == e2                 = beTrue
@@ -190,6 +193,11 @@ condition vars cond concl | True -- set to false to disable
 -- Nothing left to optizmize
 condition vars cond concl = Condition vars cond concl
 
+
+caseUnit Bottom e = Bottom
+caseUnit EUnit e  = e
+caseUnit v e      = CaseUnit v e
+
 -- | Replaces a Term in a BoolExpr
 replaceTermBE :: Expr -> Expr -> BoolExpr -> BoolExpr
 replaceTermBE d r = go
@@ -222,6 +230,8 @@ replaceExpr d r = go
        go (Conc es)     = foldr conc (Conc []) (map go es)
        go (Lambda te e) = lambda' te (go e)
        go (Pair e1 e2)  = Pair (go e1) (go e2)
+       go (Const e)     = Const (go e)
+       go (CaseUnit v e) = caseUnit (go v) (go e)
        go e             = e
 
 
@@ -265,8 +275,10 @@ app te1 te2 | otherwise                          = error $ "Type mismatch in app
                                                            show te1 ++ " " ++ show te2
 
 app' :: Expr -> Expr -> Expr
+app' Bottom    _   = Bottom    -- _|_ x = _|_
+app' (Lambda tv e1) (e2) = replaceExpr (unTypeExpr tv) e2 e1 -- lambda application
 app' Map (Conc []) = Conc []   -- map id = id
-app' ConstUnit _   = EUnit     -- id x   = x
+app' (Const e) _   = e         -- const x y = x
 app' (Conc []) v   = v         -- id x   = x
 app' f v           = App f v
 
@@ -274,24 +286,28 @@ lambda :: TypedExpr -> TypedExpr -> TypedExpr
 lambda tv e = TypedExpr (lambda' tv (unTypeExpr e)) (Arrow (typeOf tv) (typeOf e))
 
 lambda' :: TypedExpr -> Expr -> Expr
-lambda' tv e  | (Just e') <- isApplOn (unTypeExpr tv) e
+lambda' tv e  | e == EUnit           = Const EUnit
+              | (Just e') <- isApplOn (unTypeExpr tv) e
              , not (unTypeExpr tv `occursIn` e')
                                      = e'
              | unTypeExpr tv == e   = Conc []
               | otherwise            = Lambda tv e
 
 conc :: Expr -> Expr -> Expr
-conc (Conc xs) (Conc ys) = Conc (xs  ++ ys)
-conc (Conc xs)  y        = Conc (xs  ++ [y])
-conc x         (Conc ys) = Conc ([x] ++ ys)
-conc x          y        = Conc ([x,y])
+conc (Lambda v (CaseUnit v' e)) (Conc ((Const EUnit):r))
+                               | unTypeExpr v == v' = conc (Const e) (Conc r)
+conc (Lambda v (CaseUnit v' e)) (Const EUnit) | unTypeExpr v == v' = Const e
+conc (Conc xs) (Conc ys)        = Conc (xs  ++ ys)
+conc (Conc xs)  y               = Conc (xs  ++ [y])
+conc x         (Conc ys)        = Conc ([x] ++ ys)
+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) .
+               replaceTermBE (Var (FromTypVar i)) (if strict then Conc [] else Const EUnit) .
                everywhere (mkT $ go) $
                be
        where be = specialize be'
@@ -350,7 +366,13 @@ instance Show Expr where
                                   showsPrec 0 e2
        showsPrec _ EUnit         = showString "()"
        showsPrec _ Map           = showString "map"
-       showsPrec d ConstUnit     = showParen (d>10) $ showString "const ()"
+       showsPrec d (ELeft e)     = showParen (d>10) $ 
+                                       showString "Left ".
+                                       showsPrec 11 e
+       showsPrec d (ERight e)    = showParen (d>10) $ 
+                                       showString "Right ".
+                                       showsPrec 11 e
+       showsPrec d (Const e)     = showParen (d>10) $ showString "const ".showsPrec 11 e
        showsPrec d (CaseUnit t1 t2) = showParen (d>5) $
                                        showString "case " .
                                        showsPrec 0 t1 .

diff --git a/polyfix-cgi.hs b/polyfix-cgi.hs
index 0b3d966..7fcfb60 100644 (file)
--- a/polyfix-cgi.hs
+++ b/polyfix-cgi.hs
@@ -3,7 +3,7 @@ module Main where
 import ParseType (parseType')
 import SimpleFT  (freeTheorem)
 import Expr (specialize)
-import ExFindExtended (getComplete', getCompleteRaw)
+import ExFindExtended (getCompleteRaw, showTerm, showUsedTermCont)
 import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
 import Language.Haskell.FreeTheorems
        ( runChecks
@@ -54,29 +54,26 @@ generateResult typeStr typ = askDiv typeStr noHtml +++
        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)
+       pre << show ft_simple_special
        ) +++
        maindiv << (
        h3 << "The counter-example" +++
        ( case counter_example of 
                Left err -> p << "No term could be derived: " +++ pre << err
-               Right (res,used) ->
+               Right result ->
                        p << ("By disregarding the strictness conditions for the chosen "+++
                               "relations, the following term is a counter example:" +++
-                              pre << ("f = " ++ res) ) +++
+                              pre << ("f = " ++ showTerm (fst result)) ) +++
                        p << ("Whereas the abstraced variables are chosen as follows:" +++
-                              pre << used)
-       ) +++
-       h3 << "The raw counter-example" +++
-       case counter_example_raw of 
-               Left err -> p << "No term could be derived: " +++ pre << err
-               Right result ->
-                       p << (show result) +++
-                       p << (show (term2Expr (fst result))) +++
-                       p << (show (termCond2Exprs (snd result))) +++
-                       p << (show (insertTermsInCondition result (specialize ft_simple))) +++
-                       p << (gshow (insertTermsInCondition result (specialize ft_simple)))
-       ) +++
+                              pre << uncurry showUsedTermCont result) +++
+                       p << ("Inserting these defintions in the above theorem yields:" +++
+                       -- p << (show result) +++
+                       -- p << (show (term2Expr (fst result))) +++
+                       -- p << (show (termCond2Exprs (snd result))) +++
+                             pre << (show (insertTermsInCondition result ft_simple_special))
+                               ) 
+                       -- p << (gshow (insertTermsInCondition result (specialize ft_simple)))
+       )) +++
        maindiv ( p << ("In the simplified theorems, the following custom haskell " +++
                         "functions might appear:") +++
                  pre << addDefs
@@ -97,8 +94,8 @@ generateResult typeStr typ = askDiv typeStr noHtml +++
                      else Left (unlines (map render es))
                    
        ft_simple = freeTheorem typ
-        counter_example = getComplete' typ
-       counter_example_raw = getCompleteRaw typ
+       ft_simple_special = specialize ft_simple
+        counter_example = getCompleteRaw typ
        
 main = runCGI (handleErrors cgiMain)