Pairwise -> allZipWith
[darcs-mirror-polyfix.git] / SimpleFT.hs
index 12585dc..ec9d7af 100644 (file)
@@ -22,27 +22,25 @@ freeTheorem' e1 e2 (List t) = do
        [v1,v2] <- asks (take 2)
        local (drop 2) $ do
                map <- freeTheorem' (Var v1) (Var v2) t
-               return $ case map of
-                 (Equal (Var v1') ev1) | v1' == v1 -> 
-                       if ev1 == (Var v2)
-                       then Equal e1 e2
-                       else Equal e1 (App (App (Var "map") (lambda v2 ev1)) e2)
-                 _ ->       Pairwise v1 v2 map e1 e2
+               return $ allZipWith v1 v2 map e1 e2
 
 freeTheorem' e1 e2 (Arrow t1 t2) = do
        [v1,v2] <- asks (take 2)
        local (drop 2) $ do
                cond  <- freeTheorem' (Var v1) (Var v2) t1
-               case cond of
-                 (Equal (Var v1') ev1) | v1' == v1 -> do
-                       concl <- freeTheorem' (App e1 ev1) (App e2 (Var v2)) t2
-                       return $ unCond v2 concl
+               case (defFor v1 cond, defFor v2 cond) of
+                 (Just ev1, _) -> do
+                       concl <- freeTheorem' (App e1 ev1)      (App e2 (Var v2)) t2
+                       return $ unCond v2 True t1 concl
+                 (Nothing,Just ev2) -> do
+                       concl <- freeTheorem' (App e1 (Var v1)) (App e2 ev2)      t2
+                       return $ unCond v1 False t1 concl
                  _ -> do
                        concl <- freeTheorem' (App e1 (Var v1)) (App e2 (Var v2)) t2
-                       return $ Condition v1 v2 cond concl
+                       return $ Condition v1 v2 t1 cond concl
 
 freeTheorem' e1 e2 (TVar (TypVar i)) = return $
-       Equal e1 (App (Var ("g"++show i)) e2)
+       Equal (App (Var ("g"++show i)) e1) e2
 
 freeTheorem' e1 e2 (AllStar (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t
 freeTheorem' e1 e2 (All     (TypVar i) t) = TypeVarInst i `fmap` freeTheorem' e1 e2 t