max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/kernel
History
Leonardo de Moura 9afb53fad5 feat(kernel/expr): allow metavariables to have user-facing names 
We need this feature for:
1) Defining nonlinear search patterns. Example: (?m <= ?m + 1)
2) Preprocessing recursive equations and support the pattern
refinement approach used in Agda. Example: in Agda, they accept
```
def append {A : Type} : Π (m n : nat), Vec A m -> Vec A n -> Vec A (m + n)
| m n nil            ys := ys
| m n (cons m' x xs) ys := cons x (append m' n xs ys)
```
These equations have to be refined. For example, `m` has to be
replaced with `0` (in the first equation), and `succ m'` in the
second. To implement this kind of refinement, we need to convert
the pattern variables (local constants) into metavariables during
elaboration. Then, the unassigned metavariables become local constants
again. This preprocessing step will fix some of the issues on #1594.
To completely fix #1594, we will need yet another preprocessing step
which will implement "complete transition" used in the equation
compiler before we start elim_match.cpp
2017-07-16 07:16:41 -07:00
..
inductive fix(kernel/inductive/inductive): identify indices modulo whnf 2017-07-06 20:59:58 -07:00
quotient chore(kernel/quotient/quotient): update comments 2017-03-07 14:11:51 -08:00
abstract.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
abstract.h fix(frontends/lean/structure_cmd): remove evil Pi overload that accidentally abstracted constants in structure decls 2017-04-26 14:22:36 -07:00
abstract_type_context.cpp fix(frontends/lean/pp): qualify constant shadowed by local 2017-03-31 09:40:49 -07:00
abstract_type_context.h fix(frontends/lean/pp): qualify constant shadowed by local 2017-03-31 09:40:49 -07:00
cache_stack.h
CMakeLists.txt refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
declaration.cpp refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
declaration.h refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
environment.cpp refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
environment.h chore(kernel/environment): rename method 2017-05-15 14:18:16 -07:00
equiv_manager.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
equiv_manager.h feat(kernel/equiv_manager): use expr_struct_map in the equiv_manager 2016-07-07 07:39:25 -07:00
error_msgs.cpp fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
error_msgs.h fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
expr.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr.h feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr_cache.cpp refactor(kernel): add expr_cache 2015-02-03 14:59:55 -08:00
expr_cache.h refactor(kernel): add expr_cache 2015-02-03 14:59:55 -08:00
expr_eq_fn.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
expr_eq_fn.h feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information 2016-08-01 16:34:07 -07:00
expr_maps.h feat(library/type_context): allow us to control whether binder information is taken into account or not when caching type information 2016-08-01 16:34:07 -07:00
expr_pair.h feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
expr_sets.h
ext_exception.h chore(util,kernel,library): clang warnings 2017-02-17 20:01:34 -08:00
find_fn.h
for_each_fn.cpp feat(kernel): add let-expressions to the kernel 2016-02-29 16:40:17 -08:00
for_each_fn.h
formatter.cpp fix(*): remove unnecessary null pointer checks 2015-03-28 12:16:39 -07:00
formatter.h feat(library/type_context): better error messages 2016-09-28 15:59:43 -07:00
free_vars.cpp feat(kernel): add compilation flag for disabling "free var range" optimization 2017-02-21 19:40:56 -08:00
free_vars.h
init_module.cpp fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
init_module.h
instantiate.cpp feat(kernel): add compilation flag for disabling "free var range" optimization 2017-02-21 19:40:56 -08:00
instantiate.h feat(kernel/instantiate): add helper function 2016-08-14 16:16:03 -07:00
kernel_exception.cpp fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error 2017-03-27 13:42:08 -07:00
kernel_exception.h fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error 2017-03-27 13:42:08 -07:00
level.cpp fix(kernel/expr): disable caching by default 2017-03-23 08:57:56 +01:00
level.h feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs 2017-02-08 17:41:44 -08:00
normalizer_extension.cpp refactor(kernel): remove extension_context 2016-03-19 15:15:39 -07:00
normalizer_extension.h refactor(kernel): remove extension_context 2016-03-19 15:15:39 -07:00
pos_info_provider.cpp
pos_info_provider.h feat(kernel/pos_info_provider): add save_pos_info 2017-03-31 09:40:48 -07:00
replace_fn.cpp fix(kernel/replace_fn): check if running out of stack space at replace_rec_fn 2017-06-04 15:57:11 -07:00
replace_fn.h feat(kernel/replace_fn): add use_cache flag to replace function 2015-02-05 10:49:18 -08:00
scope_pos_info_provider.cpp refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
scope_pos_info_provider.h refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
standard_kernel.cpp refactor(library/standard_kernel): move standard kernel into kernel 2017-01-31 09:39:31 +01:00
standard_kernel.h refactor(library/standard_kernel): move standard kernel into kernel 2017-01-31 09:39:31 +01:00
type_checker.cpp fix(kernel/type_checker): eagerly check for proof irrelevant definitional equality 2017-07-14 21:46:04 +01:00
type_checker.h chore(kernel/type_checker): remove dead code 2017-02-15 18:05:55 -08:00