Skip to content

Tool for making sense of the Haskell code generated by the Agda compiler

License

Notifications You must be signed in to change notification settings

agda/agda-ghc-names

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

5 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

MOTIVATION:
  When compiling Agda source via the current default backend MAlonzo,
  this generates Haskell code, with automatically generated Haskell
  identifiers of the shape ``MAlonzo.Code.MyHaskellisedModuleName.dXYZ''
  for Agda entities that translate to Haskell program-level variables.
  If the MAlonzo-generated Haskell is compiled for profiling,
  and run with profiling enabled, the GHC run-time system writes
  these identifiers to the *.prof (and *.hp) files.
  This makes direct inspection of *.prof files of limited use for the
  Agda developer. The tool ``agda-ghc-names fixprof'' included here
  translates these *.prof files to *.agdaIdents.prof,
  where each dXYZ is replaced with the Agda identifier it originates from.


agda-ghc-names extract <dir>
  assumes that all *.hs files below <dir> have been generated by MAlonzo,
  and extracts the mapping from their Haskell names to the original
  Agda names. Typically, <dir> will be the --compile-dir argument
  used when compiling an Agda program.
  The mapping is saved in <dir>/agda-ghc-name-cache.dat .

  For a medium-size project, this requires around 3GB of heap space,
  and takes around 100 seconds.
  (The heavy heap usage is due to the use of haskell-src-exts
    for parsing the MAlonzo-generated Haskell files, which may be quite large.)

agda-ghc-names fixprof {+m} {+s} <dir> <progname>.prof
  generates <progname>.agdaIdents*.prof by replacing Haskell identifiers
  in <progname>.prof by Agda identifiers, as far as these can be found
  in MAlonzo-compiled *.hs files below <dir>.
  This reads <dir>/agda-ghc-name-cache.dat if it already exists,
  and otherwise generates it in the same way as
  ``agda-ghc-names extract <dir>''.
  The option ``+m'' includes also the original Haskell module column
  in the output.
  The option ``+s'' includes also the original Haskell source location column
  added in GHC-8 in the output.

agda-ghc-names find <dir> {hsIdents}
  also reads <dir>/agda-ghc-name-cache.dat if it already exists,
  and otherwise generates it in the same ways as ``agda-ghc-names extract <dir>''.
  Subsequently:
   * For each qualified Haskell identifier in {hsIdents}
     (which typically start with ``MAlonzo.Code.''),
     it prints the Agda identifiers corresponding to it.
     If {hsIdents} contains exactly one qualified identifier,
     then only the Agda identifier is printed;
     otherwise the mapping ``<hsIdent> |-> <agdaIdent>''
     is printed for each identifier given.
   * Each unqualified Haskell identifier in {hsIdents}
     is looked up in all module maps.
  If none are given on the command line, they are read from standard input.

agda-ghc-names find -m <dir> {hsModNames}
  instead dumps the whole association list for each module specified.

About

Tool for making sense of the Haskell code generated by the Agda compiler

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published