feat: Add dot file creation
This commit is contained in:
jstoobysmith
parent
a62c66bc72
commit
3c790c2e38
2 changed files with 162 additions and 29 deletions
|
|
@ -44,13 +44,36 @@ def depToWebString (d : Name) : MetaM String := do
|
|||
(mod.toString.replace "." "/") ++ ".lean"
|
||||
pure s!" * [{d}]({webPath}#L{lineNo})"
|
||||
|
||||
/-- Takes a `ConstantInfo` corresponding to a `InformalLemma` and returns
|
||||
the corresponding `InformalLemma`. -/
|
||||
unsafe def constantInfoToInformalLemma (c : ConstantInfo) : MetaM InformalLemma := do
|
||||
match c with
|
||||
| ConstantInfo.defnInfo c =>
|
||||
Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
|
||||
| _ => panic! "Passed constantInfoToInformalLemma a `ConstantInfo` that is not a `InformalLemma`"
|
||||
|
||||
/-- Takes a `ConstantInfo` corresponding to a `InformalDefinition` and returns
|
||||
the corresponding `InformalDefinition`. -/
|
||||
unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : MetaM InformalDefinition := do
|
||||
match c with
|
||||
| ConstantInfo.defnInfo c =>
|
||||
Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
|
||||
| _ => panic! "Passed constantInfoToInformalDefinition a
|
||||
`ConstantInfo` that is not a `InformalDefinition`"
|
||||
|
||||
unsafe def informalDependencies (c : ConstantInfo) : MetaM (Array Name) := do
|
||||
if Informal.isInformalLemma c then
|
||||
let informal ← constantInfoToInformalLemma c
|
||||
pure informal.dependencies.toArray
|
||||
else if Informal.isInformalDef c then
|
||||
let informal ← constantInfoToInformalDefinition c
|
||||
pure informal.dependencies.toArray
|
||||
else
|
||||
pure #[]
|
||||
|
||||
unsafe def informalLemmaToString (c : Import × ConstantInfo) : MetaM String := do
|
||||
let lineNo ← getLineNumber c.2.name
|
||||
let informalLemma ←
|
||||
match c.2 with
|
||||
| ConstantInfo.defnInfo c =>
|
||||
Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
|
||||
| _ => panic! "This should not happen"
|
||||
let informalLemma ← constantInfoToInformalLemma c.2
|
||||
let dep ← informalLemma.dependencies.mapM fun d => depToString d
|
||||
pure s!"
|
||||
Informal lemma: {informalLemma.name}
|
||||
|
|
@ -63,11 +86,7 @@ Informal lemma: {informalLemma.name}
|
|||
|
||||
unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String := do
|
||||
let lineNo ← getLineNumber c.2.name
|
||||
let informalLemma ←
|
||||
match c.2 with
|
||||
| ConstantInfo.defnInfo c =>
|
||||
Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
|
||||
| _ => panic! "This should not happen"
|
||||
let informalLemma ← constantInfoToInformalLemma c.2
|
||||
let dep ← informalLemma.dependencies.mapM fun d => depToWebString d
|
||||
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
|
||||
(c.1.module.toString.replace "." "/") ++ ".lean"
|
||||
|
|
@ -81,11 +100,7 @@ unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String
|
|||
|
||||
unsafe def informalDefToString (c : Import × ConstantInfo) : MetaM String := do
|
||||
let lineNo ← getLineNumber c.2.name
|
||||
let informalDef ←
|
||||
match c.2 with
|
||||
| ConstantInfo.defnInfo c =>
|
||||
Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
|
||||
| _ => panic! "This should not happen"
|
||||
let informalDef ← constantInfoToInformalDefinition c.2
|
||||
let dep ← informalDef.dependencies.mapM fun d => depToString d
|
||||
pure s!"
|
||||
Informal def: {informalDef.name}
|
||||
|
|
@ -97,11 +112,7 @@ Informal def: {informalDef.name}
|
|||
|
||||
unsafe def informalDefToWebString (c : Import × ConstantInfo) : MetaM String := do
|
||||
let lineNo ← getLineNumber c.2.name
|
||||
let informalDef ←
|
||||
match c.2 with
|
||||
| ConstantInfo.defnInfo c =>
|
||||
Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
|
||||
| _ => panic! "This should not happen"
|
||||
let informalDef ← constantInfoToInformalDefinition c.2
|
||||
let dep ← informalDef.dependencies.mapM fun d => depToWebString d
|
||||
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
|
||||
(c.1.module.toString.replace "." "/") ++ ".lean"
|
||||
|
|
@ -141,14 +152,19 @@ There is an implicit invitation to the reader to contribute to the formalization
|
|||
|
||||
"
|
||||
|
||||
unsafe def importToString (i : Import) : MetaM String := do
|
||||
/-- Takes an import and outputs the list of `ConstantInfo` corresponding
|
||||
to an informal definition or lemma in that import, sorted by line number. -/
|
||||
def importToInformal (i : Import) : MetaM (Array (Import × ConstantInfo)) := do
|
||||
let constants ← getConst i
|
||||
let constants := constants.filter (fun c => ¬ Lean.Name.isInternalDetail c.2.name)
|
||||
let informalConst := constants.filter fun c => Informal.isInformal c.2
|
||||
let informalConstLineNo ← informalConst.mapM fun c => getLineNumber c.2.name
|
||||
let informalConstWithLineNo := informalConst.zip informalConstLineNo
|
||||
let informalConstWithLineNoSort := informalConstWithLineNo.qsort (fun a b => a.2 < b.2)
|
||||
let informalConst := informalConstWithLineNoSort.map (fun c => c.1)
|
||||
return informalConstWithLineNoSort.map (fun c => c.1)
|
||||
|
||||
unsafe def importToString (i : Import) : MetaM String := do
|
||||
let informalConst ← importToInformal i
|
||||
let informalPrint ← (informalConst.mapM informalToString).run'
|
||||
if informalPrint.isEmpty then
|
||||
pure ""
|
||||
|
|
@ -156,19 +172,99 @@ unsafe def importToString (i : Import) : MetaM String := do
|
|||
pure ("\n\n" ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList)
|
||||
|
||||
unsafe def importToWebString (i : Import) : MetaM String := do
|
||||
let constants ← getConst i
|
||||
let constants := constants.filter (fun c => ¬ Lean.Name.isInternalDetail c.2.name)
|
||||
let informalConst := constants.filter fun c => Informal.isInformal c.2
|
||||
let informalConstLineNo ← informalConst.mapM fun c => getLineNumber c.2.name
|
||||
let informalConstWithLineNo := informalConst.zip informalConstLineNo
|
||||
let informalConstWithLineNoSort := informalConstWithLineNo.qsort (fun a b => a.2 < b.2)
|
||||
let informalConst := informalConstWithLineNoSort.map (fun c => c.1)
|
||||
let informalConst ← importToInformal i
|
||||
let informalPrint ← (informalConst.mapM informalToWebString).run'
|
||||
if informalPrint.isEmpty then
|
||||
pure ""
|
||||
else
|
||||
pure ("\n\n## " ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList)
|
||||
|
||||
section dotFile
|
||||
/-!
|
||||
|
||||
## Making the dot file for dependency graph.
|
||||
|
||||
-/
|
||||
|
||||
/-- Turns a formal definition or lemma into a node of a dot graph. -/
|
||||
def formalToNode (d : Name) : MetaM String := do
|
||||
let lineNo ← getLineNumber d
|
||||
let mod ← getModule d
|
||||
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
|
||||
(mod.toString.replace "." "/") ++ ".lean"
|
||||
pure s!"\"{d}\"[label=\"{d}\", shape=box, style=filled, fillcolor=green,
|
||||
href=\"{webPath}#L{lineNo}\"]"
|
||||
|
||||
unsafe def informalLemmaToNode (c : Import × ConstantInfo) : MetaM String := do
|
||||
let lineNo ← getLineNumber c.2.name
|
||||
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
|
||||
(c.1.module.toString.replace "." "/") ++ ".lean"
|
||||
pure s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=ellipse, style=filled, fillcolor=orange,
|
||||
href=\"{webPath}#L{lineNo}\"]"
|
||||
|
||||
unsafe def informalDefToNode (c : Import × ConstantInfo) : MetaM String := do
|
||||
let lineNo ← getLineNumber c.2.name
|
||||
let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
|
||||
(c.1.module.toString.replace "." "/") ++ ".lean"
|
||||
pure s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=box, style=filled, fillcolor=orange,
|
||||
href=\"{webPath}#L{lineNo}\"]"
|
||||
|
||||
unsafe def informalToNode (c : Import × ConstantInfo) : MetaM String := do
|
||||
if Informal.isInformalLemma c.2 then
|
||||
informalLemmaToNode c
|
||||
else if Informal.isInformalDef c.2 then
|
||||
informalDefToNode c
|
||||
else
|
||||
pure ""
|
||||
|
||||
unsafe def informalLemmaToEdges (c : Import × ConstantInfo) : MetaM (String) := do
|
||||
let informalLemma ← constantInfoToInformalLemma c.2
|
||||
let deps := informalLemma.dependencies
|
||||
let edge := deps.map (fun d => s!"\"{d}\" -> \"{c.2.name}\"")
|
||||
pure (String.intercalate "\n" edge)
|
||||
|
||||
unsafe def informalDefToEdges (c : Import × ConstantInfo) : MetaM (String) := do
|
||||
let informalDef ← constantInfoToInformalDefinition c.2
|
||||
let deps := informalDef.dependencies
|
||||
let edge := deps.map (fun d => s!"\"{d}\" -> \"{c.2.name}\"")
|
||||
pure (String.intercalate "\n" edge)
|
||||
|
||||
unsafe def informalToEdges (c : Import × ConstantInfo) : MetaM (String) := do
|
||||
if Informal.isInformalLemma c.2 then
|
||||
informalLemmaToEdges c
|
||||
else if Informal.isInformalDef c.2 then
|
||||
informalDefToEdges c
|
||||
else
|
||||
pure ""
|
||||
|
||||
unsafe def mkDot (imports : Array Import) : MetaM String := do
|
||||
let informal ← imports.mapM importToInformal
|
||||
let informal := informal.flatten
|
||||
let deps ← (informal.map (fun c => c.2)).mapM informalDependencies
|
||||
let deps := deps.flatten
|
||||
let informal_name := informal.map (fun c => c.2.name)
|
||||
let formal_deps := deps.filter (fun d => d ∉ informal_name)
|
||||
let formal_nodes ← formal_deps.mapM formalToNode
|
||||
let header := "strict digraph G {
|
||||
bgcolor=\"lightyellow\";
|
||||
label=\"Informal dependency graph for HepLean\";
|
||||
labelloc=\"t\";
|
||||
labeljust=\"l\";"
|
||||
let footer := "}"
|
||||
let nodes := String.intercalate "\n" formal_nodes.toList
|
||||
let informalLemmaNodes ← informal.mapM informalToNode
|
||||
let informalNodes := String.intercalate "\n" informalLemmaNodes.toList
|
||||
let edges ← informal.mapM informalToEdges
|
||||
let edges := String.intercalate "\n" edges.toList
|
||||
pure (header ++ "\n" ++ nodes ++ "\n" ++ informalNodes ++ "\n" ++ edges ++ "\n" ++ footer)
|
||||
|
||||
end dotFile
|
||||
|
||||
/-!
|
||||
|
||||
## Main function
|
||||
|
||||
-/
|
||||
unsafe def main (args : List String) : IO UInt32 := do
|
||||
initSearchPath (← findSysroot)
|
||||
let mods : Name := `HepLean
|
||||
|
|
@ -187,4 +283,10 @@ unsafe def main (args : List String) : IO UInt32 := do
|
|||
let out := String.intercalate "\n" importWebString.toList
|
||||
IO.println (s!"Informal file made.")
|
||||
IO.FS.writeFile fileOut (informalFileHeader ++ out)
|
||||
/- Making the dot file. -/
|
||||
if "mkDot" ∈ args then
|
||||
let dot ← CoreM.withImportModules #[`HepLean] (mkDot imports).run'
|
||||
let dotFile : System.FilePath := {toString := "./docs/InformalDot.dot"}
|
||||
IO.FS.writeFile dotFile dot
|
||||
IO.println (s!"Dot file made.")
|
||||
pure 0
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue