diff --git a/escher.hs b/escher.hs index fb24172..ebcbf3e 100644 --- a/escher.hs +++ b/escher.hs @@ -27,6 +27,9 @@ data Type = BoolT data Expr = Expr :&&: Expr -- Bool | Expr :||: Expr | NotE Expr + | Expr :=: Expr + | Leq0 Expr + | IsEmptyE Expr | Expr :+: Expr -- Int | Expr :-: Expr | IncE Expr @@ -59,14 +62,14 @@ data Conf = Conf {confInput :: [Value], data Result a = Result a | NewExamples [([Value], Value)] - | Error + | Error String deriving (Read, Show, Eq) instance Applicative Result where Result f <*> Result x = Result $ f x NewExamples es <*> NewExamples es' = NewExamples $ es ++ es' - Error <*> _ = Error - _ <*> Error = Error + Error err <*> _ = Error err + _ <*> Error err = Error err NewExamples es <*> _ = NewExamples es _ <*> NewExamples es = NewExamples es pure = Result @@ -75,12 +78,12 @@ instance Applicative Result where instance Monad Result where Result x >>= f = f x NewExamples es >>= _ = NewExamples es - Error >>= _ = Error + Error err >>= _ = Error err return = pure instance Alternative Result where - empty = Error - Error <|> y = y + empty = Error "empty" + Error err <|> y = y NewExamples es <|> _ = NewExamples es r@(Result x) <|> _ = r @@ -88,7 +91,7 @@ instance Functor Result where fmap = liftM instance MonadFail Result where - fail _ = Error + fail _ = Error "failure" -- TODO: check all laws @@ -105,12 +108,18 @@ isInt = (== IntT) . typeOf isList = (== ListT) . typeOf isTree = (== TreeT) . typeOf +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) = left < right +structuralLess (BoolV left) (BoolV right) = not left && right structuralLess (IntV left) (IntV right) = left < right && left > 0 -- ?? -structuralLess (ListV left) (ListV right) = left < right -structuralLess (TreeV left) (TreeV right) = left < right +-- 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 @@ -122,6 +131,16 @@ eval conf (left :||: right) = do BoolV leftB <- eval conf left 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 + _ -> Error $ "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 @@ -167,16 +186,25 @@ eval conf (CreateLeafE e) = do v <- eval conf e 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 newInput <- eval conf e - guard $ and $ zipWith structuralLess newInput (confInput 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) + -- NOTE: replaced guards for better errors description + -- 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) + else do + if not $ and $ zipWith structuralLess newInput (confInput conf) + then Error $ "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: ??? + 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 _ Hole = Error + 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 + else return $ confInput conf !! i -- use !? instead (?) +eval _ Hole = Error "can't eval hole" ------------ @@ -209,6 +237,9 @@ 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 @@ -245,18 +276,31 @@ matchGoal (Goal goal) st expr = let examples = syntExamples st in 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 (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 True $ map fst exprs + where step :: Bool -> Expr -> SyntState Bool + step False _ = return False + step True expr = do exprOutputs <- calcExprOutputs expr + return $ outputs == exprOutputs + -- generate next step of exprs, remove copies -forwardStep :: Expr -> [Expr] -> SyntState Expr +forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr) forwardStep comp args = do st <- get let expr = fillHoles comp args - put st { syntExprs = (expr, []) : syntExprs st} - return expr + outputs <- calcExprOutputs expr + if evalState (matchAnyOutputs outputs) st then return Nothing else do + put st { syntExprs = (expr, []) : syntExprs st} + return $ Just expr splitGoal :: Goal -> [Bool] -> Resolver splitGoal resolverGoal@(Goal outputs) selector | length outputs == length selector = @@ -266,7 +310,7 @@ splitGoal resolverGoal@(Goal outputs) selector | length outputs == length select 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 -> [Bool] -> SyntState Resolver splitGoalStep goal selector = do st <- get let r = splitGoal goal selector put st { syntUnsolvedGoals = Set.insert (resolverCond r) $ @@ -274,6 +318,7 @@ splitGoalStep goal selector = do st <- get Set.insert (resolverElse r) $ syntUnsolvedGoals st, syntResolvers = r : syntResolvers st } + return r -- TODO: use expr evaluated outputs ? trySolveGoal :: Expr -> Goal -> SyntState Bool @@ -342,7 +387,8 @@ patterns0 :: [Expr] patterns0 = [ZeroE, EmptyListE] patterns1 :: [Expr] -patterns1 = [NotE Hole, IncE Hole, +patterns1 = [NotE Hole, Leq0 Hole, + IsEmptyE Hole, IncE Hole, DecE Hole, Div2E Hole, TailE Hole, HeadE Hole, IsLeafE Hole, TreeValE Hole, @@ -353,6 +399,7 @@ patterns1 = [NotE Hole, IncE Hole, patterns2 :: [Expr] patterns2 = [Hole :&&: Hole, Hole :||: Hole, + Hole :=: Hole, Hole :+: Hole, Hole :-: Hole, Hole :++: Hole, @@ -411,27 +458,31 @@ createSynt oracle goals = let root = Goal $ map (Just . snd) goals in initSynt :: Oracle -> [([Value], Value)] -> SyntState () initSynt oracle goals = put $ createSynt oracle goals -calcExprOutputs :: Expr -> SyntState [Result Value] -calcExprOutputs expr = gets (\st -> map (\input -> eval (confBySynt input expr st) expr) $ syntExamples st) - stepOnAddedExpr :: Expr -> SyntState (Maybe Expr) stepOnAddedExpr expr = do exFound <- saturateStep expr st <- get if exFound then stepOnAddedExprs $ map fst $ syntExprs st else do -- redo prev exprs (including current) maybeResult <- terminateStep expr if isJust maybeResult then return maybeResult else do - let exprOutputs = map (\input -> eval (confBySynt input expr st) expr) $ syntExamples st - -- TODO: remove copies + exprOutputs <- calcExprOutputs expr + -- TODO + -- 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) False . syntResolvers)-- resolve existing goals - put $ foldl (splitGoalsFold exprOutputs) st $ Set.toList $ syntUnsolvedGoals st + st <- get + put $ foldl (splitGoalsFold expr exprOutputs) st $ Set.toList $ syntUnsolvedGoals st return Nothing - where splitGoalsFold outputs st goal@(Goal expected) = let matches = zipWith matchResult outputs expected in - if not $ or matches then st else - execState (splitGoalStep goal matches) st + 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 + -- 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 + -- compareExprOutputs outputs True e = do eOutputs <- calcExprOutputs e + -- outputs == eOutputs stepOnAddedExprs :: [Expr] -> SyntState (Maybe Expr) stepOnAddedExprs = foldM step Nothing @@ -439,10 +490,13 @@ stepOnAddedExprs = foldM step Nothing step res@(Just {}) _ = return res step Nothing expr = stepOnAddedExpr expr +-- TODO: throw away exprs with Errors (?) stepOnNewExpr :: Expr -> [Expr] -> SyntState (Maybe Expr) stepOnNewExpr comp args = do st <- get expr <- forwardStep comp args - stepOnAddedExpr expr + case expr of + Just expr' -> stepOnAddedExpr expr' + Nothing -> return Nothing -- stages: -- init state @@ -471,4 +525,33 @@ syntesis' exprs steps oracle inputs = -- oracle should be defined on the providi syntesis :: Int -> Oracle -> [[Value]] -> Maybe Expr syntesis = syntesis' [] +------ examples + +reverseOracle :: Oracle +reverseOracle [ListV xs] = Just $ ListV $ reverse xs +reverseOracle _ = Nothing + +reverseExamples :: [[Value]] +reverseExamples = [[ListV [IntV 1, IntV 2, IntV 3]]] + +--- + +stutterOracle :: Oracle +stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs] + return $ ListV $ x : x : 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)) } + +stutterConf :: Conf +stutterConf = Conf { confInput = head stutterExamples, + confOracle = stutterOracle, + confProg = stutterExpr, + confExamples = stutterExamples } + -- TODO: examples