mirror of
https://codeberg.org/ProgramSnail/prog_synthesis.git
synced 2025-12-06 05:28:42 +00:00
syntesis steps, goal match, fill holes
This commit is contained in:
ProgramSnail
parent
bf08ed8143
commit
e78372fbfc
1 changed files with 198 additions and 26 deletions
224
escher.hs
224
escher.hs
|
|
@ -1,20 +1,27 @@
|
|||
import Control.Monad (guard)
|
||||
import Control.Monad (guard, liftM)
|
||||
import Control.Applicative
|
||||
import Control.Monad.State
|
||||
import Data.Map (Map)
|
||||
import Data.Set (Set, insert)
|
||||
import Data.Set (delete)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
|
||||
data Value = BoolV Bool
|
||||
| IntV Int
|
||||
| ListV [Value]
|
||||
| TreeV Tree
|
||||
deriving (Read, Show, Eq)
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
data Tree = TNode { treeLeft :: Tree, treeRoot :: Value, treeRight :: Tree }
|
||||
| TLeaf Value
|
||||
deriving (Read, Show, Eq)
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
data Type = BoolT
|
||||
| IntT
|
||||
| ListT
|
||||
| TreeT
|
||||
deriving (Read, Show, Eq)
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
data Expr = Expr :&&: Expr -- Bool
|
||||
| Expr :||: Expr
|
||||
|
|
@ -39,9 +46,50 @@ data Expr = Expr :&&: Expr -- Bool
|
|||
| IfE { ifCond :: Expr, ifDoThen :: Expr, ifDoElse :: Expr }-- Control
|
||||
| SelfE Expr
|
||||
| InputE Expr
|
||||
| Hole
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
|
||||
data Conf = Conf {confInput :: [Value],
|
||||
confOracle :: [Value] -> Maybe Value,
|
||||
confProg :: Expr,
|
||||
confExamples :: [[Value]]}
|
||||
|
||||
------------
|
||||
|
||||
data Result a = Result a
|
||||
| NewExamples [([Value], Value)]
|
||||
| Error
|
||||
deriving (Read, Show, Eq)
|
||||
|
||||
data Conf = Conf { confInput :: [Value], confOracle :: [Value] -> Maybe Value, confProg :: Expr }
|
||||
instance Applicative Result where
|
||||
Result f <*> Result x = Result $ f x
|
||||
NewExamples es <*> NewExamples es' = NewExamples $ es ++ es'
|
||||
Error <*> _ = Error
|
||||
_ <*> Error = Error
|
||||
NewExamples es <*> _ = NewExamples es
|
||||
_ <*> NewExamples es = NewExamples es
|
||||
pure = Result
|
||||
|
||||
-- m1 <*> m2 = m1 >>= (\x1 -> m2 >>= (\x2 -> return (x1 x2)))
|
||||
instance Monad Result where
|
||||
Result x >>= f = f x
|
||||
NewExamples es >>= _ = NewExamples es
|
||||
Error >>= _ = Error
|
||||
return = pure
|
||||
|
||||
instance Alternative Result where
|
||||
empty = Error
|
||||
Error <|> y = y
|
||||
NewExamples es <|> _ = NewExamples es
|
||||
r@(Result x) <|> _ = r
|
||||
|
||||
instance Functor Result where
|
||||
fmap = liftM
|
||||
|
||||
instance MonadFail Result where
|
||||
fail _ = Error
|
||||
|
||||
-- TODO: check all laws
|
||||
|
||||
------------
|
||||
|
||||
|
|
@ -56,14 +104,14 @@ isInt = (== IntT) . typeOf
|
|||
isList = (== ListT) . typeOf
|
||||
isTree = (== TreeT) . typeOf
|
||||
|
||||
eval :: Conf -> Expr -> Maybe Value
|
||||
eval :: Conf -> Expr -> Result Value
|
||||
eval conf (left :&&: right) = do BoolV leftB <- eval conf left
|
||||
BoolV rightB <- eval conf right
|
||||
return $ BoolV $ leftB && rightB
|
||||
eval conf (left :||: right) = do BoolV leftB <- eval conf left
|
||||
BoolV rightB <- eval conf right
|
||||
return $ BoolV $ leftB || rightB
|
||||
eval conf (NotE e) = do BoolV b <- eval conf conf e
|
||||
eval conf (NotE e) = do BoolV b <- eval conf e
|
||||
return $ BoolV $ not b
|
||||
eval conf (left :+: right) = do IntV leftI <- eval conf left
|
||||
IntV rightI <- eval conf right
|
||||
|
|
@ -75,7 +123,7 @@ eval conf (IncE e) = do IntV i <- eval conf e
|
|||
return $ IntV $ i + 1
|
||||
eval conf (DecE e) = do IntV i <- eval conf e
|
||||
return $ IntV $ i - 1
|
||||
eval conf ZeroE = Just $ IntV 0
|
||||
eval conf ZeroE = return $ IntV 0
|
||||
eval conf (Div2E e) = do IntV i <- eval conf e
|
||||
return $ IntV $ i `div` 2
|
||||
eval conf (TailE e) = do ListV (_ : t) <- eval conf e
|
||||
|
|
@ -88,7 +136,7 @@ eval conf (left :++: right) = do ListV leftL <- eval conf left
|
|||
eval conf (left ::: right) = do leftV <- eval conf left
|
||||
ListV rightL <- eval conf right
|
||||
return $ ListV $ leftV : rightL
|
||||
eval conf EmptyListE = Just $ ListV []
|
||||
eval conf EmptyListE = return $ ListV []
|
||||
eval conf (IsLeafE e) = do TreeV t <- eval conf e
|
||||
return $ BoolV $ case t of
|
||||
TNode {} -> False
|
||||
|
|
@ -111,30 +159,154 @@ eval conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolV condB <- eval conf ifCon
|
|||
if condB then eval conf ifDoThen else eval conf ifDoElse
|
||||
eval conf (SelfE e) = do ListV newInput <- eval conf e
|
||||
guard $ length newInput < length (confInput conf)
|
||||
expectedV <- confOracle conf newInput -- TODO: add expected to Goal values list (if none), reset goal
|
||||
eval conf{ confInput = newInput } (confProg conf)
|
||||
if newInput `notElem` confExamples conf then
|
||||
(case confOracle conf newInput of
|
||||
Just expectedV -> NewExamples [(newInput, expectedV)]
|
||||
Nothing -> Error) -- TODO: ???
|
||||
else eval conf{ confInput = newInput } (confProg conf)
|
||||
eval conf (InputE e) = do IntV i <- eval conf e
|
||||
guard $ i >= 0 && i < length (confInput conf)
|
||||
return $ confInput conf !! i -- use !? instead (?)
|
||||
-- eval _ = Nothing
|
||||
eval _ Hole = Error
|
||||
|
||||
------------
|
||||
|
||||
-- bipartite graph, root is Goal
|
||||
data Goal = Goal [Resolver] [Maybe Value]
|
||||
data Resolver = Resolver { resolverCond :: Goal, resolverThen :: Goal, resolverElse :: Goal }
|
||||
newtype Goal = Goal [Maybe Value] -- result or unimportant
|
||||
deriving (Read, Show, Eq, Ord)
|
||||
-- Map sovled :: Goal -> Expr
|
||||
-- Set unsolved
|
||||
-- List Resolvers
|
||||
data Resolver = Resolver { resolverGoal :: Goal,
|
||||
resolverCond :: Goal,
|
||||
resolverThen :: Goal,
|
||||
resolverElse :: Goal } -- ids ??
|
||||
|
||||
splitGoal :: Goal -> [Bool] -> Goal
|
||||
splitGoal (Goal resolvers outputs) selector | length outputs == length selector =
|
||||
let resolverCond = Goal [] $ map (Just . BoolV) selector in
|
||||
let resolverThen = Goal [] $ zipWith (\v b -> if b then v else Nothing) outputs selector in
|
||||
let resolverElse = Goal [] $ zipWith (\v b -> if b then Nothing else v) outputs selector in
|
||||
let r = Resolver { resolverCond, resolverThen, resolverElse } in
|
||||
Goal (r : resolvers) outputs
|
||||
data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])],
|
||||
syntSolvedGoals :: Map Goal Expr,
|
||||
syntUnsolvedGoals :: Set Goal,
|
||||
syntResolvers :: [Resolver],
|
||||
syntExamples :: [[Value]],
|
||||
syntOracle :: [Value] -> Maybe Value,
|
||||
syntRoot :: Goal}
|
||||
type SyntState a = State Synt a
|
||||
|
||||
-- Inputs - vector of values
|
||||
------------
|
||||
|
||||
-- forwardStep
|
||||
-- resolveStep
|
||||
-- splitGoalStep
|
||||
-- saturateStep
|
||||
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
|
||||
fillHoles (Hole :||: Hole) [left, right] = left :||: right
|
||||
fillHoles (NotE Hole) [e] = NotE e
|
||||
fillHoles (Hole :+: Hole) [left, right] = left :+: right
|
||||
fillHoles (Hole :-: Hole) [left, right] = left :-: right
|
||||
fillHoles (IncE Hole) [e] = IncE e
|
||||
fillHoles (DecE Hole) [e] = DecE e
|
||||
-- fillHoles ZeroE
|
||||
fillHoles (Div2E Hole) [e] = Div2E e
|
||||
fillHoles (TailE Hole) [e] = TailE e
|
||||
fillHoles (HeadE Hole) [e] = HeadE e
|
||||
fillHoles (Hole :++: Hole) [left, right] = left :++: right
|
||||
fillHoles (Hole ::: Hole) [left, right] = left ::: right
|
||||
-- fillHoles EmptyListE
|
||||
fillHoles (IsLeafE Hole) [e] = IsLeafE e
|
||||
fillHoles (TreeValE Hole) [e] = TreeValE e
|
||||
fillHoles (TreeLeftE Hole) [e] = TreeLeftE e
|
||||
fillHoles (TreeRightE Hole) [e] = TreeRightE e
|
||||
fillHoles (CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole})
|
||||
[nodeLeft, nodeRoot, nodeRight] = CreateNodeE {nodeLeft, nodeRoot, nodeRight}
|
||||
fillHoles (CreateLeafE Hole) [e] = CreateLeafE e
|
||||
fillHoles (IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole})
|
||||
[ifCond, ifDoThen, ifDoElse] = IfE {ifCond, ifDoThen, ifDoElse}
|
||||
fillHoles (SelfE Hole) [e] = SelfE e
|
||||
fillHoles (InputE Hole) [e] = InputE e
|
||||
fillHoles _ _ = undefined
|
||||
|
||||
confBySynt :: [Value] -> Expr -> Synt -> Conf
|
||||
confBySynt input expr st = Conf {confInput = input,
|
||||
confOracle = syntOracle st,
|
||||
confProg = expr,
|
||||
confExamples = syntExamples st}
|
||||
|
||||
matchGoal :: Goal -> Synt -> Expr -> Bool
|
||||
matchGoal (Goal goal) st expr = let examples = syntExamples st in
|
||||
foldl checkOnInput True $ zip examples goal
|
||||
where checkOnInput False _ = False
|
||||
checkOnInput acc (input, output) = let output' = eval (confBySynt input expr st) expr in
|
||||
matchValue output' output -- TODO
|
||||
matchValue (Result x) (Just y) = True
|
||||
matchValue _ Nothing = True
|
||||
matchValue _ _ = False
|
||||
|
||||
-- generate next step of exprs, remove copies
|
||||
forwardStep :: Expr -> [Expr] -> SyntState ()
|
||||
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
|
||||
|
||||
splitGoal :: Goal -> [Bool] -> Resolver
|
||||
splitGoal resolverGoal@(Goal outputs) selector | length outputs == length selector =
|
||||
let resolverCond = Goal $ map (Just . BoolV) selector in
|
||||
let resolverThen = Goal $ zipWith (\v b -> if b then v else Nothing) outputs selector in
|
||||
let resolverElse = Goal $ zipWith (\v b -> if b then Nothing else v) outputs selector in
|
||||
Resolver { resolverGoal, resolverCond, resolverThen, resolverElse }
|
||||
|
||||
-- split goal by its index and by expr (if any answers matched), check if there is same goals to generated
|
||||
splitGoalStep :: Goal -> [Bool] -> SyntState ()
|
||||
splitGoalStep goal selector = do st <- get
|
||||
let r = splitGoal goal selector
|
||||
put st { syntUnsolvedGoals = Set.insert (resolverCond r) $
|
||||
Set.insert (resolverThen r) $
|
||||
Set.insert (resolverElse r) $
|
||||
syntUnsolvedGoals st,
|
||||
syntResolvers = r : syntResolvers st }
|
||||
|
||||
-- find all goals solved by new expr, by expr id it's values on examples, remove solved goals
|
||||
resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState ()
|
||||
resolveStep (ifCond, ifDoThen, ifDoElse) r = do st <- get
|
||||
let expr = IfE { ifCond, ifDoThen, ifDoElse }
|
||||
let goal = resolverGoal r
|
||||
put st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st,
|
||||
syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st,
|
||||
syntExprs = (expr, []) : syntExprs st }
|
||||
|
||||
-- data Resolver = Resolver { resolverGoal :: Goal, resolverCond :: Goal, resolverThen :: Goal, resolverElse :: Goal } -- ids ??
|
||||
|
||||
-- clear goal tree up to root, add example, calculate exprs on input (could be recursive ?)
|
||||
saturateStep :: Expr -> SyntState ()
|
||||
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
|
||||
NewExamples exs -> exs
|
||||
_ -> []
|
||||
searchNewExample _ exs _ = exs
|
||||
|
||||
-- try to find terminating expr
|
||||
terminateStep :: Expr -> SyntState (Maybe Expr)
|
||||
terminateStep expr = do st <- get
|
||||
return $ if matchGoal (syntRoot st) st expr
|
||||
then Just expr else Nothing
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue