[Equality on terms based on matching, selectors and observers for terms
martin.hofmann@uni-bamberg.de**20090211140142
 Terms/Unifier.hs:
 	- equal t1 t2 = matches t1 t2 && matches t2 t1
 	- equalLs as extension for Lists
 	- matches t1 t2 == True iff matching algorithm does not fail --> `catchError` used
 	- matchesLs as extension for lists
 Terms/Class.hs:
 	ctorAt, varAt, sameSymAt
 
] hunk ./src/Terms/Class.hs 24
-                           , Name, mkName)
+                           , Name, mkName) 
hunk ./src/Terms/Class.hs 31
+import Data.Function
hunk ./src/Terms/Class.hs 56
-    -> Int              -- ^ the nth sub-term
+    -> Int              -- ^ the nth sub-term (zero-based(
hunk ./src/Terms/Class.hs 58
-                        --   from position
+                        --   of the given position
hunk ./src/Terms/Class.hs 123
-
hunk ./src/Terms/Class.hs 128
+
+--    -- | @t1 `equals` t2 = true` if 't1' is identical to 't2' apart from
+--    --   variable renaming
+--    equal          :: t -> t -> Bool
+--    
+--    equalLs :: [t] -> [t] -> Bool
+--    equalLs [][] = True
+--    equalLs [] _ = False
+--    equalLs _ [] = False
+--    equalLs (t1:t1s)(t2:t2s) = (t1 `equal` t2) && (t1s `equalLs` t2s)
+    
+    
hunk ./src/Terms/Class.hs 148
-    -- | returns subterm @s@ at position @p@ in term @t@    
+    -- | returns subterm @s@ at position @p@ in term @t@, and 'Nothing' if there
+    --   is either no such position in this term, or no term at this position
+    --   (e.g. the term is a section of an infix operator)    
hunk ./src/Terms/Class.hs 152
-                    -> Position          -- ^ a position @p@
-                    -> Maybe t               -- ^ subterm @s@ in @t@ at position @p@
+                    -> Position            -- ^ a position @p@
+                    -> Maybe t             -- ^ subterm @s@ in @t@ at position @p@
hunk ./src/Terms/Class.hs 165
+    -- | Returns 'true' if both terms have the same constructor symbol at the
+    --   root position, 'False' otherwise
+    sameSymAtRoot :: t -> t -> Bool
+    
hunk ./src/Terms/Class.hs 171
-    sameAtPos :: t -> t -> Position -> Bool
-        
+    sameSymAt :: Position -> t -> t ->Bool
+    sameSymAt p t1 t2 = fromMaybe False $ liftM2 sameSymAtRoot (subtermAt t1 p)(subtermAt t2 p)
+    
hunk ./src/Terms/Class.hs 201
+    ctorAtPos :: t -> Position -> Bool
+    ctorAtPos t p = not $ varAtPos t p
+      
+    varAtPos :: t -> Position -> Bool
hunk ./src/Terms/Class.hs 217
+
+    sameSymAtRoot (VarE _) (VarE _)                        = True
+    sameSymAtRoot (ConE n1) (ConE n2)                      = n1 == n2
+    sameSymAtRoot (LitE l1) (LitE l2)                      = l1 == l2
+    sameSymAtRoot (TupE v1s)(TupE v2s)                     = on (==) length  v1s v2s
+    sameSymAtRoot t1@(AppE _ _ ) t2@(AppE _ _ )            = on (==) (head.unfoldAppE) t1 t2
+    sameSymAtRoot (ListE []) (ListE [])                    = True
+    sameSymAtRoot (ListE _)  (ListE [])                    = False
+    sameSymAtRoot (ListE []) (ListE _)                     = False
+    sameSymAtRoot (ListE _) (ListE _)                      = True
+    sameSymAtRoot (CondE c1 t1 e1) (CondE c2 t2 e2)        = True     
+    sameSymAtRoot (InfixE _ e1 _) (InfixE _ e2 _)          = e1 == e2 
+    sameSymAtRoot  _ _                                     = False
+    
hunk ./src/Terms/Class.hs 259
-                        
-    sameAtPos t1 t2 p = 
-        case (subtermAt t1 p, subtermAt t2 p) of
-        (Just st1, Just st2) -> compareAtRootE st1 st2
-        _otherwise           -> False
-            
+              
hunk ./src/Terms/Class.hs 270
-    subterms t@(AppE _ _ )                   = unfoldAppE t
+    subterms t@(AppE _ _ )                   = unfoldAppEargs t
hunk ./src/Terms/Class.hs 280
-    
+            
+    varAtPos t p = 
+        case subtermAt t p of
+            Just (VarE _) -> True
+            _owise        -> False
+            
hunk ./src/Terms/Class.hs 307
+
+    sameSymAtRoot (VarP _) (VarP _)                        = True
+    sameSymAtRoot (ConP c1 _) (ConP c2 _)                  = (c1 == c2)
+    sameSymAtRoot (LitP l1) (LitP l2)                      = l1 == l2
+    sameSymAtRoot (TupP v1s)(TupP v2s)                     = (length v1s) == (length v2s)
+    sameSymAtRoot (ListP [])(ListP [])                    = True
+    sameSymAtRoot (ListP [])(ListP _ )                    = False     
+    sameSymAtRoot (ListP _ )(ListP [])                    = False     
+    sameSymAtRoot (ListP _ )(ListP _ )                    = True     
+    sameSymAtRoot (InfixP _ n1 _) (InfixP _ n2 _)         = n1 ==  n2
+    sameSymAtRoot  _ _                                    = False
+
hunk ./src/Terms/Class.hs 338
-            
-                        
-    sameAtPos t1 t2 p = 
-        case (subtermAt t1 p, subtermAt t2 p) of
-        (Just st1, Just st2) -> compareAtRootP st1 st2
-        _otherwise           -> False
-        
+       
hunk ./src/Terms/Class.hs 348
-        
+    
+    varAtPos t p = 
+        case subtermAt t p of
+            Just (VarP _) -> True
+            _owise        -> False
+                 
hunk ./src/Terms/Class.hs 398
+-- | Returns only the arguments of an 'AppE'xpression.
hunk ./src/Terms/Class.hs 401
--- | Peals the @Exp@s out of a @AppE@
+-- | Peals the @Exp@s out of a @AppE@, where the first element should be the 
+--   @ConE@ of the function name or the constructor.
hunk ./src/Terms/Class.hs 482
-compareAtRootP :: Pat -> Pat -> Bool
-compareAtRootP (VarP _)(VarP _)               = True
-compareAtRootP (LitP l1)(LitP l2)             = l1 == l2 
-compareAtRootP (ConP n1 _)(ConP n2 _ )        = n1 == n2
-compareAtRootP (InfixP _ p1 _)(InfixP _ p2 _) = p1 == p2 
-compareAtRootP (ListP []) (ListP [])                    = True
-compareAtRootP (ListP []) (ListP _)                     = False
-compareAtRootP (ListP _)  (ListP [])                    = False
-compareAtRootP (ListP _)  (ListP _)                     = True
-compareAtRootP (TupP p1s)(TupP p2s)           = (length p1s) == (length p2s)
-compareAtRootP  _ _                           = False
+--compareAtRootP :: Pat -> Pat -> Bool
+--compareAtRootP (VarP _)(VarP _)               = True
+--compareAtRootP (LitP l1)(LitP l2)             = l1 == l2 
+--compareAtRootP (ConP n1 _)(ConP n2 _ )        = n1 == n2
+--compareAtRootP (InfixP _ p1 _)(InfixP _ p2 _) = p1 == p2 
+--compareAtRootP (ListP []) (ListP [])                    = True
+--compareAtRootP (ListP []) (ListP _)                     = False
+--compareAtRootP (ListP _)  (ListP [])                    = False
+--compareAtRootP (ListP _)  (ListP _)                     = True
+--compareAtRootP (TupP p1s)(TupP p2s)           = (length p1s) == (length p2s)
+--compareAtRootP  _ _                           = False
hunk ./src/Terms/Unifier.hs 6
-    Unifieable(mgu, applyMgu,matches)
+    Unifieable(mgu, applyMgu,matches, matchesLs, equal, equalLs)
hunk ./src/Terms/Unifier.hs 17
+import Data.Function
hunk ./src/Terms/Unifier.hs 58
+    
hunk ./src/Terms/Unifier.hs 60
+    -- | Returns a 'Substitution` with which 't1' matches 't2'. If the 
+    --   'Substitution' is empty, both terms are identical. If the terms do not
+    --   match, 'fail' is invoked in LM.
hunk ./src/Terms/Unifier.hs 65
-                          -- `catchError` (\_ -> return [])
-                          -- distinguish between equality and nomatch
-                          -- , so propagate error
+
+    -- | returns True, if 't1 `matches` t2' and vice versa.
+    equal :: t -> t -> Bool
+    equal t1 t2 = (matches t1 t2) && (matches t2 t1)
hunk ./src/Terms/Unifier.hs 70
-    matches ::  t -> t -> LM Bool
-    matches t1 t2 = liftM (not.null) $ 
-                    (matchesWithSubs t1 t2) `catchError` (\_ -> return [])
+    -- | returns True if both lists are of the same length and the elements are 
+    --   pairwise 'equal'
+    equalLs :: [t] -> [t] -> Bool
+    equalLs l1 l2 = (matchesLs l1 l2) && (matchesLs l2 l1)
hunk ./src/Terms/Unifier.hs 75
-    subsumes ::  t -> t -> LM Bool
-    subsumes t1 t2 = matches t2 t1
+     
+    -- | Returns True if 'matchesWithSubs' does not 'fail', False if it does.
+    matches ::  t -> t -> Bool
+    matches t1 t2 = unLM $ do{matchesWithSubs t1 t2 >> return True} 
+                             `catchError` (const.return $ False)
hunk ./src/Terms/Unifier.hs 81
-    match ::  t -> t -> U t
+    -- | returns True if both lists are of the same length and each element of
+    --   the first list pairwise 'matches' its colleague in the second list
+    matchesLs :: [t] -> [t] -> Bool
+                             
+    -- | subsumes = flip matches
+    subsumes ::  t -> t -> Bool
+    subsumes = flip matches
hunk ./src/Terms/Unifier.hs 89
+    -- | The matching algorithm. Note, that different from unify, where
+    --   'unify t1 t2 == unify t2 t1', 'match t1 t2 == match t2 t1' iff 
+    --   't1 == t2'
+    match ::  t -> t -> U t
+        
hunk ./src/Terms/Unifier.hs 163
+    matchesLs = matches `on` ListE
hunk ./src/Terms/Unifier.hs 165
-    match s@(VarE _) t@(VarE _)             = if (s == t) 
+    match s@(VarE i1) t@(VarE i2)             = if (i1 == i2) 
hunk ./src/Terms/Unifier.hs 169
-    match s          t@(VarE _)             = flush >> fail "No Match" 
+    match s          t@(VarE _)             = flush >> fail "No Match!" 
hunk ./src/Terms/Unifier.hs 282
+    matchesLs = matches `on` ListP
+    