From 372d38d8134b7cd8394393c2450647d7f1c0022b Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 21 Oct 2025 14:33:00 +0300 Subject: [PATCH] most of syntestis step & utils --- escher.hs | 116 +++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 88 insertions(+), 28 deletions(-) diff --git a/escher.hs b/escher.hs index a9245b1..f2962ae 100644 --- a/escher.hs +++ b/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,39 +390,73 @@ genStep xs = concatShuffle [[(p, [x]) | p <- patterns1, x <- genNext1 xs], ------ algorithm -initSynt :: Oracle -> [([Value], Value)] -> SyntState () -initSynt oracle goals = let root = Goal $ map (Just . snd) goals in - put Synt { syntExprs = [], - syntSolvedGoals = Map.empty, - syntUnsolvedGoals = Set.singleton root, - syntResolvers = [], - syntExamples = map fst goals, - syntOracle = oracle, - syntRoot = root} +createSynt :: Oracle -> [([Value], Value)] -> Synt +createSynt oracle goals = let root = Goal $ map (Just . snd) goals in + Synt { syntExprs = [], + syntSolvedGoals = Map.empty, + syntUnsolvedGoals = Set.singleton root, + syntResolvers = [], + syntExamples = map fst goals, + syntOracle = oracle, + syntRoot = root} + +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 --- TODO stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr) stepOnNewExpr comp args = do st <- get expr <- forwardStep comp args - exFound <- saturateStep 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 + stepOnAddedExpr expr --- TODO +-- stages: -- init state -- 1. gen new step exprs -- 2. process exprs by one --- 3. try solve goals, try terminate / saturate --- 4. make resolutions if goals solved --- 5. split goals, where expr partially matched -syntesis :: Int -> Oracle -> [[Value]] -> Expr -syntesis steps oracle examples = undefined +-- 3. try terminate / saturate +-- 4. try to solve existing goals +-- 5. make resolutions if goals solved +-- 6. split goals, where expr partially matched +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