mirror of
https://codeberg.org/ProgramSnail/prog_synthesis.git
synced 2025-12-05 21:18:42 +00:00
monor fixes, sepated caching eval
This commit is contained in:
parent
f27f6c5559
commit
15cbf78ed5
2 changed files with 54 additions and 32 deletions
|
|
@ -115,11 +115,13 @@ eval conf (InputE i) = do if i < 0 || i >= length (confInput conf) -- NOTE: repl
|
||||||
eval _ Hole = FatalError "can't eval hole"
|
eval _ Hole = FatalError "can't eval hole"
|
||||||
|
|
||||||
|
|
||||||
type Cache = Map Expr (Result Value)
|
type Cache = Map ([Value], 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)
|
|
||||||
|
|
||||||
|
cachedEval :: Cache -> Conf -> Expr -> (Result Value, Cache)
|
||||||
|
cachedEval cache conf expr = let input = confInput conf in
|
||||||
|
case (input, expr) `Map.lookup` cache of
|
||||||
|
Just result -> (result, cache)
|
||||||
|
Nothing -> let result = eval conf expr in
|
||||||
|
(result, if isResult result
|
||||||
|
then Map.insert (input, expr) result cache
|
||||||
|
else cache)
|
||||||
|
|
|
||||||
|
|
@ -16,21 +16,26 @@ import Debug.Trace (trace)
|
||||||
import TypeCheck
|
import TypeCheck
|
||||||
|
|
||||||
|
|
||||||
eval'' :: Conf -> Expr -> SyntState (Result Value)
|
syntEval :: [Value] -> Expr -> SyntState (Result Value)
|
||||||
eval'' conf expr = do cache <- gets syntCache
|
syntEval input expr = do cache <- gets syntCache
|
||||||
let (result, cache') = eval' cache conf expr
|
conf <- gets $ confBySynt input expr
|
||||||
modify $ \st -> st {syntCache = cache'}
|
return $ eval conf expr
|
||||||
return result
|
|
||||||
|
|
||||||
|
syntCacheEval :: [Value] -> Expr -> SyntState (Result Value)
|
||||||
|
syntCacheEval input expr = do cache <- gets syntCache
|
||||||
|
conf <- gets $ confBySynt input expr
|
||||||
|
let (result, cache') = cachedEval cache conf expr
|
||||||
|
modify $ \st -> st {syntCache = cache'}
|
||||||
|
return result
|
||||||
|
|
||||||
------------
|
------------
|
||||||
|
|
||||||
matchGoal :: Goal -> Expr -> Synt -> Bool
|
matchGoal :: Goal -> Expr -> SyntState Bool
|
||||||
matchGoal (Goal goal) expr st = let examples = syntExamples st in
|
matchGoal (Goal goal) expr = do examples <- gets syntExamples
|
||||||
foldl checkOnInput True $ zip examples goal
|
foldM checkOnInput True $ zip examples goal
|
||||||
where checkOnInput False _ = False
|
where checkOnInput False _ = return False
|
||||||
checkOnInput acc (input, output) = let output' = eval (confBySynt input expr st) expr in
|
checkOnInput acc (input, output) = do output' <- syntEval input expr
|
||||||
matchValue output' output -- TODO
|
return $ matchValue output' output -- TODO
|
||||||
matchValue (Result x) (Just y) = x == y
|
matchValue (Result x) (Just y) = x == y
|
||||||
matchValue _ Nothing = True
|
matchValue _ Nothing = True
|
||||||
matchValue _ _ = False
|
matchValue _ _ = False
|
||||||
|
|
@ -38,7 +43,12 @@ matchGoal (Goal goal) expr st = let examples = syntExamples st in
|
||||||
------ syntesis steps
|
------ syntesis steps
|
||||||
|
|
||||||
calcExprOutputs :: Expr -> SyntState [Result Value]
|
calcExprOutputs :: Expr -> SyntState [Result Value]
|
||||||
calcExprOutputs expr = gets (\st -> map (\input -> eval (confBySynt input expr st) expr) $ syntExamples st)
|
calcExprOutputs expr = do examples <- gets syntExamples
|
||||||
|
mapM (`syntEval` expr) examples
|
||||||
|
|
||||||
|
calcTemporaryExprOutputs :: Expr -> SyntState [Result Value]
|
||||||
|
calcTemporaryExprOutputs expr = do examples <- gets syntExamples
|
||||||
|
mapM (`syntEval` expr) examples
|
||||||
|
|
||||||
matchAnyOutputs :: [Result Value] -> SyntState Bool
|
matchAnyOutputs :: [Result Value] -> SyntState Bool
|
||||||
matchAnyOutputs outputs = do exprs <- gets syntExprs
|
matchAnyOutputs outputs = do exprs <- gets syntExprs
|
||||||
|
|
@ -55,11 +65,15 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs
|
||||||
forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
|
forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
|
||||||
forwardStep comp args = do let expr = fillHoles comp args
|
forwardStep comp args = do let expr = fillHoles comp args
|
||||||
typeConf <- gets $ oracleTypes . syntOracle
|
typeConf <- gets $ oracleTypes . syntOracle
|
||||||
if isNothing $ checkType typeConf expr then return Nothing else do
|
if isNothing $ checkType typeConf expr
|
||||||
outputs <- calcExprOutputs expr
|
then return Nothing
|
||||||
matchedExisting <- gets $ evalState (matchAnyOutputs outputs)
|
else do
|
||||||
|
outputs <- calcTemporaryExprOutputs expr
|
||||||
|
matchedExisting <- matchAnyOutputs outputs
|
||||||
-- TODO: all RecErrors example could be useful on future cases ?
|
-- TODO: all RecErrors example could be useful on future cases ?
|
||||||
if any isFatalError outputs || all isRecError outputs || matchedExisting then return Nothing else do
|
if matchedExisting || any isFatalError outputs || all isRecError outputs
|
||||||
|
then return Nothing
|
||||||
|
else do
|
||||||
modify $ \st -> st { syntExprs = (expr, []) : syntExprs st}
|
modify $ \st -> st { syntExprs = (expr, []) : syntExprs st}
|
||||||
return $ Just expr
|
return $ Just expr
|
||||||
|
|
||||||
|
|
@ -74,7 +88,8 @@ splitGoal resolverGoal@(Goal outputs) selector | length outputs == length select
|
||||||
splitGoalStep :: Goal -> [Bool] -> SyntState Resolver
|
splitGoalStep :: Goal -> [Bool] -> SyntState Resolver
|
||||||
splitGoalStep goal selector = do let r = splitGoal goal selector
|
splitGoalStep goal selector = do let r = splitGoal goal selector
|
||||||
resolvers <- gets syntResolvers
|
resolvers <- gets syntResolvers
|
||||||
unless (r `elem` resolvers) $ -- do not add existing resolvers
|
unless (r `elem` resolvers) $ -- do not add existing resolvers -- do not add existing resolvers
|
||||||
|
-- do not add existing resolvers
|
||||||
modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $
|
modify $ \st -> st { syntUnsolvedGoals = Set.insert (resolverCond r) $
|
||||||
Set.insert (resolverThen r) $
|
Set.insert (resolverThen r) $
|
||||||
Set.insert (resolverElse r) $
|
Set.insert (resolverElse r) $
|
||||||
|
|
@ -84,7 +99,7 @@ splitGoalStep goal selector = do let r = splitGoal goal selector
|
||||||
|
|
||||||
-- TODO: use expr evaluated outputs ?
|
-- TODO: use expr evaluated outputs ?
|
||||||
trySolveGoal :: Expr -> Goal -> SyntState Bool
|
trySolveGoal :: Expr -> Goal -> SyntState Bool
|
||||||
trySolveGoal expr goal = do doesMatch <- gets $ matchGoal goal expr
|
trySolveGoal expr goal = do doesMatch <- matchGoal goal expr
|
||||||
if doesMatch then do
|
if doesMatch then do
|
||||||
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st --,
|
modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals st --,
|
||||||
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st
|
-- syntUnsolvedGoals = Set.delete goal $ syntUnsolvedGoals st
|
||||||
|
|
@ -133,19 +148,24 @@ remakeSynt newInputs newOutputs = do st <- get
|
||||||
-- clear goal tree up to root, add example, calculate exprs on input (could be recursive ?)
|
-- clear goal tree up to root, add example, calculate exprs on input (could be recursive ?)
|
||||||
-- returns new example
|
-- returns new example
|
||||||
saturateStep :: Expr -> SyntState [[Value]]
|
saturateStep :: Expr -> SyntState [[Value]]
|
||||||
saturateStep expr = do (newInputs, newOutputs) <- gets $ \st -> unzip $ foldl (searchEx st) [] (syntExamples st)
|
saturateStep expr = do examples <- gets syntExamples
|
||||||
|
(newInputs, newOutputs) <- unzip <$> foldM searchEx [] examples
|
||||||
let exFound = not . null $ newInputs
|
let exFound = not . null $ newInputs
|
||||||
when exFound $ remakeSynt newInputs newOutputs
|
when exFound $ remakeSynt newInputs newOutputs
|
||||||
return newInputs
|
return newInputs
|
||||||
where searchEx st [] input = case eval (confBySynt input expr st) expr of
|
where searchEx [] input = do output <- syntEval input expr
|
||||||
NewExamples exs -> exs
|
return $ case output of
|
||||||
_ -> []
|
NewExamples exs -> exs
|
||||||
searchEx _ exs _ = exs
|
_ -> []
|
||||||
|
searchEx exs _ = return exs
|
||||||
|
|
||||||
-- try to find terminating expr
|
-- try to find terminating expr
|
||||||
terminateStep :: Expr -> SyntState (Maybe Expr)
|
terminateStep :: Expr -> SyntState (Maybe Expr)
|
||||||
terminateStep expr = do doesMatch <- gets $ \st -> matchGoal (syntRoot st) expr st
|
terminateStep expr = do rootGoal <- gets syntRoot
|
||||||
return $ if doesMatch then Just expr else Nothing
|
gets $ Map.lookup rootGoal . syntSolvedGoals
|
||||||
|
-- NOTE: Goal should be already solved earlier
|
||||||
|
-- doesMatch <- matchGoal rootGoal expr
|
||||||
|
-- return $ if doesMatch then Just expr else Nothing
|
||||||
|
|
||||||
stepOnAddedExpr :: Expr -> SyntState (Maybe Expr)
|
stepOnAddedExpr :: Expr -> SyntState (Maybe Expr)
|
||||||
stepOnAddedExpr expr = do newEx <- saturateStep expr
|
stepOnAddedExpr expr = do newEx <- saturateStep expr
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue