From 457d10bbdffaefafbf49cbbf38c7162d2d1a449a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 2 Sep 2024 14:18:56 +0200 Subject: [PATCH] cleanup --- ImportGraph/Cli.lean | 12 ++++++------ ImportGraph/Gexf.lean | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index d6862f0..650e47f 100644 --- a/ImportGraph/Cli.lean +++ b/ImportGraph/Cli.lean @@ -56,16 +56,16 @@ open IO.FS IO.Process Name in /-- Implementation of the import graph command line program. -/ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do -- file extensions that should be created - let extensions : Array String := match args.variableArgsAs! String with - | #[] => #["dot"] + let extensions : HashSet String := match args.variableArgsAs! String with + | #[] => HashSet.empty.insert "dot" | outputs => outputs.foldl (fun acc (o : String) => match FilePath.extension o with - | none => if acc.contains "dot" then acc else acc.push "dot" - | some "gexf" => if acc.contains "gexf" then acc else acc.push "gexf" - | some "html" => if acc.contains "gexf" then acc else acc.push "gexf" + | none => acc.insert "dot" + | some "gexf" => acc.insert "gexf" + | some "html" => acc.insert "gexf" -- currently all other formats are handled by passing the `.dot` file to -- graphviz - | some _ => if acc.contains "dot" then acc else acc.push "dot" ) #[] + | some _ => acc.insert "dot" ) {} let to ← match args.flag? "to" with | some to => pure <| to.as! ModuleName diff --git a/ImportGraph/Gexf.lean b/ImportGraph/Gexf.lean index c6240f2..b1d6c0c 100644 --- a/ImportGraph/Gexf.lean +++ b/ImportGraph/Gexf.lean @@ -26,7 +26,7 @@ def isBlackListed (env : Environment) (declName : Name) : Bool := /-- Get number of non-blacklisted declarations per file. -/ def getNumberOfDeclsPerFile (env: Environment) : NameMap Nat := - env.const2ModIdx.fold (fun acc n idx => + env.const2ModIdx.fold (fun acc n (idx : ModuleIdx) => let mod := env.allImportedModuleNames.get! idx if isBlackListed env n then acc else acc.insert mod ((acc.findD mod 0) + 1) ) {}