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

different fixes, length & reverse examples

Browse source
This commit is contained in:
ProgramSnail 2025-10-26 20:34:44 +03:00
parent c609f9c9f7
commit 482b41680e
1 changed files with 124 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

176
escher.hs
View file

@ -6,7 +6,7 @@ import Data.Set (Set, insert, delete)
import qualified Data.Map as Map import qualified Data.Map as Map
import qualified Data.Set as Set import qualified Data.Set as Set
import Data.List (inits) import Data.List (inits)
import Data.Maybe (fromMaybe, isJust) import Data.Maybe (fromMaybe, isJust, maybeToList)
data Value = BoolV Bool data Value = BoolV Bool
| IntV Int | IntV Int
@ -62,14 +62,17 @@ data Conf = Conf {confInput :: [Value],
data Result a = Result a data Result a = Result a
| NewExamples [([Value], Value)] | NewExamples [([Value], Value)]
| Error String | RecError String
| FatalError String
deriving (Read, Show, Eq) deriving (Read, Show, Eq)
instance Applicative Result where instance Applicative Result where
Result f <*> Result x = Result $ f x Result f <*> Result x = Result $ f x
NewExamples es <*> NewExamples es' = NewExamples $ es ++ es' NewExamples es <*> NewExamples es' = NewExamples $ es ++ es'
Error err <*> _ = Error err RecError err <*> _ = RecError err
_ <*> Error err = Error err _ <*> RecError err = RecError err
FatalError err <*> _ = FatalError err
_ <*> FatalError err = FatalError err
NewExamples es <*> _ = NewExamples es NewExamples es <*> _ = NewExamples es
_ <*> NewExamples es = NewExamples es _ <*> NewExamples es = NewExamples es
pure = Result pure = Result
@ -78,12 +81,14 @@ instance Applicative Result where
instance Monad Result where instance Monad Result where
Result x >>= f = f x Result x >>= f = f x
NewExamples es >>= _ = NewExamples es NewExamples es >>= _ = NewExamples es
Error err >>= _ = Error err RecError err >>= _ = RecError err
FatalError err >>= _ = FatalError err
return = pure return = pure
instance Alternative Result where instance Alternative Result where
empty = Error "empty" empty = undefined -- TMP: no guards used -- FatalError "empty" -- TODO: fatal ?
Error err <|> y = y RecError err <|> y = y
FatalError err <|> y = y
NewExamples es <|> _ = NewExamples es NewExamples es <|> _ = NewExamples es
r@(Result x) <|> _ = r r@(Result x) <|> _ = r
@ -91,7 +96,9 @@ instance Functor Result where
fmap = liftM fmap = liftM
instance MonadFail Result where instance MonadFail Result where
fail _ = Error "failure" fail _ = RecError "failure" -- TODO: fatal ?
-- instance (Foldable expr) ??
-- TODO: check all laws -- TODO: check all laws
@ -108,6 +115,15 @@ isInt = (== IntT) . typeOf
isList = (== ListT) . typeOf isList = (== ListT) . typeOf
isTree = (== TreeT) . typeOf isTree = (== TreeT) . typeOf
isResult (Result {}) = True
isResult _ = False
isNewExamples (NewExamples {}) = True
isNewExamples _ = False
isRecError (RecError {}) = True
isRecError _ = False
isFatalError (FatalError {}) = True
isFatalError _ = False
treeHeight :: Tree -> Int treeHeight :: Tree -> Int
treeHeight (TLeaf {}) = 1 treeHeight (TLeaf {}) = 1
treeHeight TNode { treeLeft, treeRoot, treeRight } = 1 + (max (treeHeight treeLeft) (treeHeight treeRight) :: Int) treeHeight TNode { treeLeft, treeRoot, treeRight } = 1 + (max (treeHeight treeLeft) (treeHeight treeRight) :: Int)
@ -122,6 +138,8 @@ 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
@ -140,7 +158,7 @@ eval conf (IsEmptyE e) = do v <- eval conf e
case v of case v of
ListV [] -> return $ BoolV True ListV [] -> return $ BoolV True
ListV _ -> return $ BoolV False ListV _ -> return $ BoolV False
_ -> Error $ "Can't take empty not from list" ++ show v _ -> FatalError $ "Can't take empty not from list" ++ show v
eval conf (left :+: right) = do IntV leftI <- eval conf left eval conf (left :+: right) = do IntV leftI <- eval conf left
IntV rightI <- eval conf right IntV rightI <- eval conf right
return $ IntV $ leftI + rightI return $ IntV $ leftI + rightI
@ -190,21 +208,21 @@ eval conf (SelfE e) = do ListV newInput <- 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 newInput /= length (confInput conf) if length newInput /= length (confInput conf)
then Error $ "self call different length, new=" ++ show newInput ++ " old=" ++ show (confInput conf) then RecError $ "self call different length, new=" ++ show newInput ++ " old=" ++ show (confInput conf)
else do else do
if not $ and $ zipWith structuralLess newInput (confInput conf) if not $ and $ zipWith structuralLess newInput (confInput conf)
then Error $ "self call on >= exprs, new=" ++ show newInput ++ " old=" ++ show (confInput conf) then RecError $ "self call on >= exprs, new=" ++ show newInput ++ " old=" ++ show (confInput conf)
else do else do
if newInput `notElem` confExamples conf then if newInput `notElem` confExamples conf then
(case confOracle conf newInput of (case confOracle conf newInput of
Just expectedV -> NewExamples [(newInput, expectedV)] Just expectedV -> NewExamples [(newInput, expectedV)]
Nothing -> Error $ "no oracle output on " ++ show newInput) -- TODO: ??? Nothing -> RecError $ "no oracle output on " ++ show newInput) -- TODO: ???
else eval conf{ confInput = newInput } (confProg conf) else eval conf{ confInput = newInput } (confProg conf)
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 Error $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i then FatalError $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i
else return $ confInput conf !! i -- use !? instead (?) else return $ confInput conf !! i -- use !? instead (?)
eval _ Hole = Error "can't eval hole" eval _ Hole = FatalError "can't eval hole"
------------ ------------
@ -262,6 +280,7 @@ fillHoles (IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole})
[ifCond, ifDoThen, ifDoElse] = IfE {ifCond, ifDoThen, ifDoElse} [ifCond, ifDoThen, ifDoElse] = IfE {ifCond, ifDoThen, ifDoElse}
fillHoles (SelfE Hole) [e] = SelfE e fillHoles (SelfE Hole) [e] = SelfE e
fillHoles (InputE Hole) [e] = InputE e fillHoles (InputE Hole) [e] = InputE e
fillHoles (InputE ZeroE) [] = InputE ZeroE -- TMP
fillHoles _ _ = undefined fillHoles _ _ = undefined
confBySynt :: [Value] -> Expr -> Synt -> Conf confBySynt :: [Value] -> Expr -> Synt -> Conf
@ -287,10 +306,10 @@ calcExprOutputs expr = gets (\st -> map (\input -> eval (confBySynt input expr s
matchAnyOutputs :: [Result Value] -> SyntState Bool matchAnyOutputs :: [Result Value] -> SyntState Bool
matchAnyOutputs outputs = do exprs <- gets syntExprs matchAnyOutputs outputs = do exprs <- gets syntExprs
foldM step True $ map fst exprs foldM step False $ map fst exprs
where step :: Bool -> Expr -> SyntState Bool where step :: Bool -> Expr -> SyntState Bool
step False _ = return False step True _ = return True
step True expr = do exprOutputs <- calcExprOutputs expr step False expr = do exprOutputs <- calcExprOutputs expr
return $ outputs == exprOutputs return $ outputs == exprOutputs
-- generate next step of exprs, remove copies -- generate next step of exprs, remove copies
@ -298,7 +317,8 @@ forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
forwardStep comp args = do st <- get forwardStep comp args = do st <- get
let expr = fillHoles comp args let expr = fillHoles comp args
outputs <- calcExprOutputs expr outputs <- calcExprOutputs expr
if evalState (matchAnyOutputs outputs) st then return Nothing else do -- TODO: FIXME separate recoverable & non-recoverable errors -- any isError outputs ||
if any isFatalError outputs || evalState (matchAnyOutputs outputs) st then return Nothing else do
put st { syntExprs = (expr, []) : syntExprs st} put st { syntExprs = (expr, []) : syntExprs st}
return $ Just expr return $ Just expr
@ -367,7 +387,7 @@ remakeSynt newInputs newOutputs = do st <- get
saturateStep :: Expr -> SyntState Bool saturateStep :: Expr -> SyntState Bool
saturateStep expr = do st <- get saturateStep expr = do st <- get
let (newInputs, newOutputs) = unzip $ foldl (searchEx st) [] (syntExamples st) let (newInputs, newOutputs) = unzip $ foldl (searchEx st) [] (syntExamples st)
let isExFound = null newInputs let isExFound = not $ null newInputs
when isExFound $ remakeSynt newInputs newOutputs when isExFound $ remakeSynt newInputs newOutputs
return isExFound return isExFound
where searchEx st [] input = case eval (confBySynt input expr st) expr of where searchEx st [] input = case eval (confBySynt input expr st) expr of
@ -384,17 +404,18 @@ terminateStep expr = do st <- get
------ patterns ------ patterns
patterns0 :: [Expr] patterns0 :: [Expr]
patterns0 = [ZeroE, EmptyListE] patterns0 = [ZeroE, EmptyListE, InputE ZeroE] -- TMP: NOTE: for faster search
patterns1 :: [Expr] patterns1 :: [Expr]
patterns1 = [NotE Hole, Leq0 Hole, patterns1 = [NotE Hole, Leq0 Hole,
IsEmptyE Hole, IncE Hole, IsEmptyE Hole, IncE Hole,
DecE Hole, Div2E Hole, DecE Hole, Div2E Hole,
TailE Hole, HeadE Hole, TailE Hole, HeadE Hole,
IsLeafE Hole, TreeValE Hole, -- IsLeafE Hole, TreeValE Hole,
TreeLeftE Hole, TreeRightE Hole, -- TreeLeftE Hole, TreeRightE Hole,
CreateLeafE Hole, SelfE Hole, -- CreateLeafE Hole, SelfE Hole,
InputE Hole] InputE Hole
]
patterns2 :: [Expr] patterns2 :: [Expr]
patterns2 = [Hole :&&: Hole, patterns2 = [Hole :&&: Hole,
@ -406,8 +427,9 @@ patterns2 = [Hole :&&: Hole,
Hole ::: Hole] Hole ::: Hole]
patterns3 :: [Expr] patterns3 :: [Expr]
patterns3 = [CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole}, patterns3 = [] -- [
IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}] -- CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole},
-- IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}]
------ generation ------ generation
@ -473,14 +495,18 @@ stepOnAddedExpr expr = do exFound <- saturateStep expr
put $ foldl (splitGoalsFold expr exprOutputs) st $ Set.toList $ syntUnsolvedGoals st put $ foldl (splitGoalsFold expr exprOutputs) st $ Set.toList $ syntUnsolvedGoals st
return Nothing return Nothing
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 $ or matches then st else if any (fromMaybe False) matches then st else
execState (do r <- splitGoalStep goal matches let matchesBool = map (fromMaybe True) matches in
execState (do r <- splitGoalStep goal matchesBool
-- TODO: always solve goal -- TODO: always solve goal
trySolveGoal expr (resolverThen r)) st trySolveGoal expr (resolverThen r)) st
matchResult (NewExamples {}) _ = False matchResult :: Result Value -> Maybe Value -> Maybe Bool -- Nothing for unimportant matches marked as Nothing
matchResult _ Nothing = True matchResult (NewExamples {}) _ = Just False
matchResult (Result x) (Just y) = x == y matchResult _ Nothing = Nothing
compareExprOutputs outputs False _ = False matchResult (RecError {}) _ = Just False
matchResult (FatalError {}) _ = Just False -- TODO: FIXME: should be none
matchResult (Result x) (Just y) = Just $ x == y
-- compareExprOutputs outputs False _ = False
-- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e -- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e
-- outputs == eOutputs -- outputs == eOutputs
@ -491,12 +517,14 @@ stepOnAddedExprs = foldM step Nothing
step Nothing expr = stepOnAddedExpr expr step Nothing expr = stepOnAddedExpr expr
-- TODO: throw away exprs with Errors (?) -- TODO: throw away exprs with Errors (?)
stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr) -- returns result and valid expr
stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr, Maybe Expr)
stepOnNewExpr comp args = do st <- get stepOnNewExpr comp args = do st <- get
expr <- forwardStep comp args expr <- forwardStep comp args
case expr of case expr of
Just expr' -> stepOnAddedExpr expr' Just expr' -> do res <- stepOnAddedExpr expr'
Nothing -> return Nothing return (res, expr)
Nothing -> return (Nothing, Nothing)
-- stages: -- stages:
-- init state -- init state
@ -508,33 +536,50 @@ stepOnNewExpr comp args = do st <- get
-- 6. split goals, where expr partially matched -- 6. split goals, where expr partially matched
syntesisStep :: Int -> [[Expr]] -> SyntState (Maybe Expr) syntesisStep :: Int -> [[Expr]] -> SyntState (Maybe Expr)
syntesisStep 0 _ = return Nothing syntesisStep 0 _ = return Nothing
syntesisStep steps prevExprs = -- oracle should be defined on the providid examples syntesisStep steps prevExprs = -- oracle should be defined on the provided emample inputs
do let currentExprs = genStep prevExprs do let genExprs = genStep prevExprs
result <- foldM step Nothing currentExprs (result, validExprs) <- foldM step (Nothing, []) genExprs
if isJust result if isJust result
then return result then return result
else syntesisStep (steps - 1) (map (uncurry fillHoles) currentExprs : prevExprs) else syntesisStep (steps - 1) (validExprs : prevExprs)
where step res@(Just {}) _ = return res where step res@(Just {}, _) _ = return res
step Nothing expr = uncurry stepOnNewExpr expr step (Nothing, exprs) expr = do (res, val) <- uncurry stepOnNewExpr expr
return (res, maybeToList val ++ exprs)
syntesis' :: [[Expr]] -> Int -> Oracle -> [[Value]] -> Maybe Expr syntesis' :: [[Expr]] -> Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
syntesis' exprs steps oracle inputs = -- oracle should be defined on the providid examples syntesis' exprs steps oracle inputs = -- oracle should be defined on the providid examples
let outputs = map (fromMaybe undefined . oracle) inputs in let outputs = map (fromMaybe undefined . oracle) inputs in
evalState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs) runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs)
syntesis :: Int -> Oracle -> [[Value]] -> Maybe Expr syntesis :: Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
syntesis = syntesis' [] syntesis = syntesis' []
------ examples ------ examples
mainExamples :: [[Value]]
mainExamples = [[ListV [IntV 1, IntV 2, IntV 3]]]
allExamples :: [[Value]]
allExamples = [[ListV [IntV 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]]
--- reverse
reverseOracle :: Oracle reverseOracle :: Oracle
reverseOracle [ListV xs] = Just $ ListV $ reverse xs reverseOracle [ListV xs] = Just $ ListV $ reverse xs
reverseOracle _ = Nothing reverseOracle _ = Nothing
reverseExamples :: [[Value]] reverseExpr :: Expr
reverseExamples = [[ListV [IntV 1, IntV 2, IntV 3]]] reverseExpr = IfE { ifCond = IsEmptyE (InputE ZeroE),
ifDoThen = EmptyListE,
ifDoElse = SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE) }
--- reverseConf :: Conf
reverseConf = Conf { confInput = head allExamples,
confOracle = reverseOracle,
confProg = reverseExpr,
confExamples = allExamples }
--- stutter
stutterOracle :: Oracle stutterOracle :: Oracle
stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs] stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs]
@ -542,16 +587,41 @@ stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs]
stutterOracle [ListV []] = Just $ ListV [] stutterOracle [ListV []] = Just $ ListV []
stutterOracle _ = Nothing stutterOracle _ = Nothing
stutterExamples :: [[Value]]
stutterExamples = [[ListV [IntV 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]]
stutterExpr :: Expr stutterExpr :: Expr
stutterExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), ifDoThen = EmptyListE, ifDoElse = HeadE (InputE ZeroE) ::: (HeadE (InputE ZeroE) ::: SelfE (TailE (InputE ZeroE) ::: EmptyListE)) } stutterExpr = IfE { ifCond = IsEmptyE (InputE ZeroE),
ifDoThen = EmptyListE,
ifDoElse = HeadE (InputE ZeroE) ::: (HeadE (InputE ZeroE) ::: SelfE (TailE (InputE ZeroE) ::: EmptyListE)) }
stutterConf :: Conf stutterConf :: Conf
stutterConf = Conf { confInput = head stutterExamples, stutterConf = Conf { confInput = head allExamples,
confOracle = stutterOracle, confOracle = stutterOracle,
confProg = stutterExpr, confProg = stutterExpr,
confExamples = stutterExamples } confExamples = allExamples }
--- length
lengthOracle :: Oracle
lengthOracle [ListV xs] = Just $ IntV $ length xs
lengthOracle _ = Nothing
lengthExpr :: Expr
lengthExpr = IfE { ifCond = IsEmptyE (InputE ZeroE),
ifDoThen = ZeroE,
ifDoElse = IncE $ SelfE (TailE (InputE ZeroE) ::: EmptyListE) }
lengthConf :: Conf
lengthConf = Conf { confInput = head allExamples,
confOracle = lengthOracle,
confProg = lengthExpr,
confExamples = allExamples }
---
idOracle :: Oracle
idOracle [x] = Just x
idOracle _ = Nothing
-- TODO: examples -- TODO: examples
main = do steps <- readLn :: IO Int
print $ fst $ syntesis steps lengthOracle allExamples