Skip to content

[Draft] Simple attributes #71

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2022-07-16
leanprover/lean4:nightly-2022-07-25
130 changes: 130 additions & 0 deletions lean/extra/attributes.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,130 @@
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.

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).

## 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
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)


/-
## 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 `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`

We'll see you at [`./attrs/dummy.lean`](./attrs/dummy.lean).


We run the `dummy_attr <number>`, and we see that we get access to the
attribute argument <number>, 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


## Implementing `sym`:
Scoped environment extension maintains scoping information, so it keeps track of
whether the tag is local or not.
-/


28 changes: 28 additions & 0 deletions lean/extra/attrs/dummy.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
import Lean
open Lean

namespace Attr
syntax (name := dummy_attr) "dummy_attr" term : 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 declName stx kind => do
let num : Nat := stx[1].toNat
dbg_trace "number + 1: {num + 1}"
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 ()
}

31 changes: 31 additions & 0 deletions lean/extra/attrs/parameteric.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
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 {
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.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}"
}
9 changes: 9 additions & 0 deletions lean/extra/attrs/simp.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
import Lean

/--
We declare a simplifcation attribute using the keyword
`register_simp_attr`,
-/
register_simp_attr fooSimp "my own foo simp attribute"


25 changes: 25 additions & 0 deletions lean/extra/attrs/tag.lean
Original file line number Diff line number Diff line change
@@ -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 => "<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 ()




118 changes: 118 additions & 0 deletions md/extra/attributes.md
Original file line number Diff line number Diff line change
@@ -1 +1,119 @@
```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.

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).

## 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
definitions that have been tagged with a given attribute, and nothing more.

```lean
@[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 <number>`, and we see that we get access to the
attribute argument <number>, 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
-- 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.

```lean
@[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


## Implementing `sym`:
Scoped environment extension maintains scoping information, so it keeps track of
whether the tag is local or not.
30 changes: 30 additions & 0 deletions md/extra/attrs/dummy.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
```lean
import Lean
open Lean

namespace Attr
syntax (name := dummy_attr) "dummy_attr" term : 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 declName stx kind => do
let num : Nat := stx[1].toNat
dbg_trace "number + 1: {num + 1}"
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 ()
}
```
Loading