From 64ee4e01a8a64c329a5b2bfd92d91c88dfdfed53 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 26 Jun 2019 10:09:57 -0700 Subject: [PATCH] refactor(library/init/lean/attributes): split `getParam` into `getParam` and `afterSet` --- library/init/lean/attributes.lean | 12 ++++++++--- library/init/lean/compiler/exportattr.lean | 4 ++-- library/init/lean/compiler/externattr.lean | 23 ++++++++++------------ library/init/lean/compiler/initattr.lean | 4 ++-- 4 files changed, 23 insertions(+), 20 deletions(-) diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean index 4f5b66c60a..5c8cd17003 100644 --- a/library/init/lean/attributes.lean +++ b/library/init/lean/attributes.lean @@ -297,7 +297,9 @@ structure ParametricAttribute (α : Type) := (attr : AttributeImpl) (ext : PersistentEnvExtension (Name × α) (NameMap α)) -def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String) (getParam : Environment → Name → Syntax → Except String (α × Environment)) : IO (ParametricAttribute α) := +def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String) + (getParam : Environment → Name → Syntax → Except String α) + (afterSet : Environment → Name → α → Except String Environment := λ env _ _, Except.ok env) : IO (ParametricAttribute α) := do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension { name := name, @@ -316,8 +318,12 @@ let attrImpl : AttributeImpl := { unless (env.getModuleIdxFor decl).isNone $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module")), match getParam env decl args with - | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) - | Except.ok (val, env) := pure $ ext.addEntry env (decl, val) + | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) + | Except.ok val := do + let env := ext.addEntry env (decl, val), + match afterSet env decl val with + | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) + | Except.ok env := pure env }, registerAttribute attrImpl, pure { attr := attrImpl, ext := ext } diff --git a/library/init/lean/compiler/exportattr.lean b/library/init/lean/compiler/exportattr.lean index 28b94289b5..2397a5fabe 100644 --- a/library/init/lean/compiler/exportattr.lean +++ b/library/init/lean/compiler/exportattr.lean @@ -18,10 +18,10 @@ private def isValidCppName : Name → Bool | _ := false def mkExportAttr : IO (ParametricAttribute Name) := -registerParametricAttribute `export "name to be used by code generators" $ λ env declName stx, +registerParametricAttribute `export "name to be used by code generators" $ λ _ _ stx, match stx with | Syntax.ident _ _ exportName _ _ := - if isValidCppName exportName then Except.ok (exportName, env) + if isValidCppName exportName then Except.ok exportName else Except.error "invalid 'export' function name, is not a valid C++ identifier" | _ := Except.error "unexpected kind of argument" diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean index 377f7b8306..6843c187a1 100644 --- a/library/init/lean/compiler/externattr.lean +++ b/library/init/lean/compiler/externattr.lean @@ -88,13 +88,13 @@ match s with constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment := default _ def mkExternAttr : IO (ParametricAttribute ExternAttrData) := -registerParametricAttribute `extern "builtin and foreign functions" $ λ env declName stx, do - val ← syntaxToExternAttrData stx, - if env.isProjectionFn declName || env.isConstructor declName then do - env ← addExtern env declName, - pure (val, env) - else - pure (val, env) +registerParametricAttribute `extern "builtin and foreign functions" + (λ _ _, syntaxToExternAttrData) + (λ env declName _, + if env.isProjectionFn declName || env.isConstructor declName then + addExtern env declName + else + pure env) @[init mkExternAttr] constant externAttr : ParametricAttribute ExternAttrData := default _ @@ -160,21 +160,18 @@ def mkExternCall (d : ExternAttrData) (backend : Name) (args : List String) : Op do e ← getExternEntryFor d backend, expandExternEntry e args -@[extern "lean_get_extern_attr_data"] -constant getExternAttrDataOld (env : @& Environment) (fn : @& Name) : Option ExternAttrData := default _ - def isExtern (env : Environment) (fn : Name) : Bool := -(getExternAttrDataOld env fn).isSome +(getExternAttrData env fn).isSome /- We say a Lean function marked as `[extern ""]` is for all backends, and it is implemented using `extern "C"`. Thus, there is no name mangling. -/ def isExternC (env : Environment) (fn : Name) : Bool := -match getExternAttrDataOld env fn with +match getExternAttrData env fn with | some { entries := [ ExternEntry.standard `all _ ], .. } := true | _ := false def getExternNameFor (env : Environment) (backend : Name) (fn : Name) : Option String := -do data ← getExternAttrDataOld env fn, +do data ← getExternAttrData env fn, entry ← getExternEntryFor data backend, match entry with | ExternEntry.standard _ n := pure n diff --git a/library/init/lean/compiler/initattr.lean b/library/init/lean/compiler/initattr.lean index 7cb153a8af..958725bd2b 100644 --- a/library/init/lean/compiler/initattr.lean +++ b/library/init/lean/compiler/initattr.lean @@ -35,10 +35,10 @@ registerParametricAttribute `init "initialization procedure for global reference match getIOTypeArg initDecl.type with | none := Except.error ("initialization function '" ++ toString initFnName ++ "' must have type of the form `IO `") | some initTypeArg := - if decl.type == initTypeArg then Except.ok (initFnName, env) + if decl.type == initTypeArg then Except.ok initFnName else Except.error ("initialization function '" ++ toString initFnName ++ "' type mismatch") | Syntax.missing := - if isIOUnit decl.type then Except.ok (Name.anonymous, env) + if isIOUnit decl.type then Except.ok Name.anonymous else Except.error "initialization function must have type `IO Unit`" | _ := Except.error "unexpected kind of argument"