From ee11fca69b55f42a48e91f8c0b6c3a8d5bfd67d7 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 27 Jul 2015 13:47:18 -0700 Subject: [PATCH] refactor(src/library/export): disambiguate export keywords --- doc/export_format.md | 164 ++++++++++++++++++++--------------------- src/library/export.cpp | 24 +++--- 2 files changed, 94 insertions(+), 94 deletions(-) diff --git a/doc/export_format.md b/doc/export_format.md index 7b59fe900..3b6ba572d 100644 --- a/doc/export_format.md +++ b/doc/export_format.md @@ -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. ``` - #s - #i + #NS + #NI ``` 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. ``` - #V - #S - #C * - #A - #L - #P + #EV + #ES + #EC * + #EA + #EL + #EP ``` 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 ``. -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 ``. +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 `*`. -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 diff --git a/src/library/export.cpp b/src/library/export.cpp index ea81151e5..aae5f1f6f 100644 --- a/src/library/export.cpp +++ b/src/library/export.cpp @@ -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");