import Control.Monad (guard, liftM, when, 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) 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 | TreeT 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, confProg :: Expr, 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: fatal ? 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 -- TODO: exprSize ? 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 RecError $ "self call different length, new=" ++ show recInput ++ " old=" ++ show (confInput conf) 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 [(recInput, recOutput)] Nothing -> RecError $ "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 else return $ confInput conf !! i -- use !? instead (?) eval _ Hole = FatalError "can't eval hole" ------------ 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 :: Set Resolver, syntExamples :: [[Value]], syntOracle :: Oracle, 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, confProg = expr, 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 {}) _ = False -- sameResults _ (RecError {}) = 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 -- TODO: FIXME separate recoverable & non-recoverable errors -- any isError outputs || matchedExisting <- gets $ evalState (matchAnyOutputs outputs) if any isFatalError 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 modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $ Set.insert (resolverThen r) $ Set.insert (resolverElse r) $ syntUnsolvedGoals st, syntResolvers = r `Set.insert` syntResolvers st } 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 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 (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 = 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 ?) saturateStep :: Expr -> SyntState Bool saturateStep expr = do (newInputs, newOutputs) <- gets $ \st -> unzip $ foldl (searchEx st) [] (syntExamples st) let isExFound = not $ null newInputs when isExFound $ remakeSynt newInputs newOutputs return isExFound 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, syntRoot = root} initSynt :: Oracle -> [([Value], Value)] -> SyntState () initSynt oracle goals = put $ createSynt oracle goals stepOnAddedExpr :: Expr -> SyntState (Maybe Expr) stepOnAddedExpr expr = do exFound <- saturateStep expr if exFound then do -- redo prev exprs (including current) st <- get 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 } gets (foldM_ (const $ trySolveGoal expr) False . syntUnsolvedGoals) -- solve existing goals gets (foldM_ (const tryResolve) Nothing . syntResolvers) -- resolve existing goals modify $ \st -> foldl (splitGoalsFold expr exprOutputs) st $ Set.toList $ syntUnsolvedGoals st return Nothing 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 gets (foldM_ (const $ flip trySolveGoal $ resolverCond r) False . map fst . syntExprs) gets (foldM_ (const $ flip trySolveGoal $ resolverElse r) False . map fst . syntExprs) -- 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 (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 -- 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 -- TODO: throw away exprs with Errors (?) -- 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 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 _ = 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, confProg = reverseExpr, confExamples = allExamples } --- stutter stutterOracle :: Oracle stutterOracle [ListV (x : xs)] = 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, confProg = stutterExpr, confExamples = allExamples } --- length lengthOracle :: Oracle lengthOracle [ListV xs] = Just $ IntV $ length xs lengthOracle _ = Nothing lengthExpr :: Expr lengthExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), ifDoThen = ZeroE, ifDoElse = IncE $ SelfE (TailE (InputE ZeroE) ::: EmptyListE) } lengthConf :: Conf lengthConf = Conf { confInput = head allExamples, confOracle = lengthOracle, confProg = lengthExpr, confExamples = allExamples } --- idOracle :: Oracle idOracle [x] = Just x idOracle _ = Nothing -- TODO: examples main = do steps <- readLn :: IO Int print $ fst $ syntesis steps lengthOracle allExamples