From 3fe524b5a0bb8614710458bc042f31814ea4a8d9 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Mon, 27 Oct 2025 01:47:15 +0300 Subject: [PATCH] main, fixes, works for length & reverse (for int lists) --- escher.hs | 68 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 35 insertions(+), 33 deletions(-) diff --git a/escher.hs b/escher.hs index 38a7ad3..99d6d5a 100644 --- a/escher.hs +++ b/escher.hs @@ -1,4 +1,6 @@ -import Control.Monad (guard, liftM, when, foldM, foldM_) +-- NOTE: it will be important to remove gets on caching addition + +import Control.Monad (guard, liftM, when, unless, foldM, foldM_) import Control.Applicative import Control.Monad.State as State import Data.Map (Map) @@ -88,7 +90,7 @@ instance Monad Result where return = pure instance Alternative Result where - empty = undefined -- TMP: no guards used -- FatalError "empty" -- TODO: fatal ? + empty = undefined -- TMP: no guards used -- FatalError "empty" -- TODO: rec ? RecError err <|> y = y FatalError err <|> y = y NewExamples es <|> _ = NewExamples es @@ -140,8 +142,6 @@ 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 @@ -210,7 +210,7 @@ eval conf (SelfE e) = do ListV recInput <- eval conf e -- 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) + 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) @@ -218,11 +218,11 @@ eval conf (SelfE e) = do ListV recInput <- eval conf e 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 + else NewExamples $ trace ("newExample: " ++ show [(recInput, recOutput)]) [(recInput, recOutput)] + Nothing -> FatalError $ "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 + 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" @@ -245,7 +245,7 @@ data Resolver = Resolver { resolverGoal :: Goal, data Synt = Synt { syntExprs :: [(Expr, [Maybe Value])], syntSolvedGoals :: Map Goal Expr, syntUnsolvedGoals :: Set Goal, - syntResolvers :: Set Resolver, + syntResolvers :: [Resolver], -- Set Resolver, syntExamples :: [[Value]], syntOracle :: Oracle, syntRoot :: Goal} @@ -322,9 +322,9 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs 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 + -- 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 @@ -338,11 +338,13 @@ splitGoal resolverGoal@(Goal outputs) selector | length outputs == length select -- 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 } + 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 ? @@ -353,8 +355,7 @@ trySolveGoal expr goal = do doesMatch <- gets $ matchGoal goal expr -- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st } return True - -- trace ("goal solved: " ++ show goal) -- TODO: trace - -- return True + -- trace ("goal solved: " ++ show goal) -- Tmp: trace else return False isGoalSolved :: Goal -> SyntState Bool @@ -367,7 +368,7 @@ goalSolution goal = gets (Map.lookup goal . syntSolvedGoals) -- returns found expr -- NOTE: goals expected to be resolved resolveStep :: (Expr, Expr, Expr) -> Resolver -> SyntState Expr --- resolveStep r _ | trace ("resolution: " ++ show r) False = undefined -- TODO: trace +-- 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, @@ -376,7 +377,7 @@ resolveStep (ifCond, ifDoThen, ifDoElse) r = do let expr = IfE { ifCond, ifDoThe return expr tryResolve :: Resolver -> SyntState (Maybe Expr) --- tryResolve r | trace ("try resolution: " ++ show r) False = undefined -- TODO +-- 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 @@ -483,7 +484,7 @@ createSynt oracle goals = let root = Goal $ map (Just . snd) goals in Synt { syntExprs = [], syntSolvedGoals = Map.empty, syntUnsolvedGoals = Set.singleton root, - syntResolvers = Set.empty, + syntResolvers = [], -- Set.empty syntExamples = map fst goals, syntOracle = oracle, syntRoot = root} @@ -495,7 +496,7 @@ 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) $ -- TODO: trace + -- trace ("exFound: " ++ show newEx) $ -- TMP: trace stepOnAddedExprs $ map fst $ syntExprs st else do -- try resolve goals & resolvers, generate new resolvers maybeResult <- terminateStep expr @@ -507,7 +508,7 @@ stepOnAddedExpr expr = do newEx <- saturateStep expr 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 $ Set.toList $ syntUnsolvedGoals st + 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 @@ -535,7 +536,6 @@ stepOnAddedExprs = foldM step Nothing 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 @@ -559,7 +559,7 @@ syntesisStep steps prevExprs = -- oracle should be defined on the provided emamp (result, validExprs) <- foldM step (Nothing, []) genExprs if isJust result then return result - else syntesisStep (steps - 1) (validExprs : prevExprs) + 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) @@ -578,13 +578,14 @@ 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 []]] +-- 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] = Just $ ListV $ reverse xs +reverseOracle [ListV xs] | all isInt xs = Just $ ListV $ reverse xs reverseOracle _ = Nothing reverseExpr :: Expr @@ -601,8 +602,8 @@ reverseConf = Conf { confInput = head allExamples, --- stutter stutterOracle :: Oracle -stutterOracle [ListV (x : xs)] = do ListV xs' <- stutterOracle [ListV xs] - return $ ListV $ x : x : xs' +stutterOracle [ListV (x : xs)] | isInt x = do ListV xs' <- stutterOracle [ListV xs] + return $ ListV $ x : x : xs' stutterOracle [ListV []] = Just $ ListV [] stutterOracle _ = Nothing @@ -640,7 +641,8 @@ idOracle :: Oracle idOracle [x] = Just x idOracle _ = Nothing --- TODO: examples - main = do steps <- readLn :: IO Int - print $ fst $ syntesis steps lengthOracle allExamples + 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)})