r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

chore: Fill universe MVars and remove out of date TODOs

main
Henrik Böving 2021-12-04 23:33:21 +01:00
parent 82c78d29bd
commit b60eca730f
1 changed files with 1 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
DocGen4/Process.lean
View File

@ -48,7 +48,6 @@ structure FieldInfo extends StructureFieldInfo where
deriving Repr deriving Repr
structure StructureInfo extends Info where structure StructureInfo extends Info where
-- TODO: Later on we probably also want the type of projection fns etc.
fieldInfo : Array FieldInfo fieldInfo : Array FieldInfo
parents : Array Name parents : Array Name
ctor : (Name × Syntax) ctor : (Name × Syntax)
@ -75,6 +74,7 @@ structure Module where
deriving Inhabited deriving Inhabited
def prettyPrintTerm (expr : Expr) : MetaM Syntax := do def prettyPrintTerm (expr : Expr) : MetaM Syntax := do
let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr)
let term ← delab Name.anonymous [] expr let term ← delab Name.anonymous [] expr
parenthesizeTerm term parenthesizeTerm term
@ -124,7 +124,6 @@ def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) :=
| Expr.forallE n _ b .. => getFieldTypeAux b (n :: vars) | Expr.forallE n _ b .. => getFieldTypeAux b (n :: vars)
| _ => (type, vars) | _ => (type, vars)
-- TODO: Fill universes
def getFieldType (projFn : Name) : MetaM Expr := do def getFieldType (projFn : Name) : MetaM Expr := do
let fn ← mkConstWithFreshMVarLevels projFn let fn ← mkConstWithFreshMVarLevels projFn
let type ← inferType fn 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.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i)
| ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i) | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
-- TODO: Find a way to extract equations nicely -- 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 => | ConstantInfo.defnInfo i =>
if ← (isProjFn i.name) then if ← (isProjFn i.name) then
none none
@ -213,7 +210,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
| ConstantInfo.recInfo i => none | ConstantInfo.recInfo i => none
| ConstantInfo.quotInfo i => none | ConstantInfo.quotInfo i => none
def prettyPrint (i : DocInfo) : CoreM String := do def prettyPrint (i : DocInfo) : CoreM String := do
match i with match i with
| axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}" | axiomInfo i => s!"axiom {i.name} : {←PrettyPrinter.formatTerm i.type}, doc string: {i.doc}"