st/prog_synthesis
1
0
Fork 0
mirror of https://codeberg.org/ProgramSnail/prog_synthesis.git synced 2025-12-06 05:28:42 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

new saturate step archetecture: call saturate only at the end, speedup

Browse source
This commit is contained in:
ProgramSnail 2025-11-18 16:27:05 +03:00
parent 15cbf78ed5
commit 75dafdab5e
3 changed files with 73 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

7
escher/Eval.hs
View file

@ -14,7 +14,8 @@ data Oracle = Oracle { oracleTypes :: TypeConf,
data Conf = Conf {confInput :: [Value], data Conf = Conf {confInput :: [Value],
confOracle :: Oracle, confOracle :: Oracle,
confExamples :: [[Value]]} confExamples :: [[Value]],
confTryFindExamples :: Bool}
-- TODO: check -- TODO: check
structuralLess :: Value -> Value -> Bool 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) then RecError $ "self call on >= exprs, new=" ++ show recInput ++ " old=" ++ show (confInput conf)
else do else do
case (oracleFunc $ confOracle conf) recInput of 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 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 Nothing -> FatalError $ "no oracle output on " ++ show recInput
where consValsM :: [Value] -> Result Value -> Result [Value] where consValsM :: [Value] -> Result Value -> Result [Value]
consValsM vs (Result v) = Result $ v : vs consValsM vs (Result v) = Result $ v : vs

100
escher/Main.hs
View file

@ -14,16 +14,22 @@ import Data.Maybe (fromMaybe, isJust, maybeToList, isNothing)
import Debug.Trace (trace) import Debug.Trace (trace)
import TypeCheck import TypeCheck
import qualified Data.List as List
syntEval :: [Value] -> Expr -> SyntState (Result Value) syntEval :: [Value] -> Expr -> SyntState (Result Value)
syntEval input expr = do cache <- gets syntCache syntEval input expr = do cache <- gets syntCache
conf <- gets $ confBySynt input expr conf <- gets $ confBySynt input expr False
return $ eval conf expr 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 :: [Value] -> Expr -> SyntState (Result Value)
syntCacheEval input expr = do cache <- gets syntCache 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 let (result, cache') = cachedEval cache conf expr
modify $ \st -> st {syntCache = cache'} modify $ \st -> st {syntCache = cache'}
return result return result
@ -44,7 +50,7 @@ matchGoal (Goal goal) expr = do examples <- gets syntExamples
calcExprOutputs :: Expr -> SyntState [Result Value] calcExprOutputs :: Expr -> SyntState [Result Value]
calcExprOutputs expr = do examples <- gets syntExamples calcExprOutputs expr = do examples <- gets syntExamples
mapM (`syntEval` expr) examples mapM (`syntEval` expr) examples -- OR: syntCacheEval (slower?)
calcTemporaryExprOutputs :: Expr -> SyntState [Result Value] calcTemporaryExprOutputs :: Expr -> SyntState [Result Value]
calcTemporaryExprOutputs expr = do examples <- gets syntExamples 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 -> [Bool] -> SyntState Resolver
splitGoalStep goal selector = do let r = splitGoal goal selector splitGoalStep goal selector = do let r = splitGoal goal selector
resolvers <- gets syntResolvers 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 -- do not add existing resolvers
modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $ modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $
Set.insert (resolverThen r) $ Set.insert (resolverThen r) $
@ -153,38 +162,54 @@ saturateStep expr = do examples <- gets syntExamples
let exFound = not . null $ newInputs let exFound = not . null $ newInputs
when exFound $ remakeSynt newInputs newOutputs when exFound $ remakeSynt newInputs newOutputs
return newInputs return newInputs
where searchEx [] input = do output <- syntEval input expr where searchEx prevExs input = do output <- syntEvalEx input expr
return $ case output of return $ List.union prevExs $ case output of -- union ??
NewExamples exs -> exs NewExamples exs -> exs
_ -> [] _ -> []
searchEx exs _ = return exs
-- try to find terminating expr -- try to find terminating expr
terminateStep :: Expr -> SyntState (Maybe Expr) terminateStep :: SyntState (Maybe Expr)
terminateStep expr = do rootGoal <- gets syntRoot terminateStep = do rootGoal <- gets syntRoot
gets $ Map.lookup rootGoal . syntSolvedGoals -- TODO: move try solve goal there ??
-- NOTE: Goal should be already solved earlier gets $ Map.lookup rootGoal . syntSolvedGoals
-- doesMatch <- matchGoal rootGoal expr -- NOTE: Goal should be already solved earlier
-- return $ if doesMatch then Just expr else Nothing -- 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 -> SyntState (Maybe Expr)
stepOnAddedExpr expr = do newEx <- saturateStep expr stepOnAddedExpr expr = do rootGoal <- gets syntRoot
if not . null $ newEx then do -- redo prev exprs (including current) trySolveGoal expr rootGoal
st <- get maybeResult <- tryTerminate expr
-- trace ("exFound: " ++ show newEx) $ -- TMP: trace if isJust maybeResult
stepOnAddedExprs $ map fst $ syntExprs st then return maybeResult
else do -- try resolve goals & resolvers, generate new resolvers else do
maybeResult <- terminateStep expr -- try resolve goals & resolvers, generate new resolvers
if isJust maybeResult then return maybeResult else do exprOutputs <- calcExprOutputs expr
exprOutputs <- calcExprOutputs expr -- NOTE: now done in fowardStep
-- NOTE: now done in fowardStep -- when (foldl (compareExprOutputs exprOutputs) True $ map fst $ syntExprs st) $ modify $ \st -> st { syntExprs = tail $ syntExprs st }
-- when (foldl (compareExprOutputs exprOutputs) True $ map fst $ syntExprs st) $ modify $ \st -> st { syntExprs = tail $ syntExprs st } unsolvedGoals <- gets syntUnsolvedGoals
unsolvedGoals <- gets syntUnsolvedGoals foldM_ (const $ trySolveGoal expr) False unsolvedGoals -- solve existing goals
foldM_ (const $ trySolveGoal expr) False unsolvedGoals -- solve existing goals resolvers <- gets syntResolvers
resolvers <- gets syntResolvers foldM_ (const tryResolve) Nothing resolvers -- resolve existing goals
foldM_ (const tryResolve) Nothing resolvers -- resolve existing goals modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st [syntRoot st] -- TODO: use Set.toList $ syntUnsolvedGoals st ?
modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st [syntRoot st] -- TODO: use Set.toList $ syntUnsolvedGoals st ? tryTerminate expr
gets $ \st -> syntRoot st `Map.lookup` syntSolvedGoals st -- 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 where splitGoalsFold expr outputs st goal@(Goal expected) = let matches = zipWith matchResult outputs expected in
if not $ any (fromMaybe False) matches then st else if not $ any (fromMaybe False) matches then st else
let matchesBool = map (fromMaybe True) matches in let matchesBool = map (fromMaybe True) matches in
@ -253,7 +278,7 @@ mainExamples = [[ListV [IntV 1, IntV 2, IntV 3]]]
allExamples :: [[Value]] allExamples :: [[Value]]
-- allExamples = [[ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]] -- 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 :: OracleFunc -> Type -> Oracle
listOracleOf f t = Oracle { oracleTypes = TypeConf { typeConfInput = [ListT IntT], listOracleOf f t = Oracle { oracleTypes = TypeConf { typeConfInput = [ListT IntT],
@ -275,7 +300,8 @@ reverseExpr = IfE { ifCond = IsEmptyE (InputE 0),
reverseConf :: Conf reverseConf :: Conf
reverseConf = Conf { confInput = head allExamples, reverseConf = Conf { confInput = head allExamples,
confOracle = listOracleOf reverseOracle $ ListT IntT, confOracle = listOracleOf reverseOracle $ ListT IntT,
confExamples = allExamples } confExamples = allExamples,
confTryFindExamples = True }
--- stutter --- stutter
@ -293,7 +319,8 @@ stutterExpr = IfE { ifCond = IsEmptyE (InputE 0),
stutterConf :: Conf stutterConf :: Conf
stutterConf = Conf { confInput = head allExamples, stutterConf = Conf { confInput = head allExamples,
confOracle = listOracleOf stutterOracle $ ListT IntT, confOracle = listOracleOf stutterOracle $ ListT IntT,
confExamples = allExamples } confExamples = allExamples,
confTryFindExamples = True }
--- length --- length
@ -309,7 +336,8 @@ lengthExpr = IfE { ifCond = IsEmptyE (InputE 0),
lengthConf :: Conf lengthConf :: Conf
lengthConf = Conf { confInput = head allExamples, lengthConf = Conf { confInput = head allExamples,
confOracle = listOracleOf lengthOracle IntT, confOracle = listOracleOf lengthOracle IntT,
confExamples = allExamples } confExamples = allExamples,
confTryFindExamples = True }
--- ---

9
escher/Syntesis.hs
View file

@ -66,10 +66,11 @@ fillHoles (SelfE hs) es | all (== Hole) hs && length hs == length es = SelfE es
fillHoles (InputE i) [] = InputE i fillHoles (InputE i) [] = InputE i
fillHoles e es = error $ "Can't fill holes in " ++ show e ++ " with " ++ show es fillHoles e es = error $ "Can't fill holes in " ++ show e ++ " with " ++ show es
confBySynt :: [Value] -> Expr -> Synt -> Conf confBySynt :: [Value] -> Expr -> Bool -> Synt -> Conf
confBySynt input expr st = Conf {confInput = input, confBySynt input expr newEx st = Conf {confInput = input,
confOracle = syntOracle st, confOracle = syntOracle st,
confExamples = syntExamples st} confExamples = syntExamples st,
confTryFindExamples = newEx}
------ patterns ------ patterns