Leonardo de Moura
6a84b9378a
chore(library/inductive_compiler/util): fix assertion
2018-06-07 16:28:54 -07:00
Leonardo de Moura
2a79da1ab6
refactor(kernel): move formatting stuff out of the kernel
2018-06-07 16:28:54 -07:00
Leonardo de Moura
8ae1e51b6d
feat(kernel): distinguish kernel_exceptions using different classes
2018-06-07 16:28:54 -07:00
Leonardo de Moura
e90585737f
refactor(*): use C++11 std::current_exception and std::rethrow_exception
...
With these new C++11 APIs, we can delete the `clone` and `rethrow`
methods from our exception classes.
2018-06-07 16:28:54 -07:00
Leonardo de Moura
2d7b6ed12c
chore(library/compiler): remove copy_tag from old compiler
2018-06-07 16:28:54 -07:00
Leonardo de Moura
3d1faee826
chore(kernel/abstract_type_context): remove dead method abstract_type_context::abstract
...
We needed this method when we were using delayed abstractions
2018-06-07 16:28:54 -07:00
Leonardo de Moura
6333043adf
refactor(kernel): abstract_local(s) ==> abstract
2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199
chore(kernel): type_checker ==> old_type_checker
2018-06-06 16:10:40 -07:00
Leonardo de Moura
0a5e7ff1a9
feat(kernel): add local_ctx
...
We will have only one kind of local constant (aka free variable) in
Lean4. Thus, we need a local context object to implement the kernel
type checker.
2018-06-06 15:24:10 -07:00
Leonardo de Moura
ee7bc150f2
chore(library/init/meta/expr): remove elaborated : bool parameter from expr
2018-06-06 09:47:01 -07:00
Leonardo de Moura
3a7229add3
chore(library/init): pexpr is now an opaque constant
2018-06-06 09:36:22 -07:00
Leonardo de Moura
441b9077b2
feat(library/comp_val): add mk_name_val_ne_proof
...
We need this procedure otherwise it takes forever to prove equation lemmas
for definitions such as:
```
def macros : name → option macro
| `lambda := some lambda_macro
| `intro_x := some intro_x_macro
| _ := none
```
We never experienced this problem in Lean3 because we used `name`
literals only occurred in patterns of *meta* definitions. So, no
equation lemma was generated.
@kha `def macros` was taking more than 1 second to elaborate on my
machine. It is now instantaneous.
2018-06-06 09:18:59 -07:00
Leonardo de Moura
e4a168af91
chore(library/init/meta): remove goal tagging feature
2018-06-06 08:46:47 -07:00
Leonardo de Moura
bd7138349a
chore(library/init/meta/pexpr): remove pexpr primitives
2018-06-05 16:28:12 -07:00
Leonardo de Moura
ab481d7e7b
chore(library/init/meta): remove unnecessary primitives
2018-06-05 16:13:22 -07:00
Leonardo de Moura
0119926022
fix(kernel/expr): constructor order
2018-06-05 15:56:51 -07:00
Leonardo de Moura
45202eca16
chore(library/init/meta): cleanup
2018-06-05 15:32:59 -07:00
Leonardo de Moura
330c9afbc0
feat(library/metavar_context): store user_name at metavar_decl
2018-06-05 14:29:55 -07:00
Leonardo de Moura
fc8aa30f0f
chore(library/pp_options): remove dead option
2018-06-05 14:27:04 -07:00
Leonardo de Moura
6472cb0579
chore(kernel/abstract_type_context): rename has_local_pp_name
2018-06-05 14:26:31 -07:00
Leonardo de Moura
8ae42417eb
fix(library/compiler/vm_compiler): missing case
2018-06-05 11:07:38 -07:00
Leonardo de Moura
0dd25b0a24
refactor(util,library): move subscripted_name_set to library
2018-06-05 08:06:32 -07:00
Leonardo de Moura
ff3a3177c3
chore(library/local_context): get_pp_name => get_user_name
2018-06-04 16:08:28 -07:00
Leonardo de Moura
de48d49b53
feat(kernel): preparing for adding new inductive datatype module
2018-06-01 14:47:49 -07:00
Leonardo de Moura
ac0352b584
refactor(kernel): remove quotitent normalizer extension
...
The `quot` type is now implemented in the kernel.
We will do the same thing for inductives.
We will not support normalizer extensions anymore in Lean4.
It doesn't make sense since we settled with 2 extensions: quotients and
inductives. Moreover, any new extension would require substantial
changes (e.g., code generator).
The normalizer_extension feature was useful when we were experimenting
with different kernel flavors.
2018-06-01 10:52:17 -07:00
Leonardo de Moura
722974e8c7
feat(kernel): add option to skip type checking at add_meta
2018-05-31 17:27:55 -07:00
Leonardo de Moura
9a671d7c7d
chore(library/compiler): delete rec_fn_macro
2018-05-31 17:11:25 -07:00
Leonardo de Moura
b95e710e8c
feat(library/compiler, library/equations_compiler): avoid rec_fn_macro in the equation and bytecode compilers
2018-05-31 17:08:12 -07:00
Leonardo de Moura
eab962bbc6
feat(kernel): add add_meta
2018-05-31 15:40:50 -07:00
Leonardo de Moura
cab6b39c76
refactor(library): remove sorry checking
...
We have to revise how we do this.
2018-05-31 15:20:39 -07:00
Leonardo de Moura
112d1da8d0
refactor(library/module): no need to store trust lvl in declarations
...
We are going to delete macros. So, we don't need to store trust_lvl information.
2018-05-31 14:55:18 -07:00
Leonardo de Moura
3c1ccc9b74
refactor(kernel): use m_meta instead of m_trusted
2018-05-31 11:18:00 -07:00
Leonardo de Moura
e80765daca
fix(library/export_decl): bug at export_decl_modification::perform
...
The `perform` method was adding the modification to the environment
where it was being applied.
2018-05-31 09:16:46 -07:00
Leonardo de Moura
80545832f4
chore(library): remove user attributes
2018-05-31 09:10:41 -07:00
Leonardo de Moura
d3272ca1c5
refactor(frontends/lean,library/tactic/kabstract): remove add_key_equivalence command
...
This command was never used in the Lean3 corelib and mathlib.
It is safe to assume it is not needed.
2018-05-30 14:10:03 -07:00
Leonardo de Moura
d707a27c2b
chore(library/class): unnecessary dependency
2018-05-30 14:05:21 -07:00
Leonardo de Moura
843cd9bacb
chore(library/compiler/rec_fn_macro): remove dead code
2018-05-30 13:16:34 -07:00
Leonardo de Moura
2ddb9d1598
refactor(library): remove delayed_abstraction macro
...
We replace them with a new kind of (delayed) assignment at `metavar_context`
```
mvar := (lctx, locals, v)
```
where `lctx` is a local context, `locals` is a list of local
constants, and `v` is an expression.
When all metavariables in `v` are assigned, this assignment is replaced with
```
mvar := Fun(locals, v)
```
2018-05-30 10:04:04 -07:00
Leonardo de Moura
c9a6f98454
chore(library/sorry): style
2018-05-29 22:27:03 -07:00
Leonardo de Moura
7842036aba
feat(library/type_context): avoid delayed_abstractions when creating binders lambda/pi/let
...
This is the first step to eliminate the delayed_abstraction macro.
2018-05-29 16:37:33 -07:00
Leonardo de Moura
0b1525b58e
fix(library/type_context): is_quick_class bug
...
It was returning false for expressions such as `let x := 10 in has_add nat`.
2018-05-29 15:12:44 -07:00
Leonardo de Moura
978ef203b9
fix(frontends/lean/elaborator): the is_def_eq test must be performed in the right local context
2018-05-29 13:35:01 -07:00
Leonardo de Moura
1332fbabd6
feat(library,frontends): remove sorry macro
...
Lean4 will not have macros.
2018-05-24 14:00:30 -07:00
Leonardo de Moura
75c63ec921
refactor(*): list<name> ==> obj_list<name>
2018-05-23 15:48:43 -07:00
Leonardo de Moura
4af1f31877
feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels
2018-05-23 14:48:22 -07:00
Leonardo de Moura
306c300226
refactor(kernel/level): implement level on top of object
2018-05-23 09:54:46 -07:00
Leonardo de Moura
b2f3d3f456
chore(*): remove redundant code
2018-05-22 16:46:04 -07:00
Leonardo de Moura
160b7e8847
refactor(library/init/meta/expr): local_const will have only one field
...
In Lean3, we supported two kinds of local constant:
context-less (inherited from Lean2) and context-based (type,
binder-info and pretty printing name are stored in the context).
The context-less was used in the kernel and a few modules we kept when
we moved from Lean2 to Lean3. Even if we keep the hybrind
representation, we should not expose the context-less to users.
2018-05-21 15:36:09 -07:00
Leonardo de Moura
92ff42776c
chore(library/tactic): remove match_tactic
2018-05-20 17:33:31 -07:00
Leonardo de Moura
4de9b8c177
chore(library/vm): rename constants
2018-05-20 12:30:15 -07:00
