From 75dafdab5eedbc2e5372e9f9f6872f52304618f9 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Tue, 18 Nov 2025 16:27:05 +0300 Subject: [PATCH] new saturate step archetecture: call saturate only at the end, speedup --- escher/Eval.hs | 7 ++-- escher/Main.hs | 100 +++++++++++++++++++++++++++++---------------- escher/Syntesis.hs | 9 ++-- 3 files changed, 73 insertions(+), 43 deletions(-) diff --git a/escher/Eval.hs b/escher/Eval.hs index 3d7a646..647e1d8 100644 --- a/escher/Eval.hs +++ b/escher/Eval.hs @@ -14,7 +14,8 @@ data Oracle = Oracle { oracleTypes :: TypeConf, data Conf = Conf {confInput :: [Value], confOracle :: Oracle, - confExamples :: [[Value]]} + confExamples :: [[Value]], + confTryFindExamples :: Bool} -- TODO: check structuralLess :: Value -> Value -> Bool @@ -100,9 +101,9 @@ eval conf (SelfE es) = do recInput <- foldM (\es e -> consValsM es (eval conf e) then RecError $ "self call on >= exprs, new=" ++ show recInput ++ " old=" ++ show (confInput conf) else do case (oracleFunc $ confOracle conf) recInput of - Just recOutput -> if recInput `elem` confExamples conf + Just recOutput -> if recInput `elem` confExamples conf || not (confTryFindExamples conf) -- TODO: better way then return recOutput - else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)] + else NewExamples $ trace ("New example: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)] Nothing -> FatalError $ "no oracle output on " ++ show recInput where consValsM :: [Value] -> Result Value -> Result [Value] consValsM vs (Result v) = Result $ v : vs diff --git a/escher/Main.hs b/escher/Main.hs index 347fba4..8cab43b 100644 --- a/escher/Main.hs +++ b/escher/Main.hs @@ -14,16 +14,22 @@ import Data.Maybe (fromMaybe, isJust, maybeToList, isNothing) import Debug.Trace (trace) import TypeCheck +import qualified Data.List as List syntEval :: [Value] -> Expr -> SyntState (Result Value) syntEval input expr = do cache <- gets syntCache - conf <- gets $ confBySynt input expr + conf <- gets $ confBySynt input expr False return $ eval conf expr +syntEvalEx :: [Value] -> Expr -> SyntState (Result Value) +syntEvalEx input expr = do cache <- gets syntCache + conf <- gets $ confBySynt input expr True + return $ eval conf expr + syntCacheEval :: [Value] -> Expr -> SyntState (Result Value) syntCacheEval input expr = do cache <- gets syntCache - conf <- gets $ confBySynt input expr + conf <- gets $ confBySynt input expr False let (result, cache') = cachedEval cache conf expr modify $ \st -> st {syntCache = cache'} return result @@ -44,7 +50,7 @@ matchGoal (Goal goal) expr = do examples <- gets syntExamples calcExprOutputs :: Expr -> SyntState [Result Value] calcExprOutputs expr = do examples <- gets syntExamples - mapM (`syntEval` expr) examples + mapM (`syntEval` expr) examples -- OR: syntCacheEval (slower?) calcTemporaryExprOutputs :: Expr -> SyntState [Result Value] calcTemporaryExprOutputs expr = do examples <- gets syntExamples @@ -88,7 +94,10 @@ splitGoal resolverGoal@(Goal outputs) selector | length outputs == length select splitGoalStep :: Goal -> [Bool] -> SyntState Resolver splitGoalStep goal selector = do let r = splitGoal goal selector resolvers <- gets syntResolvers - unless (r `elem` resolvers) $ -- do not add existing resolvers -- do not add existing resolvers + unless (r `elem` resolvers) $ -- do not add existing resolvers -- do not add existing resolvers -- do not add existing resolvers -- do not add existing resolvers + -- do not add existing resolvers + -- do not add existing resolvers + -- do not add existing resolvers -- do not add existing resolvers -- do not add existing resolvers modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $ Set.insert (resolverThen r) $ @@ -153,38 +162,54 @@ saturateStep expr = do examples <- gets syntExamples let exFound = not . null $ newInputs when exFound $ remakeSynt newInputs newOutputs return newInputs - where searchEx [] input = do output <- syntEval input expr - return $ case output of - NewExamples exs -> exs - _ -> [] - searchEx exs _ = return exs + where searchEx prevExs input = do output <- syntEvalEx input expr + return $ List.union prevExs $ case output of -- union ?? + NewExamples exs -> exs + _ -> [] -- try to find terminating expr -terminateStep :: Expr -> SyntState (Maybe Expr) -terminateStep expr = do rootGoal <- gets syntRoot - gets $ Map.lookup rootGoal . syntSolvedGoals - -- NOTE: Goal should be already solved earlier - -- doesMatch <- matchGoal rootGoal expr - -- return $ if doesMatch then Just expr else Nothing +terminateStep :: SyntState (Maybe Expr) +terminateStep = do rootGoal <- gets syntRoot + -- TODO: move try solve goal there ?? + gets $ Map.lookup rootGoal . syntSolvedGoals + -- NOTE: Goal should be already solved earlier + -- doesMatch <- matchGoal rootGoal expr + -- return $ if doesMatch then Just expr else Nothing + +-- TODO: FIXME +tryTerminate :: Expr -> SyntState (Maybe Expr) +tryTerminate expr = do maybeResult <- terminateStep + if isJust maybeResult + then do + newEx <- saturateStep expr + if not . null $ newEx + then do + -- redo prev exprs (including current) + st <- get + trace ("Reboot on new examples: " ++ show newEx) $ + stepOnAddedExprs $ map fst $ syntExprs st + else return maybeResult + else return Nothing stepOnAddedExpr :: Expr -> SyntState (Maybe Expr) -stepOnAddedExpr expr = do newEx <- saturateStep expr - if not . null $ newEx then do -- redo prev exprs (including current) - st <- get - -- trace ("exFound: " ++ show newEx) $ -- TMP: trace - stepOnAddedExprs $ map fst $ syntExprs st - else do -- try resolve goals & resolvers, generate new resolvers - maybeResult <- terminateStep expr - if isJust maybeResult then return maybeResult else do - exprOutputs <- calcExprOutputs expr - -- NOTE: now done in fowardStep - -- when (foldl (compareExprOutputs exprOutputs) True $ map fst $ syntExprs st) $ modify $ \st -> st { syntExprs = tail $ syntExprs st } - unsolvedGoals <- gets syntUnsolvedGoals - foldM_ (const $ trySolveGoal expr) False unsolvedGoals -- solve existing goals - resolvers <- gets syntResolvers - foldM_ (const tryResolve) Nothing resolvers -- resolve existing goals - modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st [syntRoot st] -- TODO: use Set.toList $ syntUnsolvedGoals st ? - gets $ \st -> syntRoot st `Map.lookup` syntSolvedGoals st +stepOnAddedExpr expr = do rootGoal <- gets syntRoot + trySolveGoal expr rootGoal + maybeResult <- tryTerminate expr + if isJust maybeResult + then return maybeResult + else do + -- try resolve goals & resolvers, generate new resolvers + exprOutputs <- calcExprOutputs expr + -- NOTE: now done in fowardStep + -- when (foldl (compareExprOutputs exprOutputs) True $ map fst $ syntExprs st) $ modify $ \st -> st { syntExprs = tail $ syntExprs st } + unsolvedGoals <- gets syntUnsolvedGoals + foldM_ (const $ trySolveGoal expr) False unsolvedGoals -- solve existing goals + resolvers <- gets syntResolvers + foldM_ (const tryResolve) Nothing resolvers -- resolve existing goals + modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st [syntRoot st] -- TODO: use Set.toList $ syntUnsolvedGoals st ? + tryTerminate expr + -- NOTE: replaced by tryTerminate + -- gets $ \st -> syntRoot st `Map.lookup` syntSolvedGoals st where splitGoalsFold expr outputs st goal@(Goal expected) = let matches = zipWith matchResult outputs expected in if not $ any (fromMaybe False) matches then st else let matchesBool = map (fromMaybe True) matches in @@ -253,7 +278,7 @@ mainExamples = [[ListV [IntV 1, IntV 2, IntV 3]]] allExamples :: [[Value]] -- allExamples = [[ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]] -allExamples = [[ListV [IntV 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]] +allExamples = [[ListV [IntV 0, IntV 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]] listOracleOf :: OracleFunc -> Type -> Oracle listOracleOf f t = Oracle { oracleTypes = TypeConf { typeConfInput = [ListT IntT], @@ -275,7 +300,8 @@ reverseExpr = IfE { ifCond = IsEmptyE (InputE 0), reverseConf :: Conf reverseConf = Conf { confInput = head allExamples, confOracle = listOracleOf reverseOracle $ ListT IntT, - confExamples = allExamples } + confExamples = allExamples, + confTryFindExamples = True } --- stutter @@ -293,7 +319,8 @@ stutterExpr = IfE { ifCond = IsEmptyE (InputE 0), stutterConf :: Conf stutterConf = Conf { confInput = head allExamples, confOracle = listOracleOf stutterOracle $ ListT IntT, - confExamples = allExamples } + confExamples = allExamples, + confTryFindExamples = True } --- length @@ -309,7 +336,8 @@ lengthExpr = IfE { ifCond = IsEmptyE (InputE 0), lengthConf :: Conf lengthConf = Conf { confInput = head allExamples, confOracle = listOracleOf lengthOracle IntT, - confExamples = allExamples } + confExamples = allExamples, + confTryFindExamples = True } --- diff --git a/escher/Syntesis.hs b/escher/Syntesis.hs index 98f73e8..85b4f73 100644 --- a/escher/Syntesis.hs +++ b/escher/Syntesis.hs @@ -66,10 +66,11 @@ fillHoles (SelfE hs) es | all (== Hole) hs && length hs == length es = SelfE es fillHoles (InputE i) [] = InputE i fillHoles e es = error $ "Can't fill holes in " ++ show e ++ " with " ++ show es -confBySynt :: [Value] -> Expr -> Synt -> Conf -confBySynt input expr st = Conf {confInput = input, - confOracle = syntOracle st, - confExamples = syntExamples st} +confBySynt :: [Value] -> Expr -> Bool -> Synt -> Conf +confBySynt input expr newEx st = Conf {confInput = input, + confOracle = syntOracle st, + confExamples = syntExamples st, + confTryFindExamples = newEx} ------ patterns