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