michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(src/library/export): disambiguate export keywords

Browse source
This commit is contained in:
Daniel Selsam 2015-07-27 13:47:18 -07:00 committed by Leonardo de Moura
parent b4504357b2
commit ee11fca69b
2 changed files with 94 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

164
doc/export_format.md
View file

@ -16,8 +16,8 @@ We can also view it as the empty name.
The following commands are used to define hierarchical names in the export file.
```
<nidx'> #s <nidx> <string>
<nidx'> #i <nidx> <integer>
<nidx'> #NS <nidx> <string>
<nidx'> #NI <nidx> <integer>
```
In both commands, `nidx` is the unique identifier of an existing hierarchical name,
@ -27,10 +27,10 @@ and the second by appending the given integer.
The hierarchical name `foo.bla.1.boo` may be defined using the following sequence of commands
```
1 #s 0 foo
2 #s 1 bla
3 #i 2 1
4 #s 3 boo
1 #NS 0 foo
2 #NS 1 bla
3 #NI 2 1
4 #NS 3 boo
```
Universe terms
@ -62,8 +62,8 @@ and `#UIM` is the "impredicative" maximum. It is defined as zero if `uidx_2` eva
The command `#UP` defines the universe parameter with name `nidx`, and `#UG` the global universe with name `nidx`.
Here is the sequence of commands for creating the universe term `imax (max 2 l1) l2`.
```
1 #s 0 l1
2 #s 0 l2
1 #NS 0 l1
2 #NS 0 l2
1 #US 0
2 #US 1
3 #UP 1
@ -82,58 +82,58 @@ Each expression has a unique identifier: a unsigned integer.
Again, the expression unique identifiers are not disjoint from the universe term and hierarchical name ones.
The following command are used to create expressions in the export file.
```
<eidx'> #V <integer>
<eidx'> #S <uidx>
<eidx'> #C <nidx> <uidx>*
<eidx'> #A <eidx_1> <eidx_2>
<eidx'> #L <info> <nidx> <eidx_1> <eidx_2>
<eidx'> #P <info> <nidx> <eidx_1> <eidx_2>
<eidx'> #EV <integer>
<eidx'> #ES <uidx>
<eidx'> #EC <nidx> <uidx>*
<eidx'> #EA <eidx_1> <eidx_2>
<eidx'> #EL <info> <nidx> <eidx_1> <eidx_2>
<eidx'> #EP <info> <nidx> <eidx_1> <eidx_2>
```
In the commands above, `uidx` denotes the unique identifier of existing universe terms,
`nidx` the unique identifier of existing hierarchical names, `eidx_1` and `eidx_2` the unique
identifier of existing expressions, `info` is an annotation (explained later), and
`eidx'` is the identifier for the expression being defined.
The command `#V` defines a bound variable with de Bruijn index `<integer>`.
The command `#S` defines a sort using the given universe term.
The command `#C` defines a constant with hierarchical name `nidx` and instantiated with 0 or more
The command `#EV` defines a bound variable with de Bruijn index `<integer>`.
The command `#ES` defines a sort using the given universe term.
The command `#EC` defines a constant with hierarchical name `nidx` and instantiated with 0 or more
universe terms `<uidx>*`.
The command `#A` defines function application where `eidx_1` is the function, and `eidx_2` is the argument.
The command `#EA` defines function application where `eidx_1` is the function, and `eidx_2` is the argument.
The binders of lambda and Pi abstractions are decorated with `info`.
This information has no semantic value for fully elaborated terms, but it is useful for pretty printing.
`info` can be one of the following annotations: `#D`, `#I`, `#S` and `#C`. The annotation `#D` corresponds to
the default binder annotation `(...)` used in `.lean` files, and `#I` to `{...}`, `#S` to `{{...}}`, and
`#C` to `[...]`.
The command `#L` defines a lambda abstraction where `nidx` is the binder name, `eidx_1` the type, and
`eidx_2` the body. The command `#P` is similar to `#L`, but defines a Pi abstraction.
`info` can be one of the following annotations: `#BD`, `#BI`, `#BS` and `#BC`. The annotation `#BD` corresponds to
the default binder annotation `(...)` used in `.lean` files, and `#BI` to `{...}`, `#BS` to `{{...}}`, and
`#BC` to `[...]`.
The command `#EL` defines a lambda abstraction where `nidx` is the binder name, `eidx_1` the type, and
`eidx_2` the body. The command `#EP` is similar to `#EL`, but defines a Pi abstraction.
Here is the sequence of commands for creating the term `fun {A : Type.{1}} (a : A), a`
```
1 #s 0 A
2 #s 1 a
1 #NS 0 A
2 #NS 1 a
1 #US 0
1 #S 1
2 #V 0
3 #L #D 2 2
4 #L #I 1 3
1 #ES 1
2 #EV 0
3 #EL #BD 2 2
4 #EL #BI 1 3
```
Now, assume the environment contains the following constant declarations:
`nat : Type.{1}`, `nat.zero : nat`, `nat.succ : nat -> nat`, and `vector.{l} : Type.{l} -> nat -> Type.{max 1 l}`.
Then, the following sequence of commands can be used to create the term `vector.{1} nat 3`.
We annotate some commands with comments of the form `-- ...` to make the example easier to understand.
```
1 #s 0 nat
2 #s 1 zero
3 #s 1 succ
4 #s 0 vector
1 #NS 0 nat
2 #NS 1 zero
3 #NS 1 succ
4 #NS 0 vector
1 #US 0
1 #C 2 -- nat.zero
2 #C 3 -- nat.succ
3 #A 2 1 -- nat.succ nat.zero
4 #A 2 3 -- nat.succ (nat.succ nat.zero)
5 #A 2 4 -- nat.succ (nat.succ (nat.succ nat.zero))
6 #C 4 1 -- vector.{1}
7 #C 1 -- nat
8 #A 6 7 -- vector.{1} nat
9 #A 8 5 -- vector.{1} nat (nat.succ (nat.succ (nat.succ nat.zero)))
1 #EC 2 -- nat.zero
2 #EC 3 -- nat.succ
3 #EA 2 1 -- nat.succ nat.zero
4 #EA 2 3 -- nat.succ (nat.succ nat.zero)
5 #EA 2 4 -- nat.succ (nat.succ (nat.succ nat.zero))
6 #EC 4 1 -- vector.{1}
7 #EC 1 -- nat
8 #EA 6 7 -- vector.{1} nat
9 #EA 8 5 -- vector.{1} nat (nat.succ (nat.succ (nat.succ nat.zero)))
```
Imported files
@ -175,18 +175,18 @@ Axioms are declared in a similar way
We are postulating the existence of an element with the given type.
The following command declare the `definition id.{l} {A : Type.{l}} (a : A) : A := a`.
```
2 #s 0 id
3 #s 0 l
4 #s 0 A
2 #NS 0 id
3 #NS 0 l
4 #NS 0 A
1 #UP 3
0 #S 1
5 #s 0 a
1 #V 0
2 #V 1
3 #P #D 5 1 2
4 #P #I 4 0 3
5 #L #D 5 1 1
6 #L #D 4 0 5
0 #ES 1
5 #NS 0 a
1 #EV 0
2 #EV 1
3 #EP #BD 5 1 2
4 #EP #BI 4 0 3
5 #EL #BD 5 1 1
6 #EL #BD 4 0 5
#DEF 2 3 | 4 6
```
@ -225,38 +225,38 @@ with tree_list : Type.{max 1 l} :=
```
is encoded by the following sequence of commands
```
2 #s 0 l
3 #s 0 tree
4 #s 0 A
2 #NS 0 l
3 #NS 0 tree
4 #NS 0 A
1 #UP 2
0 #S 1
0 #ES 1
2 #US 0
3 #UM 2 1
1 #S 3
2 #P #D 4 0 1
5 #s 3 node
6 #s 0 a
7 #s 0 tree_list
3 #C 7 1
4 #V 0
5 #A 3 4
6 #C 3 1
7 #V 1
8 #A 6 7
9 #P #D 6 5 8
10 #P #I 4 0 9
8 #s 3 empty
11 #A 6 4
12 #P #D 4 0 11
9 #s 7 nil
13 #P #D 4 0 5
10 #s 7 cons
14 #A 3 7
15 #V 2
16 #A 3 15
17 #P #D 6 14 16
18 #P #D 6 11 17
19 #P #I 4 0 18
1 #ES 3
2 #EP #D 4 0 1
5 #NS 3 node
6 #NS 0 a
7 #NS 0 tree_list
3 #EC 7 1
4 #EV 0
5 #EA 3 4
6 #EC 3 1
7 #EV 1
8 #EA 6 7
9 #EP #BD 6 5 8
10 #EP #BI 4 0 9
8 #NS 3 empty
11 #EA 6 4
12 #EP #BD 4 0 11
9 #NS 7 nil
13 #EP #BD 4 0 5
10 #NS 7 cons
14 #EA 3 7
15 #EV 2
16 #EA 3 15
17 #EP #BD 6 14 16
18 #EP #BD 6 11 17
19 #EP #BI 4 0 18
#BIND 1 2 2
#IND 3 2
#INTRO 5 10

24
src/library/export.cpp
View file

@ -37,11 +37,11 @@ class exporter {
} else if (n.is_string()) {
unsigned p = export_name(n.get_prefix());
i = m_name2idx.size();
m_out << i << " #s " << p << " " << n.get_string() << "\n";
m_out << i << " #NS " << p << " " << n.get_string() << "\n";
} else {
unsigned p = export_name(n.get_prefix());
i = m_name2idx.size();
m_out << i << " #i " << p << " " << n.get_numeral() << "\n";
m_out << i << " #NI " << p << " " << n.get_numeral() << "\n";
}
m_name2idx.insert(mk_pair(n, i));
return i;
@ -93,13 +93,13 @@ class exporter {
void display_binder_info(binder_info const & bi) {
if (bi.is_implicit())
m_out << "#I";
m_out << "#BI";
else if (bi.is_strict_implicit())
m_out << "#S";
m_out << "#BS";
else if (bi.is_inst_implicit())
m_out << "#C";
m_out << "#BC";
else
m_out << "#D";
m_out << "#BD";
}
unsigned export_binding(expr const & e, char const * k) {
@ -119,7 +119,7 @@ class exporter {
for (level const & l : const_levels(e))
ls.push_back(export_level(l));
unsigned i = m_expr2idx.size();
m_out << i << " #C " << n;
m_out << i << " #EC " << n;
for (unsigned l : ls)
m_out << " " << l;
m_out << "\n";
@ -135,12 +135,12 @@ class exporter {
switch (e.kind()) {
case expr_kind::Var:
i = m_expr2idx.size();
m_out << i << " #V " << var_idx(e) << "\n";
m_out << i << " #EV " << var_idx(e) << "\n";
break;
case expr_kind::Sort:
l = export_level(sort_level(e));
i = m_expr2idx.size();
m_out << i << " #S " << l << "\n";
m_out << i << " #ES " << l << "\n";
break;
case expr_kind::Constant:
i = export_const(e);
@ -149,13 +149,13 @@ class exporter {
e1 = export_expr(app_fn(e));
e2 = export_expr(app_arg(e));
i = m_expr2idx.size();
m_out << i << " #A " << e1 << " " << e2 << "\n";
m_out << i << " #EA " << e1 << " " << e2 << "\n";
break;
case expr_kind::Lambda:
i = export_binding(e, "#L");
i = export_binding(e, "#EL");
break;
case expr_kind::Pi:
i = export_binding(e, "#P");
i = export_binding(e, "#EP");
break;
case expr_kind::Meta:
throw exception("invald 'export', meta-variables cannot be exported");