11module Main
22 ( main
33 ) where
4-
54import Control.Exception ( SomeException
65 , catch
76 )
7+ import Control.Lens ( (.~)
8+ , (^.)
9+ )
810import Control.Monad.State
9- import Data.Function ( (&) )
10- import Control.Lens ( (.~) , (^.) )
1111import qualified Data.ByteString.Lazy.Char8 as LB
12+ import Data.Function ( (&) )
1213import Data.Time.Calendar ( Day
1314 , fromGregorian
1415 , showGregorian
@@ -29,11 +30,11 @@ import qualified Evaluation.Benchmark
2930import Evaluation.EvalTypeInf
3031import Evaluation.ReadBenchmark
3132import Examples.InferenceDriver
32- import qualified Hectare.TermSearch as Hectare
33- import Postfilter.GHCChecker
33+ import qualified Hectare.TermSearch as Hectare
3434import HooglePlus.IOFormat
3535import HooglePlus.Synthesize
3636import PetriNet.PNSolver
37+ import Postfilter.GHCChecker
3738import Types.Environment
3839import Types.Experiments
3940import Types.Filtering
@@ -215,11 +216,12 @@ precomputeGraph :: GenerationOpts -> IO ()
215216precomputeGraph = generateEnv
216217
217218-- | Parse and resolve file, then synthesize the specified goals
218- executeSearch :: SearchEngine -> SearchParams -> String -> OutputFormat -> FilePath -> IO ()
219+ executeSearch
220+ :: SearchEngine -> SearchParams -> String -> OutputFormat -> FilePath -> IO ()
219221executeSearch engine params inStr outputFormat outputFile = catch
220222 (do
221- let input = decodeInput (LB. pack inStr)
222- let tquery = query input
223+ let input = decodeInput (LB. pack inStr)
224+ let tquery = query input
223225 let examples = inExamples input
224226 hSetBuffering stdout LineBuffering
225227
@@ -228,59 +230,78 @@ executeSearch engine params inStr outputFormat outputFile = catch
228230 when (outputFormat == OutputFile && exists) $ removeFile outputFile
229231
230232 -- invoke synthesis
231- let cnt = params ^. solutionCnt
232233 case engine of
233- HooglePlus -> envToGoal loadEnv tquery examples >>= \ goal -> runHooglePlus goal cnt
234- Hectare -> envToGoal loadEnvFo tquery examples >>= \ goal -> runHectare goal
234+ HooglePlus ->
235+ envToGoal loadEnv tquery examples >>= \ goal -> runHooglePlus goal
236+ Hectare ->
237+ envToGoal loadEnvFo tquery examples >>= \ goal -> runHectare goal
235238 )
236239 (\ (e :: SomeException ) -> do
237240 printResult $ encodeWithPrefix $ QueryOutput [] (show e) []
238241 error (show e)
239242 )
240243
241- where
242- runHooglePlus :: Goal -> Int -> IO ()
243- runHooglePlus goal n = do
244- (programs, st) <- synthesize params goal
245- let initState = (st ^. filterState) { flogLevel = params ^. logLevel }
246- (cnt, fstate) <- getKPrograms goal (0 , initState) programs
247- when (cnt < n)
248- (getMoreSolutions goal (st & filterState .~ fstate) (n - cnt))
244+ where
245+ runHooglePlus :: Goal -> IO ()
246+ runHooglePlus goal = do
247+ (programs, st) <- synthesize params goal
248+ let initState = (st ^. filterState) { flogLevel = params ^. logLevel }
249+ (cnt, fstate) <- getKPrograms goal (0 , initState) programs
250+ let appDepth = params ^. maxApplicationDepth
251+ let currLen = st ^. (searchState . currentLoc)
252+ when (cnt < params ^. solutionCnt && currLen <= appDepth)
253+ (getMoreSolutions goal (st & filterState .~ fstate) cnt)
249254
250- getMoreSolutions :: Goal -> SolverState -> Int -> IO ()
251- getMoreSolutions goal@ (Goal env goalTyp _) st n = do
252- if n <= 0 then return ()
253- else do
254- (programs, st') <- runStateT (nextSolution env goalTyp) st
255- (cnt, fstate) <- getKPrograms goal (0 , st' ^. filterState) programs
256- when (cnt < n)
257- (getMoreSolutions goal (st' & filterState .~ fstate) (n - cnt))
255+ getMoreSolutions :: Goal -> SolverState -> Int -> IO ()
256+ getMoreSolutions goal@ (Goal env goalTyp _) st n = do
257+ if n >= params ^. solutionCnt
258+ then return ()
259+ else do
260+ (programs, st' ) <- runStateT (nextSolution env goalTyp) st
261+ (cnt , fstate) <- getKPrograms goal (0 , st' ^. filterState) programs
262+ let appDepth = params ^. maxApplicationDepth
263+ let currLen = st' ^. (searchState . currentLoc)
264+ when (n + cnt < params ^. solutionCnt && currLen <= appDepth)
265+ (getMoreSolutions goal (st' & filterState .~ fstate) (n + cnt))
258266
259- runHectare :: Goal -> IO ()
260- runHectare goal = do
261- let programs = Hectare. synthesize goal
262- -- print programs
263- (synthesisCnt, _) <- getKPrograms goal (0 , emptyFilterState { flogLevel = params ^. logLevel }) programs
264- when (synthesisCnt < params ^. solutionCnt) $ putStrLn " Hectare cannot find more solutions"
267+ runHectare :: Goal -> IO ()
268+ runHectare goal = do
269+ let programs = Hectare. synthesize goal
270+ -- print programs
271+ (synthesisCnt, _) <- getKPrograms
272+ goal
273+ (0 , emptyFilterState { flogLevel = params ^. logLevel })
274+ programs
275+ when (synthesisCnt < params ^. solutionCnt)
276+ $ putStrLn " Hectare cannot find more solutions"
265277
266- getKPrograms :: Goal -> (Int , FilterState ) -> [TProgram ] -> IO (Int , FilterState )
267- getKPrograms _ (n, fstate) _ | n == (params ^. solutionCnt) = return (n, fstate)
268- getKPrograms _ (n, fstate) [] = return (n, fstate)
269- getKPrograms goal (n, fstate) (p: ps) = do
270- (fstate', mbProgram) <- runPostFilter goal n fstate p
271- case mbProgram of
272- Nothing -> getKPrograms goal (n, fstate') ps
273- Just _ -> getKPrograms goal (n + 1 , fstate') ps
278+ getKPrograms
279+ :: Goal -> (Int , FilterState ) -> [TProgram ] -> IO (Int , FilterState )
280+ getKPrograms _ (n, fstate) _ | n == (params ^. solutionCnt) =
281+ return (n, fstate)
282+ getKPrograms _ (n, fstate) [] = return (n, fstate)
283+ getKPrograms goal (n, fstate) (p : ps) = do
284+ (fstate', mbProgram) <- runPostFilter goal n fstate p
285+ case mbProgram of
286+ Nothing -> getKPrograms goal (n, fstate') ps
287+ Just _ -> getKPrograms goal (n + 1 , fstate') ps
274288
275- runPostFilter :: Goal -> Int -> FilterState -> TProgram -> IO (FilterState , Maybe TProgram )
276- runPostFilter (Goal env goalType examples) cnt fstate p = do
277- (checkResult, fstate') <- runStateT (checkSolution params env goalType examples p) fstate
278- case checkResult of
279- Nothing -> return (fstate', Nothing )
280- Just exs -> do
281- queryOutput <- liftIO $ toOutput env p exs
282- case outputFormat of
283- JSON -> liftIO $ printResult $ encodeWithPrefix queryOutput
284- CommandLine -> liftIO $ printCmd cnt queryOutput Nothing
285- OutputFile -> liftIO $ printCmd cnt queryOutput (Just outputFile)
286- return (fstate', Just p)
289+ runPostFilter
290+ :: Goal
291+ -> Int
292+ -> FilterState
293+ -> TProgram
294+ -> IO (FilterState , Maybe TProgram )
295+ runPostFilter (Goal env goalType examples) cnt fstate p = do
296+ (checkResult, fstate') <- runStateT
297+ (checkSolution params env goalType examples p)
298+ fstate
299+ case checkResult of
300+ Nothing -> return (fstate', Nothing )
301+ Just exs -> do
302+ queryOutput <- liftIO $ toOutput env p exs
303+ case outputFormat of
304+ JSON -> liftIO $ printResult $ encodeWithPrefix queryOutput
305+ CommandLine -> liftIO $ printCmd cnt queryOutput Nothing
306+ OutputFile -> liftIO $ printCmd cnt queryOutput (Just outputFile)
307+ return (fstate', Just p)
0 commit comments