From 2f39933512a887e5d9d9947ce2049818e6efdc3d Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 19 Oct 2025 23:37:38 +0300 Subject: [PATCH] part of step eval --- escher.hs | 112 +++++++++++++++++++++++++++++++++++------------------- 1 file changed, 72 insertions(+), 40 deletions(-) diff --git a/escher.hs b/escher.hs index fbd00b7..a9245b1 100644 --- a/escher.hs +++ b/escher.hs @@ -1,12 +1,12 @@ -import Control.Monad (guard, liftM) +import Control.Monad (guard, liftM, when) import Control.Applicative -import Control.Monad.State +import Control.Monad.State as State import Data.Map (Map) -import Data.Set (Set, insert) -import Data.Set (delete) +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) data Value = BoolV Bool | IntV Int @@ -51,7 +51,7 @@ data Expr = Expr :&&: Expr -- Bool deriving (Read, Show, Eq, Ord) data Conf = Conf {confInput :: [Value], - confOracle :: [Value] -> Maybe Value, + confOracle :: Oracle, confProg :: Expr, confExamples :: [[Value]]} @@ -172,6 +172,8 @@ eval _ Hole = Error ------------ +type Oracle = [Value] -> Maybe Value + -- bipartite graph, root is Goal newtype Goal = Goal [Maybe Value] -- result or unimportant deriving (Read, Show, Eq, Ord) @@ -188,29 +190,12 @@ data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])], syntUnsolvedGoals :: Set Goal, syntResolvers :: [Resolver], syntExamples :: [[Value]], - syntOracle :: [Value] -> Maybe Value, + syntOracle :: Oracle, syntRoot :: Goal} type SyntState a = State Synt a ------------ -genSize0 :: [Expr] -genSize0 = undefined - --- size +1 -genSize1 :: [Expr] -> [Expr] -genSize1 = undefined - --- size +2 -genSize2 :: [Expr] -> [Expr] -genSize2 = undefined - --- size +3 -genSize3 :: [Expr] -> [Expr] -genSize3 = undefined - ------------- - --fill holes in expr with top-level holes fillHoles :: Expr -> [Expr] -> Expr fillHoles (Hole :&&: Hole) [left, right] = left :&&: right @@ -256,11 +241,14 @@ matchGoal (Goal goal) st expr = let examples = syntExamples st in matchValue _ Nothing = True matchValue _ _ = False +------ syntesis steps + -- generate next step of exprs, remove copies -forwardStep :: Expr -> [Expr] -> SyntState () +forwardStep :: Expr -> [Expr] -> SyntState Expr forwardStep comp args = do st <- get - put st { syntExprs = (fillHoles comp args, []) : syntExprs st} --- TODO: then calc results on examples, add new examples, remove duplicates + let expr = fillHoles comp args + put st { syntExprs = (expr, []) : syntExprs st} + return expr splitGoal :: Goal -> [Bool] -> Resolver splitGoal resolverGoal@(Goal outputs) selector | length outputs == length selector = @@ -288,21 +276,25 @@ resolveStep (ifCond, ifDoThen, ifDoElse) r = do st <- get syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st, syntExprs = (expr, []) : syntExprs st } +remakeSynt :: [[Value]] -> [Value] -> SyntState () +remakeSynt newInputs newOutputs = do st <- get + let Goal oldOutputs = syntRoot st + let goals = zip (newInputs ++ syntExamples st) + (newOutputs ++ map (fromMaybe undefined) oldOutputs) + initSynt (syntOracle st) goals + modify (\st' -> st' { syntExprs = syntExprs st }) + -- clear goal tree up to root, add example, calculate exprs on input (could be recursive ?) -saturateStep :: Expr -> SyntState () +saturateStep :: Expr -> SyntState Bool saturateStep expr = do st <- get - let (exs, vals) = unzip $ foldl (searchNewExample st) [] (syntExamples st) - let Goal oldRoot = syntRoot st - let newRoot = Goal $ map Just vals ++ oldRoot - put st { syntExamples = exs ++ syntExamples st, - syntSolvedGoals = Map.empty, - syntUnsolvedGoals = Set.singleton newRoot, - syntResolvers = [], - syntRoot = newRoot} - where searchNewExample st [] input = case eval (confBySynt input expr st) expr of + let (newInputs, newOutputs) = unzip $ foldl (searchEx st) [] (syntExamples st) + let isExFound = null newInputs + when isExFound $ remakeSynt newInputs newOutputs + return isExFound + where searchEx st [] input = case eval (confBySynt input expr st) expr of NewExamples exs -> exs _ -> [] - searchNewExample _ exs _ = exs + searchEx _ exs _ = exs -- try to find terminating expr terminateStep :: Expr -> SyntState (Maybe Expr) @@ -310,9 +302,8 @@ terminateStep expr = do st <- get return $ if matchGoal (syntRoot st) st expr then Just expr else Nothing ------- +------ patterns --- TODO: with holes ? patterns0 :: [Expr] patterns0 = [ZeroE, EmptyListE] @@ -337,6 +328,8 @@ patterns3 :: [Expr] patterns3 = [CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole}, IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}] +------ generation + concatShuffle :: [[a]] -> [a] concatShuffle xxs = let xxs' = filter (not . null) xxs in if null xxs' then [] else @@ -349,7 +342,7 @@ genNext1 = head -- 1 2 3 ... (n - 1) + (n - 1) ... 1 -> n, +1 for top expression genNext2 :: [[Expr]] -> [(Expr, Expr)] genNext2 exprs = let len = length exprs in - let exprs' = tail exprs in + let exprs' = tail exprs in concatShuffle $ zipWith (\xs ys -> ([(x, y) | x <- xs, y <- ys])) exprs' $ reverse exprs' @@ -368,3 +361,42 @@ genStep [] = map (, []) patterns0 genStep xs = concatShuffle [[(p, [x]) | p <- patterns1, x <- genNext1 xs], [(p, [x, y]) | p <- patterns2, (x, y) <- genNext2 xs], [(p, [x, y, z]) | p <- patterns3, (x, y, z) <- genNext3 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} + +-- 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 + +-- TODO +-- 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 + +-- TODO: examples