diff --git a/escher.hs b/escher.hs index ebcbf3e..ddc535c 100644 --- a/escher.hs +++ b/escher.hs @@ -6,7 +6,7 @@ import Data.Set (Set, insert, delete) import qualified Data.Map as Map import qualified Data.Set as Set import Data.List (inits) -import Data.Maybe (fromMaybe, isJust) +import Data.Maybe (fromMaybe, isJust, maybeToList) data Value = BoolV Bool | IntV Int @@ -62,14 +62,17 @@ data Conf = Conf {confInput :: [Value], data Result a = Result a | NewExamples [([Value], Value)] - | Error String + | 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' - Error err <*> _ = Error err - _ <*> Error err = Error err + 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 @@ -78,12 +81,14 @@ instance Applicative Result where instance Monad Result where Result x >>= f = f x NewExamples es >>= _ = NewExamples es - Error err >>= _ = Error err + RecError err >>= _ = RecError err + FatalError err >>= _ = FatalError err return = pure instance Alternative Result where - empty = Error "empty" - Error err <|> y = y + 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 @@ -91,7 +96,9 @@ instance Functor Result where fmap = liftM instance MonadFail Result where - fail _ = Error "failure" + fail _ = RecError "failure" -- TODO: fatal ? + +-- instance (Foldable expr) ?? -- TODO: check all laws @@ -108,6 +115,15 @@ 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) @@ -122,6 +138,8 @@ structuralLess (ListV left) (ListV right) = length left < length right 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 @@ -140,7 +158,7 @@ eval conf (IsEmptyE e) = do v <- eval conf e case v of ListV [] -> return $ BoolV True ListV _ -> return $ BoolV False - _ -> Error $ "Can't take empty not from list" ++ show v + _ -> 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 @@ -190,21 +208,21 @@ eval conf (SelfE e) = do ListV newInput <- eval conf e -- guard $ length newInput == length (confInput conf) -- guard $ and $ zipWith structuralLess newInput (confInput conf) if length newInput /= length (confInput conf) - then Error $ "self call different length, new=" ++ show newInput ++ " old=" ++ show (confInput conf) + then RecError $ "self call different length, new=" ++ show newInput ++ " old=" ++ show (confInput conf) else do if not $ and $ zipWith structuralLess newInput (confInput conf) - then Error $ "self call on >= exprs, new=" ++ show newInput ++ " old=" ++ show (confInput conf) + then RecError $ "self call on >= exprs, new=" ++ show newInput ++ " old=" ++ show (confInput conf) else do if newInput `notElem` confExamples conf then (case confOracle conf newInput of Just expectedV -> NewExamples [(newInput, expectedV)] - Nothing -> Error $ "no oracle output on " ++ show newInput) -- TODO: ??? + Nothing -> RecError $ "no oracle output on " ++ show newInput) -- TODO: ??? else eval conf{ confInput = newInput } (confProg conf) 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 Error $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i + then FatalError $ "can't access input " ++ show (confInput conf) ++ " by id " ++ show i else return $ confInput conf !! i -- use !? instead (?) -eval _ Hole = Error "can't eval hole" +eval _ Hole = FatalError "can't eval hole" ------------ @@ -262,6 +280,7 @@ 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 @@ -287,18 +306,19 @@ calcExprOutputs expr = gets (\st -> map (\input -> eval (confBySynt input expr s matchAnyOutputs :: [Result Value] -> SyntState Bool matchAnyOutputs outputs = do exprs <- gets syntExprs - foldM step True $ map fst exprs + foldM step False $ map fst exprs where step :: Bool -> Expr -> SyntState Bool - step False _ = return False - step True expr = do exprOutputs <- calcExprOutputs expr - return $ outputs == exprOutputs + step True _ = return True + step False expr = do exprOutputs <- calcExprOutputs expr + return $ outputs == exprOutputs -- generate next step of exprs, remove copies forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr) forwardStep comp args = do st <- get let expr = fillHoles comp args outputs <- calcExprOutputs expr - if evalState (matchAnyOutputs outputs) st then return Nothing else do + -- TODO: FIXME separate recoverable & non-recoverable errors -- any isError outputs || + if any isFatalError outputs || evalState (matchAnyOutputs outputs) st then return Nothing else do put st { syntExprs = (expr, []) : syntExprs st} return $ Just expr @@ -367,7 +387,7 @@ remakeSynt newInputs newOutputs = do st <- get saturateStep :: Expr -> SyntState Bool saturateStep expr = do st <- get let (newInputs, newOutputs) = unzip $ foldl (searchEx st) [] (syntExamples st) - let isExFound = null newInputs + let isExFound = not $ null newInputs when isExFound $ remakeSynt newInputs newOutputs return isExFound where searchEx st [] input = case eval (confBySynt input expr st) expr of @@ -384,17 +404,18 @@ terminateStep expr = do st <- get ------ patterns patterns0 :: [Expr] -patterns0 = [ZeroE, EmptyListE] +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] +-- IsLeafE Hole, TreeValE Hole, +-- TreeLeftE Hole, TreeRightE Hole, +-- CreateLeafE Hole, SelfE Hole, + InputE Hole + ] patterns2 :: [Expr] patterns2 = [Hole :&&: Hole, @@ -406,8 +427,9 @@ patterns2 = [Hole :&&: Hole, Hole ::: Hole] patterns3 :: [Expr] -patterns3 = [CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole}, - IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}] +patterns3 = [] -- [ +-- CreateNodeE {nodeLeft = Hole, nodeRoot = Hole, nodeRight = Hole}, + -- IfE {ifCond = Hole, ifDoThen = Hole, ifDoElse = Hole}] ------ generation @@ -473,14 +495,18 @@ stepOnAddedExpr expr = do exFound <- saturateStep expr put $ 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 $ or matches then st else - execState (do r <- splitGoalStep goal matches + if any (fromMaybe False) matches then st else + let matchesBool = map (fromMaybe True) matches in + execState (do r <- splitGoalStep goal matchesBool -- TODO: always solve goal trySolveGoal expr (resolverThen r)) st - matchResult (NewExamples {}) _ = False - matchResult _ Nothing = True - matchResult (Result x) (Just y) = x == y - compareExprOutputs outputs False _ = False + 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 @@ -491,12 +517,14 @@ stepOnAddedExprs = foldM step Nothing step Nothing expr = stepOnAddedExpr expr -- TODO: throw away exprs with Errors (?) -stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr) +-- returns result and valid expr +stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr, Maybe Expr) stepOnNewExpr comp args = do st <- get expr <- forwardStep comp args case expr of - Just expr' -> stepOnAddedExpr expr' - Nothing -> return Nothing + Just expr' -> do res <- stepOnAddedExpr expr' + return (res, expr) + Nothing -> return (Nothing, Nothing) -- stages: -- init state @@ -508,33 +536,50 @@ stepOnNewExpr comp args = do st <- get -- 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 providid examples - do let currentExprs = genStep prevExprs - result <- foldM step Nothing currentExprs +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) (map (uncurry fillHoles) currentExprs : prevExprs) - where step res@(Just {}) _ = return res - step Nothing expr = uncurry stepOnNewExpr expr + 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 +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 - evalState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs) + runState (syntesisStep steps exprs) (createSynt oracle $ zip inputs outputs) -syntesis :: Int -> Oracle -> [[Value]] -> Maybe Expr +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 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 -reverseExamples :: [[Value]] -reverseExamples = [[ListV [IntV 1, IntV 2, IntV 3]]] +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] @@ -542,16 +587,41 @@ stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs] stutterOracle [ListV []] = Just $ ListV [] stutterOracle _ = Nothing -stutterExamples :: [[Value]] -stutterExamples = [[ListV [IntV 1, IntV 2, IntV 3]], [ListV [IntV 2, IntV 3]], [ListV [IntV 3]], [ListV []]] - stutterExpr :: Expr -stutterExpr = IfE { ifCond = IsEmptyE (InputE ZeroE), ifDoThen = EmptyListE, ifDoElse = HeadE (InputE ZeroE) ::: (HeadE (InputE ZeroE) ::: SelfE (TailE (InputE ZeroE) ::: EmptyListE)) } +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 stutterExamples, +stutterConf = Conf { confInput = head allExamples, confOracle = stutterOracle, confProg = stutterExpr, - confExamples = stutterExamples } + 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