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

3778 commits

Author SHA1 Message Date
Gabriel Ebner
41787232f6 refactor(library/kernel_serializer): implement maximal sharing directly 2017-01-31 09:39:30 +01:00
Leonardo de Moura
d315e424ff feat(library/congr_lemma, library/fun_info): make sure opt_param gadget do not confuse the simplifier, fun_info, congr_lemma, etc 
A definition such as

  def f (a : nat) (b : nat := a) (c : nat := a) :=
  a + b + c

should *not* be treated as a dependent function.
 2017-01-30 20:23:45 -08:00
Leonardo de Moura
5da8b205b9 feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
Leonardo de Moura
d34386fef7 perf(frontends/lean/tactic_notation): closes #1345 
We can now elaborate
https://gist.github.com/gebner/439273deee592603190d4f8b4447295b
in 1.6 secs and using less than 500Kb of stack space.
It was takins 44 secs and 5Mb before this commit.

Two modifications:
1) Use pre_monad.seq instead of pre_monad.and_then.
They have the same implementation, but seq is not marked as [inline].

2) Modify how we concatenate the tactics in a begin...end block.
Before: (((a_1 ++ a_2) ++ a_3) ++ a_4)
After:  ((a_1 ++ a_2) ++ (a_3 ++ a_4))
 2017-01-30 14:13:53 -08:00
Leonardo de Moura
4fe73d3f87 fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
Leonardo de Moura
146eaf5281 fix(library/tactic/tactic_state): has_to_format universe changed 
see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
c8542bd77c fix(library/norm_num): bug when creating eq.refl 
The universe parameter was missing.

see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
a6f26f0b74 chore(library): poly_unit ==> punit 
psum, pprod and punit are used internally.

see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
bf9f7560f7 feat(frontends/lean): (Type u) can't be a proposition 
(Type u)  is the old (Type (u+1))
(PType u) is the old (Type u)
Type*     is the old (Type (_+1))
PType*    is the old Type*

The stdlib can be compiled, but we still have > 70 broken tests

See discussion at #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
0e3a8758dc fix(library/equations_compiler/structural_rec): bug when synthesizing equational lemmas 2017-01-30 11:51:07 -08:00
Gabriel Ebner
952f444710 feat(init/meta/task): allow task creation from VM 2017-01-28 08:27:23 +01:00
Gabriel Ebner
5fdc737dfc feat(library/tactic): store name of current declaration in tactic_state 2017-01-28 08:27:19 +01:00
Leonardo de Moura
9107439bce feat(frontends/lean/elaborator): default parameter prototype 
See #1340
 2017-01-27 16:32:22 -08:00
Leonardo de Moura
b1d097e63a feat(library/init/meta): add 'delta' tactic for applying delta reduction 
closes #1331
 2017-01-26 19:04:07 -08:00
Leonardo de Moura
6f502b9afd fix(library/vm): make sure vm_rb_map objects can be stored in ts_vm_obj 
See discussion at #1337
 2017-01-26 15:58:11 -08:00
Leonardo de Moura
4e625b35ad fix(library/vm/vm): memory leak at operator= 2017-01-26 13:32:44 -08:00
Leonardo de Moura
89daecb568 fix(library/type_context): assertion violation 
fixes #1335
 2017-01-25 16:05:23 -08:00
Leonardo de Moura
552ca66e9e feat(library/init/meta/pexpr): expose low level function mk_placeholder 2017-01-25 15:32:50 -08:00
Leonardo de Moura
258fb522d3 feat(library/tactic/smt): add generation heuristic to control matching loops 2017-01-24 22:46:45 -08:00
Leonardo de Moura
477ffd1bc7 fix(library/tactic/smt): make sure a partially applied terms can be used to ematch terms with "more arguments" 2017-01-24 19:25:00 -08:00
Leonardo de Moura
434ada7dcc chore(library/vm,library/tactic): add missing override 2017-01-24 16:19:36 -08:00
Leonardo de Moura
ac6bfce01c feat(library/tactic/smt/congruence_closure): improve propagation for beta reduction in the congruence closure module 2017-01-24 12:09:37 -08:00
Leonardo de Moura
28ce1e6d2b fix(library/tactic/simplify): make sure a partially applied lhs can be used to rewrite terms with "more arguments" in simp 
See discussion at issue #1331
 2017-01-23 19:53:49 -08:00
Leonardo de Moura
f60bbb5fcb fix(library/tactic/simp_lemmas): refl_lemma_rewrite, make sure a partially applied lhs can be used rewrite terms with "more arguments" 2017-01-23 19:37:35 -08:00
Leonardo de Moura
418d62ff48 fix(library/tactic/rewrite_tactic): fixes #1277 2017-01-23 16:34:07 -08:00
Leonardo de Moura
2ca2920284 fix(library/tactic/simplify): relax test 
We only need to check whether the resulting expression does not contain
temporary metavariables introduced by the simplifier.
It is ok if it contains regular metavariables that were already in the goal.

This fixes the issue reported at
https://groups.google.com/forum/#!topic/lean-user/3qzchWkut0g
 2017-01-23 09:59:06 -08:00
Gabriel Ebner
b0c67abb2f feat(library/vm/vm_aux): add vm code for sorry 2017-01-22 14:18:38 -08:00
Leonardo de Moura
cce88c6190 refactor(frontends/lean): interactive tactic support 
After this commit, new interactice tactic classes can be added without
writing C++ code (see example: tests/lean/run/my_tac_class.lean).

The tactic_evaluator was simplified, and all the complexity has been
moved to tactic_notation, and lean code.

We can now inspect the intermediate states produced by the rewrite
tactic.

The function (@scope_trace _ line col thunk) can be used to position trace
messages produced by thunk. If line/col are not provided (i.e., we
just write (scope_trace thunk)), then line/col are filled with the
position of this term by the elaborator.

We can visualize the intermediate tactic states inside nested blocks
such as (try { ... })

The new infrastructure can be used to implement custom tactic_state
pretty printers.
 2017-01-21 22:38:47 -08:00
Leonardo de Moura
7a6b9e193c feat(library/vm, frontends/lean/info_manager): add thread safe vm_obj wrapper, and use it to store arbitrary vm thunks in the info_manager 2017-01-21 22:38:33 -08:00
Leonardo de Moura
37bc2133ec fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching 
fixes #1327
 2017-01-21 22:38:17 -08:00
Leonardo de Moura
0913a7e719 feat(library/tactic/dsimplify): add trace msgs for dsimp 2017-01-21 03:12:28 -08:00
Leonardo de Moura
e8839cbcdc feat(library/app_builder): add mk_eq_mpr that removes unnecessary propext 2017-01-20 20:27:41 -08:00
Leonardo de Moura
4de71cadfa feat(library/init/meta): expose additional app_builder tactics 2017-01-20 20:27:07 -08:00
Leonardo de Moura
0adae9d7c7 chore(library/pp_options): default pp.beta = false 2017-01-20 05:25:28 -08:00
Leonardo de Moura
d0a578c3db feat(library/init/meta/environment): add is_projection 2017-01-18 18:12:08 -08:00
Leonardo de Moura
b309ef66d7 fix(library/equations_compiler/elim_match): fix #1318 2017-01-18 08:21:53 -08:00
Leonardo de Moura
694e6f47dc fix(library/init/meta/smt/ematch,library/tactic/simp_lemmas): trick for adding equations of a definition to a simp/hinst lemma set 
Before this commit, if we declared an equational lemma using 'def',
then it would not be correctly added to the simp/hinst lemma set.
The new test exposes the problem.
 2017-01-18 02:05:04 -08:00
Gabriel Ebner
0d949e0da7 chore(library/module_mgr): explain exceptional case 2017-01-17 17:10:37 -08:00
Gabriel Ebner
a230c47178 feat(util/task_queue,emacs,*): highlight running tasks with different background color 2017-01-17 17:10:37 -08:00
Leonardo de Moura
3178f41cce fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied 
see #1316
 2017-01-17 16:33:19 -08:00
Gabriel Ebner
b4774e9ed1 fix(library/vm/vm): fix segfault in call_stack_fn 2017-01-17 16:00:01 -08:00
Gabriel Ebner
1a6629ce3b feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
Leonardo de Moura
7a210a9b62 chore(library/util): style 2017-01-16 22:59:17 -08:00
Leonardo de Moura
fc00275636 fix(library/compiler/elim_recursors): it was assuming that recursive arguments occur after non recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
70b7a35cfe fix(library/constructions/has_sizeof): it was assuming that recursive arguments occur after non recursive ones 2017-01-16 22:59:17 -08:00
Leonardo de Moura
29b7001bff fix(library/equations_compiler/elim_match): avoid nasty inferred types in auxiliary declarations produced by the equation compiler 2017-01-16 22:55:12 -08:00
Leonardo de Moura
cce6e4d58c fix(library/equations_compiler/compiler): fix #1315 2017-01-16 20:01:25 -08:00
Leonardo de Moura
eabbc5bb68 chore(library/module_mgr): comment unreachable_code assertion 
@gebner, could you please take a look a check whether there is a better fix.
 2017-01-15 23:18:44 +01:00
Leonardo de Moura
67226269b4 feat(library/tactic/simp_lemmas): convenient way of adding equational lemmas of a definition to a simp set 2017-01-14 22:16:16 -08:00
Leonardo de Moura
6a5d3ed0e5 feat(library/vm/vm_string): use check_system to avoid stack overflow 2017-01-13 17:06:24 -08:00