most of syntestis step & utils

escher.hs

@@ -1,4 +1,4 @@
-import Control.Monad (guard, liftM, when)
+import Control.Monad (guard, liftM, when, foldM)
 import Control.Applicative
 import Control.Monad.State as State
 import Data.Map (Map)
@@ -6,7 +6,7 @@ import Data.Set (Set, insert, delete)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Data.List (inits)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust)
 
 data Value = BoolV Bool
            | IntV Int
@@ -267,7 +267,23 @@ splitGoalStep goal selector = do st <- get
                                                               syntUnsolvedGoals st,
                                           syntResolvers = r : syntResolvers st }
 
+-- TODO: use expr evaluated outputs ?
+trySolveGoal :: Goal -> Expr -> SyntState Bool
+trySolveGoal goal expr = do st <- get
+                            if matchGoal goal st expr then do
+                              put st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st,
+                                       syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st }
+                              return True
+                            else return False
+
+isGoalSolved :: Goal -> SyntState Bool
+isGoalSolved goal = gets (Map.member goal . syntSolvedGoals)
+
+goalSolution :: Goal -> SyntState (Maybe Expr)
+goalSolution goal = gets (Map.lookup goal . syntSolvedGoals)
+
 -- find all goals solved by new expr, by expr id it's values on examples, remove solved goals
+-- NOTE: goals expected to be resolved
 resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState ()
 resolveStep (ifCond, ifDoThen, ifDoElse) r = do st <- get
                                                 let expr = IfE { ifCond, ifDoThen, ifDoElse }
@@ -276,6 +292,16 @@ resolveStep (ifCond, ifDoThen, ifDoElse) r = do st <- get
                                                          syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st,
                                                          syntExprs = (expr, []) : syntExprs st }
 
+tryResolve :: Resolver -> SyntState Bool
+tryResolve r = do condSol <- goalSolution $ resolverCond r
+                  thenSol <- goalSolution $ resolverThen r
+                  elseSol <- goalSolution $ resolverElse r
+                  case (condSol, thenSol, elseSol) of
+                    (Just condExpr, Just thenExpr, Just elseExpr) -> do
+                      resolveStep (condExpr, thenExpr, elseExpr) r
+                      return True
+                    _ -> return False
+
 remakeSynt :: [[Value]] -> [Value] -> SyntState ()
 remakeSynt newInputs newOutputs = do st <- get
                                      let Goal oldOutputs = syntRoot st
@@ -364,9 +390,9 @@ genStep xs = concatShuffle [[(p, [x]) | p <- patterns1, x <- genNext1 xs],
 
 ------ algorithm
 
-initSynt :: Oracle -> [([Value], Value)] -> SyntState ()
+createSynt :: Oracle -> [([Value], Value)] -> Synt
-initSynt oracle goals = let root = Goal $ map (Just . snd) goals in
+createSynt oracle goals = let root = Goal $ map (Just . snd) goals in
-                        put Synt { syntExprs = [],
+                          Synt { syntExprs = [],
                                  syntSolvedGoals = Map.empty,
                                  syntUnsolvedGoals = Set.singleton root,
                                  syntResolvers = [],
@@ -374,29 +400,63 @@ initSynt oracle goals = let root = Goal $ map (Just . snd) goals in
                                  syntOracle = oracle,
                                  syntRoot = root}
 
--- TODO
+initSynt :: Oracle -> [([Value], Value)] -> SyntState ()
+initSynt oracle goals = put $ createSynt oracle goals
+
+stepOnAddedExpr :: Expr -> SyntState (Maybe Expr)
+stepOnAddedExpr expr = do exFound <- saturateStep expr
+                          st <- get
+                          if exFound then stepOnAddedExprs $ map fst $ syntExprs st else do -- redo prev exprs (including current)
+                             maybeResult <- terminateStep expr
+                             if isJust maybeResult then return maybeResult else do
+                               let exprOutputs = map (\input -> eval (confBySynt input expr st) expr) $ syntExamples st
+                               -- TODO: solve existing goals
+                               -- TODO: resolve existing goals
+                               put $ foldl (splitGoalsFold exprOutputs) st $ Set.toList $ syntUnsolvedGoals st
+                               return Nothing
+  where splitGoalsFold outputs st goal@(Goal expected) = let matches = zipWith matchResult outputs expected in
+                                                             if not $ or matches then st else
+                                                             execState (splitGoalStep goal matches) st
+        matchResult (NewExamples {}) _ = False
+        matchResult _ Nothing = True
+        matchResult (Result x) (Just y) = x == y
+
+stepOnAddedExprs :: [Expr] -> SyntState (Maybe Expr)
+stepOnAddedExprs = foldM step Nothing
+  where step :: Maybe Expr -> Expr -> SyntState (Maybe Expr)
+        step res@(Just {}) _ = return res
+        step Nothing expr = stepOnAddedExpr expr
+
 stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr)
 stepOnNewExpr comp args = do st <- get
                              expr <- forwardStep comp args
-                             exFound <- saturateStep expr
+                             stepOnAddedExpr expr
-                             -- TODO: redo prev exprs, etc. on found example
-                             maybeResult <- terminateStep expr
-                             -- TODO: terminate if result found (?) <- fideb by lazy eval (?)
-                             put $ foldl splitGoalsFold st $ Set.toList $ syntUnsolvedGoals st
-                             -- TODO: resolve goals
-                             return maybeResult
-    where splitGoalsFold st goal = let matches = [True] in -- TODO
-                                   if not $ or matches then st else
-                                   execState (splitGoalStep goal matches) st
 
--- TODO
+-- stages:
 -- init state
 -- 1. gen new step exprs
 -- 2. process exprs by one
--- 3. try solve goals, try terminate / saturate
+-- 3. try terminate / saturate
--- 4. make resolutions if goals solved
+-- 4. try to solve existing goals
--- 5. split goals, where expr partially matched
+-- 5. make resolutions if goals solved
-syntesis :: Int -> Oracle -> [[Value]] -> Expr
+-- 6. split goals, where expr partially matched
-syntesis steps oracle examples = undefined
+syntesisStep :: Int -> [[Expr]] -> SyntState (Maybe Expr)
+syntesisStep 0 _ = return Nothing
+syntesisStep steps prevExprs = -- oracle should be defined on the providid examples
+                               do let currentExprs = genStep prevExprs
+                                  result <- foldM step Nothing currentExprs
+                                  if isJust result
+                                  then return result
+                                  else syntesisStep (steps - 1) (map (uncurry fillHoles) currentExprs : prevExprs)
+  where step res@(Just {}) _ = return res
+        step Nothing expr = uncurry stepOnNewExpr expr
+
+syntesis' :: [[Expr]] -> Int -> Oracle -> [[Value]] -> Maybe Expr
+syntesis' exprs steps oracle inputs = -- oracle should be defined on the providid examples
+                                      let outputs = map (fromMaybe undefined . oracle) inputs in
+                                      evalState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs)
+
+syntesis :: Int -> Oracle -> [[Value]] -> Maybe Expr
+syntesis = syntesis' []
 
 -- TODO: examples