[ cli ] option to disable CSE

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
 

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,20 +296,18 @@ 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
                         pure Nothing
     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)

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

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]

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