[greedySplt implemented
martin.hofmann@uni-bamberg.de**20100810120931] hunk ./src/Igor2/RuleDevelopment/Partition.hs 4
-    partition, trivialPartition, partitionAt
+    partition, trivialPartition
hunk ./src/Igor2/RuleDevelopment/Partition.hs 39
+    gsplt <- doGreedySplt
hunk ./src/Igor2/RuleDevelopment/Partition.hs 41
-    let partpos  = concat.init.ruleVarPos $ crul cr
-    allParts <- mapM (partitionAt cruls) partpos
-    let parts = (filter (not.S.null)) allParts
+    let pivotpos  = concat.init.ruleVarPos $ crul cr
+    parts <- fuseParts $
+               (if gsplt then (((:[]) .) . fullPartitioning)
+                  else singlePartitioning) cruls pivotpos
hunk ./src/Igor2/RuleDevelopment/Partition.hs 46
-    llogDE ( text "At  :" <+> pretty partpos <^>
+    llogDE ( text "At  :" <+> pretty pivotpos <^>
hunk ./src/Igor2/RuleDevelopment/Partition.hs 55
- 
hunk ./src/Igor2/RuleDevelopment/Partition.hs 56
+fuseParts :: [[[CovrRule]]] -> IM [CovrRules] 
+fuseParts = lift . mapM ((liftM S.fromList).(mapM fuse))
+
hunk ./src/Igor2/RuleDevelopment/Partition.hs 61
-partitionAt :: [CovrRule] -> RulePos -> IM CovrRules
-partitionAt crs p =  lift $ liftM  S.fromList $ mapM fuse bins
+singlePartitioning :: [CovrRule] -> [RulePos] -> [[[CovrRule]]]
+singlePartitioning = (filter (not . null) .) . map . flip mkPartitionAt
+   
+-- described as 'Rapid RuleSplitting' in Emanuel's diss. Given 'n' pivot 
+-- positions, instead of making $n$ new hypothesis with partitions 
+-- corresponding to the construcotrs, make one new hypothisis, with partitions 
+-- corresponding to all pivot positions  Instead of making one partition for 
+-- each pivot position.
+fullPartitioning :: [CovrRule] -> [RulePos] -> [[CovrRule]]
+fullPartitioning =  foldr ((=<<) . mkPartitionAt) . return
hunk ./src/Igor2/RuleDevelopment/Partition.hs 72
-   where
-   bins = 
+-- partitioning helper, partitioin given CovrRule list w.r.t. the given RulePos
+mkPartitionAt :: RulePos -> [CovrRule] -> [[CovrRule]]
+mkPartitionAt p crs = 
hunk ./src/Igor2/RuleDevelopment/Partition.hs 78
-   cmpAtPos = (R.sameSymAt p) `on` crul
-   bin [] e            = [[e]]
-   bin ((x:xs):done) e
-    | cmpAtPos e x     =  (e:x:xs):done
-    | otherwise        =  (x:xs):(bin done e)  
-        
+    where
+      cmpAtPos = (R.sameSymAt p) `on` crul
+      bin [] e            = [[e]]
+      bin ((x:xs):done) e
+           | cmpAtPos e x     =  (e:x:xs):done
+           | otherwise        =  (x:xs):(bin done e)  
+     