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
7df78ea503
feat(kernel): add combinator for combining normalizer_extensions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 10:00:40 -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
69d9c8b95d
fix(tests): to reflect recent changes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 13:20:24 -07:00
Leonardo de Moura
301c395e59
perf(kernel/metavar): performance problem with occurs method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 10:35:27 -07:00
Leonardo de Moura
61661478ad
refactor(kernel/metavar): simplify substitution class, and remove dead code
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 10:03:03 -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
999782d89d
refactor(kernel/replace_fn): use thread local cache
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 05:34:45 +01:00
Leonardo de Moura
0a556c4a91
feat(util): add worker queue
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 21:59:22 +01:00
Leonardo de Moura
9517f31a71
refactor(kernel/metavar): remove unnecessary functionality
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 04:45:50 +01:00
Leonardo de Moura
405e57eb2d
refactor(kernel/formatter): add formatter_factory, and simplify formatter interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 18:32:00 +01: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
7fb2b0f6d8
feat(kernel): add method 'may_reduce_later' to normalizer_extension, and improve unifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 22:31:05 -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
ec18bd93f9
feat(frontends/lean): send tactic hint table to elaborator
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 07:03:25 -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
fedbf8595b
feat(kernel/metavar): collect unassigned metavariables while instantiating
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 16:58:09 -07:00
Leonardo de Moura
2c3e3cb544
refactor(kernel/abstract): add abstract_locals, and remove abstract_p
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
9e50d5a1b8
test(util/lazy_list): add simple lazy_list example
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
07f2379dec
refactor(kernel): add mk_local function that has only two arguments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 14:27:26 -07:00
Leonardo de Moura
34dfacc10e
refactor(frontends/lean): Bool does not need to be a reserved keyword
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 10:52:12 -07:00
Leonardo de Moura
e7019ec840
feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 22:13:25 -07:00
Leonardo de Moura
b347117cf3
feat(util/scoped_map): add 'keep' method for closing a scope without undoing operations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 11:25:14 -07:00
Leonardo de Moura
3bde699fbe
feat(frontends/lean/parser): add parse_level
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-12 12:34:55 -07:00
Leonardo de Moura
5a008717a4
feat(frontends/lean/parser): add parse_notation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 21:00:34 -07:00
Leonardo de Moura
3dc26666b9
feat(frontends/lean): add parser interface
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 18:20:59 -07:00
Leonardo de Moura
d3e3301208
refactor(frontends/lean/scanner): use the parser configuration in the environment
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 10:59:12 -07:00
Leonardo de Moura
546f9dc00b
chore(frontends/lean): use consistent name conventions, rename token_set to token_table
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 09:18:57 -07:00
Leonardo de Moura
25b822b1c7
fix(tests/util/memory): remove reference to deleted function
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 13:29:45 -07:00
Leonardo de Moura
7847f8a0ca
fix(tests/util): disable some tests that do not compile on OSX + Boost + MULTI_THREAD
2014-06-07 13:14:17 -07:00
Leonardo de Moura
d827b56777
fix(util/memory): remove get_thread_allocated_memory, it used thread_local
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 13:05:03 -07:00
Leonardo de Moura
15f0899efb
refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive
...
Motivation: clang++ on OSX does not support 'thread_local'.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 10:18:36 -07:00
Leonardo de Moura
06d2ff021b
feat(util/thread_script_state): add system_import procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 16:23:24 -07:00
Leonardo de Moura
e9ef59ab3e
feat(util): add global (thread local) script_state objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 15:46:16 -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
d10d70423a
feat(frontends/lean): add new scanner
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 18:57:26 -07:00
Leonardo de Moura
4a25e7442a
feat(kernel/expr): add optional expression caching (aka "partial" hash-consing)
...
We do not enforce full hash-consing because we would need to synchronize
the access to the hashtable/cache.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 15:35:47 -07:00
Leonardo de Moura
df3280e86e
feat(util): add lru cache
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 13:26:02 -07:00
Leonardo de Moura
5a5d66edc8
feat(util/trie): add value() method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 01:19:23 -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
1b4c9f63ce
perf(kernel/environment): improve is_descendant performance, optimize for the common case: the is_descendant tree is huge but has few deep branches
...
This is an important optimization for module.cpp. The benchmark tests/lua/slow/mod2.lua is a good example where the cost of is_descendant was neutralizing the benefit of the replace method.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 22:29:03 -07:00
Leonardo de Moura
f375ed5f7a
test(tests/kernel/environment): add more tests for environment objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 12:42:29 -07:00
Leonardo de Moura
8872d4a531
refactor(kernel): rename definition class to declaration
...
The name was misleading since not every declaration is a definition.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:41:38 -07:00
Leonardo de Moura
5ce134e24e
chore(kernel): binder => binding where appropriate
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:37:27 -07:00
Leonardo de Moura
d625c9a26c
refactor(kernel): move max_sharing to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:15:08 -07:00
Leonardo de Moura
69e72c278d
feat(kernel): add proof irrelevance for classes
...
We can use this feature to implement proof irrelevance for Identity types.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:30:32 -07:00