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

main, fixes, works for length & reverse (for int lists)

Browse source
This commit is contained in:
ProgramSnail 2025-10-27 01:47:15 +03:00
parent e8524a170f
commit 3fe524b5a0
1 changed files with 35 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

68
escher.hs
View file

@ -1,4 +1,6 @@
import Control.Monad (guard, liftM, when, foldM, foldM_) -- NOTE: it will be important to remove gets on caching addition
import Control.Monad (guard, liftM, when, unless, foldM, foldM_)
import Control.Applicative import Control.Applicative
import Control.Monad.State as State import Control.Monad.State as State
import Data.Map (Map) import Data.Map (Map)
@ -88,7 +90,7 @@ instance Monad Result where
return = pure return = pure
instance Alternative Result where instance Alternative Result where
empty = undefined -- TMP: no guards used -- FatalError "empty" -- TODO: fatal ? empty = undefined -- TMP: no guards used -- FatalError "empty" -- TODO: rec ?
RecError err <|> y = y RecError err <|> y = y
FatalError err <|> y = y FatalError err <|> y = y
NewExamples es <|> _ = NewExamples es NewExamples es <|> _ = NewExamples es
@ -140,8 +142,6 @@ structuralLess (ListV left) (ListV right) = length left < length right
structuralLess (TreeV left) (TreeV right) = treeHeight left < treeHeight right structuralLess (TreeV left) (TreeV right) = treeHeight left < treeHeight right
structuralLess _ _ = False structuralLess _ _ = False
-- TODO: exprSize ?
eval :: Conf -> Expr -> Result Value eval :: Conf -> Expr -> Result Value
eval conf (left :&&: right) = do BoolV leftB <- eval conf left eval conf (left :&&: right) = do BoolV leftB <- eval conf left
BoolV rightB <- eval conf right BoolV rightB <- eval conf right
@ -210,7 +210,7 @@ eval conf (SelfE e) = do ListV recInput <- eval conf e
-- guard $ length newInput == length (confInput conf) -- guard $ length newInput == length (confInput conf)
-- guard $ and $ zipWith structuralLess newInput (confInput conf) -- guard $ and $ zipWith structuralLess newInput (confInput conf)
if length recInput /= length (confInput conf) if length recInput /= length (confInput conf)
then RecError $ "self call different length, new=" ++ show recInput ++ " old=" ++ show (confInput conf) then FatalError $ "self call different length, new=" ++ show recInput ++ " old=" ++ show (confInput conf) -- TODO: fatal ?
else do else do
if not $ and $ zipWith structuralLess recInput (confInput conf) if not $ and $ zipWith structuralLess recInput (confInput conf)
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)
@ -218,11 +218,11 @@ eval conf (SelfE e) = do ListV recInput <- eval conf e
case confOracle conf recInput of case confOracle conf recInput of
Just recOutput -> if recInput `elem` confExamples conf Just recOutput -> if recInput `elem` confExamples conf
then return recOutput then return recOutput
else NewExamples [(recInput, recOutput)] else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)]
Nothing -> RecError $ "no oracle output on " ++ show recInput Nothing -> FatalError $ "no oracle output on " ++ show recInput
eval conf (InputE e) = do IntV i <- eval conf e eval conf (InputE e) = do IntV i <- eval conf e
if i < 0 || i >= length (confInput conf) -- NOTE: replaced guard for better errors description if i < 0 || i >= length (confInput conf) -- NOTE: replaced guard for better errors description
then FatalError $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i then FatalError $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i -- TODO: fatal ?
else return $ confInput conf !! i -- use !? instead (?) else return $ confInput conf !! i -- use !? instead (?)
eval _ Hole = FatalError "can't eval hole" eval _ Hole = FatalError "can't eval hole"
@ -245,7 +245,7 @@ data Resolver = Resolver { resolverGoal :: Goal,
data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])], data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])],
syntSolvedGoals :: Map Goal Expr, syntSolvedGoals :: Map Goal Expr,
syntUnsolvedGoals :: Set Goal, syntUnsolvedGoals :: Set Goal,
syntResolvers :: Set Resolver, syntResolvers :: [Resolver], -- Set Resolver,
syntExamples :: [[Value]], syntExamples :: [[Value]],
syntOracle :: Oracle, syntOracle :: Oracle,
syntRoot :: Goal} syntRoot :: Goal}
@ -322,9 +322,9 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs
forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr) forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
forwardStep comp args = do let expr = fillHoles comp args forwardStep comp args = do let expr = fillHoles comp args
outputs <- calcExprOutputs expr outputs <- calcExprOutputs expr
-- TODO: FIXME separate recoverable & non-recoverable errors -- any isError outputs ||
matchedExisting <- gets $ evalState (matchAnyOutputs outputs) matchedExisting <- gets $ evalState (matchAnyOutputs outputs)
if any isFatalError outputs || matchedExisting then return Nothing else do -- TODO: all RecErrors example could be useful on future cases ?
if any isFatalError outputs || all isRecError outputs || matchedExisting then return Nothing else do
modify $ \st -> st { syntExprs = (expr, []) : syntExprs st} modify $ \st -> st { syntExprs = (expr, []) : syntExprs st}
return $ Just expr return $ Just expr
@ -338,11 +338,13 @@ splitGoal resolverGoal@(Goal outputs) selector | length outputs == length select
-- split goal by its index and by expr (if any answers matched), check if there is same goals to generated -- split goal by its index and by expr (if any answers matched), check if there is same goals to generated
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
modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $ resolvers <- gets syntResolvers
Set.insert (resolverThen r) $ unless (r `elem` resolvers) $ -- do not add existing resolvers
Set.insert (resolverElse r) $ modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $
syntUnsolvedGoals st, Set.insert (resolverThen r) $
syntResolvers = r `Set.insert` syntResolvers st } Set.insert (resolverElse r) $
syntUnsolvedGoals st,
syntResolvers = r : syntResolvers st } -- Set.insert
return r return r
-- TODO: use expr evaluated outputs ? -- TODO: use expr evaluated outputs ?
@ -353,8 +355,7 @@ trySolveGoal expr goal = do doesMatch <- gets $ matchGoal goal expr
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st -- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st
} }
return True return True
-- trace ("goal solved: " ++ show goal) -- TODO: trace -- trace ("goal solved: " ++ show goal) -- Tmp: trace
-- return True
else return False else return False
isGoalSolved :: Goal -> SyntState Bool isGoalSolved :: Goal -> SyntState Bool
@ -367,7 +368,7 @@ goalSolution goal = gets (Map.lookup goal . syntSolvedGoals)
-- returns found expr -- returns found expr
-- NOTE: goals expected to be resolved -- NOTE: goals expected to be resolved
resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState Expr resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState Expr
-- resolveStep r _ | trace ("resolution: " ++ show r) False = undefined -- TODO: trace -- resolveStep r _ | trace ("resolution: " ++ show r) False = undefined -- TMP: trace
resolveStep (ifCond, ifDoThen, ifDoElse) r = do let expr = IfE { ifCond, ifDoThen, ifDoElse } resolveStep (ifCond, ifDoThen, ifDoElse) r = do let expr = IfE { ifCond, ifDoThen, ifDoElse }
let goal = resolverGoal r let goal = resolverGoal r
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st, modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st,
@ -376,7 +377,7 @@ resolveStep (ifCond, ifDoThen, ifDoElse) r = do let expr = IfE { ifCond, ifDoThe
return expr return expr
tryResolve :: Resolver -> SyntState (Maybe Expr) tryResolve :: Resolver -> SyntState (Maybe Expr)
-- tryResolve r | trace ("try resolution: " ++ show r) False = undefined -- TODO -- tryResolve r | trace ("try resolution: " ++ show r) False = undefined -- TMP: trace
tryResolve r = do condSol <- goalSolution $ resolverCond r tryResolve r = do condSol <- goalSolution $ resolverCond r
thenSol <- goalSolution $ resolverThen r thenSol <- goalSolution $ resolverThen r
elseSol <- goalSolution $ resolverElse r elseSol <- goalSolution $ resolverElse r
@ -483,7 +484,7 @@ createSynt oracle goals = let root = Goal $ map (Just . snd) goals in
Synt { syntExprs = [], Synt { syntExprs = [],
syntSolvedGoals = Map.empty, syntSolvedGoals = Map.empty,
syntUnsolvedGoals = Set.singleton root, syntUnsolvedGoals = Set.singleton root,
syntResolvers = Set.empty, syntResolvers = [], -- Set.empty
syntExamples = map fst goals, syntExamples = map fst goals,
syntOracle = oracle, syntOracle = oracle,
syntRoot = root} syntRoot = root}
@ -495,7 +496,7 @@ stepOnAddedExpr :: Expr -> SyntState (Maybe Expr)
stepOnAddedExpr expr = do newEx <- saturateStep expr stepOnAddedExpr expr = do newEx <- saturateStep expr
if not . null $ newEx then do -- redo prev exprs (including current) if not . null $ newEx then do -- redo prev exprs (including current)
st <- get st <- get
-- trace ("exFound: " ++ show newEx) $ -- TODO: trace -- trace ("exFound: " ++ show newEx) $ -- TMP: trace
stepOnAddedExprs $ map fst $ syntExprs st stepOnAddedExprs $ map fst $ syntExprs st
else do -- try resolve goals & resolvers, generate new resolvers else do -- try resolve goals & resolvers, generate new resolvers
maybeResult <- terminateStep expr maybeResult <- terminateStep expr
@ -507,7 +508,7 @@ stepOnAddedExpr expr = do newEx <- saturateStep expr
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 $ Set.toList $ syntUnsolvedGoals st modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st $ [syntRoot st] -- TODO: use Set.toList $ syntUnsolvedGoals st ?
gets $ \st -> syntRoot st `Map.lookup` syntSolvedGoals st 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
@ -535,7 +536,6 @@ stepOnAddedExprs = foldM step Nothing
step res@(Just {}) _ = return res step res@(Just {}) _ = return res
step Nothing expr = stepOnAddedExpr expr step Nothing expr = stepOnAddedExpr expr
-- TODO: throw away exprs with Errors (?)
-- returns result and valid expr -- returns result and valid expr
stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr, Maybe Expr) stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr, Maybe Expr)
stepOnNewExpr comp args = do expr <- forwardStep comp args stepOnNewExpr comp args = do expr <- forwardStep comp args
@ -559,7 +559,7 @@ syntesisStep steps prevExprs = -- oracle should be defined on the provided emamp
(result, validExprs) <- foldM step (Nothing, []) genExprs (result, validExprs) <- foldM step (Nothing, []) genExprs
if isJust result if isJust result
then return result then return result
else syntesisStep (steps - 1) (validExprs : prevExprs) else trace ("steps left: " ++ show (steps - 1)) $ syntesisStep (steps - 1) (validExprs : prevExprs)
where step res@(Just {}, _) _ = return res where step res@(Just {}, _) _ = return res
step (Nothing, exprs) expr = do (res, val) <- uncurry stepOnNewExpr expr step (Nothing, exprs) expr = do (res, val) <- uncurry stepOnNewExpr expr
return (res, maybeToList val ++ exprs) return (res, maybeToList val ++ exprs)
@ -578,13 +578,14 @@ mainExamples :: [[Value]]
mainExamples = [[ListV [IntV 1, IntV 2, IntV 3]]] 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 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]]
--- reverse --- reverse
reverseOracle :: Oracle reverseOracle :: Oracle
reverseOracle [ListV xs] = Just $ ListV $ reverse xs -- reverseOracle [ListV xs] = Just $ ListV $ reverse xs
reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs
reverseOracle _ = Nothing reverseOracle _ = Nothing
reverseExpr :: Expr reverseExpr :: Expr
@ -601,8 +602,8 @@ reverseConf = Conf { confInput = head allExamples,
--- stutter --- stutter
stutterOracle :: Oracle stutterOracle :: Oracle
stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs] stutterOracle [ListV (x : xs)] | isInt x = do ListV xs' <- stutterOracle [ListV xs]
return $ ListV $ x : x : xs' return $ ListV $ x : x : xs'
stutterOracle [ListV []] = Just $ ListV [] stutterOracle [ListV []] = Just $ ListV []
stutterOracle _ = Nothing stutterOracle _ = Nothing
@ -640,7 +641,8 @@ idOracle :: Oracle
idOracle [x] = Just x idOracle [x] = Just x
idOracle _ = Nothing idOracle _ = Nothing
-- TODO: examples
main = do steps <- readLn :: IO Int main = do steps <- readLn :: IO Int
print $ fst $ syntesis steps lengthOracle allExamples print $ fst $ syntesis steps reverseOracle allExamples
-- main = print $ (SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE)) `elem` (map fst $ syntExprs $ snd $ syntesis 10 reverseOracle allExamples)
-- Just (IfE {ifCond = IsEmptyE (InputE ZeroE), ifDoThen = InputE ZeroE :++: TailE (InputE ZeroE :++: (InputE ZeroE :++: (ZeroE ::: EmptyListE))), ifDoElse = SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE)})