[fold intro implemented and added as an option 
martin.hofmann@uni-bamberg.de**20090618030320] hunk ./src/Data/GlobalConfig.hs 14
+    , cnf_enhanced   :: Bool
hunk ./src/Data/GlobalConfig.hs 24
-defaultConfig = Conf False False (-1) Linear [] []
+defaultConfig = Conf False False False (-1) Linear [] []
hunk ./src/Data/IgorMonad.hs 9
-    tick, loopCount, loopsCount, hypoCount, isDebug, maxLoops, getPatComparison, background, 
+    tick, loopCount, loopsCount, hypoCount, isDebug, inEnhanced, ifIsSet, maxLoops, getPatComparison, background, 
hunk ./src/Data/IgorMonad.hs 87
+inEnhanced :: IM Bool
+inEnhanced = gets $ cnf_enhanced.config
+
+ifIsSet :: IM Bool -> IM a -> a ->  IM a
+ifIsSet c f d = do
+    b <- c
+    if b then f else return d
+    
hunk ./src/Data/Rules.hs 8
-    hasVarAt, hasCtorAt, matchesLhs, matchesRhs, matchEval,
+    hasVarAt, hasCtorAt, matchesLhs, matchesRhs, matchEval, matchEvals,
hunk ./src/RuleDevelopment.hs 11
+import RuleDevelopment.UniProp
hunk ./src/RuleDevelopment.hs 22
-    return $ parts  ++ subfs ++ mtchs
+    folds <- ifIsSet inEnhanced (foldUProp rf) []
+    return $ parts  ++ subfs ++ mtchs ++ folds
addfile ./src/RuleDevelopment/UniProp.hs
hunk ./src/RuleDevelopment/UniProp.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts -XTemplateHaskell #-}
+module RuleDevelopment.UniProp where
+
+import Data.Maybe (catMaybes, listToMaybe)
+import Data.List (partition)
+import qualified Data.Set as S (fromList)
+import Control.Monad
+
+import Data.IgorMonad
+import Data.CallDependencies
+import Data.Rules
+import Syntax.Expressions
+import Syntax.Terms
+import Syntax.Types
+import Logging
+
+foldUProp :: CovrRule -> IM [(CovrRules,[Call])]
+foldUProp cr = do
+    llogEnterIN 
+    llogIN (text "Check if Universal Property of 'fold' applies to: " <^>
+            pretty cr)
+    evi  <- liftM (map crul) $ breakupM cr
+    maybe noFoldCall (mkFoldCall cr)(checkUniPropAndMkIOs evi)
+     
+noFoldCall = llogIN (text "UniProp not applicable!") >> return []
+
+mkFoldCall :: CovrRule -> (RHS,[Rule]) -> IM [(CovrRules,[Call])]
+mkFoldCall cr (v,fios) =  do 
+    llogIN (text "UniProp applicable!")
+    subfnm    <- addIO.rules $ fios
+    crsub     <- coverAll subfnm
+    
+    f         <- liftM (getAll subfnm) getEvidence
+    llogIN (text "With function" <^> pretty f <$>
+            text "and start value" <^> pretty v)
+    
+    let alpha  = typeOf . head . lhs. head $ fios
+    let alist  = mkListT alpha
+    let beta   = typeOf v
+    let fty    = mkArrowT [alpha, beta, beta]
+    let fldty  = mkArrowT [fty,beta,alist,beta]
+    let fExp   = TConE subfnm fty
+    let fldarg = head.lhs.crul $ cr
+    let fldExp = foldTAppE (TConE 'foldr fldty) [fExp, v, fldarg]
+             
+    let cr' = modifycrul cr (\r -> rule (lhs r) fldExp)
+    let calls = [((name cr),subfnm,LT)]
+     
+    llogIN (text "Make Catamorphism:" <^> pretty cr')
+    return [(S.fromList [cr',crsub],calls)]
+
+     
+checkUniPropAndMkIOs :: [Rule] -> Maybe (RHS,[Rule])
+checkUniPropAndMkIOs evi = 
+    noNilIfDefForNil evi >>= \(r,rs) -> 
+    mapM (abduceIO evi) rs >>= 
+     return . (,) (rhs r)
+    
+noNilIfDefForNil :: [Rule] -> Maybe (Rule,[Rule])
+noNilIfDefForNil = maybeStripNil . partition (hasNilIn.lhs)
+
+maybeStripNil :: ([Rule], [Rule]) -> Maybe (Rule,[Rule])
+maybeStripNil (l1, l2) = 
+    listToMaybe l1 >>= \l1' -> 
+     return (l1', l2)
+
+hasNilIn :: LHS -> Bool
+hasNilIn [TListE [] _] = True
+hasNilIn [TConE n _]   = isNil n
+hasNilIn _             = False   
+
+abduceIO :: [Rule] -> Rule -> Maybe Rule
+abduceIO evi r = do
+    (x,xs) <- headTail.lhs $ r
+    xs'    <- matchEvals [xs] evi
+    return $ rule [x,xs'] (rhs r)         
+
+headTail :: LHS -> Maybe (TExp,TExp)
+headTail [TListE (x:xs) ty]          = Just (x, TListE xs ty)
+headTail [TInfixE l (TConE n _) r _] = 
+    if isCons n then Just (l,r) else Nothing
+headTail [l@(TAppE _ _ _)]           = 
+    let (o@(TConE n _):x:xs) = unfoldTAppE l
+    in if isCons n then Just (x,foldTAppE o xs) else Nothing
+headTail _                           = Nothing
hunk ./src/Syntax/Types.hs 10
-    sectionType, argumentType, unArrowT, mkArrowT, addPredicates, 
-    unfoldAppTargs, fixType
+    sectionType, argumentType, unArrowT, mkArrowT, mkListT,
+    addPredicates, unfoldAppTargs, fixType
hunk ./src/Syntax/Types.hs 113
+mkListT :: Type -> Type
+mkListT = AppT ListT
+
hunk ./src/UI/UIStarter.hs 6
-import Text.ParserCombinators.Parsec.Language( emptyDef, LanguageDef(..) )
+import Text.ParserCombinators.Parsec.Language( emptyDef, haskellDef, LanguageDef(..) )
hunk ./src/UI/UIStarter.hs 57
+    , enhanced  :: Bool
hunk ./src/UI/UIStarter.hs 83
+    , enhanced  = False
hunk ./src/UI/UIStarter.hs 264
-    newConfig = Conf (debug s) (simplify s) (maxLoops s) (cmpRecArg s) tgts bgks
+    newConfig = Conf (debug s) (simplify s)(enhanced s) (maxLoops s) (cmpRecArg s) tgts bgks
hunk ./src/UI/UIStarter.hs 414
+    , ("enhanced",           "synthesise in enhanced mode",
+            simplify, \ v s -> s { enhanced  = v })
hunk ./src/UI/UIStarter.hs 472
-         (emptyDef
+         (haskellDef