-
Notifications
You must be signed in to change notification settings - Fork 350
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: user-defined environment extensions
New test demonstrates how to use them. The user-defined extensions cannot be used in the same file where they were declared because the `initialize` commands are only executed when we import the modules containing them. TODO: user-defined attributes.
- Loading branch information
1 parent
42561bb
commit cdd1dbb
Showing
9 changed files
with
206 additions
and
68 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
/build |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
import UserExt.Tst1 | ||
import UserExt.Tst2 | ||
|
||
show_foo_set | ||
show_bla_set |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
import Lean | ||
|
||
open Lean | ||
|
||
initialize blaExtension : SimplePersistentEnvExtension Name NameSet ← | ||
registerSimplePersistentEnvExtension { | ||
name := `blaExt | ||
addEntryFn := NameSet.insert | ||
addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es | ||
} | ||
|
||
syntax (name := insertBla) "insert_bla " ident : command | ||
syntax (name := showBla) "show_bla_set" : command | ||
|
||
open Lean.Elab | ||
open Lean.Elab.Command | ||
|
||
@[commandElab insertBla] def elabInsertBla : CommandElab := fun stx => do | ||
IO.println s!"inserting {stx[1].getId}" | ||
modifyEnv fun env => blaExtension.addEntry env stx[1].getId | ||
|
||
@[commandElab showBla] def elabShowBla : CommandElab := fun stx => do | ||
IO.println s!"bla set: {blaExtension.getState (← getEnv) |>.toList}" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
import Lean | ||
|
||
open Lean | ||
|
||
initialize fooExtension : SimplePersistentEnvExtension Name NameSet ← | ||
registerSimplePersistentEnvExtension { | ||
name := `fooExt | ||
addEntryFn := NameSet.insert | ||
addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es | ||
} | ||
|
||
syntax (name := insertFoo) "insert_foo " ident : command | ||
syntax (name := showFoo) "show_foo_set" : command | ||
|
||
open Lean.Elab | ||
open Lean.Elab.Command | ||
|
||
@[commandElab insertFoo] def elabInsertFoo : CommandElab := fun stx => do | ||
IO.println s!"inserting {stx[1].getId}" | ||
modifyEnv fun env => fooExtension.addEntry env stx[1].getId | ||
|
||
@[commandElab showFoo] def elabShowFoo : CommandElab := fun stx => do | ||
IO.println s!"foo set: {fooExtension.getState (← getEnv) |>.toList}" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
import UserExt.FooExt | ||
import UserExt.BlaExt | ||
|
||
insert_foo hello | ||
insert_foo world | ||
show_foo_set | ||
|
||
insert_bla abc | ||
show_bla_set |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
import UserExt.BlaExt | ||
import UserExt.FooExt | ||
|
||
insert_foo test | ||
insert_bla defg | ||
insert_bla hij |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
[package] | ||
name = "UserExt" | ||
version = "0.1" |