diff --git a/kore/src/Kore/Log/KoreLogOptions.hs b/kore/src/Kore/Log/KoreLogOptions.hs index df48b4ee69..857e402357 100644 --- a/kore/src/Kore/Log/KoreLogOptions.hs +++ b/kore/src/Kore/Log/KoreLogOptions.hs @@ -20,6 +20,7 @@ module Kore.Log.KoreLogOptions , DebugEquationOptions (..) , selectDebugEquation , unparseKoreLogOptions + , defaultSeverity ) where import Prelude.Kore @@ -102,12 +103,14 @@ data KoreLogOptions = KoreLogOptions } deriving (Eq, Show) +defaultSeverity :: Severity +defaultSeverity = Warning defaultKoreLogOptions :: ExeName -> TimeSpec -> KoreLogOptions defaultKoreLogOptions exeName startTime = KoreLogOptions { logType = def @KoreLogType - , logLevel = Warning + , logLevel = defaultSeverity , timestampsSwitch = def @TimestampsSwitch , logEntries = mempty , debugSolverOptions = def @DebugSolverOptions diff --git a/kore/src/Kore/Repl.hs b/kore/src/Kore/Repl.hs index 41cc20db75..a15527ceb4 100644 --- a/kore/src/Kore/Repl.hs +++ b/kore/src/Kore/Repl.hs @@ -141,47 +141,46 @@ runRepl = do startTime <- liftIO $ getTime Monotonic (newState, _) <- - (\rwst -> execRWST rwst config state) - $ evaluateScript startTime replScript scriptModeOutput + (\rwst -> execRWST rwst config (state startTime)) + $ evaluateScript replScript scriptModeOutput case replMode of Interactive -> do replGreeting flip evalStateT newState $ flip runReaderT config - $ forever (repl0 startTime) + $ forever repl0 RunScript -> - runReplCommand startTime Exit newState + runReplCommand Exit newState where - runReplCommand :: TimeSpec -> ReplCommand -> ReplState -> m () - runReplCommand startTime cmd st = + runReplCommand :: ReplCommand -> ReplState -> m () + runReplCommand cmd st = void $ flip evalStateT st $ flip runReaderT config - $ replInterpreter startTime printIfNotEmpty cmd + $ replInterpreter printIfNotEmpty cmd evaluateScript - :: TimeSpec - -> ReplScript + :: ReplScript -> ScriptModeOutput -> RWST (Config m) String ReplState m () - evaluateScript startTime script outputFlag = + evaluateScript script outputFlag = maybe (pure ()) - (flip (parseEvalScript startTime) outputFlag) + (flip parseEvalScript outputFlag) (unReplScript script) - repl0 :: TimeSpec -> ReaderT (Config m) (StateT ReplState m) () - repl0 startTime = do + repl0 :: ReaderT (Config m) (StateT ReplState m) () + repl0 = do str <- prompt let command = - fromMaybe ShowUsage $ parseMaybe (commandParser startTime) str + fromMaybe ShowUsage $ parseMaybe commandParser str when (shouldStore command) $ field @"commands" Lens.%= (Seq.|> str) - void $ replInterpreter startTime printIfNotEmpty command + void $ replInterpreter printIfNotEmpty command - state :: ReplState - state = + state :: TimeSpec -> ReplState + state startTime = ReplState { axioms = addIndexesToAxioms axioms' , claims = addIndexesToClaims claims' @@ -197,7 +196,9 @@ runRepl , aliases = Map.empty , koreLogOptions = logOptions - { Log.exeName = Log.ExeName "kore-repl" } + { Log.exeName = Log.ExeName "kore-repl" + , Log.startTime = startTime + } } config :: Config m diff --git a/kore/src/Kore/Repl/Data.hs b/kore/src/Kore/Repl/Data.hs index 22ea64ccda..ab0c70e167 100644 --- a/kore/src/Kore/Repl/Data.hs +++ b/kore/src/Kore/Repl/Data.hs @@ -37,6 +37,11 @@ module Kore.Repl.Data , OutputFile (..) , makeAuxReplOutput, makeKoreReplOutput , GraphView (..) + , GeneralLogOptions (..) + , generalLogOptionsTransformer + , debugAttemptEquationTransformer + , debugApplyEquationTransformer + , debugEquationTransformer ) where import Prelude.Kore @@ -86,6 +91,11 @@ import Kore.Internal.TermLike ( TermLike ) import Kore.Log + ( ActualEntry (..) + , LogAction (..) + , MonadLog (..) + ) +import qualified Kore.Log as Log import qualified Kore.Log.Registry as Log import Kore.Step.Simplification.Data ( MonadSimplify (..) @@ -200,6 +210,74 @@ data GraphView | Expanded deriving (Eq, Show) +-- | Log options which can be changed by the log command. +data GeneralLogOptions = + GeneralLogOptions + { logType :: !Log.KoreLogType + , logLevel :: !Log.Severity + , timestampsSwitch :: !Log.TimestampsSwitch + , logEntries :: !Log.EntryTypes + } + deriving (Eq, Show) + +generalLogOptionsTransformer + :: GeneralLogOptions + -> Log.KoreLogOptions + -> Log.KoreLogOptions +generalLogOptionsTransformer + logOptions@(GeneralLogOptions _ _ _ _) + koreLogOptions + = + koreLogOptions + { Log.logLevel = logLevel + , Log.logEntries = logEntries + , Log.logType = logType + , Log.timestampsSwitch = timestampsSwitch + } + where + GeneralLogOptions + { logLevel + , logType + , logEntries + , timestampsSwitch + } = logOptions + +debugAttemptEquationTransformer + :: Log.DebugAttemptEquationOptions + -> Log.KoreLogOptions + -> Log.KoreLogOptions +debugAttemptEquationTransformer + debugAttemptEquationOptions + koreLogOptions + = + koreLogOptions + { Log.debugAttemptEquationOptions = debugAttemptEquationOptions + } + +debugApplyEquationTransformer + :: Log.DebugApplyEquationOptions + -> Log.KoreLogOptions + -> Log.KoreLogOptions +debugApplyEquationTransformer + debugApplyEquationOptions + koreLogOptions + = + koreLogOptions + { Log.debugApplyEquationOptions = debugApplyEquationOptions + } + +debugEquationTransformer + :: Log.DebugEquationOptions + -> Log.KoreLogOptions + -> Log.KoreLogOptions +debugEquationTransformer + debugEquationOptions + koreLogOptions + = + koreLogOptions + { Log.debugEquationOptions = debugEquationOptions + } + -- | List of available commands for the Repl. Note that we are always in a proof -- state. We pick the first available Claim when we initialize the state. data ReplCommand @@ -271,8 +349,19 @@ data ReplCommand -- ^ Load script from file | ProofStatus -- ^ Show proof status of each claim - | Log KoreLogOptions + -- TODO(Ana): 'Log (KoreLogOptions -> KoreLogOptions)', this would need + -- the parts of the code which depend on the 'Show' instance of 'ReplCommand' + -- to change. Do the same for Debug..Equation. + | Log GeneralLogOptions -- ^ Setup the Kore logger. + | DebugAttemptEquation Log.DebugAttemptEquationOptions + -- ^ Log debugging information about attempting to + -- apply specific equations. + | DebugApplyEquation Log.DebugApplyEquationOptions + -- ^ Log when specific equations apply. + | DebugEquation Log.DebugEquationOptions + -- ^ Log the attempts and the applications of specific + -- equations. | Exit -- ^ Exit the repl. deriving (Eq, Show) @@ -373,7 +462,7 @@ helpText = \ runs an existing alias\n\ \load file loads the file as a repl script\n\ \proof-status shows status for each claim\n\ - \log \"[\"\"]\" configures the logging output\n\ + \log \"[\"\"]\" configures the logging output\n\ \ can be debug, info,\ \ warning, error, or critical;\ \ is optional and defaults to warning\n\ @@ -390,6 +479,14 @@ helpText = \ can be 'stderr' or 'file filename'\n\ \ can be enable-log-timestamps\ \ or disable-log-timestamps\n\ + \debug-[type]-equation [eqId1] [eqId2] .. show debugging information for multiple specific equations;\ + \ [type] can be 'attempt' or 'apply', or nothing\ + \ meaning both, as follows ('debug-equation');\n\ + \ example usage: 'debug-attempt-equation eqId',\ + \ 'debug-equation eqId1 eqId2'; without arguments it will\ + \ will disable showing the info, for example: 'debug-apply-equation';\n\ + \ repl command counterparts of the equation command line options;\ + \ see command line help text for more information;\n\ \exit exits the repl\ \\n\n\ \Available modifiers:\n\ @@ -493,7 +590,7 @@ data ReplState = ReplState -- ^ Map from labels to nodes , aliases :: Map String AliasDefinition -- ^ Map of command aliases - , koreLogOptions :: !KoreLogOptions + , koreLogOptions :: !Log.KoreLogOptions -- ^ The log level, log scopes and log type decide what gets logged and -- where. } diff --git a/kore/src/Kore/Repl/Interpreter.hs b/kore/src/Kore/Repl/Interpreter.hs index 8a07305068..648ca44221 100644 --- a/kore/src/Kore/Repl/Interpreter.hs +++ b/kore/src/Kore/Repl/Interpreter.hs @@ -209,9 +209,6 @@ import Kore.Unparser , unparseToString ) import qualified Pretty -import System.Clock - ( TimeSpec - ) -- | Warning: you should never use WriterT or RWST. It is used here with -- _great care_ of evaluating the RWST to a StateT immediatly, and thus getting @@ -227,12 +224,11 @@ replInterpreter :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> (String -> IO ()) + => (String -> IO ()) -> ReplCommand -> ReaderT (Config m) (StateT ReplState m) ReplStatus -replInterpreter startTime fn cmd = - replInterpreter0 startTime +replInterpreter fn cmd = + replInterpreter0 (PrintAuxOutput fn) (PrintKoreOutput fn) cmd @@ -241,52 +237,54 @@ replInterpreter0 :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> PrintAuxOutput + => PrintAuxOutput -> PrintKoreOutput -> ReplCommand -> ReaderT (Config m) (StateT ReplState m) ReplStatus -replInterpreter0 startTime printAux printKore replCmd = do +replInterpreter0 printAux printKore replCmd = do let command = case replCmd of - ShowUsage -> showUsage $> Continue - Help -> help $> Continue - ShowClaim mc -> showClaim mc $> Continue - ShowAxiom ea -> showAxiom ea $> Continue - Prove i -> prove i $> Continue - ShowGraph v mfile out -> showGraph v mfile out $> Continue - ProveSteps n -> proveSteps n $> Continue - ProveStepsF n -> proveStepsF n $> Continue - SelectNode i -> selectNode i $> Continue - ShowConfig mc -> showConfig mc $> Continue - ShowDest mc -> showDest mc $> Continue - OmitCell c -> omitCell c $> Continue - ShowLeafs -> showLeafs $> Continue - ShowRule mc -> showRule mc $> Continue - ShowRules ns -> showRules ns $> Continue - ShowPrecBranch mn -> showPrecBranch mn $> Continue - ShowChildren mn -> showChildren mn $> Continue - Label ms -> label ms $> Continue - LabelAdd l mn -> labelAdd l mn $> Continue - LabelDel l -> labelDel l $> Continue - Redirect inn file -> redirect startTime inn file - $> Continue - Try ref -> tryAxiomClaim ref $> Continue - TryF ac -> tryFAxiomClaim ac $> Continue - Clear n -> clear n $> Continue - SaveSession file -> saveSession file $> Continue - SavePartialProof mn f -> savePartialProof mn f $> Continue - Pipe inn file args -> pipe startTime inn file args - $> Continue - AppendTo inn file -> appendTo startTime inn file - $> Continue - Alias a -> alias a $> Continue - TryAlias name -> - tryAlias startTime name printAux printKore - LoadScript file -> loadScript startTime file - $> Continue - ProofStatus -> proofStatus $> Continue - Log opts -> handleLog opts $> Continue - Exit -> exit + ShowUsage -> showUsage $> Continue + Help -> help $> Continue + ShowClaim mc -> showClaim mc $> Continue + ShowAxiom ea -> showAxiom ea $> Continue + Prove i -> prove i $> Continue + ShowGraph v mfile out -> showGraph v mfile out $> Continue + ProveSteps n -> proveSteps n $> Continue + ProveStepsF n -> proveStepsF n $> Continue + SelectNode i -> selectNode i $> Continue + ShowConfig mc -> showConfig mc $> Continue + ShowDest mc -> showDest mc $> Continue + OmitCell c -> omitCell c $> Continue + ShowLeafs -> showLeafs $> Continue + ShowRule mc -> showRule mc $> Continue + ShowRules ns -> showRules ns $> Continue + ShowPrecBranch mn -> showPrecBranch mn $> Continue + ShowChildren mn -> showChildren mn $> Continue + Label ms -> label ms $> Continue + LabelAdd l mn -> labelAdd l mn $> Continue + LabelDel l -> labelDel l $> Continue + Redirect inn file -> redirect inn file + $> Continue + Try ref -> tryAxiomClaim ref $> Continue + TryF ac -> tryFAxiomClaim ac $> Continue + Clear n -> clear n $> Continue + SaveSession file -> saveSession file $> Continue + SavePartialProof mn f -> savePartialProof mn f $> Continue + Pipe inn file args -> pipe inn file args + $> Continue + AppendTo inn file -> appendTo inn file + $> Continue + Alias a -> alias a $> Continue + TryAlias name -> + tryAlias name printAux printKore + LoadScript file -> loadScript file + $> Continue + ProofStatus -> proofStatus $> Continue + Log opts -> log opts $> Continue + DebugAttemptEquation op -> debugAttemptEquation op $> Continue + DebugApplyEquation op -> debugApplyEquation op $> Continue + DebugEquation op -> debugEquation op $> Continue + Exit -> exit (ReplOutput output, shouldContinue) <- evaluateCommand command liftIO $ Foldable.traverse_ ( replOut @@ -508,17 +506,47 @@ loadScript :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> FilePath + => FilePath -- ^ path to file -> ReplM m () -loadScript startTime file = parseEvalScript startTime file DisableOutput +loadScript file = parseEvalScript file DisableOutput + +-- | Change the general log settings. +log + :: MonadState ReplState m + => GeneralLogOptions + -> m () +log generalLogOptions = + field @"koreLogOptions" %= generalLogOptionsTransformer generalLogOptions + +-- | Log debugging information about attempting to apply +-- specific equations. +debugAttemptEquation + :: MonadState ReplState m + => Log.DebugAttemptEquationOptions + -> m () +debugAttemptEquation debugAttemptEquationOptions = + field @"koreLogOptions" + %= debugAttemptEquationTransformer debugAttemptEquationOptions -handleLog +-- | Log when specific equations apply. +debugApplyEquation :: MonadState ReplState m - => Log.KoreLogOptions + => Log.DebugApplyEquationOptions -> m () -handleLog t = field @"koreLogOptions" .= t +debugApplyEquation debugApplyEquationOptions = + field @"koreLogOptions" + %= debugApplyEquationTransformer debugApplyEquationOptions + +-- | Log the attempts and the applications of specific +-- equations. +debugEquation + :: MonadState ReplState m + => Log.DebugEquationOptions + -> m () +debugEquation debugEquationOptions = + field @"koreLogOptions" + %= debugEquationTransformer debugEquationOptions -- | Focuses the node with id equals to 'n'. selectNode @@ -825,30 +853,28 @@ redirect :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> ReplCommand + => ReplCommand -- ^ command to redirect -> FilePath -- ^ file path -> ReplM m () -redirect startTime cmd file = do +redirect cmd file = do liftIO $ withExistingDirectory file (`writeFile` "") - appendCommand startTime cmd file + appendCommand cmd file runInterpreterWithOutput :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> PrintAuxOutput + => PrintAuxOutput -> PrintKoreOutput -> ReplCommand -> Config m -> ReplM m () -runInterpreterWithOutput startTime printAux printKore cmd config = +runInterpreterWithOutput printAux printKore cmd config = get >>= (\st -> lift $ execStateReader config st - $ replInterpreter0 startTime printAux printKore cmd + $ replInterpreter0 printAux printKore cmd ) >>= put @@ -1128,22 +1154,21 @@ pipe :: forall m . MonadIO m => MonadSimplify m - => TimeSpec - -> ReplCommand + => ReplCommand -- ^ command to pipe -> String -- ^ path to the program that will receive the command's output -> [String] -- ^ additional arguments to be passed to the program -> ReplM m () -pipe startTime cmd file args = do +pipe cmd file args = do exists <- liftIO $ findExecutable file case exists of Nothing -> putStrLn' "Cannot find executable." Just exec -> do config <- ask pipeOutRef <- liftIO $ newIORef (mempty :: ReplOutput) - runInterpreterWithOutput startTime + runInterpreterWithOutput (PrintAuxOutput $ justPrint pipeOutRef) (PrintKoreOutput $ runExternalProcess pipeOutRef exec) cmd @@ -1173,26 +1198,24 @@ appendTo :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> ReplCommand + => ReplCommand -- ^ command -> FilePath -- ^ file to append to -> ReplM m () -appendTo startTime cmd file = - withExistingDirectory file (appendCommand startTime cmd) +appendTo cmd file = + withExistingDirectory file (appendCommand cmd) appendCommand :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> ReplCommand + => ReplCommand -> FilePath -> ReplM m () -appendCommand startTime cmd file = do +appendCommand cmd file = do config <- ask - runInterpreterWithOutput startTime + runInterpreterWithOutput (PrintAuxOutput $ appendFile file) (PrintKoreOutput $ appendFile file) cmd @@ -1215,12 +1238,11 @@ tryAlias :: forall m . MonadSimplify m => MonadIO m - => TimeSpec - -> ReplAlias + => ReplAlias -> PrintAuxOutput -> PrintKoreOutput -> ReplM m ReplStatus -tryAlias startTime replAlias@ReplAlias { name } printAux printKore = do +tryAlias replAlias@ReplAlias { name } printAux printKore = do res <- findAlias name case res of Nothing -> showUsage $> Continue @@ -1230,7 +1252,7 @@ tryAlias startTime replAlias@ReplAlias { name } printAux printKore = do parsedCommand = fromMaybe ShowUsage - $ parseMaybe (commandParser startTime) command + $ parseMaybe commandParser command config <- ask (cont, st') <- get >>= runInterpreter parsedCommand config put st' @@ -1245,7 +1267,7 @@ tryAlias startTime replAlias@ReplAlias { name } printAux printKore = do lift $ (`runStateT` st) $ runReaderT - (replInterpreter0 startTime printAux printKore cmd) + (replInterpreter0 printAux printKore cmd) config -- | Performs n proof steps, picking the next node unless branching occurs. @@ -1463,16 +1485,15 @@ parseEvalScript => MonadState ReplState (t m) => MonadReader (Config m) (t m) => Monad.Trans.MonadTrans t - => TimeSpec - -> FilePath + => FilePath -> ScriptModeOutput -> t m () -parseEvalScript startTime file scriptModeOutput = do +parseEvalScript file scriptModeOutput = do exists <- lift . liftIO . doesFileExist $ file if exists then do contents <- lift . liftIO $ readFile file - let result = runParser (scriptParser startTime) file contents + let result = runParser scriptParser file contents either parseFailed executeScript result else lift . liftIO . putStrLn $ "Cannot find " <> file @@ -1505,7 +1526,7 @@ parseEvalScript startTime file scriptModeOutput = do :: ReplCommand -> ReaderT (Config m) (StateT ReplState m) ReplStatus executeCommand command = - replInterpreter0 startTime + replInterpreter0 (PrintAuxOutput $ \_ -> return ()) (PrintKoreOutput $ \_ -> return ()) command @@ -1517,7 +1538,7 @@ parseEvalScript startTime file scriptModeOutput = do node <- Lens.use (field @"node") liftIO $ putStr $ "Kore (" <> show (unReplNode node) <> ")> " liftIO $ print command - replInterpreter0 startTime + replInterpreter0 (PrintAuxOutput printIfNotEmpty) (PrintKoreOutput printIfNotEmpty) command diff --git a/kore/src/Kore/Repl/Parser.hs b/kore/src/Kore/Repl/Parser.hs index f59912c65e..e8e228d9f5 100644 --- a/kore/src/Kore/Repl/Parser.hs +++ b/kore/src/Kore/Repl/Parser.hs @@ -24,6 +24,7 @@ import Data.GraphViz ( GraphvizOutput ) import qualified Data.GraphViz as Graph +import qualified Data.HashSet as HashSet import Data.List ( nub ) @@ -51,12 +52,8 @@ import Kore.Log ( EntryTypes ) import qualified Kore.Log as Log -import Kore.Log.KoreLogOptions import qualified Kore.Log.Registry as Log import Kore.Repl.Data -import System.Clock - ( TimeSpec - ) type Parser = Parsec String String @@ -65,10 +62,10 @@ type Parser = Parsec String String -- maybe ShowUsage id . Text.Megaparsec.parseMaybe commandParser -- @ -scriptParser :: TimeSpec -> Parser [ReplCommand] -scriptParser startTime = +scriptParser :: Parser [ReplCommand] +scriptParser = some ( skipSpacesAndComments - *> commandParser0 startTime (void Char.newline) + *> commandParser0 (void Char.newline) <* many Char.newline <* skipSpacesAndComments ) @@ -78,12 +75,12 @@ scriptParser startTime = skipSpacesAndComments = optional $ spaceConsumer <* Char.newline -commandParser :: TimeSpec -> Parser ReplCommand -commandParser startTime = commandParser0 startTime eof +commandParser :: Parser ReplCommand +commandParser = commandParser0 eof -commandParser0 :: TimeSpec -> Parser () -> Parser ReplCommand -commandParser0 startTime endParser = - alias <|> log startTime <|> commandParserExceptAlias endParser <|> tryAlias +commandParser0 :: Parser () -> Parser ReplCommand +commandParser0 endParser = + alias <|> logCommand <|> commandParserExceptAlias endParser <|> tryAlias commandParserExceptAlias :: Parser () -> Parser ReplCommand commandParserExceptAlias endParser = do @@ -289,16 +286,22 @@ savePartialProof = *> maybeDecimal <**> quotedOrWordWithout "" -log :: TimeSpec -> Parser ReplCommand -log startTime = do +logCommand :: Parser ReplCommand +logCommand = + log + <|> try debugAttemptEquation + <|> try debugApplyEquation + <|> debugEquation + +log :: Parser ReplCommand +log = do literal "log" logLevel <- parseSeverityWithDefault logEntries <- parseLogEntries logType <- parseLogType timestampsSwitch <- parseTimestampSwitchWithDefault - -- TODO (thomas.tuegel): Allow the user to specify --debug-applied-rule. -- TODO (thomas.tuegel): Allow the user to specify --sqlog. - pure $ Log defKoreLogOptions + pure $ Log GeneralLogOptions { logType , logLevel , timestampsSwitch @@ -306,10 +309,36 @@ log startTime = do } where parseSeverityWithDefault = - severity<|> pure (logLevel defKoreLogOptions) + severity <|> pure Log.defaultSeverity parseTimestampSwitchWithDefault = fromMaybe Log.TimestampsEnable <$> optional parseTimestampSwitch - defKoreLogOptions = defaultKoreLogOptions (ExeName "kore-repl") startTime + +debugAttemptEquation :: Parser ReplCommand +debugAttemptEquation = + DebugAttemptEquation + . Log.DebugAttemptEquationOptions + . HashSet.fromList + . fmap Text.pack + <$$> literal "debug-attempt-equation" + *> many (quotedOrWordWithout "") + +debugApplyEquation :: Parser ReplCommand +debugApplyEquation = + DebugApplyEquation + . Log.DebugApplyEquationOptions + . HashSet.fromList + . fmap Text.pack + <$$> literal "debug-apply-equation" + *> many (quotedOrWordWithout "") + +debugEquation :: Parser ReplCommand +debugEquation = + DebugEquation + . Log.DebugEquationOptions + . HashSet.fromList + . fmap Text.pack + <$$> literal "debug-equation" + *> many (quotedOrWordWithout "") severity :: Parser Log.Severity severity = sDebug <|> sInfo <|> sWarning <|> sError diff --git a/kore/test/Test/Kore/Repl/Interpreter.hs b/kore/test/Test/Kore/Repl/Interpreter.hs index d04a07a558..f0e1c4c8de 100644 --- a/kore/test/Test/Kore/Repl/Interpreter.hs +++ b/kore/test/Test/Kore/Repl/Interpreter.hs @@ -26,6 +26,7 @@ import Data.Coerce ( coerce ) import Data.Generics.Product +import qualified Data.HashSet as HashSet import Data.IORef ( IORef , modifyIORef @@ -98,35 +99,38 @@ import Test.Kore.Step.Simplification test_replInterpreter :: [TestTree] test_replInterpreter = - [ showUsage `tests` "Showing the usage message" - , help `tests` "Showing the help message" - , step5 `tests` "Performing 5 steps" - , step100 `tests` "Stepping over proof completion" - , stepf5noBranching `tests` "Performing 5 foced steps in non-branching proof" - , stepf100noBranching `tests` "Stepping over proof completion" - , makeSimpleAlias `tests` "Creating an alias with no arguments" - , trySimpleAlias `tests` "Executing an existing alias with no arguments" - , makeAlias `tests` "Creating an alias with arguments" - , aliasOfExistingCommand `tests` "Create alias of existing command" - , aliasOfUnknownCommand `tests` "Create alias of unknown command" - , recursiveAlias `tests` "Create alias of unknown command" - , tryAlias `tests` "Executing an existing alias with arguments" - , unificationFailure `tests` "Try axiom that doesn't unify" - , unificationSuccess `tests` "Try axiom that does unify" - , forceFailure `tests` "TryF axiom that doesn't unify" - , forceSuccess `tests` "TryF axiom that does unify" - , proofStatus `tests` "Multi claim proof status" - , logUpdatesState `tests` "Log command updates the state" - , showCurrentClaim `tests` "Showing current claim" - , showClaim1 `tests` "Showing the claim at index 1" - , showClaimByName `tests` "Showing the claim with the name 0to10Claim" - , showAxiomByName `tests` "Showing the axiom with the name add1Axiom" - , unificationFailureWithName `tests` "Try axiom by name that doesn't unify" - , unificationSuccessWithName `tests` "Try axiom by name that does unify" - , forceFailureWithName `tests` "TryF axiom by name that doesn't unify" - , forceSuccessWithName `tests` "TryF axiom by name that does unify" - , proveSecondClaim `tests` "Starting to prove the second claim" - , proveSecondClaimByName `tests` "Starting to prove the second claim\ + [ showUsage `tests` "Showing the usage message" + , help `tests` "Showing the help message" + , step5 `tests` "Performing 5 steps" + , step100 `tests` "Stepping over proof completion" + , stepf5noBranching `tests` "Performing 5 foced steps in non-branching proof" + , stepf100noBranching `tests` "Stepping over proof completion" + , makeSimpleAlias `tests` "Creating an alias with no arguments" + , trySimpleAlias `tests` "Executing an existing alias with no arguments" + , makeAlias `tests` "Creating an alias with arguments" + , aliasOfExistingCommand `tests` "Create alias of existing command" + , aliasOfUnknownCommand `tests` "Create alias of unknown command" + , recursiveAlias `tests` "Create alias of unknown command" + , tryAlias `tests` "Executing an existing alias with arguments" + , unificationFailure `tests` "Try axiom that doesn't unify" + , unificationSuccess `tests` "Try axiom that does unify" + , forceFailure `tests` "TryF axiom that doesn't unify" + , forceSuccess `tests` "TryF axiom that does unify" + , proofStatus `tests` "Multi claim proof status" + , logUpdatesState `tests` "Log command updates the state" + , debugAttemptEquationUpdatesState `tests` "DebugAttemptEquation command updates the state" + , debugApplyEquationUpdatesState `tests` "DebugApplyEquation command updates the state" + , debugEquationUpdatesState `tests` "DebugEquation command updates the state" + , showCurrentClaim `tests` "Showing current claim" + , showClaim1 `tests` "Showing the claim at index 1" + , showClaimByName `tests` "Showing the claim with the name 0to10Claim" + , showAxiomByName `tests` "Showing the axiom with the name add1Axiom" + , unificationFailureWithName `tests` "Try axiom by name that doesn't unify" + , unificationSuccessWithName `tests` "Try axiom by name that does unify" + , forceFailureWithName `tests` "TryF axiom by name that doesn't unify" + , forceSuccessWithName `tests` "TryF axiom by name that does unify" + , proveSecondClaim `tests` "Starting to prove the second claim" + , proveSecondClaimByName `tests` "Starting to prove the second claim\ \ referenced by name" ] @@ -533,22 +537,74 @@ showAxiomByName = logUpdatesState :: IO () logUpdatesState = do - startTime <- getTime Monotonic let axioms = [] claim = emptyClaim options = - (Log.defaultKoreLogOptions (Log.ExeName "kore-repl") startTime) - { Log.logLevel = Log.Info - , Log.logEntries = + GeneralLogOptions + { logLevel = Log.Info + , logEntries = Map.keysSet . Log.typeToText $ Log.registry + , logType = Log.LogStdErr + , timestampsSwitch = Log.TimestampsEnable } command = Log options Result { output, continue, state } <- run command axioms [claim] claim output `equalsOutput` mempty continue `equals` Continue - state `hasLogging` options + state `hasLogging` generalLogOptionsTransformer options + +debugAttemptEquationUpdatesState :: IO () +debugAttemptEquationUpdatesState = do + let + axioms = [] + claim = emptyClaim + options = + Log.DebugAttemptEquationOptions + { Log.selected = HashSet.fromList + ["symbol"] + } + command = DebugAttemptEquation options + Result { output, continue, state } <- + run command axioms [claim] claim + output `equalsOutput` mempty + continue `equals` Continue + hasLogging state (debugAttemptEquationTransformer options) + +debugApplyEquationUpdatesState :: IO () +debugApplyEquationUpdatesState = do + let + axioms = [] + claim = emptyClaim + options = + Log.DebugApplyEquationOptions + { Log.selected = HashSet.fromList + ["symbol"] + } + command = DebugApplyEquation options + Result { output, continue, state } <- + run command axioms [claim] claim + output `equalsOutput` mempty + continue `equals` Continue + hasLogging state (debugApplyEquationTransformer options) + +debugEquationUpdatesState :: IO () +debugEquationUpdatesState = do + let + axioms = [] + claim = emptyClaim + options = + Log.DebugEquationOptions + { Log.selected = HashSet.fromList + ["symbol"] + } + command = DebugEquation options + Result { output, continue, state } <- + run command axioms [claim] claim + output `equalsOutput` mempty + continue `equals` Continue + hasLogging state (debugEquationTransformer options) proveSecondClaim :: IO () proveSecondClaim = @@ -662,7 +718,7 @@ runWithState command axioms claims claim stateTransformer = do $ liftSimplifier $ flip runStateT state $ flip runReaderT config - $ replInterpreter0 startTime + $ replInterpreter0 (PrintAuxOutput . modifyAuxOutput $ output) (PrintKoreOutput . modifyKoreOutput $ output) command @@ -708,20 +764,16 @@ hasAlias st alias@AliasDefinition { name } = hasLogging :: ReplState - -> Log.KoreLogOptions + -> (Log.KoreLogOptions -> Log.KoreLogOptions) -> IO () -hasLogging st expectedLogging = - let - actualLogging = koreLogOptions st - in - actualLogging `equals` expectedLogging +hasLogging st transformer = + let actualLogging = koreLogOptions st + in actualLogging `equals` transformer actualLogging hasCurrentClaimIndex :: ReplState -> ClaimIndex -> IO () hasCurrentClaimIndex st expectedClaimIndex = - let - actualClaimIndex = claimIndex st - in - actualClaimIndex `equals` expectedClaimIndex + let actualClaimIndex = claimIndex st + in actualClaimIndex `equals` expectedClaimIndex tests :: IO () -> String -> TestTree tests = flip testCase diff --git a/kore/test/Test/Kore/Repl/Parser.hs b/kore/test/Test/Kore/Repl/Parser.hs index d0656164f6..ff83378048 100644 --- a/kore/test/Test/Kore/Repl/Parser.hs +++ b/kore/test/Test/Kore/Repl/Parser.hs @@ -10,8 +10,16 @@ import Test.Tasty ) import qualified Data.GraphViz as Graph +import Data.HashSet + ( HashSet + ) +import qualified Data.HashSet as HashSet import Data.Proxy import qualified Data.Set as Set +import Data.Text + ( Text + ) +import qualified Data.Text as Text import Numeric.Natural import Type.Reflection ( SomeTypeRep @@ -23,67 +31,64 @@ import Kore.Equation.Application , DebugAttemptEquation ) import qualified Kore.Log as Log -import Kore.Log.KoreLogOptions - ( defaultKoreLogOptions - ) import Kore.Repl.Data import Kore.Repl.Parser -import System.Clock - ( fromNanoSecs - ) import Test.Kore.Parser test_replParser :: [TestTree] test_replParser = - [ helpTests `tests` "help" - , claimTests `tests` "claim" - , axiomTests `tests` "axiom" - , proveTests `tests` "prove" - , graphTests `tests` "graph" - , stepTests `tests` "step" - , selectTests `tests` "select" - , configTests `tests` "config" - , destTests `tests` "dest" - , leafsTests `tests` "leafs" - , precBranchTests `tests` "prec-branch" - , childrenTests `tests` "children" - , exitTests `tests` "exit" - , omitTests `tests` "omit" - , labelTests `tests` "label" - , tryTests `tests` "try" - , tryFTests `tests` "tryF" - , redirectTests `tests` "redirect" - , ruleTests `tests` "rule" - , rulesTests `tests` "rules" - , stepfTests `tests` "stepf" - , clearTests `tests` "clear" - , pipeTests `tests` "pipe" - , pipeRedirectTests `tests` "pipe redirect" - , saveSessionTests `tests` "save-session" - , appendTests `tests` "append" - , pipeAppendTests `tests` "pipe append" - , noArgsAliasTests `tests` "no arguments alias tests" - , tryAliasTests `tests` "try alias" - , loadScriptTests `tests` "load file" - , initScriptTests `testsScript` "repl script" - , aliasesWithArgs `tests` "aliases with arguments" - , proofStatus `tests` "proof-status" - , logTests `tests` "log" + [ helpTests `tests` "help" + , claimTests `tests` "claim" + , axiomTests `tests` "axiom" + , proveTests `tests` "prove" + , graphTests `tests` "graph" + , stepTests `tests` "step" + , selectTests `tests` "select" + , configTests `tests` "config" + , destTests `tests` "dest" + , leafsTests `tests` "leafs" + , precBranchTests `tests` "prec-branch" + , childrenTests `tests` "children" + , exitTests `tests` "exit" + , omitTests `tests` "omit" + , labelTests `tests` "label" + , tryTests `tests` "try" + , tryFTests `tests` "tryF" + , redirectTests `tests` "redirect" + , ruleTests `tests` "rule" + , rulesTests `tests` "rules" + , stepfTests `tests` "stepf" + , clearTests `tests` "clear" + , pipeTests `tests` "pipe" + , pipeRedirectTests `tests` "pipe redirect" + , saveSessionTests `tests` "save-session" + , appendTests `tests` "append" + , pipeAppendTests `tests` "pipe append" + , noArgsAliasTests `tests` "no arguments alias tests" + , tryAliasTests `tests` "try alias" + , loadScriptTests `tests` "load file" + , initScriptTests `testsScript` "repl script" + , aliasesWithArgs `tests` "aliases with arguments" + , proofStatus `tests` "proof-status" + , logTests `tests` "log" + , debugAttemptEquationTests `tests` "debug-attempt-equation" + , debugApplyEquationTests `tests` "debug-apply-equation" + , debugEquationTests `tests` "debug-equation" ] tests :: [ParserTest ReplCommand] -> String -> TestTree tests ts pname = testGroup ("REPL.Parser." <> pname) - . parseTree (commandParser $ fromNanoSecs 0) + . parseTree commandParser $ ts testsScript :: [ParserTest [ReplCommand]] -> String -> TestTree testsScript ts pname = testGroup ("REPL.Parser." <> pname) - . parseTree (scriptParser $ fromNanoSecs 0) + . parseTree scriptParser $ ts helpTests :: [ParserTest ReplCommand] @@ -486,74 +491,169 @@ logTests :: [ParserTest ReplCommand] logTests = [ "log debug [] stderr" `parsesTo_` - Log - ( defaultKoreLogOptions - (Log.ExeName "kore-repl") - (fromNanoSecs 0) - ) - { Log.logLevel = Log.Debug - , Log.logType = Log.LogStdErr + Log GeneralLogOptions + { logLevel = Log.Debug + , logType = Log.LogStdErr + , timestampsSwitch = Log.TimestampsEnable + , logEntries = mempty } , "log [] stderr" `parsesTo_` - Log - ( defaultKoreLogOptions - (Log.ExeName "kore-repl") - (fromNanoSecs 0) - ) - { Log.logLevel = Log.Warning - , Log.logType = Log.LogStdErr + Log GeneralLogOptions + { logLevel = Log.Warning + , logType = Log.LogStdErr + , timestampsSwitch = Log.TimestampsEnable + , logEntries = mempty } , "log [DebugAttemptEquation] stderr" `parsesTo_` - Log - ( defaultKoreLogOptions - (Log.ExeName "kore-repl") - (fromNanoSecs 0) - ) - { Log.logLevel = Log.Warning - , Log.logType = Log.LogStdErr - , Log.logEntries = Set.singleton debugAttemptEquationType + Log GeneralLogOptions + { logLevel = Log.Warning + , logType = Log.LogStdErr + , logEntries = Set.singleton debugAttemptEquationType + , timestampsSwitch = Log.TimestampsEnable } , "log error [DebugAttemptEquation] stderr" `parsesTo_` - Log - ( defaultKoreLogOptions - (Log.ExeName "kore-repl") - (fromNanoSecs 0) - ) - { Log.logLevel = Log.Error - , Log.logType = Log.LogStdErr - , Log.logEntries = Set.singleton debugAttemptEquationType + Log GeneralLogOptions + { logLevel = Log.Error + , logType = Log.LogStdErr + , logEntries = Set.singleton debugAttemptEquationType + , timestampsSwitch = Log.TimestampsEnable } , "log info [ DebugAttemptEquation, DebugApplyEquation ] file \"f s\"" `parsesTo_` - Log - ( defaultKoreLogOptions - (Log.ExeName "kore-repl") - (fromNanoSecs 0) - ) - { Log.logLevel = Log.Info - , Log.logType = Log.LogFileText "f s" - , Log.logEntries = + Log GeneralLogOptions + { logLevel = Log.Info + , logType = Log.LogFileText "f s" + , logEntries = Set.fromList [debugAttemptEquationType, debugApplyEquationType] + , timestampsSwitch = Log.TimestampsEnable } , "log info [ DebugAttemptEquation DebugApplyEquation ] file \"f s\"" `parsesTo_` - Log - ( defaultKoreLogOptions - (Log.ExeName "kore-repl") - (fromNanoSecs 0) - ) - { Log.logLevel = Log.Info - , Log.logType = Log.LogFileText "f s" - , Log.logEntries = + Log GeneralLogOptions + { logLevel = Log.Info + , logType = Log.LogFileText "f s" + , logEntries = Set.fromList [debugAttemptEquationType, debugApplyEquationType] + , timestampsSwitch = Log.TimestampsEnable + } + ] + +debugAttemptEquationTests :: [ParserTest ReplCommand] +debugAttemptEquationTests = + [ "debug-attempt-equation" + `parsesTo_` + DebugAttemptEquation Log.DebugAttemptEquationOptions + { Log.selected = fromList + [] + } + , ("debug-attempt-equation " <> totalBalanceSymbolId) + `parsesTo_` + DebugAttemptEquation Log.DebugAttemptEquationOptions + { Log.selected = fromList + [totalBalanceSymbolId] + } + , ("debug-attempt-equation " <> totalBalanceSymbolId <> " " <> plusSymbolId) + `parsesTo_` + DebugAttemptEquation Log.DebugAttemptEquationOptions + { Log.selected = fromList + [totalBalanceSymbolId, plusSymbolId] + } + , "debug-attempt-equation label1 label2" + `parsesTo_` + DebugAttemptEquation Log.DebugAttemptEquationOptions + { Log.selected = fromList + ["label1", "label2"] + } + , "debug-attempt-equation MODULE.label1 MODULE.label2" + `parsesTo_` + DebugAttemptEquation Log.DebugAttemptEquationOptions + { Log.selected = fromList + ["MODULE.label1", "MODULE.label2"] + } + ] + +debugApplyEquationTests :: [ParserTest ReplCommand] +debugApplyEquationTests = + [ "debug-apply-equation" + `parsesTo_` + DebugApplyEquation Log.DebugApplyEquationOptions + { Log.selected = fromList + [] + } + , ("debug-apply-equation " <> totalBalanceSymbolId) + `parsesTo_` + DebugApplyEquation Log.DebugApplyEquationOptions + { Log.selected = fromList + [totalBalanceSymbolId] + } + , ("debug-apply-equation " <> totalBalanceSymbolId <> " " <> plusSymbolId) + `parsesTo_` + DebugApplyEquation Log.DebugApplyEquationOptions + { Log.selected = fromList + [totalBalanceSymbolId, plusSymbolId] + } + , "debug-apply-equation label1 label2" + `parsesTo_` + DebugApplyEquation Log.DebugApplyEquationOptions + { Log.selected = fromList + ["label1", "label2"] + } + , "debug-apply-equation MODULE.label1 MODULE.label2" + `parsesTo_` + DebugApplyEquation Log.DebugApplyEquationOptions + { Log.selected = fromList + ["MODULE.label1", "MODULE.label2"] } ] +debugEquationTests :: [ParserTest ReplCommand] +debugEquationTests = + [ "debug-equation" + `parsesTo_` + DebugEquation Log.DebugEquationOptions + { Log.selected = fromList + [] + } + , ("debug-equation " <> totalBalanceSymbolId) + `parsesTo_` + DebugEquation Log.DebugEquationOptions + { Log.selected = fromList + [totalBalanceSymbolId] + } + , ("debug-equation " <> totalBalanceSymbolId <> " " <> plusSymbolId) + `parsesTo_` + DebugEquation Log.DebugEquationOptions + { Log.selected = fromList + [totalBalanceSymbolId, plusSymbolId] + } + , "debug-equation label1 label2" + `parsesTo_` + DebugEquation Log.DebugEquationOptions + { Log.selected = fromList + ["label1", "label2"] + } + , "debug-equation MODULE.label1 MODULE.label2" + `parsesTo_` + DebugEquation Log.DebugEquationOptions + { Log.selected = fromList + ["MODULE.label1", "MODULE.label2"] + } + ] + +fromList :: [String] -> HashSet Text +fromList = HashSet.fromList . fmap Text.pack + +totalBalanceSymbolId, plusSymbolId :: String +totalBalanceSymbolId = + "Lbltotal'Unds'balance'LParUndsRParUnds'WITH-CONFIG'Unds'Int'Unds'AccountId" +plusSymbolId = + "Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp" + debugAttemptEquationType, debugApplyEquationType :: SomeTypeRep debugAttemptEquationType = someTypeRep (Proxy @DebugAttemptEquation) debugApplyEquationType = someTypeRep (Proxy @DebugApplyEquation)