diff --git a/escher/Eval.hs b/escher/Eval.hs new file mode 100644 index 0000000..b211050 --- /dev/null +++ b/escher/Eval.hs @@ -0,0 +1,122 @@ +module Eval where + +import Expr +import Data.Map (Map) +import qualified Data.Map.Lazy as Map +import Control.Monad (foldM) + +import Debug.Trace (trace) + +type Oracle = [Value] -> Maybe Value + +data Conf = Conf {confInput :: [Value], + confOracle :: Oracle, + confExamples :: [[Value]]} + +-- 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 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" + + +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) + diff --git a/escher/Expr.hs b/escher/Expr.hs new file mode 100644 index 0000000..649a426 --- /dev/null +++ b/escher/Expr.hs @@ -0,0 +1,102 @@ +module Expr where + +import Control.Applicative +import Control.Monad (liftM) + +data Tree a = TNode { treeLeft :: Tree a, treeRoot :: a, treeRight :: Tree a } + | TLeaf a + 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 Int + | Hole + deriving (Read, Show, Eq, Ord) + +data Value = BoolV Bool + | IntV Int + | ListV [Value] + | TreeV (Tree Value) + deriving (Read, Show, Eq, Ord) + +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 + +------------ + +isResult (Result {}) = True +isResult _ = False +isNewExamples (NewExamples {}) = True +isNewExamples _ = False +isRecError (RecError {}) = True +isRecError _ = False +isFatalError (FatalError {}) = True +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 new file mode 100644 index 0000000..e435f27 --- /dev/null +++ b/escher/Main.hs @@ -0,0 +1,297 @@ +import Expr +import Eval +import Syntesis + +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) +import TypeCheck + + +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 + + +------------ + +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 + +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 0), + ifDoThen = EmptyListE, + ifDoElse = SelfE [TailE (InputE 0)] :++: (HeadE (InputE 0) ::: 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 0), + ifDoThen = EmptyListE, + ifDoElse = HeadE (InputE 0) ::: (HeadE (InputE 0) ::: SelfE [TailE (InputE 0)]) } + +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 0), + ifDoThen = ZeroE, + ifDoElse = IncE $ SelfE [TailE (InputE 0)] } + +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)}) diff --git a/escher/Syntesis.hs b/escher/Syntesis.hs new file mode 100644 index 0000000..47c2e4d --- /dev/null +++ b/escher/Syntesis.hs @@ -0,0 +1,152 @@ +module Syntesis where + +import Expr +import Eval +import Control.Monad.State +import Data.Map.Lazy (Map) +import Data.Set (Set) +import Data.List (inits) +import qualified Data.Map.Lazy as Map +import qualified Data.Set as Set + +-- 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 hs) es | all (== Hole) hs && length hs == length es = SelfE es + -- | otherwise = error $ show hs ++ show es +fillHoles (InputE i) [] = InputE i +fillHoles e es = error $ "Can't fill holes in " ++ show e ++ " with " ++ show es + +confBySynt :: [Value] -> Expr -> Synt -> Conf +confBySynt input expr st = Conf {confInput = input, + confOracle = syntOracle st, + confExamples = syntExamples st} + + +------ patterns + +patterns0 :: [Expr] +patterns0 = [ZeroE, EmptyListE, InputE 0] -- 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] + ] + +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 diff --git a/escher/TypeCheck.hs b/escher/TypeCheck.hs new file mode 100644 index 0000000..1679175 --- /dev/null +++ b/escher/TypeCheck.hs @@ -0,0 +1,101 @@ +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 +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 x | ListT {} <- typeOf x = True + | otherwise = False +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 + 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