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

177 commits

Author SHA1 Message Date
Leonardo de Moura
d21945fa86 feat(library/phash_map): add persistent hash_map based on phashtable 2017-05-05 12:36:13 -07:00
Leonardo de Moura
4c9247d220 test(tests/library/phashtable): another perf test 2017-05-04 16:29:19 -07:00
Leonardo de Moura
9d5dacd554 test(tests/library/phashtable): add tests 2017-05-04 16:18:03 -07:00
Leonardo de Moura
bdf4d69702 feat(library): add persistent hashtable based on parray 2017-05-04 15:35:25 -07:00
Leonardo de Moura
ae96ebf6ee feat(library/parray): split "long" delta paths 2017-05-03 16:07:49 -07:00
Leonardo de Moura
6092966702 fix(library/parray): missing desctrutor/constructor invocations at reroot 2017-05-03 13:17:26 -07:00
Leonardo de Moura
97ab603325 feat(library/parray): add ensure_unshared 2017-05-03 12:57:15 -07:00
Leonardo de Moura
a69052e7ee feat(library/parray): add parray thread safe version 
We will use the thread safe version for implementing persistent hash maps.
The hash maps will be used to implement decision procedures and refactor
the congruence closure and ematching modules.
The persistent hash maps based on thread safe parrays are performant
when most of the time there is a single thread updating them.

We use a small hack to make sure we don't have any overhead for

   parray<T, false>

i.e., the thread unsafe version used in the VM.
 2017-05-02 17:15:09 -07:00
Leonardo de Moura
04fd50e4e8 chore(*): fix tests and style 2017-02-20 23:53:44 -08:00
Leonardo de Moura
e9a98362d3 feat(library): functional arrays 2017-02-20 22:00:02 -08:00
Gabriel Ebner
2867163db0 fix(tests): initialize util module 2016-12-08 13:11:53 -08:00
Gabriel Ebner
a8df381d20 feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
Gabriel Ebner
888609013f feat(tests): run tests in emscripten build 2016-10-16 14:41:35 -07:00
Leonardo de Moura
9ef3ebbd5b refactor(*): delete HoTT support 2016-09-27 16:33:39 -07:00
Leonardo de Moura
da27454c8c chore(util): remove dead code 2016-09-23 14:29:13 -07:00
Leonardo de Moura
a93eada058 feat(library/type_context): improved (and simplified) cache management for type_context 2016-08-23 17:56:58 -07:00
Leonardo de Moura
5b0100ef0b refactor(library/lazy_abstraction): lazy ==> delayed 2016-07-27 13:53:17 -07:00
Leonardo de Moura
4f3ce09b57 fix(library/type_context,library/lazy_abstraction): bug in lazy_abstraction, and handle lazy_abstraction in type inference 2016-06-25 14:47:30 -07:00
Leonardo de Moura
989dbcb265 chore(tests): fix some C++ unit tests 2016-06-10 18:29:41 -07:00
Leonardo de Moura
a6b112d3b2 fix(tests/library/occurs): compilation error 2016-03-25 14:10:07 -07:00
Leonardo de Moura
c9e9fee76a refactor(*): remove name_generator and use simpler mk_fresh_name 2016-02-11 18:05:57 -08:00
Leonardo de Moura
4bb58a04db fix(CMakeLists): remove tests for dead module, fixes #883 2015-11-19 07:59:57 -08:00
Leonardo de Moura
498afc1e6f feat(CMakeLists): add shared library 2015-08-13 11:21:05 -07:00
Leonardo de Moura
b62e6bb133 feat(library/simplifier): add rewrite rule sets 2015-06-01 15:15:57 -07:00
Leonardo de Moura
f830bf54c2 refactor(*): clarify name_generator ownership 2015-05-21 14:32:36 -07:00
Leonardo de Moura
b6fff9fbe1 chore(tests/library/blast/union_find): fix style 2015-05-12 06:24:58 -07:00
Leonardo de Moura
fa70930ef4 feat(library/blast): add union-find datastructure 2015-05-11 16:19:51 -07:00
Leonardo de Moura
57ea660963 refactor(*): start process for eliminating of opaque definitions from the kernel 
see issue #576
 2015-05-08 16:06:04 -07:00
Soonho Kong
7c5339d64e fix(CMakeLists.txt): quote CMake variables 
close #513
 2015-03-28 22:38:11 -04:00
Leonardo de Moura
3b6b23c921 refactor(kernel/expr): remove silly overloads 2014-10-16 13:37:55 -07:00
Leonardo de Moura
da481c3274 refactor(kernel): explicit initialization/finalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
531046626a refactor(*): explicit initialization/finalization for environment extensions 2014-09-22 17:30:29 -07:00
Soonho Kong
9dfa1b6c1d chore(CMakeLists.txt): replace "lib1;lib2" with "lib1" "lib2" 2014-07-31 14:31:19 -07:00
Leonardo de Moura
b4700e4eed chore(build): eliminate artificial dependencies 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-29 18:25:57 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:12:54 -07:00
Leonardo de Moura
5eaf04518b refactor(*): rename Bool to Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:43:18 -07:00
Leonardo de Moura
33cb2db5b5 feat(library/head_map): a simple indexing datastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
59755289e4 feat(library/unifier): case split on constraints of the form (f ...) =?= (f ...), where f can be unfolded, and there are metavariables in the arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 15:52:40 -07:00
Leonardo de Moura
c9cfb844f1 feat(library/unifier): add 'quick' failure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 11:28:21 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 11:37:46 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
611f29a954 chore(library/elaborator): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 16:35:00 -07:00
Leonardo de Moura
c1796d0ce4 chore(*): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-06 10:35:17 -07:00
Leonardo de Moura
7b28419260 chore(*): disable multi thread support for OSX, remove the !defined(APPLE) directives 
We should re-enable multi thread support for OSX as soon as the bug in clang is fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 18:23:26 -07:00
Leonardo de Moura
cd30bb49c1 chore(library/arith): remove unnecessary library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 16:14:15 -07:00
Leonardo de Moura
e769c26800 refactor(kernel): move files that don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:30:40 -07:00
Leonardo de Moura
f99444b130 chore(tests): move max_sharing unit tests to tests/kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 16:01:30 -07:00
Leonardo de Moura
9fda7e2529 fix(kernel): incorrect optimization in max_sharing_fn class 
The resultant expression may failed to be fully shared.
Add an example that demonstrates the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 15:38:22 -07:00
Leonardo de Moura
3b78af0db5 chore(tests/library): enable old tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-22 12:05:49 -07:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 14:48:27 -08:00