feat: tag declarations with unsafe and partial
parent
4490b1e674
commit
c2d18fe3b1
|
@ -49,9 +49,7 @@ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
|
||||||
|
|
||||||
def docInfoHeader (doc : DocInfo) : HtmlM Html := do
|
def docInfoHeader (doc : DocInfo) : HtmlM Html := do
|
||||||
let mut nodes := #[]
|
let mut nodes := #[]
|
||||||
-- TODO: noncomputable, partial
|
nodes := nodes.push <span «class»="decl_kind">{doc.getKindDescription}</span>
|
||||||
-- TODO: Support all the kinds in CSS
|
|
||||||
nodes := nodes.push <span «class»="decl_kind">{doc.getKind}</span>
|
|
||||||
nodes := nodes.push
|
nodes := nodes.push
|
||||||
<span «class»="decl_name">
|
<span «class»="decl_name">
|
||||||
<a «class»="break_within" href={←declNameToLink doc.getName}>
|
<a «class»="break_within" href={←declNameToLink doc.getName}>
|
||||||
|
@ -84,7 +82,6 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
|
||||||
return <div «class»="decl" id={doc.getName.toString}>
|
return <div «class»="decl" id={doc.getName.toString}>
|
||||||
<div «class»={doc.getKind}>
|
<div «class»={doc.getKind}>
|
||||||
<div «class»="gh_link">
|
<div «class»="gh_link">
|
||||||
-- TODO: Put the proper source link
|
|
||||||
<a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
|
<a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
|
||||||
</div>
|
</div>
|
||||||
-- TODO: Attributes
|
-- TODO: Attributes
|
||||||
|
@ -134,7 +131,6 @@ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
|
||||||
def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
|
def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
|
||||||
<nav «class»="internal_nav">
|
<nav «class»="internal_nav">
|
||||||
<h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
|
<h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
|
||||||
-- TODO: Proper source links
|
|
||||||
<p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
|
<p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
|
||||||
<div «class»="imports">
|
<div «class»="imports">
|
||||||
<details>
|
<details>
|
||||||
|
|
|
@ -40,12 +40,14 @@ structure TheoremInfo extends Info
|
||||||
|
|
||||||
structure OpaqueInfo extends Info where
|
structure OpaqueInfo extends Info where
|
||||||
value : CodeWithInfos
|
value : CodeWithInfos
|
||||||
isUnsafe : Bool
|
-- A value of partial is interpreted as this constant being part of a partial def
|
||||||
|
-- since the actual definition for a partial def is hidden behind an inaccessible value
|
||||||
|
unsafeInformation : DefinitionSafety
|
||||||
deriving Inhabited
|
deriving Inhabited
|
||||||
|
|
||||||
structure DefinitionInfo extends Info where
|
structure DefinitionInfo extends Info where
|
||||||
--value : CodeWithInfos
|
-- partial defs are handled by OpaqueInfo
|
||||||
unsafeInformation : DefinitionSafety
|
isUnsafe : Bool
|
||||||
hints : ReducibilityHints
|
hints : ReducibilityHints
|
||||||
equations : Option (Array CodeWithInfos)
|
equations : Option (Array CodeWithInfos)
|
||||||
deriving Inhabited
|
deriving Inhabited
|
||||||
|
@ -156,12 +158,17 @@ def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
|
||||||
def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
|
def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
|
||||||
let info ← Info.ofConstantVal v.toConstantVal
|
let info ← Info.ofConstantVal v.toConstantVal
|
||||||
let t ← prettyPrintTerm v.value
|
let t ← prettyPrintTerm v.value
|
||||||
return OpaqueInfo.mk info t v.isUnsafe
|
let env ← getEnv
|
||||||
|
let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
|
||||||
|
if isPartial then
|
||||||
|
return OpaqueInfo.mk info t DefinitionSafety.partial
|
||||||
|
else
|
||||||
|
let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
|
||||||
|
return OpaqueInfo.mk info t safety
|
||||||
|
|
||||||
def isInstance (declName : Name) : MetaM Bool := do
|
def isInstance (declName : Name) : MetaM Bool := do
|
||||||
(instanceExtension.getState (←getEnv)).instanceNames.contains declName
|
(instanceExtension.getState (←getEnv)).instanceNames.contains declName
|
||||||
|
|
||||||
|
|
||||||
partial def stripArgs (e : Expr) : Expr :=
|
partial def stripArgs (e : Expr) : Expr :=
|
||||||
match e.consumeMData with
|
match e.consumeMData with
|
||||||
| Expr.lam name type body data =>
|
| Expr.lam name type body data =>
|
||||||
|
@ -188,18 +195,19 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
|
||||||
|
|
||||||
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
|
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
|
||||||
let info ← Info.ofConstantVal v.toConstantVal
|
let info ← Info.ofConstantVal v.toConstantVal
|
||||||
|
let isUnsafe := v.safety == DefinitionSafety.unsafe
|
||||||
try
|
try
|
||||||
let eqs? ← getEqnsFor? v.name
|
let eqs? ← getEqnsFor? v.name
|
||||||
match eqs? with
|
match eqs? with
|
||||||
| some eqs =>
|
| some eqs =>
|
||||||
let prettyEqs ← eqs.mapM processEq
|
let prettyEqs ← eqs.mapM processEq
|
||||||
DefinitionInfo.mk info v.safety v.hints prettyEqs
|
DefinitionInfo.mk info isUnsafe v.hints prettyEqs
|
||||||
| none =>
|
| none =>
|
||||||
let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
|
let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
|
||||||
DefinitionInfo.mk info v.safety v.hints (some #[eq])
|
DefinitionInfo.mk info isUnsafe v.hints (some #[eq])
|
||||||
catch err =>
|
catch err =>
|
||||||
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
|
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
|
||||||
return DefinitionInfo.mk info v.safety v.hints none
|
return DefinitionInfo.mk info isUnsafe v.hints none
|
||||||
|
|
||||||
def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
|
def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
|
||||||
let env ← getEnv
|
let env ← getEnv
|
||||||
|
@ -327,10 +335,25 @@ def getKind : DocInfo → String
|
||||||
| theoremInfo _ => "theorem"
|
| theoremInfo _ => "theorem"
|
||||||
| opaqueInfo _ => "constant"
|
| opaqueInfo _ => "constant"
|
||||||
| definitionInfo _ => "def"
|
| definitionInfo _ => "def"
|
||||||
| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet
|
| instanceInfo _ => "instance"
|
||||||
| inductiveInfo _ => "inductive"
|
| inductiveInfo _ => "inductive"
|
||||||
| structureInfo _ => "structure"
|
| structureInfo _ => "structure"
|
||||||
| classInfo _ => "class" -- TODO: This is handled as structure right now
|
| classInfo _ => "class"
|
||||||
|
|
||||||
|
open DefinitionSafety in
|
||||||
|
def getKindDescription : DocInfo → String
|
||||||
|
| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
|
||||||
|
| theoremInfo _ => "theorem"
|
||||||
|
| opaqueInfo i =>
|
||||||
|
match i.unsafeInformation with
|
||||||
|
| safe => "constant"
|
||||||
|
| «unsafe» => "unsafe constant"
|
||||||
|
| «partial» => "partial def"
|
||||||
|
| definitionInfo i => if i.isUnsafe then "unsafe def" else "def"
|
||||||
|
| instanceInfo i => if i.isUnsafe then "unsafe instance" else "instance"
|
||||||
|
| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
|
||||||
|
| structureInfo _ => "structure"
|
||||||
|
| classInfo _ => "class"
|
||||||
|
|
||||||
def getType : DocInfo → CodeWithInfos
|
def getType : DocInfo → CodeWithInfos
|
||||||
| axiomInfo i => i.type
|
| axiomInfo i => i.type
|
||||||
|
|
Loading…
Reference in New Issue