Add --dumpcases option

Output goes in the same directory as the generated code (so
build/exec/<appname>_app for the Chez back end)

CONTRIBUTORS

@@ -10,6 +10,7 @@ Christian Rasmussen
 David Smith 
 Edwin Brady 
 GhiOm 
+Guillaume Allais
 Ilya Rezvov 
 Jan de Muijnck-Hughes 
 Kamil Shakirov 

mkdist.sh

@@ -18,7 +18,7 @@ rsync -avm --include-from='srcfiles' -f 'hide,! */' dist idris2-$1
 # Copy run time support for Idris 2
 cp -r support idris2-$1/support
 # Copy top level files and docs
-cp *.md CONTRIBUTORS Makefile LICENSE idris2.ipkg idris2-$1
+cp *.md CONTRIBUTORS Makefile LICENSE *.ipkg idris2-$1
 
 tar zcvf idris2-$1.tgz idris2-$1
 shasum -a 256 idris2-$1.tgz > idris2-$1.tgz.sha256

src/Compiler/Common.idr

@@ -87,13 +87,47 @@ natHackNames
        NS ["Prelude"] (UN "natToInteger"),
        NS ["Prelude"] (UN "integerToNat")]
 
+export
+fastAppend : List String -> String
+fastAppend xs
+    = let len = cast (foldr (+) 0 (map length xs)) in
+          unsafePerformIO $
+             do b <- newStringBuffer (len+1)
+                build b xs
+                getStringFromBuffer b
+  where
+    build : StringBuffer -> List String -> IO ()
+    build b [] = pure ()
+    build b (x :: xs) = do addToStringBuffer b x
+                           build b xs
+
+dumpCases : {auto c : Ref Ctxt Defs} ->
+            String -> List Name ->
+            Core ()
+dumpCases fn cns
+    = do defs <- get Ctxt
+         cstrs <- traverse (dumpCase defs) cns
+         Right () <- coreLift $ writeFile fn (fastAppend cstrs)
+               | Left err => throw (FileErr fn err)
+         pure ()
+  where
+    dumpCase : Defs -> Name -> Core String
+    dumpCase defs n
+        = case !(lookupCtxtExact n (gamma defs)) of
+               Nothing => pure ""
+               Just d =>
+                    case compexpr d of
+                         Nothing => pure ""
+                         Just def => pure (show n ++ " = " ++ show def ++ "\n")
+
 -- Find all the names which need compiling, from a given expression, and compile
 -- them to CExp form (and update that in the Defs)
 export
-findUsedNames : {auto c : Ref Ctxt Defs} -> Term vars ->
+findUsedNames : {auto c : Ref Ctxt Defs} ->
-                Core (List Name, NameTags)
+                Term vars -> Core (List Name, NameTags)
 findUsedNames tm
     = do defs <- get Ctxt
+         sopts <- getSession
          let ns = getRefs (Resolved (-1)) tm
          natHackNames' <- traverse toResolvedNames natHackNames
          -- make an array of Bools to hold which names we've found (quicker
@@ -116,6 +150,10 @@ findUsedNames tm
          logTime ("Compile defs " ++ show (length cns) ++ "/" ++ show asize) $
            traverse_ (compileDef tycontags) cns
          logTime "Inline" $ traverse_ inlineDef cns
+         maybe (pure ())
+               (\f => do coreLift $ putStrLn $ "Dumping case trees to " ++ f
+                         dumpCases f cns)
+               (dumpcases sopts)
          pure (cns, tycontags)
   where
     primTags : Int -> NameTags -> List Constant -> NameTags
@@ -212,17 +250,3 @@ copyLib (lib, fullname)
                  Right _ <- coreLift $ writeToFile lib bin
                     | Left err => throw (FileErr lib err)
                  pure ()
-
-export
-fastAppend : List String -> String
-fastAppend xs
-    = let len = cast (foldr (+) 0 (map length xs)) in
-          unsafePerformIO $
-             do b <- newStringBuffer (len+1)
-                build b xs
-                getStringFromBuffer b
-  where
-    build : StringBuffer -> List String -> IO ()
-    build b [] = pure ()
-    build b (x :: xs) = do addToStringBuffer b x
-                           build b xs

src/Core/Options.idr

@@ -98,6 +98,7 @@ record Session where
   logLevel : Nat
   logTimings : Bool
   debugElabCheck : Bool -- do conversion check to verify results of elaborator
+  dumpcases : Maybe String -- file to output compiled case trees
 
 public export
 record PPrinter where
@@ -142,7 +143,7 @@ defaultPPrint : PPrinter
 defaultPPrint = MkPPOpts False True False
 
 defaultSession : Session
-defaultSession = MkSessionOpts False False False Chez 0 False False
+defaultSession = MkSessionOpts False False False Chez 0 False False Nothing
 
 defaultElab : ElabDirectives
 defaultElab = MkElabDirectives True True PartialOK 3

src/Idris/CommandLine.idr

@@ -69,6 +69,8 @@ data CLOpt
   Yaffle String |
    ||| Dump metadata from a .ttm file
   Metadata String |
+   ||| Dump cases before compiling
+  DumpCases String |
    ||| Run a REPL command then exit immediately
   RunREPL String |
   FindIPKG |
@@ -143,6 +145,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               Nothing, -- run ttimp REPL rather than full Idris
            MkOpt ["--ttm" ] ["ttimp file"] (\f => [Metadata f])
               Nothing, -- dump metadata information from the given ttm file
+           MkOpt ["--dumpcases"] ["output file"] (\f => [DumpCases f])
+              Nothing, -- dump case trees to the given file
            MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
               Nothing -- do more elaborator checks (currently conversion in LinearCheck)
            ]

src/Idris/SetOptions.idr

@@ -86,6 +86,9 @@ preOptions (RunREPL _ :: opts)
 preOptions (FindIPKG :: opts)
     = do setSession (record { findipkg = True } !getSession)
          preOptions opts
+preOptions (DumpCases f :: opts)
+    = do setSession (record { dumpcases = Just f } !getSession)
+         preOptions opts
 preOptions (_ :: opts) = preOptions opts
 
 -- Options to be processed after type checking. Returns whether execution