Leonardo de Moura
22d0dc197c
fix(library/equations_compiler/pack_domain): bug in pack_domain
2017-05-18 14:24:38 -07:00
Leonardo de Moura
b69cf7ef43
fix(library/tactic/rewrite_tactic): instantiate assign metavars before rewriting
...
fixes #1587
2017-05-18 10:57:03 -07:00
Leonardo de Moura
7d937dcfcb
fix(library/tactic/simplify): instantiate assigned metavariables in the simplifier
...
This fixes a problem similar to the one described at #1587
2017-05-18 10:52:11 -07:00
Gabriel Ebner
7353a54aac
fix(library/vm/vm): prevent segfault
2017-05-18 09:41:31 -07:00
Gabriel Ebner
d9f5e0bb1f
fix(library/app_builder): prevent segfault
2017-05-18 09:41:31 -07:00
Gabriel Ebner
4528711efb
fix(library/type_context): prevent segfault
...
Temporary metavariables appeared here when pretty-printing simp_lemmas.
2017-05-18 09:41:31 -07:00
Leonardo de Moura
737136e8fd
feat(library/equations_compiler/wf_rec): apply well_founded.fix
2017-05-17 16:44:53 -07:00
Leonardo de Moura
4982e23dca
feat(library/equations_compiler/wf_rec): eliminate recursive calls using functional
2017-05-17 15:56:53 -07:00
Leonardo de Moura
56823a22b7
feat(library/equations_compiler/wf_rec): use has_well_founded type class to generate default well founded relation when one is not provided
2017-05-17 14:37:21 -07:00
Leonardo de Moura
1c87319b58
feat(library/equations_compiler): add wf_rec skeleton
2017-05-17 12:47:52 -07:00
Leonardo de Moura
dea8a856dc
chore(library/equations_compiler/compiler): generate error when using well founded recursion in meta definitions
2017-05-17 12:24:47 -07:00
Sebastian Ullrich
84997bf4de
refactor(init/meta/expr): unify expr and pexpr
2017-05-17 10:38:12 -07:00
Leonardo de Moura
0091cef9f2
feat(library/tactic): start algebraic normalizer
2017-05-15 21:46:19 -07:00
Leonardo de Moura
eddc5b0869
chore(kernel/environment): rename method
2017-05-15 14:18:16 -07:00
Sebastian Ullrich
808ab73d93
refactor(init): use list for expr.macro args
2017-05-14 19:17:28 -07:00
Sebastian Ullrich
42eb0c680e
feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives
2017-05-14 19:17:28 -07:00
Gabriel Ebner
b3975c8fc1
chore(library/vm/vm_expr): fix compiler warning
2017-05-11 11:04:11 +02:00
Sebastian Ullrich
4b21b13649
refactor(init): replace has_quote class with reflected
2017-05-09 16:02:42 -07:00
Sebastian Ullrich
ead6318ee0
feat(frontends/lean/elaborator): substitute reflected locals into expr quotes
2017-05-09 16:02:41 -07:00
Sebastian Ullrich
8c0394b294
refactor(library,frontends/lean): separate expr and pexpr macros
2017-05-09 16:02:41 -07:00
Sebastian Ullrich
2825c5fbcc
feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr
2017-05-09 16:02:41 -07:00
Leonardo de Moura
3f5bbfa0cf
fix(library/parray): missing lock
2017-05-09 13:57:28 -07:00
Leonardo de Moura
a3679a43a1
fix(library/parray): unique_lock ==> lock_guard
2017-05-09 13:57:28 -07:00
Leonardo de Moura
0ef0a7f466
chore(library/parray): more assertions
2017-05-09 13:57:28 -07:00
Leonardo de Moura
8802f7cd19
chore(library/phashtable): unnecessary/incorrect annotations
2017-05-09 13:57:28 -07:00
Leonardo de Moura
00887ba3ec
chore(library/parray): more assertions
2017-05-09 13:57:28 -07:00
Leonardo de Moura
2ddd413bef
fix(library/parray): reroot split optimization is incorrect when ThreadSafe == true
2017-05-09 13:57:28 -07:00
Leonardo de Moura
970529a8e9
fix(library/parray): copy method must create a copy of the mutex too (when ThreadSafe == true)
2017-05-09 13:57:28 -07:00
Leonardo de Moura
afadf2b1e1
feat(library/phash_map): add name_hash_map
2017-05-09 13:57:28 -07:00
Leonardo de Moura
bea122bb22
fix(library/phash_map,library/phashtable): missing const and operator
2017-05-09 13:57:28 -07:00
Gabriel Ebner
b536df3596
feat(library/type_context): add option to unfold lemmas
2017-05-08 10:14:47 -07:00
Gabriel Ebner
b4c73e562e
fix(library/vm/vm_io): use correct memory layout for io.environment
2017-05-08 15:07:48 +02:00
Gabriel Ebner
40bf75cbff
fix(library/equations_compiler/structural_rec): fix indices
2017-05-07 15:52:39 +02:00
Leonardo de Moura
d21945fa86
feat(library/phash_map): add persistent hash_map based on phashtable
2017-05-05 12:36:13 -07:00
Gabriel Ebner
f0d22ed3e5
feat(library/process,system/io): set environment variables for spawned processes
2017-05-04 16:41:11 -07:00
Gabriel Ebner
1b8533130b
feat(system/io): add function to get environment variables
2017-05-04 16:41:11 -07:00
Daniel Selsam
b7d20a333f
chore(src/library/constants): rm unused constants
2017-05-04 16:34:32 -07:00
Daniel Selsam
d727abeefc
chore(library/inductive_compiler/nested.cpp): prove all theorems in C++
2017-05-04 16:34:32 -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
39165ad66b
feat(library/parray): add helper methods and exclusive_access helper class
2017-05-04 15:35:14 -07:00
Leonardo de Moura
ae96ebf6ee
feat(library/parray): split "long" delta paths
2017-05-03 16:07:49 -07:00
Leonardo de Moura
90e434f78c
refactor(library/parray): minor refactoring
2017-05-03 13:44:42 -07:00
Sebastian Ullrich
b37b1fb7c6
refactor(library/type_context,frontends/lean/elaborator): move reflected code back into elaborator
...
Since we do not want recursive special handling of `reflected`, this seems to be
the simpler design.
2017-05-03 13:27:35 -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
2e5702d31e
fix(library/parray): it is unsafe to return reference
...
A reroot operation performed by another thread may invalidate the reference.
2017-05-03 10:02:10 -07:00
Leonardo de Moura
a8cc5c4e31
fix(library/parray): race conditions
2017-05-03 09:36:35 -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
ff916b3a93
chore(library/parray): avoid T m_elem; field at cell
...
This was bad since T default constructor would be invoked even when not
needed.
2017-05-02 16:20:15 -07:00
