From 2ef0ed7b5dbd72838158ad0dd487262aa1718fc3 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 25 May 2022 22:01:08 +0100 Subject: [PATCH 1/3] 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/3] 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/3] 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" + +