From 2dac93d360bb3f2c0205c3fa4b58831ce76cce3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 17 Feb 2022 18:59:42 +0100 Subject: [PATCH] fix: fix noncomputable Also address the changes made to module doc until doc strings are implemented. --- DocGen4/Process.lean | 26 ++++++++++---------------- lean-toolchain | 2 +- 2 files changed, 11 insertions(+), 17 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 17f981c..11905f2 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -52,7 +52,7 @@ structure DefinitionInfo extends Info where isUnsafe : Bool hints : ReducibilityHints equations : Option (Array CodeWithInfos) - isComputable : Bool + isNonComputable : Bool deriving Inhabited abbrev InstanceInfo := DefinitionInfo @@ -202,30 +202,22 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do let type ← mkForallFVars xs type pure type --- The following code is translated from ll_infer_type.cpp -def computable? (defn : Name) : MetaM Bool := do - let cstage2Name := defn.append `_cstage2 - let env ← getEnv - let extern? := externAttr.getParam env defn |>.isSome - let cstage2? := env.find? cstage2Name |>.isSome - pure $ extern? ∨ cstage2? - def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do let info ← Info.ofConstantVal v.toConstantVal let isUnsafe := v.safety == DefinitionSafety.unsafe - let isComputable ← computable? v.name + let isNonComput := isNoncomputable (←getEnv) v.name try let eqs? ← getEqnsFor? v.name match eqs? with | some eqs => let prettyEqs ← eqs.mapM processEq - pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isComputable + pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput | none => let eq ← prettyPrintTerm $ stripArgs (←valueToEq v) - pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isComputable + pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput catch err => IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}" - pure $ DefinitionInfo.mk info isUnsafe v.hints none isComputable + pure $ DefinitionInfo.mk info isUnsafe v.hints none isNonComput def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do let info ← DefinitionInfo.ofDefinitionVal v @@ -394,7 +386,7 @@ def getKindDescription : DocInfo → String let mut modifiers := #[] if i.isUnsafe then modifiers := modifiers.push "unsafe" - if ¬i.isComputable then + if i.isNonComputable then modifiers := modifiers.push "noncomputable" modifiers := modifiers.push "def" @@ -403,7 +395,7 @@ def getKindDescription : DocInfo → String let mut modifiers := #[] if i.isUnsafe then modifiers := modifiers.push "unsafe" - if ¬i.isComputable then + if i.isNonComputable then modifiers := modifiers.push "noncomputable" modifiers := modifiers.push "instance" @@ -468,6 +460,8 @@ structure AnalyzerResult where importAdj : Array (Array Bool) deriving Inhabited +deriving instance Inhabited for ModuleDoc + def process : MetaM AnalyzerResult := do let env ← getEnv let mut res := mkHashMap env.header.moduleNames.size @@ -476,7 +470,7 @@ def process : MetaM AnalyzerResult := do let moduleDoc := match getModuleDoc? env module with | none => none | some #[] => none - | some doc => doc.get! 0 + | some doc => (doc.get! 0).doc res := res.insert module (Module.mk module moduleDoc #[]) diff --git a/lean-toolchain b/lean-toolchain index 4b598af..7c2b6c2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-11 +leanprover/lean4:nightly-2022-02-17