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

3793 commits

Author SHA1 Message Date
Johannes Hölzl
3be8deb2d2 fix(library/tactic/generalize_tactic): instantiate mvars before calling kabstract 2017-02-01 18:48:10 -08:00
Leonardo de Moura
a9821f6437 fix(library/type_context): bug in revert method 
We should not assume that the arguments at to_revert are sorted by idx.
This commit fixes the bug reported at:
https://groups.google.com/forum/#!topic/lean-user/x4Zwpou3le0
 2017-02-01 10:51:24 -08:00
Leonardo de Moura
6e7929252f feat(frontends/lean, library/init): add 'thunk' gadget 
We can now write
   trace "hello" t
instead of
   trace "hello" (fun _, t)
 2017-01-31 18:41:59 -08:00
Leonardo de Moura
7cc31835e4 refactor(library/init/meta/fun_info): cleanup fun_info API 2017-01-31 18:01:54 -08:00
Leonardo de Moura
920e845b84 refactor(library/init/meta/congr_lemma): cleanup congr_lemma API 2017-01-31 16:46:13 -08:00
Leonardo de Moura
941ba6d96c chore(*): style 2017-01-31 11:04:21 -08:00
Gabriel Ebner
f404e8a2be feat(library/export,checker): add basic support for mixfix notation 2017-01-31 10:20:56 +01:00
Gabriel Ebner
54820506e4 feat(library/export): export quotient initialization 2017-01-31 10:20:55 +01:00
Gabriel Ebner
94565113a6 chore(checker): remove gmp, mpfr, and dl library dependencies 2017-01-31 09:39:31 +01:00
Gabriel Ebner
61804eb8e9 chore(util/sexpr): remove mpz and mpq cases 2017-01-31 09:39:31 +01:00
Gabriel Ebner
9e7ca0a969 feat(checker): add leanchecker executable 2017-01-31 09:39:31 +01:00
Gabriel Ebner
2f07bf352c refactor(library/standard_kernel): move standard kernel into kernel 2017-01-31 09:39:31 +01:00
Gabriel Ebner
f3b9439029 feat(library/module_mgr): add function to get combined environment 2017-01-31 09:39:31 +01:00
Gabriel Ebner
81ff87e2fd fix(library/unfold_macros): actually unfold all macros 2017-01-31 09:39:30 +01:00
Gabriel Ebner
94438b515e fix(kernel/kernel_serializer): do not disable validation of external input in release builds 2017-01-31 09:39:30 +01:00
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