From 2ef0ed7b5dbd72838158ad0dd487262aa1718fc3 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 25 May 2022 22:01:08 +0100 Subject: [PATCH 1/6] Add chapter on attributes. --- lean/extra/attributes.lean | 81 ++++ lean/extra/attrs/around.lean | 726 +++++++++++++++++++++++++++++++++++ lean/extra/attrs/dummy.lean | 26 ++ lean/extra/attrs/tag.lean | 25 ++ md/extra/attributes.md | 46 +++ 5 files changed, 904 insertions(+) create mode 100644 lean/extra/attrs/around.lean create mode 100644 lean/extra/attrs/dummy.lean create mode 100644 lean/extra/attrs/tag.lean diff --git a/lean/extra/attributes.lean b/lean/extra/attributes.lean index e69de29..dfdd2ba 100644 --- a/lean/extra/attributes.lean +++ b/lean/extra/attributes.lean @@ -0,0 +1,81 @@ +import lean.extra.attrs.dummy +import lean.extra.attrs.tag +/- +# Attributes + +Attributes in Lean allows one to perform preprocessing on definitions. +They are similar to Python's decorators and Rust's proc-macros. + +Unfortunately, it turns out that attributes must be defined in a separate module, so +we will bounce between this file and the files in the `attrs/` folder which +contain the implementations of the attributes. We'll see you at +[`./attrs/tag.lean`](./attrs/tag.lean). + +## Using `myTag` + +see that we've created a tagging infrastructure based on Lean's `TagAttribute`s, which exists +explicitly to allow us to create 'simple' attributes that wish to keep track of +definitions that have been tagged with a given attribute, and nothing more. + +-/ +@[myTag] +def tag1 : Int := 1 + +@[myTag] +def tag2 : Int := 2 + +@[myTag] +def tag3 : Int := 3 + +/- +See that we can access all the declarations that have been tagged with @[myTag]. +This simplified mechanism exists to allow us to easily tag definitions of interest. +-/ + +-- decl: tag3 | find? OfNat.ofNat.{0} Int 3 (Int.instOfNatInt 3) +-- decl: tag1 | find? OfNat.ofNat.{0} Int 1 (Int.instOfNatInt 1) +-- decl: tag2 | find? OfNat.ofNat.{0} Int 2 (Int.instOfNatInt 2) + + +/- +## Using `dummy_attr` + +We'll see you at [`./attrs/dummy.lean`](./attrs/dummy.lean). + + +We run the `dummy_attr `, and we see that we get access to the +attribute argument , the name of the declaration (`foo`), the type +of the declaration (`int`), and the value of the declaration, which +is the raw syntax tree. +-/ + +@[dummy_attr 0] +def foo : Int := 42 +-- number + 1: 1 +-- src: foo | stx: (Attr.dummy_attr "dummy_attr" (num "0")) | kind: global +-- srcDecl: +-- name: foo +-- type: Int +-- value?: (some (OfNat.ofNat.{0} Int 42 (Int.instOfNatInt 42))) + + +/- +Below is an example of a declaration that does not have any value. +-/ + +@[dummy_attr 52] +class bar +-- number + 1: 53 +-- src: bar | stx: (Attr.dummy_attr "dummy_attr" (num "52")) | kind: global +-- srcDecl: +-- name: bar +-- type: Type +-- value?: none + + +/- +## Modifying the `value` with the `around` attribute + +We're going to write an attribute that will modify a given definition +-/ + diff --git a/lean/extra/attrs/around.lean b/lean/extra/attrs/around.lean new file mode 100644 index 0000000..1996fb8 --- /dev/null +++ b/lean/extra/attrs/around.lean @@ -0,0 +1,726 @@ +import Lean +open Lean +open Lean.Meta +open Lean.Elab +open Lean.Elab.Command + +open System (FilePath) +open Std (HashMap) + +syntax (name := around_advice) "around_advice" str : attr +initialize registerTraceClass `around_advice + +initialize registerBuiltinAttribute { + name := `around_advice + descr :="around_advice print information" + add := fun src stx kind => do + dbg_trace "src: {src} | stx: {stx} | kind: {kind}" + let srcDecl : ConstantInfo ← getConstInfo src + dbg_trace "srcDecl:" + dbg_trace "\n {srcDecl.name}" + dbg_trace "\n {srcDecl.type}" + dbg_trace "\n {srcDecl.value?}" + srcDecl.updateName + return () + } + +abbrev RenameMap := HashMap Name Name + +def RenameMap.insertPair (m : RenameMap) : Name × Name → RenameMap + | (n3, n4) => m.insert n3 n4 + +initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameMap ← + registerSimplePersistentEnvExtension { + name := `renameMapExtension + addEntryFn := RenameMap.insertPair + addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es + } + +def findRename? (env : Environment) : Name → Option Name := + (renameExtension.getState env).find? + +/-- Add a (multiplicative → additive) name translation to the translations map. -/ +def insertRename (src tgt : Name) : CoreM Unit := do + if let some tgt' := findRename? (←getEnv) src then + throwError "Already exists translation {src} ↦ {tgt'}" + modifyEnv (renameExtension.addEntry · (src, tgt)) + -- | neat, we can trace like this?! + trace[to_additive] "Added translation {src} ↦ {tgt}." + +def getRenameMap (env : Environment) : RenameMap := + renameExtension.getState env + + + +partial def transformDecl (src: Name) (tgt: Name): CoreM Unit := do + let srcDecl ← getConstInfo src + dbg_trace "srcDecl:" + dbg_trace "\n {srcDecl.name}" + dbg_trace "\n {srcDecl.type}" + dbg_trace "\n {srcDecl.value?}" + return () + + +-- #print AttributeImpl +-- #print registerBuiltinAttribute + +-- initialize registerBuiltinAttribute { +-- name := `debug +-- descr :="debug print information" +-- add := fun src stx kind => do +-- dbg_trace "src: {src} | stx: {stx} | kind: {kind}" +-- let tgt := "foo" +-- if let some tgt' := findRename? (← getEnv) src then +-- throwError "{src} already has a to_additive translation {tgt'}." +-- insertRename src tgt +-- transformDecl src tgt +-- return () +-- } + +-- syntax (name := align) "#align " ident ident : command +-- +-- @[commandElab align] def elabAlign : CommandElab +-- | `(#align%$tk $id3:ident $id4:ident) => +-- liftCoreM $ addNameAlignment id3.getId id4.getId +-- | _ => throwUnsupportedSyntax +-- +-- syntax (name := lookup3) "#lookup3 " ident : command +-- +-- @[commandElab lookup3] def elabLookup3 : CommandElab +-- | `(#lookup3%$tk $id3:ident) => do +-- let n3 := id3.getId +-- match getRenameMap (← getEnv) |>.find? n3 with +-- | none => logInfoAt tk s!"name `{n3} not found" +-- | some n4 => logInfoAt tk s!"{n4}" +-- | _ => throwUnsupportedSyntax + + +-- | Add an attribute stating that this function must be debug logged. + +-- initialize ignoreArgsAttr : NameMapAttribute (List Nat) ← +-- registerNameMapAttribute { +-- name := `to_additive_ignore_args +-- descr := "Auxiliary attribute for `to_additive` stating that certain arguments are not additivized." +-- add := fun src stx => do +-- let ids ← match stx with +-- | `(attr|to_additive_ignore_args $[$ids:num]*) => pure <| ids.map (·.isNatLit?.get!) +-- | _ => throwError "unexpected to_additive_ignore_args syntax {stx}" +-- return ids.toList +-- } +-- +-- /-- Gets the set of arguments that should be ignored for the given name +-- (according to `@[to_additive_ignore_args ...]`). +-- This value is used in `additiveTestAux`. -/ +-- def ignore [Functor M] [MonadEnv M]: Name → M (Option (List Nat)) +-- | n => (ignoreArgsAttr.find? · n) <$> getEnv +-- +-- initialize reorderAttr : NameMapAttribute (List Nat) ← +-- registerNameMapAttribute { +-- name := `to_additive_reorder +-- descr := "Auxiliary attribute for `to_additive` that stores arguments that need to be reordered." +-- add := fun decl stx => +-- match stx with +-- | `(attr|to_additive_reorder $[$ids:num]*) => pure <| Array.toList <| ids.map (·.isNatLit?.get!) +-- | _ => throwError "unexpected to_additive_reorder syntax {stx}" +-- } +-- +-- /-- Get the reorder list (defined using `@[to_additive_reorder ...]`) for the given declaration. -/ +-- def getReorder [Functor M] [MonadEnv M]: Name → M (List Nat) +-- | n => (reorderAttr.find? · n |>.getD []) <$> getEnv +-- +-- /-- Given a declaration name and an argument index, determines whether this index +-- should be swapped with the next one. -/ +-- def shouldReorder [Functor M] [MonadEnv M]: Name → Nat → M Bool +-- | n, i => (i ∈ ·) <$> (getReorder n) +-- +-- initialize relevantArgAttr : NameMapAttribute (Nat) ← +-- registerNameMapAttribute { +-- name := `to_additive_relevant_arg +-- descr := "Auxiliary attribute for `to_additive` stating which arguments are the types with a multiplicative structure." +-- add := fun decl stx => +-- match stx with +-- | `(attr|to_additive_relevant_arg $id) => pure <| id.isNatLit?.get! +-- | _ => throwError "unexpected to_additive_relevant_arg syntax {stx}" +-- } +-- +-- /-- Given a declaration name and an argument index, determines whether it +-- is relevant. This is used in `applyReplacementFun` where more detail on what it +-- does can be found. -/ +-- def isRelevant [Monad M] [MonadEnv M] (n : Name) (i : Nat) : M Bool := do +-- match relevantArgAttr.find? (← getEnv) n with +-- | some j => return i == j +-- | none => return i == 0 +-- +-- /- Maps multiplicative names to their additive counterparts. -/ +-- initialize translations : NameMapExtension Name ← +-- mkNameMapExtension Name `translations +-- +-- /-- Get the multiplicative → additive translation for the given name. -/ +-- def findTranslation? (env : Environment) : Name → Option Name := +-- (ToAdditive.translations.getState env).find? +-- +-- /-- Add a (multiplicative → additive) name translation to the translations map. -/ +-- def insertTranslation (src tgt : Name) : CoreM Unit := do +-- if let some tgt' := findTranslation? (←getEnv) src then +-- throwError "Already exists translation {src} ↦ {tgt'}" +-- modifyEnv (ToAdditive.translations.addEntry · (src, tgt)) +-- trace[to_additive] "Added translation {src} ↦ {tgt}." +-- +-- /-- Get whether or not the replace-all flag is set. If this is true, then the +-- additiveTest heuristic is not used and all instances of multiplication are replaced. +-- You can enable this with `@[to_additive!]`-/ +-- def replaceAll [Functor M] [MonadOptions M] : M Bool := +-- (·.getBool `to_additive.replaceAll) <$> getOptions +-- +-- variable [Monad M] [MonadOptions M] [MonadEnv M] +-- +-- /-- Auxilliary function for `additiveTest`. The bool argument *only* matters when applied +-- to exactly a constant. -/ +-- private def additiveTestAux: Bool → Expr → M Bool +-- | b, Expr.const n _ _ => return b || (findTranslation? (← getEnv) n).isSome +-- | b, (Expr.app e a _) => do +-- if (← additiveTestAux true e) then +-- return true +-- if let (some n) := e.getAppFn.constName? then +-- if let (some l) ← ignore n then +-- if e.getAppNumArgs + 1 ∈ l then +-- return true +-- additiveTestAux false a +-- | b, (Expr.lam n e t _) => additiveTestAux false t +-- | b, (Expr.forallE n e t _) => additiveTestAux false t +-- | b, (Expr.letE n g e body _) => +-- return (←additiveTestAux false e) && (← additiveTestAux false body) +-- | b, _ => return true +-- +-- /-- +-- `additiveTest e` tests whether the expression `e` contains no constant +-- `nm` that is not applied to any arguments, and such that `translations.find?[nm] = none`. +-- This is used in `@[to_additive]` for deciding which subexpressions to transform: we only transform +-- constants if `additiveTest` applied to their first argument returns `true`. +-- This means we will replace expression applied to e.g. `α` or `α × β`, but not when applied to +-- e.g. `Nat` or `ℝ × α`. +-- We ignore all arguments specified by the `ignore` `NameMap`. +-- If `replaceAll` is `true` the test always returns `true`. +-- -/ +-- def additiveTest (e : Expr) : M Bool := do +-- if (←replaceAll) then +-- return true +-- else +-- additiveTestAux false e + +/-- +`e.applyReplacementFun f test` applies `f` to each identifier +(inductive type, defined function etc) in an expression, unless +* The identifier occurs in an application with first argument `arg`; and +* `test arg` is false. +However, if `f` is in the dictionary `relevant`, then the argument `relevant.find f` +is tested, instead of the first argument. + +Reorder contains the information about what arguments to reorder: +e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorder.find g = some [1]`. +We assume that all functions where we want to reorder arguments are fully applied. +This can be done by applying `etaExpand` first. +-/ +-- def applyReplacementFun : Expr → MetaM Expr := +-- Lean.Expr.replaceRecMeta fun r e => do +-- trace[to_additive_detail] "applyReplacementFun: replace at {e}" +-- match e with +-- | Expr.lit (Literal.natVal 1) _ => pure <| mkNatLit 0 +-- | Expr.const n₀ ls _ => do +-- let n₁ := Name.mapPrefix (findTranslation? <|← getEnv) n₀ +-- trace[to_additive_detail] "applyReplacementFun: {n₀} → {n₁}" +-- let ls : List Level ← (do -- [todo] just get Lean to figure out the levels? +-- if ← shouldReorder n₀ 1 then +-- return ls.get! 1::ls.head!::ls.drop 2 +-- return ls) +-- return some $ Lean.mkConst n₁ ls +-- | Expr.app g x _ => do +-- let gf := g.getAppFn +-- if let some nm := gf.constName? then +-- let gArgs := g.getAppArgs +-- -- e = `(nm y₁ .. yₙ x) +-- trace[to_additive_detail] "applyReplacementFun: app {nm} {gArgs} {x}" +-- if gArgs.size > 0 then +-- let c1 ← shouldReorder nm gArgs.size +-- let c2 ← additiveTest gArgs[0] +-- if c1 && c2 then +-- -- interchange `x` and the last argument of `g` +-- let x ← r x +-- let gf ← r g.appFn! +-- let ga ← r g.appArg! +-- let e₂ := mkApp2 gf x ga +-- trace[to_additive_detail] "applyReplacementFun: reordering {nm}: {x} ↔ {ga}\nBefore: {e}\nAfter: {e₂}" +-- return some e₂ +-- let c1 ← isRelevant nm gArgs.size +-- let c2 := gf.isConst +-- let c3 ← additiveTest x +-- if c1 && c2 && not c3 then +-- -- the test failed, so don't update the function body. +-- trace[to_additive_detail] "applyReplacementFun: isRelevant and test failed: {nm} {gArgs} {x}" +-- let x ← r x +-- let args ← gArgs.mapM r +-- return some $ mkApp (mkAppN gf args) x +-- return e.updateApp! (← r g) (← r x) +-- | _ => return none +-- +-- /-- Eta expands `e` at most `n` times.-/ +-- def etaExpandN (n : Nat) (e : Expr): MetaM Expr := do +-- forallBoundedTelescope (← inferType e) (some n) fun xs _ => mkLambdaFVars xs (mkAppN e xs) +-- +-- /-- `e.expand` eta-expands all expressions that have as head a constant `n` in +-- `reorder`. They are expanded until they are applied to one more argument than the maximum in +-- `reorder.find n`. -/ +-- def expand (e : Expr) : MetaM Expr := do +-- let e₂ ←e.replaceRecMeta $ fun r e => do +-- let e0 := e.getAppFn +-- let es := e.getAppArgs +-- let some e0n := e0.constName? | return none +-- let reorder ← getReorder e0n +-- if reorder.isEmpty then +-- -- no need to expand if nothing needs reordering +-- return none +-- let e' := mkAppN e0 $ ← es.mapM r +-- let needed_n := reorder.foldr Nat.max 0 + 1 +-- if needed_n ≤ es.size then +-- return some e' +-- else +-- -- in this case, we need to reorder arguments that are not yet +-- -- applied, so first η-expand the function. +-- let e' ← etaExpandN (needed_n - es.size) e' +-- return some $ e' +-- trace[to_additive_detail] "expand:\nBefore: {e}\nAfter: {e₂}" +-- return e₂ +-- +-- /-- Run applyReplacementFun on the given `srcDecl` to make a new declaration with name `tgt` -/ +-- def updateDecl +-- (tgt : Name) (srcDecl : ConstantInfo) +-- : MetaM ConstantInfo := do +-- let mut decl := srcDecl.updateName tgt +-- decl := decl.updateType $ (← applyReplacementFun (← expand decl.type)) +-- if let some v := decl.value? then +-- decl := decl.updateValue (← applyReplacementFun (← expand v)) +-- return decl +-- +-- /-- Lean 4 makes declarations which are not internal +-- (that is, head string starts with `_`) but which should be transformed. +-- eg `proof_1` in `Lean.Meta.mkAuxDefinitionFor` this might be better fixed in core. +-- This method is polyfill for that. -/ +-- def isInternal' : Name → Bool +-- | n@(Name.str _ s _) => (s.startsWith "proof_") || (Name.isInternal n) +-- | n => Name.isInternal n +-- +-- /-- transform the declaration `src` and all declarations `pre._proof_i` occurring in `src` +-- using the transforms dictionar declaration {src} which is in the namespace {pre}, but does not have the `@[to_additive]` attribute. This is not supported. Workaround: move {src} to a different namespace." +-- let env ← getEnv +-- -- we find the additive name of `src` +-- let tgt := src.mapPrefix (fun n => if n == pre then some tgt_pre else none) +-- -- we skip if we already transformed this declaration before +-- if env.contains tgt then +-- return +-- let srcDecl ← getConstInfo src +-- -- we first transform all the declarations of the form `pre._proof_i` +-- for n in srcDecl.type.listNamesWithPrefix pre do +-- transformDeclAux pre tgt_pre n +-- if let some value := srcDecl.value? then +-- for n in value.listNamesWithPrefix pre do +-- transformDeclAux pre tgt_pre n +-- -- now transform the source declaration +-- let trgDecl : ConstantInfo ← MetaM.run' $ updateDecl tgt srcDecl +-- if ¬ trgDecl.hasValue then +-- throwError "Expected {trgDecl.name} to have a value." +-- trace[to_additive] "generating\n{trgDecl.name} :=\n {trgDecl.value!}" +-- try +-- -- make sure that the type is correct, +-- -- and emit a more helpful error message if it fails +-- discard <| MetaM.run' <| inferType trgDecl.value! +-- catch +-- | Exception.error stx msg => throwError "@[to_additive] failed. +-- Type mismatch in additive declaration. For help, see the docstring +-- of `to_additive.attr`, section `Troubleshooting`. +-- Failed to add declaration\n{trgDecl.name}:\n{msg}" +-- | e => panic! "unreachable" +-- addAndCompile trgDecl.toDeclaration! +-- if isProtected (← getEnv) src then +-- setEnv $ addProtected (← getEnv) tgt +-- +-- /-- This should copy all of the attributes on src to tgt. +-- At the moment it only copies `simp` attributes because attributes +-- are not stored by the environment. +-- +-- [todo] add more attributes. A change is coming to core that should +-- allow us to iterate the attributes applied to a given decalaration. +-- -/ +-- def copyAttributes (src tgt : Name) : CoreM Unit := do +-- -- [todo] other simp theorems +-- let some ext ← getSimpExtension? `simp | return () +-- let thms ← ext.getTheorems +-- if (¬ thms.isLemma src) || thms.isLemma tgt then +-- return () +-- -- [todo] how to get prio data from SimpTheorems? +-- MetaM.run' $ Lean.Meta.addSimpTheorem ext tgt +-- (post := true) +-- (inv := false) +-- (attrKind := AttributeKind.global) +-- (prio := 1000) +-- return () +-- +-- /-- +-- Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and +-- the body using the `translations` dictionary. +-- This is used to implement `@[to_additive]`. +-- -/ +-- def transformDecl (src tgt : Name) : CoreM Unit := do +-- transformDeclAux src tgt src +-- let eqns? ← MetaM.run' (getEqnsFor? src true) +-- -- now transform all of the equational lemmas +-- if let some eqns := eqns? then +-- for src_eqn in eqns do +-- transformDeclAux src tgt src_eqn +-- -- [todo] copy attributes for equations +-- -- [todo] add equation lemmas to tgt_eqn +-- copyAttributes src tgt +-- return () +-- /-- +-- Find the first argument of `nm` that has a multiplicative type-class on it. +-- Returns 1 if there are no types with a multiplicative class as arguments. +-- E.g. `prod.group` returns 1, and `pi.has_one` returns 2. +-- -/ +-- def firstMultiplicativeArg (nm : Name) : MetaM (Option Nat) := do +-- let d ← getConstInfo nm +-- forallTelescopeReducing (← getConstInfo nm).type fun xs _ => do +-- -- xs are the arguments to the constant +-- let xs := xs.toList +-- let l ← xs.mapM fun x => do +-- -- x is an argument and i is the index +-- -- write `x : (y₀ : α₀) → ... → (yₙ : αₙ) → tgt_fn tgt_args₀ ... tgt_argsₘ` +-- forallTelescopeReducing (← inferType x) fun ys tgt => do +-- let (tgt_fn, tgt_args) := tgt.getAppFnArgs +-- let n_bi := ys.size +-- if let some c := tgt.getAppFn.constName? then +-- if findTranslation? (← getEnv) c |>.isNone then +-- return [] +-- return tgt_args.toList.filterMap fun tgt_arg => +-- xs.findIdx? fun x => Expr.containsFVar tgt_arg x.fvarId! +-- trace[to_additive_detail] "firstMultiplicativeArg: {l}" +-- match l.join with +-- | [] => return none +-- | (head :: tail) => return some <| tail.foldr Nat.min head +-- +-- +-- /-- `ValueType` is the type of the arguments that can be provided to `to_additive`. -/ +-- structure ValueType : Type where +-- /-- Replace all multiplicative declarations, do not use the heuristic. -/ +-- replaceAll : Bool := false +-- /-- View the trace of the to_additive procedure. +-- Equivalent to `set_option trace.to_additive true`. -/ +-- trace : Bool := false +-- /-- The name of the target (the additive declaration).-/ +-- tgt : Name := Name.anonymous +-- /-- An optional doc string.-/ +-- doc : Option String := none +-- /-- If `allow_auto_name` is `false` (default) then +-- `@[to_additive]` will check whether the given name can be auto-generated. -/ +-- allowAutoName : Bool := false +-- deriving Repr +-- +-- /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. -/ +-- def addCommPrefix : Bool → String → String +-- | true, s => "comm" ++ s.capitalize +-- | false, s => s +-- +-- /-- Dictionary used by `to_additive.guess_name` to autogenerate names. +-- [todo] update to Lean 4 naming -/ +-- private def guessNameDict : Bool → List String → List String +-- | is_comm, ("one" :: "le" :: s) => addCommPrefix is_comm "nonneg" :: guessNameDict false s +-- | is_comm, ("one" :: "lt" :: s) => addCommPrefix is_comm "pos" :: guessNameDict false s +-- | is_comm, ("le" :: "one" :: s) => addCommPrefix is_comm "nonpos" :: guessNameDict false s +-- | is_comm, ("lt" :: "one" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s +-- | is_comm, ("mul" :: "single" :: s) => addCommPrefix is_comm "single" :: guessNameDict false s +-- | is_comm, ("mul" :: "support" :: s) => addCommPrefix is_comm "support" :: guessNameDict false s +-- | is_comm, ("mul" :: "tsupport" :: s) => addCommPrefix is_comm "tsupport" :: guessNameDict false s +-- | is_comm, ("mul" :: "indicator" :: s) => addCommPrefix is_comm "indicator" :: guessNameDict false s +-- | is_comm, ("mul" :: s) => addCommPrefix is_comm "add" :: guessNameDict false s +-- | is_comm, ("smul" :: s) => addCommPrefix is_comm "vadd" :: guessNameDict false s +-- | is_comm, ("inv" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s +-- | is_comm, ("div" :: s) => addCommPrefix is_comm "sub" :: guessNameDict false s +-- | is_comm, ("one" :: s) => addCommPrefix is_comm "zero" :: guessNameDict false s +-- | is_comm, ("prod" :: s) => addCommPrefix is_comm "sum" :: guessNameDict false s +-- | is_comm, ("finprod" :: s) => addCommPrefix is_comm "finsum" :: guessNameDict false s +-- | is_comm, ("pow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s +-- | is_comm, ("npow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s +-- | is_comm, ("zpow" :: s) => addCommPrefix is_comm "zsmul" :: guessNameDict false s +-- | is_comm, ("monoid" :: s) => ("add_" ++ addCommPrefix is_comm "monoid") :: guessNameDict false s +-- | is_comm, ("submonoid" :: s) => ("add_" ++ addCommPrefix is_comm "submonoid") :: guessNameDict false s +-- | is_comm, ("group" :: s) => ("add_" ++ addCommPrefix is_comm "group") :: guessNameDict false s +-- | is_comm, ("subgroup" :: s) => ("add_" ++ addCommPrefix is_comm "subgroup") :: guessNameDict false s +-- | is_comm, ("semigroup" :: s) => ("add_" ++ addCommPrefix is_comm "semigroup") :: guessNameDict false s +-- | is_comm, ("magma" :: s) => ("add_" ++ addCommPrefix is_comm "magma") :: guessNameDict false s +-- | is_comm, ("haar" :: s) => ("add_" ++ addCommPrefix is_comm "haar") :: guessNameDict false s +-- | is_comm, ("prehaar" :: s) => ("add_" ++ addCommPrefix is_comm "prehaar") :: guessNameDict false s +-- | is_comm, ("unit" :: s) => ("add_" ++ addCommPrefix is_comm "unit") :: guessNameDict false s +-- | is_comm, ("units" :: s) => ("add_" ++ addCommPrefix is_comm "units") :: guessNameDict false s +-- | is_comm, ("comm" :: s) => guessNameDict true s +-- | is_comm, (x :: s) => (addCommPrefix is_comm x :: guessNameDict false s) +-- | true, [] => ["comm"] +-- | false, [] => [] +-- +-- /-- Autogenerate target name for `to_additive`. -/ +-- def guessName : String → String := +-- -- [todo] replace with camelcase logic? +-- String.mapTokens ''' $ +-- fun s => String.intercalate (String.singleton '_') $ +-- guessNameDict false (s.splitOn "_") +-- +-- /-- Return the provided target name or autogenerate one if one was not provided. -/ +-- def targetName (src tgt : Name) (allowAutoName : Bool) : CoreM Name := do +-- let res ← do +-- if tgt.getPrefix != Name.anonymous || allowAutoName then +-- return tgt +-- let (Name.str pre s _) := src | throwError "to_additive: can't transport {src}" +-- let tgt_auto := guessName s +-- if tgt.toString == tgt_auto then +-- dbg_trace "{src}: correctly autogenerated target name {tgt_auto}, you may remove the explicit {tgt} argument." +-- let pre := pre.mapPrefix <| findTranslation? (← getEnv) +-- if tgt == Name.anonymous then +-- return Name.mkStr pre tgt_auto +-- else +-- return Name.mkStr pre tgt.toString +-- if res == src && tgt != src then +-- throwError "to_additive: can't transport {src} to itself." +-- return res +-- +-- private def proceedFieldsAux (src tgt : Name) (f : Name → CoreM (List String)) : CoreM Unit := do +-- let srcFields ← f src +-- let tgtFields ← f tgt +-- if srcFields.length != tgtFields.length then +-- throwError "Failed to map fields of {src}, {tgt} with {srcFields} ↦ {tgtFields}" +-- for (srcField, tgtField) in List.zip srcFields tgtFields do +-- if srcField != tgtField then +-- insertTranslation (src ++ srcField) (tgt ++ tgtField) +-- +-- /-- Add the structure fields of `src` to the translations dictionary +-- so that future uses of `to_additive` will map them to the corresponding `tgt` fields. -/ +-- def proceedFields (src tgt : Name) : CoreM Unit := do +-- let env : Environment ← getEnv +-- let aux := proceedFieldsAux src tgt +-- aux (fun n => do +-- let fields := if isStructure env n then getStructureFieldsFlattened env n else #[] +-- return fields |> .map Name.toString |> Array.toList +-- ) +-- -- [todo] run to_additive on the constructors of n: +-- -- aux (fun n => (env.constructorsOf n).mmap $ ... +-- +-- private def elabToAdditiveAux +-- (replaceAll trace : Bool) (tgt : Option Syntax) (doc : Option Syntax) : ValueType := +-- { replaceAll := replaceAll +-- trace := trace +-- tgt := match tgt with | some tgt => tgt.getId | none => Name.anonymous +-- doc := doc.bind (·.isStrLit?) +-- allowAutoName := false +-- } +-- +-- private def elabToAdditive : Syntax → CoreM ValueType +-- | `(attr| to_additive $[!%$replaceAll]? $[?%$trace]? $[$tgt]? $[$doc]?) => +-- return elabToAdditiveAux replaceAll.isSome trace.isSome tgt doc +-- | _ => throwUnsupportedSyntax +-- +-- /-! +-- The attribute `to_additive` can be used to automatically transport theorems +-- and definitions (but not inductive types and structures) from a multiplicative +-- theory to an additive theory. +-- +-- To use this attribute, just write: +-- +-- ``` +-- @[to_additive] +-- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm +-- ``` +-- +-- This code will generate a theorem named `add_comm'`. It is also +-- possible to manually specify the name of the new declaration: +-- +-- ``` +-- @[to_additive add_foo] +-- theorem foo := sorry +-- ``` +-- +-- An existing documentation string will _not_ be automatically used, so if the theorem or definition +-- has a doc string, a doc string for the additive version should be passed explicitly to +-- `to_additive`. +-- +-- ``` +-- /-- Multiplication is commutative -/ +-- @[to_additive "Addition is commutative"] +-- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm +-- ``` +-- +-- The transport tries to do the right thing in most cases using several +-- heuristics described below. However, in some cases it fails, and +-- requires manual intervention. +-- +-- If the declaration to be transported has attributes which need to be +-- copied to the additive version, then `to_additive` should come last: +-- +-- ``` +-- @[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x +-- ``` +-- +-- Currently only the `simp` attribute is supported. +-- +-- ## Implementation notes +-- +-- The transport process generally works by taking all the names of +-- identifiers appearing in the name, type, and body of a declaration and +-- creating a new declaration by mapping those names to additive versions +-- using a simple string-based dictionary and also using all declarations +-- that have previously been labeled with `to_additive`. +-- +-- In the `mul_comm'` example above, `to_additive` maps: +-- * `mul_comm'` to `add_comm'`, +-- * `comm_semigroup` to `add_comm_semigroup`, +-- * `x * y` to `x + y` and `y * x` to `y + x`, and +-- * `comm_semigroup.mul_comm'` to `add_comm_semigroup.add_comm'`. +-- +-- ### Heuristics +-- +-- `to_additive` uses heuristics to determine whether a particular identifier has to be +-- mapped to its additive version. The basic heuristic is +-- +-- * Only map an identifier to its additive version if its first argument doesn't +-- contain any unapplied identifiers. +-- +-- Examples: +-- * `@Mul.mul Nat n m` (i.e. `(n * m : Nat)`) will not change to `+`, since its +-- first argument is `Nat`, an identifier not applied to any arguments. +-- * `@Mul.mul (α × β) x y` will change to `+`. It's first argument contains only the identifier +-- `prod`, but this is applied to arguments, `α` and `β`. +-- * `@Mul.mul (α × Int) x y` will not change to `+`, since its first argument contains `Int`. +-- +-- The reasoning behind the heuristic is that the first argument is the type which is "additivized", +-- and this usually doesn't make sense if this is on a fixed type. +-- +-- There are some exceptions to this heuristic: +-- +-- * Identifiers that have the `@[to_additive]` attribute are ignored. +-- For example, multiplication in `↥Semigroup` is replaced by addition in `↥AddSemigroup`. +-- * If an identifier `d` has attribute `@[to_additive_relevant_arg n]` then the argument +-- in position `n` is checked for a fixed type, instead of checking the first argument. +-- `@[to_additive]` will automatically add the attribute `@[to_additive_relevant_arg n]` to a +-- declaration when the first argument has no multiplicative type-class, but argument `n` does. +-- * If an identifier has attribute `@[to_additive_ignore_args n1 n2 ...]` then all the arguments in +-- positions `n1`, `n2`, ... will not be checked for unapplied identifiers (start counting from 1). +-- For example, `cont_mdiff_map` has attribute `@[to_additive_ignore_args 21]`, which means +-- that its 21st argument `(n : WithTop Nat)` can contain `Nat` +-- (usually in the form `has_top.top Nat ...`) and still be additivized. +-- So `@Mul.mul (C^∞⟮I, N; I', G⟯) _ f g` will be additivized. +-- +-- ### Troubleshooting +-- +-- If `@[to_additive]` fails because the additive declaration raises a type mismatch, there are +-- various things you can try. +-- The first thing to do is to figure out what `@[to_additive]` did wrong by looking at the type +-- mismatch error. +-- +-- * Option 1: It additivized a declaration `d` that should remain multiplicative. Solution: +-- * Make sure the first argument of `d` is a type with a multiplicative structure. If not, can you +-- reorder the (implicit) arguments of `d` so that the first argument becomes a type with a +-- multiplicative structure (and not some indexing type)? +-- The reason is that `@[to_additive]` doesn't additivize declarations if their first argument +-- contains fixed types like `Nat` or `ℝ`. See section Heuristics. +-- If the first argument is not the argument with a multiplicative type-class, `@[to_additive]` +-- should have automatically added the attribute `@[to_additive_relevant_arg]` to the declaration. +-- You can test this by running the following (where `d` is the full name of the declaration): +-- ``` +-- #eval (do isRelevant `d >>= trace) +-- ``` +-- The expected output is `n` where the `n`-th argument of `d` is a type (family) with a +-- multiplicative structure on it. If you get a different output (or a failure), you could add +-- the attribute `@[to_additive_relevant_arg n]` manually, where `n` is an argument with a +-- multiplicative structure. +-- * Option 2: It didn't additivize a declaration that should be additivized. +-- This happened because the heuristic applied, and the first argument contains a fixed type, +-- like `Nat` or `ℝ`. Solutions: +-- * If the fixed type has an additive counterpart (like `↥Semigroup`), give it the `@[to_additive]` +-- attribute. +-- * If the fixed type occurs inside the `k`-th argument of a declaration `d`, and the +-- `k`-th argument is not connected to the multiplicative structure on `d`, consider adding +-- attribute `[to_additive_ignore_args k]` to `d`. +-- * If you want to disable the heuristic and replace all multiplicative +-- identifiers with their additive counterpart, use `@[to_additive!]`. +-- * Option 3: Arguments / universe levels are incorrectly ordered in the additive version. +-- This likely only happens when the multiplicative declaration involves `pow`/`^`. Solutions: +-- * Ensure that the order of arguments of all relevant declarations are the same for the +-- multiplicative and additive version. This might mean that arguments have an "unnatural" order +-- (e.g. `Monoid.npow n x` corresponds to `x ^ n`, but it is convenient that `Monoid.npow` has this +-- argument order, since it matches `AddMonoid.nsmul n x`. +-- * If this is not possible, add the `[to_additive_reorder k]` to the multiplicative declaration +-- to indicate that the `k`-th and `(k+1)`-st arguments are reordered in the additive version. +-- +-- If neither of these solutions work, and `to_additive` is unable to automatically generate the +-- additive version of a declaration, manually write and prove the additive version. +-- Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to +-- `multiplicative G`. +-- Afterwards, apply the attribute manually: +-- +-- ``` +-- attribute [to_additive foo_add_bar] foo_bar +-- ``` +-- +-- This will allow future uses of `to_additive` to recognize that +-- `foo_bar` should be replaced with `foo_add_bar`. +-- +-- ### Handling of hidden definitions +-- +-- Before transporting the “main” declaration `src`, `to_additive` first +-- scans its type and value for names starting with `src`, and transports +-- them. This includes auxiliary definitions like `src._match_1`, +-- `src._proof_1`. +-- +-- In addition to transporting the “main” declaration, `to_additive` transports +-- its equational lemmas and tags them as equational lemmas for the new declaration, +-- attributes present on the original equational lemmas are also transferred first (notably +-- `_refl_lemma`). +-- +-- ### Structure fields and constructors +-- +-- If `src` is a structure, then `to_additive` automatically adds +-- structure fields to its mapping, and similarly for constructors of +-- inductive types. +-- +-- For new structures this means that `to_additive` automatically handles +-- coercions, and for old structures it does the same, if ancestry +-- information is present in `@[ancestor]` attributes. The `ancestor` +-- attribute must come before the `to_additive` attribute, and it is +-- essential that the order of the base structures passed to `ancestor` matches +-- between the multiplicative and additive versions of the structure. +-- +-- ### Name generation +-- +-- * If `@[to_additive]` is called without a `name` argument, then the +-- new name is autogenerated. First, it takes the longest prefix of +-- the source name that is already known to `to_additive`, and replaces +-- this prefix with its additive counterpart. Second, it takes the last +-- part of the name (i.e., after the last dot), and replaces common +-- name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. +-- +-- * [todo] Namespaces can be transformed using `map_namespace`. For example: +-- ``` +-- run_cmd to_additive.map_namespace `quotient_group `quotient_add_group +-- ``` +-- +-- Later uses of `to_additive` on declarations in the `quotient_group` +-- namespace will be created in the `quotient_add_group` namespaces. +-- +-- * If `@[to_additive]` is called with a `name` argument `new_name` +-- /without a dot/, then `to_additive` updates the prefix as described +-- above, then replaces the last part of the name with `new_name`. +-- +-- * If `@[to_additive]` is called with a `name` argument +-- `new_namespace.new_name` /with a dot/, then `to_additive` uses this +-- new name as is. +-- +-- As a safety check, in the first case `to_additive` double checks +-- that the new name differs from the original one. +-- +-- -/ +def foo : Int := 10 diff --git a/lean/extra/attrs/dummy.lean b/lean/extra/attrs/dummy.lean new file mode 100644 index 0000000..b4d49da --- /dev/null +++ b/lean/extra/attrs/dummy.lean @@ -0,0 +1,26 @@ +import Lean +open Lean + +namespace Attr +syntax (name := dummy_attr) "dummy_attr" term : attr +initialize registerTraceClass `dummy_attr + +initialize registerBuiltinAttribute { + name := `dummy_attr + descr :="dummy_attr print information" + add := fun src stx kind => do + let num : Nat := stx[1].toNat + dbg_trace "number + 1: {num + 1}" + dbg_trace "src: {src} | stx: {stx} | kind: {kind}" + let srcDecl ← getConstInfo src + dbg_trace "srcDecl:" + dbg_trace " name: {srcDecl.name}" + dbg_trace " type: {srcDecl.type}" + dbg_trace " value?: {srcDecl.value?}" + return () + } + +-- QUESTION: Can I uncomment this? +-- @[dummy_attr "foo"] +-- def foo : Int := 42 + diff --git a/lean/extra/attrs/tag.lean b/lean/extra/attrs/tag.lean new file mode 100644 index 0000000..de93638 --- /dev/null +++ b/lean/extra/attrs/tag.lean @@ -0,0 +1,25 @@ +import Lean + +open Lean Meta System Std Elab Command + + +initialize myTagAttribute : TagAttribute ← + registerTagAttribute `myTag "We are testing this custom tag." + + +def listAllTagged : MetaM Unit := do + let env <- getEnv + for declName in myTagAttribute.ext.getState env do + let mval := env.find? declName + let mstr := match mval with | .none => "" | .some v => toString v.value! + dbg_trace "decl: {declName} | find? {mstr}" + -- let x : NameSet := myTagAttribute.ext.getState env + + +elab "listAllTagged" : command => do + liftTermElabM (some `listAllTagged) (listAllTagged) + return () + + + + diff --git a/md/extra/attributes.md b/md/extra/attributes.md index 8b13789..92363ed 100644 --- a/md/extra/attributes.md +++ b/md/extra/attributes.md @@ -1 +1,47 @@ +```lean +import lean.extra.attrs.dummy +``` +# Attributes + +Attributes in Lean allows one to perform preprocessing on definitions. They are similar to Python's +decorators and Rust's proc-macros. + +Unfortunately, it turns out that attributes must be defined in a separate module, so +we will bounce between this file and the files in the `attrs/` folder which +contain the implementations of the attributes. We'll see you at +[`./attrs/dummy.lean`](./attrs/dummy.lean). + +## Using the `dummy_attr` + +We run the `dummy_attr`, and we see that we get access to the name +of the declaration (`foo`), the type of the declaration (`int`), and the +value of the declaration, which is the raw syntax tree. + +```lean +@[dummy_attr] +def foo : Int := 42 +-- src: foo | stx: (Attr.dummy_attr "dummy_attr") | kind: global +-- srcDecl: +-- name: foo +-- type: Int +-- value?: (some (OfNat.ofNat.{0} Int 42 (Int.instOfNatInt 42))) +``` + +Below is an example of a declaration that does not have any value. + +```lean +@[dummy_attr] +class bar +-- src: bar | stx: (Attr.dummy_attr "dummy_attr") | kind: global +-- srcDecl: +-- name: bar +-- type: Type +-- value?: none +``` + +## Modifying the `value` with the `around` attribute + +We're going to write an attribute that will modify a given definition + +## Tagging: `interesting` Definitions From 5da271c61b2c51251632bc50952f282b90eb1d7c Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 22 Jul 2022 22:36:11 +0100 Subject: [PATCH 2/6] add parametric attribute --- lean/extra/attributes.lean | 29 ++++++++++++++++++++++++++++- lean/extra/attrs/parameteric.lean | 23 +++++++++++++++++++++++ 2 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 lean/extra/attrs/parameteric.lean diff --git a/lean/extra/attributes.lean b/lean/extra/attributes.lean index dfdd2ba..d3a44ca 100644 --- a/lean/extra/attributes.lean +++ b/lean/extra/attributes.lean @@ -1,5 +1,6 @@ import lean.extra.attrs.dummy import lean.extra.attrs.tag +import lean.extra.attrs.parametric /- # Attributes @@ -11,7 +12,7 @@ we will bounce between this file and the files in the `attrs/` folder which contain the implementations of the attributes. We'll see you at [`./attrs/tag.lean`](./attrs/tag.lean). -## Using `myTag` +## Tag attributes with `myTag` see that we've created a tagging infrastructure based on Lean's `TagAttribute`s, which exists explicitly to allow us to create 'simple' attributes that wish to keep track of @@ -37,6 +38,26 @@ This simplified mechanism exists to allow us to easily tag definitions of intere -- decl: tag2 | find? OfNat.ofNat.{0} Int 2 (Int.instOfNatInt 2) +/- +## Parametric attributes with `myParam` + +A parametric attribute is like a tag attribute, while adding support for +parameters in the attribute. + +We shall add an attribute called `myParam`, which recieves two parameters, +a priority, denoted by a natural number, and an optional tag `important`. + + +We'll see you at [`./attrs/parametric.lean`](./attrs/dummy.lean). + +-/ + + + +@[myParam 10] def h1 (x : Nat) := 2*x + 1 +@[myParam 20 important] def h2 (x : Nat) := 2*x + 1 + + /- ## Using `dummy_attr` @@ -77,5 +98,11 @@ class bar ## Modifying the `value` with the `around` attribute We're going to write an attribute that will modify a given definition + + +## Implementing `sym`: +Scoped environment extension maintains scoping information, so it keeps track of +whether the tag is local or not. -/ + diff --git a/lean/extra/attrs/parameteric.lean b/lean/extra/attrs/parameteric.lean new file mode 100644 index 0000000..2d8a74e --- /dev/null +++ b/lean/extra/attrs/parameteric.lean @@ -0,0 +1,23 @@ +import Lean +open Lean + +-- The name of the syntax is important. The name is +-- used to connect to the corresponding attribute. +syntax (name := myParam) "myParam" num "important"? : attr + +initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← + registerParametricAttribute { + name := `myParam /- + The attribute name must match the `syntax` declaration name. + -/ + descr := "parametric attribute containing a priority and flag" + getParam := fun _ stx => + match stx with + | `(attr| myParam $prio:num) => + return (prio.toNat, false) + | `(attr| myParam $prio:num important) => + return (prio.toNat, true) + | _ => throwError "unexpected foo attribute" + afterSet := fun declName val => do + IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}" + } From 2d7f2667dc8a15249aa5bee506e916fd6567bf0c Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 22 Jul 2022 22:38:11 +0100 Subject: [PATCH 3/6] add simp attribute --- lean/extra/attributes.lean | 21 +++++++++++++++++++++ lean/extra/attrs/around.lean | 9 +++++++++ lean/extra/attrs/simp.lean | 3 +++ 3 files changed, 33 insertions(+) create mode 100644 lean/extra/attrs/simp.lean diff --git a/lean/extra/attributes.lean b/lean/extra/attributes.lean index d3a44ca..4ec2c6f 100644 --- a/lean/extra/attributes.lean +++ b/lean/extra/attributes.lean @@ -1,6 +1,7 @@ import lean.extra.attrs.dummy import lean.extra.attrs.tag import lean.extra.attrs.parametric +import lean.extra.attrs.simp /- # Attributes @@ -58,6 +59,26 @@ We'll see you at [`./attrs/parametric.lean`](./attrs/dummy.lean). @[myParam 20 important] def h2 (x : Nat) := 2*x + 1 +/- +## Using `simpAttr` +-/ + +@[my_simp] theorem f_eq : f x = x + 2 := rfl +@[my_simp] theorem g_eq : g x = x + 1 := rfl + +example : f x + g x = 2*x + 3 := by + simp_arith -- does not appy f_eq and g_eq + simp_arith [f, g] + +example : f x + g x = 2*x + 3 := by + simp_arith [my_simp] + +example : f x = id (x + 2) := by + simp + simp [my_simp] + + + /- ## Using `dummy_attr` diff --git a/lean/extra/attrs/around.lean b/lean/extra/attrs/around.lean index 1996fb8..70068d6 100644 --- a/lean/extra/attrs/around.lean +++ b/lean/extra/attrs/around.lean @@ -34,8 +34,17 @@ initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameM name := `renameMapExtension addEntryFn := RenameMap.insertPair addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es + initial := sorry } +/- +The key is Name × Name, and the value is RenameMap. +The entires are written into the `olean` files. +The functions `addEntryFn` tells us how to compute the values from the keys. +So the values are "just" a caching mechanism for the keys, where the keys tell us +what data is to be stored. +-/ + def findRename? (env : Environment) : Name → Option Name := (renameExtension.getState env).find? diff --git a/lean/extra/attrs/simp.lean b/lean/extra/attrs/simp.lean new file mode 100644 index 0000000..e4e12ae --- /dev/null +++ b/lean/extra/attrs/simp.lean @@ -0,0 +1,3 @@ +register_simp_attr fooSimp "my own foo simp attribute" + + From 67e636cfcf4e950c3a9d90c7d83dc49e899cedc8 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jul 2022 22:17:31 +0100 Subject: [PATCH 4/6] generate markdown for attributes --- lakefile.lean | 2 + lean-toolchain | 2 +- lean/extra/attrs/parameteric.lean | 4 +- lean/extra/attrs/simp.lean | 8 + md/extra/attributes.md | 96 +++- md/extra/attrs/around.md | 772 ++++++++++++++++++++++++++++++ md/extra/attrs/dummy.md | 27 ++ md/extra/attrs/parameteric.md | 25 + md/extra/attrs/simp.md | 11 + md/extra/attrs/tag.md | 23 + 10 files changed, 955 insertions(+), 15 deletions(-) create mode 100644 md/extra/attrs/around.md create mode 100644 md/extra/attrs/dummy.md create mode 100644 md/extra/attrs/parameteric.md create mode 100644 md/extra/attrs/simp.md create mode 100644 md/extra/attrs/tag.md diff --git a/lakefile.lean b/lakefile.lean index 81cf615..005af1a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -27,6 +27,7 @@ script build do if ← runCmd "python" #["-m", "lean2md", "lean", "md"] then return 1 if ← runCmd "python" #["-m", "lean2md", "lean/main", "md/main"] then return 1 if ← runCmd "python" #["-m", "lean2md", "lean/extra", "md/extra"] then return 1 + if ← runCmd "python" #["-m", "lean2md", "lean/extra/attrs", "md/extra/atrs"] then return 1 return 0 @@ -36,5 +37,6 @@ script viper_build do if ← runCmd "viper" #["-m", "lean2md", "lean", "md"] then return 1 if ← runCmd "viper" #["-m", "lean2md", "lean/main", "md/main"] then return 1 if ← runCmd "viper" #["-m", "lean2md", "lean/extra", "md/extra"] then return 1 + if ← runCmd "viper" #["-m", "lean2md", "lean/extra/attrs", "md/extra/attrs"] then return 1 return 0 diff --git a/lean-toolchain b/lean-toolchain index b6f166c..99f81a4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-07-16 +leanprover/lean4:nightly-2022-07-25 diff --git a/lean/extra/attrs/parameteric.lean b/lean/extra/attrs/parameteric.lean index 2d8a74e..caca66e 100644 --- a/lean/extra/attrs/parameteric.lean +++ b/lean/extra/attrs/parameteric.lean @@ -14,9 +14,9 @@ initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← getParam := fun _ stx => match stx with | `(attr| myParam $prio:num) => - return (prio.toNat, false) + return (prio.getNat, false) | `(attr| myParam $prio:num important) => - return (prio.toNat, true) + return (prio.getNat, true) | _ => throwError "unexpected foo attribute" afterSet := fun declName val => do IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}" diff --git a/lean/extra/attrs/simp.lean b/lean/extra/attrs/simp.lean index e4e12ae..2cd0795 100644 --- a/lean/extra/attrs/simp.lean +++ b/lean/extra/attrs/simp.lean @@ -1,3 +1,11 @@ +import Lean + + + +/-- +We declare a simplifcation attribute using the keyword +`register_simp_attr`, +-/ register_simp_attr fooSimp "my own foo simp attribute" diff --git a/md/extra/attributes.md b/md/extra/attributes.md index 92363ed..258ac51 100644 --- a/md/extra/attributes.md +++ b/md/extra/attributes.md @@ -1,27 +1,95 @@ ```lean import lean.extra.attrs.dummy +import lean.extra.attrs.tag +import lean.extra.attrs.parametric +import lean.extra.attrs.simp ``` # Attributes -Attributes in Lean allows one to perform preprocessing on definitions. They are similar to Python's -decorators and Rust's proc-macros. +Attributes in Lean allows one to perform preprocessing on definitions. +They are similar to Python's decorators and Rust's proc-macros. Unfortunately, it turns out that attributes must be defined in a separate module, so we will bounce between this file and the files in the `attrs/` folder which contain the implementations of the attributes. We'll see you at -[`./attrs/dummy.lean`](./attrs/dummy.lean). +[`./attrs/tag.lean`](./attrs/tag.lean). -## Using the `dummy_attr` +## Tag attributes with `myTag` -We run the `dummy_attr`, and we see that we get access to the name -of the declaration (`foo`), the type of the declaration (`int`), and the -value of the declaration, which is the raw syntax tree. +see that we've created a tagging infrastructure based on Lean's `TagAttribute`s, which exists +explicitly to allow us to create 'simple' attributes that wish to keep track of +definitions that have been tagged with a given attribute, and nothing more. ```lean -@[dummy_attr] +@[myTag] +def tag1 : Int := 1 + +@[myTag] +def tag2 : Int := 2 + +@[myTag] +def tag3 : Int := 3 +``` + +See that we can access all the declarations that have been tagged with @[myTag]. +This simplified mechanism exists to allow us to easily tag definitions of interest. + +```lean +-- decl: tag3 | find? OfNat.ofNat.{0} Int 3 (Int.instOfNatInt 3) +-- decl: tag1 | find? OfNat.ofNat.{0} Int 1 (Int.instOfNatInt 1) +-- decl: tag2 | find? OfNat.ofNat.{0} Int 2 (Int.instOfNatInt 2) +``` + +## Parametric attributes with `myParam` + +A parametric attribute is like a tag attribute, while adding support for +parameters in the attribute. + +We shall add an attribute called `myParam`, which recieves two parameters, +a priority, denoted by a natural number, and an optional tag `important`. + + +We'll see you at [`./attrs/parametric.lean`](./attrs/dummy.lean). + +```lean +@[myParam 10] def h1 (x : Nat) := 2*x + 1 +@[myParam 20 important] def h2 (x : Nat) := 2*x + 1 +``` + +## Using `simpAttr` + +```lean +@[my_simp] theorem f_eq : f x = x + 2 := rfl +@[my_simp] theorem g_eq : g x = x + 1 := rfl + +example : f x + g x = 2*x + 3 := by + simp_arith -- does not appy f_eq and g_eq + simp_arith [f, g] + +example : f x + g x = 2*x + 3 := by + simp_arith [my_simp] + +example : f x = id (x + 2) := by + simp + simp [my_simp] +``` + +## Using `dummy_attr` + +We'll see you at [`./attrs/dummy.lean`](./attrs/dummy.lean). + + +We run the `dummy_attr `, and we see that we get access to the +attribute argument , the name of the declaration (`foo`), the type +of the declaration (`int`), and the value of the declaration, which +is the raw syntax tree. + +```lean +@[dummy_attr 0] def foo : Int := 42 --- src: foo | stx: (Attr.dummy_attr "dummy_attr") | kind: global +-- number + 1: 1 +-- src: foo | stx: (Attr.dummy_attr "dummy_attr" (num "0")) | kind: global -- srcDecl: -- name: foo -- type: Int @@ -31,9 +99,10 @@ def foo : Int := 42 Below is an example of a declaration that does not have any value. ```lean -@[dummy_attr] +@[dummy_attr 52] class bar --- src: bar | stx: (Attr.dummy_attr "dummy_attr") | kind: global +-- number + 1: 53 +-- src: bar | stx: (Attr.dummy_attr "dummy_attr" (num "52")) | kind: global -- srcDecl: -- name: bar -- type: Type @@ -44,4 +113,7 @@ class bar We're going to write an attribute that will modify a given definition -## Tagging: `interesting` Definitions + +## Implementing `sym`: +Scoped environment extension maintains scoping information, so it keeps track of +whether the tag is local or not. diff --git a/md/extra/attrs/around.md b/md/extra/attrs/around.md new file mode 100644 index 0000000..bfd5e64 --- /dev/null +++ b/md/extra/attrs/around.md @@ -0,0 +1,772 @@ +```lean +import Lean +open Lean +open Lean.Meta +open Lean.Elab +open Lean.Elab.Command + +open System (FilePath) +open Std (HashMap) + +syntax (name := around_advice) "around_advice" str : attr +initialize registerTraceClass `around_advice + +initialize registerBuiltinAttribute { + name := `around_advice + descr :="around_advice print information" + add := fun src stx kind => do + dbg_trace "src: {src} | stx: {stx} | kind: {kind}" + let srcDecl : ConstantInfo ← getConstInfo src + dbg_trace "srcDecl:" + dbg_trace "\n {srcDecl.name}" + dbg_trace "\n {srcDecl.type}" + dbg_trace "\n {srcDecl.value?}" + srcDecl.updateName + return () + } + +abbrev RenameMap := HashMap Name Name + +def RenameMap.insertPair (m : RenameMap) : Name × Name → RenameMap + | (n3, n4) => m.insert n3 n4 + +initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameMap ← + registerSimplePersistentEnvExtension { + name := `renameMapExtension + addEntryFn := RenameMap.insertPair + addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es + initial := sorry + } +``` + +The key is Name × Name, and the value is RenameMap. +The entires are written into the `olean` files. +The functions `addEntryFn` tells us how to compute the values from the keys. +So the values are "just" a caching mechanism for the keys, where the keys tell us +what data is to be stored. + +```lean +def findRename? (env : Environment) : Name → Option Name := + (renameExtension.getState env).find? +``` + +- Add a (multiplicative → additive) name translation to the translations map. + +def insertRename (src tgt : Name) : CoreM Unit := do + if let some tgt' := findRename? (←getEnv) src then + throwError "Already exists translation {src} ↦ {tgt'}" + modifyEnv (renameExtension.addEntry · (src, tgt)) + -- | neat, we can trace like this?! + trace[to_additive] "Added translation {src} ↦ {tgt}." + +def getRenameMap (env : Environment) : RenameMap := + renameExtension.getState env + + + +partial def transformDecl (src: Name) (tgt: Name): CoreM Unit := do + let srcDecl ← getConstInfo src + dbg_trace "srcDecl:" + dbg_trace "\n {srcDecl.name}" + dbg_trace "\n {srcDecl.type}" + dbg_trace "\n {srcDecl.value?}" + return () + + +-- #print AttributeImpl +-- #print registerBuiltinAttribute + +-- initialize registerBuiltinAttribute { +-- name := `debug +-- descr :="debug print information" +-- add := fun src stx kind => do +-- dbg_trace "src: {src} | stx: {stx} | kind: {kind}" +-- let tgt := "foo" +-- if let some tgt' := findRename? (← getEnv) src then +-- throwError "{src} already has a to_additive translation {tgt'}." +-- insertRename src tgt +-- transformDecl src tgt +-- return () +-- } + +-- syntax (name := align) "#align " ident ident : command +-- +-- @[commandElab align] def elabAlign : CommandElab +-- | `(#align%$tk $id3:ident $id4:ident) => +-- liftCoreM $ addNameAlignment id3.getId id4.getId +-- | _ => throwUnsupportedSyntax +-- +-- syntax (name := lookup3) "#lookup3 " ident : command +-- +-- @[commandElab lookup3] def elabLookup3 : CommandElab +-- | `(#lookup3%$tk $id3:ident) => do +-- let n3 := id3.getId +-- match getRenameMap (← getEnv) |>.find? n3 with +-- | none => logInfoAt tk s!"name `{n3} not found" +-- | some n4 => logInfoAt tk s!"{n4}" +-- | _ => throwUnsupportedSyntax + + +-- | Add an attribute stating that this function must be debug logged. + +-- initialize ignoreArgsAttr : NameMapAttribute (List Nat) ← +-- registerNameMapAttribute { +-- name := `to_additive_ignore_args +-- descr := "Auxiliary attribute for `to_additive` stating that certain arguments are not additivized." +-- add := fun src stx => do +-- let ids ← match stx with +-- | `(attr|to_additive_ignore_args $[$ids:num]*) => pure <| ids.map (·.isNatLit?.get!) +-- | _ => throwError "unexpected to_additive_ignore_args syntax {stx}" +-- return ids.toList +-- } +-- +-- /-- Gets the set of arguments that should be ignored for the given name +-- (according to `@[to_additive_ignore_args ...]`). +-- This value is used in `additiveTestAux`. + +-- def ignore [Functor M] [MonadEnv M]: Name → M (Option (List Nat)) +-- | n => (ignoreArgsAttr.find? · n) <$> getEnv +-- +-- initialize reorderAttr : NameMapAttribute (List Nat) ← +-- registerNameMapAttribute { +-- name := `to_additive_reorder +-- descr := "Auxiliary attribute for `to_additive` that stores arguments that need to be reordered." +-- add := fun decl stx => +-- match stx with +-- | `(attr|to_additive_reorder $[$ids:num]*) => pure <| Array.toList <| ids.map (·.isNatLit?.get!) +-- | _ => throwError "unexpected to_additive_reorder syntax {stx}" +-- } +-- +-- /-- Get the reorder list (defined using `@[to_additive_reorder ...]`) for the given declaration. + +-- def getReorder [Functor M] [MonadEnv M]: Name → M (List Nat) +-- | n => (reorderAttr.find? · n |>.getD []) <$> getEnv +-- +-- /-- Given a declaration name and an argument index, determines whether this index +-- should be swapped with the next one. + +-- def shouldReorder [Functor M] [MonadEnv M]: Name → Nat → M Bool +-- | n, i => (i ∈ ·) <$> (getReorder n) +-- +-- initialize relevantArgAttr : NameMapAttribute (Nat) ← +-- registerNameMapAttribute { +-- name := `to_additive_relevant_arg +-- descr := "Auxiliary attribute for `to_additive` stating which arguments are the types with a multiplicative structure." +-- add := fun decl stx => +-- match stx with +-- | `(attr|to_additive_relevant_arg $id) => pure <| id.isNatLit?.get! +-- | _ => throwError "unexpected to_additive_relevant_arg syntax {stx}" +-- } +-- +-- /-- Given a declaration name and an argument index, determines whether it +-- is relevant. This is used in `applyReplacementFun` where more detail on what it +-- does can be found. + +-- def isRelevant [Monad M] [MonadEnv M] (n : Name) (i : Nat) : M Bool := do +-- match relevantArgAttr.find? (← getEnv) n with +-- | some j => return i == j +-- | none => return i == 0 +-- +-- /- Maps multiplicative names to their additive counterparts. + +-- initialize translations : NameMapExtension Name ← +-- mkNameMapExtension Name `translations +-- +-- /-- Get the multiplicative → additive translation for the given name. + +-- def findTranslation? (env : Environment) : Name → Option Name := +-- (ToAdditive.translations.getState env).find? +-- +-- /-- Add a (multiplicative → additive) name translation to the translations map. + +-- def insertTranslation (src tgt : Name) : CoreM Unit := do +-- if let some tgt' := findTranslation? (←getEnv) src then +-- throwError "Already exists translation {src} ↦ {tgt'}" +-- modifyEnv (ToAdditive.translations.addEntry · (src, tgt)) +-- trace[to_additive] "Added translation {src} ↦ {tgt}." +-- +-- /-- Get whether or not the replace-all flag is set. If this is true, then the +-- additiveTest heuristic is not used and all instances of multiplication are replaced. +-- You can enable this with `@[to_additive!]` + +-- def replaceAll [Functor M] [MonadOptions M] : M Bool := +-- (·.getBool `to_additive.replaceAll) <$> getOptions +-- +-- variable [Monad M] [MonadOptions M] [MonadEnv M] +-- +-- /-- Auxilliary function for `additiveTest`. The bool argument *only* matters when applied +-- to exactly a constant. + +-- private def additiveTestAux: Bool → Expr → M Bool +-- | b, Expr.const n _ _ => return b || (findTranslation? (← getEnv) n).isSome +-- | b, (Expr.app e a _) => do +-- if (← additiveTestAux true e) then +-- return true +-- if let (some n) := e.getAppFn.constName? then +-- if let (some l) ← ignore n then +-- if e.getAppNumArgs + 1 ∈ l then +-- return true +-- additiveTestAux false a +-- | b, (Expr.lam n e t _) => additiveTestAux false t +-- | b, (Expr.forallE n e t _) => additiveTestAux false t +-- | b, (Expr.letE n g e body _) => +-- return (←additiveTestAux false e) && (← additiveTestAux false body) +-- | b, _ => return true +-- +-- /-- +-- `additiveTest e` tests whether the expression `e` contains no constant +-- `nm` that is not applied to any arguments, and such that `translations.find?[nm] = none`. +-- This is used in `@[to_additive]` for deciding which subexpressions to transform: we only transform +-- constants if `additiveTest` applied to their first argument returns `true`. +-- This means we will replace expression applied to e.g. `α` or `α × β`, but not when applied to +-- e.g. `Nat` or `ℝ × α`. +-- We ignore all arguments specified by the `ignore` `NameMap`. +-- If `replaceAll` is `true` the test always returns `true`. +-- + +```lean +-- def additiveTest (e : Expr) : M Bool := do +-- if (←replaceAll) then +-- return true +-- else +-- additiveTestAux false e +``` + +- +`e.applyReplacementFun f test` applies `f` to each identifier +(inductive type, defined function etc) in an expression, unless +* The identifier occurs in an application with first argument `arg`; and +* `test arg` is false. +However, if `f` is in the dictionary `relevant`, then the argument `relevant.find f` +is tested, instead of the first argument. + +Reorder contains the information about what arguments to reorder: +e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorder.find g = some [1]`. +We assume that all functions where we want to reorder arguments are fully applied. +This can be done by applying `etaExpand` first. + +-- def applyReplacementFun : Expr → MetaM Expr := +-- Lean.Expr.replaceRecMeta fun r e => do +-- trace[to_additive_detail] "applyReplacementFun: replace at {e}" +-- match e with +-- | Expr.lit (Literal.natVal 1) _ => pure <| mkNatLit 0 +-- | Expr.const n₀ ls _ => do +-- let n₁ := Name.mapPrefix (findTranslation? <|← getEnv) n₀ +-- trace[to_additive_detail] "applyReplacementFun: {n₀} → {n₁}" +-- let ls : List Level ← (do -- [todo] just get Lean to figure out the levels? +-- if ← shouldReorder n₀ 1 then +-- return ls.get! 1::ls.head!::ls.drop 2 +-- return ls) +-- return some $ Lean.mkConst n₁ ls +-- | Expr.app g x _ => do +-- let gf := g.getAppFn +-- if let some nm := gf.constName? then +-- let gArgs := g.getAppArgs +-- -- e = `(nm y₁ .. yₙ x) +-- trace[to_additive_detail] "applyReplacementFun: app {nm} {gArgs} {x}" +-- if gArgs.size > 0 then +-- let c1 ← shouldReorder nm gArgs.size +-- let c2 ← additiveTest gArgs[0] +-- if c1 && c2 then +-- -- interchange `x` and the last argument of `g` +-- let x ← r x +-- let gf ← r g.appFn! +-- let ga ← r g.appArg! +-- let e₂ := mkApp2 gf x ga +-- trace[to_additive_detail] "applyReplacementFun: reordering {nm}: {x} ↔ {ga}\nBefore: {e}\nAfter: {e₂}" +-- return some e₂ +-- let c1 ← isRelevant nm gArgs.size +-- let c2 := gf.isConst +-- let c3 ← additiveTest x +-- if c1 && c2 && not c3 then +-- -- the test failed, so don't update the function body. +-- trace[to_additive_detail] "applyReplacementFun: isRelevant and test failed: {nm} {gArgs} {x}" +-- let x ← r x +-- let args ← gArgs.mapM r +-- return some $ mkApp (mkAppN gf args) x +-- return e.updateApp! (← r g) (← r x) +-- | _ => return none +-- +-- /-- Eta expands `e` at most `n` times. + +-- def etaExpandN (n : Nat) (e : Expr): MetaM Expr := do +-- forallBoundedTelescope (← inferType e) (some n) fun xs _ => mkLambdaFVars xs (mkAppN e xs) +-- +-- /-- `e.expand` eta-expands all expressions that have as head a constant `n` in +-- `reorder`. They are expanded until they are applied to one more argument than the maximum in +-- `reorder.find n`. + +-- def expand (e : Expr) : MetaM Expr := do +-- let e₂ ←e.replaceRecMeta $ fun r e => do +-- let e0 := e.getAppFn +-- let es := e.getAppArgs +-- let some e0n := e0.constName? | return none +-- let reorder ← getReorder e0n +-- if reorder.isEmpty then +-- -- no need to expand if nothing needs reordering +-- return none +-- let e' := mkAppN e0 $ ← es.mapM r +-- let needed_n := reorder.foldr Nat.max 0 + 1 +-- if needed_n ≤ es.size then +-- return some e' +-- else +-- -- in this case, we need to reorder arguments that are not yet +-- -- applied, so first η-expand the function. +-- let e' ← etaExpandN (needed_n - es.size) e' +-- return some $ e' +-- trace[to_additive_detail] "expand:\nBefore: {e}\nAfter: {e₂}" +-- return e₂ +-- +-- /-- Run applyReplacementFun on the given `srcDecl` to make a new declaration with name `tgt` + +-- def updateDecl +-- (tgt : Name) (srcDecl : ConstantInfo) +-- : MetaM ConstantInfo := do +-- let mut decl := srcDecl.updateName tgt +-- decl := decl.updateType $ (← applyReplacementFun (← expand decl.type)) +-- if let some v := decl.value? then +-- decl := decl.updateValue (← applyReplacementFun (← expand v)) +-- return decl +-- +-- /-- Lean 4 makes declarations which are not internal +-- (that is, head string starts with `_`) but which should be transformed. +-- eg `proof_1` in `Lean.Meta.mkAuxDefinitionFor` this might be better fixed in core. +-- This method is polyfill for that. + +-- def isInternal' : Name → Bool +-- | n@(Name.str _ s _) => (s.startsWith "proof_") || (Name.isInternal n) +-- | n => Name.isInternal n +-- +-- /-- transform the declaration `src` and all declarations `pre._proof_i` occurring in `src` +-- using the transforms dictionar declaration {src} which is in the namespace {pre}, but does not have the `@[to_additive]` attribute. This is not supported. Workaround: move {src} to a different namespace." +-- let env ← getEnv +-- -- we find the additive name of `src` +-- let tgt := src.mapPrefix (fun n => if n == pre then some tgt_pre else none) +-- -- we skip if we already transformed this declaration before +-- if env.contains tgt then +-- return +-- let srcDecl ← getConstInfo src +-- -- we first transform all the declarations of the form `pre._proof_i` +-- for n in srcDecl.type.listNamesWithPrefix pre do +-- transformDeclAux pre tgt_pre n +-- if let some value := srcDecl.value? then +-- for n in value.listNamesWithPrefix pre do +-- transformDeclAux pre tgt_pre n +-- -- now transform the source declaration +-- let trgDecl : ConstantInfo ← MetaM.run' $ updateDecl tgt srcDecl +-- if ¬ trgDecl.hasValue then +-- throwError "Expected {trgDecl.name} to have a value." +-- trace[to_additive] "generating\n{trgDecl.name} :=\n {trgDecl.value!}" +-- try +-- -- make sure that the type is correct, +-- -- and emit a more helpful error message if it fails +-- discard <| MetaM.run' <| inferType trgDecl.value! +-- catch +-- | Exception.error stx msg => throwError "@[to_additive] failed. +-- Type mismatch in additive declaration. For help, see the docstring +-- of `to_additive.attr`, section `Troubleshooting`. +-- Failed to add declaration\n{trgDecl.name}:\n{msg}" +-- | e => panic! "unreachable" +-- addAndCompile trgDecl.toDeclaration! +-- if isProtected (← getEnv) src then +-- setEnv $ addProtected (← getEnv) tgt +-- +-- /-- This should copy all of the attributes on src to tgt. +-- At the moment it only copies `simp` attributes because attributes +-- are not stored by the environment. +-- +-- [todo] add more attributes. A change is coming to core that should +-- allow us to iterate the attributes applied to a given decalaration. +-- + +-- def copyAttributes (src tgt : Name) : CoreM Unit := do +-- -- [todo] other simp theorems +-- let some ext ← getSimpExtension? `simp | return () +-- let thms ← ext.getTheorems +-- if (¬ thms.isLemma src) || thms.isLemma tgt then +-- return () +-- -- [todo] how to get prio data from SimpTheorems? +-- MetaM.run' $ Lean.Meta.addSimpTheorem ext tgt +-- (post := true) +-- (inv := false) +-- (attrKind := AttributeKind.global) +-- (prio := 1000) +-- return () +-- +-- /-- +-- Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and +-- the body using the `translations` dictionary. +-- This is used to implement `@[to_additive]`. +-- + +-- def transformDecl (src tgt : Name) : CoreM Unit := do +-- transformDeclAux src tgt src +-- let eqns? ← MetaM.run' (getEqnsFor? src true) +-- -- now transform all of the equational lemmas +-- if let some eqns := eqns? then +-- for src_eqn in eqns do +-- transformDeclAux src tgt src_eqn +-- -- [todo] copy attributes for equations +-- -- [todo] add equation lemmas to tgt_eqn +-- copyAttributes src tgt +-- return () +-- /-- +-- Find the first argument of `nm` that has a multiplicative type-class on it. +-- Returns 1 if there are no types with a multiplicative class as arguments. +-- E.g. `prod.group` returns 1, and `pi.has_one` returns 2. +-- + +-- def firstMultiplicativeArg (nm : Name) : MetaM (Option Nat) := do +-- let d ← getConstInfo nm +-- forallTelescopeReducing (← getConstInfo nm).type fun xs _ => do +-- -- xs are the arguments to the constant +-- let xs := xs.toList +-- let l ← xs.mapM fun x => do +-- -- x is an argument and i is the index +-- -- write `x : (y₀ : α₀) → ... → (yₙ : αₙ) → tgt_fn tgt_args₀ ... tgt_argsₘ` +-- forallTelescopeReducing (← inferType x) fun ys tgt => do +-- let (tgt_fn, tgt_args) := tgt.getAppFnArgs +-- let n_bi := ys.size +-- if let some c := tgt.getAppFn.constName? then +-- if findTranslation? (← getEnv) c |>.isNone then +-- return [] +-- return tgt_args.toList.filterMap fun tgt_arg => +-- xs.findIdx? fun x => Expr.containsFVar tgt_arg x.fvarId! +-- trace[to_additive_detail] "firstMultiplicativeArg: {l}" +-- match l.join with +-- | [] => return none +-- | (head :: tail) => return some <| tail.foldr Nat.min head +-- +-- +-- /-- `ValueType` is the type of the arguments that can be provided to `to_additive`. + +-- structure ValueType : Type where +-- /-- Replace all multiplicative declarations, do not use the heuristic. + +-- replaceAll : Bool := false +-- /-- View the trace of the to_additive procedure. +-- Equivalent to `set_option trace.to_additive true`. + +-- trace : Bool := false +-- /-- The name of the target (the additive declaration). + +-- tgt : Name := Name.anonymous +-- /-- An optional doc string. + +-- doc : Option String := none +-- /-- If `allow_auto_name` is `false` (default) then +-- `@[to_additive]` will check whether the given name can be auto-generated. + +-- allowAutoName : Bool := false +-- deriving Repr +-- +-- /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. + +-- def addCommPrefix : Bool → String → String +-- | true, s => "comm" ++ s.capitalize +-- | false, s => s +-- +-- /-- Dictionary used by `to_additive.guess_name` to autogenerate names. +-- [todo] update to Lean 4 naming + +-- private def guessNameDict : Bool → List String → List String +-- | is_comm, ("one" :: "le" :: s) => addCommPrefix is_comm "nonneg" :: guessNameDict false s +-- | is_comm, ("one" :: "lt" :: s) => addCommPrefix is_comm "pos" :: guessNameDict false s +-- | is_comm, ("le" :: "one" :: s) => addCommPrefix is_comm "nonpos" :: guessNameDict false s +-- | is_comm, ("lt" :: "one" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s +-- | is_comm, ("mul" :: "single" :: s) => addCommPrefix is_comm "single" :: guessNameDict false s +-- | is_comm, ("mul" :: "support" :: s) => addCommPrefix is_comm "support" :: guessNameDict false s +-- | is_comm, ("mul" :: "tsupport" :: s) => addCommPrefix is_comm "tsupport" :: guessNameDict false s +-- | is_comm, ("mul" :: "indicator" :: s) => addCommPrefix is_comm "indicator" :: guessNameDict false s +-- | is_comm, ("mul" :: s) => addCommPrefix is_comm "add" :: guessNameDict false s +-- | is_comm, ("smul" :: s) => addCommPrefix is_comm "vadd" :: guessNameDict false s +-- | is_comm, ("inv" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s +-- | is_comm, ("div" :: s) => addCommPrefix is_comm "sub" :: guessNameDict false s +-- | is_comm, ("one" :: s) => addCommPrefix is_comm "zero" :: guessNameDict false s +-- | is_comm, ("prod" :: s) => addCommPrefix is_comm "sum" :: guessNameDict false s +-- | is_comm, ("finprod" :: s) => addCommPrefix is_comm "finsum" :: guessNameDict false s +-- | is_comm, ("pow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s +-- | is_comm, ("npow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s +-- | is_comm, ("zpow" :: s) => addCommPrefix is_comm "zsmul" :: guessNameDict false s +-- | is_comm, ("monoid" :: s) => ("add_" ++ addCommPrefix is_comm "monoid") :: guessNameDict false s +-- | is_comm, ("submonoid" :: s) => ("add_" ++ addCommPrefix is_comm "submonoid") :: guessNameDict false s +-- | is_comm, ("group" :: s) => ("add_" ++ addCommPrefix is_comm "group") :: guessNameDict false s +-- | is_comm, ("subgroup" :: s) => ("add_" ++ addCommPrefix is_comm "subgroup") :: guessNameDict false s +-- | is_comm, ("semigroup" :: s) => ("add_" ++ addCommPrefix is_comm "semigroup") :: guessNameDict false s +-- | is_comm, ("magma" :: s) => ("add_" ++ addCommPrefix is_comm "magma") :: guessNameDict false s +-- | is_comm, ("haar" :: s) => ("add_" ++ addCommPrefix is_comm "haar") :: guessNameDict false s +-- | is_comm, ("prehaar" :: s) => ("add_" ++ addCommPrefix is_comm "prehaar") :: guessNameDict false s +-- | is_comm, ("unit" :: s) => ("add_" ++ addCommPrefix is_comm "unit") :: guessNameDict false s +-- | is_comm, ("units" :: s) => ("add_" ++ addCommPrefix is_comm "units") :: guessNameDict false s +-- | is_comm, ("comm" :: s) => guessNameDict true s +-- | is_comm, (x :: s) => (addCommPrefix is_comm x :: guessNameDict false s) +-- | true, [] => ["comm"] +-- | false, [] => [] +-- +-- /-- Autogenerate target name for `to_additive`. + +-- def guessName : String → String := +-- -- [todo] replace with camelcase logic? +-- String.mapTokens ''' $ +-- fun s => String.intercalate (String.singleton '_') $ +-- guessNameDict false (s.splitOn "_") +-- +-- /-- Return the provided target name or autogenerate one if one was not provided. + +-- def targetName (src tgt : Name) (allowAutoName : Bool) : CoreM Name := do +-- let res ← do +-- if tgt.getPrefix != Name.anonymous || allowAutoName then +-- return tgt +-- let (Name.str pre s _) := src | throwError "to_additive: can't transport {src}" +-- let tgt_auto := guessName s +-- if tgt.toString == tgt_auto then +-- dbg_trace "{src}: correctly autogenerated target name {tgt_auto}, you may remove the explicit {tgt} argument." +-- let pre := pre.mapPrefix <| findTranslation? (← getEnv) +-- if tgt == Name.anonymous then +-- return Name.mkStr pre tgt_auto +-- else +-- return Name.mkStr pre tgt.toString +-- if res == src && tgt != src then +-- throwError "to_additive: can't transport {src} to itself." +-- return res +-- +-- private def proceedFieldsAux (src tgt : Name) (f : Name → CoreM (List String)) : CoreM Unit := do +-- let srcFields ← f src +-- let tgtFields ← f tgt +-- if srcFields.length != tgtFields.length then +-- throwError "Failed to map fields of {src}, {tgt} with {srcFields} ↦ {tgtFields}" +-- for (srcField, tgtField) in List.zip srcFields tgtFields do +-- if srcField != tgtField then +-- insertTranslation (src ++ srcField) (tgt ++ tgtField) +-- +-- /-- Add the structure fields of `src` to the translations dictionary +-- so that future uses of `to_additive` will map them to the corresponding `tgt` fields. + +-- def proceedFields (src tgt : Name) : CoreM Unit := do +-- let env : Environment ← getEnv +-- let aux := proceedFieldsAux src tgt +-- aux (fun n => do +-- let fields := if isStructure env n then getStructureFieldsFlattened env n else #[] +-- return fields |> .map Name.toString |> Array.toList +-- ) +-- -- [todo] run to_additive on the constructors of n: +-- -- aux (fun n => (env.constructorsOf n).mmap $ ... +-- +-- private def elabToAdditiveAux +-- (replaceAll trace : Bool) (tgt : Option Syntax) (doc : Option Syntax) : ValueType := +-- { replaceAll := replaceAll +-- trace := trace +-- tgt := match tgt with | some tgt => tgt.getId | none => Name.anonymous +-- doc := doc.bind (·.isStrLit?) +-- allowAutoName := false +-- } +-- +-- private def elabToAdditive : Syntax → CoreM ValueType +-- | `(attr| to_additive $[!%$replaceAll]? $[?%$trace]? $[$tgt]? $[$doc]?) => +-- return elabToAdditiveAux replaceAll.isSome trace.isSome tgt doc +-- | _ => throwUnsupportedSyntax +-- +-- /-! +-- The attribute `to_additive` can be used to automatically transport theorems +-- and definitions (but not inductive types and structures) from a multiplicative +-- theory to an additive theory. +-- +-- To use this attribute, just write: +-- +-- ``` +-- @[to_additive] +-- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm +-- ``` +-- +-- This code will generate a theorem named `add_comm'`. It is also +-- possible to manually specify the name of the new declaration: +-- +-- ``` +-- @[to_additive add_foo] +-- theorem foo := sorry +-- ``` +-- +-- An existing documentation string will _not_ be automatically used, so if the theorem or definition +-- has a doc string, a doc string for the additive version should be passed explicitly to +-- `to_additive`. +-- +-- ``` +-- /-- Multiplication is commutative + +-- @[to_additive "Addition is commutative"] +-- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm +-- ``` +-- +-- The transport tries to do the right thing in most cases using several +-- heuristics described below. However, in some cases it fails, and +-- requires manual intervention. +-- +-- If the declaration to be transported has attributes which need to be +-- copied to the additive version, then `to_additive` should come last: +-- +-- ``` +-- @[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x +-- ``` +-- +-- Currently only the `simp` attribute is supported. +-- +-- ## Implementation notes +-- +-- The transport process generally works by taking all the names of +-- identifiers appearing in the name, type, and body of a declaration and +-- creating a new declaration by mapping those names to additive versions +-- using a simple string-based dictionary and also using all declarations +-- that have previously been labeled with `to_additive`. +-- +-- In the `mul_comm'` example above, `to_additive` maps: +-- * `mul_comm'` to `add_comm'`, +-- * `comm_semigroup` to `add_comm_semigroup`, +-- * `x * y` to `x + y` and `y * x` to `y + x`, and +-- * `comm_semigroup.mul_comm'` to `add_comm_semigroup.add_comm'`. +-- +-- ### Heuristics +-- +-- `to_additive` uses heuristics to determine whether a particular identifier has to be +-- mapped to its additive version. The basic heuristic is +-- +-- * Only map an identifier to its additive version if its first argument doesn't +-- contain any unapplied identifiers. +-- +-- Examples: +-- * `@Mul.mul Nat n m` (i.e. `(n * m : Nat)`) will not change to `+`, since its +-- first argument is `Nat`, an identifier not applied to any arguments. +-- * `@Mul.mul (α × β) x y` will change to `+`. It's first argument contains only the identifier +-- `prod`, but this is applied to arguments, `α` and `β`. +-- * `@Mul.mul (α × Int) x y` will not change to `+`, since its first argument contains `Int`. +-- +-- The reasoning behind the heuristic is that the first argument is the type which is "additivized", +-- and this usually doesn't make sense if this is on a fixed type. +-- +-- There are some exceptions to this heuristic: +-- +-- * Identifiers that have the `@[to_additive]` attribute are ignored. +-- For example, multiplication in `↥Semigroup` is replaced by addition in `↥AddSemigroup`. +-- * If an identifier `d` has attribute `@[to_additive_relevant_arg n]` then the argument +-- in position `n` is checked for a fixed type, instead of checking the first argument. +-- `@[to_additive]` will automatically add the attribute `@[to_additive_relevant_arg n]` to a +-- declaration when the first argument has no multiplicative type-class, but argument `n` does. +-- * If an identifier has attribute `@[to_additive_ignore_args n1 n2 ...]` then all the arguments in +-- positions `n1`, `n2`, ... will not be checked for unapplied identifiers (start counting from 1). +-- For example, `cont_mdiff_map` has attribute `@[to_additive_ignore_args 21]`, which means +-- that its 21st argument `(n : WithTop Nat)` can contain `Nat` +-- (usually in the form `has_top.top Nat ...`) and still be additivized. +-- So `@Mul.mul (C^∞⟮I, N; I', G⟯) _ f g` will be additivized. +-- +-- ### Troubleshooting +-- +-- If `@[to_additive]` fails because the additive declaration raises a type mismatch, there are +-- various things you can try. +-- The first thing to do is to figure out what `@[to_additive]` did wrong by looking at the type +-- mismatch error. +-- +-- * Option 1: It additivized a declaration `d` that should remain multiplicative. Solution: +-- * Make sure the first argument of `d` is a type with a multiplicative structure. If not, can you +-- reorder the (implicit) arguments of `d` so that the first argument becomes a type with a +-- multiplicative structure (and not some indexing type)? +-- The reason is that `@[to_additive]` doesn't additivize declarations if their first argument +-- contains fixed types like `Nat` or `ℝ`. See section Heuristics. +-- If the first argument is not the argument with a multiplicative type-class, `@[to_additive]` +-- should have automatically added the attribute `@[to_additive_relevant_arg]` to the declaration. +-- You can test this by running the following (where `d` is the full name of the declaration): +-- ``` +-- #eval (do isRelevant `d >>= trace) +-- ``` +-- The expected output is `n` where the `n`-th argument of `d` is a type (family) with a +-- multiplicative structure on it. If you get a different output (or a failure), you could add +-- the attribute `@[to_additive_relevant_arg n]` manually, where `n` is an argument with a +-- multiplicative structure. +-- * Option 2: It didn't additivize a declaration that should be additivized. +-- This happened because the heuristic applied, and the first argument contains a fixed type, +-- like `Nat` or `ℝ`. Solutions: +-- * If the fixed type has an additive counterpart (like `↥Semigroup`), give it the `@[to_additive]` +-- attribute. +-- * If the fixed type occurs inside the `k`-th argument of a declaration `d`, and the +-- `k`-th argument is not connected to the multiplicative structure on `d`, consider adding +-- attribute `[to_additive_ignore_args k]` to `d`. +-- * If you want to disable the heuristic and replace all multiplicative +-- identifiers with their additive counterpart, use `@[to_additive!]`. +-- * Option 3: Arguments / universe levels are incorrectly ordered in the additive version. +-- This likely only happens when the multiplicative declaration involves `pow`/`^`. Solutions: +-- * Ensure that the order of arguments of all relevant declarations are the same for the +-- multiplicative and additive version. This might mean that arguments have an "unnatural" order +-- (e.g. `Monoid.npow n x` corresponds to `x ^ n`, but it is convenient that `Monoid.npow` has this +-- argument order, since it matches `AddMonoid.nsmul n x`. +-- * If this is not possible, add the `[to_additive_reorder k]` to the multiplicative declaration +-- to indicate that the `k`-th and `(k+1)`-st arguments are reordered in the additive version. +-- +-- If neither of these solutions work, and `to_additive` is unable to automatically generate the +-- additive version of a declaration, manually write and prove the additive version. +-- Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to +-- `multiplicative G`. +-- Afterwards, apply the attribute manually: +-- +-- ``` +-- attribute [to_additive foo_add_bar] foo_bar +-- ``` +-- +-- This will allow future uses of `to_additive` to recognize that +-- `foo_bar` should be replaced with `foo_add_bar`. +-- +-- ### Handling of hidden definitions +-- +-- Before transporting the “main” declaration `src`, `to_additive` first +-- scans its type and value for names starting with `src`, and transports +-- them. This includes auxiliary definitions like `src._match_1`, +-- `src._proof_1`. +-- +-- In addition to transporting the “main” declaration, `to_additive` transports +-- its equational lemmas and tags them as equational lemmas for the new declaration, +-- attributes present on the original equational lemmas are also transferred first (notably +-- `_refl_lemma`). +-- +-- ### Structure fields and constructors +-- +-- If `src` is a structure, then `to_additive` automatically adds +-- structure fields to its mapping, and similarly for constructors of +-- inductive types. +-- +-- For new structures this means that `to_additive` automatically handles +-- coercions, and for old structures it does the same, if ancestry +-- information is present in `@[ancestor]` attributes. The `ancestor` +-- attribute must come before the `to_additive` attribute, and it is +-- essential that the order of the base structures passed to `ancestor` matches +-- between the multiplicative and additive versions of the structure. +-- +-- ### Name generation +-- +-- * If `@[to_additive]` is called without a `name` argument, then the +-- new name is autogenerated. First, it takes the longest prefix of +-- the source name that is already known to `to_additive`, and replaces +-- this prefix with its additive counterpart. Second, it takes the last +-- part of the name (i.e., after the last dot), and replaces common +-- name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. +-- +-- * [todo] Namespaces can be transformed using `map_namespace`. For example: +-- ``` +-- run_cmd to_additive.map_namespace `quotient_group `quotient_add_group +-- ``` +-- +-- Later uses of `to_additive` on declarations in the `quotient_group` +-- namespace will be created in the `quotient_add_group` namespaces. +-- +-- * If `@[to_additive]` is called with a `name` argument `new_name` +-- /without a dot/, then `to_additive` updates the prefix as described +-- above, then replaces the last part of the name with `new_name`. +-- +-- * If `@[to_additive]` is called with a `name` argument +-- `new_namespace.new_name` /with a dot/, then `to_additive` uses this +-- new name as is. +-- +-- As a safety check, in the first case `to_additive` double checks +-- that the new name differs from the original one. +-- +-- + +```lean +def foo : Int := 10 +``` diff --git a/md/extra/attrs/dummy.md b/md/extra/attrs/dummy.md new file mode 100644 index 0000000..6c5f851 --- /dev/null +++ b/md/extra/attrs/dummy.md @@ -0,0 +1,27 @@ +```lean +import Lean +open Lean + +namespace Attr +syntax (name := dummy_attr) "dummy_attr" term : attr +initialize registerTraceClass `dummy_attr + +initialize registerBuiltinAttribute { + name := `dummy_attr + descr :="dummy_attr print information" + add := fun src stx kind => do + let num : Nat := stx[1].toNat + dbg_trace "number + 1: {num + 1}" + dbg_trace "src: {src} | stx: {stx} | kind: {kind}" + let srcDecl ← getConstInfo src + dbg_trace "srcDecl:" + dbg_trace " name: {srcDecl.name}" + dbg_trace " type: {srcDecl.type}" + dbg_trace " value?: {srcDecl.value?}" + return () + } + +-- QUESTION: Can I uncomment this? +-- @[dummy_attr "foo"] +-- def foo : Int := 42 +``` diff --git a/md/extra/attrs/parameteric.md b/md/extra/attrs/parameteric.md new file mode 100644 index 0000000..8e56d69 --- /dev/null +++ b/md/extra/attrs/parameteric.md @@ -0,0 +1,25 @@ +import Lean +open Lean + +-- The name of the syntax is important. The name is +-- used to connect to the corresponding attribute. +syntax (name := myParam) "myParam" num "important"? : attr + +initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← + registerParametricAttribute { + name := `myParam /- + The attribute name must match the `syntax` declaration name. + +```lean +descr := "parametric attribute containing a priority and flag" + getParam := fun _ stx => + match stx with + | `(attr| myParam $prio:num) => + return (prio.getNat, false) + | `(attr| myParam $prio:num important) => + return (prio.getNat, true) + | _ => throwError "unexpected foo attribute" + afterSet := fun declName val => do + IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}" + } +``` diff --git a/md/extra/attrs/simp.md b/md/extra/attrs/simp.md new file mode 100644 index 0000000..ad579e3 --- /dev/null +++ b/md/extra/attrs/simp.md @@ -0,0 +1,11 @@ +```lean +import Lean +``` + +- +We declare a simplifcation attribute using the keyword +`register_simp_attr`, + +```lean +register_simp_attr fooSimp "my own foo simp attribute" +``` diff --git a/md/extra/attrs/tag.md b/md/extra/attrs/tag.md new file mode 100644 index 0000000..09a863b --- /dev/null +++ b/md/extra/attrs/tag.md @@ -0,0 +1,23 @@ +```lean +import Lean + +open Lean Meta System Std Elab Command + + +initialize myTagAttribute : TagAttribute ← + registerTagAttribute `myTag "We are testing this custom tag." + + +def listAllTagged : MetaM Unit := do + let env <- getEnv + for declName in myTagAttribute.ext.getState env do + let mval := env.find? declName + let mstr := match mval with | .none => "" | .some v => toString v.value! + dbg_trace "decl: {declName} | find? {mstr}" + -- let x : NameSet := myTagAttribute.ext.getState env + + +elab "listAllTagged" : command => do + liftTermElabM (some `listAllTagged) (listAllTagged) + return () +``` From 73d33772ec22829058f03647072f802a297ba031 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jul 2022 22:29:48 +0100 Subject: [PATCH 5/6] delete the complicated case --- lean/extra/attributes.lean | 15 +- lean/extra/attrs/around.lean | 735 ------------------------------ lean/extra/attrs/dummy.lean | 18 +- lean/extra/attrs/parameteric.lean | 16 +- lean/extra/attrs/simp.lean | 2 - 5 files changed, 30 insertions(+), 756 deletions(-) delete mode 100644 lean/extra/attrs/around.lean diff --git a/lean/extra/attributes.lean b/lean/extra/attributes.lean index 4ec2c6f..fdad209 100644 --- a/lean/extra/attributes.lean +++ b/lean/extra/attributes.lean @@ -1,7 +1,8 @@ import lean.extra.attrs.dummy import lean.extra.attrs.tag -import lean.extra.attrs.parametric -import lean.extra.attrs.simp +-- import lean.extra.attrs.parametric +-- import lean.extra.attrs.simp + /- # Attributes @@ -10,7 +11,7 @@ They are similar to Python's decorators and Rust's proc-macros. Unfortunately, it turns out that attributes must be defined in a separate module, so we will bounce between this file and the files in the `attrs/` folder which -contain the implementations of the attributes. We'll see you at +contain the implementations of the attributes. We'll see you at [`./attrs/tag.lean`](./attrs/tag.lean). ## Tag attributes with `myTag` @@ -43,7 +44,7 @@ This simplified mechanism exists to allow us to easily tag definitions of intere ## Parametric attributes with `myParam` A parametric attribute is like a tag attribute, while adding support for -parameters in the attribute. +parameters in the attribute. We shall add an attribute called `myParam`, which recieves two parameters, a priority, denoted by a natural number, and an optional tag `important`. @@ -101,12 +102,12 @@ def foo : Int := 42 -- value?: (some (OfNat.ofNat.{0} Int 42 (Int.instOfNatInt 42))) -/- +/- Below is an example of a declaration that does not have any value. -/ @[dummy_attr 52] -class bar +class bar -- number + 1: 53 -- src: bar | stx: (Attr.dummy_attr "dummy_attr" (num "52")) | kind: global -- srcDecl: @@ -123,7 +124,7 @@ We're going to write an attribute that will modify a given definition ## Implementing `sym`: Scoped environment extension maintains scoping information, so it keeps track of -whether the tag is local or not. +whether the tag is local or not. -/ diff --git a/lean/extra/attrs/around.lean b/lean/extra/attrs/around.lean deleted file mode 100644 index 70068d6..0000000 --- a/lean/extra/attrs/around.lean +++ /dev/null @@ -1,735 +0,0 @@ -import Lean -open Lean -open Lean.Meta -open Lean.Elab -open Lean.Elab.Command - -open System (FilePath) -open Std (HashMap) - -syntax (name := around_advice) "around_advice" str : attr -initialize registerTraceClass `around_advice - -initialize registerBuiltinAttribute { - name := `around_advice - descr :="around_advice print information" - add := fun src stx kind => do - dbg_trace "src: {src} | stx: {stx} | kind: {kind}" - let srcDecl : ConstantInfo ← getConstInfo src - dbg_trace "srcDecl:" - dbg_trace "\n {srcDecl.name}" - dbg_trace "\n {srcDecl.type}" - dbg_trace "\n {srcDecl.value?}" - srcDecl.updateName - return () - } - -abbrev RenameMap := HashMap Name Name - -def RenameMap.insertPair (m : RenameMap) : Name × Name → RenameMap - | (n3, n4) => m.insert n3 n4 - -initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameMap ← - registerSimplePersistentEnvExtension { - name := `renameMapExtension - addEntryFn := RenameMap.insertPair - addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es - initial := sorry - } - -/- -The key is Name × Name, and the value is RenameMap. -The entires are written into the `olean` files. -The functions `addEntryFn` tells us how to compute the values from the keys. -So the values are "just" a caching mechanism for the keys, where the keys tell us -what data is to be stored. --/ - -def findRename? (env : Environment) : Name → Option Name := - (renameExtension.getState env).find? - -/-- Add a (multiplicative → additive) name translation to the translations map. -/ -def insertRename (src tgt : Name) : CoreM Unit := do - if let some tgt' := findRename? (←getEnv) src then - throwError "Already exists translation {src} ↦ {tgt'}" - modifyEnv (renameExtension.addEntry · (src, tgt)) - -- | neat, we can trace like this?! - trace[to_additive] "Added translation {src} ↦ {tgt}." - -def getRenameMap (env : Environment) : RenameMap := - renameExtension.getState env - - - -partial def transformDecl (src: Name) (tgt: Name): CoreM Unit := do - let srcDecl ← getConstInfo src - dbg_trace "srcDecl:" - dbg_trace "\n {srcDecl.name}" - dbg_trace "\n {srcDecl.type}" - dbg_trace "\n {srcDecl.value?}" - return () - - --- #print AttributeImpl --- #print registerBuiltinAttribute - --- initialize registerBuiltinAttribute { --- name := `debug --- descr :="debug print information" --- add := fun src stx kind => do --- dbg_trace "src: {src} | stx: {stx} | kind: {kind}" --- let tgt := "foo" --- if let some tgt' := findRename? (← getEnv) src then --- throwError "{src} already has a to_additive translation {tgt'}." --- insertRename src tgt --- transformDecl src tgt --- return () --- } - --- syntax (name := align) "#align " ident ident : command --- --- @[commandElab align] def elabAlign : CommandElab --- | `(#align%$tk $id3:ident $id4:ident) => --- liftCoreM $ addNameAlignment id3.getId id4.getId --- | _ => throwUnsupportedSyntax --- --- syntax (name := lookup3) "#lookup3 " ident : command --- --- @[commandElab lookup3] def elabLookup3 : CommandElab --- | `(#lookup3%$tk $id3:ident) => do --- let n3 := id3.getId --- match getRenameMap (← getEnv) |>.find? n3 with --- | none => logInfoAt tk s!"name `{n3} not found" --- | some n4 => logInfoAt tk s!"{n4}" --- | _ => throwUnsupportedSyntax - - --- | Add an attribute stating that this function must be debug logged. - --- initialize ignoreArgsAttr : NameMapAttribute (List Nat) ← --- registerNameMapAttribute { --- name := `to_additive_ignore_args --- descr := "Auxiliary attribute for `to_additive` stating that certain arguments are not additivized." --- add := fun src stx => do --- let ids ← match stx with --- | `(attr|to_additive_ignore_args $[$ids:num]*) => pure <| ids.map (·.isNatLit?.get!) --- | _ => throwError "unexpected to_additive_ignore_args syntax {stx}" --- return ids.toList --- } --- --- /-- Gets the set of arguments that should be ignored for the given name --- (according to `@[to_additive_ignore_args ...]`). --- This value is used in `additiveTestAux`. -/ --- def ignore [Functor M] [MonadEnv M]: Name → M (Option (List Nat)) --- | n => (ignoreArgsAttr.find? · n) <$> getEnv --- --- initialize reorderAttr : NameMapAttribute (List Nat) ← --- registerNameMapAttribute { --- name := `to_additive_reorder --- descr := "Auxiliary attribute for `to_additive` that stores arguments that need to be reordered." --- add := fun decl stx => --- match stx with --- | `(attr|to_additive_reorder $[$ids:num]*) => pure <| Array.toList <| ids.map (·.isNatLit?.get!) --- | _ => throwError "unexpected to_additive_reorder syntax {stx}" --- } --- --- /-- Get the reorder list (defined using `@[to_additive_reorder ...]`) for the given declaration. -/ --- def getReorder [Functor M] [MonadEnv M]: Name → M (List Nat) --- | n => (reorderAttr.find? · n |>.getD []) <$> getEnv --- --- /-- Given a declaration name and an argument index, determines whether this index --- should be swapped with the next one. -/ --- def shouldReorder [Functor M] [MonadEnv M]: Name → Nat → M Bool --- | n, i => (i ∈ ·) <$> (getReorder n) --- --- initialize relevantArgAttr : NameMapAttribute (Nat) ← --- registerNameMapAttribute { --- name := `to_additive_relevant_arg --- descr := "Auxiliary attribute for `to_additive` stating which arguments are the types with a multiplicative structure." --- add := fun decl stx => --- match stx with --- | `(attr|to_additive_relevant_arg $id) => pure <| id.isNatLit?.get! --- | _ => throwError "unexpected to_additive_relevant_arg syntax {stx}" --- } --- --- /-- Given a declaration name and an argument index, determines whether it --- is relevant. This is used in `applyReplacementFun` where more detail on what it --- does can be found. -/ --- def isRelevant [Monad M] [MonadEnv M] (n : Name) (i : Nat) : M Bool := do --- match relevantArgAttr.find? (← getEnv) n with --- | some j => return i == j --- | none => return i == 0 --- --- /- Maps multiplicative names to their additive counterparts. -/ --- initialize translations : NameMapExtension Name ← --- mkNameMapExtension Name `translations --- --- /-- Get the multiplicative → additive translation for the given name. -/ --- def findTranslation? (env : Environment) : Name → Option Name := --- (ToAdditive.translations.getState env).find? --- --- /-- Add a (multiplicative → additive) name translation to the translations map. -/ --- def insertTranslation (src tgt : Name) : CoreM Unit := do --- if let some tgt' := findTranslation? (←getEnv) src then --- throwError "Already exists translation {src} ↦ {tgt'}" --- modifyEnv (ToAdditive.translations.addEntry · (src, tgt)) --- trace[to_additive] "Added translation {src} ↦ {tgt}." --- --- /-- Get whether or not the replace-all flag is set. If this is true, then the --- additiveTest heuristic is not used and all instances of multiplication are replaced. --- You can enable this with `@[to_additive!]`-/ --- def replaceAll [Functor M] [MonadOptions M] : M Bool := --- (·.getBool `to_additive.replaceAll) <$> getOptions --- --- variable [Monad M] [MonadOptions M] [MonadEnv M] --- --- /-- Auxilliary function for `additiveTest`. The bool argument *only* matters when applied --- to exactly a constant. -/ --- private def additiveTestAux: Bool → Expr → M Bool --- | b, Expr.const n _ _ => return b || (findTranslation? (← getEnv) n).isSome --- | b, (Expr.app e a _) => do --- if (← additiveTestAux true e) then --- return true --- if let (some n) := e.getAppFn.constName? then --- if let (some l) ← ignore n then --- if e.getAppNumArgs + 1 ∈ l then --- return true --- additiveTestAux false a --- | b, (Expr.lam n e t _) => additiveTestAux false t --- | b, (Expr.forallE n e t _) => additiveTestAux false t --- | b, (Expr.letE n g e body _) => --- return (←additiveTestAux false e) && (← additiveTestAux false body) --- | b, _ => return true --- --- /-- --- `additiveTest e` tests whether the expression `e` contains no constant --- `nm` that is not applied to any arguments, and such that `translations.find?[nm] = none`. --- This is used in `@[to_additive]` for deciding which subexpressions to transform: we only transform --- constants if `additiveTest` applied to their first argument returns `true`. --- This means we will replace expression applied to e.g. `α` or `α × β`, but not when applied to --- e.g. `Nat` or `ℝ × α`. --- We ignore all arguments specified by the `ignore` `NameMap`. --- If `replaceAll` is `true` the test always returns `true`. --- -/ --- def additiveTest (e : Expr) : M Bool := do --- if (←replaceAll) then --- return true --- else --- additiveTestAux false e - -/-- -`e.applyReplacementFun f test` applies `f` to each identifier -(inductive type, defined function etc) in an expression, unless -* The identifier occurs in an application with first argument `arg`; and -* `test arg` is false. -However, if `f` is in the dictionary `relevant`, then the argument `relevant.find f` -is tested, instead of the first argument. - -Reorder contains the information about what arguments to reorder: -e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorder.find g = some [1]`. -We assume that all functions where we want to reorder arguments are fully applied. -This can be done by applying `etaExpand` first. --/ --- def applyReplacementFun : Expr → MetaM Expr := --- Lean.Expr.replaceRecMeta fun r e => do --- trace[to_additive_detail] "applyReplacementFun: replace at {e}" --- match e with --- | Expr.lit (Literal.natVal 1) _ => pure <| mkNatLit 0 --- | Expr.const n₀ ls _ => do --- let n₁ := Name.mapPrefix (findTranslation? <|← getEnv) n₀ --- trace[to_additive_detail] "applyReplacementFun: {n₀} → {n₁}" --- let ls : List Level ← (do -- [todo] just get Lean to figure out the levels? --- if ← shouldReorder n₀ 1 then --- return ls.get! 1::ls.head!::ls.drop 2 --- return ls) --- return some $ Lean.mkConst n₁ ls --- | Expr.app g x _ => do --- let gf := g.getAppFn --- if let some nm := gf.constName? then --- let gArgs := g.getAppArgs --- -- e = `(nm y₁ .. yₙ x) --- trace[to_additive_detail] "applyReplacementFun: app {nm} {gArgs} {x}" --- if gArgs.size > 0 then --- let c1 ← shouldReorder nm gArgs.size --- let c2 ← additiveTest gArgs[0] --- if c1 && c2 then --- -- interchange `x` and the last argument of `g` --- let x ← r x --- let gf ← r g.appFn! --- let ga ← r g.appArg! --- let e₂ := mkApp2 gf x ga --- trace[to_additive_detail] "applyReplacementFun: reordering {nm}: {x} ↔ {ga}\nBefore: {e}\nAfter: {e₂}" --- return some e₂ --- let c1 ← isRelevant nm gArgs.size --- let c2 := gf.isConst --- let c3 ← additiveTest x --- if c1 && c2 && not c3 then --- -- the test failed, so don't update the function body. --- trace[to_additive_detail] "applyReplacementFun: isRelevant and test failed: {nm} {gArgs} {x}" --- let x ← r x --- let args ← gArgs.mapM r --- return some $ mkApp (mkAppN gf args) x --- return e.updateApp! (← r g) (← r x) --- | _ => return none --- --- /-- Eta expands `e` at most `n` times.-/ --- def etaExpandN (n : Nat) (e : Expr): MetaM Expr := do --- forallBoundedTelescope (← inferType e) (some n) fun xs _ => mkLambdaFVars xs (mkAppN e xs) --- --- /-- `e.expand` eta-expands all expressions that have as head a constant `n` in --- `reorder`. They are expanded until they are applied to one more argument than the maximum in --- `reorder.find n`. -/ --- def expand (e : Expr) : MetaM Expr := do --- let e₂ ←e.replaceRecMeta $ fun r e => do --- let e0 := e.getAppFn --- let es := e.getAppArgs --- let some e0n := e0.constName? | return none --- let reorder ← getReorder e0n --- if reorder.isEmpty then --- -- no need to expand if nothing needs reordering --- return none --- let e' := mkAppN e0 $ ← es.mapM r --- let needed_n := reorder.foldr Nat.max 0 + 1 --- if needed_n ≤ es.size then --- return some e' --- else --- -- in this case, we need to reorder arguments that are not yet --- -- applied, so first η-expand the function. --- let e' ← etaExpandN (needed_n - es.size) e' --- return some $ e' --- trace[to_additive_detail] "expand:\nBefore: {e}\nAfter: {e₂}" --- return e₂ --- --- /-- Run applyReplacementFun on the given `srcDecl` to make a new declaration with name `tgt` -/ --- def updateDecl --- (tgt : Name) (srcDecl : ConstantInfo) --- : MetaM ConstantInfo := do --- let mut decl := srcDecl.updateName tgt --- decl := decl.updateType $ (← applyReplacementFun (← expand decl.type)) --- if let some v := decl.value? then --- decl := decl.updateValue (← applyReplacementFun (← expand v)) --- return decl --- --- /-- Lean 4 makes declarations which are not internal --- (that is, head string starts with `_`) but which should be transformed. --- eg `proof_1` in `Lean.Meta.mkAuxDefinitionFor` this might be better fixed in core. --- This method is polyfill for that. -/ --- def isInternal' : Name → Bool --- | n@(Name.str _ s _) => (s.startsWith "proof_") || (Name.isInternal n) --- | n => Name.isInternal n --- --- /-- transform the declaration `src` and all declarations `pre._proof_i` occurring in `src` --- using the transforms dictionar declaration {src} which is in the namespace {pre}, but does not have the `@[to_additive]` attribute. This is not supported. Workaround: move {src} to a different namespace." --- let env ← getEnv --- -- we find the additive name of `src` --- let tgt := src.mapPrefix (fun n => if n == pre then some tgt_pre else none) --- -- we skip if we already transformed this declaration before --- if env.contains tgt then --- return --- let srcDecl ← getConstInfo src --- -- we first transform all the declarations of the form `pre._proof_i` --- for n in srcDecl.type.listNamesWithPrefix pre do --- transformDeclAux pre tgt_pre n --- if let some value := srcDecl.value? then --- for n in value.listNamesWithPrefix pre do --- transformDeclAux pre tgt_pre n --- -- now transform the source declaration --- let trgDecl : ConstantInfo ← MetaM.run' $ updateDecl tgt srcDecl --- if ¬ trgDecl.hasValue then --- throwError "Expected {trgDecl.name} to have a value." --- trace[to_additive] "generating\n{trgDecl.name} :=\n {trgDecl.value!}" --- try --- -- make sure that the type is correct, --- -- and emit a more helpful error message if it fails --- discard <| MetaM.run' <| inferType trgDecl.value! --- catch --- | Exception.error stx msg => throwError "@[to_additive] failed. --- Type mismatch in additive declaration. For help, see the docstring --- of `to_additive.attr`, section `Troubleshooting`. --- Failed to add declaration\n{trgDecl.name}:\n{msg}" --- | e => panic! "unreachable" --- addAndCompile trgDecl.toDeclaration! --- if isProtected (← getEnv) src then --- setEnv $ addProtected (← getEnv) tgt --- --- /-- This should copy all of the attributes on src to tgt. --- At the moment it only copies `simp` attributes because attributes --- are not stored by the environment. --- --- [todo] add more attributes. A change is coming to core that should --- allow us to iterate the attributes applied to a given decalaration. --- -/ --- def copyAttributes (src tgt : Name) : CoreM Unit := do --- -- [todo] other simp theorems --- let some ext ← getSimpExtension? `simp | return () --- let thms ← ext.getTheorems --- if (¬ thms.isLemma src) || thms.isLemma tgt then --- return () --- -- [todo] how to get prio data from SimpTheorems? --- MetaM.run' $ Lean.Meta.addSimpTheorem ext tgt --- (post := true) --- (inv := false) --- (attrKind := AttributeKind.global) --- (prio := 1000) --- return () --- --- /-- --- Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and --- the body using the `translations` dictionary. --- This is used to implement `@[to_additive]`. --- -/ --- def transformDecl (src tgt : Name) : CoreM Unit := do --- transformDeclAux src tgt src --- let eqns? ← MetaM.run' (getEqnsFor? src true) --- -- now transform all of the equational lemmas --- if let some eqns := eqns? then --- for src_eqn in eqns do --- transformDeclAux src tgt src_eqn --- -- [todo] copy attributes for equations --- -- [todo] add equation lemmas to tgt_eqn --- copyAttributes src tgt --- return () --- /-- --- Find the first argument of `nm` that has a multiplicative type-class on it. --- Returns 1 if there are no types with a multiplicative class as arguments. --- E.g. `prod.group` returns 1, and `pi.has_one` returns 2. --- -/ --- def firstMultiplicativeArg (nm : Name) : MetaM (Option Nat) := do --- let d ← getConstInfo nm --- forallTelescopeReducing (← getConstInfo nm).type fun xs _ => do --- -- xs are the arguments to the constant --- let xs := xs.toList --- let l ← xs.mapM fun x => do --- -- x is an argument and i is the index --- -- write `x : (y₀ : α₀) → ... → (yₙ : αₙ) → tgt_fn tgt_args₀ ... tgt_argsₘ` --- forallTelescopeReducing (← inferType x) fun ys tgt => do --- let (tgt_fn, tgt_args) := tgt.getAppFnArgs --- let n_bi := ys.size --- if let some c := tgt.getAppFn.constName? then --- if findTranslation? (← getEnv) c |>.isNone then --- return [] --- return tgt_args.toList.filterMap fun tgt_arg => --- xs.findIdx? fun x => Expr.containsFVar tgt_arg x.fvarId! --- trace[to_additive_detail] "firstMultiplicativeArg: {l}" --- match l.join with --- | [] => return none --- | (head :: tail) => return some <| tail.foldr Nat.min head --- --- --- /-- `ValueType` is the type of the arguments that can be provided to `to_additive`. -/ --- structure ValueType : Type where --- /-- Replace all multiplicative declarations, do not use the heuristic. -/ --- replaceAll : Bool := false --- /-- View the trace of the to_additive procedure. --- Equivalent to `set_option trace.to_additive true`. -/ --- trace : Bool := false --- /-- The name of the target (the additive declaration).-/ --- tgt : Name := Name.anonymous --- /-- An optional doc string.-/ --- doc : Option String := none --- /-- If `allow_auto_name` is `false` (default) then --- `@[to_additive]` will check whether the given name can be auto-generated. -/ --- allowAutoName : Bool := false --- deriving Repr --- --- /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. -/ --- def addCommPrefix : Bool → String → String --- | true, s => "comm" ++ s.capitalize --- | false, s => s --- --- /-- Dictionary used by `to_additive.guess_name` to autogenerate names. --- [todo] update to Lean 4 naming -/ --- private def guessNameDict : Bool → List String → List String --- | is_comm, ("one" :: "le" :: s) => addCommPrefix is_comm "nonneg" :: guessNameDict false s --- | is_comm, ("one" :: "lt" :: s) => addCommPrefix is_comm "pos" :: guessNameDict false s --- | is_comm, ("le" :: "one" :: s) => addCommPrefix is_comm "nonpos" :: guessNameDict false s --- | is_comm, ("lt" :: "one" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s --- | is_comm, ("mul" :: "single" :: s) => addCommPrefix is_comm "single" :: guessNameDict false s --- | is_comm, ("mul" :: "support" :: s) => addCommPrefix is_comm "support" :: guessNameDict false s --- | is_comm, ("mul" :: "tsupport" :: s) => addCommPrefix is_comm "tsupport" :: guessNameDict false s --- | is_comm, ("mul" :: "indicator" :: s) => addCommPrefix is_comm "indicator" :: guessNameDict false s --- | is_comm, ("mul" :: s) => addCommPrefix is_comm "add" :: guessNameDict false s --- | is_comm, ("smul" :: s) => addCommPrefix is_comm "vadd" :: guessNameDict false s --- | is_comm, ("inv" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s --- | is_comm, ("div" :: s) => addCommPrefix is_comm "sub" :: guessNameDict false s --- | is_comm, ("one" :: s) => addCommPrefix is_comm "zero" :: guessNameDict false s --- | is_comm, ("prod" :: s) => addCommPrefix is_comm "sum" :: guessNameDict false s --- | is_comm, ("finprod" :: s) => addCommPrefix is_comm "finsum" :: guessNameDict false s --- | is_comm, ("pow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s --- | is_comm, ("npow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s --- | is_comm, ("zpow" :: s) => addCommPrefix is_comm "zsmul" :: guessNameDict false s --- | is_comm, ("monoid" :: s) => ("add_" ++ addCommPrefix is_comm "monoid") :: guessNameDict false s --- | is_comm, ("submonoid" :: s) => ("add_" ++ addCommPrefix is_comm "submonoid") :: guessNameDict false s --- | is_comm, ("group" :: s) => ("add_" ++ addCommPrefix is_comm "group") :: guessNameDict false s --- | is_comm, ("subgroup" :: s) => ("add_" ++ addCommPrefix is_comm "subgroup") :: guessNameDict false s --- | is_comm, ("semigroup" :: s) => ("add_" ++ addCommPrefix is_comm "semigroup") :: guessNameDict false s --- | is_comm, ("magma" :: s) => ("add_" ++ addCommPrefix is_comm "magma") :: guessNameDict false s --- | is_comm, ("haar" :: s) => ("add_" ++ addCommPrefix is_comm "haar") :: guessNameDict false s --- | is_comm, ("prehaar" :: s) => ("add_" ++ addCommPrefix is_comm "prehaar") :: guessNameDict false s --- | is_comm, ("unit" :: s) => ("add_" ++ addCommPrefix is_comm "unit") :: guessNameDict false s --- | is_comm, ("units" :: s) => ("add_" ++ addCommPrefix is_comm "units") :: guessNameDict false s --- | is_comm, ("comm" :: s) => guessNameDict true s --- | is_comm, (x :: s) => (addCommPrefix is_comm x :: guessNameDict false s) --- | true, [] => ["comm"] --- | false, [] => [] --- --- /-- Autogenerate target name for `to_additive`. -/ --- def guessName : String → String := --- -- [todo] replace with camelcase logic? --- String.mapTokens ''' $ --- fun s => String.intercalate (String.singleton '_') $ --- guessNameDict false (s.splitOn "_") --- --- /-- Return the provided target name or autogenerate one if one was not provided. -/ --- def targetName (src tgt : Name) (allowAutoName : Bool) : CoreM Name := do --- let res ← do --- if tgt.getPrefix != Name.anonymous || allowAutoName then --- return tgt --- let (Name.str pre s _) := src | throwError "to_additive: can't transport {src}" --- let tgt_auto := guessName s --- if tgt.toString == tgt_auto then --- dbg_trace "{src}: correctly autogenerated target name {tgt_auto}, you may remove the explicit {tgt} argument." --- let pre := pre.mapPrefix <| findTranslation? (← getEnv) --- if tgt == Name.anonymous then --- return Name.mkStr pre tgt_auto --- else --- return Name.mkStr pre tgt.toString --- if res == src && tgt != src then --- throwError "to_additive: can't transport {src} to itself." --- return res --- --- private def proceedFieldsAux (src tgt : Name) (f : Name → CoreM (List String)) : CoreM Unit := do --- let srcFields ← f src --- let tgtFields ← f tgt --- if srcFields.length != tgtFields.length then --- throwError "Failed to map fields of {src}, {tgt} with {srcFields} ↦ {tgtFields}" --- for (srcField, tgtField) in List.zip srcFields tgtFields do --- if srcField != tgtField then --- insertTranslation (src ++ srcField) (tgt ++ tgtField) --- --- /-- Add the structure fields of `src` to the translations dictionary --- so that future uses of `to_additive` will map them to the corresponding `tgt` fields. -/ --- def proceedFields (src tgt : Name) : CoreM Unit := do --- let env : Environment ← getEnv --- let aux := proceedFieldsAux src tgt --- aux (fun n => do --- let fields := if isStructure env n then getStructureFieldsFlattened env n else #[] --- return fields |> .map Name.toString |> Array.toList --- ) --- -- [todo] run to_additive on the constructors of n: --- -- aux (fun n => (env.constructorsOf n).mmap $ ... --- --- private def elabToAdditiveAux --- (replaceAll trace : Bool) (tgt : Option Syntax) (doc : Option Syntax) : ValueType := --- { replaceAll := replaceAll --- trace := trace --- tgt := match tgt with | some tgt => tgt.getId | none => Name.anonymous --- doc := doc.bind (·.isStrLit?) --- allowAutoName := false --- } --- --- private def elabToAdditive : Syntax → CoreM ValueType --- | `(attr| to_additive $[!%$replaceAll]? $[?%$trace]? $[$tgt]? $[$doc]?) => --- return elabToAdditiveAux replaceAll.isSome trace.isSome tgt doc --- | _ => throwUnsupportedSyntax --- --- /-! --- The attribute `to_additive` can be used to automatically transport theorems --- and definitions (but not inductive types and structures) from a multiplicative --- theory to an additive theory. --- --- To use this attribute, just write: --- --- ``` --- @[to_additive] --- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm --- ``` --- --- This code will generate a theorem named `add_comm'`. It is also --- possible to manually specify the name of the new declaration: --- --- ``` --- @[to_additive add_foo] --- theorem foo := sorry --- ``` --- --- An existing documentation string will _not_ be automatically used, so if the theorem or definition --- has a doc string, a doc string for the additive version should be passed explicitly to --- `to_additive`. --- --- ``` --- /-- Multiplication is commutative -/ --- @[to_additive "Addition is commutative"] --- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm --- ``` --- --- The transport tries to do the right thing in most cases using several --- heuristics described below. However, in some cases it fails, and --- requires manual intervention. --- --- If the declaration to be transported has attributes which need to be --- copied to the additive version, then `to_additive` should come last: --- --- ``` --- @[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x --- ``` --- --- Currently only the `simp` attribute is supported. --- --- ## Implementation notes --- --- The transport process generally works by taking all the names of --- identifiers appearing in the name, type, and body of a declaration and --- creating a new declaration by mapping those names to additive versions --- using a simple string-based dictionary and also using all declarations --- that have previously been labeled with `to_additive`. --- --- In the `mul_comm'` example above, `to_additive` maps: --- * `mul_comm'` to `add_comm'`, --- * `comm_semigroup` to `add_comm_semigroup`, --- * `x * y` to `x + y` and `y * x` to `y + x`, and --- * `comm_semigroup.mul_comm'` to `add_comm_semigroup.add_comm'`. --- --- ### Heuristics --- --- `to_additive` uses heuristics to determine whether a particular identifier has to be --- mapped to its additive version. The basic heuristic is --- --- * Only map an identifier to its additive version if its first argument doesn't --- contain any unapplied identifiers. --- --- Examples: --- * `@Mul.mul Nat n m` (i.e. `(n * m : Nat)`) will not change to `+`, since its --- first argument is `Nat`, an identifier not applied to any arguments. --- * `@Mul.mul (α × β) x y` will change to `+`. It's first argument contains only the identifier --- `prod`, but this is applied to arguments, `α` and `β`. --- * `@Mul.mul (α × Int) x y` will not change to `+`, since its first argument contains `Int`. --- --- The reasoning behind the heuristic is that the first argument is the type which is "additivized", --- and this usually doesn't make sense if this is on a fixed type. --- --- There are some exceptions to this heuristic: --- --- * Identifiers that have the `@[to_additive]` attribute are ignored. --- For example, multiplication in `↥Semigroup` is replaced by addition in `↥AddSemigroup`. --- * If an identifier `d` has attribute `@[to_additive_relevant_arg n]` then the argument --- in position `n` is checked for a fixed type, instead of checking the first argument. --- `@[to_additive]` will automatically add the attribute `@[to_additive_relevant_arg n]` to a --- declaration when the first argument has no multiplicative type-class, but argument `n` does. --- * If an identifier has attribute `@[to_additive_ignore_args n1 n2 ...]` then all the arguments in --- positions `n1`, `n2`, ... will not be checked for unapplied identifiers (start counting from 1). --- For example, `cont_mdiff_map` has attribute `@[to_additive_ignore_args 21]`, which means --- that its 21st argument `(n : WithTop Nat)` can contain `Nat` --- (usually in the form `has_top.top Nat ...`) and still be additivized. --- So `@Mul.mul (C^∞⟮I, N; I', G⟯) _ f g` will be additivized. --- --- ### Troubleshooting --- --- If `@[to_additive]` fails because the additive declaration raises a type mismatch, there are --- various things you can try. --- The first thing to do is to figure out what `@[to_additive]` did wrong by looking at the type --- mismatch error. --- --- * Option 1: It additivized a declaration `d` that should remain multiplicative. Solution: --- * Make sure the first argument of `d` is a type with a multiplicative structure. If not, can you --- reorder the (implicit) arguments of `d` so that the first argument becomes a type with a --- multiplicative structure (and not some indexing type)? --- The reason is that `@[to_additive]` doesn't additivize declarations if their first argument --- contains fixed types like `Nat` or `ℝ`. See section Heuristics. --- If the first argument is not the argument with a multiplicative type-class, `@[to_additive]` --- should have automatically added the attribute `@[to_additive_relevant_arg]` to the declaration. --- You can test this by running the following (where `d` is the full name of the declaration): --- ``` --- #eval (do isRelevant `d >>= trace) --- ``` --- The expected output is `n` where the `n`-th argument of `d` is a type (family) with a --- multiplicative structure on it. If you get a different output (or a failure), you could add --- the attribute `@[to_additive_relevant_arg n]` manually, where `n` is an argument with a --- multiplicative structure. --- * Option 2: It didn't additivize a declaration that should be additivized. --- This happened because the heuristic applied, and the first argument contains a fixed type, --- like `Nat` or `ℝ`. Solutions: --- * If the fixed type has an additive counterpart (like `↥Semigroup`), give it the `@[to_additive]` --- attribute. --- * If the fixed type occurs inside the `k`-th argument of a declaration `d`, and the --- `k`-th argument is not connected to the multiplicative structure on `d`, consider adding --- attribute `[to_additive_ignore_args k]` to `d`. --- * If you want to disable the heuristic and replace all multiplicative --- identifiers with their additive counterpart, use `@[to_additive!]`. --- * Option 3: Arguments / universe levels are incorrectly ordered in the additive version. --- This likely only happens when the multiplicative declaration involves `pow`/`^`. Solutions: --- * Ensure that the order of arguments of all relevant declarations are the same for the --- multiplicative and additive version. This might mean that arguments have an "unnatural" order --- (e.g. `Monoid.npow n x` corresponds to `x ^ n`, but it is convenient that `Monoid.npow` has this --- argument order, since it matches `AddMonoid.nsmul n x`. --- * If this is not possible, add the `[to_additive_reorder k]` to the multiplicative declaration --- to indicate that the `k`-th and `(k+1)`-st arguments are reordered in the additive version. --- --- If neither of these solutions work, and `to_additive` is unable to automatically generate the --- additive version of a declaration, manually write and prove the additive version. --- Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to --- `multiplicative G`. --- Afterwards, apply the attribute manually: --- --- ``` --- attribute [to_additive foo_add_bar] foo_bar --- ``` --- --- This will allow future uses of `to_additive` to recognize that --- `foo_bar` should be replaced with `foo_add_bar`. --- --- ### Handling of hidden definitions --- --- Before transporting the “main” declaration `src`, `to_additive` first --- scans its type and value for names starting with `src`, and transports --- them. This includes auxiliary definitions like `src._match_1`, --- `src._proof_1`. --- --- In addition to transporting the “main” declaration, `to_additive` transports --- its equational lemmas and tags them as equational lemmas for the new declaration, --- attributes present on the original equational lemmas are also transferred first (notably --- `_refl_lemma`). --- --- ### Structure fields and constructors --- --- If `src` is a structure, then `to_additive` automatically adds --- structure fields to its mapping, and similarly for constructors of --- inductive types. --- --- For new structures this means that `to_additive` automatically handles --- coercions, and for old structures it does the same, if ancestry --- information is present in `@[ancestor]` attributes. The `ancestor` --- attribute must come before the `to_additive` attribute, and it is --- essential that the order of the base structures passed to `ancestor` matches --- between the multiplicative and additive versions of the structure. --- --- ### Name generation --- --- * If `@[to_additive]` is called without a `name` argument, then the --- new name is autogenerated. First, it takes the longest prefix of --- the source name that is already known to `to_additive`, and replaces --- this prefix with its additive counterpart. Second, it takes the last --- part of the name (i.e., after the last dot), and replaces common --- name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. --- --- * [todo] Namespaces can be transformed using `map_namespace`. For example: --- ``` --- run_cmd to_additive.map_namespace `quotient_group `quotient_add_group --- ``` --- --- Later uses of `to_additive` on declarations in the `quotient_group` --- namespace will be created in the `quotient_add_group` namespaces. --- --- * If `@[to_additive]` is called with a `name` argument `new_name` --- /without a dot/, then `to_additive` updates the prefix as described --- above, then replaces the last part of the name with `new_name`. --- --- * If `@[to_additive]` is called with a `name` argument --- `new_namespace.new_name` /with a dot/, then `to_additive` uses this --- new name as is. --- --- As a safety check, in the first case `to_additive` double checks --- that the new name differs from the original one. --- --- -/ -def foo : Int := 10 diff --git a/lean/extra/attrs/dummy.lean b/lean/extra/attrs/dummy.lean index b4d49da..d9517d5 100644 --- a/lean/extra/attrs/dummy.lean +++ b/lean/extra/attrs/dummy.lean @@ -3,16 +3,22 @@ open Lean namespace Attr syntax (name := dummy_attr) "dummy_attr" term : attr -initialize registerTraceClass `dummy_attr +/- +This uses a low level attribute registration function. We declare the attribute +with `registerBuiltinAttribute`. The `name` field is the name of the attribute, which +should match with the `syntax` above for parsing. The `descr` is the textual description +of the attribute used for docstrings. The `add` function is run when the attribute is applied to a +declaration of name `declName`. `stx` is the syntax of the attribute including arguments +-/ initialize registerBuiltinAttribute { name := `dummy_attr descr :="dummy_attr print information" - add := fun src stx kind => do + add := fun declName stx kind => do let num : Nat := stx[1].toNat dbg_trace "number + 1: {num + 1}" - dbg_trace "src: {src} | stx: {stx} | kind: {kind}" - let srcDecl ← getConstInfo src + dbg_trace "declName: {declName} | stx: {stx} | kind: {kind}" + let srcDecl ← getConstInfo declName dbg_trace "srcDecl:" dbg_trace " name: {srcDecl.name}" dbg_trace " type: {srcDecl.type}" @@ -20,7 +26,3 @@ initialize registerBuiltinAttribute { return () } --- QUESTION: Can I uncomment this? --- @[dummy_attr "foo"] --- def foo : Int := 42 - diff --git a/lean/extra/attrs/parameteric.lean b/lean/extra/attrs/parameteric.lean index caca66e..063d592 100644 --- a/lean/extra/attrs/parameteric.lean +++ b/lean/extra/attrs/parameteric.lean @@ -5,6 +5,14 @@ open Lean -- used to connect to the corresponding attribute. syntax (name := myParam) "myParam" num "important"? : attr +/- + +This declarares the attribute `myParamAttr`, which is parametrized +by a value of type `(Nat × Bool)`. The `getParam` function describes how to build +a value of `(Nat × Bool)` given the raw syntax declared by `myParam` above. +The `afterSet` function can be used as a finalizer to perform processing once we have +a parsed value. +-/ initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← registerParametricAttribute { name := `myParam /- @@ -13,11 +21,11 @@ initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← descr := "parametric attribute containing a priority and flag" getParam := fun _ stx => match stx with - | `(attr| myParam $prio:num) => - return (prio.getNat, false) - | `(attr| myParam $prio:num important) => + | `(attr| myParam $prio:num) => + return (prio.getNat, false) + | `(attr| myParam $prio:num important) => return (prio.getNat, true) - | _ => throwError "unexpected foo attribute" + | _ => throwError "unexpected foo attribute" afterSet := fun declName val => do IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}" } diff --git a/lean/extra/attrs/simp.lean b/lean/extra/attrs/simp.lean index 2cd0795..467146f 100644 --- a/lean/extra/attrs/simp.lean +++ b/lean/extra/attrs/simp.lean @@ -1,7 +1,5 @@ import Lean - - /-- We declare a simplifcation attribute using the keyword `register_simp_attr`, From d381cba5681582407b46fe554b0e1504d9f28132 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jul 2022 22:30:13 +0100 Subject: [PATCH 6/6] refresh md as well --- md/extra/attributes.md | 10 +- md/extra/attrs/around.md | 772 ---------------------------------- md/extra/attrs/dummy.md | 19 +- md/extra/attrs/parameteric.md | 16 +- 4 files changed, 28 insertions(+), 789 deletions(-) delete mode 100644 md/extra/attrs/around.md diff --git a/md/extra/attributes.md b/md/extra/attributes.md index 258ac51..82d0927 100644 --- a/md/extra/attributes.md +++ b/md/extra/attributes.md @@ -1,8 +1,8 @@ ```lean import lean.extra.attrs.dummy import lean.extra.attrs.tag -import lean.extra.attrs.parametric -import lean.extra.attrs.simp +-- import lean.extra.attrs.parametric +-- import lean.extra.attrs.simp ``` # Attributes @@ -12,7 +12,7 @@ They are similar to Python's decorators and Rust's proc-macros. Unfortunately, it turns out that attributes must be defined in a separate module, so we will bounce between this file and the files in the `attrs/` folder which -contain the implementations of the attributes. We'll see you at +contain the implementations of the attributes. We'll see you at [`./attrs/tag.lean`](./attrs/tag.lean). ## Tag attributes with `myTag` @@ -44,7 +44,7 @@ This simplified mechanism exists to allow us to easily tag definitions of intere ## Parametric attributes with `myParam` A parametric attribute is like a tag attribute, while adding support for -parameters in the attribute. +parameters in the attribute. We shall add an attribute called `myParam`, which recieves two parameters, a priority, denoted by a natural number, and an optional tag `important`. @@ -100,7 +100,7 @@ Below is an example of a declaration that does not have any value. ```lean @[dummy_attr 52] -class bar +class bar -- number + 1: 53 -- src: bar | stx: (Attr.dummy_attr "dummy_attr" (num "52")) | kind: global -- srcDecl: diff --git a/md/extra/attrs/around.md b/md/extra/attrs/around.md deleted file mode 100644 index bfd5e64..0000000 --- a/md/extra/attrs/around.md +++ /dev/null @@ -1,772 +0,0 @@ -```lean -import Lean -open Lean -open Lean.Meta -open Lean.Elab -open Lean.Elab.Command - -open System (FilePath) -open Std (HashMap) - -syntax (name := around_advice) "around_advice" str : attr -initialize registerTraceClass `around_advice - -initialize registerBuiltinAttribute { - name := `around_advice - descr :="around_advice print information" - add := fun src stx kind => do - dbg_trace "src: {src} | stx: {stx} | kind: {kind}" - let srcDecl : ConstantInfo ← getConstInfo src - dbg_trace "srcDecl:" - dbg_trace "\n {srcDecl.name}" - dbg_trace "\n {srcDecl.type}" - dbg_trace "\n {srcDecl.value?}" - srcDecl.updateName - return () - } - -abbrev RenameMap := HashMap Name Name - -def RenameMap.insertPair (m : RenameMap) : Name × Name → RenameMap - | (n3, n4) => m.insert n3 n4 - -initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameMap ← - registerSimplePersistentEnvExtension { - name := `renameMapExtension - addEntryFn := RenameMap.insertPair - addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es - initial := sorry - } -``` - -The key is Name × Name, and the value is RenameMap. -The entires are written into the `olean` files. -The functions `addEntryFn` tells us how to compute the values from the keys. -So the values are "just" a caching mechanism for the keys, where the keys tell us -what data is to be stored. - -```lean -def findRename? (env : Environment) : Name → Option Name := - (renameExtension.getState env).find? -``` - -- Add a (multiplicative → additive) name translation to the translations map. - -def insertRename (src tgt : Name) : CoreM Unit := do - if let some tgt' := findRename? (←getEnv) src then - throwError "Already exists translation {src} ↦ {tgt'}" - modifyEnv (renameExtension.addEntry · (src, tgt)) - -- | neat, we can trace like this?! - trace[to_additive] "Added translation {src} ↦ {tgt}." - -def getRenameMap (env : Environment) : RenameMap := - renameExtension.getState env - - - -partial def transformDecl (src: Name) (tgt: Name): CoreM Unit := do - let srcDecl ← getConstInfo src - dbg_trace "srcDecl:" - dbg_trace "\n {srcDecl.name}" - dbg_trace "\n {srcDecl.type}" - dbg_trace "\n {srcDecl.value?}" - return () - - --- #print AttributeImpl --- #print registerBuiltinAttribute - --- initialize registerBuiltinAttribute { --- name := `debug --- descr :="debug print information" --- add := fun src stx kind => do --- dbg_trace "src: {src} | stx: {stx} | kind: {kind}" --- let tgt := "foo" --- if let some tgt' := findRename? (← getEnv) src then --- throwError "{src} already has a to_additive translation {tgt'}." --- insertRename src tgt --- transformDecl src tgt --- return () --- } - --- syntax (name := align) "#align " ident ident : command --- --- @[commandElab align] def elabAlign : CommandElab --- | `(#align%$tk $id3:ident $id4:ident) => --- liftCoreM $ addNameAlignment id3.getId id4.getId --- | _ => throwUnsupportedSyntax --- --- syntax (name := lookup3) "#lookup3 " ident : command --- --- @[commandElab lookup3] def elabLookup3 : CommandElab --- | `(#lookup3%$tk $id3:ident) => do --- let n3 := id3.getId --- match getRenameMap (← getEnv) |>.find? n3 with --- | none => logInfoAt tk s!"name `{n3} not found" --- | some n4 => logInfoAt tk s!"{n4}" --- | _ => throwUnsupportedSyntax - - --- | Add an attribute stating that this function must be debug logged. - --- initialize ignoreArgsAttr : NameMapAttribute (List Nat) ← --- registerNameMapAttribute { --- name := `to_additive_ignore_args --- descr := "Auxiliary attribute for `to_additive` stating that certain arguments are not additivized." --- add := fun src stx => do --- let ids ← match stx with --- | `(attr|to_additive_ignore_args $[$ids:num]*) => pure <| ids.map (·.isNatLit?.get!) --- | _ => throwError "unexpected to_additive_ignore_args syntax {stx}" --- return ids.toList --- } --- --- /-- Gets the set of arguments that should be ignored for the given name --- (according to `@[to_additive_ignore_args ...]`). --- This value is used in `additiveTestAux`. - --- def ignore [Functor M] [MonadEnv M]: Name → M (Option (List Nat)) --- | n => (ignoreArgsAttr.find? · n) <$> getEnv --- --- initialize reorderAttr : NameMapAttribute (List Nat) ← --- registerNameMapAttribute { --- name := `to_additive_reorder --- descr := "Auxiliary attribute for `to_additive` that stores arguments that need to be reordered." --- add := fun decl stx => --- match stx with --- | `(attr|to_additive_reorder $[$ids:num]*) => pure <| Array.toList <| ids.map (·.isNatLit?.get!) --- | _ => throwError "unexpected to_additive_reorder syntax {stx}" --- } --- --- /-- Get the reorder list (defined using `@[to_additive_reorder ...]`) for the given declaration. - --- def getReorder [Functor M] [MonadEnv M]: Name → M (List Nat) --- | n => (reorderAttr.find? · n |>.getD []) <$> getEnv --- --- /-- Given a declaration name and an argument index, determines whether this index --- should be swapped with the next one. - --- def shouldReorder [Functor M] [MonadEnv M]: Name → Nat → M Bool --- | n, i => (i ∈ ·) <$> (getReorder n) --- --- initialize relevantArgAttr : NameMapAttribute (Nat) ← --- registerNameMapAttribute { --- name := `to_additive_relevant_arg --- descr := "Auxiliary attribute for `to_additive` stating which arguments are the types with a multiplicative structure." --- add := fun decl stx => --- match stx with --- | `(attr|to_additive_relevant_arg $id) => pure <| id.isNatLit?.get! --- | _ => throwError "unexpected to_additive_relevant_arg syntax {stx}" --- } --- --- /-- Given a declaration name and an argument index, determines whether it --- is relevant. This is used in `applyReplacementFun` where more detail on what it --- does can be found. - --- def isRelevant [Monad M] [MonadEnv M] (n : Name) (i : Nat) : M Bool := do --- match relevantArgAttr.find? (← getEnv) n with --- | some j => return i == j --- | none => return i == 0 --- --- /- Maps multiplicative names to their additive counterparts. - --- initialize translations : NameMapExtension Name ← --- mkNameMapExtension Name `translations --- --- /-- Get the multiplicative → additive translation for the given name. - --- def findTranslation? (env : Environment) : Name → Option Name := --- (ToAdditive.translations.getState env).find? --- --- /-- Add a (multiplicative → additive) name translation to the translations map. - --- def insertTranslation (src tgt : Name) : CoreM Unit := do --- if let some tgt' := findTranslation? (←getEnv) src then --- throwError "Already exists translation {src} ↦ {tgt'}" --- modifyEnv (ToAdditive.translations.addEntry · (src, tgt)) --- trace[to_additive] "Added translation {src} ↦ {tgt}." --- --- /-- Get whether or not the replace-all flag is set. If this is true, then the --- additiveTest heuristic is not used and all instances of multiplication are replaced. --- You can enable this with `@[to_additive!]` - --- def replaceAll [Functor M] [MonadOptions M] : M Bool := --- (·.getBool `to_additive.replaceAll) <$> getOptions --- --- variable [Monad M] [MonadOptions M] [MonadEnv M] --- --- /-- Auxilliary function for `additiveTest`. The bool argument *only* matters when applied --- to exactly a constant. - --- private def additiveTestAux: Bool → Expr → M Bool --- | b, Expr.const n _ _ => return b || (findTranslation? (← getEnv) n).isSome --- | b, (Expr.app e a _) => do --- if (← additiveTestAux true e) then --- return true --- if let (some n) := e.getAppFn.constName? then --- if let (some l) ← ignore n then --- if e.getAppNumArgs + 1 ∈ l then --- return true --- additiveTestAux false a --- | b, (Expr.lam n e t _) => additiveTestAux false t --- | b, (Expr.forallE n e t _) => additiveTestAux false t --- | b, (Expr.letE n g e body _) => --- return (←additiveTestAux false e) && (← additiveTestAux false body) --- | b, _ => return true --- --- /-- --- `additiveTest e` tests whether the expression `e` contains no constant --- `nm` that is not applied to any arguments, and such that `translations.find?[nm] = none`. --- This is used in `@[to_additive]` for deciding which subexpressions to transform: we only transform --- constants if `additiveTest` applied to their first argument returns `true`. --- This means we will replace expression applied to e.g. `α` or `α × β`, but not when applied to --- e.g. `Nat` or `ℝ × α`. --- We ignore all arguments specified by the `ignore` `NameMap`. --- If `replaceAll` is `true` the test always returns `true`. --- - -```lean --- def additiveTest (e : Expr) : M Bool := do --- if (←replaceAll) then --- return true --- else --- additiveTestAux false e -``` - -- -`e.applyReplacementFun f test` applies `f` to each identifier -(inductive type, defined function etc) in an expression, unless -* The identifier occurs in an application with first argument `arg`; and -* `test arg` is false. -However, if `f` is in the dictionary `relevant`, then the argument `relevant.find f` -is tested, instead of the first argument. - -Reorder contains the information about what arguments to reorder: -e.g. `g x₁ x₂ x₃ ... xₙ` becomes `g x₂ x₁ x₃ ... xₙ` if `reorder.find g = some [1]`. -We assume that all functions where we want to reorder arguments are fully applied. -This can be done by applying `etaExpand` first. - --- def applyReplacementFun : Expr → MetaM Expr := --- Lean.Expr.replaceRecMeta fun r e => do --- trace[to_additive_detail] "applyReplacementFun: replace at {e}" --- match e with --- | Expr.lit (Literal.natVal 1) _ => pure <| mkNatLit 0 --- | Expr.const n₀ ls _ => do --- let n₁ := Name.mapPrefix (findTranslation? <|← getEnv) n₀ --- trace[to_additive_detail] "applyReplacementFun: {n₀} → {n₁}" --- let ls : List Level ← (do -- [todo] just get Lean to figure out the levels? --- if ← shouldReorder n₀ 1 then --- return ls.get! 1::ls.head!::ls.drop 2 --- return ls) --- return some $ Lean.mkConst n₁ ls --- | Expr.app g x _ => do --- let gf := g.getAppFn --- if let some nm := gf.constName? then --- let gArgs := g.getAppArgs --- -- e = `(nm y₁ .. yₙ x) --- trace[to_additive_detail] "applyReplacementFun: app {nm} {gArgs} {x}" --- if gArgs.size > 0 then --- let c1 ← shouldReorder nm gArgs.size --- let c2 ← additiveTest gArgs[0] --- if c1 && c2 then --- -- interchange `x` and the last argument of `g` --- let x ← r x --- let gf ← r g.appFn! --- let ga ← r g.appArg! --- let e₂ := mkApp2 gf x ga --- trace[to_additive_detail] "applyReplacementFun: reordering {nm}: {x} ↔ {ga}\nBefore: {e}\nAfter: {e₂}" --- return some e₂ --- let c1 ← isRelevant nm gArgs.size --- let c2 := gf.isConst --- let c3 ← additiveTest x --- if c1 && c2 && not c3 then --- -- the test failed, so don't update the function body. --- trace[to_additive_detail] "applyReplacementFun: isRelevant and test failed: {nm} {gArgs} {x}" --- let x ← r x --- let args ← gArgs.mapM r --- return some $ mkApp (mkAppN gf args) x --- return e.updateApp! (← r g) (← r x) --- | _ => return none --- --- /-- Eta expands `e` at most `n` times. - --- def etaExpandN (n : Nat) (e : Expr): MetaM Expr := do --- forallBoundedTelescope (← inferType e) (some n) fun xs _ => mkLambdaFVars xs (mkAppN e xs) --- --- /-- `e.expand` eta-expands all expressions that have as head a constant `n` in --- `reorder`. They are expanded until they are applied to one more argument than the maximum in --- `reorder.find n`. - --- def expand (e : Expr) : MetaM Expr := do --- let e₂ ←e.replaceRecMeta $ fun r e => do --- let e0 := e.getAppFn --- let es := e.getAppArgs --- let some e0n := e0.constName? | return none --- let reorder ← getReorder e0n --- if reorder.isEmpty then --- -- no need to expand if nothing needs reordering --- return none --- let e' := mkAppN e0 $ ← es.mapM r --- let needed_n := reorder.foldr Nat.max 0 + 1 --- if needed_n ≤ es.size then --- return some e' --- else --- -- in this case, we need to reorder arguments that are not yet --- -- applied, so first η-expand the function. --- let e' ← etaExpandN (needed_n - es.size) e' --- return some $ e' --- trace[to_additive_detail] "expand:\nBefore: {e}\nAfter: {e₂}" --- return e₂ --- --- /-- Run applyReplacementFun on the given `srcDecl` to make a new declaration with name `tgt` - --- def updateDecl --- (tgt : Name) (srcDecl : ConstantInfo) --- : MetaM ConstantInfo := do --- let mut decl := srcDecl.updateName tgt --- decl := decl.updateType $ (← applyReplacementFun (← expand decl.type)) --- if let some v := decl.value? then --- decl := decl.updateValue (← applyReplacementFun (← expand v)) --- return decl --- --- /-- Lean 4 makes declarations which are not internal --- (that is, head string starts with `_`) but which should be transformed. --- eg `proof_1` in `Lean.Meta.mkAuxDefinitionFor` this might be better fixed in core. --- This method is polyfill for that. - --- def isInternal' : Name → Bool --- | n@(Name.str _ s _) => (s.startsWith "proof_") || (Name.isInternal n) --- | n => Name.isInternal n --- --- /-- transform the declaration `src` and all declarations `pre._proof_i` occurring in `src` --- using the transforms dictionar declaration {src} which is in the namespace {pre}, but does not have the `@[to_additive]` attribute. This is not supported. Workaround: move {src} to a different namespace." --- let env ← getEnv --- -- we find the additive name of `src` --- let tgt := src.mapPrefix (fun n => if n == pre then some tgt_pre else none) --- -- we skip if we already transformed this declaration before --- if env.contains tgt then --- return --- let srcDecl ← getConstInfo src --- -- we first transform all the declarations of the form `pre._proof_i` --- for n in srcDecl.type.listNamesWithPrefix pre do --- transformDeclAux pre tgt_pre n --- if let some value := srcDecl.value? then --- for n in value.listNamesWithPrefix pre do --- transformDeclAux pre tgt_pre n --- -- now transform the source declaration --- let trgDecl : ConstantInfo ← MetaM.run' $ updateDecl tgt srcDecl --- if ¬ trgDecl.hasValue then --- throwError "Expected {trgDecl.name} to have a value." --- trace[to_additive] "generating\n{trgDecl.name} :=\n {trgDecl.value!}" --- try --- -- make sure that the type is correct, --- -- and emit a more helpful error message if it fails --- discard <| MetaM.run' <| inferType trgDecl.value! --- catch --- | Exception.error stx msg => throwError "@[to_additive] failed. --- Type mismatch in additive declaration. For help, see the docstring --- of `to_additive.attr`, section `Troubleshooting`. --- Failed to add declaration\n{trgDecl.name}:\n{msg}" --- | e => panic! "unreachable" --- addAndCompile trgDecl.toDeclaration! --- if isProtected (← getEnv) src then --- setEnv $ addProtected (← getEnv) tgt --- --- /-- This should copy all of the attributes on src to tgt. --- At the moment it only copies `simp` attributes because attributes --- are not stored by the environment. --- --- [todo] add more attributes. A change is coming to core that should --- allow us to iterate the attributes applied to a given decalaration. --- - --- def copyAttributes (src tgt : Name) : CoreM Unit := do --- -- [todo] other simp theorems --- let some ext ← getSimpExtension? `simp | return () --- let thms ← ext.getTheorems --- if (¬ thms.isLemma src) || thms.isLemma tgt then --- return () --- -- [todo] how to get prio data from SimpTheorems? --- MetaM.run' $ Lean.Meta.addSimpTheorem ext tgt --- (post := true) --- (inv := false) --- (attrKind := AttributeKind.global) --- (prio := 1000) --- return () --- --- /-- --- Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and --- the body using the `translations` dictionary. --- This is used to implement `@[to_additive]`. --- - --- def transformDecl (src tgt : Name) : CoreM Unit := do --- transformDeclAux src tgt src --- let eqns? ← MetaM.run' (getEqnsFor? src true) --- -- now transform all of the equational lemmas --- if let some eqns := eqns? then --- for src_eqn in eqns do --- transformDeclAux src tgt src_eqn --- -- [todo] copy attributes for equations --- -- [todo] add equation lemmas to tgt_eqn --- copyAttributes src tgt --- return () --- /-- --- Find the first argument of `nm` that has a multiplicative type-class on it. --- Returns 1 if there are no types with a multiplicative class as arguments. --- E.g. `prod.group` returns 1, and `pi.has_one` returns 2. --- - --- def firstMultiplicativeArg (nm : Name) : MetaM (Option Nat) := do --- let d ← getConstInfo nm --- forallTelescopeReducing (← getConstInfo nm).type fun xs _ => do --- -- xs are the arguments to the constant --- let xs := xs.toList --- let l ← xs.mapM fun x => do --- -- x is an argument and i is the index --- -- write `x : (y₀ : α₀) → ... → (yₙ : αₙ) → tgt_fn tgt_args₀ ... tgt_argsₘ` --- forallTelescopeReducing (← inferType x) fun ys tgt => do --- let (tgt_fn, tgt_args) := tgt.getAppFnArgs --- let n_bi := ys.size --- if let some c := tgt.getAppFn.constName? then --- if findTranslation? (← getEnv) c |>.isNone then --- return [] --- return tgt_args.toList.filterMap fun tgt_arg => --- xs.findIdx? fun x => Expr.containsFVar tgt_arg x.fvarId! --- trace[to_additive_detail] "firstMultiplicativeArg: {l}" --- match l.join with --- | [] => return none --- | (head :: tail) => return some <| tail.foldr Nat.min head --- --- --- /-- `ValueType` is the type of the arguments that can be provided to `to_additive`. - --- structure ValueType : Type where --- /-- Replace all multiplicative declarations, do not use the heuristic. - --- replaceAll : Bool := false --- /-- View the trace of the to_additive procedure. --- Equivalent to `set_option trace.to_additive true`. - --- trace : Bool := false --- /-- The name of the target (the additive declaration). - --- tgt : Name := Name.anonymous --- /-- An optional doc string. - --- doc : Option String := none --- /-- If `allow_auto_name` is `false` (default) then --- `@[to_additive]` will check whether the given name can be auto-generated. - --- allowAutoName : Bool := false --- deriving Repr --- --- /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. - --- def addCommPrefix : Bool → String → String --- | true, s => "comm" ++ s.capitalize --- | false, s => s --- --- /-- Dictionary used by `to_additive.guess_name` to autogenerate names. --- [todo] update to Lean 4 naming - --- private def guessNameDict : Bool → List String → List String --- | is_comm, ("one" :: "le" :: s) => addCommPrefix is_comm "nonneg" :: guessNameDict false s --- | is_comm, ("one" :: "lt" :: s) => addCommPrefix is_comm "pos" :: guessNameDict false s --- | is_comm, ("le" :: "one" :: s) => addCommPrefix is_comm "nonpos" :: guessNameDict false s --- | is_comm, ("lt" :: "one" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s --- | is_comm, ("mul" :: "single" :: s) => addCommPrefix is_comm "single" :: guessNameDict false s --- | is_comm, ("mul" :: "support" :: s) => addCommPrefix is_comm "support" :: guessNameDict false s --- | is_comm, ("mul" :: "tsupport" :: s) => addCommPrefix is_comm "tsupport" :: guessNameDict false s --- | is_comm, ("mul" :: "indicator" :: s) => addCommPrefix is_comm "indicator" :: guessNameDict false s --- | is_comm, ("mul" :: s) => addCommPrefix is_comm "add" :: guessNameDict false s --- | is_comm, ("smul" :: s) => addCommPrefix is_comm "vadd" :: guessNameDict false s --- | is_comm, ("inv" :: s) => addCommPrefix is_comm "neg" :: guessNameDict false s --- | is_comm, ("div" :: s) => addCommPrefix is_comm "sub" :: guessNameDict false s --- | is_comm, ("one" :: s) => addCommPrefix is_comm "zero" :: guessNameDict false s --- | is_comm, ("prod" :: s) => addCommPrefix is_comm "sum" :: guessNameDict false s --- | is_comm, ("finprod" :: s) => addCommPrefix is_comm "finsum" :: guessNameDict false s --- | is_comm, ("pow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s --- | is_comm, ("npow" :: s) => addCommPrefix is_comm "nsmul" :: guessNameDict false s --- | is_comm, ("zpow" :: s) => addCommPrefix is_comm "zsmul" :: guessNameDict false s --- | is_comm, ("monoid" :: s) => ("add_" ++ addCommPrefix is_comm "monoid") :: guessNameDict false s --- | is_comm, ("submonoid" :: s) => ("add_" ++ addCommPrefix is_comm "submonoid") :: guessNameDict false s --- | is_comm, ("group" :: s) => ("add_" ++ addCommPrefix is_comm "group") :: guessNameDict false s --- | is_comm, ("subgroup" :: s) => ("add_" ++ addCommPrefix is_comm "subgroup") :: guessNameDict false s --- | is_comm, ("semigroup" :: s) => ("add_" ++ addCommPrefix is_comm "semigroup") :: guessNameDict false s --- | is_comm, ("magma" :: s) => ("add_" ++ addCommPrefix is_comm "magma") :: guessNameDict false s --- | is_comm, ("haar" :: s) => ("add_" ++ addCommPrefix is_comm "haar") :: guessNameDict false s --- | is_comm, ("prehaar" :: s) => ("add_" ++ addCommPrefix is_comm "prehaar") :: guessNameDict false s --- | is_comm, ("unit" :: s) => ("add_" ++ addCommPrefix is_comm "unit") :: guessNameDict false s --- | is_comm, ("units" :: s) => ("add_" ++ addCommPrefix is_comm "units") :: guessNameDict false s --- | is_comm, ("comm" :: s) => guessNameDict true s --- | is_comm, (x :: s) => (addCommPrefix is_comm x :: guessNameDict false s) --- | true, [] => ["comm"] --- | false, [] => [] --- --- /-- Autogenerate target name for `to_additive`. - --- def guessName : String → String := --- -- [todo] replace with camelcase logic? --- String.mapTokens ''' $ --- fun s => String.intercalate (String.singleton '_') $ --- guessNameDict false (s.splitOn "_") --- --- /-- Return the provided target name or autogenerate one if one was not provided. - --- def targetName (src tgt : Name) (allowAutoName : Bool) : CoreM Name := do --- let res ← do --- if tgt.getPrefix != Name.anonymous || allowAutoName then --- return tgt --- let (Name.str pre s _) := src | throwError "to_additive: can't transport {src}" --- let tgt_auto := guessName s --- if tgt.toString == tgt_auto then --- dbg_trace "{src}: correctly autogenerated target name {tgt_auto}, you may remove the explicit {tgt} argument." --- let pre := pre.mapPrefix <| findTranslation? (← getEnv) --- if tgt == Name.anonymous then --- return Name.mkStr pre tgt_auto --- else --- return Name.mkStr pre tgt.toString --- if res == src && tgt != src then --- throwError "to_additive: can't transport {src} to itself." --- return res --- --- private def proceedFieldsAux (src tgt : Name) (f : Name → CoreM (List String)) : CoreM Unit := do --- let srcFields ← f src --- let tgtFields ← f tgt --- if srcFields.length != tgtFields.length then --- throwError "Failed to map fields of {src}, {tgt} with {srcFields} ↦ {tgtFields}" --- for (srcField, tgtField) in List.zip srcFields tgtFields do --- if srcField != tgtField then --- insertTranslation (src ++ srcField) (tgt ++ tgtField) --- --- /-- Add the structure fields of `src` to the translations dictionary --- so that future uses of `to_additive` will map them to the corresponding `tgt` fields. - --- def proceedFields (src tgt : Name) : CoreM Unit := do --- let env : Environment ← getEnv --- let aux := proceedFieldsAux src tgt --- aux (fun n => do --- let fields := if isStructure env n then getStructureFieldsFlattened env n else #[] --- return fields |> .map Name.toString |> Array.toList --- ) --- -- [todo] run to_additive on the constructors of n: --- -- aux (fun n => (env.constructorsOf n).mmap $ ... --- --- private def elabToAdditiveAux --- (replaceAll trace : Bool) (tgt : Option Syntax) (doc : Option Syntax) : ValueType := --- { replaceAll := replaceAll --- trace := trace --- tgt := match tgt with | some tgt => tgt.getId | none => Name.anonymous --- doc := doc.bind (·.isStrLit?) --- allowAutoName := false --- } --- --- private def elabToAdditive : Syntax → CoreM ValueType --- | `(attr| to_additive $[!%$replaceAll]? $[?%$trace]? $[$tgt]? $[$doc]?) => --- return elabToAdditiveAux replaceAll.isSome trace.isSome tgt doc --- | _ => throwUnsupportedSyntax --- --- /-! --- The attribute `to_additive` can be used to automatically transport theorems --- and definitions (but not inductive types and structures) from a multiplicative --- theory to an additive theory. --- --- To use this attribute, just write: --- --- ``` --- @[to_additive] --- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm --- ``` --- --- This code will generate a theorem named `add_comm'`. It is also --- possible to manually specify the name of the new declaration: --- --- ``` --- @[to_additive add_foo] --- theorem foo := sorry --- ``` --- --- An existing documentation string will _not_ be automatically used, so if the theorem or definition --- has a doc string, a doc string for the additive version should be passed explicitly to --- `to_additive`. --- --- ``` --- /-- Multiplication is commutative - --- @[to_additive "Addition is commutative"] --- theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm --- ``` --- --- The transport tries to do the right thing in most cases using several --- heuristics described below. However, in some cases it fails, and --- requires manual intervention. --- --- If the declaration to be transported has attributes which need to be --- copied to the additive version, then `to_additive` should come last: --- --- ``` --- @[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x --- ``` --- --- Currently only the `simp` attribute is supported. --- --- ## Implementation notes --- --- The transport process generally works by taking all the names of --- identifiers appearing in the name, type, and body of a declaration and --- creating a new declaration by mapping those names to additive versions --- using a simple string-based dictionary and also using all declarations --- that have previously been labeled with `to_additive`. --- --- In the `mul_comm'` example above, `to_additive` maps: --- * `mul_comm'` to `add_comm'`, --- * `comm_semigroup` to `add_comm_semigroup`, --- * `x * y` to `x + y` and `y * x` to `y + x`, and --- * `comm_semigroup.mul_comm'` to `add_comm_semigroup.add_comm'`. --- --- ### Heuristics --- --- `to_additive` uses heuristics to determine whether a particular identifier has to be --- mapped to its additive version. The basic heuristic is --- --- * Only map an identifier to its additive version if its first argument doesn't --- contain any unapplied identifiers. --- --- Examples: --- * `@Mul.mul Nat n m` (i.e. `(n * m : Nat)`) will not change to `+`, since its --- first argument is `Nat`, an identifier not applied to any arguments. --- * `@Mul.mul (α × β) x y` will change to `+`. It's first argument contains only the identifier --- `prod`, but this is applied to arguments, `α` and `β`. --- * `@Mul.mul (α × Int) x y` will not change to `+`, since its first argument contains `Int`. --- --- The reasoning behind the heuristic is that the first argument is the type which is "additivized", --- and this usually doesn't make sense if this is on a fixed type. --- --- There are some exceptions to this heuristic: --- --- * Identifiers that have the `@[to_additive]` attribute are ignored. --- For example, multiplication in `↥Semigroup` is replaced by addition in `↥AddSemigroup`. --- * If an identifier `d` has attribute `@[to_additive_relevant_arg n]` then the argument --- in position `n` is checked for a fixed type, instead of checking the first argument. --- `@[to_additive]` will automatically add the attribute `@[to_additive_relevant_arg n]` to a --- declaration when the first argument has no multiplicative type-class, but argument `n` does. --- * If an identifier has attribute `@[to_additive_ignore_args n1 n2 ...]` then all the arguments in --- positions `n1`, `n2`, ... will not be checked for unapplied identifiers (start counting from 1). --- For example, `cont_mdiff_map` has attribute `@[to_additive_ignore_args 21]`, which means --- that its 21st argument `(n : WithTop Nat)` can contain `Nat` --- (usually in the form `has_top.top Nat ...`) and still be additivized. --- So `@Mul.mul (C^∞⟮I, N; I', G⟯) _ f g` will be additivized. --- --- ### Troubleshooting --- --- If `@[to_additive]` fails because the additive declaration raises a type mismatch, there are --- various things you can try. --- The first thing to do is to figure out what `@[to_additive]` did wrong by looking at the type --- mismatch error. --- --- * Option 1: It additivized a declaration `d` that should remain multiplicative. Solution: --- * Make sure the first argument of `d` is a type with a multiplicative structure. If not, can you --- reorder the (implicit) arguments of `d` so that the first argument becomes a type with a --- multiplicative structure (and not some indexing type)? --- The reason is that `@[to_additive]` doesn't additivize declarations if their first argument --- contains fixed types like `Nat` or `ℝ`. See section Heuristics. --- If the first argument is not the argument with a multiplicative type-class, `@[to_additive]` --- should have automatically added the attribute `@[to_additive_relevant_arg]` to the declaration. --- You can test this by running the following (where `d` is the full name of the declaration): --- ``` --- #eval (do isRelevant `d >>= trace) --- ``` --- The expected output is `n` where the `n`-th argument of `d` is a type (family) with a --- multiplicative structure on it. If you get a different output (or a failure), you could add --- the attribute `@[to_additive_relevant_arg n]` manually, where `n` is an argument with a --- multiplicative structure. --- * Option 2: It didn't additivize a declaration that should be additivized. --- This happened because the heuristic applied, and the first argument contains a fixed type, --- like `Nat` or `ℝ`. Solutions: --- * If the fixed type has an additive counterpart (like `↥Semigroup`), give it the `@[to_additive]` --- attribute. --- * If the fixed type occurs inside the `k`-th argument of a declaration `d`, and the --- `k`-th argument is not connected to the multiplicative structure on `d`, consider adding --- attribute `[to_additive_ignore_args k]` to `d`. --- * If you want to disable the heuristic and replace all multiplicative --- identifiers with their additive counterpart, use `@[to_additive!]`. --- * Option 3: Arguments / universe levels are incorrectly ordered in the additive version. --- This likely only happens when the multiplicative declaration involves `pow`/`^`. Solutions: --- * Ensure that the order of arguments of all relevant declarations are the same for the --- multiplicative and additive version. This might mean that arguments have an "unnatural" order --- (e.g. `Monoid.npow n x` corresponds to `x ^ n`, but it is convenient that `Monoid.npow` has this --- argument order, since it matches `AddMonoid.nsmul n x`. --- * If this is not possible, add the `[to_additive_reorder k]` to the multiplicative declaration --- to indicate that the `k`-th and `(k+1)`-st arguments are reordered in the additive version. --- --- If neither of these solutions work, and `to_additive` is unable to automatically generate the --- additive version of a declaration, manually write and prove the additive version. --- Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to --- `multiplicative G`. --- Afterwards, apply the attribute manually: --- --- ``` --- attribute [to_additive foo_add_bar] foo_bar --- ``` --- --- This will allow future uses of `to_additive` to recognize that --- `foo_bar` should be replaced with `foo_add_bar`. --- --- ### Handling of hidden definitions --- --- Before transporting the “main” declaration `src`, `to_additive` first --- scans its type and value for names starting with `src`, and transports --- them. This includes auxiliary definitions like `src._match_1`, --- `src._proof_1`. --- --- In addition to transporting the “main” declaration, `to_additive` transports --- its equational lemmas and tags them as equational lemmas for the new declaration, --- attributes present on the original equational lemmas are also transferred first (notably --- `_refl_lemma`). --- --- ### Structure fields and constructors --- --- If `src` is a structure, then `to_additive` automatically adds --- structure fields to its mapping, and similarly for constructors of --- inductive types. --- --- For new structures this means that `to_additive` automatically handles --- coercions, and for old structures it does the same, if ancestry --- information is present in `@[ancestor]` attributes. The `ancestor` --- attribute must come before the `to_additive` attribute, and it is --- essential that the order of the base structures passed to `ancestor` matches --- between the multiplicative and additive versions of the structure. --- --- ### Name generation --- --- * If `@[to_additive]` is called without a `name` argument, then the --- new name is autogenerated. First, it takes the longest prefix of --- the source name that is already known to `to_additive`, and replaces --- this prefix with its additive counterpart. Second, it takes the last --- part of the name (i.e., after the last dot), and replaces common --- name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. --- --- * [todo] Namespaces can be transformed using `map_namespace`. For example: --- ``` --- run_cmd to_additive.map_namespace `quotient_group `quotient_add_group --- ``` --- --- Later uses of `to_additive` on declarations in the `quotient_group` --- namespace will be created in the `quotient_add_group` namespaces. --- --- * If `@[to_additive]` is called with a `name` argument `new_name` --- /without a dot/, then `to_additive` updates the prefix as described --- above, then replaces the last part of the name with `new_name`. --- --- * If `@[to_additive]` is called with a `name` argument --- `new_namespace.new_name` /with a dot/, then `to_additive` uses this --- new name as is. --- --- As a safety check, in the first case `to_additive` double checks --- that the new name differs from the original one. --- --- - -```lean -def foo : Int := 10 -``` diff --git a/md/extra/attrs/dummy.md b/md/extra/attrs/dummy.md index 6c5f851..e08a497 100644 --- a/md/extra/attrs/dummy.md +++ b/md/extra/attrs/dummy.md @@ -4,24 +4,27 @@ open Lean namespace Attr syntax (name := dummy_attr) "dummy_attr" term : attr -initialize registerTraceClass `dummy_attr +``` + +This uses a low level attribute registration function. We declare the attribute +with `registerBuiltinAttribute`. The `name` field is the name of the attribute, which +should match with the `syntax` above for parsing. The `descr` is the textual description +of the attribute used for docstrings. The `add` function is run when the attribute is applied to a +declaration of name `declName`. `stx` is the syntax of the attribute including arguments +```lean initialize registerBuiltinAttribute { name := `dummy_attr descr :="dummy_attr print information" - add := fun src stx kind => do + add := fun declName stx kind => do let num : Nat := stx[1].toNat dbg_trace "number + 1: {num + 1}" - dbg_trace "src: {src} | stx: {stx} | kind: {kind}" - let srcDecl ← getConstInfo src + dbg_trace "declName: {declName} | stx: {stx} | kind: {kind}" + let srcDecl ← getConstInfo declName dbg_trace "srcDecl:" dbg_trace " name: {srcDecl.name}" dbg_trace " type: {srcDecl.type}" dbg_trace " value?: {srcDecl.value?}" return () } - --- QUESTION: Can I uncomment this? --- @[dummy_attr "foo"] --- def foo : Int := 42 ``` diff --git a/md/extra/attrs/parameteric.md b/md/extra/attrs/parameteric.md index 8e56d69..11e9f24 100644 --- a/md/extra/attrs/parameteric.md +++ b/md/extra/attrs/parameteric.md @@ -1,9 +1,17 @@ +```lean import Lean open Lean -- The name of the syntax is important. The name is -- used to connect to the corresponding attribute. syntax (name := myParam) "myParam" num "important"? : attr +``` + +This declarares the attribute `myParamAttr`, which is parametrized +by a value of type `(Nat × Bool)`. The `getParam` function describes how to build +a value of `(Nat × Bool)` given the raw syntax declared by `myParam` above. +The `afterSet` function can be used as a finalizer to perform processing once we have +a parsed value. initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← registerParametricAttribute { @@ -14,11 +22,11 @@ initialize fooParamAttr : ParametricAttribute (Nat × Bool) ← descr := "parametric attribute containing a priority and flag" getParam := fun _ stx => match stx with - | `(attr| myParam $prio:num) => - return (prio.getNat, false) - | `(attr| myParam $prio:num important) => + | `(attr| myParam $prio:num) => + return (prio.getNat, false) + | `(attr| myParam $prio:num important) => return (prio.getNat, true) - | _ => throwError "unexpected foo attribute" + | _ => throwError "unexpected foo attribute" afterSet := fun declName val => do IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}" }