From 4e8f4fcaefd38d65fb45d29b67284fbba7213b55 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 21 Oct 2020 10:57:58 +0200 Subject: [PATCH] refactor: extract `AttributeImplCore`, introduce `ParametricAttributeImpl` --- src/Lean/Attributes.lean | 35 ++++++++++++----------- src/Lean/Compiler/ExportAttr.lean | 16 +++++++---- src/Lean/Compiler/ExternAttr.lean | 11 +++++--- src/Lean/Compiler/ImplementedByAttr.lean | 23 ++++++++------- src/Lean/Compiler/InitAttr.lean | 36 +++++++++++++----------- src/Lean/Meta/RecursorInfo.lean | 13 +++++---- 6 files changed, 77 insertions(+), 57 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index a922d4137b..4bc16566c8 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -36,11 +36,15 @@ instance : MonadResolveName AttrM := { -- TODO: after we delete the old frontend, we should use `EIO` with a richer exception kind at AttributeImpl. -- We must perform a similar modification at `PersistentEnvExtension` -structure AttributeImpl := +structure AttributeImplCore := (name : Name) (descr : String) + (applicationTime := AttributeApplicationTime.afterTypeChecking) + +structure AttributeImpl extends AttributeImplCore := (add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit) - (applicationTime : AttributeApplicationTime := AttributeApplicationTime.afterTypeChecking) + -- TODO: shouldn't be necessary + (applicationTime := AttributeApplicationTime.afterTypeChecking) instance : Inhabited AttributeImpl := ⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩ @@ -315,13 +319,15 @@ structure ParametricAttribute (α : Type) := (attr : AttributeImpl) (ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)) -def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String) - (getParam : Name → Syntax → AttrM α) - (afterSet : Name → α → AttrM Unit := fun env _ _ => pure ()) - (appTime := AttributeApplicationTime.afterTypeChecking) - : IO (ParametricAttribute α) := do +structure ParametricAttributeImpl (α : Type) extends AttributeImplCore := + (getParam : Name → Syntax → AttrM α) + (afterSet : Name → α → AttrM Unit := fun env _ _ => pure ()) + -- TODO: shouldn't be necessary + (applicationTime := AttributeApplicationTime.afterTypeChecking) + +def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension { - name := name, + name := impl.name, mkInitial := pure {}, addImportedFn := fun _ _ => pure {}, addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2, @@ -330,19 +336,16 @@ def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr r.qsort (fun a b => Name.quickLt a.1 b.1), statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size } - let attrImpl : AttributeImpl := { - name := name, - descr := descr, - applicationTime := appTime, + let attrImpl : AttributeImpl := { impl with add := fun decl args persistent => do - unless persistent do throwError! "invalid attribute '{name}', must be persistent" + unless persistent do throwError! "invalid attribute '{impl.name}', must be persistent" let env ← getEnv unless (env.getModuleIdxFor? decl).isNone do - throwError! "invalid attribute '{name}', declaration is in an imported module" - let val ← getParam decl args + throwError! "invalid attribute '{impl.name}', declaration is in an imported module" + let val ← impl.getParam decl args let env' := ext.addEntry env (decl, val) setEnv env' - try afterSet decl val catch _ => setEnv env + try impl.afterSet decl val catch _ => setEnv env } registerBuiltinAttribute attrImpl pure { attr := attrImpl, ext := ext } diff --git a/src/Lean/Compiler/ExportAttr.lean b/src/Lean/Compiler/ExportAttr.lean index 98ada2a3e5..19553ee123 100644 --- a/src/Lean/Compiler/ExportAttr.lean +++ b/src/Lean/Compiler/ExportAttr.lean @@ -18,12 +18,16 @@ private def isValidCppName : Name → Bool | _ => false builtin_initialize exportAttr : ParametricAttribute Name ← -registerParametricAttribute `export "name to be used by code generators" $ fun _ stx => - match attrParamSyntaxToIdentifier stx with - | some exportName => - if isValidCppName exportName then pure exportName - else throwError "invalid 'export' function name, is not a valid C++ identifier" - | _ => throwError "unexpected kind of argument" +registerParametricAttribute { + name := `export, + descr := "name to be used by code generators", + getParam := fun _ stx => + match attrParamSyntaxToIdentifier stx with + | some exportName => + if isValidCppName exportName then pure exportName + else throwError "invalid 'export' function name, is not a valid C++ identifier" + | _ => throwError "unexpected kind of argument", +} @[export lean_get_export_name_for] def getExportNameFor (env : Environment) (n : Name) : Option Name := diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index c4e4edcbc8..9072a5859d 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/src/Lean/Compiler/ExternAttr.lean @@ -80,15 +80,18 @@ private def syntaxToExternAttrData (s : Syntax) : ExceptT String Id ExternAttrDa constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment builtin_initialize externAttr : ParametricAttribute ExternAttrData ← - registerParametricAttribute `extern "builtin and foreign functions" - (fun _ stx => ofExcept $ syntaxToExternAttrData stx) - (fun declName _ => do + registerParametricAttribute { + name := `extern, + descr := "builtin and foreign functions", + getParam := fun _ stx => ofExcept $ syntaxToExternAttrData stx, + afterSet := fun declName _ => do let env ← getEnv if env.isProjectionFn declName || env.isConstructor declName then do env ← ofExcept $ addExtern env declName setEnv env else - pure ()) + pure (), + } @[export lean_get_extern_attr_data] def getExternAttrData (env : Environment) (n : Name) : Option ExternAttrData := diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean index 13ddef798e..0c8581b2f4 100644 --- a/src/Lean/Compiler/ImplementedByAttr.lean +++ b/src/Lean/Compiler/ImplementedByAttr.lean @@ -9,16 +9,19 @@ import Lean.MonadEnv namespace Lean.Compiler -builtin_initialize implementedByAttr : ParametricAttribute Name ← -registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) function that implements opaque constant" fun declName stx => do - let decl ← getConstInfo declName - match attrParamSyntaxToIdentifier stx with - | some fnName => - let fnName ← resolveGlobalConstNoOverload fnName; - let fnDecl ← getConstInfo fnName; - if decl.type == fnDecl.type then pure fnName - else throwError! "invalid function '{fnName}' type mismatch" - | _ => throwError "expected identifier" +builtin_initialize implementedByAttr : ParametricAttribute Name ← registerParametricAttribute { + name := `implementedBy, + descr := "name of the Lean (probably unsafe) function that implements opaque constant", + getParam := fun declName stx => do + let decl ← getConstInfo declName + match attrParamSyntaxToIdentifier stx with + | some fnName => + let fnName ← resolveGlobalConstNoOverload fnName + let fnDecl ← getConstInfo fnName + if decl.type == fnDecl.type then pure fnName + else throwError! "invalid function '{fnName}' type mismatch" + | _ => throwError "expected identifier", +} @[export lean_get_implemented_by] def getImplementedBy (env : Environment) (declName : Name) : Option Name := diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index b7a3d8b168..106536b582 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -23,22 +23,26 @@ match getIOTypeArg type with | _ => false def registerInitAttr (attrName : Name) : IO (ParametricAttribute Name) := -registerParametricAttribute attrName "initialization procedure for global references" fun declName stx => do - let decl ← getConstInfo declName - match attrParamSyntaxToIdentifier stx with - | some initFnName => - let initFnName ← resolveGlobalConstNoOverload initFnName - let initDecl ← getConstInfo initFnName - match getIOTypeArg initDecl.type with - | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO `") - | some initTypeArg => - if decl.type == initTypeArg then pure initFnName - else throwError ("initialization function '" ++ initFnName ++ "' type mismatch") - | _ => match stx with - | Syntax.missing => - if isIOUnit decl.type then pure Name.anonymous - else throwError "initialization function must have type `IO Unit`" - | _ => throwError "unexpected kind of argument" +registerParametricAttribute { + name := `init, + descr := "initialization procedure for global references", + getParam := fun declName stx => do + let decl ← getConstInfo declName + match attrParamSyntaxToIdentifier stx with + | some initFnName => + let initFnName ← resolveGlobalConstNoOverload initFnName + let initDecl ← getConstInfo initFnName + match getIOTypeArg initDecl.type with + | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO `") + | some initTypeArg => + if decl.type == initTypeArg then pure initFnName + else throwError ("initialization function '" ++ initFnName ++ "' type mismatch") + | _ => match stx with + | Syntax.missing => + if isIOUnit decl.type then pure Name.anonymous + else throwError "initialization function must have type `IO Unit`" + | _ => throwError "unexpected kind of argument", +} builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 5cf3440df8..f884296708 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -269,11 +269,14 @@ match cinfo with | _ => mkRecursorInfoAux cinfo majorPos? builtin_initialize recursorAttribute : ParametricAttribute Nat ← - registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise" - (fun _ stx => ofExcept $ syntaxToMajorPos stx) - (fun declName majorPos => do - (mkRecursorInfoCore declName (some majorPos)).run' - pure ()) +registerParametricAttribute { + name := `recursor, + descr := "user defined recursor, numerical parameter specifies position of the major premise", + getParam := fun _ stx => ofExcept $ syntaxToMajorPos stx, + afterSet := fun declName majorPos => do + (mkRecursorInfoCore declName (some majorPos)).run' + pure () +} def getMajorPos? (env : Environment) (declName : Name) : Option Nat := recursorAttribute.getParam env declName