Commit graph

633 commits

Author SHA1 Message Date
Leonardo de Moura
fbf13994d8 refactor(*): use + for concatenating format objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 09:35:25 -07:00
Leonardo de Moura
01736bf82a feat(util/sexpr/format): expose flatten
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 12:00:32 -07:00
Leonardo de Moura
e602c4ba49 feat(frontends/lean): change multicomment to /- ... -/
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:55:13 -07:00
Leonardo de Moura
b746492ac8 refactor(library/simple_formatter): rename simple_formatter to print
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:32:08 -07:00
Leonardo de Moura
7d987df429 refactor(kernel/formatter): move simple_formatter to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:26:45 -07:00
Soonho Kong
42c2fef0f2 fix(tests/util/sequence.cpp): clang build error 2014-08-20 21:20:17 -07:00
Leonardo de Moura
9588336c15 refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
4cf3d32e0c chore(*): create alias for std::pair
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
fcf1778ee0 feat(util): add sequence object with O(1) concatenation operation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
0d5e346143 fix(library/expr_lt): make sure the builtin order is AC-compatible
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 15:51:10 -07:00
Leonardo de Moura
2dca68e645 chore(util/list): add inline functions for commonly used patterns in list processing code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-03 13:51:38 -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
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