From 59503712f39422d9cea52f051aa2eb8c01281eca Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 2 Apr 2020 16:06:00 +0100 Subject: [PATCH] Add --dumpcases option Output goes in the same directory as the generated code (so build/exec/_app for the Chez back end) --- CONTRIBUTORS | 1 + mkdist.sh | 2 +- src/Compiler/Common.idr | 56 ++++++++++++++++++++++++++++----------- src/Core/Options.idr | 3 ++- src/Idris/CommandLine.idr | 4 +++ src/Idris/SetOptions.idr | 3 +++ 6 files changed, 51 insertions(+), 18 deletions(-) diff --git a/CONTRIBUTORS b/CONTRIBUTORS index eaafc70..9015d0d 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -10,6 +10,7 @@ Christian Rasmussen David Smith Edwin Brady GhiOm +Guillaume Allais Ilya Rezvov Jan de Muijnck-Hughes Kamil Shakirov diff --git a/mkdist.sh b/mkdist.sh index d3203ab..60574f1 100755 --- a/mkdist.sh +++ b/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 diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index f90da84..09d816a 100644 --- a/src/Compiler/Common.idr +++ b/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 -> - Core (List Name, NameTags) +findUsedNames : {auto c : Ref Ctxt Defs} -> + 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 diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 7b3df44..f700f61 100644 --- a/src/Core/Options.idr +++ b/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 diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index e7f47c9..01b5947 100644 --- a/src/Idris/CommandLine.idr +++ b/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) ] diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 25ee0d4..b9d9ae6 100644 --- a/src/Idris/SetOptions.idr +++ b/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