package idris2-dep-graph-test
version = 0.1.0
authors = "Tomáš Zemanovič"
-- maintainers =
-- license =
-- brief =
-- readme =
-- homepage =
-- sourceloc =
-- bugtracker =
-- the Idris2 version required (e.g. langversion >= 0.5.1)
-- langversion
-- packages to add to search path
depends = idris2-dep-graph
-- modules to install
-- modules =
-- main file (i.e. file to load at REPL)
main = Main
-- name of executable
executable = "idris2-dep-graph-test"
-- opts =
sourcedir = "src"
-- builddir =
-- outputdir =
-- script to run before building
-- prebuild =
-- script to run after building
-- postbuild =
-- script to run after building, before installing
-- preinstall =
-- script to run after installing
-- postinstall =
-- script to run before cleaning
-- preclean =
-- script to run after cleaning
-- postclean =

module Main
main : IO ()
main = putStrLn "Test successful!"

module Main
import DepGraph.Data
import DepGraph.Cli
import Idris.Package.Extra
import Idris.Driver.Extra
import Compiler.Common
import Core.Context
import Core.Directory
import Core.InitPrimitives
import Data.String
import Idris.Error
import Idris.Pretty
import Idris.ModTree
import Idris.SetOptions
import Idris.Syntax
import Idris.REPL
import System
import System.File
import System.Term
import Libraries.Data.StringMap
import Libraries.System.Directory.Tree
import Libraries.Utils.Path
%hide Idris.Syntax.Module -- DepGraph.Data.Module
--------------------------------------------------------------------------------
-- Common utils
--------------------------------------------------------------------------------
loadPkg :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  String ->
  Core (PkgDesc, String)
loadPkg file = do
  let Just (root, filename) = splitParent file
      | _ => throw $ InternalError "Tried to split empty string"
  let True = isSuffixOf ".ipkg" filename
      | _ => do
        coreLift $ putStrLn $
          "Packages must have an '.ipkg' extension: " ++ show file ++ "."
        coreLift $ exitWith $ ExitFailure 1
  setWorkingDir root
  pkg <- parsePkgFile True filename
  pure (pkg, root)
||| Ensure file path is absolute (uses `getWorkingDir`)
toAbsolute : String -> Core String
toAbsolute path = do
  if isAbsolute path
    then pure path
    else do
      wdir <- getWorkingDir
      pure $ wdir </> path
--------------------------------------------------------------------------------
-- Modules dependency graph
--------------------------------------------------------------------------------
processMod :
  (modFilter : List ModuleIdent -> List ModuleIdent) ->
  BuildMod ->
  Module
processMod modFilter mod =
  MkModule
    { name = show mod.buildNS
    , deps = show <$> modFilter mod.imports
    }
record RawPkgModules where
  constructor MkRawPkgModules
  name : String
  root : String
  ||| Absolute paths to modules
  mods : List String
  buildMods : List BuildMod
processPkgMods :
  ModOpts ->
  (localMods : List ModuleIdent) ->
  RawPkgModules ->
  PkgModules
processPkgMods opts localMods rawPkg = do
  let MkRawPkgModules { name, root, mods, buildMods } = rawPkg
  let modules = (processMod modFilter) <$> buildMods
  MkPkgModules { name, modules }
  where
    modFilter : List ModuleIdent -> List ModuleIdent
    modFilter =
      if opts.withExternal
       then id
       else filter $ \mod => any (== mod) localMods
getLocalMods :
  ModOpts ->
  (localFiles : List String) ->
  RawPkgModules ->
  List ModuleIdent
getLocalMods opts localFiles rawPkg =
  buildNS <$> (modFilter rawPkg.root) rawPkg.buildMods
  where
    modFilter : String -> List BuildMod -> List BuildMod
    modFilter dir =
      if opts.withExternal
       then id
       else filter $ \mod =>
         any (\local => (dir </> buildFile mod) == local) localFiles
findPkgModules :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  PkgDesc ->
  Core (List String)
findPkgModules pkg = do
  withWarnings $ addDeps pkg
  runScript (prebuild pkg)
  pure $ maybe (map snd (modules pkg))
               (\m => snd m :: map snd (modules pkg))
               (mainmod pkg)
getAllBuildMods :
  {auto c : Ref Ctxt Defs} ->
  {auto o : Ref ROpts REPLOpts} ->
  FC -> (done : List BuildMod) ->
  (allFiles : List String) ->
  Core (List BuildMod)
getAllBuildMods fc done [] = pure done
getAllBuildMods fc done (f :: fs) = do
  ms <- getBuildMods fc done f
  getAllBuildMods fc (ms ++ done) fs
loadPkgModules :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  String ->
  Core RawPkgModules
loadPkgModules file = do
  (pkg, root) <- loadPkg file
  whenJust (builddir pkg) setBuildDir
  setOutputDir (outputdir pkg)
  mods <- traverse toAbsolute !(findPkgModules pkg)
  -- There might be duplicates, so if something is already processed, drop it
  buildMods <- dropLater <$> getAllBuildMods EmptyFC [] mods
  pure $ MkRawPkgModules { name = pkg.name, root, mods, buildMods }
  where
    dropLater : List BuildMod -> List BuildMod
    dropLater [] = []
    dropLater (b :: bs)
        = b :: dropLater (filter (\x => buildFile x /= buildFile b) bs)
modMain :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  ModOpts ->
  List String ->
  Core ()
modMain opts files = do
  pkgs <- for files loadPkgModules
  let localFiles = concat $ mods <$> pkgs
  let localMods = concat $ getLocalMods opts localFiles <$> pkgs
  let modules = (processPkgMods opts localMods) <$> pkgs
  coreLift $ putStrLn $ show modules
--------------------------------------------------------------------------------
-- Package dependency graph
--------------------------------------------------------------------------------
processPackage :
  (isLocal : Bool) ->
  (localOnly : Bool) ->
  (localPkgs : List String) ->
  PkgDesc ->
  Core Package
processPackage isLocal localOnly localPkgs pkg = do
  pure $ MkPackage pkg.name deps isLocal
  where
    depName : Depends -> String
    depName dep = dep.pkgname
    pkgFilter : List String -> List String
    pkgFilter = if localOnly
      then filter $ \pkg => any (== pkg) localPkgs
      else id
    deps : List String
    deps = pkgFilter $ depName <$> pkg.depends
record Candidate where
  constructor MkCandidate
  name      : String
  version   : Maybe PkgVersion
  directory : String
toCandidate : (name : String) -> (String,Maybe PkgVersion) -> Candidate
toCandidate name (dir,v) = MkCandidate name v dir
record ResolutionError where
  constructor MkRE
  decisions : List Candidate
  depends   : Depends
  version   : Maybe PkgVersion
prepend : Candidate -> ResolutionError -> ResolutionError
prepend p = { decisions $= (p ::)}
reason : Maybe PkgVersion -> String
reason Nothing  = "no matching version is installed."
reason (Just x) = "only found version \{show x} which is out of bounds."
printResolutionError : ResolutionError -> String
printResolutionError (MkRE ds d v) = go [<] ds
  where go : SnocList String -> List Candidate -> String
        go ss []        =
          let pre        := "Required \{d.pkgname} \{show d.pkgbounds} but"
              failure    := "\{pre} \{reason v}"
              candidates := case ss of
                               [<] => ""
                               ss  => " Resolved transitive dependencies: " ++ (fastConcat $ intersperse "; " $ cast ss) ++ "."
           in failure ++ candidates
        go ss (c :: cs) =
          let v := fromMaybe defaultVersion c.version
           in go (ss :< "\{c.name}-\{show v}") cs
data ResolutionRes : Type where
  Resolved : List String -> ResolutionRes
  Failed   : List ResolutionError -> ResolutionRes
printErrs : (pkgDirs : List String) -> PkgDesc -> List ResolutionError -> String
printErrs pkgDirs x es =
  let errors := unlines $ "Failed to resolve the dependencies for \{x.name}:"
                          :: map (indent 2 . printResolutionError) es
      dirs   := unlines $ "Searched for packages in:"
                          :: map (indent 2) pkgDirs
  in """
     \{errors}
     \{dirs}
     For more details on what packages Idris2 can locate, run `idris2 --list-packages`
     """
-- try all possible resolution paths, keeping the first
-- that works
tryAll :  List Candidate
       -> (Candidate -> Core ResolutionRes)
       -> Core ResolutionRes
tryAll ps f = go [<] ps
  where go :  SnocList ResolutionError
           -> List Candidate
           -> Core ResolutionRes
        go se []        = pure (Failed $ se <>> [])
        go se (x :: xs) = do
          Failed errs <- f x | Resolved res => pure (Resolved res)
          go (se <>< map (prepend x) errs) xs
pkgDirs :
    {auto c : Ref Ctxt Defs} ->
    Core (List String)
pkgDirs = do
  localdir <- pkgLocalDirectory
  d <- getDirs
  pure (localdir ::  (show <$> d.package_search_paths))
||| Find all dependencies (transitively) from the given package file.
findDeps :
    {auto c : Ref Ctxt Defs} ->
    {auto s : Ref Syn SyntaxInfo} ->
    {auto o : Ref ROpts REPLOpts} ->
    PkgDesc ->
    Core (List String)
findDeps pkg = do
  Resolved allPkgs <- getTransitiveDeps pkg.depends empty
    | Failed errs => throw $ GenericMsg EmptyFC (printErrs !pkgDirs pkg errs)
  log "package.depends" 10 $ "all depends: \{show allPkgs}"
  pure allPkgs
  where
    -- Note: findPkgDir throws an error if a package is not found
    -- *unless* --ignore-missing-ipkg is enabled
    -- therefore, if findPkgDir returns Nothing, skip the package
    --
    -- We use a backtracking algorithm here: If several versions of
    -- a package are installed, we must try all, which are are
    -- potentially in bounds, because their set of dependencies
    -- might be different across versions and not all of them
    -- might lead to a resolvable situation.
    getTransitiveDeps :
        List Depends ->
        (done : StringMap (Maybe PkgVersion, String)) ->
        Core ResolutionRes
    getTransitiveDeps [] done = do
      ms <- for (StringMap.toList done) $
        \(pkg, (mv, pkgFile)) => do pure $ (</> pkgFile) <$> !(findPkgDir pkg (exactBounds mv))
      pure . Resolved $ catMaybes ms
    getTransitiveDeps (dep :: deps) done =
      case lookup dep.pkgname done of
        Just (mv, pkgFile) =>
          if inBounds mv dep.pkgbounds
            -- already resolved dependency is in bounds
            -- so we keep it and resolve remaining deps
            then getTransitiveDeps deps done
            -- the resolved dependency does not satisfy the
            -- current bounds. we return an error and backtrack
            else pure (Failed [MkRE [] dep $ mv <|> Just defaultVersion])
        Nothing => do
          log "package.depends" 50 "adding new dependency: \{dep.pkgname} (\{show dep.pkgbounds})"
          pkgDirs <- findPkgDirs dep.pkgname dep.pkgbounds
          let candidates := toCandidate dep.pkgname <$> pkgDirs
          case candidates of
            [] => do
              defs <- get Ctxt
              if defs.options.session.ignoreMissingPkg
                -- this corresponds to what `findPkgDir` does in
                -- case of `ignoreMissingPkg` being set to `True`
                then getTransitiveDeps deps done
                else pure (Failed [MkRE [] dep Nothing])
            _  => tryAll candidates $ \(MkCandidate name mv pkgDir) => do
              let pkgFile = pkgDir </> name <.> "ipkg"
              True <- coreLift $ exists pkgFile
                | False => getTransitiveDeps deps (insert name (mv, pkgFile) done)
              pkg <- parsePkgFile False pkgFile
              getTransitiveDeps
                (pkg.depends ++ deps)
                (insert pkg.name (pkg.version, pkgFile) done)
pkgMain :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  PkgOpts ->
  List String ->
  Core ()
pkgMain opts files = do
  let MkPkgOpts {localOnly} = opts
  pkgsWithRoots <- for files loadPkg
  let pkgs = fst <$> pkgsWithRoots
  let localPkgs = (.name) <$> pkgs
  deps <- if localOnly
    then pure []
    else do
      -- Remove duplicates
      deps <- dropLater <$> concat <$> for pkgs findDeps
      pkgsWithRoots <- for deps loadPkg
      let deps = fst <$> pkgsWithRoots
      -- There might also be local pkgs in deps, remove those too
      pure $ filter (\d => all (\local => local /= d.name) localPkgs) deps
  local <- for pkgs $ processPackage True localOnly localPkgs
  deps <- for deps $ processPackage False localOnly localPkgs
  coreLift $ putStrLn $ show (local ++ deps)
  where
    dropLater : List String -> List String
    dropLater [] = []
    dropLater (b :: bs)
        = b :: dropLater (filter (/= b) bs)
--------------------------------------------------------------------------------
-- Common
--------------------------------------------------------------------------------
setupPackPkgPath :
  {auto c : Ref Ctxt Defs} ->
  Core Bool
setupPackPkgPath = do
  (res, code) <- coreLift $ run "pack package-path"
  let success = code >= 0
  when success $
    traverseList1_ addPackageSearchPath $ splitPaths res
  pure success
findIpkgs : {root : Path} -> Tree root -> IO (List String)
findIpkgs t = depthFirst check t (pure [])
  where
    check : {root : Path} -> FileName root ->
            Lazy (IO (List String)) -> IO (List String)
    check fn next = do
      if ".ipkg" `isSuffixOf` fileName fn
        then do pure $ (toFilePath fn) :: !next
        else next
||| If the user did not provide any package file we can look in the working
||| directory.
localPackageFiles : List String -> Core (List String)
localPackageFiles pkgs@(_ :: _) = for pkgs toAbsolute
localPackageFiles _ = do
  wdir <- getWorkingDir
  tree <-  coreLift $ filter filePred dirPred <$> (explore $ parse wdir)
  candidates <- coreLift $ findIpkgs tree
  let pkgs = filter (".ipkg" `isSuffixOf`) candidates
  for pkgs toAbsolute
    where
      filePred : {root : _} -> FileName root -> Bool
      filePred name = True
      dirPred : {root : _} -> FileName root -> Bool
      dirPred name = all (/= fileName name) ignore
        where
          ignore : List String
          ignore = [".git", ".pijul"]
handleSubCmd :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  List String ->
  List CLOpt ->
  Core ()
handleSubCmd pathargs opts = do
  files <- localPackageFiles pathargs
  case subCmd opts of
    SubCmdMod opts => modMain opts files
    SubCmdPkg opts => pkgMain opts files
quitWithError :
  {auto c : Ref Ctxt Defs} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto o : Ref ROpts REPLOpts} ->
  Error ->
  Core a
quitWithError err = do
  doc <- display err
  msg <- render doc
  coreLift (die msg)
auxMain : List CLOpt -> Core ()
auxMain opts = do
  defs <- initDefs
  c <- newRef Ctxt defs
  s <- newRef Syn initSyntax
  setCG {c} Chez
  addPrimitives
  setWorkingDir "."
  let outmode = REPL InfoLvl
  o <- newRef ROpts (REPL.Opts.defaultOpts Nothing outmode [])
  True <- setupPackPkgPath
    | False => updateEnv
  let ipkgs = findInputs opts
  flip catch quitWithError $ handleSubCmd ipkgs opts
main : IO ()
main = do
  Right opts <- getCmdOpts
    | Left err => do ignore $ fPutStrLn stderr $ "Error: " ++ err
                     exitWith (ExitFailure 1)
  continue <- quitOpts opts
  when continue $ do
    setupTerm
    coreRun (auxMain opts)
      (\err : Error => do ignore $ fPutStrLn stderr $ "Uncaught error: " ++ show err
                          exitWith (ExitFailure 1))
      (\res => pure ())

||| Re-exports Idris.Package with some private declarations.
|||
||| `Idris.Package` private items are visible here because of the common module
||| prefix.
|||
||| Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.
module Idris.Package.Extra
import public Idris.Package
import Idris.Package as P
import Idris.REPL
import Idris.Syntax
import IdrisPaths
||| Emit captured warnings from inner scope and clear them
||| afterwards (to avoid emitting them in some unrelated
||| codepath later).
export
withWarnings : Ref Ctxt Defs =>
               Ref Syn SyntaxInfo =>
               Ref ROpts REPLOpts =>
               Core a -> Core a
withWarnings = P.withWarnings
export
runScript : Maybe (FC, String) -> Core ()
runScript = P.runScript
||| Add all dependencies (transitively) from the given package file into the
||| context so modules from each is accessible during compilation.
export
addDeps :
    {auto c : Ref Ctxt Defs} ->
    {auto s : Ref Syn SyntaxInfo} ->
    {auto o : Ref ROpts REPLOpts} ->
    PkgDesc ->
    Core ()
addDeps = P.addDeps

||| Re-exports Idris.Driver with some private declarations.
|||
||| `Idris.Driver` private items are visible here because of the common module
||| prefix.
|||
||| Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.
module Idris.Driver.Extra
import public Idris.Driver
import Core.Context
import Data.List1
import Idris.Driver as D
import Idris.REPL
export
updateEnv : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            Core ()
updateEnv = D.updateEnv
export
splitPaths : String -> List1 String
splitPaths = D.splitPaths

module DepGraph.Data
import Data.String
%default total
dquote : String -> String
dquote str = "\"" ++ str ++ "\""
joinSemicolon : List String -> String
joinSemicolon = joinBy "; "
--------------------------------------------------------------------------------
-- Modules dependency graph
--------------------------------------------------------------------------------
public export
record Module where
  constructor MkModule
  name : String
  deps : List String
public export
record PkgModules where
  constructor MkPkgModules
  name : String
  modules : List Module
public export
PkgsModules : Type
PkgsModules = List PkgModules
export
Show PkgsModules where
  show pkgs = "digraph { splines=\"ortho\";" ++ subgraphs ++ edges ++ "}"
    where
      depEdge : String -> String -> String
      depEdge srcName destName = dquote srcName ++ " -> " ++ dquote destName
      moduleEdge : Module -> String
      moduleEdge mod = joinSemicolon $ depEdge mod.name <$> mod.deps
      pkgEdge : PkgModules -> String
      pkgEdge pkg = concat $ moduleEdge <$> pkg.modules
      moduleNode : Module -> String
      moduleNode mod = dquote mod.name ++ "[style=\"filled\", fillcolor=white]"
      pkgSubgraph : PkgModules -> String
      pkgSubgraph pkg =
        -- prefix the name with "cluster" to group its nodes in a labelled box
        "subgraph " ++ (dquote $ "cluster_" ++ pkg.name)
        ++ "{"
        ++ "style=\"filled\"; fillcolor = \"linen\";"
        ++ "label=" ++ dquote pkg.name ++ ";"
        ++ (joinSemicolon $ moduleNode <$> pkg.modules)
        ++ "}"
      subgraphs, edges : String
      subgraphs = concat $ pkgSubgraph <$> pkgs
      edges = concat $ pkgEdge <$> pkgs
--------------------------------------------------------------------------------
-- Packages dependency graph
--------------------------------------------------------------------------------
public export
record Package where
  constructor MkPackage
  name : String
  deps : List String
  isLocal : Bool
public export
Packages : Type
Packages = List Package
export
Show Packages where
  show pkgs = "digraph {" ++ inner ++ "}"
    where
      depEdge : String -> String -> String
      depEdge srcName destName = dquote srcName ++ " -> " ++ dquote destName
      pkgEdge : Package -> List String
      pkgEdge pkg = depEdge pkg.name <$> pkg.deps
      pkgNode : Package -> String
      pkgNode pkg =
        (dquote pkg.name)
        ++ "["
        ++ (if pkg.isLocal
             then "style=\"filled\"; fillcolor =\"linen\";"
             else "")
        ++ "]"
      edges = concat $ pkgEdge <$> pkgs
      nodes = pkgNode <$> pkgs
      inner = joinSemicolon (nodes ++ edges)

module DepGraph.Cli
import Data.List1
import Data.String
import System
public export
record ModOpts where
  constructor MkModOpts
  withExternal : Bool
public export
record PkgOpts where
  constructor MkPkgOpts
  localOnly : Bool
||| CLOpt - possible command line options
public export
data CLOpt
  =
  ||| Module import graph
  Module ModOpts |
  ||| Package dependency graph
  Package PkgOpts |
  ||| The input Idris file
  InputFile String |
  ||| Display help text
  Help |
  ||| Display app version
  Version
data OptType
  = Required String
  | Optional String
  | Flag String
public export
data SubCmd =
  ||| Module import graph
  SubCmdMod ModOpts |
  ||| Package dependency graph
  SubCmdPkg PkgOpts
Show OptType where
  show (Required a) = "<" ++ a ++ ">"
  show (Optional a) = "[" ++ a ++ "]"
  show (Flag a) = "[--" ++ a ++ "]"
ActType : List OptType -> Type
ActType [] = List CLOpt
ActType (Required a :: as) = String -> ActType as
ActType (Optional a :: as) = Maybe String -> ActType as
ActType (Flag a :: as) = Bool -> ActType as
record OptDesc where
  constructor MkOpt
  flags : List String
  argdescs : List OptType
  action : ActType argdescs
  help : Maybe String
optSeparator : OptDesc
optSeparator = MkOpt [] [] [] Nothing
showDefault : Show a => a -> String
showDefault x = "(default " ++ show x ++ ")"
options : List OptDesc
options =
  [ MkOpt ["package", "pkg", "p"] [Flag "local-only"]
      (\localOnly => [Package $ MkPkgOpts {localOnly}])
      (Just "(default) Generate a package dependency graph")
  , MkOpt ["module", "mod", "m"] [Flag "with-external"]
      (\withExternal => [Module $ MkModOpts {withExternal}])
      (Just "Generate a module import graph")
  , MkOpt ["--help", "-h", "-?"] [] [Help]
      (Just "Display help text")
  , MkOpt ["--version", "-v"] [] [Version]
      (Just "Display version string")
  ]
optShow : OptDesc -> (String, Maybe String)
optShow (MkOpt [] _ _ _) = ("", Just "")
optShow (MkOpt flags argdescs action help) =
  (showSep ", " flags ++ " " ++ showSep " " (map show argdescs), help)
  where
    showSep : String -> List String -> String
    showSep sep [] = ""
    showSep sep [x] = x
    showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
firstColumnWidth : Nat
firstColumnWidth = foldr max 0 $ map (length . fst . optShow) options
makeTextFromOptionsOrEnvs : List (String, Maybe String) -> String
makeTextFromOptionsOrEnvs rows = concatMap (optUsage firstColumnWidth) rows
  where
    optUsage : Nat -> (String, Maybe String) -> String
    optUsage maxOpt (optshow, help) =
      maybe
        ""  -- Don't show anything if there's no help string (that means
            -- it's an internal option)
        (\h =>
          "  " ++ optshow ++
          pack (List.replicate (minus (maxOpt + 2) (length optshow)) ' ') ++
          h ++ "\n")
        help
optsUsage : String
optsUsage = makeTextFromOptionsOrEnvs $ map optShow options
-- TODO get version from .ipkg
export
versionMsg : String
versionMsg = "Dep-graph version 0.1.0"
export
usage : String
usage = """
  \{ versionMsg }
  Usage: dep-graph [options] [ipkg file...]
  Available options:
  \{ optsUsage }
  """
processArgs : String -> (args : List OptType) -> List String -> ActType args ->
              Either String (List CLOpt, List String)
processArgs flag [] xs f = Right (f, xs)
-- Missing required arguments
processArgs flag (opt@(Required _) :: as) [] f =
  Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
processArgs flag (Optional a :: as) [] f =
  processArgs flag as [] (f Nothing)
processArgs flag (Flag a :: as) [] f =
  processArgs flag as [] (f False)
-- Happy cases
processArgs flag (Required a :: as) (x :: xs) f =
  processArgs flag as xs (f x)
processArgs flag (Optional a :: as) (x :: xs) f =
  if isPrefixOf "-" x
    then processArgs flag as (x :: xs) (f Nothing)
    else processArgs flag as xs (f $ Just x)
processArgs flag (Flag a :: as) (x :: xs) f =
  if x == "--" ++ a
    then processArgs flag as xs (f True)
    else processArgs flag as (x :: xs) (f False)
matchFlag : (d : OptDesc) -> List String ->
            Either String (Maybe (List CLOpt, List String))
matchFlag d [] = Right Nothing -- Nothing left to match
matchFlag d (x :: xs) =
  if x `elem` flags d
    then do
      args <- processArgs x (argdescs d) xs (action d)
      Right (Just args)
    else Right Nothing
findMatch : List OptDesc -> List String ->
            Either String (List CLOpt, List String)
findMatch [] [] = Right ([], [])
findMatch [] (f :: args) =
  case unpack f of
    '-' :: '-' :: _ => Left "Unknown flag \{f}"
    _ => Right ([InputFile f], args)
findMatch (d :: ds) args =
  case !(matchFlag d args) of
    Nothing => findMatch ds args
    Just res => Right res
parseOpts : List OptDesc -> List String -> Either String (List CLOpt)
parseOpts opts [] = Right []
parseOpts opts args = do
  (cl, rest) <- findMatch opts args
  cls <- assert_total (parseOpts opts rest) -- 'rest' smaller than 'args'
  pure (cl ++ cls)
export
getCmdOpts : IO (Either String (List CLOpt))
getCmdOpts = do
  (_ :: opts) <- getArgs
    | _ => pure (Left "Invalid command line")
  pure $ parseOpts options opts
export
findInputs : List CLOpt -> List String
findInputs [] = []
findInputs (InputFile f :: fs) = f :: findInputs fs
findInputs (_ :: fs) = findInputs fs
export
quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _) = do
  putStrLn versionMsg
  pure False
quitOpts (Help :: _) = do
  putStrLn usage
  pure False
quitOpts (_ :: opts) = quitOpts opts
export
subCmd : List CLOpt -> SubCmd
subCmd [] = SubCmdPkg $ MkPkgOpts {localOnly = False} -- default
subCmd (Module opts :: _) = SubCmdMod opts
subCmd (Package opts :: _) = SubCmdPkg opts
subCmd (f :: fs) = subCmd fs

[custom.all.idris2-dep-graph]
type = "local"
path = "."
ipkg = "idris2-dep-graph.ipkg"
test = "test/test.ipkg"
[custom.all.idris2-dep-graph-test]
type = "local"
path = "test"
ipkg = "test.ipkg"

package idris2-dep-graph
version = 0.1.0
authors = "Tomáš Zemanovič"
-- maintainers =
-- license =
-- brief =
-- readme =
-- homepage =
-- sourceloc =
-- bugtracker =
-- the Idris2 version required (e.g. langversion >= 0.5.1)
-- langversion
-- packages to add to search path
depends
  = idris2 >= 0.8.0
-- modules to install
modules
  = DepGraph.Data
  , DepGraph.Cli
  , Idris.Driver.Extra
  , Idris.Package.Extra
-- main file (i.e. file to load at REPL)
main = Main
-- name of executable
executable = "idris2-dep-graph"
-- opts =
sourcedir = "src"
-- builddir =
-- outputdir =
-- script to run before building
-- prebuild =
-- script to run after building
-- postbuild =
-- script to run after building, before installing
-- preinstall =
-- script to run after installing
-- postinstall =
-- script to run before cleaning
-- preclean =
-- script to run after cleaning
-- postclean =

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.43.0 (0)
 -->
<!-- Title: %3 Pages: 1 -->
<svg width="225pt" height="332pt"
 viewBox="0.00 0.00 225.08 332.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 328)">
<title>%3</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-328 221.08,-328 221.08,4 -4,4"/>
<!-- idris2&#45;dep&#45;graph -->
<g id="node1" class="node">
<title>idris2&#45;dep&#45;graph</title>
<ellipse fill="linen" stroke="black" cx="108.54" cy="-234" rx="87.99" ry="18"/>
<text text-anchor="middle" x="108.54" y="-230.3" font-family="Times,serif" font-size="14.00">idris2&#45;dep&#45;graph</text>
</g>
<!-- idris2 -->
<g id="node3" class="node">
<title>idris2</title>
<ellipse fill="none" stroke="black" cx="108.54" cy="-162" rx="37.89" ry="18"/>
<text text-anchor="middle" x="108.54" y="-158.3" font-family="Times,serif" font-size="14.00">idris2</text>
</g>
<!-- idris2&#45;dep&#45;graph&#45;&gt;idris2 -->
<g id="edge1" class="edge">
<title>idris2&#45;dep&#45;graph&#45;&gt;idris2</title>
<path fill="none" stroke="black" d="M108.54,-215.7C108.54,-207.98 108.54,-198.71 108.54,-190.11"/>
<polygon fill="black" stroke="black" points="112.04,-190.1 108.54,-180.1 105.04,-190.1 112.04,-190.1"/>
</g>
<!-- idris2&#45;dep&#45;graph&#45;test -->
<g id="node2" class="node">
<title>idris2&#45;dep&#45;graph&#45;test</title>
<ellipse fill="linen" stroke="black" cx="108.54" cy="-306" rx="108.58" ry="18"/>
<text text-anchor="middle" x="108.54" y="-302.3" font-family="Times,serif" font-size="14.00">idris2&#45;dep&#45;graph&#45;test</text>
</g>
<!-- idris2&#45;dep&#45;graph&#45;test&#45;&gt;idris2&#45;dep&#45;graph -->
<g id="edge2" class="edge">
<title>idris2&#45;dep&#45;graph&#45;test&#45;&gt;idris2&#45;dep&#45;graph</title>
<path fill="none" stroke="black" d="M108.54,-287.7C108.54,-279.98 108.54,-270.71 108.54,-262.11"/>
<polygon fill="black" stroke="black" points="112.04,-262.1 108.54,-252.1 105.04,-262.1 112.04,-262.1"/>
</g>
<!-- network -->
<g id="node5" class="node">
<title>network</title>
<ellipse fill="none" stroke="black" cx="108.54" cy="-90" rx="48.99" ry="18"/>
<text text-anchor="middle" x="108.54" y="-86.3" font-family="Times,serif" font-size="14.00">network</text>
</g>
<!-- idris2&#45;&gt;network -->
<g id="edge3" class="edge">
<title>idris2&#45;&gt;network</title>
<path fill="none" stroke="black" d="M108.54,-143.7C108.54,-135.98 108.54,-126.71 108.54,-118.11"/>
<polygon fill="black" stroke="black" points="112.04,-118.1 108.54,-108.1 105.04,-118.1 112.04,-118.1"/>
</g>
<!-- linear -->
<g id="node4" class="node">
<title>linear</title>
<ellipse fill="none" stroke="black" cx="108.54" cy="-18" rx="37.89" ry="18"/>
<text text-anchor="middle" x="108.54" y="-14.3" font-family="Times,serif" font-size="14.00">linear</text>
</g>
<!-- network&#45;&gt;linear -->
<g id="edge4" class="edge">
<title>network&#45;&gt;linear</title>
<path fill="none" stroke="black" d="M108.54,-71.7C108.54,-63.98 108.54,-54.71 108.54,-46.11"/>
<polygon fill="black" stroke="black" points="112.04,-46.1 108.54,-36.1 105.04,-46.1 112.04,-46.1"/>
</g>
</g>
</svg>

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
 "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<!-- Generated by graphviz version 2.43.0 (0)
 -->
<!-- Title: %3 Pages: 1 -->
<svg width="797pt" height="171pt"
 viewBox="0.00 0.00 797.00 171.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 167)">
<title>%3</title>
<polygon fill="white" stroke="transparent" points="-4,4 -4,-167 793,-167 793,4 -4,4"/>
<g id="clust1" class="cluster">
<title>cluster_idris2&#45;dep&#45;graph</title>
<polygon fill="linen" stroke="black" points="8,-8 8,-155 781,-155 781,-8 8,-8"/>
<text text-anchor="middle" x="394.5" y="-139.8" font-family="Times,serif" font-size="14.00">idris2&#45;dep&#45;graph</text>
</g>
<!-- DepGraph.Data -->
<g id="node1" class="node">
<title>DepGraph.Data</title>
<ellipse fill="white" stroke="black" cx="99" cy="-34" rx="83.39" ry="18"/>
<text text-anchor="middle" x="99" y="-30.3" font-family="Times,serif" font-size="14.00">DepGraph.Data</text>
</g>
<!-- DepGraph.Cli -->
<g id="node2" class="node">
<title>DepGraph.Cli</title>
<ellipse fill="white" stroke="black" cx="274" cy="-34" rx="73.39" ry="18"/>
<text text-anchor="middle" x="274" y="-30.3" font-family="Times,serif" font-size="14.00">DepGraph.Cli</text>
</g>
<!-- Idris.Package.Extra -->
<g id="node3" class="node">
<title>Idris.Package.Extra</title>
<ellipse fill="white" stroke="black" cx="467" cy="-34" rx="102.08" ry="18"/>
<text text-anchor="middle" x="467" y="-30.3" font-family="Times,serif" font-size="14.00">Idris.Package.Extra</text>
</g>
<!-- Idris.Driver.Extra -->
<g id="node4" class="node">
<title>Idris.Driver.Extra</title>
<ellipse fill="white" stroke="black" cx="680" cy="-34" rx="92.88" ry="18"/>
<text text-anchor="middle" x="680" y="-30.3" font-family="Times,serif" font-size="14.00">Idris.Driver.Extra</text>
</g>
<!-- Main -->
<g id="node5" class="node">
<title>Main</title>
<ellipse fill="white" stroke="black" cx="370" cy="-106" rx="34.39" ry="18"/>
<text text-anchor="middle" x="370" y="-102.3" font-family="Times,serif" font-size="14.00">Main</text>
</g>
<!-- Main&#45;&gt;DepGraph.Data -->
<g id="edge1" class="edge">
<title>Main&#45;&gt;DepGraph.Data</title>
<path fill="none" stroke="black" d="M335.4,-106C262.34,-106 99,-106 99,-106 99,-106 99,-62.17 99,-62.17"/>
<polygon fill="black" stroke="black" points="102.5,-62.17 99,-52.17 95.5,-62.17 102.5,-62.17"/>
</g>
<!-- Main&#45;&gt;DepGraph.Cli -->
<g id="edge2" class="edge">
<title>Main&#45;&gt;DepGraph.Cli</title>
<path fill="none" stroke="black" d="M341.5,-95.68C341.5,-95.68 341.5,-51.24 341.5,-51.24"/>
<polygon fill="black" stroke="black" points="345,-51.24 341.5,-41.24 338,-51.24 345,-51.24"/>
</g>
<!-- Main&#45;&gt;Idris.Package.Extra -->
<g id="edge3" class="edge">
<title>Main&#45;&gt;Idris.Package.Extra</title>
<path fill="none" stroke="black" d="M384.7,-89.66C384.7,-89.66 384.7,-54.69 384.7,-54.69"/>
<polygon fill="black" stroke="black" points="388.2,-54.69 384.7,-44.69 381.2,-54.69 388.2,-54.69"/>
</g>
<!-- Main&#45;&gt;Idris.Driver.Extra -->
<g id="edge4" class="edge">
<title>Main&#45;&gt;Idris.Driver.Extra</title>
<path fill="none" stroke="black" d="M404.66,-106C485.55,-106 680,-106 680,-106 680,-106 680,-62.17 680,-62.17"/>
<polygon fill="black" stroke="black" points="683.5,-62.17 680,-52.17 676.5,-62.17 683.5,-62.17"/>
</g>
</g>
</svg>

# Idris2-dep-graph
Produce graphiz (dot) graph of package dependencies or module imports of Idris2 packages.
## Usage
This app works by default with [pack](https://github.com/stefan-hoeck/idris2-pack) by looking up its package dir via `pack package-path`. Alternatively, you can use the same env vars as with Idris2 (e.g. `IDRIS2_PACKAGE_PATH`).
To use, run the tool in the directory of the package(s) of interest:
```bash
# Package dependency graph
#   Use `--local-only` to exclude non-local package
idris2-dep-graph pkg
# Module imports graph:
#   Use `--with-external` to include modules imported from other packages (non-transitive)
idris2-dep-graph mod
# Usually you'll just pipe the result to `dot` and save the result
idris2-dep-graph ... | dot -Tsvg > graph.svg
```
You can give it one or more .ipkg paths after the sub-command for a specific selection. If you don't specify any .ipkg paths, it will recursively look for all in the current dir.
## Example outputs on this package
### Package dependencies
![Package dependencies](./assets/pkg.svg)
### Module imports
![Module imports](./assets/mod.svg)

# Idris
build/

build/
*.*~
.pijul