From edc6c373b00ff0827bbaf47dc3a0a63ed3574782 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 5 Nov 2025 01:58:03 +0300 Subject: [PATCH] type check preparation: add types to oracle --- .gitignore | 4 + escher.hs | 195 ++++++++---- escher/Eval.hs | 7 +- escher/Expr.hs | 12 +- escher/Main.hs | 23 +- escher/Syntesis.hs | 1 + escher/TypeCheck.hs | 12 +- escher/escher.hs | 728 -------------------------------------------- 8 files changed, 179 insertions(+), 803 deletions(-) create mode 100644 .gitignore delete mode 100644 escher/escher.hs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..c32703d --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +02 +**Main +**.hi +**.o diff --git a/escher.hs b/escher.hs index 99d6d5a..9f4715c 100644 --- a/escher.hs +++ b/escher.hs @@ -15,17 +15,18 @@ import Debug.Trace (trace) data Value = BoolV Bool | IntV Int | ListV [Value] - | TreeV Tree + | TreeV (Tree Value) deriving (Read, Show, Eq, Ord) -data Tree = TNode { treeLeft :: Tree, treeRoot :: Value, treeRight :: Tree } - | TLeaf Value +data Tree a = TNode { treeLeft :: Tree a, treeRoot :: a, treeRight :: Tree a } + | TLeaf a deriving (Read, Show, Eq, Ord) data Type = BoolT | IntT - | ListT - | TreeT + | ListT Type + | TreeT Type + | AnyT deriving (Read, Show, Eq, Ord) data Expr = Expr :&&: Expr -- Bool @@ -52,14 +53,13 @@ data Expr = Expr :&&: Expr -- Bool | CreateNodeE { nodeLeft :: Expr, nodeRoot :: Expr, nodeRight :: Expr } | CreateLeafE Expr | IfE { ifCond :: Expr, ifDoThen :: Expr, ifDoElse :: Expr }-- Control - | SelfE Expr - | InputE Expr + | SelfE [Expr] + | InputE Int | Hole deriving (Read, Show, Eq, Ord) data Conf = Conf {confInput :: [Value], confOracle :: Oracle, - confProg :: Expr, confExamples :: [[Value]]} ------------ @@ -111,13 +111,17 @@ instance MonadFail Result where typeOf :: Value -> Type typeOf (BoolV {}) = BoolT typeOf (IntV {}) = IntT -typeOf (ListV {}) = ListT -typeOf (TreeV {}) = TreeT +typeOf (ListV (v : _)) = ListT $ typeOf v +typeOf (ListV []) = ListT AnyT +typeOf (TreeV (TNode { treeLeft, treeRoot, treeRight })) = TreeT $ typeOf treeRoot +typeOf (TreeV (TLeaf v)) = TreeT $ typeOf v isBool = (== BoolT) . typeOf isInt = (== IntT) . typeOf -isList = (== ListT) . typeOf -isTree = (== TreeT) . typeOf +isList x | ListT {} <- typeOf x = True + | otherwise = False +isTree x | TreeT {} <- typeOf x = True + | otherwise = False isResult (Result {}) = True isResult _ = False @@ -128,7 +132,7 @@ isRecError _ = False isFatalError (FatalError {}) = True isFatalError _ = False -treeHeight :: Tree -> Int +treeHeight :: Tree a -> Int treeHeight (TLeaf {}) = 1 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 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 +eval conf (SelfE es) = do recInput <- foldM (\es e -> consValsM es (eval conf e)) [] es + -- 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 + where consValsM :: [Value] -> Result Value -> Result [Value] + 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 ? else return $ confInput conf !! i -- use !? instead (?) 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 @@ -248,6 +345,7 @@ data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])], syntResolvers :: [Resolver], -- Set Resolver, syntExamples :: [[Value]], syntOracle :: Oracle, + syntCache :: Cache, syntRoot :: Goal} 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 (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 (SelfE hs) es | all (== Hole) hs && length hs == length es = SelfE es +fillHoles (InputE i) [] = InputE i fillHoles _ _ = undefined confBySynt :: [Value] -> Expr -> Synt -> Conf confBySynt input expr st = Conf {confInput = input, confOracle = syntOracle st, - confProg = expr, confExamples = syntExamples st} matchGoal :: Goal -> Expr -> Synt -> Bool @@ -314,9 +410,9 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs 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 {}) _ = False - -- sameResults _ (RecError {}) = False + 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) @@ -415,7 +511,7 @@ terminateStep expr = do doesMatch <- gets $ \st -> matchGoal (syntRoot st) expr ------ patterns 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 = [NotE Hole, Leq0 Hole, @@ -425,8 +521,8 @@ patterns1 = [NotE Hole, Leq0 Hole, -- IsLeafE Hole, TreeValE Hole, -- TreeLeftE Hole, TreeRightE Hole, -- CreateLeafE Hole, - SelfE Hole, - InputE Hole + SelfE [Hole], + InputE 0 ] patterns2 :: [Expr] @@ -487,6 +583,7 @@ createSynt oracle goals = let root = Goal $ map (Just . snd) goals in syntResolvers = [], -- Set.empty syntExamples = map fst goals, syntOracle = oracle, + syntCache = Map.empty, -- ?? syntRoot = root} initSynt :: Oracle -> [([Value], Value)] -> SyntState () @@ -508,7 +605,7 @@ stepOnAddedExpr expr = do newEx <- saturateStep expr 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 ? + 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 @@ -524,7 +621,6 @@ stepOnAddedExpr expr = do newEx <- saturateStep expr matchResult (NewExamples {}) _ = Just False matchResult _ Nothing = Nothing 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 @@ -589,14 +685,13 @@ reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs reverseOracle _ = Nothing reverseExpr :: Expr -reverseExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), +reverseExpr = IfE { ifCond = IsEmptyE (InputE 0), 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 { confInput = head allExamples, confOracle = reverseOracle, - confProg = reverseExpr, confExamples = allExamples } --- stutter @@ -608,14 +703,13 @@ stutterOracle [ListV []] = Just $ ListV [] stutterOracle _ = Nothing stutterExpr :: Expr -stutterExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), +stutterExpr = IfE { ifCond = IsEmptyE (InputE 0), 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 { confInput = head allExamples, confOracle = stutterOracle, - confProg = stutterExpr, confExamples = allExamples } --- length @@ -625,14 +719,13 @@ lengthOracle [ListV xs] = Just $ IntV $ length xs lengthOracle _ = Nothing lengthExpr :: Expr -lengthExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), +lengthExpr = IfE { ifCond = IsEmptyE (InputE 0), ifDoThen = ZeroE, - ifDoElse = IncE $ SelfE (TailE (InputE ZeroE) ::: EmptyListE) } + ifDoElse = IncE $ SelfE [TailE (InputE 0)] } lengthConf :: Conf lengthConf = Conf { confInput = head allExamples, confOracle = lengthOracle, - confProg = lengthExpr, confExamples = allExamples } --- diff --git a/escher/Eval.hs b/escher/Eval.hs index b211050..3dfec0e 100644 --- a/escher/Eval.hs +++ b/escher/Eval.hs @@ -7,7 +7,10 @@ import Control.Monad (foldM) 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], 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) then RecError $ "self call on >= exprs, new=" ++ show recInput ++ " old=" ++ show (confInput conf) else do - case confOracle conf recInput of + case (oracleFunc $ confOracle conf) recInput of Just recOutput -> if recInput `elem` confExamples conf then return recOutput else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)] diff --git a/escher/Expr.hs b/escher/Expr.hs index 649a426..255d82a 100644 --- a/escher/Expr.hs +++ b/escher/Expr.hs @@ -42,6 +42,16 @@ data Value = BoolV Bool | TreeV (Tree Value) 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 | NewExamples [([Value], Value)] | RecError String @@ -98,5 +108,3 @@ isFatalError _ = False treeHeight :: Tree a -> Int treeHeight (TLeaf {}) = 1 treeHeight TNode { treeLeft, treeRoot, treeRight } = 1 + (max (treeHeight treeLeft) (treeHeight treeRight) :: Int) - - diff --git a/escher/Main.hs b/escher/Main.hs index e435f27..add2554 100644 --- a/escher/Main.hs +++ b/escher/Main.hs @@ -218,7 +218,7 @@ syntesisStep steps prevExprs = -- oracle should be defined on the provided emamp 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 + let outputs = map (fromMaybe undefined . oracleFunc oracle) inputs in runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs) 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 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 -reverseOracle :: Oracle +reverseOracle :: OracleFunc -- reverseOracle [ListV xs] = Just $ ListV $ reverse xs reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs reverseOracle _ = Nothing @@ -247,12 +252,12 @@ reverseExpr = IfE { ifCond = IsEmptyE (InputE 0), reverseConf :: Conf reverseConf = Conf { confInput = head allExamples, - confOracle = reverseOracle, + confOracle = listOracleOf reverseOracle $ ListT IntT, confExamples = allExamples } --- stutter -stutterOracle :: Oracle +stutterOracle :: OracleFunc stutterOracle [ListV (x : xs)] | isInt x = do ListV xs' <- stutterOracle [ListV xs] return $ ListV $ x : x : xs' stutterOracle [ListV []] = Just $ ListV [] @@ -265,12 +270,12 @@ stutterExpr = IfE { ifCond = IsEmptyE (InputE 0), stutterConf :: Conf stutterConf = Conf { confInput = head allExamples, - confOracle = stutterOracle, + confOracle = listOracleOf stutterOracle $ ListT IntT, confExamples = allExamples } --- length -lengthOracle :: Oracle +lengthOracle :: OracleFunc lengthOracle [ListV xs] = Just $ IntV $ length xs lengthOracle _ = Nothing @@ -281,17 +286,17 @@ lengthExpr = IfE { ifCond = IsEmptyE (InputE 0), lengthConf :: Conf lengthConf = Conf { confInput = head allExamples, - confOracle = lengthOracle, + confOracle = listOracleOf lengthOracle IntT, confExamples = allExamples } --- -idOracle :: Oracle +idOracle :: OracleFunc idOracle [x] = Just x idOracle _ = Nothing 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) -- 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)}) diff --git a/escher/Syntesis.hs b/escher/Syntesis.hs index 47c2e4d..98f73e8 100644 --- a/escher/Syntesis.hs +++ b/escher/Syntesis.hs @@ -2,6 +2,7 @@ module Syntesis where import Expr import Eval + import Control.Monad.State import Data.Map.Lazy (Map) import Data.Set (Set) diff --git a/escher/TypeCheck.hs b/escher/TypeCheck.hs index 1679175..876d9c2 100644 --- a/escher/TypeCheck.hs +++ b/escher/TypeCheck.hs @@ -3,13 +3,6 @@ module TypeCheck where import Expr import Control.Monad -data Type = BoolT - | IntT - | ListT Type - | TreeT Type - | AnyT - deriving (Read, Show, Eq, Ord) - typeOf :: Value -> Type typeOf (BoolV {}) = BoolT typeOf (IntV {}) = IntT @@ -25,9 +18,6 @@ isList x | ListT {} <- typeOf x = True isTree x | TreeT {} <- typeOf x = True | otherwise = False -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 @@ -70,7 +60,7 @@ 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 EmptyListE = return $ ListT AnyT -- TODO FIXME: deal with AnyT checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e return BoolT checkType conf (TreeValE e) = do TreeT t <- checkType conf e diff --git a/escher/escher.hs b/escher/escher.hs deleted file mode 100644 index 00515ef..0000000 --- a/escher/escher.hs +++ /dev/null @@ -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)})