Remove obsolete functions (as top levels)
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 14 Oct 2008 12:49:05 +0000 (12:49 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 14 Oct 2008 12:49:05 +0000 (12:49 +0000)
Expr.hs
SimpleFT.hs

diff --git a/Expr.hs b/Expr.hs
index eb60aac..74d2a98 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -63,15 +63,53 @@ aand x        y        = And ([x,y])
 
 beTrue = And []
 
+-- | Is any var (or part of var) defined in cond, and can be replaced in concl?
+condition :: [TypedExpr] -> BoolExpr -> BoolExpr -> BoolExpr
+condition vars cond concl | ((vars',cond',concl'):_) <- mapMaybe try vars
+                         = condition vars' cond' concl'
+                          | otherwise
+                          = Condition vars cond concl
+  where try v = do d <- defFor v cond --Maybe Monad
+                   return (delete v vars, replaceTermBE v d cond, replaceTermBE v d concl)
+
+-- | Replaces a Term in a BoolExpr
+replaceTermBE :: TypedExpr -> TypedExpr -> BoolExpr -> BoolExpr
+replaceTermBE d' r' = go
+  where d = unTypeExpr d'
+        r = unTypeExpr r'
+       go (e1 `Equal` e2) | d == e1 && r == e2 = beTrue
+                           | d == e2 && r == e1 = beTrue
+                           | otherwise          = go' e1 `Equal` go' e2
+        go (And es)        = foldr aand beTrue (map go es)
+        go (AllZipWith v1 v2 be e1 e2) 
+                           = AllZipWith v1 v2 (go be) (go' e1) (go' e2)
+       go (Condition vs cond concl)
+                          = condition vs (go cond) (go concl)
+       go (UnpackPair v1 v2 e be)
+                          = unpackPair v1 v2 (goT e) (go be)
+       go (TypeVarInst _ _) = error "TypeVarInst not expected here"
+       goT = replaceTypedExpr d' r'
+       go' = replaceExpr d r
+
+replaceExpr :: Expr -> Expr -> Expr -> Expr
+replaceExpr d r = everywhere (mkT go)
+  where go e | e == d    = r 
+             | otherwise = e
+
+replaceTypedExpr :: TypedExpr -> TypedExpr -> TypedExpr -> TypedExpr
+replaceTypedExpr d r = everywhere (mkT go)
+  where go e | e == d    = r 
+             | otherwise = e
+
 -- | Is inside the term a definition for the variable?
 defFor :: TypedExpr -> BoolExpr -> Maybe TypedExpr
 defFor tv be | Just e' <- defFor' (unTypeExpr tv) be
                          = Just (TypedExpr e' (typeOf tv))
              | otherwise = Nothing
        
-defFor' v (e1 `Equal` e2) | v == e1                 = Just e2
-                          | v == e2                 = Just e1
-defFor' v (And es)        | [d]  <- mapMaybe (defFor' v) es -- exactly one definition
+defFor' e (e1 `Equal` e2) | e == e1                 = Just e2
+                          | e == e2                 = Just e1
+defFor' e (And es)        | [d]  <- mapMaybe (defFor' e) es -- exactly one definition
                                                    = Just d
 defFor' _ _                                         = Nothing
 
index 15324e1..7dda161 100644 (file)
@@ -32,22 +32,13 @@ freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
                fillTuplevars True t1 $ \tve2 ->  do
                        cond  <- freeTheorem' (tve1) (tve2) t1
                        concl <- freeTheorem' (app e1 tve1) (app e2 tve2) t2
-                       return $ Condition [tve1, tve2] cond concl
+                       return $ condition [tve1, tve2] cond concl
 
        -- No tuple on the left hand side:
                                  | otherwise  = getSideVars t1 $ \(v1,v2) -> do
        cond  <- freeTheorem'  v1  v2 t1
-       -- See if the variables (tv*) actually have equivalent terms (ev*)
-       case (defFor  v1 cond, defFor  v2 cond) of
-         (Just ev1, _) -> do
-               concl <- freeTheorem' (app e1 ev1) (app e2  v2) t2
-               return $ unCond v2 concl
-         (Nothing,Just ev2) -> do
-               concl <- freeTheorem' (app e1  v1) (app e2 ev2) t2
-               return $ unCond v1 concl
-         _ -> do
-               concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
-               return $ Condition [ v1, v2 ] cond concl
+       concl <- freeTheorem' (app e1  v1) (app e2  v2) t2
+       return $ condition [ v1, v2 ] cond concl
 
 freeTheorem' e1 e2 (List t) = getSideVars t $ \(v1,v2) -> do
        map <- freeTheorem' v1 v2 t