[Bugfix in pattern matching Exp and Pat
martin.hofmann@uni-bamberg.de**20090218090730
 match t@(AppE _ _)(TupE s)	 for up to 10-tuples
 match (TupE s) t@(AppE _ _)	 for up to 10-tuples
 match (ListE [])c@(ConE n)	 for n == '([])
 match c@(ConE n)(ListE [])       for n == '([])
 simialr for unify and Pat
 match(ConP n []) (ListP [])	 for n == '(:)
 match(ConP n ([p,ps])) (ListP (s:ss)) for n == '(:)
] hunk ./src/Terms/Unifier.hs 104
-				>> flush >> fail "No Match!"
+				>> flush "No Match!"
hunk ./src/Terms/Unifier.hs 133
-                                            then flush >> fail "Not unifieable"
+                                            then flush "Not unifieable"
hunk ./src/Terms/Unifier.hs 165
-    match s@(VarE i1) t@(VarE i2)             = if (i1 == i2) 
-                                                then return () 
-                                                else matchVar s t
+    -- matching variables
+    match s@(VarE i1) t@(VarE i2)
+        | i1 == i2                          = return ()
+        | otherwise                         = matchVar s t
hunk ./src/Terms/Unifier.hs 170
-    match s          t@(VarE _)             = flush >> fail "No Match!" 
-    
+    match s          t@(VarE _)             = flush "No Match!"
+    -- matching constructors    
hunk ./src/Terms/Unifier.hs 174
-        | otherwise                         = flush >> fail "No Match!"  
-        
+        | otherwise                         = flush "No Match!"  
+    -- matching literals          
hunk ./src/Terms/Unifier.hs 178
-        | otherwise                         = flush >> fail "No Match!"  
-         
+        | otherwise                         = flush "No Match!" 
+    -- matching tuples
hunk ./src/Terms/Unifier.hs 182
-        | otherwise                         = flush >> fail "No Match!"  
+        | otherwise                         = flush "No Match!"
+    match (TupE s) t@(AppE _ _)             = 
+        case unfoldAppE t of
+            (op:args) ->
+                if op == (ConE '(,)) && (length s) == (length args) ||
+                   op == (ConE '(,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,,)) && (length s) == (length args) 
+                  then mapM_ (uncurry match) (zip s args)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"  
+    match t@(AppE _ _)(TupE s)              = 
+        case unfoldAppE t of
+            (op:args) ->
+                if op == (ConE '(,)) && (length s) == (length args) ||
+                   op == (ConE '(,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,,)) && (length s) == (length args) 
+                  then mapM_ (uncurry match) (zip args s)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"  
hunk ./src/Terms/Unifier.hs 220
-    match (ListE (s:ss)) t@(AppE _ _)       = do
+    match (ListE [])c@(ConE n)               
+        | c == (ConE '[])                   = return ()
+        | otherwise                         = flush "No Match!"  
+    match c@(ConE n)(ListE [])              
+        | c == (ConE '[])                   = return ()
+        | otherwise                         = flush "No Match!"  
+    match (ListE (s:ss)) t@(AppE _ _)       =
hunk ./src/Terms/Unifier.hs 231
-                  else flush >> fail "No Match!"  
-            _owise       -> flush >> fail "No Match!"  
-    match t@(AppE _ _) s@(ListE _)          = match s t 
+                  else flush "No Match!"  
+            _owise       -> flush "No Match!"  
+    match t@(AppE _ _) (ListE (s:ss))       =
+        case unfoldAppE t of
+            (op:a1:[a2]) ->
+                if op == (ConE '(:))
+                  then match s a1 >> match (ListE ss) a2
+                  else flush "No Match!"  
+            _owise       -> flush "No Match!"  
hunk ./src/Terms/Unifier.hs 245
-        | otherwise                         = flush >> fail "No Match!"  
+        | otherwise                         = flush "No Match!"  
hunk ./src/Terms/Unifier.hs 257
-    unify s@(VarE _) t@(VarE _)             = if (s == t) 
-                                                then return () 
-                                                else unifyVar s t
+    unify s@(VarE _) t@(VarE _)
+        |(s == t)                           = return ()
+        | otherwise                         = unifyVar s t
hunk ./src/Terms/Unifier.hs 265
-        | otherwise                         = flush >> fail "Not unifieable" 
+        | otherwise                         = flush "Not unifieable" 
hunk ./src/Terms/Unifier.hs 269
-        | otherwise                         = flush >> fail "Not unifieable"
+        | otherwise                         = flush "Not unifieable"
hunk ./src/Terms/Unifier.hs 273
-        | otherwise                         = flush >> fail "Not unifieable" 
-        
+        | otherwise                         = flush "Not unifieable"
+    unify (TupE s) t@(AppE _ _)             = 
+        case unfoldAppE t of
+            (op:args) ->
+                if op == (ConE '(,)) && (length s) == (length args) ||
+                   op == (ConE '(,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,,)) && (length s) == (length args) 
+                  then mapM_ (uncurry unify) (zip s args)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"  
+    unify t@(AppE _ _)(TupE s)              = 
+        case unfoldAppE t of
+            (op:args) ->
+                if op == (ConE '(,)) && (length s) == (length args) ||
+                   op == (ConE '(,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,)) && (length s) == (length args) ||
+                   op == (ConE '(,,,,,,,,,,)) && (length s) == (length args) 
+                  then mapM_ (uncurry unify) (zip args s)
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable"
hunk ./src/Terms/Unifier.hs 307
-    unify (ListE (s:ss))(ListE (t:ts))      = unify s t >> unify (ListE ss) (ListE ts)
+    unify (ListE (s:ss))(ListE (t:ts))      = 
+        unify s t >> unify (ListE ss) (ListE ts)
hunk ./src/Terms/Unifier.hs 311
-    unify (ListE (s:ss)) t@(AppE _ _)       = do
+    unify (ListE [])c@(ConE n)             
+        | c == (ConE '[])                   = return ()
+        | otherwise                         = flush "Not unifieable!"  
+    unify c@(ConE n)(ListE [])              
+        | c == (ConE '[])                   = return ()
+        | otherwise                         = flush "Not unifieable!"  
+    unify (ListE (s:ss)) t@(AppE _ _)       = 
hunk ./src/Terms/Unifier.hs 322
-                  else flush >> fail "Not unifieable" 
-            _owise       -> flush >> fail "Not unifieable" 
-    unify t@(AppE _ _) s@(ListE _)          = unify s t 
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable" 
+    unify t@(AppE _ _) (ListE (s:ss))       =
+        case unfoldAppE t of
+            (op:a1:[a2]) ->
+                if op == (ConE '(:))
+                  then unify s a1 >> unify (ListE ss) a2
+                  else flush "Not unifieable" 
+            _owise       -> flush "Not unifieable" 
hunk ./src/Terms/Unifier.hs 336
-        | otherwise                         = flush >> fail "Not unifieable" 
+        | otherwise                         = flush "Not unifieable" 
hunk ./src/Terms/Unifier.hs 373
-    match s@(VarP _) t@(VarP _ )       = if (s == t) then return () else matchVar s t
-    match s@(VarP _) t                 = matchVar s t
-    match s          t@(VarP _)        = matchVar t s 
-         
+    match s@(VarP _) t@(VarP _ )           
+        | s == t                          = return ()
+        | otherwise                       = matchVar s t
+    match s@(VarP _) t                    = matchVar s t
+    match s          t@(VarP _)           = matchVar t s          
hunk ./src/Terms/Unifier.hs 379
-        | (s == t)                     = return () 
-        | otherwise                    = flush >> fail  "No Match!"  
-         
-    match (ListP [])(ListP [])         = return ()
-    match (ListP (s:ss))(ListP (t:ts)) = match s t >> match (ListP ss) (ListP ts) 
+        | (s == t)                        = return () 
+        | otherwise                       = flush  "No Match!"         
+    match (ListP [])(ListP [])            = return ()
+    match (ListP (s:ss))(ListP (t:ts))    = match s t >> match (ListP ss) (ListP ts) 
hunk ./src/Terms/Unifier.hs 385
-    match (ListP (s:ss))(ConP n ([p,ps]))= 
-        if n == '(:)
-          then match s p >> match (ListP ss) ps
-          else flush >> fail  "Not unifieable"  
-    match s@(ListP _) t@(ConP _ _)     = match t s
-    
+    match (ListP [])(ConP n [])
+        |n == '[]                         = return ()
+        | otherwise                       = flush  "No Match!"  
+    match(ConP n []) (ListP [])
+        |n == '[]                         = return ()
+        | otherwise                       = flush  "No Match!"  
+    match (ListP (s:ss))(ConP n ([p,ps]))
+        |n == '(:)                        = match s p >> match (ListP ss) ps
+        | otherwise                       = flush  "No Match!"  
+    match(ConP n ([p,ps])) (ListP (s:ss))
+        | n == '(:)                       = match s p >> match (ListP ss) ps
+        | otherwise                       = flush  "No Match!"  
+    match s@(ListP _) t@(ConP _ _)        = match t s    
hunk ./src/Terms/Unifier.hs 399
-        | n1 == n2                     = mapM_ (uncurry match) (zip p1 p2)
-        | otherwise                    = flush >> fail  "No Match!"  
-        
+        | n1 == n2                        = mapM_ (uncurry match) (zip p1 p2)
+        | otherwise                       = flush  "No Match!"          
hunk ./src/Terms/Unifier.hs 402
-        | (length s) == (length t)     = mapM_ (uncurry match) (zip s t)
-        | otherwise                    = flush >> fail  "No Match!"  
-        
+        | (length s) == (length t)        = mapM_ (uncurry match) (zip s t)
+        | otherwise                       = flush  "No Match!"       
+    match (ConP n p) (TupP t) 
+        | n == '(,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | n == '(,,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip p t)
+        | otherwise                    = flush "No Match!"      
+    match (TupP t)(ConP n p) 
+        | n == '(,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | n == '(,,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry match) (zip t p)
+        | otherwise                    = flush "No Match!"      
hunk ./src/Terms/Unifier.hs 427
-        | s2 == t2                     = match s1 t1 >> match s3 t3
-        | otherwise = flush >> fail  "No Match!"  
-        
-    match s t                          =    
-        flush >> fail  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))
+        | s2 == t2                        = match s1 t1 >> match s3 t3
+        | otherwise = flush  "No Match!"          
+    match s t                             =    
+        flush  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))
hunk ./src/Terms/Unifier.hs 433
-    unify s@(VarP _) t@(VarP _ )       = if (s == t) then return () else unifyVar s t
+    unify s@(VarP _) t@(VarP _ )        
+        | s == t                       = return ()
+        | otherwise                    = unifyVar s t
hunk ./src/Terms/Unifier.hs 437
-    unify s          t@(VarP _)        = unifyVar t s 
-         
+    unify s          t@(VarP _)        = unifyVar t s         
hunk ./src/Terms/Unifier.hs 440
-        | otherwise                    = flush >> fail  "Not unifieable"
-         
+        | otherwise                    = flush  "Not unifieable"         
hunk ./src/Terms/Unifier.hs 445
-    unify (ListP (s:ss))(ConP n ([p,ps]))= 
-        if n == '(:)
-          then unify s p >> unify (ListP ss) ps
-          else flush >> fail  "Not unifieable"
-    unify s@(ListP _) t@(ConP _ _)     = unify t s
-    
+    unify (ListP [])(ConP n [])        
+        | n == '[]                     = return ()
+        | otherwise                    = flush "Not unifieable"
+    unify(ConP n []) (ListP [])
+        |n == '[]                      = return ()
+        | otherwise                    = flush  "Not unifieable"
+    unify (ListP (s:ss))(ConP n ([p,ps]))
+        |n == '(:)                     = unify s p >> unify (ListP ss) ps
+        | otherwise                    = flush "Not unifieable"
+    unify(ConP n ([p,ps])) (ListP (s:ss))
+        | n == '(:)                    = unify s p >> unify (ListP ss) ps
+        | otherwise                    = flush "Not unifieable"    
hunk ./src/Terms/Unifier.hs 459
-        | otherwise                    = flush >> fail  "Not unifieable"
-        
+        | otherwise                    = flush  "Not unifieable"        
hunk ./src/Terms/Unifier.hs 462
-        | otherwise                    = flush >> fail  "Not unifieable"
-        
+        | otherwise                    = flush  "Not unifieable"       
+    unify (ConP n p) (TupP t) 
+        | n == '(,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | n == '(,,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip p t)
+        | otherwise                    = flush  "Not unifieable"       
+    unify (TupP t)(ConP n p) 
+        | n == '(,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | n == '(,,,,,,,,,) && (length p) == (length t) = mapM_ (uncurry unify) (zip t p)
+        | otherwise                    = flush  "Not unifieable" 
hunk ./src/Terms/Unifier.hs 487
-        | otherwise = flush >> fail  "Not unifieable"
-        
+        | otherwise = flush  "Not unifieable"        
hunk ./src/Terms/Unifier.hs 489
-        flush >> fail  ("Term " ++ (show s) ++ "not unifieable with " ++ (show t))
+        flush  ("Term " ++ (show s) ++ "not unifieable with " ++ (show t))
hunk ./src/Terms/Unifier.hs 491
-flush :: (MonadState (Substitution t) m) => m () 
-flush = put []
+flush :: (MonadState (Substitution t) m) => String -> m () 
+flush s = put [] >> fail s