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

type check preparation: add types to oracle

Browse source
This commit is contained in:
ProgramSnail 2025-11-05 01:58:03 +03:00
parent b7963e87a6
commit edc6c373b0
8 changed files with 179 additions and 803 deletions
Download patch file Download diff file Expand all files Collapse all files

4
.gitignore vendored Normal file
View file

@ -0,0 +1,4 @@
02
**Main
**.hi
**.o

195
escher.hs
View file

@ -15,17 +15,18 @@ import Debug.Trace (trace)
data Value = BoolV Bool data Value = BoolV Bool
| IntV Int | IntV Int
| ListV [Value] | ListV [Value]
| TreeV Tree | TreeV (Tree Value)
deriving (Read, Show, Eq, Ord) deriving (Read, Show, Eq, Ord)
data Tree = TNode { treeLeft :: Tree, treeRoot :: Value, treeRight :: Tree } data Tree a = TNode { treeLeft :: Tree a, treeRoot :: a, treeRight :: Tree a }
| TLeaf Value | TLeaf a
deriving (Read, Show, Eq, Ord) deriving (Read, Show, Eq, Ord)
data Type = BoolT data Type = BoolT
| IntT | IntT
| ListT | ListT Type
| TreeT | TreeT Type
| AnyT
deriving (Read, Show, Eq, Ord) deriving (Read, Show, Eq, Ord)
data Expr = Expr :&&: Expr -- Bool data Expr = Expr :&&: Expr -- Bool
@ -52,14 +53,13 @@ data Expr = Expr :&&: Expr -- Bool
| CreateNodeE { nodeLeft :: Expr, nodeRoot :: Expr, nodeRight :: Expr } | CreateNodeE { nodeLeft :: Expr, nodeRoot :: Expr, nodeRight :: Expr }
| CreateLeafE Expr | CreateLeafE Expr
| IfE { ifCond :: Expr, ifDoThen :: Expr, ifDoElse :: Expr }-- Control | IfE { ifCond :: Expr, ifDoThen :: Expr, ifDoElse :: Expr }-- Control
| SelfE Expr | SelfE [Expr]
| InputE Expr | InputE Int
| Hole | Hole
deriving (Read, Show, Eq, Ord) deriving (Read, Show, Eq, Ord)
data Conf = Conf {confInput :: [Value], data Conf = Conf {confInput :: [Value],
confOracle :: Oracle, confOracle :: Oracle,
confProg :: Expr,
confExamples :: [[Value]]} confExamples :: [[Value]]}
------------ ------------
@ -111,13 +111,17 @@ instance MonadFail Result where
typeOf :: Value -> Type typeOf :: Value -> Type
typeOf (BoolV {}) = BoolT typeOf (BoolV {}) = BoolT
typeOf (IntV {}) = IntT typeOf (IntV {}) = IntT
typeOf (ListV {}) = ListT typeOf (ListV (v : _)) = ListT $ typeOf v
typeOf (TreeV {}) = TreeT typeOf (ListV []) = ListT AnyT
typeOf (TreeV (TNode { treeLeft, treeRoot, treeRight })) = TreeT $ typeOf treeRoot
typeOf (TreeV (TLeaf v)) = TreeT $ typeOf v
isBool = (== BoolT) . typeOf isBool = (== BoolT) . typeOf
isInt = (== IntT) . typeOf isInt = (== IntT) . typeOf
isList = (== ListT) . typeOf isList x | ListT {} <- typeOf x = True
isTree = (== TreeT) . typeOf | otherwise = False
isTree x | TreeT {} <- typeOf x = True
| otherwise = False
isResult (Result {}) = True isResult (Result {}) = True
isResult _ = False isResult _ = False
@ -128,7 +132,7 @@ isRecError _ = False
isFatalError (FatalError {}) = True isFatalError (FatalError {}) = True
isFatalError _ = False isFatalError _ = False
treeHeight :: Tree -> Int treeHeight :: Tree a -> 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)
@ -205,27 +209,120 @@ eval conf (CreateLeafE e) = do v <- eval conf e
return $ TreeV $ TLeaf v return $ TreeV $ TLeaf v
eval conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolV condB <- eval conf ifCond eval conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolV condB <- eval conf ifCond
if condB then eval conf ifDoThen else eval conf ifDoElse if condB then eval conf ifDoThen else eval conf ifDoElse
eval conf (SelfE e) = do ListV recInput <- eval conf e eval conf (SelfE es) = do recInput <- foldM (\es e -> consValsM es (eval conf e)) [] es
-- NOTE: replaced guards for better errors description -- NOTE: replaced guards for better errors description
-- 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 FatalError $ "self call different length, new=" ++ show recInput ++ " old=" ++ show (confInput conf) -- TODO: fatal ? 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)
else do else do
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 $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)] else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)]
Nothing -> FatalError $ "no oracle output on " ++ show recInput Nothing -> FatalError $ "no oracle output on " ++ show recInput
eval conf (InputE e) = do IntV i <- eval conf e where consValsM :: [Value] -> Result Value -> Result [Value]
if i < 0 || i >= length (confInput conf) -- NOTE: replaced guard for better errors description consValsM vs (Result v) = Result $ v : vs
consValsM _ (FatalError err) = FatalError err
consValsM _ (RecError err) = RecError err
consValsM _ (NewExamples ex) = NewExamples ex
eval conf (InputE i) = do 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 -- TODO: fatal ? 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"
data TypeConf = TypeConf { typeConfInput :: [Type],
typeConfOutput :: Type }
checkType :: TypeConf -> Expr -> Maybe Type
checkType conf (left :&&: right) = do BoolT <- checkType conf left
BoolT <- checkType conf right
return BoolT
checkType conf (left :||: right) = do BoolT <- checkType conf left
BoolT <- checkType conf right
return BoolT
checkType conf (NotE e) = do BoolT <- checkType conf e
return BoolT
checkType conf (left :=: right) = do leftT <- checkType conf left
rightT <- checkType conf right
guard $ leftT == rightT
return BoolT
checkType conf (Leq0 e) = do IntT <- checkType conf e
return BoolT
checkType conf (IsEmptyE e) = do ListT _ <- checkType conf e
return BoolT
checkType conf (left :+: right) = do IntT <- checkType conf left
IntT <- checkType conf right
return IntT
checkType conf (left :-: right) = do IntT <- checkType conf left
IntT <- checkType conf right
return IntT
checkType conf (IncE e) = do IntT <- checkType conf e
return IntT
checkType conf (DecE e) = do IntT <- checkType conf e
return IntT
checkType conf ZeroE = return IntT
checkType conf (Div2E e) = do IntT <- checkType conf e
return IntT
checkType conf (TailE e) = do ListT t <- checkType conf e
return $ ListT t
checkType conf (HeadE e) = do ListT t <- checkType conf e
return t
checkType conf (left :++: right) = do ListT t <- checkType conf left
ListT u <- checkType conf right
guard $ t == u
return $ ListT t
checkType conf (left ::: right) = do t <- checkType conf left
ListT u <- checkType conf right
guard $ t == u
return $ ListT t
checkType conf EmptyListE = return $ ListT AnyT -- TODO
checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e
return BoolT
checkType conf (TreeValE e) = do TreeT t <- checkType conf e
return t
checkType conf (TreeLeftE e) = do TreeT t <- checkType conf e
return $ TreeT t
checkType conf (TreeRightE e) = do TreeT t <- checkType conf e
return $ TreeT t
checkType conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeT t <- checkType conf nodeLeft
u <- checkType conf nodeRoot
guard $ t == u
TreeT w <- checkType conf nodeRight
guard $ t == w
return $ TreeT t
checkType conf (CreateLeafE e) = do t <- checkType conf e
return $ TreeT t
checkType conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolT <- checkType conf ifCond
leftT <- checkType conf ifDoThen
rightT <- checkType conf ifDoElse
guard $ leftT == rightT
return leftT
checkType conf (SelfE es) = do let ts = typeConfInput conf
guard $ length ts == length es
guard $ and $ zipWith (\t e -> checkType conf e == Just t) ts es
return $ typeConfOutput conf
checkType conf (InputE i) = Just $ typeConfInput conf !! i
checkType _ Hole = Nothing
-- checkType _ _ = Nothing
type Cache = Map Expr (Result Value)
eval' :: Cache -> Conf -> Expr -> (Result Value, Cache)
eval' cache conf expr = case expr `Map.lookup` cache of
Just result -> (result, cache)
Nothing -> let result = eval conf expr in
(result, Map.insert expr result cache)
eval'' :: Conf -> Expr -> SyntState (Result Value)
eval'' conf expr = do cache <- gets syntCache
let (result, cache') = eval' cache conf expr
modify $ \st -> st {syntCache = cache'}
return result
------------ ------------
type Oracle = [Value] -> Maybe Value type Oracle = [Value] -> Maybe Value
@ -248,6 +345,7 @@ data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])],
syntResolvers :: [Resolver], -- Set Resolver, syntResolvers :: [Resolver], -- Set Resolver,
syntExamples :: [[Value]], syntExamples :: [[Value]],
syntOracle :: Oracle, syntOracle :: Oracle,
syntCache :: Cache,
syntRoot :: Goal} syntRoot :: Goal}
type SyntState a = State Synt a type SyntState a = State Synt a
@ -281,15 +379,13 @@ fillHoles (CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole})
fillHoles (CreateLeafE Hole) [e] = CreateLeafE e fillHoles (CreateLeafE Hole) [e] = CreateLeafE e
fillHoles (IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}) 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 hs) es | all (== Hole) hs && length hs == length es = SelfE es
fillHoles (InputE Hole) [e] = InputE e fillHoles (InputE i) [] = InputE i
fillHoles (InputE ZeroE) [] = InputE ZeroE -- TMP
fillHoles _ _ = undefined fillHoles _ _ = undefined
confBySynt :: [Value] -> Expr -> Synt -> Conf confBySynt :: [Value] -> Expr -> Synt -> Conf
confBySynt input expr st = Conf {confInput = input, confBySynt input expr st = Conf {confInput = input,
confOracle = syntOracle st, confOracle = syntOracle st,
confProg = expr,
confExamples = syntExamples st} confExamples = syntExamples st}
matchGoal :: Goal -> Expr -> Synt -> Bool matchGoal :: Goal -> Expr -> Synt -> Bool
@ -314,9 +410,9 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs
step True _ = return True step True _ = return True
step False expr = do exprOutputs <- calcExprOutputs expr step False expr = do exprOutputs <- calcExprOutputs expr
return $ outputs == exprOutputs -- and $ zipWith sameResults outputs exprOutputs return $ outputs == exprOutputs -- and $ zipWith sameResults outputs exprOutputs
-- sameResults (Result left) (Result right) = left == right sameResults (Result left) (Result right) = left == right
-- sameResults (RecError {}) _ = False sameResults (RecError {}) (RecError {}) = True
-- sameResults _ (RecError {}) = False sameResults _ _ = False
-- generate next step of exprs, remove copies -- generate next step of exprs, remove copies
forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr) forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
@ -415,7 +511,7 @@ terminateStep expr = do doesMatch <- gets $ \st -> matchGoal (syntRoot st) expr
------ patterns ------ patterns
patterns0 :: [Expr] patterns0 :: [Expr]
patterns0 = [ZeroE, EmptyListE, InputE ZeroE] -- TMP: NOTE: for faster search patterns0 = [ZeroE, EmptyListE, InputE 0] -- TMP: NOTE: for faster search
patterns1 :: [Expr] patterns1 :: [Expr]
patterns1 = [NotE Hole, Leq0 Hole, patterns1 = [NotE Hole, Leq0 Hole,
@ -425,8 +521,8 @@ patterns1 = [NotE Hole, Leq0 Hole,
-- IsLeafE Hole, TreeValE Hole, -- IsLeafE Hole, TreeValE Hole,
-- TreeLeftE Hole, TreeRightE Hole, -- TreeLeftE Hole, TreeRightE Hole,
-- CreateLeafE Hole, -- CreateLeafE Hole,
SelfE Hole, SelfE [Hole],
InputE Hole InputE 0
] ]
patterns2 :: [Expr] patterns2 :: [Expr]
@ -487,6 +583,7 @@ createSynt oracle goals = let root = Goal $ map (Just . snd) goals in
syntResolvers = [], -- Set.empty syntResolvers = [], -- Set.empty
syntExamples = map fst goals, syntExamples = map fst goals,
syntOracle = oracle, syntOracle = oracle,
syntCache = Map.empty, -- ??
syntRoot = root} syntRoot = root}
initSynt :: Oracle -> [([Value], Value)] -> SyntState () initSynt :: Oracle -> [([Value], Value)] -> SyntState ()
@ -508,7 +605,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 $ [syntRoot st] -- TODO: use 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
@ -524,7 +621,6 @@ stepOnAddedExpr expr = do newEx <- saturateStep expr
matchResult (NewExamples {}) _ = Just False matchResult (NewExamples {}) _ = Just False
matchResult _ Nothing = Nothing matchResult _ Nothing = Nothing
matchResult (RecError {}) _ = Just False matchResult (RecError {}) _ = Just False
matchResult (FatalError {}) _ = Just False -- TODO: FIXME: should be none
matchResult (Result x) (Just y) = Just $ x == y matchResult (Result x) (Just y) = Just $ x == y
-- compareExprOutputs outputs False _ = False -- compareExprOutputs outputs False _ = False
-- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e -- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e
@ -589,14 +685,13 @@ reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs
reverseOracle _ = Nothing reverseOracle _ = Nothing
reverseExpr :: Expr reverseExpr :: Expr
reverseExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), reverseExpr = IfE { ifCond = IsEmptyE (InputE 0),
ifDoThen = EmptyListE, ifDoThen = EmptyListE,
ifDoElse = SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE) } ifDoElse = SelfE [TailE (InputE 0)] :++: (HeadE (InputE 0) ::: EmptyListE) }
reverseConf :: Conf reverseConf :: Conf
reverseConf = Conf { confInput = head allExamples, reverseConf = Conf { confInput = head allExamples,
confOracle = reverseOracle, confOracle = reverseOracle,
confProg = reverseExpr,
confExamples = allExamples } confExamples = allExamples }
--- stutter --- stutter
@ -608,14 +703,13 @@ stutterOracle [ListV []] = Just $ ListV []
stutterOracle _ = Nothing stutterOracle _ = Nothing
stutterExpr :: Expr stutterExpr :: Expr
stutterExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), stutterExpr = IfE { ifCond = IsEmptyE (InputE 0),
ifDoThen = EmptyListE, ifDoThen = EmptyListE,
ifDoElse = HeadE (InputE ZeroE) ::: (HeadE (InputE ZeroE) ::: SelfE (TailE (InputE ZeroE) ::: EmptyListE)) } ifDoElse = HeadE (InputE 0) ::: (HeadE (InputE 0) ::: SelfE [TailE (InputE 0)]) }
stutterConf :: Conf stutterConf :: Conf
stutterConf = Conf { confInput = head allExamples, stutterConf = Conf { confInput = head allExamples,
confOracle = stutterOracle, confOracle = stutterOracle,
confProg = stutterExpr,
confExamples = allExamples } confExamples = allExamples }
--- length --- length
@ -625,14 +719,13 @@ lengthOracle [ListV xs] = Just $ IntV $ length xs
lengthOracle _ = Nothing lengthOracle _ = Nothing
lengthExpr :: Expr lengthExpr :: Expr
lengthExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), lengthExpr = IfE { ifCond = IsEmptyE (InputE 0),
ifDoThen = ZeroE, ifDoThen = ZeroE,
ifDoElse = IncE $ SelfE (TailE (InputE ZeroE) ::: EmptyListE) } ifDoElse = IncE $ SelfE [TailE (InputE 0)] }
lengthConf :: Conf lengthConf :: Conf
lengthConf = Conf { confInput = head allExamples, lengthConf = Conf { confInput = head allExamples,
confOracle = lengthOracle, confOracle = lengthOracle,
confProg = lengthExpr,
confExamples = allExamples } confExamples = allExamples }
--- ---

7
escher/Eval.hs
View file

@ -7,7 +7,10 @@ import Control.Monad (foldM)
import Debug.Trace (trace) import Debug.Trace (trace)
type Oracle = [Value] -> Maybe Value type OracleFunc = [Value] -> Maybe Value
data Oracle = Oracle { oracleTypes :: TypeConf,
oracleFunc :: OracleFunc }
data Conf = Conf {confInput :: [Value], data Conf = Conf {confInput :: [Value],
confOracle :: Oracle, confOracle :: Oracle,
@ -96,7 +99,7 @@ eval conf (SelfE es) = do recInput <- foldM (\es e -> consValsM es (eval conf e)
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)
else do else do
case confOracle conf recInput of case (oracleFunc $ 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 $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)] else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)]

12
escher/Expr.hs
View file

@ -42,6 +42,16 @@ data Value = BoolV Bool
| TreeV (Tree Value) | TreeV (Tree Value)
deriving (Read, Show, Eq, Ord) deriving (Read, Show, Eq, Ord)
data Type = BoolT
| IntT
| ListT Type
| TreeT Type
| AnyT
deriving (Read, Show, Eq, Ord)
data TypeConf = TypeConf { typeConfInput :: [Type],
typeConfOutput :: Type }
data Result a = Result a data Result a = Result a
| NewExamples [([Value], Value)] | NewExamples [([Value], Value)]
| RecError String | RecError String
@ -98,5 +108,3 @@ isFatalError _ = False
treeHeight :: Tree a -> Int treeHeight :: Tree a -> 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)

23
escher/Main.hs
View file

@ -218,7 +218,7 @@ syntesisStep steps prevExprs = -- oracle should be defined on the provided emamp
syntesis' :: [[Expr]] -> Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt) 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 . oracleFunc oracle) inputs in
runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs) runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs)
syntesis :: Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt) syntesis :: Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
@ -233,9 +233,14 @@ 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 []]]
listOracleOf :: OracleFunc -> Type -> Oracle
listOracleOf f t = Oracle { oracleTypes = TypeConf { typeConfInput = [ListT IntT],
typeConfOutput = t },
oracleFunc = f }
--- reverse --- reverse
reverseOracle :: Oracle reverseOracle :: OracleFunc
-- 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 [ListV xs] | all isInt xs = Just $ ListV $ reverse xs
reverseOracle _ = Nothing reverseOracle _ = Nothing
@ -247,12 +252,12 @@ reverseExpr = IfE { ifCond = IsEmptyE (InputE 0),
reverseConf :: Conf reverseConf :: Conf
reverseConf = Conf { confInput = head allExamples, reverseConf = Conf { confInput = head allExamples,
confOracle = reverseOracle, confOracle = listOracleOf reverseOracle $ ListT IntT,
confExamples = allExamples } confExamples = allExamples }
--- stutter --- stutter
stutterOracle :: Oracle stutterOracle :: OracleFunc
stutterOracle [ListV (x : xs)] | isInt x = 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 []
@ -265,12 +270,12 @@ stutterExpr = IfE { ifCond = IsEmptyE (InputE 0),
stutterConf :: Conf stutterConf :: Conf
stutterConf = Conf { confInput = head allExamples, stutterConf = Conf { confInput = head allExamples,
confOracle = stutterOracle, confOracle = listOracleOf stutterOracle $ ListT IntT,
confExamples = allExamples } confExamples = allExamples }
--- length --- length
lengthOracle :: Oracle lengthOracle :: OracleFunc
lengthOracle [ListV xs] = Just $ IntV $ length xs lengthOracle [ListV xs] = Just $ IntV $ length xs
lengthOracle _ = Nothing lengthOracle _ = Nothing
@ -281,17 +286,17 @@ lengthExpr = IfE { ifCond = IsEmptyE (InputE 0),
lengthConf :: Conf lengthConf :: Conf
lengthConf = Conf { confInput = head allExamples, lengthConf = Conf { confInput = head allExamples,
confOracle = lengthOracle, confOracle = listOracleOf lengthOracle IntT,
confExamples = allExamples } confExamples = allExamples }
--- ---
idOracle :: Oracle idOracle :: OracleFunc
idOracle [x] = Just x idOracle [x] = Just x
idOracle _ = Nothing idOracle _ = Nothing
main = do steps <- readLn :: IO Int main = do steps <- readLn :: IO Int
print $ fst $ syntesis steps reverseOracle allExamples print $ fst $ syntesis steps (listOracleOf reverseOracle $ ListT IntT) allExamples
-- main = print $ (SelfE (TailE (InputE ZeroE) ::: EmptyListE) :++: (HeadE (InputE ZeroE) ::: EmptyListE)) `elem` (map fst $ syntExprs $ snd $ syntesis 10 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)}) -- 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)})

1
escher/Syntesis.hs
View file

@ -2,6 +2,7 @@ module Syntesis where
import Expr import Expr
import Eval import Eval
import Control.Monad.State import Control.Monad.State
import Data.Map.Lazy (Map) import Data.Map.Lazy (Map)
import Data.Set (Set) import Data.Set (Set)

12
escher/TypeCheck.hs
View file

@ -3,13 +3,6 @@ module TypeCheck where
import Expr import Expr
import Control.Monad import Control.Monad
data Type = BoolT
| IntT
| ListT Type
| TreeT Type
| AnyT
deriving (Read, Show, Eq, Ord)
typeOf :: Value -> Type typeOf :: Value -> Type
typeOf (BoolV {}) = BoolT typeOf (BoolV {}) = BoolT
typeOf (IntV {}) = IntT typeOf (IntV {}) = IntT
@ -25,9 +18,6 @@ isList x | ListT {} <- typeOf x = True
isTree x | TreeT {} <- typeOf x = True isTree x | TreeT {} <- typeOf x = True
| otherwise = False | otherwise = False
data TypeConf = TypeConf { typeConfInput :: [Type],
typeConfOutput :: Type }
checkType :: TypeConf -> Expr -> Maybe Type checkType :: TypeConf -> Expr -> Maybe Type
checkType conf (left :&&: right) = do BoolT <- checkType conf left checkType conf (left :&&: right) = do BoolT <- checkType conf left
BoolT <- checkType conf right BoolT <- checkType conf right
@ -70,7 +60,7 @@ checkType conf (left ::: right) = do t <- checkType conf left
ListT u <- checkType conf right ListT u <- checkType conf right
guard $ t == u guard $ t == u
return $ ListT t return $ ListT t
checkType conf EmptyListE = return $ ListT AnyT -- TODO checkType conf EmptyListE = return $ ListT AnyT -- TODO FIXME: deal with AnyT
checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e
return BoolT return BoolT
checkType conf (TreeValE e) = do TreeT t <- checkType conf e checkType conf (TreeValE e) = do TreeT t <- checkType conf e

728
escher/escher.hs
View file

@ -1,728 +0,0 @@
-- 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.Monad.State as State
import Data.Map (Map)
import Data.Set (Set)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List (inits)
import Data.Maybe (fromMaybe, isJust, maybeToList)
import Debug.Trace (trace)
data Value = BoolV Bool
| IntV Int
| ListV [Value]
| TreeV Tree
deriving (Read, Show, Eq, Ord)
data Tree = TNode { treeLeft :: Tree, treeRoot :: Value, treeRight :: Tree }
| TLeaf Value
deriving (Read, Show, Eq, Ord)
data Type = BoolT
| IntT
| ListT Type
| TreeT Type
| AnyT
deriving (Read, Show, Eq, Ord)
data Expr = Expr :&&: Expr -- Bool
| Expr :||: Expr
| NotE Expr
| Expr :=: Expr
| Leq0 Expr
| IsEmptyE Expr
| Expr :+: Expr -- Int
| Expr :-: Expr
| IncE Expr
| DecE Expr
| ZeroE
| Div2E Expr
| TailE Expr -- List
| HeadE Expr
| Expr :++: Expr -- cat
| Expr ::: Expr -- cons
| EmptyListE
| IsLeafE Expr -- Tree
| TreeValE Expr
| TreeLeftE Expr
| TreeRightE Expr
| CreateNodeE { nodeLeft :: Expr, nodeRoot :: Expr, nodeRight :: Expr }
| CreateLeafE Expr
| IfE { ifCond :: Expr, ifDoThen :: Expr, ifDoElse :: Expr }-- Control
| SelfE Expr
| InputE Expr
| Hole
deriving (Read, Show, Eq, Ord)
data Conf = Conf {confInput :: [Value],
confOracle :: Oracle,
confExamples :: [[Value]]}
------------
data Result a = Result a
| NewExamples [([Value], Value)]
| RecError String
| FatalError String
deriving (Read, Show, Eq)
instance Applicative Result where
Result f <*> Result x = Result $ f x
NewExamples es <*> NewExamples es' = NewExamples $ es ++ es'
RecError err <*> _ = RecError err
_ <*> RecError err = RecError err
FatalError err <*> _ = FatalError err
_ <*> FatalError err = FatalError err
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
RecError err >>= _ = RecError err
FatalError err >>= _ = FatalError err
return = pure
instance Alternative Result where
empty = undefined -- TMP: no guards used -- FatalError "empty" -- TODO: rec ?
RecError err <|> y = y
FatalError err <|> y = y
NewExamples es <|> _ = NewExamples es
r@(Result x) <|> _ = r
instance Functor Result where
fmap = liftM
instance MonadFail Result where
fail _ = RecError "failure" -- TODO: fatal ?
-- instance (Foldable expr) ??
-- TODO: check all laws
------------
typeOf :: Value -> Type
typeOf (BoolV {}) = BoolT
typeOf (IntV {}) = IntT
typeOf (ListV {}) = ListT
typeOf (TreeV {}) = TreeT
isBool = (== BoolT) . typeOf
isInt = (== IntT) . typeOf
isList = (== ListT) . 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 (TLeaf {}) = 1
treeHeight TNode { treeLeft, treeRoot, treeRight } = 1 + (max (treeHeight treeLeft) (treeHeight treeRight) :: Int)
-- TODO: check
structuralLess :: Value -> Value -> Bool
structuralLess (BoolV left) (BoolV right) = not left && right
structuralLess (IntV left) (IntV right) = left < right && left > 0 -- ??
-- TODO: require same elems ?
structuralLess (ListV left) (ListV right) = length left < length right
-- TODO: require subtree ?
structuralLess (TreeV left) (TreeV right) = treeHeight left < treeHeight right
structuralLess _ _ = False
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 e
return $ BoolV $ not b
eval conf (left :=: right) = do leftV <- eval conf left
rightV <- eval conf right
return $ BoolV $ leftV == rightV
eval conf (Leq0 e) = do IntV i <- eval conf e
return $ BoolV $ i <= 0
eval conf (IsEmptyE e) = do v <- eval conf e
case v of
ListV [] -> return $ BoolV True
ListV _ -> return $ BoolV False
_ -> FatalError $ "Can't take empty not from list" ++ show v
eval conf (left :+: right) = do IntV leftI <- eval conf left
IntV rightI <- eval conf right
return $ IntV $ leftI + rightI
eval conf (left :-: right) = do IntV leftI <- eval conf left
IntV rightI <- eval conf right
return $ IntV $ leftI - rightI
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 = 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
return $ ListV t
eval conf (HeadE e) = do ListV (h : _) <- eval conf e
return h
eval conf (left :++: right) = do ListV leftL <- eval conf left
ListV rightL <- eval conf right
return $ ListV $ leftL ++ rightL
eval conf (left ::: right) = do leftV <- eval conf left
ListV rightL <- eval conf right
return $ ListV $ leftV : rightL
eval conf EmptyListE = return $ ListV []
eval conf (IsLeafE e) = do TreeV t <- eval conf e
return $ BoolV $ case t of
TNode {} -> False
TLeaf {} -> True
eval conf (TreeValE e) = do TreeV t <- eval conf e
return $ case t of
n@TNode {} -> treeRoot n
TLeaf e -> e
eval conf (TreeLeftE e) = do TreeV n@(TNode {}) <- eval conf e
return $ TreeV $ treeLeft n
eval conf (TreeRightE e) = do TreeV n@(TNode {}) <- eval conf e
return $ TreeV $ treeRight n
eval conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeV treeLeft <- eval conf nodeLeft
treeRoot <- eval conf nodeRoot
TreeV treeRight <- eval conf nodeRight
return $ TreeV $ TNode { treeLeft, treeRoot, treeRight }
eval conf (CreateLeafE e) = do v <- eval conf e
return $ TreeV $ TLeaf v
eval conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolV condB <- eval conf ifCond
if condB then eval conf ifDoThen else eval conf ifDoElse
eval conf (SelfE e) = do ListV recInput <- eval conf e
-- NOTE: replaced guards for better errors description
-- guard $ length newInput == length (confInput conf)
-- guard $ and $ zipWith structuralLess newInput (confInput conf)
if length recInput /= length (confInput conf)
then FatalError $ "self call different length, new=" ++ show recInput ++ " old=" ++ show (confInput conf) -- TODO: fatal ?
else do
if not $ and $ zipWith structuralLess recInput (confInput conf)
then RecError $ "self call on >= exprs, new=" ++ show recInput ++ " old=" ++ show (confInput conf)
else do
case confOracle conf recInput of
Just recOutput -> if recInput `elem` confExamples conf
then return recOutput
else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)]
Nothing -> FatalError $ "no oracle output on " ++ show recInput
eval conf (InputE e) = do IntV i <- eval conf e
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 -- TODO: fatal ?
else return $ confInput conf !! i -- use !? instead (?)
eval _ Hole = FatalError "can't eval hole"
-- TODO: types on container exstraction (polymorphic types / holes or generic containers?), input & oracle types <- change conf
checkType :: Conf -> Expr -> Maybe Type
checkType conf (left :&&: right) = do BoolT <- checkType conf left
BoolT <- checkType conf right
return BoolT
checkType conf (left :||: right) = do BoolT <- checkType conf left
BoolT <- checkType conf right
return BoolT
checkType conf (NotE e) = do BoolT <- checkType conf e
return BoolT
checkType conf (left :=: right) = do leftT <- checkType conf left
rightT <- checkType conf right
guard $ leftT == rightT
return BoolT
checkType conf (Leq0 e) = do IntT <- checkType conf e
return BoolT
checkType conf (IsEmptyE e) = do ListT AnyT <- checkType conf e
return BoolT
checkType conf (left :+: right) = do IntT <- checkType conf left
IntT <- checkType conf right
return IntT
checkType conf (left :-: right) = do IntT <- checkType conf left
IntT <- checkType conf right
return IntT
checkType conf (IncE e) = do IntT <- checkType conf e
return IntT
checkType conf (DecE e) = do IntT <- checkType conf e
return IntT
checkType conf ZeroE = return IntT
checkType conf (Div2E e) = do IntT <- checkType conf e
return IntT
checkType conf (TailE e) = do ListT t <- checkType conf e
return $ ListT t
checkType conf (HeadE e) = do ListT t <- checkType conf e
return t
checkType conf (left :++: right) = do ListT t <- checkType conf left
ListT u <- checkType conf right
guard $ t == u
return $ ListT t
checkType conf (left ::: right) = do t <- checkType conf left
ListT u <- checkType conf right
guard $ t == u
return $ ListT t
checkType conf EmptyListE = return ListT
checkType conf (IsLeafE e) = do TreeT <- checkType conf e
return BoolT
checkType conf (TreeValE e) = do TreeT <- checkType conf e
return undefined -- FIXME
checkType conf (TreeLeftE e) = do TreeT <- checkType conf e
return TreeT
checkType conf (TreeRightE e) = do TreeT <- checkType conf e
return TreeT
checkType conf (CreateNodeE {nodeLeft, nodeRoot, nodeRight}) = do TreeT <- checkType conf nodeLeft
_ <- checkType conf nodeRoot
TreeT <- checkType conf nodeRight
return TreeT
checkType conf (CreateLeafE e) = do _ <- checkType conf e
return TreeT
checkType conf (IfE {ifCond, ifDoThen, ifDoElse}) = do BoolT <- checkType conf ifCond
leftT <- checkType conf ifDoThen
rightT <- checkType conf ifDoElse
guard $ leftT == rightT
return leftT
checkType conf (SelfE e) = do ListT <- checkType conf e
return undefined -- FIXME: return oracle retunr type
checkType conf (InputE e) = undefined -- FIXME: use predefined input indices, pass input types
checkType _ Hole = Nothing
-- checkType _ _ = Nothing
type Cache = Map Expr (Result Value)
eval' :: Cache -> Conf -> Expr -> (Result Value, Cache)
eval' cache conf expr = case expr `Map.lookup` cache of
Just result -> (result, cache)
Nothing -> let result = eval conf expr in
(result, Map.insert expr result cache)
eval'' :: Conf -> Expr -> SyntState (Result Value)
eval'' conf expr = do cache <- gets syntCache
let (result, cache') = eval' cache conf expr
modify $ \st -> st {syntCache = cache'}
return result
------------
type Oracle = [Value] -> Maybe Value
-- bipartite graph, root is 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 ??
deriving (Read, Show, Eq, Ord)
data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])],
syntSolvedGoals :: Map Goal Expr,
syntUnsolvedGoals :: Set Goal,
syntResolvers :: [Resolver], -- Set Resolver,
syntExamples :: [[Value]],
syntOracle :: Oracle,
syntCache :: Cache,
syntRoot :: Goal}
type SyntState a = State Synt a
------------
--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 (Leq0 Hole) [e] = Leq0 e
fillHoles (IsEmptyE Hole) [e] = IsEmptyE 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 [] = 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 [] = 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 (InputE ZeroE) [] = InputE ZeroE -- TMP
fillHoles _ _ = undefined
confBySynt :: [Value] -> Expr -> Synt -> Conf
confBySynt input expr st = Conf {confInput = input,
confOracle = syntOracle st,
confExamples = syntExamples st}
matchGoal :: Goal -> Expr -> Synt -> Bool
matchGoal (Goal goal) expr st = 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) = x == y
matchValue _ Nothing = True
matchValue _ _ = False
------ syntesis steps
calcExprOutputs :: Expr -> SyntState [Result Value]
calcExprOutputs expr = gets (\st -> map (\input -> eval (confBySynt input expr st) expr) $ syntExamples st)
matchAnyOutputs :: [Result Value] -> SyntState Bool
matchAnyOutputs outputs = do exprs <- gets syntExprs
foldM step False $ map fst exprs
where step :: Bool -> Expr -> SyntState Bool
step True _ = return True
step False expr = do exprOutputs <- calcExprOutputs expr
return $ outputs == exprOutputs -- and $ zipWith sameResults outputs exprOutputs
sameResults (Result left) (Result right) = left == right
sameResults (RecError {}) (RecError {}) = True
sameResults _ _ = False
-- generate next step of exprs, remove copies
forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
forwardStep comp args = do let expr = fillHoles comp args
outputs <- calcExprOutputs expr
matchedExisting <- gets $ evalState (matchAnyOutputs outputs)
-- 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}
return $ Just expr
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 Resolver
splitGoalStep goal selector = do let r = splitGoal goal selector
resolvers <- gets syntResolvers
unless (r `elem` resolvers) $ -- do not add existing resolvers
modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $
Set.insert (resolverThen r) $
Set.insert (resolverElse r) $
syntUnsolvedGoals st,
syntResolvers = r : syntResolvers st } -- Set.insert
return r
-- TODO: use expr evaluated outputs ?
trySolveGoal :: Expr -> Goal -> SyntState Bool
trySolveGoal expr goal = do doesMatch <- gets $ matchGoal goal expr
if doesMatch then do
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st --,
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st
}
return True
-- trace ("goal solved: " ++ show goal) -- Tmp: trace
else return False
isGoalSolved :: Goal -> SyntState Bool
isGoalSolved goal = gets (Map.member goal . syntSolvedGoals)
goalSolution :: Goal -> SyntState (Maybe Expr)
goalSolution goal = gets (Map.lookup goal . syntSolvedGoals)
-- find all goals solved by new expr, by expr id it's values on examples, remove solved goals
-- returns found expr
-- NOTE: goals expected to be resolved
resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState Expr
-- resolveStep r _ | trace ("resolution: " ++ show r) False = undefined -- TMP: trace
resolveStep (ifCond, ifDoThen, ifDoElse) r = do let expr = IfE { ifCond, ifDoThen, ifDoElse }
let goal = resolverGoal r
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st,
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st,
syntExprs = (expr, []) : syntExprs st }
return expr
tryResolve :: Resolver -> SyntState (Maybe Expr)
-- tryResolve r | trace ("try resolution: " ++ show r) False = undefined -- TMP: trace
tryResolve r = do condSol <- goalSolution $ resolverCond r
thenSol <- goalSolution $ resolverThen r
elseSol <- goalSolution $ resolverElse r
case (condSol, thenSol, elseSol) of
(Just condExpr, Just thenExpr, Just elseExpr) -> do
expr <- resolveStep (condExpr, thenExpr, elseExpr) r
return $ Just expr
_ -> return Nothing
remakeSynt :: [[Value]] -> [Value] -> SyntState ()
remakeSynt newInputs newOutputs = do st <- get
let Goal oldOutputs = syntRoot st
goals <- gets $ \st -> zip (newInputs ++ syntExamples st)
(newOutputs ++ map (fromMaybe undefined) oldOutputs)
initSynt (syntOracle st) goals
modify (\st' -> st' { syntExprs = syntExprs st })
-- clear goal tree up to root, add example, calculate exprs on input (could be recursive ?)
-- returns new example
saturateStep :: Expr -> SyntState [[Value]]
saturateStep expr = do (newInputs, newOutputs) <- gets $ \st -> unzip $ foldl (searchEx st) [] (syntExamples st)
let exFound = not . null $ newInputs
when exFound $ remakeSynt newInputs newOutputs
return newInputs
where searchEx st [] input = case eval (confBySynt input expr st) expr of
NewExamples exs -> exs
_ -> []
searchEx _ exs _ = exs
-- try to find terminating expr
terminateStep :: Expr -> SyntState (Maybe Expr)
terminateStep expr = do doesMatch <- gets $ \st -> matchGoal (syntRoot st) expr st
return $ if doesMatch then Just expr else Nothing
------ patterns
patterns0 :: [Expr]
patterns0 = [ZeroE, EmptyListE, InputE ZeroE] -- TMP: NOTE: for faster search
patterns1 :: [Expr]
patterns1 = [NotE Hole, Leq0 Hole,
IsEmptyE Hole, IncE Hole,
DecE Hole, Div2E Hole,
TailE Hole, HeadE Hole,
-- IsLeafE Hole, TreeValE Hole,
-- TreeLeftE Hole, TreeRightE Hole,
-- CreateLeafE Hole,
SelfE Hole,
InputE Hole
]
patterns2 :: [Expr]
patterns2 = [Hole :&&: Hole,
Hole :||: Hole,
Hole :=: Hole,
Hole :+: Hole,
Hole :-: Hole,
Hole :++: Hole,
Hole ::: Hole]
patterns3 :: [Expr]
patterns3 = []
-- [CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole},
-- IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}]
------ generation
concatShuffle :: [[a]] -> [a]
concatShuffle xxs = let xxs' = filter (not . null) xxs in
if null xxs' then [] else
map head xxs' ++ concatShuffle (map tail xxs')
-- -> n, +1 for top expression
genNext1 :: [[Expr]] -> [Expr]
genNext1 = head
-- 1 2 3 ... (n - 1) + (n - 1) ... 1 -> n, +1 for top expression
genNext2 :: [[Expr]] -> [(Expr, Expr)]
genNext2 exprs = let len = length exprs in
let exprs' = tail exprs in
concatShuffle $
zipWith (\xs ys -> ([(x, y) | x <- xs, y <- ys])) exprs' $
reverse exprs'
-- map genNext2 [1, 1 2, 1 2 3, ..., 1 2 ... (n - 1)] + (n - 1) (n - 2) ... 1 -> n, +1 for top expression
genNext3 :: [[Expr]] -> [(Expr, Expr, Expr)]
genNext3 exprs = let exprs' = tail exprs in
let prefixes = map genNext2 $ tail $ inits exprs' in
let ends = reverse exprs' in
concatShuffle $
zipWith (\xys zs -> ([(x, y, z) | (x, y) <- xys, z <- zs])) prefixes ends
-- get list of patterns and holes for forward steps
genStep :: [[Expr]] -> [(Expr, [Expr])]
genStep [] = map (, []) patterns0
genStep xs = concatShuffle [[(p, [x]) | p <- patterns1, x <- genNext1 xs],
[(p, [x, y]) | p <- patterns2, (x, y) <- genNext2 xs],
[(p, [x, y, z]) | p <- patterns3, (x, y, z) <- genNext3 xs]]
------ algorithm
createSynt :: Oracle -> [([Value], Value)] -> Synt
createSynt oracle goals = let root = Goal $ map (Just . snd) goals in
Synt { syntExprs = [],
syntSolvedGoals = Map.empty,
syntUnsolvedGoals = Set.singleton root,
syntResolvers = [], -- Set.empty
syntExamples = map fst goals,
syntOracle = oracle,
syntCache = Map.empty, -- ??
syntRoot = root}
initSynt :: Oracle -> [([Value], Value)] -> SyntState ()
initSynt oracle goals = put $ createSynt oracle goals
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
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
execState (do r <- splitGoalStep goal matchesBool
exprs <- gets syntExprs
foldM_ (const $ flip trySolveGoal $ resolverCond r) False $ map fst exprs
exprs <- gets syntExprs
foldM_ (const $ flip trySolveGoal $ resolverElse r) False $ map fst exprs
-- TODO: replace with always solve goal
trySolveGoal expr (resolverThen r)) st
matchResult :: Result Value -> Maybe Value -> Maybe Bool -- Nothing for unimportant matches marked as Nothing
matchResult (NewExamples {}) _ = Just False
matchResult _ Nothing = Nothing
matchResult (RecError {}) _ = Just False
matchResult (Result x) (Just y) = Just $ x == y
-- compareExprOutputs outputs False _ = False
-- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e
-- outputs == eOutputs
stepOnAddedExprs :: [Expr] -> SyntState (Maybe Expr)
stepOnAddedExprs = foldM step Nothing
where step :: Maybe Expr -> Expr -> SyntState (Maybe Expr)
step res@(Just {}) _ = return res
step Nothing expr = stepOnAddedExpr expr
-- returns result and valid expr
stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr, Maybe Expr)
stepOnNewExpr comp args = do expr <- forwardStep comp args
case expr of
Just expr' -> do res <- stepOnAddedExpr expr'
return (res, expr)
Nothing -> return (Nothing, Nothing)
-- stages:
-- init state
-- 1. gen new step exprs
-- 2. process exprs by one
-- 3. try terminate / saturate
-- 4. try to solve existing goals
-- 5. make resolutions if goals solved
-- 6. split goals, where expr partially matched
syntesisStep :: Int -> [[Expr]] -> SyntState (Maybe Expr)
syntesisStep 0 _ = return Nothing
syntesisStep steps prevExprs = -- oracle should be defined on the provided emample inputs
do let genExprs = genStep prevExprs
(result, validExprs) <- foldM step (Nothing, []) genExprs
if isJust result
then return result
else trace ("steps left: " ++ show (steps - 1)) $ syntesisStep (steps - 1) (validExprs : prevExprs)
where step res@(Just {}, _) _ = return res
step (Nothing, exprs) expr = do (res, val) <- uncurry stepOnNewExpr expr
return (res, maybeToList val ++ exprs)
syntesis' :: [[Expr]] -> Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
syntesis' exprs steps oracle inputs = -- oracle should be defined on the providid examples
let outputs = map (fromMaybe undefined . oracle) inputs in
runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs)
syntesis :: Int -> Oracle -> [[Value]] -> (Maybe Expr, Synt)
syntesis = syntesis' []
------ examples
mainExamples :: [[Value]]
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 []]]
--- reverse
reverseOracle :: Oracle
-- reverseOracle [ListV xs] = Just $ ListV $ reverse xs
reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs
reverseOracle _ = Nothing
reverseExpr :: Expr
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,
confExamples = allExamples }
--- stutter
stutterOracle :: Oracle
stutterOracle [ListV (x : xs)] | isInt x = do ListV xs' <- stutterOracle [ListV xs]
return $ ListV $ x : x : xs'
stutterOracle [ListV []] = Just $ ListV []
stutterOracle _ = Nothing
stutterExpr :: Expr
stutterExpr = IfE { ifCond = IsEmptyE (InputE ZeroE),
ifDoThen = EmptyListE,
ifDoElse = HeadE (InputE ZeroE) ::: (HeadE (InputE ZeroE) ::: SelfE (TailE (InputE ZeroE) ::: EmptyListE)) }
stutterConf :: Conf
stutterConf = Conf { confInput = head allExamples,
confOracle = stutterOracle,
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,
confExamples = allExamples }
---
idOracle :: Oracle
idOracle [x] = Just x
idOracle _ = Nothing
main = do steps <- readLn :: IO Int
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)})