comments
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 14 Oct 2008 10:29:04 +0000 (10:29 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 14 Oct 2008 10:29:04 +0000 (10:29 +0000)
Expr.hs
SimpleFT.hs

diff --git a/Expr.hs b/Expr.hs
index 180a376..2563050 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -37,8 +37,13 @@ allZipWith v1 v2 rel e1 e2 | Just v1' <- defFor v1 rel =
                            | otherwise =
                                AllZipWith v1 v2 rel e1 e2
 
+-- | Is inside the term a definition for the variable?
 defFor v (e1 `Equal` e2) | (Var v) == e1 = Just e2
                          | (Var v) == e2 = Just e1
+defFor v (e1 `And` e2)   | Just d  <- defFor v e1
+                        , Nothing <- defFor v e2 = Just d
+defFor v (e1 `And` e2)   | Just d  <- defFor v e2
+                        , Nothing <- defFor v e1 = Just d
 defFor _ _                               = Nothing
 
 app Map (Conc []) = Conc []
index add0c1a..9113a61 100644 (file)
@@ -22,14 +22,18 @@ freeTheorem' e1 e2 (TVar (TypVar i)) = return $
        Equal (App (Var ("g"++show i)) e1) e2
 
 freeTheorem' e1 e2 (Arrow t1 t2) | isTuple t1 = do
+       -- Create patterns for (possily nested) tuples and only give
+       -- the inner variables names
        fillTuplevars t1 $ \ve1 -> 
                fillTuplevars t1 $ \ve2 ->  do
                        cond  <- freeTheorem' ve1 ve2 t1
                        concl <- freeTheorem' (App e1 ve1) (App e2 ve2) t2
                        return $ Condition ve1 ve2 t1 cond concl
 
+       -- No tuple on the left hand side:
                                  | otherwise  = getVars 2 $ \[v1,v2] -> do
        cond  <- freeTheorem' (Var v1) (Var v2) t1
+       -- See if the variables actually have definitions
        case (defFor v1 cond, defFor v2 cond) of
          (Just ev1, _) -> do
                concl <- freeTheorem' (App e1 ev1)      (App e2 (Var v2)) t2