Reducer refactor (#211)

* Defining new, easier to read, functions for combining reducers * Adjusted quasiquote reducer * Cleaning up Reducers * Documentation --------- Co-authored-by: Bill Hallahan <[email protected]>
BillHallahan · Oct 3, 2023 · 5a29b69 · 5a29b69
1 parent db1fb5c
commit 5a29b69
Show file tree

Hide file tree

Showing 8 changed files with 175 additions and 165 deletions.
diff --git a/src/G2/Equiv/G2Calls.hs b/src/G2/Equiv/G2Calls.hs
@@ -90,16 +90,13 @@ rewriteRedHaltOrd solver simplifier h_opp track_opp config (NC { use_labeled_err
  state_name = Name "state" Nothing 0 Nothing
 
  m_logger = fmap SomeReducer $ getLogger config
+ some_std_red = enforceProgressRed :== NoProgress --> stdRed share retReplaceSymbFuncVar solver simplifier
+ extra_red = symbolicSwapperRed h_opp track_opp ~> concSymReducer use_labels ~> labeledErrorsRed
+ red = equivReducer :== NoProgress .--> extra_red :== NoProgress .--> some_std_red
  in
  (case m_logger of
- Just logger -> SomeReducer (
- (stdRed share retReplaceSymbFuncVar solver simplifier <~?
- enforceProgressRed) <~? labeledErrorsRed <~ concSymReducer use_labels <~ symbolicSwapperRed h_opp track_opp) .<~?
- (logger .<~ SomeReducer equivReducer)
- Nothing -> SomeReducer (
- ((stdRed share retReplaceSymbFuncVar solver simplifier <~?
- enforceProgressRed) <~? labeledErrorsRed <~ concSymReducer use_labels <~ symbolicSwapperRed h_opp track_opp) <~?
- equivReducer)
+ Just logger -> logger .~> red 
+ Nothing -> red 
  , SomeHalter
  (discardIfAcceptedTagHalter state_name
  <~> enforceProgressHalter

diff --git a/src/G2/Execution/Interface.hs b/src/G2/Execution/Interface.hs
@@ -10,14 +10,12 @@ import G2.Execution.Reducer
 import G2.Execution.Rules
 import G2.Language.Support
 
-import Control.Monad.IO.Class 
-
 {-# INLINE runExecutionToProcessed #-}
-runExecutionToProcessed :: (MonadIO m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m (Processed (State t), Bindings)
+runExecutionToProcessed :: (Monad m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m (Processed (State t), Bindings)
 runExecutionToProcessed = runReducer
 
 {-# INLINE runExecution #-}
-runExecution :: (MonadIO m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m ([State t], Bindings)
+runExecution :: (Monad m, Ord b) => Reducer m rv t -> Halter m hv t -> Orderer sov b t -> State t -> Bindings -> m ([State t], Bindings)
 runExecution r h ord s b = do
  (pr, b') <- runReducer r h ord s b
  return (accepted pr, b')
diff --git a/src/G2/Execution/Reducer.hs b/src/G2/Execution/Reducer.hs
diff --git a/src/G2/Interface/Interface.hs b/src/G2/Interface/Interface.hs
@@ -262,24 +262,22 @@ initRedHaltOrd solver simplifier config =
  state_name = Name "state" Nothing 0 Nothing
 
  m_logger = fmap SomeReducer $ getLogger config
+
+ logger_std_red f = case m_logger of
+ Just logger -> logger .~> SomeReducer (stdRed share f solver simplifier)
+ Nothing -> SomeReducer (stdRed share f solver simplifier)
  in
  case higherOrderSolver config of
  AllFuncs ->
- (SomeReducer (nonRedPCRed)
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier))
+ ( logger_std_red retReplaceSymbFuncVar .== Finished .--> SomeReducer nonRedPCRed
  , SomeHalter
  (switchEveryNHalter 20
  <~> maxOutputsHalter (maxOutputs config)
  <~> zeroHalter (steps config)
  <~> acceptIfViolatedHalter)
  , SomeOrderer $ pickLeastUsedOrderer)
  SingleFunc ->
- ( SomeReducer (nonRedPCRed <~| taggerRed state_name)
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier))
+ ( logger_std_red retReplaceSymbFuncVar .== Finished .--> taggerRed state_name :== Finished --> nonRedPCRed
  , SomeHalter
  (discardIfAcceptedTagHalter state_name
  <~> switchEveryNHalter 20
@@ -288,10 +286,7 @@ initRedHaltOrd solver simplifier config =
  <~> acceptIfViolatedHalter)
  , SomeOrderer $ pickLeastUsedOrderer)
  SymbolicFunc ->
- (SomeReducer (nonRedPCRed)
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncTemplate solver simplifier) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncTemplate solver simplifier))
+ ( logger_std_red retReplaceSymbFuncTemplate .== Finished .--> SomeReducer nonRedPCRed
  , SomeHalter
  (switchEveryNHalter 20
  <~> maxOutputsHalter (maxOutputs config)
@@ -437,7 +432,7 @@ runG2WithSomes red hal ord solver simplifier mem state bindings =
 runG2Pre :: ( Named t
  , ASTContainer t Expr
  , ASTContainer t Type) => MemConfig -> State t -> Bindings -> (State t, Bindings)
-runG2Pre mem s@(State { known_values = kv, type_classes = tc }) bindings =
+runG2Pre mem s bindings =
  let
  (swept, bindings') = markAndSweepPreserving mem s bindings
  in
@@ -470,7 +465,7 @@ runG2Post red hal ord solver simplifier is bindings = do
  , Ord b) => Reducer (SM.StateT PrettyGuide IO) rv t -> Halter (SM.StateT PrettyGuide IO) hv t -> Orderer sov b t ->
  MemConfig -> State t -> Bindings -> SM.StateT PrettyGuide IO ([State t], Bindings) #-}
 runG2ThroughExecution ::
- ( MonadIO m
+ ( Monad m
  , Named t
  , ASTContainer t Expr
  , ASTContainer t Type

diff --git a/src/G2/Liquid/G2Calls.hs b/src/G2/Liquid/G2Calls.hs
@@ -127,7 +127,7 @@ checkAbstracted' g2call solver simplifier share s bindings abs_fc@(FuncCall { fu
 
  let pres = HS.fromList $ namesList s' ++ namesList bindings
  (er, bindings') <- g2call 
- (SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ hitsLibError))
+ (SomeReducer (hitsLibError ~> stdRed share retReplaceSymbFuncVar solver simplifier))
  (SomeHalter (swhnfHalter <~> acceptOnlyOneHalter <~> switchEveryNHalter 200))
  (SomeOrderer (incrAfterN 2000 (adtSizeOrderer 0 Nothing)))
  solver simplifier
@@ -181,8 +181,8 @@ getAbstracted g2call solver simplifier share s bindings abs_fc@(FuncCall { funcN
  , track = ([] :: [FuncCall], False)}
 
  (er, bindings') <- g2call 
- (SomeReducer ((nonRedPCRed .|. nonRedPCRedConst)
-  <~| (stdRed share retReplaceSymbFuncVar solver simplifier <~ hitsLibErrorGatherer)))
+ (((hitsLibErrorGatherer ~> stdRed share retReplaceSymbFuncVar solver simplifier) :== Finished
+ --> (nonRedPCRed .|. nonRedPCRedConst) ))
  (SomeHalter (swhnfHalter <~> acceptOnlyOneHalter <~> switchEveryNHalter 200))
  (SomeOrderer (incrAfterN 2000 (adtSizeOrderer 0 Nothing)))
  solver simplifier
@@ -325,7 +325,7 @@ reduceCalls g2call solver simplifier config bindings er = do
 
 reduceViolated :: (Solver solver, Simplifier simplifier) => G2Call solver simplifier -> solver -> simplifier -> Sharing -> Bindings -> ExecRes LHTracker -> IO (Bindings, ExecRes LHTracker)
 reduceViolated g2call solver simplifier share bindings er@(ExecRes { final_state = s, violated = Just v }) = do
- let red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| redArbErrors)
+ let red = redArbErrors :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
  (s', bindings', v') <- reduceFuncCall g2call red solver simplifier s bindings v
  -- putStrLn $ "v = " ++ show v
  -- putStrLn $ "v' = " ++ show v'
@@ -337,7 +337,7 @@ reduceViolated _ _ _ _ b er = return (b, er)
 reduceAbstracted :: (Solver solver, Simplifier simplifier) => G2Call solver simplifier -> solver -> simplifier -> Sharing -> Bindings -> ExecRes LHTracker -> IO (Bindings, ExecRes LHTracker)
 reduceAbstracted g2call solver simplifier share bindings
  er@(ExecRes { final_state = (s@State { track = lht}) }) = do
- let red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| redArbErrors)
+ let red = redArbErrors :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
  fcs = abstract_calls lht
 
  ((s', bindings'), fcs') <- mapAccumM (\(s_, b_) fc -> do
@@ -375,7 +375,7 @@ reduceFuncCallMaybeList :: ( ASTContainer t Expr
  , Solver solver
  , Simplifier simplifier) => G2Call solver simplifier -> solver -> simplifier -> Sharing -> Bindings -> State t -> [FuncCall] -> IO (State t, Bindings, [FuncCall])
 reduceFuncCallMaybeList g2call solver simplifier share bindings st fcs = do
- let red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| redArbErrors)
+ let red = redArbErrors :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
  ((s', b'), fcs') <- mapAccumM (\(s, b) fc -> do
  s_b_fc <- reduceFuncCallMaybe g2call red solver simplifier s b fc
  case s_b_fc of

diff --git a/src/G2/Liquid/Inference/G2Calls.hs b/src/G2/Liquid/Inference/G2Calls.hs
@@ -412,11 +412,12 @@ gatherReducerHalterOrderer infconfig config lhconfig solver simplifier = do
 
  timer_halter <- stdTimerHalter (timeout_se infconfig * 3)
 
+ let red = case m_logger of
+ Just logger -> logger .~> SomeReducer (gathererReducer ~> stdRed share retReplaceSymbFuncVar solver simplifier)
+ Nothing -> SomeReducer (gathererReducer ~> stdRed share retReplaceSymbFuncVar solver simplifier)
+
  return
- (SomeReducer (nonRedPCRed <~| taggerRed state_name)
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ gathererReducer) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ gathererReducer))
+ (red .== Finished .--> (taggerRed state_name :== Finished --> nonRedPCRed)
  , SomeHalter
  (discardIfAcceptedTagHalter state_name
  <~> switchEveryNHalter (switch_after lhconfig)
@@ -542,19 +543,20 @@ inferenceReducerHalterOrderer infconfig config lhconfig solver simplifier entry
  <~> lhSWHNFHalter
  <~> timer_halter
  <~> lh_timer_halter
- let some_red = SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier
-  <~ higherOrderCallsRed
-  <~ allCallsRed
-  <~| redArbErrors
- <~| lhRed cfn
- <~? existentialInstRed)
+ let some_red = existentialInstRed :== NoProgress .-->
+ lhRed cfn :== Finished .--> 
+ redArbErrors :== Finished .-->
+ SomeReducer (allCallsRed ~>
+ higherOrderCallsRed ~>
+ stdRed share retReplaceSymbFuncVar solver simplifier)
 
  return $
- (SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name)
- .<~| (SomeReducer (nonRedPCRed <~| taggerRed state_name))
- .<~| (case m_logger of
- Just logger -> some_red .<~ logger
- Nothing -> some_red)
+ (
+ (case m_logger of
+ Just logger -> logger .~> some_red
+ Nothing -> some_red) .== Finished .-->
+ (taggerRed state_name :== Finished --> nonRedPCRed) .== Finished .-->
+ (taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed)
  , SomeHalter
  (discardIfAcceptedTagHalter state_name <~> halter)
  , SomeOrderer (incrAfterN 2000 (quotTrueAssert (ordComb (+) (pcSizeOrderer 0) (adtSizeOrderer 0 (Just instFuncTickName))))))
@@ -626,13 +628,16 @@ realCExReducerHalterOrderer infconfig config lhconfig entry modname solver simpl
  <~> zeroHalter (0 + extra_depth)
  <~> lhAcceptIfViolatedHalter
  <~> timer_halter
+
+ lh_std_red = lhRed cfn :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
+ log_opt_red = case m_logger of
+ Just logger -> logger .~> lh_std_red
+ Nothing -> lh_std_red
 
  return $
- (SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name)
- .<~| (SomeReducer (nonRedPCRed <~| taggerRed state_name))
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn))
+ (log_opt_red .== Finished .-->
+ (taggerRed state_name :== Finished --> nonRedPCRed) .== Finished .-->
+ (taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed)
  , SomeHalter
  (discardIfAcceptedTagHalter state_name <~> halter)
  , SomeOrderer (incrAfterN 1000 (adtSizeOrderer 0 Nothing)))
@@ -1095,7 +1100,7 @@ genericG2CallLogging config solver s bindings lg = do
  let simplifier = IdSimplifier
  share = sharing config
 
- fslb <- runG2WithSomes (SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~ prettyLogger lg))
+ fslb <- runG2WithSomes (SomeReducer (prettyLogger lg ~> stdRed share retReplaceSymbFuncVar solver simplifier))
  (SomeHalter swhnfHalter)
  (SomeOrderer nextOrderer)
  solver simplifier PreserveAllMC s bindings

diff --git a/src/G2/Liquid/Interface.hs b/src/G2/Liquid/Interface.hs
@@ -445,13 +445,16 @@ lhReducerHalterOrderer config lhconfig solver simplifier entry mb_modname cfn st
  non_red = nonRedPCRed .|. nonRedPCRedConst
 
  m_logger = fmap SomeReducer $ getLogger config
+
+ lh_std_red = existentialInstRed :== NoProgress .--> lhRed cfn :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
+ opt_logger_red = case m_logger of
+ Just logger -> logger .~> lh_std_red
+ Nothing -> lh_std_red
  in
  if higherOrderSolver config == AllFuncs then
- ( SomeReducer non_red
- .<~| (SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name))
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed))
+ (opt_logger_red .== Finished .-->
+ (taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed) .== Finished .-->
+ SomeReducer non_red
  , SomeHalter
  (maxOutputsHalter (maxOutputs config)
  <~> zeroHalter (steps config)
@@ -461,11 +464,9 @@ lhReducerHalterOrderer config lhconfig solver simplifier entry mb_modname cfn st
  <~> lhAcceptIfViolatedHalter)
  , SomeOrderer lhLimitByAcceptedOrderer)
  else
- (SomeReducer (nonRedAbstractReturnsRed <~| taggerRed abs_ret_name)
- .<~| (SomeReducer (non_red <~| taggerRed state_name))
- .<~| (case m_logger of
- Just logger -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed) .<~ logger
- Nothing -> SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier <~| lhRed cfn <~? existentialInstRed))
+ (opt_logger_red .== Finished .-->
+ ((taggerRed state_name :== Finished --> non_red)) .== Finished .-->
+ (taggerRed abs_ret_name :== Finished --> nonRedAbstractReturnsRed)
  , SomeHalter
  (discardIfAcceptedTagHalter state_name
  <~> discardIfAcceptedTagHalter abs_ret_name

diff --git a/src/G2/QuasiQuotes/QuasiQuotes.hs b/src/G2/QuasiQuotes/QuasiQuotes.hs
@@ -277,9 +277,7 @@ qqRedHaltOrd config solver simplifier =
 
  state_name = G2.Name "state" Nothing 0 Nothing
  in
- ( SomeReducer
- (nonRedPCRed <~| taggerRed state_name)
- .<~| (SomeReducer (stdRed share retReplaceSymbFuncVar solver simplifier))
+ ( taggerRed state_name :== Finished .--> nonRedPCRed :== Finished --> stdRed share retReplaceSymbFuncVar solver simplifier
  , SomeHalter
  (discardIfAcceptedTagHalter state_name 
  <~> acceptIfViolatedHalter)