Leonardo de Moura
|
968c0d799f
|
refactor(kernel): implement substitution methods
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
5f4b1cf47e
|
feat(kernel): define metavar substitution based on red-black trees
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
f855dbb7b0
|
feat(util): add maps based on red-black trees
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
54d5088c98
|
feat(util/rb_tree): add check_invariant for red black trees
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
1ab12eb105
|
refactor(util/splay_map): remove unnecessary operation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
528ea367ad
|
feat(util): add red-black trees
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
fdde12e6af
|
refactor(kernel): remove unnecessary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
2a73389ed3
|
refactor(kernel): justification objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
50300126a5
|
refactor(util/name_generator): make sure there is no risk of overflow, name generators will be extensively used in version 0.2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
501435f6fc
|
feat(kernel): add has_local predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
e1f4f1f0d1
|
feat(util/thread): add atomic_uchar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
997f32378c
|
refactor(kernel): remove unnecessary files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
6baa59376c
|
refactor(kernel): normalizer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:56 -07:00 |
|
Leonardo de Moura
|
eb046c11fb
|
refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
410d5cc8ed
|
fix(kernel): remove unnecessary file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
16aa1ebbac
|
refactor(kernel): replace_visitor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
101888e079
|
refactor(kernel): delete update_expr
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
b5f0f28009
|
refactor(kernel): environment, kernel object and exceptions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
3c8ccdd33d
|
test(util/exception): experiment with exceptions with nested std::function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
737fe6830f
|
test(tests/kernel): adjust expr tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
f986963a95
|
refactor(kernel): serializer and deserializer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
74f74d2f79
|
refactor(kernel): shallow copy procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
5da501d538
|
fix(kernel): style warnings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
73c8bf4436
|
refactor(tests/kernel): move tests to new kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
565dbe1700
|
fix(kernel/instantiate): bug in new head_beta_reduce
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
d17990ed78
|
refactor(kernel): add formatter and simplify contexts
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
53ee205dc6
|
fix(kernel): memory corruption bugs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
72e1678ad9
|
refactor(kernel): cleanup instantiate and abstract procedures, implement update procedures
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
db31cc37a1
|
refactor(kernel/free_vars): cleanup free_vars procedures
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
533f44e224
|
refactor(kernel/expr): for_each_fn, replace_fn, and find_fn without templates
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:55 -07:00 |
|
Leonardo de Moura
|
69b9f2dd37
|
refactor(kernel/expr): for_each and find functional objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
23988f528c
|
refactor(kernel/expr): add expr constructors, and expression equality test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
9d3db8de1f
|
fix(kernel/diff_cnstrs): missing include
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
02413d7c44
|
refactor(kernel/expr): adding suport for universe polymorphism, and simplify metavariable representation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
13cfd60622
|
fix(kernel/diff_cnstrs): copyright msg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
76b1ddb967
|
feat(kernel): add difference constraint solver with backtracking support, and justification generation, this solver will be used to check the satisfiability of universe level constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
9f93b5d97e
|
feat(kernel/level): new universe level datastructure for universe level polymorphism
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
1b6b33b3f5
|
refactor(kernel): start version 0.2, new kernel with universe polymorphism and better/cleaner support for metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-18 10:27:54 -07:00 |
|
Leonardo de Moura
|
0c1674ab70
|
feat(builtin): quotient types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-12 00:20:46 -07:00 |
|
Leonardo de Moura
|
e0eacd1f9f
|
feat(builtin): simpler encoding of sum types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-03 18:30:45 -08:00 |
|
Leonardo de Moura
|
f8a12363f2
|
doc(examples/wf): use 'have' construct in wf example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-03-03 18:29:19 -08:00 |
|
Leonardo de Moura
|
26bf21b91d
|
test(examples/lean): opaque pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-27 11:38:34 -08:00 |
|
Leonardo de Moura
|
1d10953da4
|
fix(library/elaborator): add hack for experimenting with algebraic hierarchy
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-25 11:20:40 -08:00 |
|
Leonardo de Moura
|
aa8240985a
|
test(examples/lean): small version of algebraic hierarchy (proof of concept)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-24 20:51:19 -08:00 |
|
Leonardo de Moura
|
309e7ba880
|
fix(library/elaborator): temporary fix for bug reported by Jeremy
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-24 15:26:21 -08:00 |
|
Leonardo de Moura
|
16844fff73
|
feat(builtin): simulate binary encoding
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-20 20:44:05 -08:00 |
|
Leonardo de Moura
|
d79e9af210
|
fix(frontends/lean): help msg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-18 09:31:30 -08:00 |
|
Leonardo de Moura
|
f781ad823c
|
doc(builtin): Diaconescu’s theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-18 09:12:09 -08:00 |
|
Leonardo de Moura
|
e9dada5e14
|
refactor(builtin/kernel): use standard definition for 'or' and 'and'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-17 12:05:34 -08:00 |
|
Leonardo de Moura
|
4692e04d70
|
feat(builtin/proof_irrel): prove proof irrelevance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-02-16 18:06:10 -08:00 |
|