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

8105 commits

Author SHA1 Message Date
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
50cfbc1fd5 fix(kernel/quotient/quotient): add missing import 2017-01-31 09:39:30 +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
4d3ff955d3 feat(frontends/lean): nicer syntax for default parameter values 
See #1340
 2017-01-30 15:54:26 -08:00
Leonardo de Moura
c09f60de6e fix(frontends/lean/structure_cmd): fixes #1347 2017-01-30 14:49:14 -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
36f37a3472 fix(frontends/lean/builtin_cmds): make vm_eval_cmd robust with respect to changes universe level changes at has_to_string 
see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
3b38f71f11 fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 
We had to change subtype to use Sort since the axiom
strong_indefinite_description uses it.

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
77a9feaf70 refactor(frontends/lean): PType ==> Sort 
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
35224685a9 chore(kernel/quotient/quotient): remove leftover 2017-01-26 13:05:09 -08:00
Sebastian Ullrich
2c3f6d0e1c fix(frontends/lean/structure_cmd): default field values of Pi type 
There were two separate issues:
* An explicit Pi as the type of a field with a default value would be considered a field reference
* An implicit Pi would be instantiated by the elaborator during `visit_structure_instance`
 2017-01-26 18:53:55 +01:00
Sebastian Ullrich
5c5c998813 fix(frontends/lean/structure_cmd): fix default field values referencing universe variables 2017-01-26 18:52:20 +01:00
Sebastian Ullrich
92ebaaa0f8 fix(frontends/lean/builtin_exprs): ite/dite prec should be lowest 2017-01-26 18:52:20 +01:00
Sebastian Ullrich
e8a387b724 fix(emacs/lean-info): do not update info windows during text selection 
Fixes #1332
 2017-01-25 18:33:19 -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
750d02c3ac feat(frontends/lean/definition_cmds): remove equations_result macro from elaborated theorems 2017-01-24 16:51:33 -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
0ba60e62d7 feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's 
Before this commit, an user could define their own prelude and change
the types of quot, quot.mk, quot.lift or quot.ind.
By doing that, they could prove false.

This commit prevents this kind of abuse.
It also modifies the definition of `quot` and avoids the `setoid`
dependency.
The previous `quot` type is now called `quotient`, and it is defined
using the new `quot` type provided by the kernel.

See discussion at #1330
 2017-01-24 15:59:38 -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
1d98192071 fix(util/rb_tree): bug at equal_elems 
This commit also adds an iterator class to rb_tree and rb_map.
 2017-01-23 14:04:26 -08:00
Leonardo de Moura
977c8ed7dd chore(CMakeLists): do not use TCMALLOC by default 
@kha @gebner @jroesch

I changed the default to TCMALLOC=OFF.
We have been having problems on OSX, and this morning I had a nasty bug on
Ubuntu 12.04 when using TCMALLOC
 2017-01-23 11:03:14 -08:00
Leonardo de Moura
0048d0490b fix(frontends/lean/parser): structure followed by doc string 2017-01-23 10:35: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
Leonardo de Moura
71a7a7f466 feat(frontends/lean): add default field values 2017-01-22 21:25:49 -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
75525a1120 fix(frontends/lean/definition_cmds): allow '.' after equations 2017-01-22 12:51:23 -08:00