max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
12990 commits 1 branch 0 tags 5.3 GiB
Commit graph

4376 commits

Author SHA1 Message Date
Gabriel Ebner
488850e03a fix(library/util): get_num_inductive_hypotheses_for: use whnf to detect recursive arguments 
Fixes #1812.
 2017-09-05 08:28:32 +02:00
Gabriel Ebner
de0fc09ab9 fix(library/congr_lemma): always return heq in mk_hcongr_lemma 2017-08-29 16:36:37 +02:00
Gabriel Ebner
9920062b69 fix(kernel/expr,library/constructions/projection): preserve instance-implicitness in structure parameters 2017-08-27 16:47:04 +02:00
Sebastian Ullrich
07d8b18caf feat(init/meta/pexpr): expose pexpr.is_placeholder 2017-08-26 23:22:06 +02:00
Sebastian Ullrich
3062c6feb7 feat(init/meta): expose pexpr.get_structure_instance_info 2017-08-24 10:36:43 +02:00
Leonardo de Moura
e99ce26b16 fix(library/type_context): fixes #1801 
This commit also fixes the decay in error message quality reported at
c6a10b127f
 2017-08-22 14:03:58 -07:00
Leonardo de Moura
fb2186334a fix(library/init/meta/relation_tactics,library/tactic/subst_tactic): fixes #1772 2017-08-21 14:51:30 -07:00
Gabriel Ebner
7453148ad2 fix(library/tactic/simp_lemmas): only check has_idx_metavar in simp_lemmas.rewrite 
This copies the change made in 2ca2920284
 2017-08-20 09:30:16 +02:00
Leonardo de Moura
94e7b46214 fix(library/string): is_char_value bug 
Type may be a metavariable, and the is_def_eq test may succeed by
unifying the metavariable with `char`
 2017-08-18 15:29:51 -07:00
Leonardo de Moura
d4f2bb77b8 feat(frontends/lean): recursive equation preprocessor 
To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.

We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.
 2017-08-18 15:06:11 -07:00
Gabriel Ebner
bbfbf1d8f5 doc(library/tactic/simp_lemmas): document and test change in ext_add_core 2017-08-18 19:34:08 +02:00
Gabriel Ebner
6b9bf5e2b7 fix(library/tactic/simp_lemmas): report invalid simplification lemmas also in add() 2017-08-18 19:32:51 +02:00
Gabriel Ebner
0d8e62ed40 feat(library/tactic/simp_lemmas): add both equational lemmas and the definition itself 2017-08-18 08:54:04 +02:00
Gabriel Ebner
256ca9789f fix(library/tactic/simp_lemmas): fix typo in pp 2017-08-18 08:54:03 +02:00
Gabriel Ebner
6bd3fe2449 feat(library/tactic/simp_lemmas): support congruence lemmas that are metavariable applications 2017-08-18 08:54:03 +02:00
Leonardo de Moura
0660e18943 feat(library/metavar_context): add method for setting metavar user facing name 2017-08-17 16:03:32 -07:00
Sebastian Ullrich
579d4a459e chore(init/meta/interactive): check simp lemmas for ambiguous overloads 
Fixes #1786
 2017-08-15 12:43:02 +02:00
Gabriel Ebner
32ddac5f40 feat(library/tactic/kabstract): expose kabstract to VM 2017-08-14 11:41:54 +02:00
Gabriel Ebner
867bc46d99 feat(library/vm/vm_parser): expose parse_command_like to the vm 2017-08-14 11:41:48 +02:00
Gabriel Ebner
e2717ec2c5 fix(library/compiler/inliner): inline auxiliary declarations 
Fixes #1763.
 2017-08-06 10:24:26 +02:00
Gabriel Ebner
0c15724e8e fix(library/tactic/simplify): handle universe polymorphic simplification rules 
The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not.  Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
 2017-08-03 17:42:07 +01:00
Leonardo de Moura
f39e42bf2d fix(library/tactic/destruct_tactic): fixes #1766 2017-08-02 15:35:33 +01:00
Leonardo de Moura
fdaa26f2fd feat(library/equations_compiler/wf_rec): fixes #1782 2017-08-02 15:12:04 +01:00
Gabriel Ebner
ce509e621a refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
Sebastian Ullrich
4f66673fc2 feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers 2017-08-02 14:32:39 +01:00
Gabriel Ebner
89e1b196db fix(library/compiler/preprocess): do not unfold noncomputable definitions 
This happened in Johannes' real number formalization.  We tried to
unfold a noncomputable definition even though it would have been erased
afterwards, and failed.

The check_computable check was introduced in order to fix the error
message in #1401, the error message is still intelligible in that
example.
 2017-08-01 08:37:18 +01:00
Gabriel Ebner
25aa847aba fix(library/constructions/brec_on): make motive explicit in *.below 
Otherwise you can't figure out the type from the pretty-printed output
`nat.below n`.
 2017-07-23 09:38:44 +01:00
Gabriel Ebner
537b11f358 fix(library/tactic/cases_tactic): do not let internal exception escape 
This was doubly ungood since the contained vm_obj was shared across
threads.  @digama0 wseq.exists_of_lift_rel_left should work now.
 2017-07-22 15:25:56 +01:00
Leonardo de Moura
4faae27069 perf(frontends/lean): add notation #[...] 
The new notation should be use to input long sequences.
Closes #1755
 2017-07-21 04:20:48 -07:00
Leonardo de Moura
3bcbfbf348 perf(library/compiler/elim_recursors): beta_reduce ==> head_beta_reduce 
This commit fixes the byte code generation performace problem
exposed by #1755
 2017-07-21 03:32:23 -07:00
Leonardo de Moura
af80c2890d chore(library/init/meta/tactic): define focus_aux using is_assigned 2017-07-21 02:39:55 -07:00
Sebastian Ullrich
46c1a1a844 refactor(frontends/lean/elaborator,kernel/error_msgs): remove duplicate code 2017-07-21 01:46:31 -07:00
Sebastian Ullrich
f8cfc4ea1b feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors 2017-07-21 01:46:31 -07:00
Gabriel Ebner
53898d47b0 fix(library/tactic/smt/congruence_tactics): fix cc_state.add 2017-07-20 09:17:23 +01:00
Gabriel Ebner
776b440d55 fix(library/constructions/projection): fix macro expansion 
Thanks to @fpvandoorn for noticing this issue in Lean 2!  We encountered
this situation when the inferred type of the projection argument did not
reduce to the structure type with the current transparency setting of
the type context.
 2017-07-18 19:56:20 +01:00
Gabriel Ebner
ba2718a89d feat(library/init/meta/environment): expose function to unfold all macros 2017-07-18 19:49:53 +01:00
Gabriel Ebner
e94095cdf3 chore(library/tactic/cases_tactic): add a bit more information to error message 2017-07-18 09:07:09 +01:00
Gabriel Ebner
317319ded3 chore(library/tactic/cases_tactic): improve error message for unsupported equalities 
@leodemoura Should we add a flag to introduce the equalities as
hypotheses in this case?
 2017-07-18 08:55:36 +01:00
Gabriel Ebner
573525fb9f fix(library/kernel_serializer): fix build error 2017-07-16 16:29:30 +01:00
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
Gabriel Ebner
246d71f3ff feat(library/equations_compiler): error recovery 2017-07-16 05:17:38 -07:00
Gabriel Ebner
0579e68ab8 feat(library/export): add option to only export a single declaration 2017-07-14 09:49:24 +01:00
Gabriel Ebner
80ec86d230 fix(library/vm/vm_int): tons of fixes for int.shiftl 2017-07-11 22:54:26 +01:00
Gabriel Ebner
138c427bcb fix(library/vm_int): correct mpz implementation for int.rem 2017-07-11 22:53:59 +01:00
Gabriel Ebner
d0245c4c2f fix(library/vm/vm_int): unformly unbox small ints 2017-07-11 22:53:18 +01:00
Gabriel Ebner
27a39c4a2d fix(library/tactic/eval): do not catch exceptions 2017-07-11 22:52:31 +01:00
Mario Carneiro
ced436a707 fix(library/vm/vm_nat): fix VM definition of nat.shiftr 
fixes #1723
 2017-07-11 20:53:15 +01:00
Josh Pollock
ee55a03205 fix(src/library/vm,tests/lean): fixes #1723 2017-07-09 08:05:05 +02:00
Sebastian Ullrich
ac8de2472e feat(library/tactic/induction_tactic): clear hypothesis before introducing new ones 2017-07-07 10:06:30 -07:00
Leonardo de Moura
91f4fd9507 fix(library/equations_compiler/elim_match): undo bcf44f7 
See issue #1739

Main problem with this commit: the counter-examples for non-exhaustive matches will be
cryptic when using nested inductive types.
 2017-07-07 09:16:07 -07:00