From a7b1113078453274aaf1e4823dbd0cdc43a91eb0 Mon Sep 17 00:00:00 2001 From: Aleksei Volkov Date: Tue, 28 Nov 2023 21:58:28 +0300 Subject: [PATCH] [ cli ] option to disable CSE --- CHANGELOG.md | 4 +++- src/Compiler/Opts/CSE.idr | 47 ++++++++++++++++++++++----------------- src/Core/Options.idr | 3 ++- src/Idris/CommandLine.idr | 6 ++++- src/Idris/SetOptions.idr | 3 +++ 5 files changed, 39 insertions(+), 24 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 36cc8b1bf6b..905db7b4a4d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -32,11 +32,13 @@ These features together give an ability to inspect whether particular expressions are recursive (including mutual recursion). -### REPL changes +### REPL/CLI changes * Adds documentation for unquotes `~( )`. * Adds documentation for laziness and codata primitives: `Lazy`, `Inf`, `Delay`, and `Force`. +* Adds `--no-cse` command-line option to disable common subexpression elimination + for code generation debugging. ### Backend changes diff --git a/src/Compiler/Opts/CSE.idr b/src/Compiler/Opts/CSE.idr index e469fcc0c5a..59595e75219 100644 --- a/src/Compiler/Opts/CSE.idr +++ b/src/Compiler/Opts/CSE.idr @@ -30,7 +30,9 @@ module Compiler.Opts.CSE import Core.CompileExpr import Core.Context import Core.Context.Log +import Core.Core import Core.Name +import Core.Options import Core.TT import Core.Ord @@ -294,11 +296,10 @@ analyzeDef d@(MkCon _ _ _) = pure d analyzeDef d@(MkForeign _ _ _) = pure d analyzeDef d@(MkError _) = pure d -analyzeName : Ref Sts St - => Ref Ctxt Defs +compileName : Ref Ctxt Defs => Name -> Core (Maybe (Name, FC, CDef)) -analyzeName fn = do +compileName fn = do defs <- get Ctxt Just def <- lookupCtxtExact fn (gamma defs) | Nothing => do log "compile.execute" 50 $ "Couldn't find " ++ show fn @@ -306,8 +307,7 @@ analyzeName fn = do let Just cexp = compexpr def | Nothing => do log "compile.execute" 50 $ "Couldn't compile " ++ show fn pure Nothing - cexp' <- analyzeDef cexp - pure $ Just (fn, location def, cexp') + pure $ Just (fn, location def, cexp) -------------------------------------------------------------------------------- -- Replacing Expressions @@ -472,19 +472,24 @@ cse : Ref Ctxt Defs -> (mainExpr : CExp ns) -> Core (List (Name, FC, CDef), CExp ns) cse defs me = do - log "compiler.cse" 10 $ "Analysing " ++ show (length defs) ++ " names" - s <- newRef Sts $ MkSt empty 0 - analyzedDefs <- catMaybes <$> traverse analyzeName defs - MkSt um _ <- get Sts - srep <- newRef ReplaceMap $ toReplaceMap um - replacedDefs <- traverse replaceDef analyzedDefs - replacedMain <- replaceExp 1 me - replaceMap <- get ReplaceMap - let filtered = SortedMap.toList replaceMap - log "compiler.cse" 10 $ unlines $ - "Found the following unadjusted subexpressions:" - :: map (\(name,(_,cnt)) => - show name ++ ": count " ++ show cnt - ) filtered - let newDefs := newToplevelDefs replaceMap ++ replacedDefs - pure (newDefs, replacedMain) + compilerDefs <- get Ctxt + compiledDefs <- catMaybes <$> traverse compileName defs + if compilerDefs.options.session.noCSE + then pure (compiledDefs, me) + else do + log "compiler.cse" 10 $ "Analysing " ++ show (length defs) ++ " names" + s <- newRef Sts $ MkSt empty 0 + analyzedDefs <- traverse (traversePair (traversePair analyzeDef)) compiledDefs + MkSt um _ <- get Sts + srep <- newRef ReplaceMap $ toReplaceMap um + replacedDefs <- traverse replaceDef analyzedDefs + replacedMain <- replaceExp 1 me + replaceMap <- get ReplaceMap + let filtered = SortedMap.toList replaceMap + log "compiler.cse" 10 $ unlines $ + "Found the following unadjusted subexpressions:" + :: map (\(name,(_,cnt)) => + show name ++ ": count " ++ show cnt + ) filtered + let newDefs := newToplevelDefs replaceMap ++ replacedDefs + pure (newDefs, replacedMain) diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 5bbe901dc38..edddaebc4c4 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -159,6 +159,7 @@ record Session where profile : Bool -- generate profiling information, if supported logErrorCount : Nat -- when parsing alternatives fails, how many errors -- should be shown. + noCSE : Bool -- disable common subexpression elimination -- Warnings warningsAsErrors : Bool @@ -222,7 +223,7 @@ export defaultSession : Session defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False False defaultLogLevel Nothing False Nothing Nothing - Nothing Nothing False 1 False True + Nothing Nothing False 1 False False True False [] False False export diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 4cce94016a3..cef2d6d954f 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -161,7 +161,9 @@ data CLOpt ||| Generate bash completion script BashCompletionScript String | ||| Turn on %default total globally - Total + Total | + ||| Disable common subexpression elimination + NoCSE ||| Extract the host and port to bind the IDE socket to export @@ -244,6 +246,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] (Just $ "Set output directory"), MkOpt ["--profile"] [] [Profile] (Just "Generate profile data when compiling, if supported"), + MkOpt ["--no-cse"] [] [NoCSE] + (Just "Disable common subexpression elimination"), optSeparator, MkOpt ["--total"] [] [Total] diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 5a60149fad0..a90fa532566 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -433,6 +433,9 @@ preOptions (BashCompletionScript fun :: _) preOptions (Total :: opts) = do updateSession ({ totalReq := Total }) preOptions opts +preOptions (NoCSE :: opts) + = do updateSession ({ noCSE := True }) + preOptions opts preOptions (_ :: opts) = preOptions opts -- Options to be processed after type checking. Returns whether execution