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

695 commits

Author SHA1 Message Date
Leonardo de Moura
6c3d55ff7f chore(util/json): workaround for mingw 2016-10-14 17:24:47 -07:00
Leonardo de Moura
3162bac4e7 feat(shell/lean): disable assertion violation dialog in server mode 2016-10-13 18:56:10 -07:00
Gabriel Ebner
9e518efe46 fix(util/debug): put lean_unreachable into a block 2016-10-13 18:49:10 -07:00
Gabriel Ebner
bd09d8febe feat(shell/json): json-formatted error messages 2016-10-13 18:49:10 -07:00
Gabriel Ebner
b05b514cc2 refactor(*): structured message objects 2016-10-13 18:49:10 -07:00
Gabriel Ebner
837938981e fix(tests/util/lp): fix debug build 2016-10-03 22:22:12 -07:00
Leonardo de Moura
e9ef7d1342 chore(util/parray): remove dead code 2016-10-03 19:09:57 -07:00
Leonardo de Moura
e6fbbbbc2d feat(util/rb_map): add unsigned_map 2016-10-03 16:26:58 -07:00
Leonardo de Moura
872360db0f feat(util/hash): use #if 2016-10-02 10:46:11 -07:00
Leonardo de Moura
ee3c857c88 fix(util/hash): 32-bit version 2016-10-02 10:03:04 -07:00
Leonardo de Moura
d0d75c0923 refactor(kernel): reduce number of configurations supported in the kernel 
Now, eta and impredicativity are assumed to be always true.

Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
 2016-09-27 17:07:01 -07:00
Leonardo de Moura
d4ed8baf3c chore(util/thread): mark global as static 2016-09-27 15:53:49 -07:00
Leonardo de Moura
da27454c8c chore(util): remove dead code 2016-09-23 14:29:13 -07:00
Leonardo de Moura
165e2d5b97 chore(*): fix compilation warnings 2016-09-19 17:36:28 -07:00
Gabriel Ebner
4dac796337 feat(library/local_context): make get_unused_name O(log(n)) 2016-09-19 16:38:03 -07:00
Daniel Selsam
52f87760d8 feat(src/library/inductive_compiler): support for nested inductive types 2016-09-16 12:50:59 -07:00
Leonardo de Moura
803c956d18 feat(util/sexpr/option_declarations): allow options to be registered after initialization 2016-08-19 16:58:30 -07:00
Leonardo de Moura
2899f909a6 feat(util/fresh_name): API for detecting whether a name was created using mk_fresh_name 2016-08-05 19:02:31 -07:00
Leonardo de Moura
1b528ba327 chore(util/name): remove assertion 
The procedure get_tagged_name_suffix violates the assertion.
Alternative solution: change return type of get_tagged_name_suffix to
optional<std::string> since it is only used for pretty printing.
 2016-07-30 19:53:58 -07:00
Leonardo de Moura
8b533a54c2 feat(frontends/lean/pp): improve purify_metavars 2016-07-30 15:31:06 -07:00
Sebastian Ullrich
3974d798c8 chore(util/name): remove confusing precondition comment 2016-07-29 23:44:22 -04:00
Sebastian Ullrich
6f4a6c39f3 fix(util/lp): fix compilation error 2016-07-29 23:44:22 -04:00
Sebastian Ullrich
661fafc940 refactor(frontends/lean): replace different attribute classes with single scoped_ext 2016-07-29 18:51:23 -04:00
Leonardo de Moura
01283512a6 feat(frontends/lean/elaborator): add code for deciding which function application elaboration procedure should be used 2016-07-25 12:55:28 -07:00
Leonardo de Moura
35888fae2c refactor(util/list): remove coercion from T -> list<T> 2016-06-22 10:00:07 -07:00
Leonardo de Moura
62905152f9 feat(kernel/environment): add is_eqp for environment 2016-06-14 12:28:59 -07:00
Leonardo de Moura
0e7f95e4d0 perf(util/rb_tree,until/rb_map): reduce object size 2016-06-07 08:33:31 -07:00
Leonardo de Moura
83f64ef8b3 chore(util): remove dead code 2016-06-02 18:38:07 -07:00
Soonho Kong
b95bc8ff5b feat(util/memory.cpp): use COMP_HAS_SIZED_DEALLOCATION macro 
To conditionally include sized deallocation definitions.

Related issue #1044
 2016-06-02 11:53:08 -07:00
Sebastian Ullrich
ac4efdf660 fix(util/memory): add C++14 sized delete operators 
Fixes #1044
 2016-06-02 11:52:51 -07:00
Lev Nachmanson
5f565cfbe5 dev(lp): fix column_info initialization in lp_solver 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-06-02 11:51:52 -07:00
Lev Nachmanson
2aea6066fa dev(lp): refactor the lar_core_solver parameters into a separate struct 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-06-02 11:51:45 -07:00
Lev Nachmanson
9680081376 dev(lp): move some dummy field from lar_solver to lar_core_solver 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-06-02 11:51:37 -07:00
Lev Nachmanson
1f9ef61839 dev(lp): simplify the design of lar_solver 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-06-02 11:51:29 -07:00
Lev Nachmanson
96824e375b dev(lp): add a file 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-06-02 11:51:18 -07:00
Lev Nachmanson
c2d795e46a dev(lp): integrate with z3 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-06-02 11:51:07 -07:00
Leonardo de Moura
53811822d4 chore(*): style 2016-05-25 18:10:15 -07:00
Leonardo de Moura
11b63b0fcd fix(util/small_object_allocator): warning 2016-05-13 15:20:32 -07:00
Leonardo de Moura
92bc367c5c feat(util): add small object allocator 2016-05-13 14:41:31 -07:00
Leonardo de Moura
5189a83f57 feat(library/vm): pretty print bytecode 2016-05-11 16:57:56 -07:00
Leonardo de Moura
906c4f86f1 feat(library/vm): add vm_decl(s) 2016-05-10 21:11:07 -07:00
Leonardo de Moura
7641b602ca chore(util): fun_array ==> parray 2016-05-10 16:05:41 -07:00
Leonardo de Moura
6cb8e82fef feat(util/fun_array): add functional array 2016-05-09 17:40:26 -07:00
Leonardo de Moura
889bdec2f7 feat(util/rb_tree): add unsigned_rev_cmp 2016-05-01 19:30:51 -07:00
Leonardo de Moura
a823b0e6ec feat(library/type_context): pop_local for type_context 2016-03-09 10:22:48 -08:00
Leonardo de Moura
c8e5907b70 feat(util/rb_tree,util/rb_map): add back_find_if 2016-03-05 13:29:34 -08:00
Leonardo de Moura
82fb38b440 feat(util/rb_tree): add for_each_greater 2016-03-01 15:42:27 -08:00
Leonardo de Moura
2982db6f80 feat(library/local_context): add new local context type 2016-03-01 13:40:37 -08:00
Lev Nachmanson
23079a75a7 dev(lp): fix build for clang, avoid clang-3.3 bug, cleanup permutation_matrix 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2016-02-26 16:07:16 -08:00
Leonardo de Moura
9b15c4c669 feat(util/rb_map): add find_if 2016-02-24 16:02:16 -08:00