[completely switched to typed terms, algo runs, but may not be correct
martin.hofmann@uni-bamberg.de**20090417104357] hunk ./src/Context/ContextBuilder.hs 15
+-- for translation 
+import Language.Haskell.Meta.Parse
+import qualified Data.Typeable as T
+import Data.Generics
+import Language.Haskell.Exts.Parser (ParseResult(..))
+import qualified Language.Haskell.Exts.Syntax as Hs
+--
+
hunk ./src/Context/ContextBuilder.hs 27
---import Syntax.TempRules
hunk ./src/Context/ContextBuilder.hs 32
+import Data.Rules
+
hunk ./src/Context/ContextBuilder.hs 37
-import Language.Haskell.Meta.Parse
-import qualified Data.Typeable as T
-import Data.Generics
-import Language.Haskell.Exts.Parser (ParseResult(..))
-import qualified Language.Haskell.Exts.Syntax as Hs
-
hunk ./src/Context/ContextBuilder.hs 280
-    toTExp :: Type -> t -> C TExp
+    toTExp   :: Type -> t -> C TExp
hunk ./src/Context/ContextBuilder.hs 285
-    toTPat :: Type -> t -> C TPat
+    toTPat   :: Type -> t -> C TPat
hunk ./src/Context/ContextBuilder.hs 351
-    toTPat _ p = fail $ "No Translation defined for " ++ (show p)    
-
---data Type
--- = ForallT [Name] Cxt Type
--- | VarT Name
--- | ConT Name
--- | TupleT Int
--- | ArrowT
--- | ListT
--- | AppT Type Type
-
-
+    toTPat _ p = fail $ "No Translation defined for " ++ (show p)
hunk ./src/Context/ContextBuilder.hs 354
-clauses2rules :: ModuleCtx -> Name -> [Clause] -> Either String (Name, [([TPat], TExp)])
+clauses2rules :: ModuleCtx -> Name -> [Clause] -> Either String (Name, Rules)
hunk ./src/Context/ContextBuilder.hs 358
-                        return (n,rs)
+                        return (n, mkRules rs)
hunk ./src/Context/ModuleContext.hs 5
+
hunk ./src/Context/ModuleContext.hs 9
-import qualified Context.SynthesisContext as SC
-import Logging
hunk ./src/Context/ModuleContext.hs 10
+import Data.Rules
+import Data.Either
+import Data.List (intersperse)
hunk ./src/Context/ModuleContext.hs 14
-type Rule = ([TPat],TExp)
-type Rules = [Rule]
+import qualified Context.SynthesisContext as SC
+
+import Logging
hunk ./src/Context/ModuleContext.hs 21
+--type Rule = ([TPat], TExp) 
+--type Rules = [Rule]
hunk ./src/Context/ModuleContext.hs 36
+getBindings :: [Name] -> ModuleCtx -> Either String [(Name, Rules)]
+getBindings ns ctx = do
+    let (ls,rs) = partitionEithers $ map (getBinding ctx) ns
+    if not.null $ ls
+      then fail $ errmsg ls
+      else return rs
+    where
+    errmsg s = "No examples found for function name(s) " ++
+               concat (intersperse ", " s) ++
+               "!"
hunk ./src/Context/ModuleContext.hs 47
+getBinding :: (Monad m) => ModuleCtx -> Name -> m (Name, Rules)
+getBinding ctx n =
+    case Map.lookup n (mctx_bindings ctx) of
+        Just rs -> return (n,rs)
+        Nothing -> fail $ "'" ++ (show n) ++ "'" 
hunk ./src/Data/Initialiser.hs 1
-{-# OPTIONS_GHC -fglasgow-exts -XTemplateHaskell #-}
--- | This module defines several functions to translate from/to TH datatypes
-module Data.Initialiser (
-    
-    -- * Converting from Language.haskell.TH
-    decs2rules, dec2rules, clauses2rules, clause2rules,
-    -- * Converting to Language.haskell.TH
-    hypos2decs,rules2decs, rules2dec, rules2clauses, rule2clauses,
-
-    -- * Helpers
-    toRule,
-    
-    )where
-
-import Language.Haskell.TH 
-import Language.Haskell.TH.Syntax
-import Control.Monad
-import Data.Rules (Rules,Rule, rules, rule, lhs, rhs)
-import qualified Data.Rules as R
-import Data.List
-import qualified Data.Set as S
-
-import Debug.Trace
-import Data.Hypotheses (Hypos, Hypo, hypo)
-import qualified Data.Hypotheses as H
-
-import Logging
-
--- | Convert a list of Language.Haskell.TH.Dec to a list of Name Rules pairs
---   A Dec is expected to be a function definition (FunD), if not, an error
---   is thrown.
-decs2rules :: [Dec] -> [(Name,Rules)]
-decs2rules = map dec2rules
-
--- | Convert a single Language.Haskell.TH.Dec to a Name Rules pair
---   A Dec is expected to be a function definition (FunD), if not, an error
---   is thrown.
-dec2rules :: Dec -> (Name,Rules)
-dec2rules (FunD n cs) =  (n,clauses2rules cs) 
-dec2rules d = error $ 
-    "Initialiser.dec2rules: " ++ 
-    show d ++ 
-    " is not a function definition!"
-
--- | Convert a list of Langugae.Haskell.TH.Clause to Rules.
---   A Clause is expected to have a normal (not guarded) body (NormalB),
---   otherwise an error is thrown.
-clauses2rules :: [Clause] -> Rules
-clauses2rules cs =  rules $ map clause2rules cs
-
--- | Convert a sibgle Langugae.Haskell.TH.Clause to a Rule.
---   A Clause is expected to have a normal (not guarded) body (NormalB),
---   otherwise an error is thrown.
-clause2rules :: Clause -> Rule
-clause2rules (Clause ls (NormalB rs) _) = rule ls rs
-clause2rules c = error $ 
-    "Cannot transform clause " ++ 
-    (show c) ++ 
-    " to a rule!"
-
---   
-hypos2decs :: [[(Name,Rules)]] -> [[Dec]]
-hypos2decs hs =  map rules2decs hs
-
-rules2decs :: [(Name,Rules)] -> [Dec]
-rules2decs = map rules2dec
-
-rules2dec :: (Name,Rules) -> Dec
-rules2dec (n,rs) = FunD n (rules2clauses rs)
-
-rules2clauses :: Rules -> [Clause]
-rules2clauses rs = map rule2clauses (S.toList rs)
-     
-rule2clauses :: Rule -> Clause
-rule2clauses r = Clause (lhs r) (NormalB $ rhs r) [] 
-    
-
---
--- Convenience Functions for Testing
---
-
-toRule :: [Dec] -> Rule
-toRule = head . S.toList . snd . dec2rules . head
---
----------------------------------------------------
----- Testing Data
---------------------------------------------------- 
---printQ q = (runQ q) >>= putStrLn . pprint 
---showQ q = (runQ q) >>= putStrLn . show
---mkVP s = VarP (mkName s)
---mkVE s = VarE (mkName s)
--- 
---rev = liftM head [d| rev [] = []
---                     rev [x] = [x]
---                     rev [x,y] = [y,x]
---                     rev [x,y,z] = [z,x,y]
---                     rev [w,x,y,z] = [z,y,x,w] 
---                 |]
---revai = liftM head [d| rev x = x
---                       rev (x1:xs) = (x1:xs)
---                       rev (x1:x2:xs) = (x1:x2:xs)
---                       rev (x1:x2:x3:xs) = (x1:x2:x3:xs)
---                       rev (x1:x2:x3:x4:[]) = (x1:x2:x3:x4:[]) 
---                   |]
---rev0 = rule [ConP '[] []] (ConE '[])
---rev1 = rule [ListP [mkVP "a_6"]] (ListE [mkVE "a_6"])
---rev2 = rule [ListP [mkVP "a_7",mkVP "b_8"]] (ListE [mkVE "b_8",mkVE "a_7"])
---rev3 = rule [ListP [mkVP "a_9",mkVP "b_10",mkVP "c_11"]] (ListE [mkVE "c_11",mkVE "b_10",mkVE "a_9"])
---rev4 = rule [ListP [mkVP "a_12",mkVP "b_13",mkVP "c_14", mkVP "d_15"]] (ListE [mkVE "d_15", mkVE "c_14",mkVE "b_12",mkVE "a_11"])
---
---ep = (mkVP "y1_14")
---revai04 = rule [mkVP "x_14"] (mkVE "y_14")
---fragai04 = ruleFrag (mkName "rev") revai04 [0,1,2,3,4] []
---revai14 = rule [InfixP (mkVP "x1_15") '(:) (mkVP "x_16")] 
---                (InfixE (Just (mkVE "y1_15")) (ConE '(:)) (Just (mkVE "ys_16")))
---fragai14 = ruleFrag (mkName "rev") revai14 [1,2,3,4] []                
---revai24 = rule [InfixP (mkVP "x1_17") '(:) (InfixP (mkVP "x2_18") '(:) (mkVP "xs_19"))]
---               (InfixE (Just (mkVE "y1_17")) (ConE '(:)) (Just (InfixE (Just (mkVE "y2_18")) (ConE '(:)) (Just (mkVE "ys_19")))))
---fragai24 = ruleFrag (mkName "rev") revai24 [2,3,4] []                
---revai34 = rule [InfixP (mkVP "x1_20") '(:) (InfixP (mkVP "x2_21") '(:) (InfixP (mkVP "x3_22") '(:) (mkVP "xs_23")))]
---               (InfixE (Just (mkVE "y1_20")) (ConE '(:)) (Just (InfixE (Just (mkVE "y2_21")) (ConE '(:)) (Just (InfixE (Just (mkVE "y3_22")) (ConE '(:)) (Just (mkVE "ys_23")))))))
---fragai34 = ruleFrag (mkName "rev") revai34 [3,4] []                
---revai44 = rule [InfixP (mkVP "x1_24") '(:) (InfixP (mkVP "x2_25") '(:) (InfixP (mkVP "x3_26") '(:) (InfixP (mkVP "x4_27") '(:) (ConP '[] []))))]
---               (InfixE (Just (mkVE "y1_24")) (ConE '(:)) (Just (InfixE (Just (mkVE "y2_25")) (ConE '(:)) (Just (InfixE (Just (mkVE "y3_26")) (ConE '(:)) (Just (InfixE (Just (mkVE "y4_27")) (ConE '(:)) (Just (ConE '[])))))))))
---fragai44 = ruleFrag (mkName "rev") revai44 [4] []                
---
---fragsempty = ruleFrags []
---fragsai04 = ruleFrags [fragai04]
---fragsai14 = ruleFrags [fragai04,fragai14]
---fragsai24 = ruleFrags [fragai04,fragai14,fragai24]
---fragsai34 = ruleFrags [fragai04,fragai14,fragai24,fragai34]
---fragsai44 = ruleFrags [fragai04,fragai14,fragai24,fragai34,fragai44]
---
---hypor04 = hypo $ ruleFrags [fragai04]
---hypor14 = hypo $ fragsai14 --ruleFrags [fragai04,fragai14]
---hypor24 = hypo $ ruleFrags [fragai04,fragai14,fragai24]
---hypor34 = hypo $ ruleFrags [fragai04,fragai14,fragai24,fragai34]
---hypor44 = hypo $ ruleFrags [fragai04,fragai14,fragai24,fragai34,fragai44]
---
---
---pd0414 = (fragai04,ruleFrags [fragai04,fragai14],[])
---pd1424 = (fragai14,ruleFrags [fragai04,fragai14,fragai24],[])
---pd2434 = (fragai24,ruleFrags [fragai04,fragai14,fragai24,fragai34],[])
---pd3444 = (fragai34,ruleFrags [fragai04,fragai14,fragai24,fragai34,fragai44],[])
---
-----revhsp0 = initHSpace hypor04
-----revhsp1 = insert hypor24 revhsp0
-----revhsp2 = insert hypor34 revhsp1
-----revhsp3 = insert hypor44 revhsp2
-----
-----test1 = propagate pd1424 $ propagate pd0414 revhsp3
-----
-----hyposrevall = insert hypor44 $ insert hypor34 $ insert hypor24 $ insert hypor14 $  initHSpace hypor04
---
---revs = (mkName "rev", rules [rev0,rev1,rev2,rev3,rev4])
---
---snoc = liftM head [d| snoc [] w = [w]
---                      snoc [w] x = [w,x]
---                      snoc [w,x] y = [w,x,y]
---                      snoc [w,x,y] z = [w,x,y,z] 
---                  |]
---
---snoc0 = rule [ConP '[] [], mkVP "w_0"](ListE [mkVE "w_0"])
---snoc1 = rule [ListP [mkVP "w_1"],mkVP "x_2"] (ListE [mkVE "w_1",mkVE "x_2"])
---snoc2 = rule [ListP [mkVP "w_3",mkVP "x_4"],mkVP "y_5"] (ListE [mkVE "w_3",mkVE "x_4",mkVE "y_5"])
---snoc3 = rule [ListP [mkVP "w_6",mkVP "x_7",mkVP "y_8"],mkVP "z_9"] (ListE [mkVE "w_6",mkVE "x_7",mkVE "y_8",mkVE "z_9"])
---
rmfile ./src/Data/Initialiser.hs
hunk ./src/Data/Rules.hs 4
-    Rule, rule, rhs, lhs,
+    Rule, mkRule, rule, rhs, lhs,
hunk ./src/Data/Rules.hs 9
-    Rules, rules, subrule, insertCall, subsumesAll,
+    Rules, mkRules, rules, subrule, insertCall, subsumesAll,
hunk ./src/Data/Rules.hs 12
-    LHS, RHS,
+    LHS, RHS, hypos2decs,
hunk ./src/Data/Rules.hs 25
-import qualified Data.Set as S (empty, fromList, toAscList, map, null, insert, delete)
+import qualified Data.Set as S (empty, fromList, toList, toAscList, map, null, insert, delete)
hunk ./src/Data/Rules.hs 34
+
+
hunk ./src/Data/Rules.hs 50
-type LHS = [Pat]
-type RHS = Exp
+type LHS = [TPat]
+type RHS = TExp
+
+mkRule :: ([TPat],TExp) -> Rule
+mkRule (l,r) = rule l r
hunk ./src/Data/Rules.hs 56
+mkRules = rules . (map mkRule)
hunk ./src/Data/Rules.hs 65
-rule :: LHS -> RHS -> Rule
+rule :: [TPat] -> TExp -> Rule
hunk ./src/Data/Rules.hs 78
-type OpenPos = (Exp,[Position])
+type OpenPos = (TExp,[Position])
hunk ./src/Data/Rules.hs 82
-freeVars  :: Rule -> [Exp]
+freeVars  :: Rule -> [TExp]
hunk ./src/Data/Rules.hs 87
-    in map VarE diff
+    in map (mkVar (rhs r)) diff
hunk ./src/Data/Rules.hs 114
-replaceInLhs :: Rule -> RulePos -> Pat -> Rule
+replaceInLhs :: Rule -> RulePos -> TPat -> Rule
hunk ./src/Data/Rules.hs 119
-replaceInRhs :: Rule -> RulePos -> Exp -> Rule
+replaceInRhs :: Rule -> RulePos -> TExp -> Rule
hunk ./src/Data/Rules.hs 124
+-- TODO niocer and clearer
hunk ./src/Data/Rules.hs 126
-insertCall p n r = replaceInRhs r p (pat2Call n (lhs r)) 
+insertCall (Body pos) n r = 
+    let callpat = lhs r
+        subty   = typeOf . fromJust . (flip subtermAt pos) . rhs $ r
+    in replaceInRhs r (Body pos) (tPat2Call n subty callpat) 
hunk ./src/Data/Rules.hs 131
-ruleSubtermAt :: RulePos -> Rule -> Either (Maybe Pat) (Maybe Exp)
+ruleSubtermAt :: RulePos -> Rule -> Either (Maybe TPat) (Maybe TExp)
hunk ./src/Data/Rules.hs 135
-lhsSubtermAt :: RulePos -> Rule -> Maybe Pat
+lhsSubtermAt :: RulePos -> Rule -> Maybe TPat
hunk ./src/Data/Rules.hs 140
-rhsSubtermAt :: RulePos -> Rule -> Maybe Exp
+rhsSubtermAt :: RulePos -> Rule -> Maybe TExp
hunk ./src/Data/Rules.hs 161
-        (left,right)<-  antiunify2 tlhss rhss pat2Exp
+        (left,right)<-  antiunify2 tlhss rhss tPat2TExp
hunk ./src/Data/Rules.hs 183
-	pretty r = text.pprint $ Clause (lhs r) (NormalB $ rhs r) []
+	pretty = text.pprint.rule2clause
hunk ./src/Data/Rules.hs 186
+-------------
+-- Auxiliaries
+-------------
+pat2Call :: Name ->[Pat] -> Exp
+pat2Call n ps = foldl1 AppE $ (ConE n):(map pat2Exp ps)    
+    
+pat2Exp :: Pat -> Exp
+pat2Exp (VarP i)        = (VarE i)
+pat2Exp (LitP l)       = (LitE l) 
+pat2Exp (ConP n ps)    = foldl1 AppE $ (ConE n):(map pat2Exp ps)
+pat2Exp (InfixP l n r) = InfixE (Just . pat2Exp $ l)(ConE n)(Just . pat2Exp $ r) 
+pat2Exp (ListP l)      = ListE $ map pat2Exp l
+pat2Exp (TupP ps)      = TupE $ map pat2Exp ps
+pat2Exp p              = error $ "Syntax.IFTemplateHaskell.pat2Exp: Pattern " 
+                              ++ show p 
+                              ++ " cannot be transformed into an Expression!" 
+    
+tPat2Call :: Name -> Type -> [TPat] -> TExp
+tPat2Call n ty ps = foldTAppE (TConE n ty) (map tPat2TExp ps)    
hunk ./src/Data/Rules.hs 206
+tPat2TExp :: TPat -> TExp
+tPat2TExp (TVarP i t) = (TVarE i t)
+tPat2TExp (TLitP l t) = (TLitE l t) 
+tPat2TExp (TConP n ps t) = foldTAppE (TConE n t) (map tPat2TExp ps)
+tPat2TExp (TInfixP l n r t) =
+    TInfixE (Just . tPat2TExp $ l)
+            (TConE n $ mkArrowT [typeOf l, typeOf r, t])
+            (Just . tPat2TExp $ r)            
+            t 
+tPat2TExp (TListP l t) = TListE (map tPat2TExp l) t
+tPat2TExp (TTupP ps t) = TTupE  (map tPat2TExp ps) t
+--tPat2TExp p = error $ "Syntax.IFTemplateHaskell.tPat2TExp: Pattern " ++ show p ++
+--                  " cannot be transformed into an Expression!" 
+
+hypos2decs :: [[(Name,Rules)]] -> [[Dec]]
+hypos2decs hs =  map rules2decs hs
+
+rules2decs :: [(Name,Rules)] -> [Dec]
+rules2decs = map rules2dec
+
+rules2dec :: (Name,Rules) -> Dec
+rules2dec (n,rs) = FunD n (rules2clauses rs)
+
+rules2clauses :: Rules -> [Clause]
+rules2clauses rs = map rule2clause (S.toList rs)
+     
+rule2clause :: Rule -> Clause
+rule2clause r = Clause ((map fromTPat) $ lhs r) (NormalB . fromTExp . rhs $ r) [] 
+            
hunk ./src/Logging/PrettyPrinter.hs 4
-    printResult, 
+    --printResult, 
hunk ./src/Logging/PrettyPrinter.hs 18
-import Data.Time.Clock
-import Data.Time.Calendar
-import System.CPUTime
-import System.IO
-import System.Mem
+--import Data.Time.Clock
+--import Data.Time.Calendar
+--import System.CPUTime
+--import System.IO
+--import System.Mem
hunk ./src/Logging/PrettyPrinter.hs 29
-
-date :: IO (Integer,Int,Int,Integer) -- :: (year,month,day,CPUTime)
-date = do
-       (y,m,d) <- getCurrentTime >>= return . toGregorian . utctDay
-       s       <- getCPUTime
-       return (y,m,d,s)
-
-showDate = date >>= \(y,m,d,s) ->
-             return $ (shows y) . (shows m). (shows d) $ show s
-
-printResult :: (Either String [[Dec]],Log) -> IO()
-printResult (r,l) = do 
-    file    <- showDate >>= \d -> return ("log/" ++ d ++ ".log")
-    fhandle <-openFile file AppendMode
-    printLog l  [fhandle,stdout]
-    case r of
-        Left  e -> mapM_ ((flip hPutStr)  ("UNCAUGHT ERROR: " ++ e)) [fhandle,stdout]
-        Right r -> printDecs r [fhandle,stdout]
-    hClose fhandle
-    
-                
-printLog :: Log -> [Handle] -> IO ()
-printLog logs handles =  mapM_ (flip hPutDoc content) handles
-    where    
-    content = frame "Log Log Log Log Log Log Log" <$> pretty logs
-
-printDecs :: [[Dec]] -> [Handle] -> IO()
-printDecs decs handles = do
-    let hyponum = length decs
-    docs <- liftM vcat $ mapM (printInQ  hyponum) (zip decs [1..])
-    let content = frame "Results Results Results" <$$> docs
-    mapM_ ((flip hPutDoc) content) handles
-
-printInQ :: Int -> ([Dec],Int) -> IO Doc    
-printInQ = \j (d,i) -> (runQ.return) d >>= \p -> 
-                return $ indent 6 (text "- - - - - HYPOTHESE" <+> int i <+> 
-                                   text "of" <+> int j <+> text "- - - - -") <$$>
-                         linebreak <> 
-                         vcat (map pretty p) <>
-                         linebreak 
-                         
-frame s = vsep [line,header s,line,softline]
-    where
-    line     = (text "*") <+>
-               hsep (replicate (colwidth -2) (text "-")) <+>
-               text  "*"
-    spaces   = ((colwidth) - (length s)) `div` 2 
-    colwidth =  72
-    header s = (text "|") <+> hsep (replicate spaces space) <+>
-               text s <+> hsep (replicate spaces space) <+> (text "|")    
+--
+--date :: IO (Integer,Int,Int,Integer) -- :: (year,month,day,CPUTime)
+--date = do
+--       (y,m,d) <- getCurrentTime >>= return . toGregorian . utctDay
+--       s       <- getCPUTime
+--       return (y,m,d,s)
+--
+--showDate = date >>= \(y,m,d,s) ->
+--             return $ (shows y) . (shows m). (shows d) $ show s
+--
+--printResult :: (Either String [[Dec]],Log) -> IO()
+--printResult (r,l) = do 
+--    file    <- showDate >>= \d -> return ("log/" ++ d ++ ".log")
+--    fhandle <- openFile file AppendMode
+--    printLog l  [fhandle,stdout]
+--    case r of
+--        Left  e -> mapM_ ((flip hPutStr)  ("UNCAUGHT ERROR: " ++ e)) [fhandle,stdout]
+--        Right r -> printDecs r [fhandle,stdout]
+--    hClose fhandle
+--    
+--                
+--printLog :: Log -> [Handle] -> IO ()
+--printLog logs handles =  mapM_ (flip hPutDoc content) handles
+--    where    
+--    content = frame "Log Log Log Log Log Log Log" <$> pretty logs
+--
+--printDecs :: [[Dec]] -> [Handle] -> IO()
+--printDecs decs handles = do
+--    let hyponum = length decs
+--    docs <- liftM vcat $ mapM (printInQ  hyponum) (zip decs [1..])
+--    let content = frame "Results Results Results" <$$> docs
+--    mapM_ ((flip hPutDoc) content) handles
+--
+--printInQ :: Int -> ([Dec],Int) -> IO Doc    
+--printInQ = \j (d,i) -> (runQ.return) d >>= \p -> 
+--                return $ indent 6 (text "- - - - - HYPOTHESE" <+> int i <+> 
+--                                   text "of" <+> int j <+> text "- - - - -") <$$>
+--                         linebreak <> 
+--                         vcat (map pretty p) <>
+--                         linebreak 
+--                         
+--frame s = vsep [line,header s,line,softline]
+--    where
+--    line     = (text "*") <+>
+--               hsep (replicate (colwidth -2) (text "-")) <+>
+--               text  "*"
+--    spaces   = ((colwidth) - (length s)) `div` 2 
+--    colwidth =  72
+--    header s = (text "|") <+> hsep (replicate spaces space) <+>
+--               text s <+> hsep (replicate spaces space) <+> (text "|")    
hunk ./src/Main.hs 11
-import Data.Initialiser 
+--import Data.Initialiser 
hunk ./src/Main.hs 312
-igortest = startSynthesis revdef [d||]
+--igortest = startSynthesis revdef [d||]
hunk ./src/Main.hs 314
- 
+
hunk ./src/Syntax/Expressions.hs 534
+           
+fromTExp (TVarE n _)         = VarE n
+fromTExp (TLitE n _)         = LitE n
+fromTExp (TConE n _)         = ConE n
+fromTExp (TListE l _)        = ListE (map fromTExp l)
+fromTExp (TTupE l _)         = TupE (map fromTExp l)
+fromTExp (TAppE a1 a2 _)     = AppE (fromTExp a1) (fromTExp a2)                
+fromTExp (TInfixE e1 e2 e3 _) = 
+    InfixE (liftM fromTExp e1)(fromTExp e2)(liftM fromTExp e3)
hunk ./src/Syntax/Patterns.hs 111
-    --subterms (TConP _ pats _)    = pats
+    subterms (TConP _ pats _)    = pats
hunk ./src/Syntax/Patterns.hs 116
-    subterms    p                = 
-        error $ "Terms.subterms at TPat: Not implemented for Pattern " ++ (show p)
+--    subterms    p                = 
+--        error $ "Terms.subterms at TPat: Not implemented for Pattern " ++ (show p)
hunk ./src/Syntax/Patterns.hs 373
+
+    
+
+fromTPat (TVarP n _)   = VarP n
+fromTPat (TLitP n _)   = LitP n
+fromTPat (TTupP l _)   = TupP (map fromTPat l)
+fromTPat (TListP l _)  = ListP (map fromTPat l)
+fromTPat (TConP n l _) = ConP n (map fromTPat l)
+fromTPat (TInfixP l n r _) =
+    InfixP (fromTPat l) n (fromTPat r)
+
+
hunk ./src/Syntax/Terms.hs 17
-    mapGetPos, pat2Call, applyAtIndex,
+    mapGetPos, applyAtIndex,
hunk ./src/Syntax/Terms.hs 19
-    isTuple, isNil, isCons,
-    pat2Exp,
-    module Syntax.IFTemplateHaskell
+    isTuple, isNil, isCons
hunk ./src/Syntax/Terms.hs 241
-pat2Call :: Name ->[Pat] -> Exp
-pat2Call n ps = foldl1 AppE $ (ConE n):(map pat2Exp ps)    
-    
-pat2Exp :: Pat -> Exp
-pat2Exp (VarP i) = (VarE i)
-pat2Exp (LitP l) = (LitE l) 
-pat2Exp (ConP n ps) = foldl1 AppE $ (ConE n):(map pat2Exp ps)
-pat2Exp (InfixP l n r) = flip InfixE (ConE n) (Just . pat2Exp $ l)(Just . pat2Exp $ r) 
-pat2Exp (ListP l) = ListE $ map pat2Exp l
-pat2Exp (TupP ps) = ListE $ map pat2Exp ps
-pat2Exp p = error $ "Terms.class.pat2Exp: Pattern " ++ show p ++
-                  " cannot be transformed into an Expression!" 
hunk ./src/SynthesisEngine.hs 8
+import Data.Rules (hypos2decs)
hunk ./src/SynthesisEngine.hs 14
-import Data.Initialiser
+--import Data.Initialiser
hunk ./src/SynthesisEngine.hs 28
--}
-startSynthesis :: Q [Dec] -> Q [Dec] -> IO()
-startSynthesis a b = runQ $
-    do tgt <- a
-       bgk <- b  
-       runIO $ printResult $ (runLM  (synthesise tgt bgk)) 
+-} 
hunk ./src/SynthesisEngine.hs 30
+startSynthesis :: [(Name,Rules)] -> [(Name,Rules)] -> (Either String [[Dec]],Log)
+startSynthesis tgt bgk = runLM  (synthesise tgt bgk) 
hunk ./src/SynthesisEngine.hs 33
-synthesise :: [Dec] -> [Dec] -> LM [[Dec]]
-synthesise tgtsQ bgksQ = do
-    let tgts     =  decs2rules tgtsQ --  [(Name,Rules)]
-    let bgks     =  decs2rules bgksQ
+synthesise :: [(Name,Rules)] -> [(Name,Rules)] -> LM [[Dec]]
+synthesise tgts bgks = do
hunk ./src/SynthesisEngine.hs 38
-    result       <- (runIM ( synthesiseTargets tnms) igordata) 
+    result <- runIM ( synthesiseTargets tnms) igordata 
hunk ./src/SynthesisEngine.hs 40
-      
+
+-- WAS
+--startSynthesis :: Q [Dec] -> Q [Dec] -> IO()
+--startSynthesis a b = runQ $
+--    do tgt <- a
+--       bgk <- b  
+--       runIO $ printResult $ (runLM  (synthesise tgt bgk)) 
+--
+--synthesise :: [Dec] -> [Dec] -> LM [[Dec]]
+--synthesise tgtsQ bgksQ = do
+--    let tgts     =  decs2rules tgtsQ --  [(Name,Rules)]
+--    let bgks     =  decs2rules bgksQ
+--    let tnms     =  (map fst) tgts
+--    let allrs    =  (++) tgts bgks 
+--    let igordata = initIgor allrs
+--    result       <- (runIM ( synthesiseTargets tnms) igordata) 
+--    return $ hypos2decs result
+--       
hunk ./src/UI/UIStarter.hs 4
-import Text.ParserCombinators.Parsec
-import qualified Text.ParserCombinators.Parsec.Token as P
+import Text.ParserCombinators.Parsec hiding (space)
+import qualified Text.ParserCombinators.Parsec.Token as T
hunk ./src/UI/UIStarter.hs 12
+import System.CPUTime
+import System.IO
+import System.Mem
+
+import Data.Time.Clock
+import Data.Time.Calendar
hunk ./src/UI/UIStarter.hs 21
-import Logging hiding (integer)
hunk ./src/UI/UIStarter.hs 22
+import SynthesisEngine
+import Logging hiding (integer)
hunk ./src/UI/UIStarter.hs 113
+runCmd s (Generalise tgts bgks) = startIgor s tgts bgks
hunk ./src/UI/UIStarter.hs 135
-\  |   | ____  ___________| | |  ._       \n\
-\  |   |/ __ \\/  _ \\_  __ \\ | | _| |__ \n\ 
+\  |   | ____  ____ ._____| | |  ._       \n\
+\  |   |/ __ \\/  _ \\|  __ \\ | | _| |__ \n\ 
hunk ./src/UI/UIStarter.hs 190
-
+startIgor :: EnvState -> [Name] -> [Name] -> IO (Bool,EnvState)
+startIgor s tgts bgks = do
+    let exmpls = liftM2 (,) (getBindings tgts (context s))(getBindings tgts (context s))
+    case exmpls of
+        Left msg      -> putStrLn msg >> return (False, s)
+        Right (ts,bs) -> do
+           printResult $ startSynthesis ts bs
+           return (False, s)
+    
hunk ./src/UI/UIStarter.hs 208
+
+
+
+date :: IO (Integer,Int,Int,Integer) -- :: (year,month,day,CPUTime)
+date = do
+       (y,m,d) <- getCurrentTime >>= return . toGregorian . utctDay
+       s       <- getCPUTime
+       return (y,m,d,s)
+
+showDate = date >>= \(y,m,d,s) ->
+             return $ (shows y) . (shows m). (shows d) $ show s
+
+printResult :: (Either String [[Dec]],Log) -> IO()
+printResult (r,l) = do 
+    file    <- showDate >>= \d -> return ("log/" ++ d ++ ".log")
+    fhandle <- openFile file AppendMode
+    printLog l  [fhandle,stdout]
+    case r of
+        Left  e -> mapM_ ((flip hPutStr)  ("UNCAUGHT ERROR: " ++ e)) [fhandle,stdout]
+        Right r -> printDecs r [fhandle,stdout]
+    hClose fhandle
+    
+                
+printLog :: Log -> [Handle] -> IO ()
+printLog logs handles =  mapM_ (flip hPutDoc content) handles
+    where    
+    content = frame "Log Log Log Log Log Log Log" <$> pretty logs
+
+printDecs :: [[Dec]] -> [Handle] -> IO()
+printDecs decs handles = do
+    let hyponum = length decs
+    docs <- liftM vcat $ mapM (printInQ  hyponum) (zip decs [1..])
+    let content = frame "Results Results Results" <$$> docs
+    mapM_ ((flip hPutDoc) content) handles
+
+printInQ :: Int -> ([Dec],Int) -> IO Doc    
+printInQ = \j (d,i) -> (runQ.return) d >>= \p -> 
+                return $ indent 6 (text "- - - - - HYPOTHESE" <+> int i <+> 
+                                   text "of" <+> int j <+> text "- - - - -") <$$>
+                         linebreak <> 
+                         vcat (map pretty p) <>
+                         linebreak 
+                         
+frame s = vsep [line,header s,line,softline]
+    where
+    line     = (text "*") <+>
+               hsep (replicate (colwidth -2) (text "-")) <+>
+               text  "*"
+    spaces   = ((colwidth) - (length s)) `div` 2 
+    colwidth =  72
+    header s = (text "|") <+> hsep (replicate spaces space) <+>
+               text s <+> hsep (replicate spaces space) <+> (text "|")    
+
+
+
+
+
hunk ./src/UI/UIStarter.hs 278
+ | Generalise [Name] [Name]
hunk ./src/UI/UIStarter.hs 287
-    , (":batch \"path/to/file\"",       "Run a batch file",            stringLiteral >>= return . Batch)
-    , (":load \"path/to/file\"",        "Load a spec file into context.",             stringLiteral >>= return . Load)
+    , (":batch \"path/to/file\"",       "Run a batch file",             pString Batch)
+    , (":load \"path/to/file\"",        "Load a spec file into context.",             pString Load)
hunk ./src/UI/UIStarter.hs 291
+    , (":generalise \"tgts\" [with \"bgks\"]",                 "Start generalisation.",                  pStart)
hunk ./src/UI/UIStarter.hs 293
-    , (":yell \"something\"",           "Yell on command line.",        stringLiteral >>= return . Yell)
+    , (":yell \"something\"",           "Yell on command line.",        pString Yell)
hunk ./src/UI/UIStarter.hs 303
-getHelp (cmd, help, _) = cmd ++ replicate (25 - length cmd) ' ' ++ help
+getHelp (cmd, help, _) = cmd ++ replicate (35 - length cmd) ' ' ++ help
hunk ./src/UI/UIStarter.hs 322
-lexer :: P.TokenParser ()
-lexer = P.makeTokenParser
+lexer :: T.TokenParser ()
+lexer = T.makeTokenParser
hunk ./src/UI/UIStarter.hs 328
-         , reservedOpNames = [":",";","+","-","="]
+         , reservedOpNames = [":",";","+","-","=", "with"]
hunk ./src/UI/UIStarter.hs 332
-whiteSpace = P.whiteSpace lexer
---parens     = P.parens lexer
---semi       = P.semi lexer
---colon      = P.colon lexer
-semiSep1   = P.semiSep1 lexer
-reserved   = P.reserved lexer
-reservedOp = P.reservedOp lexer
-stringLiteral     = P.stringLiteral lexer
-integer     = P.integer lexer
+whiteSpace    = T.whiteSpace lexer
+--parens        = P.parens lexer
+--semi          = P.semi lexer
+--colon         = P.colon lexer
+semiSep1      = T.semiSep1 lexer
+reserved      = T.reserved lexer
+reservedOp    = T.reservedOp lexer
+stringLiteral = T.stringLiteral lexer
+integer       = T.integer lexer
hunk ./src/UI/UIStarter.hs 391
+pString :: (String -> Cmd) -> Parser Cmd
+pString c = stringLiteral >>= return . c
+
+pNames = liftM ((map mkName) .  words) $ stringLiteral
+
+pStart :: Parser Cmd
+pStart = do{ targets <- pNames
+           ; bgkldg  <- choice [ do{eof; return []}
+                               , do{reservedOp "with"; pNames}
+                               ]
+           ;return $ Generalise targets bgkldg
+           }
+     <?> " \"t1 t2 ...\" [with \"b1 b2 ...\"]"
+          