From deb6739fcc3fabc31ba6af0bc07b4a48a28f2959 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 27 Nov 2021 16:19:45 +0100 Subject: [PATCH 01/50] chore: Initial Lake project --- .gitignore | 2 ++ lakefile.lean | 7 +++++++ lean-toolchain | 1 + 3 files changed, 10 insertions(+) create mode 100644 .gitignore create mode 100644 lakefile.lean create mode 100644 lean-toolchain diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..29035da --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +/build +/lean_packages diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..2f747bb --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package «doc-gen4» { + -- add configuration options here + supportInterpreter := true +} diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..22206e9 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2021-11-26 From 2574c22e4a2a0ed49d70109ecdaed7a4a0b7524c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 27 Nov 2021 16:19:56 +0100 Subject: [PATCH 02/50] feat: First experimentations --- DocGen4.lean | 2 + DocGen4/Load.lean | 22 +++++++++ DocGen4/Process.lean | 112 +++++++++++++++++++++++++++++++++++++++++++ Main.lean | 10 ++++ 4 files changed, 146 insertions(+) create mode 100644 DocGen4.lean create mode 100644 DocGen4/Load.lean create mode 100644 DocGen4/Process.lean create mode 100644 Main.lean diff --git a/DocGen4.lean b/DocGen4.lean new file mode 100644 index 0000000..9ce5c22 --- /dev/null +++ b/DocGen4.lean @@ -0,0 +1,2 @@ +import DocGen4.Process +import DocGen4.Load diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean new file mode 100644 index 0000000..3c9d49c --- /dev/null +++ b/DocGen4/Load.lean @@ -0,0 +1,22 @@ +import Lean +import DocGen4.Process + +namespace DocGen4 + +open Lean System + +def printSearchPath : IO PUnit := do + IO.println s!"{←searchPathRef.get}" + +def setSearchPath (path : List FilePath) : IO PUnit := do + searchPathRef.set path + +def load (imports : List Name) : IO (List DocInfo) := do + let env ← importModules (List.map (Import.mk · false) imports) Options.empty + let doc ← Prod.fst <$> (Meta.MetaM.toIO (process env) {} { env := env} {} {}) + for i in doc do + let s ← Core.CoreM.toIO i.prettyPrint {} { env := env } + IO.println s.fst + return doc + +end DocGen4 diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean new file mode 100644 index 0000000..306ecde --- /dev/null +++ b/DocGen4/Process.lean @@ -0,0 +1,112 @@ +import Lean +import Lean.Meta.Match.MatcherInfo +import Lean.PrettyPrinter + +namespace DocGen4 + +open Lean Meta PrettyPrinter + +def prettyPrintTerm (expr : Expr) : MetaM Syntax := + delab Name.anonymous [] expr + +structure Info where + name : Name + type : Syntax + doc : Option String + module : Name + deriving Repr + +def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do + let env ← getEnv + let type := (←prettyPrintTerm v.type ) + let doc := findDocString? env v.name + match (env.getModuleIdxFor? v.name) with + | some modidx => + let module := env.allImportedModuleNames.get! modidx + return Info.mk v.name type doc module + | none => panic! "impossible" + +structure AxiomInfo extends Info where + isUnsafe : Bool + deriving Repr + +def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do + let info ← Info.ofConstantVal v.toConstantVal + return AxiomInfo.mk info v.isUnsafe + +structure TheoremInfo extends Info where + deriving Repr + +def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do + let info ← Info.ofConstantVal v.toConstantVal + return TheoremInfo.mk info + +structure OpaqueInfo extends Info where + value : Syntax + isUnsafe : Bool + deriving Repr + +def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do + let info ← Info.ofConstantVal v.toConstantVal + let value ← prettyPrintTerm v.value + return OpaqueInfo.mk info value v.isUnsafe + +inductive DocInfo where +| axiomInfo (info : AxiomInfo) : DocInfo +| theoremInfo (info : TheoremInfo) : DocInfo +| opaqueInfo (info : OpaqueInfo) : DocInfo +| definitionInfo : DocInfo +| mutualInductiveInfo : DocInfo +| inductiveInfo : DocInfo +| structureInfo : DocInfo +| classInfo : DocInfo +| classInductiveInfo : DocInfo +deriving Repr + +namespace DocInfo + +private def isBlackListed (declName : Name) : MetaM Bool := do + let env ← getEnv + (declName.isInternal && !isPrivateName declName) + <||> isAuxRecursor env declName + <||> isNoConfusion env declName + <||> isRec declName + <||> isMatcher declName + +-- TODO: Figure out how to associate names etc. with where they actually came from module wise +def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do + if (←isBlackListed name) then + return none + match info with + | ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i) + | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i) + | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i) + -- TODO: Find a way to extract equations nicely + | ConstantInfo.defnInfo i => none + -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) + | ConstantInfo.inductInfo i => none + -- we ignore these for now + | ConstantInfo.ctorInfo i => none + | ConstantInfo.recInfo i => none + | ConstantInfo.quotInfo i => none + + +def prettyPrint (i : DocInfo) : CoreM String := do + match i with + | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type} from {i.module}, doc string: {i.doc}" + | theoremInfo i => s!"theorem {i.name} : {←PrettyPrinter.formatTerm i.type} from {i.module}, doc string: {i.doc}" + | opaqueInfo i => s!"constant {i.name} : {←PrettyPrinter.formatTerm i.type} from {i.module}, doc string: {i.doc}" + | _ => "" + +end DocInfo + +def process : Environment → MetaM (List DocInfo) := λ env => do + let mut res := [] + for cinfo in env.constants.toList do + let dinfo := ←DocInfo.ofConstant cinfo + match dinfo with + | some d => res := d :: res + | none => () + return res + +end DocGen4 diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..44a838d --- /dev/null +++ b/Main.lean @@ -0,0 +1,10 @@ +import DocGen4 +import Lean + +open DocGen4 Lean + +def main : IO Unit := do + -- This should be set by lake at some point + setSearchPath ["/home/nix/Desktop/formal_verification/lean/mathlib4/build/lib", "/home/nix/.elan/toolchains/leanprover--lean4---nightly-2021-11-24/lib/lean"] + let doc ← load [`Mathlib] + return () From dd0cebb44a1694caa719808a101b22cd16a60cc6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 28 Nov 2021 21:31:22 +0100 Subject: [PATCH 03/50] feat: Sort everything into modules instead of just declaration lists --- DocGen4/Load.lean | 11 ++--- DocGen4/Process.lean | 99 ++++++++++++++++++++++++++++---------------- 2 files changed, 69 insertions(+), 41 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 3c9d49c..9c27f8f 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -1,9 +1,10 @@ import Lean import DocGen4.Process +import Std.Data.HashMap namespace DocGen4 -open Lean System +open Lean System Std def printSearchPath : IO PUnit := do IO.println s!"{←searchPathRef.get}" @@ -11,11 +12,11 @@ def printSearchPath : IO PUnit := do def setSearchPath (path : List FilePath) : IO PUnit := do searchPathRef.set path -def load (imports : List Name) : IO (List DocInfo) := do +def load (imports : List Name) : IO (HashMap Name Module) := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty - let doc ← Prod.fst <$> (Meta.MetaM.toIO (process env) {} { env := env} {} {}) - for i in doc do - let s ← Core.CoreM.toIO i.prettyPrint {} { env := env } + let doc ← Prod.fst <$> (Meta.MetaM.toIO (process) {} { env := env} {} {}) + for (_, module) in doc.toList do + let s ← Core.CoreM.toIO module.prettyPrint {} { env := env } IO.println s.fst return doc diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 306ecde..1b00f22 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -1,56 +1,30 @@ import Lean import Lean.Meta.Match.MatcherInfo import Lean.PrettyPrinter +import Std.Data.HashMap namespace DocGen4 -open Lean Meta PrettyPrinter - -def prettyPrintTerm (expr : Expr) : MetaM Syntax := - delab Name.anonymous [] expr +open Lean Meta PrettyPrinter Std structure Info where name : Name type : Syntax doc : Option String - module : Name deriving Repr -def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do - let env ← getEnv - let type := (←prettyPrintTerm v.type ) - let doc := findDocString? env v.name - match (env.getModuleIdxFor? v.name) with - | some modidx => - let module := env.allImportedModuleNames.get! modidx - return Info.mk v.name type doc module - | none => panic! "impossible" - structure AxiomInfo extends Info where isUnsafe : Bool deriving Repr -def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do - let info ← Info.ofConstantVal v.toConstantVal - return AxiomInfo.mk info v.isUnsafe - structure TheoremInfo extends Info where deriving Repr -def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do - let info ← Info.ofConstantVal v.toConstantVal - return TheoremInfo.mk info - structure OpaqueInfo extends Info where value : Syntax isUnsafe : Bool deriving Repr -def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do - let info ← Info.ofConstantVal v.toConstantVal - let value ← prettyPrintTerm v.value - return OpaqueInfo.mk info value v.isUnsafe - inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo | theoremInfo (info : TheoremInfo) : DocInfo @@ -63,6 +37,34 @@ inductive DocInfo where | classInductiveInfo : DocInfo deriving Repr +structure Module where + name : Name + doc : Option String + members : Array DocInfo + deriving Inhabited, Repr + +def prettyPrintTerm (expr : Expr) : MetaM Syntax := + delab Name.anonymous [] expr + +def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do + let env ← getEnv + let type := (←prettyPrintTerm v.type ) + let doc := findDocString? env v.name + return Info.mk v.name type doc + +def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do + let info ← Info.ofConstantVal v.toConstantVal + return AxiomInfo.mk info v.isUnsafe + +def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do + let info ← Info.ofConstantVal v.toConstantVal + return TheoremInfo.mk info + +def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do + let info ← Info.ofConstantVal v.toConstantVal + let value ← prettyPrintTerm v.value + return OpaqueInfo.mk info value v.isUnsafe + namespace DocInfo private def isBlackListed (declName : Name) : MetaM Bool := do @@ -93,19 +95,44 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, def prettyPrint (i : DocInfo) : CoreM String := do match i with - | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type} from {i.module}, doc string: {i.doc}" - | theoremInfo i => s!"theorem {i.name} : {←PrettyPrinter.formatTerm i.type} from {i.module}, doc string: {i.doc}" - | opaqueInfo i => s!"constant {i.name} : {←PrettyPrinter.formatTerm i.type} from {i.module}, doc string: {i.doc}" + | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" + | theoremInfo i => s!"theorem {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" + | opaqueInfo i => s!"constant {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | _ => "" end DocInfo -def process : Environment → MetaM (List DocInfo) := λ env => do - let mut res := [] +namespace Module + +def prettyPrint (m : Module) : CoreM String := do + let pretty := s!"Module {m.name}, doc string: {m.doc} with members:\n" + Array.foldlM (λ p mem => return p ++ " " ++ (←mem.prettyPrint) ++ "\n") pretty m.members + +end Module + +def process : MetaM (HashMap Name Module) := do + let env ← getEnv + let mut res := mkHashMap env.header.moduleNames.size + for module in env.header.moduleNames do + -- TODO: Check why modules can have multiple doc strings and add that later on + let moduleDoc := match getModuleDoc? env module with + | none => none + | some #[] => none + | some doc => doc.get! 0 + + res := res.insert module (Module.mk module moduleDoc #[]) + for cinfo in env.constants.toList do - let dinfo := ←DocInfo.ofConstant cinfo - match dinfo with - | some d => res := d :: res + let d := ←DocInfo.ofConstant cinfo + match d with + | some dinfo => + match (env.getModuleIdxFor? cinfo.fst) with + | some modidx => + -- TODO: Check whether this is still efficient + let moduleName := env.allImportedModuleNames.get! modidx + let module := res.find! moduleName + res := res.insert moduleName {module with members := module.members.push dinfo} + | none => panic! "impossible" | none => () return res From 54d7f92f2bc8a5ade6d204500dcb86840197e298 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 28 Nov 2021 21:39:55 +0100 Subject: [PATCH 04/50] feat: Count declarations that were processed --- Main.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Main.lean b/Main.lean index 44a838d..8a6c700 100644 --- a/Main.lean +++ b/Main.lean @@ -7,4 +7,5 @@ def main : IO Unit := do -- This should be set by lake at some point setSearchPath ["/home/nix/Desktop/formal_verification/lean/mathlib4/build/lib", "/home/nix/.elan/toolchains/leanprover--lean4---nightly-2021-11-24/lib/lean"] let doc ← load [`Mathlib] + IO.println s!"Processed {doc.size} declarations" return () From d2fddd7cff68994f790bfefa368cae8c34c38f0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 1 Dec 2021 18:25:11 +0100 Subject: [PATCH 05/50] feat: Print count of declarations and modules processed --- DocGen4/Load.lean | 5 ++++- Main.lean | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 9c27f8f..2df73fd 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -14,10 +14,13 @@ def setSearchPath (path : List FilePath) : IO PUnit := do def load (imports : List Name) : IO (HashMap Name Module) := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty - let doc ← Prod.fst <$> (Meta.MetaM.toIO (process) {} { env := env} {} {}) + -- TODO parameterize maxHeartbeats + let doc ← Prod.fst <$> (Meta.MetaM.toIO (process) { maxHeartbeats := 100000000} { env := env} {} {}) for (_, module) in doc.toList do let s ← Core.CoreM.toIO module.prettyPrint {} { env := env } IO.println s.fst + IO.println s!"Processed {List.foldl (λ a (_, b) => a + b.members.size) 0 doc.toList} declarations" + IO.println s!"Processed {doc.size} modules" return doc end DocGen4 diff --git a/Main.lean b/Main.lean index 8a6c700..639455f 100644 --- a/Main.lean +++ b/Main.lean @@ -3,9 +3,9 @@ import Lean open DocGen4 Lean + def main : IO Unit := do -- This should be set by lake at some point setSearchPath ["/home/nix/Desktop/formal_verification/lean/mathlib4/build/lib", "/home/nix/.elan/toolchains/leanprover--lean4---nightly-2021-11-24/lib/lean"] let doc ← load [`Mathlib] - IO.println s!"Processed {doc.size} declarations" return () From 21bcc3d0bc4c20872c3e178b50ca8f3726a6bfb6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 1 Dec 2021 18:25:22 +0100 Subject: [PATCH 06/50] feat: Print definitions and inductives --- DocGen4/Process.lean | 58 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 49 insertions(+), 9 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 1b00f22..c77c97f 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -25,30 +25,44 @@ structure OpaqueInfo extends Info where isUnsafe : Bool deriving Repr +structure DefinitionInfo extends Info where + --value : Syntax + unsafeInformation : DefinitionSafety + hints : ReducibilityHints + +structure InductiveInfo extends Info where + numParams : Nat -- Number of parameters + numIndices : Nat -- Number of indices + all : List Name -- List of all (including this one) inductive datatypes in the mutual declaration containing this one + ctors : List (Name × Syntax) -- List of all constructors and their type for this inductive datatype + isRec : Bool -- `true` Iff it is recursive + isUnsafe : Bool + isReflexive : Bool + isNested : Bool + deriving Repr + inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo | theoremInfo (info : TheoremInfo) : DocInfo | opaqueInfo (info : OpaqueInfo) : DocInfo -| definitionInfo : DocInfo -| mutualInductiveInfo : DocInfo -| inductiveInfo : DocInfo +| definitionInfo (info : DefinitionInfo) : DocInfo +| inductiveInfo (info : InductiveInfo) : DocInfo | structureInfo : DocInfo | classInfo : DocInfo | classInductiveInfo : DocInfo -deriving Repr structure Module where name : Name doc : Option String members : Array DocInfo - deriving Inhabited, Repr + deriving Inhabited def prettyPrintTerm (expr : Expr) : MetaM Syntax := delab Name.anonymous [] expr def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv - let type := (←prettyPrintTerm v.type ) + let type := (←prettyPrintTerm v.type) let doc := findDocString? env v.name return Info.mk v.name type doc @@ -65,16 +79,35 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do let value ← prettyPrintTerm v.value return OpaqueInfo.mk info value v.isUnsafe +def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do + let info ← Info.ofConstantVal v.toConstantVal + -- Elaborating the value yields weird exceptions + --let value ← prettyPrintTerm v.value + return DefinitionInfo.mk info v.safety v.hints + +def getConstructorType (ctor : Name) : MetaM Syntax := do + let env ← getEnv + match env.find? ctor with + | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type + | _ => panic! s!"Constructor {ctor} was requested but does not exist" + +def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do + let info ← Info.ofConstantVal v.toConstantVal + let env ← getEnv + let ctors ← List.mapM (λ name => do (name, ←getConstructorType name)) v.ctors + return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested + namespace DocInfo private def isBlackListed (declName : Name) : MetaM Bool := do let env ← getEnv - (declName.isInternal && !isPrivateName declName) + declName.isInternal <||> isAuxRecursor env declName <||> isNoConfusion env declName <||> isRec declName <||> isMatcher declName + -- TODO: Figure out how to associate names etc. with where they actually came from module wise def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do if (←isBlackListed name) then @@ -84,9 +117,12 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i) | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i) -- TODO: Find a way to extract equations nicely - | ConstantInfo.defnInfo i => none + -- TODO: Instances are definitions as well (for example coeTrans), figure out: + -- - how we can know whether they are instances + -- - how we can access unnamed instances (they probably have internal names?, change the blacklist?) + | ConstantInfo.defnInfo i => some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i) -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) - | ConstantInfo.inductInfo i => none + | ConstantInfo.inductInfo i => some $ inductiveInfo (←InductiveInfo.ofInductiveVal i) -- we ignore these for now | ConstantInfo.ctorInfo i => none | ConstantInfo.recInfo i => none @@ -98,6 +134,10 @@ def prettyPrint (i : DocInfo) : CoreM String := do | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | theoremInfo i => s!"theorem {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | opaqueInfo i => s!"constant {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" + | definitionInfo i => s!"def {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" + | inductiveInfo i => + let ctorString ← i.ctors.mapM (λ (name, type) => do s!"{name} : {←PrettyPrinter.formatTerm type}") + s!"inductive {i.name} : {←PrettyPrinter.formatTerm i.type}, ctors: {ctorString}, doc string: {i.doc}" | _ => "" end DocInfo From 006b92deaa1ce89cce115782b7728ba1fa4b4865 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 2 Dec 2021 10:34:20 +0100 Subject: [PATCH 07/50] feat: Rudamentary structure support --- DocGen4/Process.lean | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index c77c97f..fd42109 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -41,13 +41,19 @@ structure InductiveInfo extends Info where isNested : Bool deriving Repr +structure StructureInfo extends Info where + fieldInfo : Array StructureFieldInfo + parents : Array Name + ctor : (Name × Syntax) + deriving Repr + inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo | theoremInfo (info : TheoremInfo) : DocInfo | opaqueInfo (info : OpaqueInfo) : DocInfo | definitionInfo (info : DefinitionInfo) : DocInfo | inductiveInfo (info : InductiveInfo) : DocInfo -| structureInfo : DocInfo +| structureInfo (info : StructureInfo) : DocInfo | classInfo : DocInfo | classInductiveInfo : DocInfo @@ -97,9 +103,19 @@ def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do let ctors ← List.mapM (λ name => do (name, ←getConstructorType name)) v.ctors return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested +def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do + let info ← Info.ofConstantVal v.toConstantVal + let env ← getEnv + let parents := getParentStructures env v.name + let ctor := getStructureCtor env v.name |>.name + let ctorType ← getConstructorType ctor + match getStructureInfo? env v.name with + | some i => return StructureInfo.mk info i.fieldInfo parents (ctor, ctorType) + | none => panic! s!"{v.name} is not a structure" + namespace DocInfo -private def isBlackListed (declName : Name) : MetaM Bool := do +def isBlackListed (declName : Name) : MetaM Bool := do let env ← getEnv declName.isInternal <||> isAuxRecursor env declName @@ -122,7 +138,11 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, -- - how we can access unnamed instances (they probably have internal names?, change the blacklist?) | ConstantInfo.defnInfo i => some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i) -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) - | ConstantInfo.inductInfo i => some $ inductiveInfo (←InductiveInfo.ofInductiveVal i) + | ConstantInfo.inductInfo i => + if isStructure (←getEnv) i.name then + some $ structureInfo (←StructureInfo.ofInductiveVal i) + else + some $ inductiveInfo (←InductiveInfo.ofInductiveVal i) -- we ignore these for now | ConstantInfo.ctorInfo i => none | ConstantInfo.recInfo i => none @@ -138,6 +158,9 @@ def prettyPrint (i : DocInfo) : CoreM String := do | inductiveInfo i => let ctorString ← i.ctors.mapM (λ (name, type) => do s!"{name} : {←PrettyPrinter.formatTerm type}") s!"inductive {i.name} : {←PrettyPrinter.formatTerm i.type}, ctors: {ctorString}, doc string: {i.doc}" + | structureInfo i => + let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" + s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}" | _ => "" end DocInfo From 989e7bce2b43357793ca3a6523b8aaed00647978 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 2 Dec 2021 11:09:54 +0100 Subject: [PATCH 08/50] feat: Filter projection functions from defs --- DocGen4/Process.lean | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index fd42109..5e374f3 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -42,6 +42,7 @@ structure InductiveInfo extends Info where deriving Repr structure StructureInfo extends Info where + -- TODO: Later on we probably also want the type of projection fns etc. fieldInfo : Array StructureFieldInfo parents : Array Name ctor : (Name × Syntax) @@ -123,8 +124,22 @@ def isBlackListed (declName : Name) : MetaM Bool := do <||> isRec declName <||> isMatcher declName +-- TODO: Is this actually the best way? +def isProjFn (declName : Name) : MetaM Bool := do + let env ← getEnv + match declName with + | Name.str parent name _ => + if isStructure env parent then + match getStructureInfo? env parent with + | some i => + match i.fieldNames.find? (· == name) with + | some _ => true + | none => false + | none => panic! s!"{parent} is not a structure" + else + false + | _ => false --- TODO: Figure out how to associate names etc. with where they actually came from module wise def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do if (←isBlackListed name) then return none @@ -136,7 +151,12 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, -- TODO: Instances are definitions as well (for example coeTrans), figure out: -- - how we can know whether they are instances -- - how we can access unnamed instances (they probably have internal names?, change the blacklist?) - | ConstantInfo.defnInfo i => some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i) + -- TODO: Filter out projection fns + | ConstantInfo.defnInfo i => + if (←isProjFn i.name) then + none + else + some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i) -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) | ConstantInfo.inductInfo i => if isStructure (←getEnv) i.name then From a6979dd3d45273f72e36e8f8acb5d0dc7dd37385 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 2 Dec 2021 11:17:46 +0100 Subject: [PATCH 09/50] feat: Rudamentary class support --- DocGen4/Process.lean | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 5e374f3..06e2a9d 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -48,6 +48,9 @@ structure StructureInfo extends Info where ctor : (Name × Syntax) deriving Repr +structure ClassInfo extends StructureInfo where + hasOutParam : Bool + inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo | theoremInfo (info : TheoremInfo) : DocInfo @@ -55,7 +58,7 @@ inductive DocInfo where | definitionInfo (info : DefinitionInfo) : DocInfo | inductiveInfo (info : InductiveInfo) : DocInfo | structureInfo (info : StructureInfo) : DocInfo -| classInfo : DocInfo +| classInfo (info : ClassInfo) : DocInfo | classInductiveInfo : DocInfo structure Module where @@ -114,6 +117,10 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do | some i => return StructureInfo.mk info i.fieldInfo parents (ctor, ctorType) | none => panic! s!"{v.name} is not a structure" +def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do + let sinfo ← StructureInfo.ofInductiveVal v + return ClassInfo.mk sinfo $ hasOutParams (←getEnv) v.name + namespace DocInfo def isBlackListed (declName : Name) : MetaM Bool := do @@ -159,8 +166,12 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i) -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) | ConstantInfo.inductInfo i => - if isStructure (←getEnv) i.name then - some $ structureInfo (←StructureInfo.ofInductiveVal i) + let env ← getEnv + if isStructure env i.name then + if isClass env i.name then + some $ classInfo (←ClassInfo.ofInductiveVal i) + else + some $ structureInfo (←StructureInfo.ofInductiveVal i) else some $ inductiveInfo (←InductiveInfo.ofInductiveVal i) -- we ignore these for now @@ -181,6 +192,9 @@ def prettyPrint (i : DocInfo) : CoreM String := do | structureInfo i => let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}" + | classInfo i => + let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" + s!"class {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}" | _ => "" end DocInfo From 8c30f2954213983d3594acdce9d5d0fc4da5f4cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 3 Dec 2021 20:37:25 +0100 Subject: [PATCH 10/50] feat: Instance support --- DocGen4/Process.lean | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 06e2a9d..4c72fdf 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -1,7 +1,8 @@ import Lean -import Lean.Meta.Match.MatcherInfo import Lean.PrettyPrinter import Std.Data.HashMap +import Lean.Meta.SynthInstance + namespace DocGen4 @@ -30,6 +31,8 @@ structure DefinitionInfo extends Info where unsafeInformation : DefinitionSafety hints : ReducibilityHints +abbrev InstanceInfo := DefinitionInfo + structure InductiveInfo extends Info where numParams : Nat -- Number of parameters numIndices : Nat -- Number of indices @@ -50,12 +53,14 @@ structure StructureInfo extends Info where structure ClassInfo extends StructureInfo where hasOutParam : Bool + instances : Array Syntax inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo | theoremInfo (info : TheoremInfo) : DocInfo | opaqueInfo (info : OpaqueInfo) : DocInfo | definitionInfo (info : DefinitionInfo) : DocInfo +| instanceInfo (info : InstanceInfo) : DocInfo | inductiveInfo (info : InductiveInfo) : DocInfo | structureInfo (info : StructureInfo) : DocInfo | classInfo (info : ClassInfo) : DocInfo @@ -72,7 +77,7 @@ def prettyPrintTerm (expr : Expr) : MetaM Syntax := def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv - let type := (←prettyPrintTerm v.type) + let type ← prettyPrintTerm v.type let doc := findDocString? env v.name return Info.mk v.name type doc @@ -89,6 +94,9 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do let value ← prettyPrintTerm v.value return OpaqueInfo.mk info value v.isUnsafe +def isInstance (declName : Name) : MetaM Bool := do + (instanceExtension.getState (←getEnv)).instanceNames.contains declName + def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do let info ← Info.ofConstantVal v.toConstantVal -- Elaborating the value yields weird exceptions @@ -104,7 +112,7 @@ def getConstructorType (ctor : Name) : MetaM Syntax := do def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv - let ctors ← List.mapM (λ name => do (name, ←getConstructorType name)) v.ctors + let ctors ← v.ctors.mapM (λ name => do (name, ←getConstructorType name)) return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do @@ -119,7 +127,11 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do let sinfo ← StructureInfo.ofInductiveVal v - return ClassInfo.mk sinfo $ hasOutParams (←getEnv) v.name + let fn ← mkConstWithFreshMVarLevels v.name + let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn) + let insts ← SynthInstance.getInstances (mkAppN fn xs) + let insts_stx ← insts.mapM prettyPrintTerm + return ClassInfo.mk sinfo (hasOutParams (←getEnv) v.name) insts_stx namespace DocInfo @@ -157,13 +169,15 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, -- TODO: Find a way to extract equations nicely -- TODO: Instances are definitions as well (for example coeTrans), figure out: -- - how we can know whether they are instances - -- - how we can access unnamed instances (they probably have internal names?, change the blacklist?) - -- TODO: Filter out projection fns | ConstantInfo.defnInfo i => - if (←isProjFn i.name) then + if ← (isProjFn i.name) then none else - some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i) + let info ← DefinitionInfo.ofDefinitionVal i + if (←isInstance i.name) then + some $ instanceInfo info + else + some $ definitionInfo info -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) | ConstantInfo.inductInfo i => let env ← getEnv @@ -186,6 +200,7 @@ def prettyPrint (i : DocInfo) : CoreM String := do | theoremInfo i => s!"theorem {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | opaqueInfo i => s!"constant {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | definitionInfo i => s!"def {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" + | instanceInfo i => s!"instance {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | inductiveInfo i => let ctorString ← i.ctors.mapM (λ (name, type) => do s!"{name} : {←PrettyPrinter.formatTerm type}") s!"inductive {i.name} : {←PrettyPrinter.formatTerm i.type}, ctors: {ctorString}, doc string: {i.doc}" @@ -193,8 +208,8 @@ def prettyPrint (i : DocInfo) : CoreM String := do let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}" | classInfo i => - let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" - s!"class {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}" + let instanceString ← i.instances.mapM (λ i => do s!"{←PrettyPrinter.formatTerm i}") + s!"class {i.name} : {←PrettyPrinter.formatTerm i.type}, instances : {instanceString}, doc string: {i.doc}" | _ => "" end DocInfo From ac8d9e254e4639bb03891232ddbe5d47ae8163cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Dec 2021 22:31:10 +0100 Subject: [PATCH 11/50] feat: parenthesize in the pretty printer --- DocGen4/Process.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 4c72fdf..9e5924e 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -72,8 +72,9 @@ structure Module where members : Array DocInfo deriving Inhabited -def prettyPrintTerm (expr : Expr) : MetaM Syntax := - delab Name.anonymous [] expr +def prettyPrintTerm (expr : Expr) : MetaM Syntax := do + let term ← delab Name.anonymous [] expr + parenthesizeTerm term def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv From b8cf967b841d54b0efdb03d28b0f2d4512389c24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Dec 2021 22:32:34 +0100 Subject: [PATCH 12/50] chore: Focus on basic declarations for now --- DocGen4/Process.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 9e5924e..0aefa85 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -64,7 +64,6 @@ inductive DocInfo where | inductiveInfo (info : InductiveInfo) : DocInfo | structureInfo (info : StructureInfo) : DocInfo | classInfo (info : ClassInfo) : DocInfo -| classInductiveInfo : DocInfo structure Module where name : Name From 82c78d29bd8cd486850676a6f3566e98ee3e68a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Dec 2021 22:33:00 +0100 Subject: [PATCH 13/50] feat: rudimentary structure field support --- DocGen4/Process.lean | 33 +++++++++++++++++++++++++++------ 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 0aefa85..7dfd9c2 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -3,7 +3,6 @@ import Lean.PrettyPrinter import Std.Data.HashMap import Lean.Meta.SynthInstance - namespace DocGen4 open Lean Meta PrettyPrinter Std @@ -44,9 +43,13 @@ structure InductiveInfo extends Info where isNested : Bool deriving Repr +structure FieldInfo extends StructureFieldInfo where + type : Syntax + deriving Repr + structure StructureInfo extends Info where -- TODO: Later on we probably also want the type of projection fns etc. - fieldInfo : Array StructureFieldInfo + fieldInfo : Array FieldInfo parents : Array Name ctor : (Name × Syntax) deriving Repr @@ -115,6 +118,19 @@ def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do let ctors ← v.ctors.mapM (λ name => do (name, ←getConstructorType name)) return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested +def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) := + match type with + | Expr.forallE `self _ b .. => (b, (`self :: vars)) + | Expr.forallE n _ b .. => getFieldTypeAux b (n :: vars) + | _ => (type, vars) + +-- TODO: Fill universes +def getFieldType (projFn : Name) : MetaM Expr := do + let fn ← mkConstWithFreshMVarLevels projFn + let type ← inferType fn + let (type, vars) := getFieldTypeAux type [] + type.instantiate $ vars.toArray.map mkConst + def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv @@ -122,7 +138,11 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let ctor := getStructureCtor env v.name |>.name let ctorType ← getConstructorType ctor match getStructureInfo? env v.name with - | some i => return StructureInfo.mk info i.fieldInfo parents (ctor, ctorType) + | some i => + let fieldInfo ← i.fieldInfo.mapM (λ info => do + let type ← getFieldType info.projFn + FieldInfo.mk info (←prettyPrintTerm type)) + return StructureInfo.mk info fieldInfo parents (ctor, ctorType) | none => panic! s!"{v.name} is not a structure" def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do @@ -206,11 +226,12 @@ def prettyPrint (i : DocInfo) : CoreM String := do s!"inductive {i.name} : {←PrettyPrinter.formatTerm i.type}, ctors: {ctorString}, doc string: {i.doc}" | structureInfo i => let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" - s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}" + let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.fieldName} : {←PrettyPrinter.formatTerm f.type}") + s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" | classInfo i => let instanceString ← i.instances.mapM (λ i => do s!"{←PrettyPrinter.formatTerm i}") - s!"class {i.name} : {←PrettyPrinter.formatTerm i.type}, instances : {instanceString}, doc string: {i.doc}" - | _ => "" + let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.fieldName} : {←PrettyPrinter.formatTerm f.type}") + s!"class {i.name} : {←PrettyPrinter.formatTerm i.type}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" end DocInfo From b60eca730f1e24294360845d9cd762278f0783bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Dec 2021 23:33:21 +0100 Subject: [PATCH 14/50] chore: Fill universe MVars and remove out of date TODOs --- DocGen4/Process.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 7dfd9c2..3189af3 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -48,7 +48,6 @@ structure FieldInfo extends StructureFieldInfo where deriving Repr structure StructureInfo extends Info where - -- TODO: Later on we probably also want the type of projection fns etc. fieldInfo : Array FieldInfo parents : Array Name ctor : (Name × Syntax) @@ -75,6 +74,7 @@ structure Module where deriving Inhabited def prettyPrintTerm (expr : Expr) : MetaM Syntax := do + let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr) let term ← delab Name.anonymous [] expr parenthesizeTerm term @@ -124,7 +124,6 @@ def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) := | Expr.forallE n _ b .. => getFieldTypeAux b (n :: vars) | _ => (type, vars) --- TODO: Fill universes def getFieldType (projFn : Name) : MetaM Expr := do let fn ← mkConstWithFreshMVarLevels projFn let type ← inferType fn @@ -187,8 +186,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i) | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i) -- TODO: Find a way to extract equations nicely - -- TODO: Instances are definitions as well (for example coeTrans), figure out: - -- - how we can know whether they are instances | ConstantInfo.defnInfo i => if ← (isProjFn i.name) then none @@ -213,7 +210,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, | ConstantInfo.recInfo i => none | ConstantInfo.quotInfo i => none - def prettyPrint (i : DocInfo) : CoreM String := do match i with | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" From 821d57fd1c641959dbb01d8af47825c43933f0de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Dec 2021 23:40:59 +0100 Subject: [PATCH 15/50] feat: Also print parents in structures and classes --- DocGen4/Process.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 3189af3..fe6a6c0 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -223,11 +223,11 @@ def prettyPrint (i : DocInfo) : CoreM String := do | structureInfo i => let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.fieldName} : {←PrettyPrinter.formatTerm f.type}") - s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" + s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" | classInfo i => let instanceString ← i.instances.mapM (λ i => do s!"{←PrettyPrinter.formatTerm i}") let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.fieldName} : {←PrettyPrinter.formatTerm f.type}") - s!"class {i.name} : {←PrettyPrinter.formatTerm i.type}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" + s!"class {i.name} : {←PrettyPrinter.formatTerm i.type} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" end DocInfo From 4d8aa10ecb81afd6834ed7b251b642f991294ca3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 5 Dec 2021 02:54:38 +0100 Subject: [PATCH 16/50] chore: Little refactoring for Name x Syntax tuples --- DocGen4/Process.lean | 62 ++++++++++++++++++++++++++------------------ 1 file changed, 37 insertions(+), 25 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index fe6a6c0..e7f6d1c 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -7,9 +7,15 @@ namespace DocGen4 open Lean Meta PrettyPrinter Std -structure Info where - name : Name +structure NameInfo where + name : Name type : Syntax + deriving Repr + +def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do + s!"{i.name} : {←PrettyPrinter.formatTerm i.type}" + +structure Info extends NameInfo where doc : Option String deriving Repr @@ -36,26 +42,28 @@ structure InductiveInfo extends Info where numParams : Nat -- Number of parameters numIndices : Nat -- Number of indices all : List Name -- List of all (including this one) inductive datatypes in the mutual declaration containing this one - ctors : List (Name × Syntax) -- List of all constructors and their type for this inductive datatype + ctors : List NameInfo -- List of all constructors and their type for this inductive datatype isRec : Bool -- `true` Iff it is recursive isUnsafe : Bool isReflexive : Bool isNested : Bool deriving Repr -structure FieldInfo extends StructureFieldInfo where - type : Syntax +structure FieldInfo extends NameInfo where + projFn : Name + subobject? : Option Name deriving Repr structure StructureInfo extends Info where fieldInfo : Array FieldInfo parents : Array Name - ctor : (Name × Syntax) + ctor : NameInfo deriving Repr structure ClassInfo extends StructureInfo where hasOutParam : Bool instances : Array Syntax + deriving Repr inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo @@ -82,7 +90,7 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv let type ← prettyPrintTerm v.type let doc := findDocString? env v.name - return Info.mk v.name type doc + return Info.mk ⟨v.name, type⟩ doc def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do let info ← Info.ofConstantVal v.toConstantVal @@ -112,10 +120,11 @@ def getConstructorType (ctor : Name) : MetaM Syntax := do | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type | _ => panic! s!"Constructor {ctor} was requested but does not exist" +-- TODO: Obtain parameters that come after the inductive Name def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv - let ctors ← v.ctors.mapM (λ name => do (name, ←getConstructorType name)) + let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name)) return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) := @@ -130,6 +139,11 @@ def getFieldType (projFn : Name) : MetaM Expr := do let (type, vars) := getFieldTypeAux type [] type.instantiate $ vars.toArray.map mkConst +def FieldInfo.ofStructureFieldInfo (i : StructureFieldInfo) : MetaM FieldInfo := do + let type ← getFieldType i.projFn + let ni := NameInfo.mk i.fieldName (←prettyPrintTerm type) + FieldInfo.mk ni i.projFn i.subobject? + def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv @@ -138,10 +152,8 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let ctorType ← getConstructorType ctor match getStructureInfo? env v.name with | some i => - let fieldInfo ← i.fieldInfo.mapM (λ info => do - let type ← getFieldType info.projFn - FieldInfo.mk info (←prettyPrintTerm type)) - return StructureInfo.mk info fieldInfo parents (ctor, ctorType) + let fieldInfos ← i.fieldInfo.mapM FieldInfo.ofStructureFieldInfo + return StructureInfo.mk info fieldInfos parents ⟨ctor, ctorType⟩ | none => panic! s!"{v.name} is not a structure" def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do @@ -212,22 +224,22 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, def prettyPrint (i : DocInfo) : CoreM String := do match i with - | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" - | theoremInfo i => s!"theorem {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" - | opaqueInfo i => s!"constant {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" - | definitionInfo i => s!"def {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" - | instanceInfo i => s!"instance {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" + | axiomInfo i => s!"axiom {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | theoremInfo i => s!"theorem {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | opaqueInfo i => s!"constant {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | definitionInfo i => s!"def {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | instanceInfo i => s!"instance {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" | inductiveInfo i => - let ctorString ← i.ctors.mapM (λ (name, type) => do s!"{name} : {←PrettyPrinter.formatTerm type}") - s!"inductive {i.name} : {←PrettyPrinter.formatTerm i.type}, ctors: {ctorString}, doc string: {i.doc}" + let ctorString ← i.ctors.mapM NameInfo.prettyPrint + s!"inductive {←i.toNameInfo.prettyPrint}, ctors: {ctorString}, doc string: {i.doc}" | structureInfo i => - let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}" - let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.fieldName} : {←PrettyPrinter.formatTerm f.type}") - s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" + let ctorString ← i.ctor.prettyPrint + let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.name} : {←PrettyPrinter.formatTerm f.type}") + s!"structure {←i.toNameInfo.prettyPrint} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" | classInfo i => - let instanceString ← i.instances.mapM (λ i => do s!"{←PrettyPrinter.formatTerm i}") - let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.fieldName} : {←PrettyPrinter.formatTerm f.type}") - s!"class {i.name} : {←PrettyPrinter.formatTerm i.type} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" + let instanceString ← i.instances.mapM PrettyPrinter.formatTerm + let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo) + s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" end DocInfo From 29a249e8fdd640c7367415c063d817ad1aebe66d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 5 Dec 2021 14:56:25 +0100 Subject: [PATCH 17/50] feat: Automatic search path + modules as CLI arguments --- DocGen4/Load.lean | 36 ++++++++++++++++++++++++++++++------ Main.lean | 12 ++++++------ 2 files changed, 36 insertions(+), 12 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 2df73fd..e44cd95 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -4,18 +4,42 @@ import Std.Data.HashMap namespace DocGen4 -open Lean System Std +open Lean System Std IO -def printSearchPath : IO PUnit := do - IO.println s!"{←searchPathRef.get}" +def getLakePath : IO FilePath := do + match (← IO.getEnv "LAKE") with + | some path => System.FilePath.mk path + | none => + let lakePath := (←findSysroot?) / "bin" / "lake" + lakePath.withExtension System.FilePath.exeExtension -def setSearchPath (path : List FilePath) : IO PUnit := do - searchPathRef.set path +-- Modified from the LSP Server +def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : IO Lean.SearchPath := do + let args := #["print-paths"] ++ imports + let cmdStr := " ".intercalate (toString lakePath :: args.toList) + let lakeProc ← Process.spawn { + stdin := Process.Stdio.null + stdout := Process.Stdio.piped + stderr := Process.Stdio.piped + cmd := lakePath.toString + args + } + let stdout := String.trim (← lakeProc.stdout.readToEnd) + let stderr := String.trim (← lakeProc.stderr.readToEnd) + match (← lakeProc.wait) with + | 0 => + let stdout := stdout.split (· == '\n') |>.getLast! + let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?) + | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" + initSearchPath (← findSysroot?) paths.oleanPath + paths.oleanPath.mapM realPathNormalized + | 2 => pure [] -- no lakefile.lean + | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" def load (imports : List Name) : IO (HashMap Name Module) := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats - let doc ← Prod.fst <$> (Meta.MetaM.toIO (process) { maxHeartbeats := 100000000} { env := env} {} {}) + let doc ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {}) for (_, module) in doc.toList do let s ← Core.CoreM.toIO module.prettyPrint {} { env := env } IO.println s.fst diff --git a/Main.lean b/Main.lean index 639455f..a4bab64 100644 --- a/Main.lean +++ b/Main.lean @@ -1,11 +1,11 @@ import DocGen4 import Lean -open DocGen4 Lean +open DocGen4 Lean IO - -def main : IO Unit := do - -- This should be set by lake at some point - setSearchPath ["/home/nix/Desktop/formal_verification/lean/mathlib4/build/lib", "/home/nix/.elan/toolchains/leanprover--lean4---nightly-2021-11-24/lib/lean"] - let doc ← load [`Mathlib] +def main (args : List String) : IO Unit := do + let modules := args + let path ← lakeSetupSearchPath (←getLakePath) modules.toArray + IO.println s!"Loading modules from: {path}" + let doc ← load $ modules.map Name.mkSimple return () From 7785c9f5bdf6740e99a42f135d581f9b1d3bd0e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 5 Dec 2021 15:45:19 +0100 Subject: [PATCH 18/50] feat: Fetch declaration ranges for constants --- DocGen4/Process.lean | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index e7f6d1c..0763c65 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -17,6 +17,7 @@ def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do structure Info extends NameInfo where doc : Option String + declarationRange : DeclarationRange deriving Repr structure AxiomInfo extends Info where @@ -90,7 +91,10 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv let type ← prettyPrintTerm v.type let doc := findDocString? env v.name - return Info.mk ⟨v.name, type⟩ doc + match ←findDeclarationRanges? v.name with + -- TODO: Maybe selection range is more relevant? Figure this out in the future + | some range => return Info.mk ⟨v.name, type⟩ doc range.range + | none => panic! s!"{v.name} is a declaration without position" def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do let info ← Info.ofConstantVal v.toConstantVal @@ -167,12 +171,16 @@ def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do namespace DocInfo def isBlackListed (declName : Name) : MetaM Bool := do - let env ← getEnv - declName.isInternal - <||> isAuxRecursor env declName - <||> isNoConfusion env declName - <||> isRec declName - <||> isMatcher declName + match ←findDeclarationRanges? declName with + | some _ => + let env ← getEnv + declName.isInternal + <||> isAuxRecursor env declName + <||> isNoConfusion env declName + <||> isRec declName + <||> isMatcher declName + -- TODO: Evaluate whether filtering out declarations without range is sensible + | none => true -- TODO: Is this actually the best way? def isProjFn (declName : Name) : MetaM Bool := do From 77cb52e9cb4bce46c6eb325a0dccaac6be2212f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 10 Dec 2021 13:29:04 +0100 Subject: [PATCH 19/50] chore: Inline licensing --- DocGen4.lean | 6 ++++++ DocGen4/Load.lean | 6 ++++++ DocGen4/Process.lean | 6 ++++++ 3 files changed, 18 insertions(+) diff --git a/DocGen4.lean b/DocGen4.lean index 9ce5c22..d8b7233 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -1,2 +1,8 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ + import DocGen4.Process import DocGen4.Load diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index e44cd95..7d04c64 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ + import Lean import DocGen4.Process import Std.Data.HashMap diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 0763c65..6116f9b 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ + import Lean import Lean.PrettyPrinter import Std.Data.HashMap From 11de4f7f5593a1ceaba284601b5ed3334f79e026 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 10 Dec 2021 14:30:39 +0100 Subject: [PATCH 20/50] chore: Import ToHtmlFormat https://github.com/leanprover/lean4/pull/723 Added some slight modifications so it is inside the DocGen4 instead of the Lean4.Widget namespace. --- DocGen4.lean | 1 + DocGen4/ToHtmlFormat.lean | 90 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 91 insertions(+) create mode 100644 DocGen4/ToHtmlFormat.lean diff --git a/DocGen4.lean b/DocGen4.lean index d8b7233..2b8c14f 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -6,3 +6,4 @@ Authors: Henrik Böving import DocGen4.Process import DocGen4.Load +import DocGen4.ToHtmlFormat diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean new file mode 100644 index 0000000..778edf7 --- /dev/null +++ b/DocGen4/ToHtmlFormat.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2021 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Wojciech Nawrocki, Sebastian Ullrich, Henrik Böving +-/ +import Lean.Data.Json +import Lean.Parser + +/-! This module defines: +- a representation of HTML trees +- together with a JSX-like DSL for writing them +- and widget support for visualizing any type as HTML. -/ + +namespace DocGen4 + +open Lean + +inductive Html where + -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson + -- element (tag : String) (attrs : Array HtmlAttribute) (children : Array Html) + | element : String → Array (String × String) → Array Html → Html + | text : String → Html + deriving Repr, BEq, Inhabited, FromJson, ToJson + +instance : Coe String Html := + ⟨Html.text⟩ + +namespace Jsx +open Parser PrettyPrinter + +declare_syntax_cat jsxElement +declare_syntax_cat jsxChild + +def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") +def jsxAttr : Parser := ident >> "=" >> jsxAttrVal + +-- JSXTextCharacter : SourceCharacter but not one of {, <, > or } +def jsxText : Parser := + withAntiquot (mkAntiquot "jsxText" `jsxText) { + fn := fun c s => + let startPos := s.pos + let s := takeWhile1Fn (not ∘ "{<>}$".contains) "expected JSX text" c s + mkNodeToken `jsxText startPos c s } + +@[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure () +@[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure () + +scoped syntax "<" ident jsxAttr* "/>" : jsxElement +scoped syntax "<" ident jsxAttr* ">" jsxChild* "" : jsxElement + +scoped syntax jsxText : jsxChild +scoped syntax "{" term "}" : jsxChild +scoped syntax jsxElement : jsxChild + +scoped syntax:max jsxElement : term + +macro_rules + | `(<$n $[$ns = $vs]* />) => + let ns := ns.map (quote <| toString ·.getId) + let vs := vs.map fun + | `(jsxAttrVal| $s:strLit) => s + | `(jsxAttrVal| { $t:term }) => t + | _ => unreachable! + `(Html.element $(quote <| toString n.getId) #[ $[($ns, $vs)],* ] #[]) + | `(<$n $[$ns = $vs]* >$cs*) => + if n.getId == m.getId then do + let ns := ns.map (quote <| toString ·.getId) + let vs := vs.map fun + | `(jsxAttrVal| $s:strLit) => s + | `(jsxAttrVal| { $t:term }) => t + | _ => unreachable! + let cs ← cs.mapM fun + | `(jsxChild|$t:jsxText) => `(Html.text $(quote t[0].getAtomVal!)) + -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t` + | `(jsxChild|{$t}) => t + | `(jsxChild|$e:jsxElement) => `($e:jsxElement) + | _ => unreachable! + let tag := toString n.getId + `(Html.element $(quote tag) #[ $[($ns, $vs)],* ] #[ $[$cs],* ]) + else Macro.throwError ("expected ") + +end Jsx + +/-- A type which implements `ToHtmlFormat` will be visualized +as the resulting HTML in editors which support it. -/ +class ToHtmlFormat (α : Type u) where + formatHtml : α → Html + +end DocGen4 From e9a9e17439f92c974bd9688ba99a1ba2a18bbb77 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 10 Dec 2021 15:24:38 +0100 Subject: [PATCH 21/50] feat: Basic Html to String converter It works okay-ish for basic HTML which should be good enough for now --- DocGen4/ToHtmlFormat.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index 778edf7..2b617d2 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -26,6 +26,27 @@ inductive Html where instance : Coe String Html := ⟨Html.text⟩ +namespace Html + +def attributesToString (attrs : Array (String × String)) :String := + attrs.foldl (λ acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") "" + +-- TODO: Termination proof +partial def toStringAux : Html → String +| element tag attrs #[] => s!"<{tag}{attributesToString attrs}/>\n" +| element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" +| element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" +| element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" +| text s => s + +def toString (html : Html) : String := + html.toStringAux.trimRight + +instance : ToString Html := + ⟨toString⟩ + +end Html + namespace Jsx open Parser PrettyPrinter From c2da7afd76b8294bbb4ca7582a7d8f243571889e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 11 Dec 2021 14:26:32 +0100 Subject: [PATCH 22/50] chore: Update compiler and fix minor breaking change --- DocGen4/Process.lean | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 6116f9b..89b7313 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -96,7 +96,7 @@ def prettyPrintTerm (expr : Expr) : MetaM Syntax := do def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv let type ← prettyPrintTerm v.type - let doc := findDocString? env v.name + let doc ← findDocString? env v.name match ←findDeclarationRanges? v.name with -- TODO: Maybe selection range is more relevant? Figure this out in the future | some range => return Info.mk ⟨v.name, type⟩ doc range.range diff --git a/lean-toolchain b/lean-toolchain index 22206e9..45db7af 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2021-11-26 +leanprover/lean4:nightly-2021-12-10 From 413a24da56490189334a76a71f87ebf5a45474b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:18:24 +0100 Subject: [PATCH 23/50] feat: improve HTML to String a bit --- DocGen4/ToHtmlFormat.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index 2b617d2..b2f4629 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -33,7 +33,6 @@ def attributesToString (attrs : Array (String × String)) :String := -- TODO: Termination proof partial def toStringAux : Html → String -| element tag attrs #[] => s!"<{tag}{attributesToString attrs}/>\n" | element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" | element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" | element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" From 0719fd6e30f9341af06e4a83a5da36b3cb420f06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:18:48 +0100 Subject: [PATCH 24/50] feat: Allow Array Html as child of an HTMl node --- DocGen4/ToHtmlFormat.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index b2f4629..8afda02 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -52,7 +52,7 @@ open Parser PrettyPrinter declare_syntax_cat jsxElement declare_syntax_cat jsxChild -def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") +def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") <|> ("[" >> termParser >> "]") def jsxAttr : Parser := ident >> "=" >> jsxAttrVal -- JSXTextCharacter : SourceCharacter but not one of {, <, > or } @@ -60,7 +60,7 @@ def jsxText : Parser := withAntiquot (mkAntiquot "jsxText" `jsxText) { fn := fun c s => let startPos := s.pos - let s := takeWhile1Fn (not ∘ "{<>}$".contains) "expected JSX text" c s + let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s mkNodeToken `jsxText startPos c s } @[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure () @@ -71,6 +71,7 @@ scoped syntax "<" ident jsxAttr* ">" jsxChild* "" : jsxElement scoped syntax jsxText : jsxChild scoped syntax "{" term "}" : jsxChild +scoped syntax "[" term "]" : jsxChild scoped syntax jsxElement : jsxChild scoped syntax:max jsxElement : term @@ -91,13 +92,14 @@ macro_rules | `(jsxAttrVal| { $t:term }) => t | _ => unreachable! let cs ← cs.mapM fun - | `(jsxChild|$t:jsxText) => `(Html.text $(quote t[0].getAtomVal!)) + | `(jsxChild|$t:jsxText) => `(#[Html.text $(quote t[0].getAtomVal!)]) -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t` - | `(jsxChild|{$t}) => t - | `(jsxChild|$e:jsxElement) => `($e:jsxElement) + | `(jsxChild|{$t}) => `(#[$t]) + | `(jsxChild|[$t]) => `($t) + | `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement]) | _ => unreachable! let tag := toString n.getId - `(Html.element $(quote tag) #[ $[($ns, $vs)],* ] #[ $[$cs],* ]) + `(Html.element $(quote tag) #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ])) else Macro.throwError ("expected ") end Jsx From 0f0a355a931c7501cdabe2d0efe59e00dd584a00 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:20:03 +0100 Subject: [PATCH 25/50] feat: include_str macro for static file inclusion --- DocGen4/IncludeStr.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 DocGen4/IncludeStr.lean diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean new file mode 100644 index 0000000..335365a --- /dev/null +++ b/DocGen4/IncludeStr.lean @@ -0,0 +1,21 @@ +import Lean + +namespace DocGen4 + +open Lean System IO Lean.Elab.Term + +syntax (name := includeStr) "include_str" str : term + +@[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do + let str := stx[1].isStrLit?.get! + let path := FilePath.mk str + if ←path.pathExists then + if ←path.isDir then + throwError s!"{str} is a directory" + else + let content ← FS.readFile path + return mkStrLit content + else + throwError s!"\"{str}\" does not exist as a file" + +end DocGen4 From fcfe11e168b1048afa3713f9f1c47cef05b49306 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:20:44 +0100 Subject: [PATCH 26/50] feat: Hierarchy datatype --- DocGen4/Hierarchy.lean | 72 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 72 insertions(+) create mode 100644 DocGen4/Hierarchy.lean diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean new file mode 100644 index 0000000..d023e85 --- /dev/null +++ b/DocGen4/Hierarchy.lean @@ -0,0 +1,72 @@ +import Lean +import Std.Data.HashMap + +namespace DocGen4 + +open Lean Std Name + +def getDepth : Name → Nat +| Name.anonymous => 0 +| Name.str p _ _ => getDepth p + 1 +| Name.num p _ _ => getDepth p + 1 + +def getNLevels (name : Name) (levels: Nat) : Name := + (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous + where + components := name.components' + +inductive Hierarchy where +| node : Name → RBNode Name (λ _ => Hierarchy) → Hierarchy + +instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous RBNode.leaf⟩ + +abbrev HierarchyMap := RBNode Name (λ _ => Hierarchy) + +-- Everything in this namespace is adapted from stdlib's RBNode +namespace HierarchyMap + +def toList : HierarchyMap → List (Name × Hierarchy) +| t => t.revFold (fun ps k v => (k, v)::ps) [] + +def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (Name × Hierarchy) → σ → m (ForInStep σ)) : m σ := + t.forIn init (fun a b acc => f (a, b) acc) + +instance : ForIn m HierarchyMap (Name × Hierarchy) where + forIn := HierarchyMap.hForIn + +end HierarchyMap + +namespace Hierarchy + +def empty (n : Name) : Hierarchy := node n RBNode.leaf + +def getName : Hierarchy → Name +| node n _ => n + +def getChildren : Hierarchy → HierarchyMap +| node _ c => c + +partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := do + let hn := h.getName + let mut cs := h.getChildren + if getDepth hn ≥ getDepth n then + panic! "Invalid insert" + else if getDepth hn + 1 == getDepth n then + match cs.find Name.cmp n with + | none => + node hn (cs.insert Name.cmp n $ empty n) + | some _ => h + else + let leveledName := getNLevels n (getDepth hn + 1) + match cs.find Name.cmp leveledName with + | some nextLevel => + cs := cs.erase Name.cmp leveledName + node hn $ cs.insert Name.cmp leveledName (nextLevel.insert! n) + | none => + let child := (insert! (empty leveledName) n) + node hn $ cs.insert Name.cmp leveledName child + +partial def fromArray (names : Array Name) : Hierarchy := names.foldl insert! (empty anonymous) + +end Hierarchy +end DocGen4 From ded884ce9c1dfb6f56e8ba8a6ce6fbe14b109f3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:21:53 +0100 Subject: [PATCH 27/50] feat: HTML Index + CSS --- DocGen4.lean | 4 +- DocGen4/Load.lean | 11 +- DocGen4/Output.lean | 130 ++++++++++ DocGen4/Process.lean | 12 +- Main.lean | 2 +- static/style.css | 562 +++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 708 insertions(+), 13 deletions(-) create mode 100644 DocGen4/Output.lean create mode 100644 static/style.css diff --git a/DocGen4.lean b/DocGen4.lean index 2b8c14f..bc6d9b6 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -3,7 +3,9 @@ Copyright (c) 2021 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ - +import DocGen4.Hierarchy import DocGen4.Process import DocGen4.Load import DocGen4.ToHtmlFormat +import DocGen4.IncludeStr +import DocGen4.Output diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 7d04c64..0767545 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -42,15 +42,10 @@ def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : | 2 => pure [] -- no lakefile.lean | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" -def load (imports : List Name) : IO (HashMap Name Module) := do +def load (imports : List Name) : IO AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats - let doc ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {}) - for (_, module) in doc.toList do - let s ← Core.CoreM.toIO module.prettyPrint {} { env := env } - IO.println s.fst - IO.println s!"Processed {List.foldl (λ a (_, b) => a + b.members.size) 0 doc.toList} declarations" - IO.println s!"Processed {doc.size} modules" - return doc + let res ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {}) + return res end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean new file mode 100644 index 0000000..9c1f124 --- /dev/null +++ b/DocGen4/Output.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Lean +import Std.Data.HashMap +import DocGen4.Process +import DocGen4.ToHtmlFormat +import DocGen4.IncludeStr + +namespace DocGen4 + +open Lean Std +open scoped DocGen4.Jsx + +structure SiteContext where + root : String + result : AnalyzerResult + +abbrev HtmlM := Reader SiteContext + +def getRoot : HtmlM String := do (←read).root +def getResult : HtmlM AnalyzerResult := do (←read).result + +def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := + new >>= base + +def nameToPath (n : Name) : String := do + let parts := n.components.map Name.toString + return (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" + +partial def moduleListAux (h : Hierarchy) : HtmlM Html := do + if h.getChildren.toList.length == 0 then + + else + let children := Array.mk (h.getChildren.toList.map Prod.snd) + -- TODO: Is having no children really the correct criterium for a clickable module? + let (dirs, files) := children.partition (λ c => c.getChildren.toList.length != 0) + let nodes := (←(dirs.mapM moduleListAux)) ++ (←(files.mapM moduleListAux)) + return
+ {h.getName.toString} + [nodes] +
+ +def moduleList : HtmlM (Array Html) := do + let hierarchy := (←getResult).hierarchy + let mut list := Array.empty + for (n, cs) in hierarchy.getChildren do + list := list.push

{n.toString}

+ list := list.push $ ←moduleListAux cs + list + +def navbar : HtmlM Html := do + + +def baseHtml (title : String) (site : Html) : HtmlM Html := do + + + + + + {title} + + + + + + + + +
+

Documentation

+

{title}

+ -- TODO: Replace this form with our own search +
+ + + +
+
+ + + + {site} + + {←navbar} + -- TODO Add the js stuff + + + + +def index : HtmlM Html := do templateExtends (baseHtml "Index") $ +
+ +

Welcome to the documentation page

+ What is up? +
+ +open IO System + +def styleCss : String := include_str "./static/style.css" + +def htmlOutput (result : AnalyzerResult) : IO Unit := do + -- TODO: parameterize this + let config := { root := "/", result := result } + let basePath := FilePath.mk "./build/doc/" + let indexHtml := ReaderT.run index config + FS.createDirAll basePath + FS.writeFile (basePath / "index.html") indexHtml.toString + FS.writeFile (basePath / "style.css") styleCss + +end DocGen4 + diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 89b7313..950beac 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -9,6 +9,8 @@ import Lean.PrettyPrinter import Std.Data.HashMap import Lean.Meta.SynthInstance +import DocGen4.Hierarchy + namespace DocGen4 open Lean Meta PrettyPrinter Std @@ -221,7 +223,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, some $ instanceInfo info else some $ definitionInfo info - -- TODO: Differentiate between all the different types of inductives (structures, classes etc.) | ConstantInfo.inductInfo i => let env ← getEnv if isStructure env i.name then @@ -265,7 +266,12 @@ def prettyPrint (m : Module) : CoreM String := do end Module -def process : MetaM (HashMap Name Module) := do +structure AnalyzerResult where + modules : HashMap Name Module + hierarchy : Hierarchy + deriving Inhabited + +def process : MetaM AnalyzerResult := do let env ← getEnv let mut res := mkHashMap env.header.moduleNames.size for module in env.header.moduleNames do @@ -289,6 +295,6 @@ def process : MetaM (HashMap Name Module) := do res := res.insert moduleName {module with members := module.members.push dinfo} | none => panic! "impossible" | none => () - return res + return { modules := res, hierarchy := Hierarchy.fromArray env.header.moduleNames } end DocGen4 diff --git a/Main.lean b/Main.lean index a4bab64..cdae0ee 100644 --- a/Main.lean +++ b/Main.lean @@ -8,4 +8,4 @@ def main (args : List String) : IO Unit := do let path ← lakeSetupSearchPath (←getLakePath) modules.toArray IO.println s!"Loading modules from: {path}" let doc ← load $ modules.map Name.mkSimple - return () + htmlOutput doc diff --git a/static/style.css b/static/style.css new file mode 100644 index 0000000..5743e2f --- /dev/null +++ b/static/style.css @@ -0,0 +1,562 @@ +@import url('https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro&family=Source+Code+Pro:wght@600&display=swap'); + +* { + box-sizing: border-box; +} + +body { + font-family: 'Open Sans', sans-serif; +} +h1, h2, h3, h4, h5, h6 { + font-family: 'Merriweather', serif; +} + +body { line-height: 1.5; } +nav { line-height: normal; } + +:root { + --header-height: 3em; + --header-bg: #f8f8f8; + --fragment-offset: calc(var(--header-height) + 1em); + --content-width: 55vw; +} +@supports (width: min(10px, 5vw)) { + :root { + --content-width: clamp(20em, 55vw, 60em); + } +} + +#nav_toggle { + display: none; +} +label[for="nav_toggle"] { + display: none; +} + +header { + height: var(--header-height); + float: left; + position: fixed; + width: 100vw; + max-width: 100%; + left: 0; + right: 0; + top: 0; + --header-side-padding: 2em; + padding: 0 var(--header-side-padding); + background: var(--header-bg); + z-index: 1; + display: flex; + align-items: center; + justify-content: space-between; +} +@supports (width: min(10px, 5vw)) { + header { + --header-side-padding: calc(max(2em, (100vw - var(--content-width) - 30em) / 2)); + } +} +@media screen and (max-width: 1000px) { + :root { + --content-width: 100vw; + } + + .internal_nav { + display: none; + } + + body .nav { + width: 100vw; + max-width: 100vw; + margin-left: 1em; + z-index: 1; + } + + body main { + width: unset; + max-width: unset; + margin-left: unset; + margin-right: unset; + } + body .decl > div { + overflow-x: unset; + } + + #nav_toggle:not(:checked) ~ .nav { + display: none; + } + #nav_toggle:checked ~ main { + visibility: hidden; + } + + label[for="nav_toggle"]::before { + content: '≡'; + } + label[for="nav_toggle"] { + display: inline-block; + margin-right: 1em; + border: 1px solid #ccc; + padding: 0.5ex 1ex; + cursor: pointer; + background: #eee; + } + #nav_toggle:checked ~ * label[for="nav_toggle"] { + background: white; + } + + body header h1 { + font-size: 100%; + } + + header { + --header-side-padding: 1ex; + } +} +@media screen and (max-width: 700px) { + header h1 span { display: none; } + :root { --header-side-padding: 1ex; } + #search_form button { display: none; } + #search_form input { width: 100%; } + header #search_results { + left: 1ex; + right: 1ex; + width: inherit; + } + body header > * { margin: 0; } +} + +header > * { + display: inline-block; + padding: 0; + margin: 0 1em; + vertical-align: middle; +} + +header h1 { + font-weight: normal; + font-size: 160%; +} + +header header_filename { + font-size: 150%; +} +@media (max-width: 80em) { + .header .header_filename { + display: none; + } +} + +/* inserted by nav.js */ +#search_results { + position: absolute; + top: var(--header-height); + right: calc(var(--header-side-padding)); + width: calc(20em + 4em); + z-index: 1; + background: var(--header-bg); + border: 1px solid #aaa; + border-top: none; + overflow-x: hidden; + overflow-y: auto; + max-height: calc(100vh - var(--header-height)); +} + +#search_results:empty { + display: none; +} + +#search_results[state="loading"]:empty { + display: block; + cursor: progress; +} +#search_results[state="loading"]:empty::before { + display: block; + content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 '; + padding: 1ex; + animation: marquee 10s linear infinite; +} +@keyframes marquee { + 0% { transform: translate(100%, 0); } + 100% { transform: translate(-100%, 0); } +} + +#search_results[state="done"]:empty { + display: block; + text-align: center; + padding: 1ex; +} +#search_results[state="done"]:empty::before { + content: '(no results)'; + font-style: italic; +} + +#search_results a { + display: block; + color: inherit; + padding: 1ex; + border-left: 0.5ex solid transparent; + padding-left: 0.5ex; + cursor: pointer; +} +#search_results .selected { + background: white; + border-color: #f0a202; +} + +main, nav { + margin-top: calc(var(--header-height) + 1em); +} + +/* extra space for scrolling things to the top */ +main { + margin-bottom: 90vh; +} + +main { + max-width: var(--content-width); + /* center it: */ + margin-left: auto; + margin-right: auto; +} + +nav { + float: left; + height: calc(100vh - var(--header-height) - 1em); + position: fixed; + top: 0; + overflow: auto; + scrollbar-width: thin; + scrollbar-color: transparent transparent; +} + +nav:hover { + scrollbar-color: gray transparent; +} + +nav { + --column-available-space: calc((100vw - var(--content-width) - 5em)/2); + --column-width: calc(var(--column-available-space) - 1ex); + --dist-to-edge: 1ex; + width: var(--content-width); + max-width: var(--column-width); +} +@supports (width: min(10px, 5vw)) { + .nav { --desired-column-width: 20em; } + .internal_nav { --desired-column-width: 30em; } + nav { + --column-available-space: calc(max(0px, (100vw - var(--content-width) - 5em)/2)); + --column-width: calc(clamp(0px, var(--column-available-space) - 1ex, var(--desired-column-width))); + --dist-to-edge: calc(max(1ex, var(--column-available-space) - var(--column-width))); + } +} + +.nav { left: var(--dist-to-edge); } +.internal_nav { right: var(--dist-to-edge); } + +.internal_nav .nav_link, .taclink { + /* indent everything but first line by 2ex */ + text-indent: -2ex; padding-left: 2ex; +} + +.internal_nav .imports { + margin-bottom: 1rem; +} + +.tagfilter-div { + margin-bottom: 1em; +} +.tagfilter-div > summary { + margin-bottom: 1ex; +} + +.nav details > * { + padding-left: 2ex; +} +.nav summary { + cursor: pointer; + padding-left: 0; +} +.nav summary::marker { + font-size: 85%; +} + +.nav .nav_file { + display: inline-block; +} + +.nav h3 { + margin-block-end: 4px; +} + +.nav h4 { + margin-bottom: 1ex; +} + +/* People use way too long declaration names. */ +.internal_nav, .decl_name { + overflow-wrap: break-word; +} + +.decl > div, .mod_doc { + padding-left: 8px; + padding-right: 8px; +} + +.decl { + margin-top: 20px; + margin-bottom: 20px; +} + +.decl > div { + /* sometimes declarations arguments are way too long + and would continue into the right column, + so put a scroll bar there: */ + overflow-x: auto; +} + +/* Make `#id` links appear below header. */ +.decl, h1[id], h2[id], h3[id], h4[id], h5[id], h6[id] { + scroll-margin-top: var(--fragment-offset); +} +/* don't need as much vertical space for these +inline elements */ +a[id], li[id] { + scroll-margin-top: var(--header-height); +} + +/* HACK: Safari doesn't support scroll-margin-top for +fragment links (yet?) +https://caniuse.com/mdn-css_properties_scroll-margin-top +https://bugs.webkit.org/show_bug.cgi?id=189265 +*/ +@supports not (scroll-margin-top: var(--fragment-offset)) { + .decl::before, h1[id]::before, h2[id]::before, h3[id]::before, + h4[id]::before, h5[id]::before, h6[id]::before, + a[id]::before, li[id]::before { + content: ""; + display: block; + height: var(--fragment-offset); + margin-top: calc(-1 * var(--fragment-offset)); + box-sizing: inherit; + visibility: hidden; + width: 1px; + } +} + + +/* hide # after markdown headings except on hover */ +.markdown-heading:not(:hover) > .hover-link { + visibility: hidden; +} + +main h2, main h3, main h4, main h5, main h6 { + margin-top: 2rem; +} +.decl + .mod_doc > h2, + .decl + .mod_doc > h3, + .decl + .mod_doc > h4, + .decl + .mod_doc > h5, + .decl + .mod_doc > h6 { + margin-top: 4rem; +} + +.def { + border-left: 10px solid #92dce5; + border-top: 2px solid #92dce5; +} + +.theorem { + border-left: 10px solid #8fe388; + border-top: 2px solid #8fe388; +} + +.axiom, .constant { + border-left: 10px solid #f44708; + border-top: 2px solid #f44708; +} + +.structure, .inductive { + border-left: 10px solid #f0a202; + border-top: 2px solid #f0a202; +} + +.fn { + display: inline-block; + /* border: 1px dashed red; */ + text-indent: -1ex; + padding-left: 1ex; + white-space: pre-wrap; + vertical-align: top; +} + +.fn { --fn: 1; } +.fn .fn { --fn: 2; } +.fn .fn .fn { --fn: 3; } +.fn .fn .fn .fn { --fn: 4; } +.fn .fn .fn .fn .fn { --fn: 5; } +.fn .fn .fn .fn .fn .fn { --fn: 6; } +.fn .fn .fn .fn .fn .fn .fn { --fn: 7; } +.fn .fn .fn .fn .fn .fn .fn .fn { --fn: 8; } +.fn { + transition: background-color 100ms ease-in-out; +} + +.def .fn:hover { + background-color: hsla(187, 61%, calc(100% - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(187, 61%, calc(100% - 5%*(var(--fn) + 1))); + border-radius: 5px; +} +.theorem .fn:hover { + background-color: hsla(115, 62%, calc(100% - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(115, 62%, calc(100% - 5%*(var(--fn) + 1))); + border-radius: 5px; +} +.axiom .fn:hover, .constant .fn:hover { + background-color: hsla(16, 94%, calc(100% - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(16, 94%, calc(100% - 5%*(var(--fn) + 1))); + border-radius: 5px; +} +.structure .fn:hover, .inductive .fn:hover { + background-color: hsla(40, 98%, calc(100% - 5%*var(--fn))); + box-shadow: 0 0 0 1px hsla(40, 98%, calc(100% - 5%*(var(--fn) + 1))); + border-radius: 5px; +} + +.decl_args, .decl_type { + font-weight: normal; +} + +.implicits, .impl_arg { + color: black; + white-space: nowrap; +} + +.decl_kind, .decl_name { + font-weight: bold; +} + +/* break long declaration names at periods where possible */ +.break_within { + word-break: break-all; +} + +.break_within .name { + word-break: normal; +} + +.decl_header { + /* indent everything but first line twice as much as decl_type */ + text-indent: -8ex; padding-left: 8ex; +} + +.decl_type { + margin-top: 2px; + margin-left: 4ex; /* extra indentation */ +} + +.imports li, code, .decl_header, .attributes, .structure_field, + .constructor, .instances li, .equation, #search_results div { + font-family: 'Source Code Pro', monospace; +} + +pre { + white-space: break-spaces; +} + +code, pre { background: #f3f3f3; } +code, pre { border-radius: 5px; } +code { padding: 1px 3px; } +pre { padding: 1ex; } +pre code { padding: 0 0; } + +#howabout code { background: inherit; } +#howabout li { margin-bottom: 0.5ex; } + +.structure_fields, .constructors { + display: block; + padding-inline-start: 0; + margin-top: 1ex; + text-indent: -2ex; padding-left: 2ex; +} + +.structure_field { + display: block; +} +.structure_field:before { + content: '('; + color: gray; +} +.structure_field:after { + content: ')'; + color: gray; +} + +.constructor { + display: block; +} +.constructor:before { + content: '| '; + color: gray; +} + +/** Don't show underline on types, to prevent the ≤ vs < confusion. **/ +a:link, a:visited, a:active { + color:hsl(210, 100%, 30%); + text-decoration: none; +} + +/** Show it on hover though. **/ +a:hover { + text-decoration: underline; +} + +.impl_arg { + font-style: italic; + transition: opacity 300ms ease-in; +} + +.decl_header:not(:hover) .impl_arg { + opacity: 30%; + transition: opacity 1000ms ease-out; +} + +.gh_link { + float: right; + margin-left: 20px; +} + +.docfile h2, .note h2 { + margin-block-start: 3px; + margin-block-end: 0px; +} + +.docfile h2 a { + color: black; +} + +.tags { + margin-bottom: 1ex; +} + +.tags ul { + display: inline; + padding: 0; +} + +.tags li { + border: 1px solid #555; + border-radius: 4px; + list-style-type: none; + padding: 1px 3px; + margin-left: 1ex; + display: inline-block; +} + +/* used by nav.js */ +.hide { display: none; } + +.tactic, .note { + border-top: 3px solid #0479c7; + padding-top: 2em; + margin-top: 2em; + margin-bottom: 2em; +} From 40ec83362336cfc1009ca4c17ea2aa015def5df4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:27:38 +0100 Subject: [PATCH 28/50] doc: Basic usage in README --- README.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/README.md b/README.md index fcf7a8a..d0ff1e1 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,15 @@ # doc-gen4 Document Generator for Lean 4 + +## Usage +You can call `doc-gen4` from the top of a Lake project like this: +```sh +$ /path/to/doc-gen4 Module +``` +Where `Module` is one or more of the top level modules you want to document. +The tool will then proceed to compile the project using lake (if that hasn't happened yet), +analyze it and put the result in `./build/doc`. +You could e.g. host the files locally with the built-in Python webserver: +```sh +$ cd build/doc && python -m http.server +``` From dbbe11da0a34026a1d9aad4d6c31bdba72ff99ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:28:52 +0100 Subject: [PATCH 29/50] chore: In file licensing --- DocGen4/Hierarchy.lean | 5 +++++ DocGen4/IncludeStr.lean | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean index d023e85..034a290 100644 --- a/DocGen4/Hierarchy.lean +++ b/DocGen4/Hierarchy.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ import Lean import Std.Data.HashMap diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean index 335365a..6946ab5 100644 --- a/DocGen4/IncludeStr.lean +++ b/DocGen4/IncludeStr.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ import Lean namespace DocGen4 From 5e5bbe6ffb2585ee98227cbd407fe48d8e58f328 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 12 Dec 2021 13:33:24 +0100 Subject: [PATCH 30/50] chore: Update lean toolchain --- DocGen4/Hierarchy.lean | 2 +- DocGen4/Output.lean | 7 ++++--- lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean index 034a290..9f8a0d4 100644 --- a/DocGen4/Hierarchy.lean +++ b/DocGen4/Hierarchy.lean @@ -51,7 +51,7 @@ def getName : Hierarchy → Name def getChildren : Hierarchy → HierarchyMap | node _ c => c -partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := do +partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do let hn := h.getName let mut cs := h.getChildren if getDepth hn ≥ getDepth n then diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 9c1f124..a11618f 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -26,9 +26,10 @@ def getResult : HtmlM AnalyzerResult := do (←read).result def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base -def nameToPath (n : Name) : String := do - let parts := n.components.map Name.toString - return (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" +def nameToPath (n : Name) : String := + (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" + where + parts := n.components.map Name.toString partial def moduleListAux (h : Hierarchy) : HtmlM Html := do if h.getChildren.toList.length == 0 then diff --git a/lean-toolchain b/lean-toolchain index 45db7af..8b6c918 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2021-12-10 +leanprover/lean4:nightly-2021-12-12 From 9256aaa0fcdedc596cbc8a88d077e44c36578b74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 13 Dec 2021 13:00:53 +0100 Subject: [PATCH 31/50] feat: 404 page and module hierarchy --- DocGen4/Output.lean | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index a11618f..4d92118 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -13,6 +13,7 @@ namespace DocGen4 open Lean Std open scoped DocGen4.Jsx +open IO System structure SiteContext where root : String @@ -26,22 +27,27 @@ def getResult : HtmlM AnalyzerResult := do (←read).result def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base -def nameToPath (n : Name) : String := +def nameToUrl (n : Name) : String := (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" where parts := n.components.map Name.toString +def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := + basePath / parts.foldl (λ acc p => acc / FilePath.mk p) (FilePath.mk ".") + where + parts := n.components.dropLast.map Name.toString + partial def moduleListAux (h : Hierarchy) : HtmlM Html := do if h.getChildren.toList.length == 0 then else let children := Array.mk (h.getChildren.toList.map Prod.snd) -- TODO: Is having no children really the correct criterium for a clickable module? let (dirs, files) := children.partition (λ c => c.getChildren.toList.length != 0) let nodes := (←(dirs.mapM moduleListAux)) ++ (←(files.mapM moduleListAux)) - return
+ return
{h.getName.toString} [nodes]
@@ -107,6 +113,13 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do +def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ +
+

404 Not Found

+

Unfortunately, the page you were looking for is no longer here.

+
+
+ def index : HtmlM Html := do templateExtends (baseHtml "Index") $
@@ -114,18 +127,28 @@ def index : HtmlM Html := do templateExtends (baseHtml "Index") $ What is up?
-open IO System - def styleCss : String := include_str "./static/style.css" +def moduleToHtml (module : Module) : HtmlM Html := do templateExtends (baseHtml module.name.toString) $ +
+

This is the page of {module.name.toString}

+
+ def htmlOutput (result : AnalyzerResult) : IO Unit := do -- TODO: parameterize this let config := { root := "/", result := result } let basePath := FilePath.mk "./build/doc/" let indexHtml := ReaderT.run index config + let notFoundHtml := ReaderT.run notFound config FS.createDirAll basePath FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "style.css") styleCss + FS.writeFile (basePath / "404.html") notFoundHtml.toString + for (module, content) in result.modules.toArray do + let moduleHtml := ReaderT.run (moduleToHtml content) config + let path := basePath / (nameToUrl module) + FS.createDirAll $ nameToDirectory basePath module + FS.writeFile path moduleHtml.toString end DocGen4 From d2594669faf269133c57b15b25d5266b15e88296 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 13 Dec 2021 20:47:52 +0100 Subject: [PATCH 32/50] feat: Revamp the hierarchy mechanism Previously the hierarchy mechanism wouldn't show modules in files that have names, equal to some directory with submodules. --- DocGen4/Hierarchy.lean | 38 ++++++++++++++++++++++++-------------- DocGen4/Output.lean | 30 +++++++++++++++--------------- 2 files changed, 39 insertions(+), 29 deletions(-) diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean index 9f8a0d4..205fec0 100644 --- a/DocGen4/Hierarchy.lean +++ b/DocGen4/Hierarchy.lean @@ -21,9 +21,9 @@ def getNLevels (name : Name) (levels: Nat) : Name := components := name.components' inductive Hierarchy where -| node : Name → RBNode Name (λ _ => Hierarchy) → Hierarchy +| node (name : Name) (isFile : Bool) (children : RBNode Name (λ _ => Hierarchy)) : Hierarchy -instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous RBNode.leaf⟩ +instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩ abbrev HierarchyMap := RBNode Name (λ _ => Hierarchy) @@ -43,35 +43,45 @@ end HierarchyMap namespace Hierarchy -def empty (n : Name) : Hierarchy := node n RBNode.leaf +def empty (n : Name) (isFile : Bool) : Hierarchy := + node n isFile RBNode.leaf def getName : Hierarchy → Name -| node n _ => n +| node n _ _ => n def getChildren : Hierarchy → HierarchyMap -| node _ c => c +| node _ _ c => c + +def isFile : Hierarchy → Bool +| node _ f _ => f partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do let hn := h.getName let mut cs := h.getChildren - if getDepth hn ≥ getDepth n then - panic! "Invalid insert" - else if getDepth hn + 1 == getDepth n then + + assert! getDepth hn ≤ getDepth n + + if getDepth hn + 1 == getDepth n then match cs.find Name.cmp n with | none => - node hn (cs.insert Name.cmp n $ empty n) - | some _ => h + node hn h.isFile (cs.insert Name.cmp n $ empty n true) + | some (node _ true _) => h + | some hierarchy@(node _ false ccs) => + cs := cs.erase Name.cmp n + node hn h.isFile (cs.insert Name.cmp n $ node n true ccs) else let leveledName := getNLevels n (getDepth hn + 1) match cs.find Name.cmp leveledName with | some nextLevel => cs := cs.erase Name.cmp leveledName - node hn $ cs.insert Name.cmp leveledName (nextLevel.insert! n) + -- BUG? + node hn h.isFile $ cs.insert Name.cmp leveledName (nextLevel.insert! n) | none => - let child := (insert! (empty leveledName) n) - node hn $ cs.insert Name.cmp leveledName child + let child := (insert! (empty leveledName false) n) + node hn h.isFile $ cs.insert Name.cmp leveledName child -partial def fromArray (names : Array Name) : Hierarchy := names.foldl insert! (empty anonymous) +partial def fromArray (names : Array Name) : Hierarchy := + names.foldl insert! (empty anonymous false) end Hierarchy end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 4d92118..3be747c 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -37,27 +37,27 @@ def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := where parts := n.components.dropLast.map Name.toString -partial def moduleListAux (h : Hierarchy) : HtmlM Html := do - if h.getChildren.toList.length == 0 then - - else - let children := Array.mk (h.getChildren.toList.map Prod.snd) - -- TODO: Is having no children really the correct criterium for a clickable module? - let (dirs, files) := children.partition (λ c => c.getChildren.toList.length != 0) - let nodes := (←(dirs.mapM moduleListAux)) ++ (←(files.mapM moduleListAux)) - return
- {h.getName.toString} - [nodes] -
+def moduleListFile (file : Name) : HtmlM Html := do + + +partial def moduleListDir (h : Hierarchy) : HtmlM Html := do + let children := Array.mk (h.getChildren.toList.map Prod.snd) + let dirs := children.filter (λ c => c.getChildren.toList.length != 0) + let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName + return
+ {h.getName.toString} + [(←(dirs.mapM moduleListDir))] + [(←(files.mapM moduleListFile))] +
def moduleList : HtmlM (Array Html) := do let hierarchy := (←getResult).hierarchy let mut list := Array.empty for (n, cs) in hierarchy.getChildren do list := list.push

{n.toString}

- list := list.push $ ←moduleListAux cs + list := list.push $ ←moduleListDir cs list def navbar : HtmlM Html := do From ef8ecec0d7d7bfec2729756c0c2341c1bc35c15e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 13 Dec 2021 21:27:08 +0100 Subject: [PATCH 33/50] feat: Implement visibility in the navbar --- DocGen4/Output.lean | 44 +++++++++++++++++++++++++++++++------------- 1 file changed, 31 insertions(+), 13 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 3be747c..81d1179 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -18,11 +18,15 @@ open IO System structure SiteContext where root : String result : AnalyzerResult + currentName : Option Name + +def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} abbrev HtmlM := Reader SiteContext def getRoot : HtmlM String := do (←read).root def getResult : HtmlM AnalyzerResult := do (←read).result +def getCurrentName : HtmlM (Option Name) := do (←read).currentName def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base @@ -38,19 +42,32 @@ def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := parts := n.components.dropLast.map Name.toString def moduleListFile (file : Name) : HtmlM Html := do - + let attributes := match ←getCurrentName with + | some name => + if file == name then + #[("class", "nav_link"), ("visible", "")] + else + #[("class", "nav_link")] + | none => #[("class", "nav_link")] + let nodes := #[{file.toString}] + return Html.element "div" attributes nodes partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) let dirs := children.filter (λ c => c.getChildren.toList.length != 0) let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName - return
- {h.getName.toString} - [(←(dirs.mapM moduleListDir))] - [(←(files.mapM moduleListFile))] -
+ let dirNodes ← (dirs.mapM moduleListDir) + let fileNodes ← (files.mapM moduleListFile) + let attributes := match ←getCurrentName with + | some name => + if h.getName.isPrefixOf name then + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")] + else + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + | none => + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes + return Html.element "details" attributes nodes def moduleList : HtmlM (Array Html) := do let hierarchy := (←getResult).hierarchy @@ -129,14 +146,15 @@ def index : HtmlM Html := do templateExtends (baseHtml "Index") $ def styleCss : String := include_str "./static/style.css" -def moduleToHtml (module : Module) : HtmlM Html := do templateExtends (baseHtml module.name.toString) $ -
-

This is the page of {module.name.toString}

-
+def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do + templateExtends (baseHtml module.name.toString) $ +
+

This is the page of {module.name.toString}

+
def htmlOutput (result : AnalyzerResult) : IO Unit := do -- TODO: parameterize this - let config := { root := "/", result := result } + let config := { root := "/", result := result, currentName := none} let basePath := FilePath.mk "./build/doc/" let indexHtml := ReaderT.run index config let notFoundHtml := ReaderT.run notFound config From 551eeee09d340fa7de729aafa285db2ae30209a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 13 Dec 2021 21:36:21 +0100 Subject: [PATCH 34/50] feat: import nav.js Just a copy and paste + include in the template, it will most likely have to be modified in the future. --- DocGen4/Output.lean | 10 +- static/nav.js | 239 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 248 insertions(+), 1 deletion(-) create mode 100644 static/nav.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 81d1179..91ac120 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -125,8 +125,14 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do {site} {←navbar} - -- TODO Add the js stuff + -- Lean in JS in HTML in Lean...very meta + + + -- TODO Add more js stuff + @@ -145,6 +151,7 @@ def index : HtmlM Html := do templateExtends (baseHtml "Index") $ def styleCss : String := include_str "./static/style.css" +def navJs : String := include_str "./static/nav.js" def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do templateExtends (baseHtml module.name.toString) $ @@ -162,6 +169,7 @@ def htmlOutput (result : AnalyzerResult) : IO Unit := do FS.writeFile (basePath / "index.html") indexHtml.toString FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString + FS.writeFile (basePath / "nav.js") navJs for (module, content) in result.modules.toArray do let moduleHtml := ReaderT.run (moduleToHtml content) config let path := basePath / (nameToUrl module) diff --git a/static/nav.js b/static/nav.js new file mode 100644 index 0000000..fe1a170 --- /dev/null +++ b/static/nav.js @@ -0,0 +1,239 @@ +// Persistent expansion cookie for the file tree +// --------------------------------------------- + +let expanded = {}; +for (const e of (sessionStorage.getItem('expanded') || '').split(',')) { + if (e !== '') { + expanded[e] = true; + } +} + +function saveExpanded() { + sessionStorage.setItem("expanded", + Object.getOwnPropertyNames(expanded).filter((e) => expanded[e]).join(",")); +} + +for (const elem of document.getElementsByClassName('nav_sect')) { + const id = elem.getAttribute('data-path'); + if (!id) continue; + if (expanded[id]) { + elem.open = true; + } + elem.addEventListener('toggle', () => { + expanded[id] = elem.open; + saveExpanded(); + }); +} + +for (const currentFileLink of document.getElementsByClassName('visible')) { + currentFileLink.scrollIntoView({block: 'center'}); +} + + + + + + +// Tactic list tag filter +// ---------------------- + +function filterSelectionClass(tagNames, classname) { + if (tagNames.length == 0) { + for (const elem of document.getElementsByClassName(classname)) { + elem.classList.remove("hide"); + } + } else { + // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected + for (const elem of document.getElementsByClassName(classname)) { + elem.classList.add("hide"); + for (const tagName of tagNames) { + if (elem.classList.contains(tagName)) { + elem.classList.remove("hide"); + } + } + } + } + } + + function filterSelection(c) { + filterSelectionClass(c, "tactic"); + filterSelectionClass(c, "taclink"); + } + +var filterBoxes = document.getElementsByClassName("tagfilter"); + +function updateDisplay() { + filterSelection(getSelectValues()); +} + +function getSelectValues() { + var result = []; + + for (const opt of filterBoxes) { + + if (opt.checked) { + result.push(opt.value); + } + } + return result; + } + +function setSelectVal(val) { + for (const opt of filterBoxes) { + opt.checked = val; + } +} + +updateDisplay(); + +for (const opt of filterBoxes) { + opt.addEventListener('change', updateDisplay); +} + +const tse = document.getElementById("tagfilter-selectall") +if (tse != null) { + tse.addEventListener('change', function() { + setSelectVal(this.checked); + updateDisplay(); + }); +} + + + + + + +// Simple declaration search +// ------------------------- + +const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location); +const declSearch = (q) => new Promise((resolve, reject) => { + const worker = new SharedWorker(searchWorkerURL); + worker.port.start(); + worker.port.onmessage = ({data}) => resolve(data); + worker.port.onmessageerror = (e) => reject(e); + worker.port.postMessage({q}); +}); + +const srId = 'search_results'; +document.getElementById('search_form') + .appendChild(document.createElement('div')) + .id = srId; + +function handleSearchCursorUpDown(down) { + const sel = document.querySelector(`#${srId} .selected`); + const sr = document.getElementById(srId); + if (sel) { + sel.classList.remove('selected'); + const toSelect = down ? + sel.nextSibling || sr.firstChild: + sel.previousSibling || sr.lastChild; + toSelect && toSelect.classList.add('selected'); + } else { + const toSelect = down ? sr.firstChild : sr.lastChild; + toSelect && toSelect.classList.add('selected'); + } +} + +function handleSearchEnter() { + const sel = document.querySelector(`#${srId} .selected`) + || document.getElementById(srId).firstChild; + sel.click(); +} + +const searchInput = document.querySelector('#search_form input[name=q]'); + +searchInput.addEventListener('keydown', (ev) => { + switch (ev.key) { + case 'Down': + case 'ArrowDown': + ev.preventDefault(); + handleSearchCursorUpDown(true); + break; + case 'Up': + case 'ArrowUp': + ev.preventDefault(); + handleSearchCursorUpDown(false); + break; + case 'Enter': + ev.preventDefault(); + handleSearchEnter(); + break; + } +}); + +searchInput.addEventListener('input', async (ev) => { + const text = ev.target.value; + + if (!text) { + const sr = document.getElementById(srId); + sr.removeAttribute('state'); + sr.replaceWith(sr.cloneNode(false)); + return; + } + + document.getElementById(srId).setAttribute('state', 'loading'); + + const result = await declSearch(text); + if (ev.target.value != text) return; + + const oldSR = document.getElementById('search_results'); + const sr = oldSR.cloneNode(false); + for (const {decl} of result) { + const d = sr.appendChild(document.createElement('a')); + d.innerText = decl; + d.title = decl; + d.href = `${siteRoot}find/${decl}`; + } + sr.setAttribute('state', 'done'); + oldSR.replaceWith(sr); +}); + + + + + + +// 404 page goodies +// ---------------- + +const howabout = document.getElementById('howabout'); +if (howabout) { + howabout.innerText = "Please wait a second. I'll try to help you."; + + howabout.parentNode + .insertBefore(document.createElement('pre'), howabout) + .appendChild(document.createElement('code')) + .innerText = window.location.href.replace(/[/]/g, '/\u200b'); + + const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1]; + declSearch(query).then((results) => { + howabout.innerText = 'How about one of these instead:'; + const ul = howabout.appendChild(document.createElement('ul')); + for (const {decl} of results) { + const li = ul.appendChild(document.createElement('li')); + const a = li.appendChild(document.createElement('a')); + a.href = `${siteRoot}find/${decl}`; + a.appendChild(document.createElement('code')).innerText = decl; + } + }); +} + + + + + + +// Rewrite GitHub links +// -------------------- + +for (const elem of document.getElementsByClassName('gh_link')) { + const a = elem.firstElementChild; + // commit is set in add_commit.js + for (const [prefix, replacement] of commit) { + if (a.href.startsWith(prefix)) { + a.href = a.href.replace(prefix, replacement); + break; + } + } +} From 686f111438ec0dc2345799fc4110d5162f581303 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 09:24:49 +0100 Subject: [PATCH 35/50] chore: Split Output.lean into multiple files --- DocGen4/Output.lean | 155 ++--------------------------------- DocGen4/Output/Base.lean | 47 +++++++++++ DocGen4/Output/Index.lean | 22 +++++ DocGen4/Output/Module.lean | 21 +++++ DocGen4/Output/Navbar.lean | 70 ++++++++++++++++ DocGen4/Output/NotFound.lean | 22 +++++ DocGen4/Output/Template.lean | 57 +++++++++++++ 7 files changed, 244 insertions(+), 150 deletions(-) create mode 100644 DocGen4/Output/Base.lean create mode 100644 DocGen4/Output/Index.lean create mode 100644 DocGen4/Output/Module.lean create mode 100644 DocGen4/Output/Navbar.lean create mode 100644 DocGen4/Output/NotFound.lean create mode 100644 DocGen4/Output/Template.lean diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 91ac120..88ced36 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -4,160 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import Lean -import Std.Data.HashMap import DocGen4.Process -import DocGen4.ToHtmlFormat -import DocGen4.IncludeStr +import DocGen4.Output.Base +import DocGen4.Output.Index +import DocGen4.Output.Module +import DocGen4.Output.NotFound namespace DocGen4 -open Lean Std -open scoped DocGen4.Jsx -open IO System - -structure SiteContext where - root : String - result : AnalyzerResult - currentName : Option Name - -def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} - -abbrev HtmlM := Reader SiteContext - -def getRoot : HtmlM String := do (←read).root -def getResult : HtmlM AnalyzerResult := do (←read).result -def getCurrentName : HtmlM (Option Name) := do (←read).currentName - -def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := - new >>= base - -def nameToUrl (n : Name) : String := - (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" - where - parts := n.components.map Name.toString - -def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := - basePath / parts.foldl (λ acc p => acc / FilePath.mk p) (FilePath.mk ".") - where - parts := n.components.dropLast.map Name.toString - -def moduleListFile (file : Name) : HtmlM Html := do - let attributes := match ←getCurrentName with - | some name => - if file == name then - #[("class", "nav_link"), ("visible", "")] - else - #[("class", "nav_link")] - | none => #[("class", "nav_link")] - let nodes := #[{file.toString}] - return Html.element "div" attributes nodes - -partial def moduleListDir (h : Hierarchy) : HtmlM Html := do - let children := Array.mk (h.getChildren.toList.map Prod.snd) - let dirs := children.filter (λ c => c.getChildren.toList.length != 0) - let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName - let dirNodes ← (dirs.mapM moduleListDir) - let fileNodes ← (files.mapM moduleListFile) - let attributes := match ←getCurrentName with - | some name => - if h.getName.isPrefixOf name then - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")] - else - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] - | none => - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] - let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes - return Html.element "details" attributes nodes - -def moduleList : HtmlM (Array Html) := do - let hierarchy := (←getResult).hierarchy - let mut list := Array.empty - for (n, cs) in hierarchy.getChildren do - list := list.push

{n.toString}

- list := list.push $ ←moduleListDir cs - list - -def navbar : HtmlM Html := do - - -def baseHtml (title : String) (site : Html) : HtmlM Html := do - - - - - - {title} - - - - - - - - -
-

Documentation

-

{title}

- -- TODO: Replace this form with our own search -
- - - -
-
- - - - {site} - - {←navbar} - - -- Lean in JS in HTML in Lean...very meta - - - -- TODO Add more js stuff - - - - -def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ -
-

404 Not Found

-

Unfortunately, the page you were looking for is no longer here.

-
-
- -def index : HtmlM Html := do templateExtends (baseHtml "Index") $ -
- -

Welcome to the documentation page

- What is up? -
- -def styleCss : String := include_str "./static/style.css" -def navJs : String := include_str "./static/nav.js" - -def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do - templateExtends (baseHtml module.name.toString) $ -
-

This is the page of {module.name.toString}

-
+open Lean Std IO System Output def htmlOutput (result : AnalyzerResult) : IO Unit := do -- TODO: parameterize this diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean new file mode 100644 index 0000000..5f18ab0 --- /dev/null +++ b/DocGen4/Output/Base.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Lean +import DocGen4.Process +import DocGen4.IncludeStr + +namespace DocGen4 +namespace Output + +open Lean System + +structure SiteContext where + root : String + result : AnalyzerResult + currentName : Option Name + +def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} + +abbrev HtmlM := Reader SiteContext + +def getRoot : HtmlM String := do (←read).root +def getResult : HtmlM AnalyzerResult := do (←read).result +def getCurrentName : HtmlM (Option Name) := do (←read).currentName + +def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := + new >>= base + +def nameToUrl (n : Name) : String := + (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" + where + parts := n.components.map Name.toString + +def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := + basePath / parts.foldl (· / ·) (FilePath.mk ".") + where + parts := n.components.dropLast.map Name.toString + +section Static + def styleCss : String := include_str "./static/style.css" + def navJs : String := include_str "./static/nav.js" +end Static + +end Output +end DocGen4 diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean new file mode 100644 index 0000000..b09ac47 --- /dev/null +++ b/DocGen4/Output/Index.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def index : HtmlM Html := do templateExtends (baseHtml "Index") $ +
+ +

Welcome to the documentation page

+ What is up? +
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean new file mode 100644 index 0000000..44438b2 --- /dev/null +++ b/DocGen4/Output/Module.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do + templateExtends (baseHtml module.name.toString) $ +
+

This is the page of {module.name.toString}

+
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean new file mode 100644 index 0000000..1975a70 --- /dev/null +++ b/DocGen4/Output/Navbar.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Lean +import DocGen4.ToHtmlFormat +import DocGen4.Output.Base + +namespace DocGen4 +namespace Output + +open Lean +open scoped DocGen4.Jsx + +def moduleListFile (file : Name) : HtmlM Html := do + let attributes := match ←getCurrentName with + | some name => + if file == name then + #[("class", "nav_link"), ("visible", "")] + else + #[("class", "nav_link")] + | none => #[("class", "nav_link")] + let nodes := #[{file.toString}] + return Html.element "div" attributes nodes + +partial def moduleListDir (h : Hierarchy) : HtmlM Html := do + let children := Array.mk (h.getChildren.toList.map Prod.snd) + let dirs := children.filter (λ c => c.getChildren.toList.length != 0) + let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName + let dirNodes ← (dirs.mapM moduleListDir) + let fileNodes ← (files.mapM moduleListFile) + let attributes := match ←getCurrentName with + | some name => + if h.getName.isPrefixOf name then + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")] + else + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + | none => + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes + return Html.element "details" attributes nodes + +def moduleList : HtmlM (Array Html) := do + let hierarchy := (←getResult).hierarchy + let mut list := Array.empty + for (n, cs) in hierarchy.getChildren do + list := list.push

{n.toString}

+ list := list.push $ ←moduleListDir cs + list + +def navbar : HtmlM Html := do + + +end Output +end DocGen4 diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean new file mode 100644 index 0000000..ed5d547 --- /dev/null +++ b/DocGen4/Output/NotFound.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ +
+

404 Not Found

+

Unfortunately, the page you were looking for is no longer here.

+
+
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean new file mode 100644 index 0000000..5d82257 --- /dev/null +++ b/DocGen4/Output/Template.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Navbar + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def baseHtml (title : String) (site : Html) : HtmlM Html := do + + + + + + {title} + + + + + + + + +
+

Documentation

+

{title}

+ -- TODO: Replace this form with our own search +
+ + + +
+
+ + + + {site} + + {←navbar} + + -- Lean in JS in HTML in Lean...very meta + + + -- TODO Add more js stuff + + + + +end Output +end DocGen4 From dcd57e8c5f1bbe34ec5d1b13ee25bbb44dd21c49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 09:32:21 +0100 Subject: [PATCH 36/50] feat: Fix siteRoot in JS --- DocGen4/Output/Template.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 5d82257..0e28fc6 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -45,7 +45,7 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do -- Lean in JS in HTML in Lean...very meta -- TODO Add more js stuff From d5915fcb13e4e12e384686e849e315ee833a3a8b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 11:25:10 +0100 Subject: [PATCH 37/50] Revert "feat: Fix siteRoot in JS" This reverts commit dcd57e8c5f1bbe34ec5d1b13ee25bbb44dd21c49. --- DocGen4/Output/Template.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 0e28fc6..5d82257 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -45,7 +45,7 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do -- Lean in JS in HTML in Lean...very meta -- TODO Add more js stuff From 2adf5125c134a8804ad7d253cea4e1ef445a3d63 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 11:59:13 +0100 Subject: [PATCH 38/50] feat: Fix outputs paths --- DocGen4/Output.lean | 4 ++-- DocGen4/Output/Base.lean | 10 ++++++++-- DocGen4/Output/Navbar.lean | 8 ++++---- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 88ced36..ce81d2f 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -27,8 +27,8 @@ def htmlOutput (result : AnalyzerResult) : IO Unit := do FS.writeFile (basePath / "nav.js") navJs for (module, content) in result.modules.toArray do let moduleHtml := ReaderT.run (moduleToHtml content) config - let path := basePath / (nameToUrl module) - FS.createDirAll $ nameToDirectory basePath module + let path := moduleNameToFile basePath module + FS.createDirAll $ moduleNameToDirectory basePath module FS.writeFile path moduleHtml.toString end DocGen4 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 5f18ab0..2e4b07a 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -28,12 +28,18 @@ def getCurrentName : HtmlM (Option Name) := do (←read).currentName def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base -def nameToUrl (n : Name) : String := +-- TODO: Change this to HtmlM and auto add the root URl +def moduleNameToUrl (n : Name) : String := (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" where parts := n.components.map Name.toString -def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := +def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath := + FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html" + where + parts := n.components.map Name.toString + +def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := basePath / parts.foldl (· / ·) (FilePath.mk ".") where parts := n.components.dropLast.map Name.toString diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 1975a70..27da4c0 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -21,7 +21,7 @@ def moduleListFile (file : Name) : HtmlM Html := do else #[("class", "nav_link")] | none => #[("class", "nav_link")] - let nodes := #[{file.toString}] + let nodes := #[{file.toString}] return Html.element "div" attributes nodes partial def moduleListDir (h : Hierarchy) : HtmlM Html := do @@ -33,11 +33,11 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let attributes := match ←getCurrentName with | some name => if h.getName.isPrefixOf name then - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")] + #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName), ("open", "")] else - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)] | none => - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)] let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes return Html.element "details" attributes nodes From b019faf7baac87af7c8791db80ae4819360f8f0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 11:59:36 +0100 Subject: [PATCH 39/50] feat: An initial list of declarations and their kinds --- DocGen4/Output/Module.lean | 26 +++++++++++++++++++++++--- DocGen4/Process.lean | 20 ++++++++++++++++++++ 2 files changed, 43 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 44438b2..bb4ea87 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -11,11 +11,31 @@ namespace Output open scoped DocGen4.Jsx +-- TODO: This is a mix of decl.j2 and decl_header.j2, there is tons of stuff still missing +def docInfoToHtml (doc : DocInfo) : HtmlM Html := do +
+
+
+ -- TODO: Put the proper source link + source +
+ -- TODO: Attributes + -- TODO: Noncomputable, partial etc. + {doc.getKind} + -- TODO: HTMLify the name etc. + {doc.getName.toString} + -- TODO: args + -- TODO: The actual type information we are here for +
+
+ def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do + -- TODO: Probably some sort of ordering by line number would be cool? + -- maybe they should already be ordered in members. + let docInfos ← module.members.mapM docInfoToHtml + -- TODO: This is missing imports, imported by, source link, list of decls templateExtends (baseHtml module.name.toString) $ -
-

This is the page of {module.name.toString}

-
+ Html.element "main" #[] docInfos end Output end DocGen4 diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 950beac..b1bc9fc 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -256,6 +256,26 @@ def prettyPrint (i : DocInfo) : CoreM String := do let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo) s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" +def getName : DocInfo → Name +| axiomInfo i => i.name +| theoremInfo i => i.name +| opaqueInfo i => i.name +| definitionInfo i => i.name +| instanceInfo i => i.name +| inductiveInfo i => i.name +| structureInfo i => i.name +| classInfo i => i.name + +def getKind : DocInfo → String +| axiomInfo _ => "axiom" +| theoremInfo _ => "theorem" +| opaqueInfo _ => "constant" +| definitionInfo _ => "def" +| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet +| inductiveInfo _ => "inductive" +| structureInfo _ => "structure" +| classInfo _ => "class" -- TODO: This is handled as structure right now + end DocInfo namespace Module From cb582aab57b14a821e6e26a62c33365a03b725c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 12:02:05 +0100 Subject: [PATCH 40/50] feat: Some more progress logging --- DocGen4/Load.lean | 1 + Main.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 0767545..1dd0717 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -45,6 +45,7 @@ def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : def load (imports : List Name) : IO AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats + IO.println "Processing modules" let res ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {}) return res diff --git a/Main.lean b/Main.lean index cdae0ee..bc5c77a 100644 --- a/Main.lean +++ b/Main.lean @@ -8,4 +8,5 @@ def main (args : List String) : IO Unit := do let path ← lakeSetupSearchPath (←getLakePath) modules.toArray IO.println s!"Loading modules from: {path}" let doc ← load $ modules.map Name.mkSimple + IO.println "Outputting HTML" htmlOutput doc From dc5c2ab92a680361dd768e32d68e884c326a856c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 15:59:04 +0100 Subject: [PATCH 41/50] chore: Add an HtmlT if we need more monads later on --- DocGen4/Output/Base.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 2e4b07a..cb1d7b0 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -19,7 +19,8 @@ structure SiteContext where def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} -abbrev HtmlM := Reader SiteContext +abbrev HtmlT := ReaderT SiteContext +abbrev HtmlM := HtmlT Id def getRoot : HtmlM String := do (←read).root def getResult : HtmlM AnalyzerResult := do (←read).result From 03ec9c2e1dc736d502d4bf07cc0523572e9fc1cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 15:59:33 +0100 Subject: [PATCH 42/50] chore: Cleanup the JSX parser a bit --- DocGen4/ToHtmlFormat.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index 8afda02..4d6110b 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -52,7 +52,7 @@ open Parser PrettyPrinter declare_syntax_cat jsxElement declare_syntax_cat jsxChild -def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") <|> ("[" >> termParser >> "]") +def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") def jsxAttr : Parser := ident >> "=" >> jsxAttrVal -- JSXTextCharacter : SourceCharacter but not one of {, <, > or } From 2df4891c9f9cfff4581a613b4632cfb19b11149b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 15:59:43 +0100 Subject: [PATCH 43/50] feat: Setup infrastructure for type HTMLifying --- DocGen4/Output/Module.lean | 24 ++++++++++++----- DocGen4/Process.lean | 53 ++++++++++++++++++++------------------ 2 files changed, 46 insertions(+), 31 deletions(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index bb4ea87..4a9b8aa 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -3,6 +3,9 @@ Copyright (c) 2021 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +import Lean +import Lean.PrettyPrinter + import DocGen4.ToHtmlFormat import DocGen4.Output.Template @@ -10,8 +13,21 @@ namespace DocGen4 namespace Output open scoped DocGen4.Jsx +open Lean PrettyPrinter + +def docInfoHeader (doc : DocInfo) : HtmlM Html := do + let mut nodes := #[] + -- TODO: noncomputable, partial + -- TODO: Support all the kinds in CSS + nodes := nodes.push {doc.getKind} + -- TODO: HTMLify the name etc. + nodes := nodes.push doc.getName.toString + -- TODO: Figure out how we can get explicit, implicit and TC args and put them here + nodes := nodes.push : + nodes := nodes.push
Type!!!
+ -- TODO: The final type of the declaration + return
[nodes]
--- TODO: This is a mix of decl.j2 and decl_header.j2, there is tons of stuff still missing def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
@@ -20,11 +36,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do source
-- TODO: Attributes - -- TODO: Noncomputable, partial etc. - {doc.getKind} - -- TODO: HTMLify the name etc. - {doc.getName.toString} - -- TODO: args + {←docInfoHeader doc} -- TODO: The actual type information we are here for
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index b1bc9fc..0ed467c 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -15,33 +15,30 @@ namespace DocGen4 open Lean Meta PrettyPrinter Std +abbrev InfoSyntax := (Syntax × RBMap Delaborator.Pos Elab.Info compare) + structure NameInfo where name : Name - type : Syntax - deriving Repr + type : InfoSyntax def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do - s!"{i.name} : {←PrettyPrinter.formatTerm i.type}" + s!"{i.name} : {←PrettyPrinter.formatTerm i.type.fst}" structure Info extends NameInfo where doc : Option String declarationRange : DeclarationRange - deriving Repr structure AxiomInfo extends Info where isUnsafe : Bool - deriving Repr -structure TheoremInfo extends Info where - deriving Repr +structure TheoremInfo extends Info structure OpaqueInfo extends Info where - value : Syntax + value : InfoSyntax isUnsafe : Bool - deriving Repr structure DefinitionInfo extends Info where - --value : Syntax + --value : InfoSyntax unsafeInformation : DefinitionSafety hints : ReducibilityHints @@ -56,23 +53,19 @@ structure InductiveInfo extends Info where isUnsafe : Bool isReflexive : Bool isNested : Bool - deriving Repr structure FieldInfo extends NameInfo where projFn : Name subobject? : Option Name - deriving Repr structure StructureInfo extends Info where fieldInfo : Array FieldInfo parents : Array Name ctor : NameInfo - deriving Repr structure ClassInfo extends StructureInfo where hasOutParam : Bool - instances : Array Syntax - deriving Repr + instances : Array InfoSyntax inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo @@ -90,18 +83,18 @@ structure Module where members : Array DocInfo deriving Inhabited -def prettyPrintTerm (expr : Expr) : MetaM Syntax := do +def prettyPrintTerm (expr : Expr) : MetaM InfoSyntax := do let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr) - let term ← delab Name.anonymous [] expr - parenthesizeTerm term + let (stx, info) ← delabCore Name.anonymous [] expr + (←parenthesizeTerm stx, info) def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv - let type ← prettyPrintTerm v.type + let t ← prettyPrintTerm v.type let doc ← findDocString? env v.name match ←findDeclarationRanges? v.name with -- TODO: Maybe selection range is more relevant? Figure this out in the future - | some range => return Info.mk ⟨v.name, type⟩ doc range.range + | some range => return Info.mk ⟨v.name, t⟩ doc range.range | none => panic! s!"{v.name} is a declaration without position" def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do @@ -114,8 +107,8 @@ def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do let info ← Info.ofConstantVal v.toConstantVal - let value ← prettyPrintTerm v.value - return OpaqueInfo.mk info value v.isUnsafe + let t ← prettyPrintTerm v.value + return OpaqueInfo.mk info t v.isUnsafe def isInstance (declName : Name) : MetaM Bool := do (instanceExtension.getState (←getEnv)).instanceNames.contains declName @@ -126,7 +119,7 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := --let value ← prettyPrintTerm v.value return DefinitionInfo.mk info v.safety v.hints -def getConstructorType (ctor : Name) : MetaM Syntax := do +def getConstructorType (ctor : Name) : MetaM InfoSyntax := do let env ← getEnv match env.find? ctor with | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type @@ -249,10 +242,10 @@ def prettyPrint (i : DocInfo) : CoreM String := do s!"inductive {←i.toNameInfo.prettyPrint}, ctors: {ctorString}, doc string: {i.doc}" | structureInfo i => let ctorString ← i.ctor.prettyPrint - let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.name} : {←PrettyPrinter.formatTerm f.type}") + let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.name} : {←PrettyPrinter.formatTerm f.type.fst}") s!"structure {←i.toNameInfo.prettyPrint} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" | classInfo i => - let instanceString ← i.instances.mapM PrettyPrinter.formatTerm + let instanceString ← i.instances.mapM (PrettyPrinter.formatTerm ∘ Prod.fst) let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo) s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" @@ -276,6 +269,16 @@ def getKind : DocInfo → String | structureInfo _ => "structure" | classInfo _ => "class" -- TODO: This is handled as structure right now +def getType : DocInfo → InfoSyntax +| axiomInfo i => i.type +| theoremInfo i => i.type +| opaqueInfo i => i.type +| definitionInfo i => i.type +| instanceInfo i => i.type +| inductiveInfo i => i.type +| structureInfo i => i.type +| classInfo i => i.type + end DocInfo namespace Module From ef716c93515677247f93a082a5294cd2bb8c37a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 17:04:56 +0100 Subject: [PATCH 44/50] chore: Use builtin Name methods instead --- DocGen4/Hierarchy.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean index 205fec0..045581a 100644 --- a/DocGen4/Hierarchy.lean +++ b/DocGen4/Hierarchy.lean @@ -10,11 +10,6 @@ namespace DocGen4 open Lean Std Name -def getDepth : Name → Nat -| Name.anonymous => 0 -| Name.str p _ _ => getDepth p + 1 -| Name.num p _ _ => getDepth p + 1 - def getNLevels (name : Name) (levels: Nat) : Name := (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous where @@ -59,9 +54,9 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do let hn := h.getName let mut cs := h.getChildren - assert! getDepth hn ≤ getDepth n + assert! getNumParts hn ≤ getNumParts n - if getDepth hn + 1 == getDepth n then + if getNumParts hn + 1 == getNumParts n then match cs.find Name.cmp n with | none => node hn h.isFile (cs.insert Name.cmp n $ empty n true) @@ -70,7 +65,7 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do cs := cs.erase Name.cmp n node hn h.isFile (cs.insert Name.cmp n $ node n true ccs) else - let leveledName := getNLevels n (getDepth hn + 1) + let leveledName := getNLevels n (getNumParts hn + 1) match cs.find Name.cmp leveledName with | some nextLevel => cs := cs.erase Name.cmp leveledName From 3c01cf1e686c3c1efe25024c0ba6f4d35f464bfa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 17:20:44 +0100 Subject: [PATCH 45/50] feat: Name linking --- DocGen4/Output.lean | 2 +- DocGen4/Output/Base.lean | 7 +++---- DocGen4/Output/Module.lean | 14 ++++++++++++-- DocGen4/Output/Navbar.lean | 9 +++++---- DocGen4/Process.lean | 11 +++++++++-- 5 files changed, 30 insertions(+), 13 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index ce81d2f..b64b550 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -25,7 +25,7 @@ def htmlOutput (result : AnalyzerResult) : IO Unit := do FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString FS.writeFile (basePath / "nav.js") navJs - for (module, content) in result.modules.toArray do + for (module, content) in result.moduleInfo.toArray do let moduleHtml := ReaderT.run (moduleToHtml content) config let path := moduleNameToFile basePath module FS.createDirAll $ moduleNameToDirectory basePath module diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index cb1d7b0..92deae9 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -30,10 +30,9 @@ def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : H new >>= base -- TODO: Change this to HtmlM and auto add the root URl -def moduleNameToUrl (n : Name) : String := - (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" - where - parts := n.components.map Name.toString +def moduleNameToLink (n : Name) : HtmlM String := do + let parts := n.components.map Name.toString + (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath := FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html" diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 4a9b8aa..8bca416 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -15,13 +15,23 @@ namespace Output open scoped DocGen4.Jsx open Lean PrettyPrinter +def declNameToLink (name : Name) : HtmlM String := do + let res ← getResult + let module := res.moduleNames[res.name2ModIdx.find! name] + (←moduleNameToLink module) ++ "#" ++ name.toString + def docInfoHeader (doc : DocInfo) : HtmlM Html := do let mut nodes := #[] -- TODO: noncomputable, partial -- TODO: Support all the kinds in CSS nodes := nodes.push {doc.getKind} - -- TODO: HTMLify the name etc. - nodes := nodes.push doc.getName.toString + nodes := nodes.push + + + -- TODO: HTMLify the name + {doc.getName.toString} + + -- TODO: Figure out how we can get explicit, implicit and TC args and put them here nodes := nodes.push : nodes := nodes.push
Type!!!
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 27da4c0..c787279 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -21,7 +21,7 @@ def moduleListFile (file : Name) : HtmlM Html := do else #[("class", "nav_link")] | none => #[("class", "nav_link")] - let nodes := #[{file.toString}] + let nodes := #[{file.toString}] return Html.element "div" attributes nodes partial def moduleListDir (h : Hierarchy) : HtmlM Html := do @@ -30,14 +30,15 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName let dirNodes ← (dirs.mapM moduleListDir) let fileNodes ← (files.mapM moduleListFile) + let moduleLink ← moduleNameToLink h.getName let attributes := match ←getCurrentName with | some name => if h.getName.isPrefixOf name then - #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName), ("open", "")] + #[("class", "nav_sect"), ("data-path", moduleLink), ("open", "")] else - #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)] + #[("class", "nav_sect"), ("data-path", moduleLink)] | none => - #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)] + #[("class", "nav_sect"), ("data-path", moduleLink)] let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes return Html.element "details" attributes nodes diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 0ed467c..00321f0 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -290,7 +290,9 @@ def prettyPrint (m : Module) : CoreM String := do end Module structure AnalyzerResult where - modules : HashMap Name Module + name2ModIdx : HashMap Name ModuleIdx + moduleNames : Array Name + moduleInfo : HashMap Name Module hierarchy : Hierarchy deriving Inhabited @@ -318,6 +320,11 @@ def process : MetaM AnalyzerResult := do res := res.insert moduleName {module with members := module.members.push dinfo} | none => panic! "impossible" | none => () - return { modules := res, hierarchy := Hierarchy.fromArray env.header.moduleNames } + return { + name2ModIdx := env.const2ModIdx, + moduleNames := env.header.moduleNames, + moduleInfo := res, + hierarchy := Hierarchy.fromArray env.header.moduleNames + } end DocGen4 From 4380fe088d42dbeac27e4d0b2346d6abc247b823 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 23:53:06 +0100 Subject: [PATCH 46/50] feat: Sanitize Syntax --- DocGen4/Process.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 00321f0..51ec4ff 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -86,6 +86,7 @@ structure Module where def prettyPrintTerm (expr : Expr) : MetaM InfoSyntax := do let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr) let (stx, info) ← delabCore Name.anonymous [] expr + let stx := sanitizeSyntax stx |>.run' { options := ←getOptions } (←parenthesizeTerm stx, info) def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do From d18e71966c12006a93fdbf74aacfedfb0e561530 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 18 Dec 2021 00:01:31 +0100 Subject: [PATCH 47/50] feat: Store Format instead of Syntax in DocInfo --- DocGen4/Process.lean | 48 +++++++++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 51ec4ff..486d77b 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -15,14 +15,14 @@ namespace DocGen4 open Lean Meta PrettyPrinter Std -abbrev InfoSyntax := (Syntax × RBMap Delaborator.Pos Elab.Info compare) +abbrev InfoFormat := (Format × RBMap Delaborator.Pos Elab.Info compare) structure NameInfo where name : Name - type : InfoSyntax + type : InfoFormat -def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do - s!"{i.name} : {←PrettyPrinter.formatTerm i.type.fst}" +def NameInfo.prettyPrint (i : NameInfo) : String := + s!"{i.name} : {i.type.fst}" structure Info extends NameInfo where doc : Option String @@ -34,11 +34,11 @@ structure AxiomInfo extends Info where structure TheoremInfo extends Info structure OpaqueInfo extends Info where - value : InfoSyntax + value : InfoFormat isUnsafe : Bool structure DefinitionInfo extends Info where - --value : InfoSyntax + --value : InfoFormat unsafeInformation : DefinitionSafety hints : ReducibilityHints @@ -65,7 +65,7 @@ structure StructureInfo extends Info where structure ClassInfo extends StructureInfo where hasOutParam : Bool - instances : Array InfoSyntax + instances : Array InfoFormat inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo @@ -83,11 +83,13 @@ structure Module where members : Array DocInfo deriving Inhabited -def prettyPrintTerm (expr : Expr) : MetaM InfoSyntax := do +def prettyPrintTerm (expr : Expr) : MetaM InfoFormat := do let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr) let (stx, info) ← delabCore Name.anonymous [] expr let stx := sanitizeSyntax stx |>.run' { options := ←getOptions } - (←parenthesizeTerm stx, info) + let stx ← parenthesizeTerm stx + let fmt ← PrettyPrinter.formatTerm stx + (fmt, info) def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv @@ -120,7 +122,7 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := --let value ← prettyPrintTerm v.value return DefinitionInfo.mk info v.safety v.hints -def getConstructorType (ctor : Name) : MetaM InfoSyntax := do +def getConstructorType (ctor : Name) : MetaM InfoFormat := do let env ← getEnv match env.find? ctor with | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type @@ -233,22 +235,22 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, def prettyPrint (i : DocInfo) : CoreM String := do match i with - | axiomInfo i => s!"axiom {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | theoremInfo i => s!"theorem {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | opaqueInfo i => s!"constant {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | definitionInfo i => s!"def {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | instanceInfo i => s!"instance {←i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | axiomInfo i => s!"axiom {i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | theoremInfo i => s!"theorem {i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | opaqueInfo i => s!"constant {i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | definitionInfo i => s!"def {i.toNameInfo.prettyPrint}, doc string: {i.doc}" + | instanceInfo i => s!"instance {i.toNameInfo.prettyPrint}, doc string: {i.doc}" | inductiveInfo i => - let ctorString ← i.ctors.mapM NameInfo.prettyPrint + let ctorString := i.ctors.map NameInfo.prettyPrint s!"inductive {←i.toNameInfo.prettyPrint}, ctors: {ctorString}, doc string: {i.doc}" | structureInfo i => - let ctorString ← i.ctor.prettyPrint - let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.name} : {←PrettyPrinter.formatTerm f.type.fst}") - s!"structure {←i.toNameInfo.prettyPrint} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" + let ctorString := i.ctor.prettyPrint + let fieldString := i.fieldInfo.map (λ f => s!"{f.name} : {f.type.fst}") + s!"structure {i.toNameInfo.prettyPrint} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" | classInfo i => - let instanceString ← i.instances.mapM (PrettyPrinter.formatTerm ∘ Prod.fst) - let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo) - s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" + let instanceString := i.instances.map Prod.fst + let fieldString := i.fieldInfo.map (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo) + s!"class {i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" def getName : DocInfo → Name | axiomInfo i => i.name @@ -270,7 +272,7 @@ def getKind : DocInfo → String | structureInfo _ => "structure" | classInfo _ => "class" -- TODO: This is handled as structure right now -def getType : DocInfo → InfoSyntax +def getType : DocInfo → InfoFormat | axiomInfo i => i.type | theoremInfo i => i.type | opaqueInfo i => i.type From 0efbcd1f60596c0d0235fe0b224ebbdc1a9ce798 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 25 Dec 2021 14:04:35 +0100 Subject: [PATCH 48/50] feat: Newline free HTML formatting Some of the HTML elements we are generating are newline sensitive which requires the HTML to String formatter to optionally omit additional newlines. --- DocGen4/Output/Navbar.lean | 4 ++-- DocGen4/ToHtmlFormat.lean | 15 ++++++++------- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index c787279..6a2e07a 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -22,7 +22,7 @@ def moduleListFile (file : Name) : HtmlM Html := do #[("class", "nav_link")] | none => #[("class", "nav_link")] let nodes := #[{file.toString}] - return Html.element "div" attributes nodes + return Html.element "div" false attributes nodes partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) @@ -40,7 +40,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do | none => #[("class", "nav_sect"), ("data-path", moduleLink)] let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes - return Html.element "details" attributes nodes + return Html.element "details" false attributes nodes def moduleList : HtmlM (Array Html) := do let hierarchy := (←getResult).hierarchy diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index 4d6110b..e0fbfaf 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -18,8 +18,8 @@ open Lean inductive Html where -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson - -- element (tag : String) (attrs : Array HtmlAttribute) (children : Array Html) - | element : String → Array (String × String) → Array Html → Html + -- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html) + | element : String → Bool → Array (String × String) → Array Html → Html | text : String → Html deriving Repr, BEq, Inhabited, FromJson, ToJson @@ -33,9 +33,10 @@ def attributesToString (attrs : Array (String × String)) :String := -- TODO: Termination proof partial def toStringAux : Html → String -| element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" -| element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" -| element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" +| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" +| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" +| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" +| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" | text s => s def toString (html : Html) : String := @@ -83,7 +84,7 @@ macro_rules | `(jsxAttrVal| $s:strLit) => s | `(jsxAttrVal| { $t:term }) => t | _ => unreachable! - `(Html.element $(quote <| toString n.getId) #[ $[($ns, $vs)],* ] #[]) + `(Html.element $(quote <| toString n.getId) false #[ $[($ns, $vs)],* ] #[]) | `(<$n $[$ns = $vs]* >$cs*) => if n.getId == m.getId then do let ns := ns.map (quote <| toString ·.getId) @@ -99,7 +100,7 @@ macro_rules | `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement]) | _ => unreachable! let tag := toString n.getId - `(Html.element $(quote tag) #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ])) + `(Html.element $(quote tag) false #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ])) else Macro.throwError ("expected ") end Jsx From 5e0956c4b03881fc50661324bbf2b8095c666775 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 25 Dec 2021 14:08:09 +0100 Subject: [PATCH 49/50] feat: Proper linking of all constants Previously constants in function applications where either not linked at all or linked in a weird way, this change fixes it by making use of a (as of now umerged) compiler modification as well as Lean.Widget's TaggedText. --- DocGen4/Load.lean | 3 +- DocGen4/Output/Module.lean | 35 ++++++++++++++++-- DocGen4/Process.lean | 76 +++++++++++++++----------------------- lean-toolchain | 2 +- 4 files changed, 64 insertions(+), 52 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 1dd0717..5f23a57 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -46,7 +46,6 @@ def load (imports : List Name) : IO AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats IO.println "Processing modules" - let res ← Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000} { env := env} {} {}) - return res + Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}) end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 8bca416..460439e 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -5,6 +5,7 @@ Authors: Henrik Böving -/ import Lean import Lean.PrettyPrinter +import Lean.Widget.TaggedText import DocGen4.ToHtmlFormat import DocGen4.Output.Template @@ -13,13 +14,41 @@ namespace DocGen4 namespace Output open scoped DocGen4.Jsx -open Lean PrettyPrinter +open Lean PrettyPrinter Widget Elab def declNameToLink (name : Name) : HtmlM String := do let res ← getResult let module := res.moduleNames[res.name2ModIdx.find! name] (←moduleNameToLink module) ++ "#" ++ name.toString +def splitWhitespaces (s : String) : (String × String × String) := Id.run do + let front := "".pushn ' ' (s.find (!Char.isWhitespace ·)) + let mut s := s.trimLeft + let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace)) + s:= s.trimRight + (front, s, back) + +partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do + match i with + | TaggedText.text t => return #[t] + | TaggedText.append tt => tt.foldlM (λ acc t => do acc ++ (←infoFormatToHtml t)) #[] + | TaggedText.tag a t => + match a.info.val.info with + | Info.ofTermInfo i => + match i.expr.consumeMData with + | Expr.const name _ _ => + match t with + | TaggedText.text t => + let (front, t, back) := splitWhitespaces t + let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t] + #[Html.text front, elem, Html.text back] + | _ => + -- TODO: Is this ever reachable? + #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)] + | _ => + #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] + | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] + def docInfoHeader (doc : DocInfo) : HtmlM Html := do let mut nodes := #[] -- TODO: noncomputable, partial @@ -34,7 +63,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do -- TODO: Figure out how we can get explicit, implicit and TC args and put them here nodes := nodes.push : - nodes := nodes.push
Type!!!
+ nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) -- TODO: The final type of the declaration return
[nodes]
@@ -57,7 +86,7 @@ def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName mo let docInfos ← module.members.mapM docInfoToHtml -- TODO: This is missing imports, imported by, source link, list of decls templateExtends (baseHtml module.name.toString) $ - Html.element "main" #[] docInfos + Html.element "main" false #[] docInfos end Output end DocGen4 diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 486d77b..91d6693 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -13,34 +13,35 @@ import DocGen4.Hierarchy namespace DocGen4 -open Lean Meta PrettyPrinter Std - -abbrev InfoFormat := (Format × RBMap Delaborator.Pos Elab.Info compare) +open Lean Meta PrettyPrinter Std Widget structure NameInfo where name : Name - type : InfoFormat - -def NameInfo.prettyPrint (i : NameInfo) : String := - s!"{i.name} : {i.type.fst}" + type : CodeWithInfos + deriving Inhabited structure Info extends NameInfo where doc : Option String declarationRange : DeclarationRange + deriving Inhabited structure AxiomInfo extends Info where isUnsafe : Bool + deriving Inhabited structure TheoremInfo extends Info + deriving Inhabited structure OpaqueInfo extends Info where - value : InfoFormat + value : CodeWithInfos isUnsafe : Bool + deriving Inhabited structure DefinitionInfo extends Info where - --value : InfoFormat + --value : CodeWithInfos unsafeInformation : DefinitionSafety hints : ReducibilityHints + deriving Inhabited abbrev InstanceInfo := DefinitionInfo @@ -53,19 +54,23 @@ structure InductiveInfo extends Info where isUnsafe : Bool isReflexive : Bool isNested : Bool + deriving Inhabited structure FieldInfo extends NameInfo where projFn : Name subobject? : Option Name + deriving Inhabited structure StructureInfo extends Info where fieldInfo : Array FieldInfo parents : Array Name ctor : NameInfo + deriving Inhabited structure ClassInfo extends StructureInfo where hasOutParam : Bool - instances : Array InfoFormat + instances : Array CodeWithInfos + deriving Inhabited inductive DocInfo where | axiomInfo (info : AxiomInfo) : DocInfo @@ -76,6 +81,7 @@ inductive DocInfo where | inductiveInfo (info : InductiveInfo) : DocInfo | structureInfo (info : StructureInfo) : DocInfo | classInfo (info : ClassInfo) : DocInfo + deriving Inhabited structure Module where name : Name @@ -83,13 +89,18 @@ structure Module where members : Array DocInfo deriving Inhabited -def prettyPrintTerm (expr : Expr) : MetaM InfoFormat := do - let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr) - let (stx, info) ← delabCore Name.anonymous [] expr - let stx := sanitizeSyntax stx |>.run' { options := ←getOptions } - let stx ← parenthesizeTerm stx - let fmt ← PrettyPrinter.formatTerm stx - (fmt, info) +def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do + let (fmt, infos) ← formatInfos expr + let tt := TaggedText.prettyTagged fmt + let ctx := { + env := ← getEnv + mctx := ← getMCtx + options := ← getOptions + currNamespace := ← getCurrNamespace + openDecls := ← getOpenDecls + fileMap := arbitrary + } + tagExprInfos ctx infos tt def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv @@ -122,7 +133,7 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := --let value ← prettyPrintTerm v.value return DefinitionInfo.mk info v.safety v.hints -def getConstructorType (ctor : Name) : MetaM InfoFormat := do +def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do let env ← getEnv match env.find? ctor with | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type @@ -233,25 +244,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, | ConstantInfo.recInfo i => none | ConstantInfo.quotInfo i => none -def prettyPrint (i : DocInfo) : CoreM String := do - match i with - | axiomInfo i => s!"axiom {i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | theoremInfo i => s!"theorem {i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | opaqueInfo i => s!"constant {i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | definitionInfo i => s!"def {i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | instanceInfo i => s!"instance {i.toNameInfo.prettyPrint}, doc string: {i.doc}" - | inductiveInfo i => - let ctorString := i.ctors.map NameInfo.prettyPrint - s!"inductive {←i.toNameInfo.prettyPrint}, ctors: {ctorString}, doc string: {i.doc}" - | structureInfo i => - let ctorString := i.ctor.prettyPrint - let fieldString := i.fieldInfo.map (λ f => s!"{f.name} : {f.type.fst}") - s!"structure {i.toNameInfo.prettyPrint} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}" - | classInfo i => - let instanceString := i.instances.map Prod.fst - let fieldString := i.fieldInfo.map (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo) - s!"class {i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}" - def getName : DocInfo → Name | axiomInfo i => i.name | theoremInfo i => i.name @@ -272,7 +264,7 @@ def getKind : DocInfo → String | structureInfo _ => "structure" | classInfo _ => "class" -- TODO: This is handled as structure right now -def getType : DocInfo → InfoFormat +def getType : DocInfo → CodeWithInfos | axiomInfo i => i.type | theoremInfo i => i.type | opaqueInfo i => i.type @@ -284,14 +276,6 @@ def getType : DocInfo → InfoFormat end DocInfo -namespace Module - -def prettyPrint (m : Module) : CoreM String := do - let pretty := s!"Module {m.name}, doc string: {m.doc} with members:\n" - Array.foldlM (λ p mem => return p ++ " " ++ (←mem.prettyPrint) ++ "\n") pretty m.members - -end Module - structure AnalyzerResult where name2ModIdx : HashMap Name ModuleIdx moduleNames : Array Name diff --git a/lean-toolchain b/lean-toolchain index 8b6c918..dcca6df 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2021-12-12 +lean4 From 02d8c528d96d3b23430767d2cf660fa556f78ed7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 25 Dec 2021 16:55:30 +0100 Subject: [PATCH 50/50] feat: Show arguments of types of decls separately --- DocGen4/Output/Module.lean | 21 ++++++++++++++++++++- DocGen4/Process.lean | 36 ++++++++++++++++++++++++++++++++++-- 2 files changed, 54 insertions(+), 3 deletions(-) diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 460439e..b467935 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -49,6 +49,24 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] +def argToHtml (arg : Arg) : HtmlM Html := do + let (l, r, implicit) := match arg.binderInfo with + | BinderInfo.default => ("(", ")", false) + | BinderInfo.implicit => ("{", "}", true) + | BinderInfo.strictImplicit => ("⦃", "⦄", true) + | BinderInfo.instImplicit => ("[", "]", true) + -- TODO: Can this ever be reached here? What does it mean? + | BinderInfo.auxDecl => unreachable! + let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "] + nodes := nodes.append (←infoFormatToHtml arg.type) + nodes := nodes.push r + let inner := Html.element "span" true #[("class", "fn")] nodes + let html := Html.element "span" false #[("class", "decl_args")] #[inner] + if implicit then + {html} + else + html + def docInfoHeader (doc : DocInfo) : HtmlM Html := do let mut nodes := #[] -- TODO: noncomputable, partial @@ -61,7 +79,8 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do {doc.getName.toString} - -- TODO: Figure out how we can get explicit, implicit and TC args and put them here + for arg in doc.getArgs do + nodes := nodes.push (←argToHtml arg) nodes := nodes.push : nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) -- TODO: The final type of the declaration diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 91d6693..7de63ac 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -20,7 +20,13 @@ structure NameInfo where type : CodeWithInfos deriving Inhabited +structure Arg where + name : Name + type : CodeWithInfos + binderInfo : BinderInfo + structure Info extends NameInfo where + args : Array Arg doc : Option String declarationRange : DeclarationRange deriving Inhabited @@ -89,6 +95,20 @@ structure Module where members : Array DocInfo deriving Inhabited +partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) := + match e.consumeMData with + | Expr.lam name type body data => + let name := name.eraseMacroScopes + let arg := (name, type, data.binderInfo) + let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) + (#[arg] ++ args, final) + | Expr.forallE name type body data => + let name := name.eraseMacroScopes + let arg := (name, type, data.binderInfo) + let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) + (#[arg] ++ args, final) + | _ => (#[], e) + def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do let (fmt, infos) ← formatInfos expr let tt := TaggedText.prettyTagged fmt @@ -104,11 +124,13 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv - let t ← prettyPrintTerm v.type + let (args, type) := typeToArgsType v.type + let type ← prettyPrintTerm type + let args ← args.mapM (λ (n, e, b) => do Arg.mk n (←prettyPrintTerm e) b) let doc ← findDocString? env v.name match ←findDeclarationRanges? v.name with -- TODO: Maybe selection range is more relevant? Figure this out in the future - | some range => return Info.mk ⟨v.name, t⟩ doc range.range + | some range => return Info.mk ⟨v.name, type⟩ args doc range.range | none => panic! s!"{v.name} is a declaration without position" def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do @@ -274,6 +296,16 @@ def getType : DocInfo → CodeWithInfos | structureInfo i => i.type | classInfo i => i.type +def getArgs : DocInfo → Array Arg +| axiomInfo i => i.args +| theoremInfo i => i.args +| opaqueInfo i => i.args +| definitionInfo i => i.args +| instanceInfo i => i.args +| inductiveInfo i => i.args +| structureInfo i => i.args +| classInfo i => i.args + end DocInfo structure AnalyzerResult where