diff --git a/escher/Eval.hs b/escher/Eval.hs index 3dfec0e..3d7a646 100644 --- a/escher/Eval.hs +++ b/escher/Eval.hs @@ -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" -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) +type Cache = Map ([Value], Expr) (Result Value) +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) diff --git a/escher/Main.hs b/escher/Main.hs index 77fbd3f..347fba4 100644 --- a/escher/Main.hs +++ b/escher/Main.hs @@ -16,21 +16,26 @@ 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 +syntEval :: [Value] -> Expr -> SyntState (Result Value) +syntEval input expr = do cache <- gets syntCache + conf <- gets $ confBySynt input expr + return $ eval conf expr +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 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 +matchGoal :: Goal -> Expr -> SyntState Bool +matchGoal (Goal goal) expr = do examples <- gets syntExamples + foldM checkOnInput True $ zip examples goal + where checkOnInput False _ = return False + checkOnInput acc (input, output) = do output' <- syntEval input expr + return $ matchValue output' output -- TODO matchValue (Result x) (Just y) = x == y matchValue _ Nothing = True matchValue _ _ = False @@ -38,7 +43,12 @@ matchGoal (Goal goal) expr st = let examples = syntExamples st in ------ syntesis steps 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 outputs = do exprs <- gets syntExprs @@ -55,11 +65,15 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr) forwardStep comp args = do let expr = fillHoles comp args typeConf <- gets $ oracleTypes . syntOracle - if isNothing $ checkType typeConf expr then return Nothing else do - outputs <- calcExprOutputs expr - matchedExisting <- gets $ evalState (matchAnyOutputs outputs) + if isNothing $ checkType typeConf expr + then return Nothing + else do + outputs <- calcTemporaryExprOutputs expr + matchedExisting <- 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 + if matchedExisting || any isFatalError outputs || all isRecError outputs + then return Nothing + else do modify $ \st -> st { syntExprs = (expr, []) : syntExprs st} return $ Just expr @@ -74,7 +88,8 @@ splitGoal resolverGoal@(Goal outputs) selector | length outputs == length select 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 + 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) $ Set.insert (resolverThen r) $ Set.insert (resolverElse r) $ @@ -84,7 +99,7 @@ splitGoalStep goal selector = do let r = splitGoal goal selector -- TODO: use expr evaluated outputs ? 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 modify $ \st -> st { syntSolvedGoals = Map.insert goal expr $ syntSolvedGoals 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 ?) -- returns new example 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 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 + where searchEx [] input = do output <- syntEval input expr + return $ case output of + NewExamples exs -> exs + _ -> [] + searchEx exs _ = return 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 +terminateStep expr = do rootGoal <- gets syntRoot + 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 = do newEx <- saturateStep expr