Commit graph

3281 commits

Author SHA1 Message Date
Leonardo de Moura
a533bf29da fix(library/unifier): broken optimization was missing solution
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 17:41:22 -07:00
Leonardo de Moura
77c0456be4 fix(kernel/metavar): make sure instantiate_metavars_fn does not loop on 'fake' recursive dependencies, we say they are fake because they disappear after applying beta-reduction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 12:04:33 -07:00
Leonardo de Moura
2eb84c5f74 fix(library/unifier): make sure we do not miss dependency
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 11:38:43 -07:00
Leonardo de Moura
2fae6ebc3a feat(emacs): add missing keywords
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 08:50:18 -07:00
Leonardo de Moura
1f2099e298 perf(kernel/for_each_fn): use cache stack trick at for_each_fn
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 19:32:11 -07:00
Leonardo de Moura
7d25158254 fix(kernel/replace_fn): bug in the cache
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 18:33:15 -07:00
Leonardo de Moura
61df118339 refactor(kernel/for_each_fn): simplify module interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 18:16:41 -07:00
Leonardo de Moura
42867d6fcd refactor(kernel/find_fn): simplify find_fn module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 18:09:58 -07:00
Leonardo de Moura
314c0822de fix(library/unifier): bugs exposed by recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 17:31:07 -07:00
Leonardo de Moura
71afb83fcd feat(shell/lean): rename multi-threading option to -j
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 14:35:02 -07:00
Leonardo de Moura
13fe28dd1c perf(library/unifier): delay the instantiation of metavariables occurring in the types of local constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 14:31:30 -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
adddf06e44 perf(kernel/metavar): avoid destructive update in occurs method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 13:12:29 -07:00
Leonardo de Moura
4286f5dd36 perf(kernel/justification): make sure depends_on doesn't get 'lost' in justification objects with a lot of shared objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 11:56:17 -07:00
Leonardo de Moura
35481cb045 fix(library/unifier): potentially changing flag from l_false ==> l_undef
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 10:59:53 -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
caf3e5a449 fix(kernel/metavar): missing justification bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 08:41:09 -07:00
Leonardo de Moura
75005765d6 perf(library/unifier): add small performance improvement
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 17:58:40 -07:00
Leonardo de Moura
90189f8eb6 chore(frontends/lean/elaborator): fix outdated comment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 17:50:13 -07:00
Leonardo de Moura
35e7302d8a perf(frontends/lean/elaborator): fix performance bottleneck
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 17:45:45 -07:00
Leonardo de Moura
697bcf4b4f perf(library/unifier): improve performance of instantiate_meta method
It provides a significant performance boost in some files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 16:24:07 -07:00
Leonardo de Moura
5ad6d5cbc4 feat(kernel/converter): add eta-expansion to converter, this is important when terms contains metavariables
For example, consider the unification constrains

    fun (x : A), f (?m x)  =?=  f

Eta-reduction is not applicable since (?m x) is not a variable.
However, if we eta-expand the left-hand-side, we get

   fun (x : A), f (?m x)  =?=  fun (x : A), f x

which is reduced to

      (?m x) =?= x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 16:24:02 -07:00
Leonardo de Moura
e81d96ffc1 feat(build): add build option for jemalloc
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 13:44:47 -07:00
Leonardo de Moura
368c94ccc5 feat(util/rb_tree): use memory_pool at rb_tree, 5% performance improvement when using multiple threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 10:53:07 -07:00
Leonardo de Moura
fd7e20f11c fix(util/thread): thread_specific_ptr finalization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 10:50:44 -07:00
Leonardo de Moura
a7c6c3e840 fix(kernel/expr): memory corruption in dealloc method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 10:16:44 -07:00
Leonardo de Moura
b522ea6f2d refactor(library/standard): rename bit to bool
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 09:49: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
4c6ebdeaf9 perf(util/memory_pool): use memory_pool for hierarchical names and justification objects we get a 8% performance improvement when using multiple threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 09:18:26 -07:00
Leonardo de Moura
c8b6f0c7fb refactor(util): rename fixed_size_allocator to memory_pool
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 07:49:40 -07:00
Leonardo de Moura
725f370e59 fix(build): number of core detection on OSX
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 20:07:11 -07:00
Leonardo de Moura
77537d43a3 fix(util): add missing file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 18:58:24 -07:00
Leonardo de Moura
79ea7c5910 perf(kernel/expr): minimize access to system memory allocator by recycling expr_cells
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 18:46:47 -07:00
Leonardo de Moura
e3d4b2490d perf(kernel/type_checker): improve infer_app peformance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 17:11:47 -07:00
Leonardo de Moura
ad87c0b3e1 fix(frontends/lean): race condition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 09:32:13 -07:00
Leonardo de Moura
de657e8df0 fix(util/rc): reference counter memory_order flags
See discussion at
http://www.chaoticmind.net/~hcb/projects/boost.atomic/doc/atomic/usage_examples.html#boost_atomic.usage_examples.example_reference_counters
http://stackoverflow.com/questions/10268737/c11-atomics-and-intrusive-shared-pointer-reference-count

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 08:23:01 -07:00
Leonardo de Moura
c02629c76d feat(util/lean_path): allow 'import dirname' as shorthand for 'import dirname.default'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 19:59:13 -07:00
Leonardo de Moura
9c499e723f perf(build): use make -j option when invoking external makefile for compiling Lean libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 19:38:46 -07:00
Leonardo de Moura
cff6bf8c6d fix(library/module): sign error is circular module dependency is detected
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 19:21:54 -07:00
Leonardo de Moura
ba9dd8b686 fix(library/choice): style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-21 01:36:53 +01:00
Leonardo de Moura
9ef4d44a86 chore(frontends/lean): add 'replace' auxiliary funcs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 01:10:49 +01:00
Leonardo de Moura
438a42d010 feat(library/unifier): improve error message when metavar assignment is type incorrect
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 00:19:32 +01:00
Leonardo de Moura
e39a6e732a refactor(kernel/error_msgs): move pp_type_mismatch to error_msgs module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 00:19:31 +01:00
Leonardo de Moura
55db3aaaa1 fix(library/module): module index assignment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 00:19:31 +01:00
Leonardo de Moura
bef64305cf feat(kernel/constraint): add 'print' function for debugging purposes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 00:19:31 +01:00
Leonardo de Moura
c1b7d7bf7e fix(library/choice): we should be able to store 'choice' operators in .olean files, this can happen because of notation decls
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 00:19:31 +01:00
Leonardo de Moura
d69db172a1 chore(kernel/replace_fn): add syntax sugar for replace function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-19 12:53:37 +01:00
Leonardo de Moura
6b60db7b93 fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-19 09:55:34 +01:00
Leonardo de Moura
66ba3c8a0b fix(frontends/lean/elaborator): bug in the elaborator reported by Jeremy
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-18 23:48:27 +01:00
Soonho Kong
5118ee7a83 chore(CMakeLists.txt): mark gmp and mpfr as required packages 2014-07-18 08:29:51 -04:00
Leonardo de Moura
4c98686d4f fix(emacs): syntax highlight bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 20:48:06 +01:00
Leonardo de Moura
661e681ac9 feat(frontends/lean/decl_cmds): allow parameters with different types to be declared using the same 'parameters' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 20:47:33 +01:00
Leonardo de Moura
120d3b5c1a fix(kernel/type_checker): error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 19:38:20 +01:00
Leonardo de Moura
9289717169 perf(kernel/expr): inline get_free_var_range, and cache its value for local and metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 08:51:46 +01:00
Leonardo de Moura
9fcb31bd5e perf(kernel/instantiate): add custom instantiate for 'easy' cases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 08:29:04 +01:00
Leonardo de Moura
a78fb8f013 perf(library/unifier): minimize the number of constraints generated in the flex_rigid 'imitation' step
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 06:32:21 +01:00
Leonardo de Moura
8798fa4419 fix(kernel/replace): make sure 'replace' is reentrant
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-17 04:37:27 +01:00
Leonardo de Moura
aae40f07e2 perf(kernel/expr): use thread local deletion buffer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-16 08:39:03 +01:00
Leonardo de Moura
a748e8f858 perf(kernel/type_checker): improve infer_lambda performance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-16 07:52:53 +01:00
Leonardo de Moura
c97b4c7725 perf(kernel/converter): improve is_def_eq_binding
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-16 07:33:45 +01:00
Leonardo de Moura
6ddba9c276 fix(library/unifier): bug in process_delta
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-16 04:55:09 +01:00
Leonardo de Moura
c8849d42e9 fix(library/unifier): tolerate exceptions in the type_checker::infer method. This can happen since when we try projections we don't check whether they are type correct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-16 03:05:19 +01:00
Leonardo de Moura
f7317a7139 feat(build): compile HoTT library when building
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 21:56:36 +01:00
Leonardo de Moura
359bfe93d5 feat(library/hott): add basic HoTT definitions and theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 21:46:33 +01: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
bd0cc5c365 fix(library/expr_pair): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 04:11:27 +01:00
Leonardo de Moura
a18cf94d09 perf(library/unifier): minimize the use of instantiate_metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 03:55:27 +01:00
Leonardo de Moura
29c7eeaa99 refactor(library/unifier): improve occurs_context_check
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 02:08:16 +01:00
Leonardo de Moura
46005b4ffe perf(kernel/metavar): improve occurs_expr method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 01:57:17 +01:00
Leonardo de Moura
0f44e3c9f4 fix(frontends/lean): calc configuration commands, add check_constant_next auxiliary method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 01:19:47 +01:00
Leonardo de Moura
ffdb43da02 perf(kernel/type_checker): improve infer_pi performance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 22:56:38 +01:00
Leonardo de Moura
b72105efff perf(kernel/type_checker): improve infer_lambda performance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 22:39:45 +01:00
Leonardo de Moura
eac38d43c2 refactor(kernel/type_checker): break infer_type_core into smaller methods
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 22:15:52 +01:00
Leonardo de Moura
7ed373811d perf(frontends/lean/elaborator): improve visit_binding performance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 17:08:32 +01:00
Leonardo de Moura
91e8f0b8fa chore(frontends/lean/elaborator): replace ... withe exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 16:37:55 +01:00
Leonardo de Moura
2e6184a721 fix(frontends/lean): more bugs in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 06:27:36 +01:00
Leonardo de Moura
b53e6eda58 refactor(frontends/lean): eliminate the abstract method 'family' from parser
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 05:44:06 +01:00
Leonardo de Moura
8167ad329f fix(frontends/lean): bug in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 05:04:01 +01:00
Leonardo de Moura
195429611b refactor(frontends/lean/builtin_cmds): cleanup 'check' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 04:25:53 +01:00
Leonardo de Moura
5c51be4585 refactor(frontends/lean): use expr_struct_set when collecting locals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 04:12:58 +01:00
Leonardo de Moura
6c442b250c refactor(frontends/lean): minor code reorg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 03:47:49 +01:00
Leonardo de Moura
43fa75f7a9 fix(frontends/lean/decl_cmds): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 03:36:06 +01:00
Leonardo de Moura
fab7934265 refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 02:53:02 +01:00
Leonardo de Moura
bdfd219246 feat(frontends/lean): improve error message for placeholder that can't be synthesized
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 22:35:57 +01:00
Leonardo de Moura
943092eaf0 refactor(frontends/lean/elaborator): reorg class elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 14:50:52 +01:00
Leonardo de Moura
c03ae24d22 fix(frontends/lean/elaborator): option name
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 14:03:47 +01:00
Leonardo de Moura
1d16b5d2ad fix(frontends/lean/elaborator): propagate tags for getting better error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 11:10:26 +01:00
Leonardo de Moura
8da44f1cd5 feat(frontends/lean/parser): disable quasie-hash consing in new threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 04:11:17 +01:00
Leonardo de Moura
614d8a768b fix(library/unifier): flex_rigid case (?M ...) =?= (f ...), where f is not a constant nor a local
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 02:46:04 +01:00
Leonardo de Moura
a31457efde fix(frontends/lean/parser): copy rec and initial fields when processing Exprs and ScopedExpr
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 01:24:55 +01:00
Leonardo de Moura
585127ef66 fix(util/worker_queue): bug in join method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 23:25:43 +01:00
Leonardo de Moura
7ccb9a389c feat(frontends/lean): process theorems in parallel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 22:50:57 +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
6d95250d4b fix(library/kernel_serializer): make sure temporary (internal) binder names do not leak into .olean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 20:23:38 +01:00
Leonardo de Moura
cb93d194ed perf(frontends/lean/elaborator): improve performance of pi_abstract_context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 17:49:14 +01:00
Leonardo de Moura
03bbec08e5 perf(frontends/lean/elaborator): replace abstract with abstract_local
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 09:54:22 +01:00
Leonardo de Moura
1d273fcfdd chore(frontends/lean): rename 'obtains' to 'obtain'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 06:35:24 +01:00
Leonardo de Moura
a38dc76b37 feat(kernel/metavar): add option to instantiate only expr metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 05:54:05 +01:00
Leonardo de Moura
80d1a6b993 perf(kernel/converter): do not cache easy cases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 05:39:14 +01:00
Leonardo de Moura
391e5e2bc2 perf(library/unifier): use d_instantiate_metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 05:12:09 +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
50f76fd138 perf(library/unifier): improve m_mvar_occs management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 04:23:02 +01:00
Leonardo de Moura
c3e8e83e50 perf(library/unifier): simple optimization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-11 20:21:41 +01:00
Leonardo de Moura
1230e942aa feat(library/unifier): handle 'first-order' flex-flex constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-11 04:51:28 +01:00
Leonardo de Moura
024299f56b fix(frontends/lean): name of auxiliary hypothesis in 'obtains' expression, and also marked them as non-contextual
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-11 04:50:53 +01:00
Leonardo de Moura
cf34f75ab5 feat(frontends/lean): add 'obtains' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-11 04:08:51 +01:00
Leonardo de Moura
9a3227344e fix(library/tactic): compilation warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 23:23:48 +01:00
Leonardo de Moura
eeedb6fb18 fix(kernel/expr_eq_fn): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 23:21:24 +01:00
Leonardo de Moura
b62abf0f06 refactor(library/tactic/goal): remove redundance, goal pp method was duplicating some of the functionality provided by the pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 18:59:03 +01:00
Leonardo de Moura
6af7e7f794 fix(kernel/expr_eq_fn): take local pp name into account when annotations are considered in the equality test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 18:56: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
c13c75b93e feat(frontends/lean/pp): add option for displaying fully qualified names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 15:55:19 +01:00
Leonardo de Moura
49bc3fffbd fix(frontends/lean/pp): purify procedure for local names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 14:13:51 +01:00
Leonardo de Moura
fc8ddcb0ce feat(frontends/lean): improve 'check' command when used inside sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 14:07:41 +01:00
Leonardo de Moura
1a6d0784f2 feat(kernel/level): improve universe level normalization procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:49:41 +01:00
Leonardo de Moura
313c7066e7 feat(frontends/lean): add Type' as notation for Type.{_+1}
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:28:36 +01:00
Leonardo de Moura
d9b2801eeb feat(frontends/lean): use the same universe in declarations such as (A B : Type)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:18:52 +01:00
Leonardo de Moura
12d89ea0b9 fix(kernel/level): is_geq predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:18:41 +01:00
Leonardo de Moura
0ec6fa02de feat(frontends/lean/pp_options): remove the 'lean.' prefix
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 19:19:35 -07:00
Leonardo de Moura
aff766430d fix(frontends/lean/pp): universe pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 19:17:28 -07:00
Leonardo de Moura
43eba857cb feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 18:47:10 -07:00
Leonardo de Moura
d31cde473e fix(util/sexpr): nested Lua objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 11:13:17 -07:00
Leonardo de Moura
2ef7b9be2f feat(frontends/lean): add basic pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 01:12:36 -07:00
Leonardo de Moura
91b0dcad0f fix(library/tactic): avoid 'unknown' message in trace_tac when position information is not available
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 17:48:41 -07:00
Leonardo de Moura
a1601e7a5f feat(library/tactic/apply_tactic): add option for 'refreshing' universe metavariables in the 'apply' tactic
The new test ../../tests/lean/run/tactic27.lean demonstrates why we need this feature. The tactic 'apply @refl' is actually 'apply @refl.{?l}'. It is used inside of a repeat tactical. Each iteration of the 'repeat' may need to use a different value for ?l. Before this commit, there was not way to say we want a fresh ?l each iteration.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 16:55:23 -07:00
Leonardo de Moura
547ca9b3c4 fix(library/inductive_unifier_plugin): missing test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 16:39:39 -07:00
Leonardo de Moura
4505016154 feat(frontends/lean): allow tactic_hints to be applied when class-instance mechanism fails
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
5e836092cc feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
a3be63af73 feat(frontends/lean): add tactic_hint command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -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
2fa2589220 feat(frontends/lean): add pretty printer configuration options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
da4c1922e3 feat(frontends/lean): add '_root_' prefix for referencing names in the root namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 19:15:46 -07:00
Leonardo de Moura
b43fb7448c feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 19:00:06 -07:00
Leonardo de Moura
e6d4c01b88 feat(frontends/lean): check whether namespace exists or not in the 'using' command, add to_valid_namespace_name helper function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 18:17:10 -07:00
Leonardo de Moura
bd1873f6b1 feat(frontends/lean): add coercion modifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 17:48:20 -07:00
Leonardo de Moura
08465f049a feat(frontends/lean): remove [class] annotation and 'class' command, they are redundant, we only need [instance] and 'instance'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 16:09:30 -07:00
Leonardo de Moura
112353861c feat(frontends/lean): rename command 'reset_proof_qed' to 'set_proof_qed'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 15:48:16 -07:00
Leonardo de Moura
c16951aba6 fix(library/aliases): aliasing behavior
The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 15:40:55 -07:00
Leonardo de Moura
b9d08ff28c feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 14:53:06 -07:00
Leonardo de Moura
10b0dfeb37 feat(frontends/lean/class): allow many instances to provided with a single 'instance' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 14:41:14 -07:00
Leonardo de Moura
6ceecf6a15 feat(library/aliases): remove duplicates from aliasing tables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 12:59:57 -07:00
Leonardo de Moura
a84107db3d fix(util/sexpr): Lua 5.1 incompatibility
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 12:55:00 -07:00
Leonardo de Moura
b956ce68d2 feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 12:50:43 -07:00
Leonardo de Moura
fe448d47be feat(library/unifier): improve failure report
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 12:03:37 -07:00
Leonardo de Moura
ce14ced08e feat(util/sexpr): allow Lua objects to be embedded in Lean s-expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 10:45:19 -07:00
Leonardo de Moura
c47d9c01ee fix(util/sexpr): crash in the sexpr Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 09:41:14 -07:00
Leonardo de Moura
831de22bcd fix(frontends/lean): bugs in notation management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 09:31:42 -07:00
Leonardo de Moura
e8bd267a00 fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 21:54:16 -07:00
Leonardo de Moura
67363c893e chore(frontends/lean/elaborator): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 21:41:19 -07:00
Leonardo de Moura
48b28ad75c fix(library/unifier): missing test in flex_rigid
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 21:36:23 -07:00
Leonardo de Moura
dcf7cf00ff fix(*): bugs in the type checker, inductive datatypes, and unifier
The bugs were indentified when performing the tiny change in the file
tests/lean/run/group.lean
2014-07-06 18:44:56 -07:00
Leonardo de Moura
9a13bef4f3 fix(frontends/lean): fix (and simplify) parameter universe inference
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 16:56:54 -07:00
Leonardo de Moura
9be1a4ab46 fix(library/module): module index assignment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 23:32:18 -07:00
Leonardo de Moura
29981322b9 fix(kernel/type_checker): missing check
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 21:50:32 -07:00
Leonardo de Moura
b3de4bb061 fix(frontends/lean/decl_cmds): modifiers should be after universe parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 21:49:32 -07:00
Leonardo de Moura
55894f01e3 feat(frontends/lean): add 'opaque_hint' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 18:58:20 -07:00
Leonardo de Moura
32a605e793 fix(frontends/lean/builtin_cmds): allow 'check' command to unfold the current module opaque definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 17:39:49 -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
fc4df6a430 feat(kernel/expr): add O(1) predicates has_expr_metavar and has_univ_metavar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 13:11:30 -07:00
Leonardo de Moura
e366aadad0 refactor(library/converter): expose is_opaque predicate in the converter interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 12:05:23 -07:00
Leonardo de Moura
8aa217ea76 chore(library/unifier): update comments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 11:06:13 -07:00
Leonardo de Moura
72bce91c18 refactor(library/unifier): move inductive datatype support to inductive_unifier_plugin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 11:00:35 -07:00
Leonardo de Moura
e445515f2b refactor(kernel): move standard and hott kernel instantiations to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 10:31:27 -07:00
Leonardo de Moura
ab929d7201 refactor(library/unifier): store the unifier_plugin in the environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 10:25:58 -07:00
Leonardo de Moura
a52c9f4e2b feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 09:43:16 -07:00
Leonardo de Moura
efabd2280c feat(library/unifier): allow unifier to unfold opaque definitions of the current module
It is not clear whether this is a good idea or not. In some cases, it seems to do more harm than good.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 00:46:03 -07:00
Leonardo de Moura
ac1585fd1a feat(library/unifier): divide constraints in clear groups
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 00:04:38 -07:00
Leonardo de Moura
f242971b55 feat(library/unifier): delay constraints where the lhs or rhs are of the form (?m ... (intro ...))
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 23:36:31 -07:00
Leonardo de Moura
1e40525a0c fix(library/unifier): simple bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 21:15:32 -07:00
Leonardo de Moura
4af474010a fix(frontends/lean/elaborator): unintended use of local instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 18:49:05 -07:00
Leonardo de Moura
99fb6431a6 fix(frontends/lean/elaborator): support for local instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 18:38:08 -07:00
Leonardo de Moura
6ea7bb3ea4 feat(frontends/lean/builtin_exprs): add 'including' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 18:37:09 -07:00
Leonardo de Moura
8ab0b5bee3 feat(frontends/lean/elaborator): use local declarations as class instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 18:18:25 -07:00
Leonardo de Moura
00e1a7db23 feat(frontends/lean/elaborator): add class instance elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 15:45:50 -07:00
Leonardo de Moura
079672f6f9 feat(frontends/lean): add 'class' and 'instances' infrastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 14:28:09 -07:00
Leonardo de Moura
f1884ee5f9 chore(frontends/lean): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 13:22:32 -07:00
Leonardo de Moura
d7cb1952ae feat(kernel): simplify choice_fn, and make its interface closer to the unifier_plugin interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 12:47:33 -07:00
Leonardo de Moura
b94ce412ae fix(library/unifier): non-termination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 10:32:01 -07:00
Leonardo de Moura
e0501104e2 feat(library/tactic): add 'fixpoint' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 01:30:28 -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
ce282a549a feat(frontends/lean): add 'prefix' notation declaration command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 21:37:56 -07:00
Leonardo de Moura
110b622b83 feat(library/unifier): add support for unification constraints of the form "(elim ... (?m ...)) =?= t", where elim is an eliminator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 20:41:51 -07:00
Leonardo de Moura
c854ad3d65 refactor(library/unifier): add is_def_eq alias
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 18:01:59 -07:00
Leonardo de Moura
b5f63e78ca feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 17:23:29 -07:00
Leonardo de Moura
fa1857e6a9 fix(frontends/lean/notation_cmd): fix default, add 'prev' action
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 16:44:44 -07:00
Leonardo de Moura
aba4534acb feat(library/unifier): 'forget' justifications after finding a solution, the justifications are only needed inside the unifier (for implementing nonchronological backtracking)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 14:14:07 -07:00
Leonardo de Moura
a009225435 feat(kernel/metavar): expose destructive assign
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 14:07:47 -07:00
Leonardo de Moura
b49902807c refactor(kernel/metavar): separate substitution from their justifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 14:01:22 -07:00
Leonardo de Moura
abbd054b51 feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 13:04:46 -07:00
Leonardo de Moura
079592c446 feat(library/unifier): eagerly apply substitution to improve quick failure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 12:58:30 -07:00
Leonardo de Moura
db0ef64c04 feat(util/lazy_list_fn): handle the 'is_nil' case more efficiently
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 11:29:04 -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
dd96bb151b refactor(library/unifier): reduce the number unify procedure 'flavors'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 11:15:43 -07:00
Leonardo de Moura
d63ccbcf94 fix(library/unifier): missing case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 10:51:59 -07:00
Leonardo de Moura
0ff145e59b feat(library/tactic): add apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 09:20:01 -07:00
Leonardo de Moura
c9994ca00c feat(library/unifier): when projecting give preference to most recent locals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 09:01:29 -07:00
Leonardo de Moura
e3ab0a1d10 feat(frontends/lean): improve error messages when users forget to import 'tactic'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 08:33:29 -07:00
Leonardo de Moura
6b8b5f3dd8 feat(library/tactic): expose more builtin tactics, cleanup expr_to_tactic procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 08:06:28 -07:00
Leonardo de Moura
a7d660f875 feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 20:45:10 -07:00
Leonardo de Moura
5527955ba8 feat(frontends/lean): add 'proof-qed' notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 19:30:48 -07:00
Leonardo de Moura
138267b53a feat(frontends/lean/elaborator) add trick for improving error messages when mixing tactics, elaboration and exact tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:58:32 -07:00
Leonardo de Moura
c3abf81382 chore(emacs): update emacs mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:37:53 -07:00
Leonardo de Moura
60c637fb9d feat(library/tactic): add 'exact' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:37:32 -07:00
Leonardo de Moura
37b5b7c4c2 feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:10:42 -07:00
Leonardo de Moura
04b2a620f8 fix(frontends/lean/elaborator): instantiate metavariables before displaying error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:07:11 -07:00
Leonardo de Moura
3809a3cc2c chore(frontends/lean): code cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 17:32:13 -07:00
Leonardo de Moura
181a739a5e feat(frontends/lean/elaborator): report unassigned metavariables as goals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 16:26:06 -07:00
Leonardo de Moura
6a6ebd5c2d refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 15:39:25 -07:00
Leonardo de Moura
d46ade94a7 refactor(frontends/lean): remove unnecessary code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:47:41 -07:00
Leonardo de Moura
3e1bb96935 feat(library/tactic/goal): propagate tag (for position information) from goal to subgoal
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:47:18 -07:00
Leonardo de Moura
ee531ec0e2 feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact]
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:09:01 -07:00
Leonardo de Moura
0f27856e4a feat(library/tactic): new apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 13:14:50 -07:00
Leonardo de Moura
cc3fb0c51f feat(util/name_generator): allow name generator to be created without providing any argument in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 12:39:41 -07:00
Leonardo de Moura
6ab46396d8 feat(library/tactic): expose 'trace' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:52:45 -07:00
Leonardo de Moura
e1d909455c refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:45:09 -07:00
Leonardo de Moura
a66a08c89e feat(frontends/lean): parse strings as expressions of type 'string.string'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:00:55 -07:00
Leonardo de Moura
8b8881deae fix(util/hash): relax pre-condition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 09:56:50 -07:00
Leonardo de Moura
f464775af6 fix(frontends/lean/parser): bug when parsing identifiers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:36:25 -07:00
Leonardo de Moura
0198dfc7c5 feat(frontends/lean): parse numerals as expressions of type 'num.num'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:09:33 -07:00
Leonardo de Moura
7593ee1468 refactor(library/standard): remove parameter from 'tactic' inductive type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:09:24 -07:00
Leonardo de Moura
b2b76b078f feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 20:43:53 -07:00
Leonardo de Moura
cbac21ec7f feat(library/tactic): add trick for 'embedding' tactics inside Lean expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 19:05:22 -07:00
Leonardo de Moura
2df92b0701 refactor(library/tactic): simplify proof_state
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 18:02:17 -07:00
Leonardo de Moura
7abe2e7242 fix(frontends/lean/token_table): precedence for '@'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 17:06:09 -07:00
Leonardo de Moura
5b69f88664 feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:55:41 -07:00
Leonardo de Moura
ec3743dede fix(frontends/lean/parser): avoid nontermination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:46:58 -07:00
Leonardo de Moura
8cdf44b87b feat(frontends/lean/notation_cmd): allow 'max' to use as a precedence level
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:46:32 -07:00
Leonardo de Moura
4cb5f97038 refactor(library/tactic): simplify tactic framework, no more proof builders
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:11:19 -07:00
Leonardo de Moura
ad12abcdb4 fix(library/unifier): bug in process_eq_constraint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:22:05 -07:00
Leonardo de Moura
abe12b0631 fix(shell/lean): only save .olean file if there are no errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:04:18 -07:00
Leonardo de Moura
c84218e24a chore(frontends/lean/inductive_cmd): cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 17:16:10 -07:00
Leonardo de Moura
3e299a1d5a refactor(frontends/lean/parser): move parser Lua bindings to a separate file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 17:00:10 -07:00
Leonardo de Moura
bccc3df1aa chore(frontends/lean): reduce code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 16:52:20 -07:00
Leonardo de Moura
e3f9b21c30 fix(kernel/inductive): bug in inductive datatype computational rule, we *must* first instantiate universe variables, *and then* the arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 14:15:16 -07:00
Leonardo de Moura
6e6f778ecf fix(kernel/converter): missing case for local constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 12:57:25 -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
c2ab31113f refactor(library/tactic): remove cex_builder and 'precision' for proof_state's
These two features make sense for solvers, but not in a general purpose tactic framework for building proofs like the one in Lean.

In most cases, we cannot build a counterexample anyway. These two features should be added in a custom framework for combining preprocessing techniques like in Z3.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 08:48:07 -07:00
Leonardo de Moura
8d584e54da feat(frontends/lean): add exact_apply
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 00:51:11 -07:00
Leonardo de Moura
ccdb96775f feat(frontends/lean/parser): allow 'assume'/'take'/'fun' as notation for apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 23:00:41 -07:00
Leonardo de Moura
33cb9382aa feat(frontends/lean): add beta-reduction tactic command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 19:41:54 -07:00
Leonardo de Moura
360e9b9486 feat(library/tactic): add apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 18:33:53 -07:00
Leonardo de Moura
6645fdeae0 feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 12:24:13 -07:00
Leonardo de Moura
a8f9594046 refactor(kernel/instantiate): rename instantiate_params to instantiate_univ_params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 12:09:55 -07:00
Leonardo de Moura
2510d5722a feat(frontends/lean): add unfold tactic command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 12:05:45 -07:00
Leonardo de Moura
937d7b2813 fix(library/tactic): unfold tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 12:04:58 -07:00
Leonardo de Moura
6d09d82a7c feat(frontends/lean): add notation for orelse tactic, add show and now tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 11:39:18 -07:00
Leonardo de Moura
a1bbb09de4 feat(frontends/lean): add notation for then tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 11:24:56 -07:00
Leonardo de Moura
15f270d9f3 fix(library/tactic): memory leak that only happens when compiling with clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 11:07:06 -07:00
Leonardo de Moura
6891f48c67 fix(library/module): do not store full path of imported modules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 10:48:57 -07:00
Leonardo de Moura
e59889d84f fix(build): do not build libraries when cross compiling
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 10:00:08 -07:00
Leonardo de Moura
1f0171cd57 fix(frontends/lean/dependencies): compilation warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:55:30 -07:00
Leonardo de Moura
ffa175009b feat(frontends/lean): use tactics for solving unassigned metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:50:16 -07:00
Leonardo de Moura
1e39a21823 feat(frontends/lean): add basic tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:03:51 -07:00
Leonardo de Moura
cf28981f45 feat(tests/lean/run): add test_single script that sets the LEAN_PATH
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 07:47: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
5a7e198583 feat(build): add Makefile for libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 18:41:53 -07:00
Leonardo de Moura
65c63e146f feat(frontends/lean): add display_deps function, and --deps command line option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 18:35:18 -07:00
Leonardo de Moura
193ce35419 refactor(frontends/lean/inductive_cmd): redesign inductive datatype elaboration, use the new elaborator, and use simpler algorithm to infer the resulting universe
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 15:33:56 -07:00
Leonardo de Moura
0adacb5191 feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 13:57:36 -07:00
Leonardo de Moura
0e015974ca fix(library/unifier): bug in process_flex_rigid, also cleanup the code and break it into different cases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 11:19:56 -07:00
Leonardo de Moura
7075f6e94a fix(library/module): make sure decls from imported modules have module_idx > 0
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 08:36:54 -07:00
Leonardo de Moura
58b6169e8b fix(library/max_sharing): take binder annotations into account
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 08:31:09 -07:00
Leonardo de Moura
47ff300d1a fix(frontends/lean): '@' explicit mark
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 07:30:36 -07:00
Leonardo de Moura
cf9b486179 feat(frontends/lean): automatically import lua modules imported by imported lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 23:23:51 -07:00
Leonardo de Moura
2673a33bf3 fix(util/thread_script_state): new state was being added twice to g_states, use import_explicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 19:58:28 -07:00
Leonardo de Moura
e408998e06 fix(library/tactic): name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 18:42:59 -07:00
Leonardo de Moura
fa72e7b874 refactor(library/tactic): simplify tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 18:35:59 -07:00
Leonardo de Moura
5524c6c3d8 refactor(library/tactic/proof_state): simplify proof state
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 14:49:48 -07:00
Leonardo de Moura
c6ac89d967 refactor(library/tactic/proof_builder): simplify proof builder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 12:25:04 -07:00
Leonardo de Moura
aaa7960b75 refactor(library/tactic/goal): use local names for hypotheses
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 11:11:12 -07:00
Leonardo de Moura
d84b745241 refactor(library/tactic/cex_builder): simplify cex_builder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 07:14:33 -07:00
Leonardo de Moura
b4e4c4d610 chore(library/tactic): remove unnecessary file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 07:02:13 -07:00
Leonardo de Moura
f1d8d8dcf9 chore(library/tactic): update goal objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 07:00:12 -07:00
Leonardo de Moura
ad70044ae1 chore(library/tactic): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-27 07:00:12 -07:00
Leonardo de Moura
e55b4bf86d fix(library/unifier): bug in flex_rigid case: binding imitation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 20:43:49 -07:00
Leonardo de Moura
50e21586b0 feat(library/unifier): do not create a case-split for choice constraints that produce only one alternative
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 18:52:13 -07:00
Leonardo de Moura
443022d840 feat(util/lazy_list): add is_nil predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 18:51:35 -07:00
Leonardo de Moura
ccce9d90a4 feat(frontends/lean/elaborator): add 'delayed coercions', add example demonstrating why the new feature is useful
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 18:39:23 -07:00
Leonardo de Moura
ed299c0914 feat(library/coercion): add has_coercions_to function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 18:38:27 -07:00
Leonardo de Moura
b11e1a5f34 feat(kernel/type_checker): add mk_app_justification auxiliary function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 18:38:09 -07:00
Leonardo de Moura
e769121c2a fix(frontends/lean/elaborator): memory leaks that only occur when compiling with clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 16:02:54 -07:00
Leonardo de Moura
340dc622c6 fix(kernel/formatter): make sure simple formatter output is not sensitive to internal names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 14:58:59 -07:00
Leonardo de Moura
150d285b39 fix (library/unifier): occurs_context_check
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 14:45:36 -07:00
Leonardo de Moura
16bdc51fc4 refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 13:36:31 -07:00
Leonardo de Moura
ac03b3204a fix(kernel/formatter): add missing parentheses
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 12:07:28 -07:00
Leonardo de Moura
a70f8dd98e feat(kernel/inductive): mark parameters, type formers and indices as implicit parameters in the elimination rule
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 11:05:14 -07:00
Leonardo de Moura
5e0e737213 feat(library/scoped_ext): do not import 'children' namespace objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 10:32:34 -07:00
Leonardo de Moura
930960c54d fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 10:06:50 -07:00
Leonardo de Moura
0480dab986 feat(frontends/lean/parse_table): avoid duplicates in the parse table
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 09:32:19 -07:00
Leonardo de Moura
ab2bbaef3f feat(util/list_fn): add remove function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 09:32:19 -07:00
Leonardo de Moura
2d2f23cda6 feat(library/lean/lean): improve overload error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 08:52:40 -07:00
Leonardo de Moura
656bcd55ed fix(frontends/lean): save 'choice' position
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 08:50:44 -07:00
Leonardo de Moura
6085a54416 feat(library/error_handling): improve unifier_exception error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 08:49:50 -07:00
Leonardo de Moura
e735a8e5ff fix(library/unifier): bug in conflict resolution
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 08:42:40 -07:00
Leonardo de Moura
cdc41244ae fix(kernel/justification): missing 'const'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 08:18:18 -07:00
Leonardo de Moura
52ff29a6f7 feat(frontends/lean): add 'coercion' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-26 08:08:39 -07:00
Leonardo de Moura
06f9e7bfdd fix(build): add missing file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 18:12:23 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 17:50:49 -07:00
Leonardo de Moura
9f83ef8f6c chore(frontends/lean/elaborator): cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 17:13:03 -07:00
Leonardo de Moura
a42a80407a fix(library/unifier): when imitating (f a), abstract local constants occurring in f
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 16:11:31 -07:00
Leonardo de Moura
1d4352aeb4 fix(kernel/converter): missing case: two constants c.{l1} and c.{l2} where l1 and l2 are structurally different but equivalent (or can be made equivalent)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 16:05:41 -07:00
Leonardo de Moura
543b1003a6 fix(frontends/lean/elaborator): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 13:11:35 -07:00
Leonardo de Moura
c9133f33dd feat(kernel/expr): add flat_app auxiliary function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 12:51:22 -07:00
Leonardo de Moura
f2b41312fb feat(frontends/lean): add '@' explicit notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 12:50:47 -07:00
Leonardo de Moura
905209df1c fix(frontends/lean/elaborator): to cache values, we must push/pop whenever we update the m_ctx
Thus, we are disabling the cache for now.
It is also unclear whether it is useful or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 11:05:14 -07:00
Leonardo de Moura
5c40b466cc fix(kernel/type_checker): use the application to provide error location
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 10:42:58 -07:00
Leonardo de Moura
0791c83731 fix(frontends/lean/parser): add missing save_pos
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 10:32:43 -07:00
Leonardo de Moura
6ec5d768d0 fix(kernel/type_checker): bug in the app_delayed_justification object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 10:09:45 -07:00
Leonardo de Moura
f981a4c1fe fix(library/unifier): bug in lambda_abstract_locals auxiliary function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 09:59:08 -07:00
Leonardo de Moura
6db6048bf8 feat(library/error_handling): pretty print unifier exceptions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 09:41:25 -07:00
Leonardo de Moura
18a883ab1b fix(library/unifier): set conflict if type mismatch during metavariable assignment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 09:33:34 -07:00
Leonardo de Moura
5b6589709c fix(frontends/lean/decl_cmds): allow binders but no type in definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 09:00:57 -07:00
Leonardo de Moura
c427c5bdc9 feat(kernel/type_checker): improve 'declaration still has metavars' error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 08:51:33 -07:00
Leonardo de Moura
3e7dfa6212 fix(frontends/lean): infer type of definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 08:39:14 -07:00
Leonardo de Moura
d055c4880f feat(frontends/lean): connect new elaborator to frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-25 08:31:00 -07:00
Leonardo de Moura
fe0cee7536 feat(frontends/lean): add frontend elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 18:25:56 -07:00
Leonardo de Moura
d7436e600b fix(library/resolve_macro): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 17:40:58 -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
609aeae390 feat(kernel/type_checker): expose app_delayed_justification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 14:54:37 -07:00
Leonardo de Moura
2c0f596665 fix(library/choice): avoid assertion violation when Lua API is misused
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 12:14:38 -07:00
Leonardo de Moura
3169f8c126 feat(library): add mk_explicit/is_explicit procedures for '@'-expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 12:11:27 -07:00
Leonardo de Moura
d915f0cc32 refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-24 09:00:14 -07:00
Leonardo de Moura
d8a8300a4f fix(kernel/expr): initialization problem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 16:55:51 -07:00
Leonardo de Moura
61595f516c fix(frontends/lean/notation_cmd): initialization bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 16:20:28 -07:00
Leonardo de Moura
aa8b5655dd feat(frontends/lean): add notation overwrite
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 16:10:36 -07:00
Leonardo de Moura
60f230a206 doc(library/unifier): ignore flex-flex constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 14:33:09 -07:00
Leonardo de Moura
7df397fe63 test(lua): add universe constraint unifier test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 14:19:02 -07:00
Leonardo de Moura
a0e4dccdac refactor(kernel/constraint): rename choice constraint fields
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 13:52:03 -07:00
Leonardo de Moura
60c60c6cf5 feat(library/kernel_bindings): add mk_choice_cnstr to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 13:39:21 -07:00
Leonardo de Moura
6d14de76f3 feat(kernel/constraint): add 'delayed' flag to choice constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 12:56:06 -07:00
Leonardo de Moura
66016df0ad feat(library/unifier): add imitation step for macros
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 12:44:22 -07:00
Leonardo de Moura
2fa5b17592 feat(library/unifier): add unifier.max_steps unifier.use_exceptions options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 12:38:57 -07:00
Leonardo de Moura
7b188ea37e feat(library/unifier): implement flex-rigid case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 11:00:35 -07:00
Leonardo de Moura
68d55ef398 doc(library/unifier): document some of the unifier_fn methods
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-23 08:22:38 -07:00
Leonardo de Moura
9f7b92a410 refactor(library/unifier): combine active and delayed constraint sets
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 21:10:59 -07:00
Leonardo de Moura
4da9c2a2cb fix(emacs): modify emacs mode to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:56:53 -07:00
Leonardo de Moura
5bd86754af feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:51:00 -07:00
Leonardo de Moura
228f51dcfa feat(library/unifier): add support for choice constraint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 17:21:24 -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
c8a07dee53 feat(library/unifier): add unifier_plugin support, and unit test with plugin implemented using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 16:27:04 -07:00
Leonardo de Moura
238a0dbfba fix(library/unifier): memory violation, and missing set_conflict
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 14:09:06 -07:00
Leonardo de Moura
25cb1bf6a1 fix(kernel/converter): use type_checker::scope to make sure we restore the cache, and remove constraints when is_def_eq fails in the converter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 14:08:54 -07:00
Leonardo de Moura
a1d94d71ec refactor(kernel/converter): eliminate converter::context, use type_checker directly
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 13:52:47 -07:00
Leonardo de Moura
edb2e85898 refactor(kernel/type_checker): remove type_checker::imp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 13:39:58 -07:00
Leonardo de Moura
29a00c46d0 feat(library/unifier): add main loop and resolve_conflict
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 11:57:10 -07:00
Leonardo de Moura
644c387cfe refactor(kernel/constraint): rename: level constraints are also equality constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 10:50:47 -07:00
Leonardo de Moura
1c47bd4847 fix(kernel/converter): remove temporary workaround, and temporarily disable unit test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 10:39:22 -07:00
Leonardo de Moura
73666af4a4 fix(library/register_module): missing open_unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 10:01:51 -07:00
Leonardo de Moura
c7c5e41653 fix(frontends/lean/parser): warning when compiling in release mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 09:58:05 -07:00
Leonardo de Moura
3953d4d122 feat(kernel/type_checker): add push/pop methods to type_checker, they control the cache, and allow the type checker to reuse results even when it is used inside of a backtracking search
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 09:58:05 -07:00
Leonardo de Moura
eca22edda3 fix(kernel/type_checker): restore type checker cache when a failure occurs, do not send constraints to add_cnstr_fn when a type checker failure occurrs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-22 09:00:32 -07:00
Leonardo de Moura
9c745057b4 feat(library/unifier): add unify_fn skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 20:08:39 -07:00
Leonardo de Moura
aac3830e31 fix(kernel/converter): add temporary fix, we need to be able to backtrack constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 20:08:39 -07:00
Leonardo de Moura
f9a21166f0 feat(kernel/type_checker): add type_checker::is_def_eq method that takes a justification as argument
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 20:08:39 -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
bf8f3318d8 feat(library): add unifier module skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 13:38:17 -07:00
Leonardo de Moura
37bee8c852 refactor(kernel/type_checker): simplify replace constraint_handler with closure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -07:00
Leonardo de Moura
86a56fbd2d feat(library/kernel_bindings): expose methods substitution::for_each_expr and substitution::for_each_level in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-21 12:25:54 -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
67088b130e refactor(kernel/constraint): simplify constraint interface, and add choice constraint
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
2589d60bfd feat(frontends/lean): add nameless 'have' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 17:18:18 -07:00
Leonardo de Moura
4b227409bf feat(frontends/lean): add 'then have' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 14:27:21 -07:00
Leonardo de Moura
4560413a92 feat(frontends/lean): add '[fact]' modifier for 'have' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
39177ec10a feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
16412daf39 feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 11:58:05 -07:00
Leonardo de Moura
5c17411a86 fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-20 09:46:58 -07:00
Leonardo de Moura
2cc8172d61 refactor(frontends/lean): remove m_pos field from parameter object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 23:06:49 -07:00
Leonardo de Moura
2954d10df5 refactor(kernel/converter): remove unnecessary exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 23:06:49 -07:00
Leonardo de Moura
05d1832425 refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 22:33:58 -07:00
Leonardo de Moura
0cc8117fb4 fix(frontends/lean): add missing file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-19 06:10:15 -07:00
Leonardo de Moura
bdab979e09 feat(frontends/lean): add inductive_cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 16:00:59 -07:00
Leonardo de Moura
461689f758 refactor(frontends/lean/builtin_cmds): move declaration commands to new file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 15:55:52 -07:00
Leonardo de Moura
08845be2fc feat(frontends/lean/notation_cmd): improve 'notation' cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 09:28:01 -07:00
Leonardo de Moura
3e3c4ee5ed feat(frontends/lean/parser): add local_scope object to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 08:38:23 -07:00
Leonardo de Moura
6259d20218 feat(frontends/lean/parser): expand Lua parser API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 08:03:17 -07:00
Leonardo de Moura
77c5319c4a chore(*): remove Lua 'migrate'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-18 07:01:34 -07:00
Leonardo de Moura
3ea24c0f32 fix(library/kernel_bindings): set_environment and set_io_state objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:36:47 -07:00
Leonardo de Moura
06002c5312 feat(frontends/lean/parser): use system_import when processing Lean import command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:09:42 -07:00
Leonardo de Moura
b9a7cc41ef feat(shell): use system_import for lua files provided in the command line (i.e., their code will be available for all threads)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 22:04:09 -07:00
Leonardo de Moura
1378fa5cbb refactor(util/script_state): remove support for threads and communication channels from the Lua API, the goal is to keep is simple, and use one Lua state object per thread
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 21:56:45 -07:00
Leonardo de Moura
f17e8a853a feat(frontends/lean): allow parser actions to be implemented using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 21:56:16 -07:00
Leonardo de Moura
4cbc429192 feat(frontends/lean/calc): add parse_calc function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 17:16:15 -07:00
Leonardo de Moura
037cfcf622 refactor(frontends/lean/notation_cmd): add register_notation_cmds procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 13:39:44 -07:00
Leonardo de Moura
f6dc6e6504 feat(emacs): add new calc commands to lean emacs mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 13:36:35 -07:00
Leonardo de Moura
e178979061 feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 13:35:31 -07:00
Leonardo de Moura
ddba6b222a feat(frontends/lean): add calculational proof environment extension, it stores transitivity, reflexivity (and substitution) rules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 13:13:13 -07:00
Leonardo de Moura
50806314d4 feat(util/name): add name_pair, and lex order
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 13:09:29 -07:00
Leonardo de Moura
f9d81c24d3 feat(library/expr_lt): add lex comparison for expression pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 12:14:22 -07:00
Leonardo de Moura
28c904abea feat(frontends/lean/parser): add 'flag' for disabling 'unknown identifier' errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 10:30:03 -07:00
Leonardo de Moura
4be05e1d8c refactor(frontends/lean): expose notation_entry and token_entry structures, and add functions for parsing notation without affecting the environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 10:12:04 -07:00
Leonardo de Moura
819c8276f2 feat(frontends/lean/builtin_cmds): add 'variables' command family
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-17 08:25:00 -07:00
Leonardo de Moura
ea49176043 feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 18:42:39 -07:00
Leonardo de Moura
639d58f4c7 feat(frontends/lean/builtin_cmds): add 'print options' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 17:31:28 -07:00
Leonardo de Moura
3e377a9732 feat(frontends/lean/builtin_cmds): add 'set_option' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 17:27:43 -07:00
Leonardo de Moura
0779db7ae9 fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:56:11 -07:00
Leonardo de Moura
73b7a44c84 fix(shell/CMakeFiles): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:55:16 -07:00
Leonardo de Moura
82e79d9c78 fix(frontends/lean/parser): style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:54:44 -07:00
Leonardo de Moura
a964ceb0e2 feat(frontends/lean): add 'import' command, add command line option for setting number of threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:37:46 -07:00
Leonardo de Moura
79d32b768d feat(shell): add '--hott' command line option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 15:50:27 -07:00
Leonardo de Moura
4f3da90443 feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 15:04:29 -07:00
Leonardo de Moura
2c4175341c feat(library/placeholder): allow types to be attached to placeholders
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 14:35:55 -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
21c54755a9 fix(kernel/converter): bug in is_def_eq
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 14:09:12 -07:00
Leonardo de Moura
f1e3449aae fix(frontends/lean): propagate position information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 13:20:10 -07:00
Leonardo de Moura
2312f43443 fix(kernel/abstract): propagate tags when abstracting
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 13:00:13 -07:00
Leonardo de Moura
f70b1b028a feat(frontends/lean): provide position to parse_fn external function, add 'by' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 12:28:58 -07:00
Leonardo de Moura
77b0e9d05d feat(emacs): add 'abbreviation' in the list of keywords
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 10:54:04 -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
6db265e7ab feat(frontends/lean/builtin_exprs): parse '_' placeholder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 10:41:08 -07:00
Leonardo de Moura
249168ce0b feat(emacs): add 'postfix' in the list of keywords
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 10:03:36 -07:00
Leonardo de Moura
5ce0502a36 feat(frontends/lean/builtin_exprs): add parser for 'let' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 09:50:34 -07:00
Leonardo de Moura
775e10186d refactor(parser): use 'scope objects' for creating local scopes and setting m_type_use_placeholder flag
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 09:24:41 -07:00
Leonardo de Moura
cb49e3719e fix(util/optional): bug in emplace method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 09:24:15 -07:00
Leonardo de Moura
27130c9499 feat(frontends/lean): local notation 'shadows' global one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 11:50:41 -07:00
Leonardo de Moura
28047a33ae feat(frontends/lean): add local notation support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 11:30:52 -07:00
Leonardo de Moura
9931033554 feat(shell/lean): remove --olean option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 10:50:35 -07:00
Leonardo de Moura
64cafd6875 feat(frontends/lean/notation_cmd): add 'notation' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 10:49:05 -07:00
Leonardo de Moura
961b0bfacf feat(kernel/type_checker): use argument position when reporting application type mismatch errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 10:06:53 -07:00
Leonardo de Moura
9b389a96d5 feat(frontends/lean/notation_cmd): modify infixl/infixr/postfix command syntax
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-15 08:28:49 -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
891a3fb48b feat(frontends/lean): add command block reader with snapshot and resume
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 14:13:32 -07:00
Leonardo de Moura
6b99a29c2c refactor(frontends/lean): add local_decls template that is cheap to copy
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 09:56:05 -07:00
Leonardo de Moura
5fee6fd140 feat(shell/lean): add '-o' command line option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 08:10:43 -07:00
Leonardo de Moura
282a35bd1b feat(frontends/lean): add '#setline' directive
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-14 07:28:56 -07:00
Leonardo de Moura
48c58af9b5 feat(frontends/lean/parser): allow explicit universe level to be provided to aliases and locals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 18:00:52 -07:00
Leonardo de Moura
a65c43c0db feat(frontends/lean/builtin_cmds): add definition command family
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 17:30:35 -07:00
Leonardo de Moura
01cecb76db feat(frontends/lean/builtin_cmds): add 'variable' command family
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 15:13:50 -07:00
Leonardo de Moura
ce259e6265 feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 11:34:43 -07:00
Leonardo de Moura
378b691ea7 feat(emacs): update keywords
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 11:25:24 -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
5aca452439 feat(library/aliases): add 'exceptions' and support for universes to add_aliases procedure, add for_each_universe method to environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-13 08:26:05 -07:00
Leonardo de Moura
a914345d29 feat(library): new scoping framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-12 19:33:02 -07:00
Leonardo de Moura
d50376249f feat(library/aliases): add level aliases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-12 12:35:02 -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
cffbae3667 test(tests/lean/run): add new test group, where we just execute Lean (and don't check output)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 21:07:23 -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
e7d7996fa9 feat(frontends/lean/parser): add parser_binder(s) and abstract methods
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 18:51:12 -07:00
Leonardo de Moura
959c3ffc68 feat(frontends/lean/parser): add parse_id method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 15:09:16 -07:00
Leonardo de Moura
1a67cc7293 fix(kernel/for_each_fn): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 15:06:11 -07:00
Leonardo de Moura
05edbe00ad chore(shell): re-activate .lean tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:36:42 -07:00
Leonardo de Moura
1c5d3295cc refactor(library/deep_copy): use replace to implement deep_copy
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
4f83b1a50b feat(library): add choice expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
c8e272d20b feat(util/lua): add check_atleast_num_args helper function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
1972a09021 feat(frontends/lean/builtin_cmds): add simple 'print' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
7fd502993b refactor(frontends/lean/cmd_table): remove register_builtin_cmd procedures, they would cause initialization problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:35:34 -07:00
Leonardo de Moura
2e8ebb6d9e feat(frontends/lean/parser): add 'parse_commands' and 'parse_script'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 14:32:07 -07:00
Leonardo de Moura
431b47377d feat(library/kernel_bindings): add 'set_env/set_environment' commands for updating the global environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 11:03:12 -07:00
Leonardo de Moura
8fcc25d55a fix(frontends/lean/token_table): static initialization problem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-11 10:56:04 -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
e2adb101d5 feat(frontends/lean): add parser_config environment extension
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 10:39:22 -07:00
Leonardo de Moura
637eae40ad feat(library/aliases): add support for alias overloading
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 10:05:51 -07:00
Leonardo de Moura
d81df2efe2 feat(frontends/lean/parse_table): add use_lambda_abstraction flag to scoped_expr_actions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-10 09:39:01 -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
00e0cc15ba feat(frontends/lean/token_set): add token_set Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 16:49:22 -07:00
Leonardo de Moura
25640faaeb fix(util/trie): bug in for_each method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 16:43:01 -07:00
Leonardo de Moura
af0c93e0eb feat(frontends/lean/parse_table): add typedef for notation::parse_table
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 15:54:56 -07:00
Leonardo de Moura
439b6c1e96 feat(frontends/lean/parse_table): add parse_table Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 15:33:39 -07:00
Leonardo de Moura
722ea7273e feat(frontends/lean): add parse_table datastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-09 13:20:33 -07:00
Leonardo de Moura
fe6ab51c12 feat(kernel/inductive): add APIs for retrieving information about declared inductive datatypes, intro rules, and elimination rules
The new API is important for implementing environment transformation procedures, and export Lean environment to different systems (e.g., Coq).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-08 17:15:21 -07:00
Leonardo de Moura
1c49b4d85f chore(*): replace unique_lock with lock_guard when we do not need to use conditional variables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 20:55:25 -07:00
Leonardo de Moura
fb5c7c8e92 fix(util/stackinfo): on OSX Boost does not seem to be based on pthread library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 20:47:46 -07:00
Leonardo de Moura
7124866a4f fix(library/module): potential deadlock when child thread threw an exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 20:34:18 -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
a04af30d85 fix(CMakeLists): remove -pthread flag when compiling using Boost on OSX
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 13:21:00 -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
a42856c1d2 refactor(*): minimize dependency on thread local storage, simplify MK_THREAD_LOCAL_GET
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 12:16:01 -07:00
Leonardo de Moura
d9794d8ea4 feat(CMakeLists): hide compilation warnings due to Boost when using g++ on OSX
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 11:59:31 -07:00
Leonardo de Moura
482f5b01e9 feat(util/thread): add simpler MK_THREAD_LOCAL_GET macro for when BOOST=OFF and MULTI_THREAD=ON
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 11:34:50 -07:00
Leonardo de Moura
8d1ec69599 fix(CMakeLists): use Boost_LIBRARIES
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 11:31:56 -07:00
Leonardo de Moura
5bf4138a4f feat(util/thread): add custom MK_THREAD_LOCAL_GET macros for when LEAN_MULTI_THREAD is not defined
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 10:41:17 -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
91df9a5550 feat(util/thread): add LEAN_THREAD_PTR macro, it uses boost::thread_specific_ptr instead of thread_local keyword when we compile with Boost
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 08:16:20 -07:00
Leonardo de Moura
6700cf1f73 fix(util/thread): add missing declaration when compiling with Boost
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-07 08:05:19 -07:00
Leonardo de Moura
af0b02f521 fix(util/thread_script_state): add a better workaround for clang++ bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:54:10 -07:00
Leonardo de Moura
89a7898054 fix(*): static variable initialization problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:44:12 -07:00
Leonardo de Moura
3562c76161 fix(util/sexpr/options): add workaround for clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:14:39 -07:00
Leonardo de Moura
db36d465dc chore(util/sexpr): cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:01:43 -07:00
Leonardo de Moura
4a43016735 fix(kernel/expr): expr_cache initialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-06 18:00:26 -07:00
Leonardo de Moura
8d4312d9d8 fix(util/thread): warning messages 2014-06-06 17:50:46 -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
4cf1b05831 refactor(library/token_set): move to frontends/lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 13:10:50 -07:00
Leonardo de Moura
70c3ae8692 feat(library/token_set): register builtin commands
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 13:05:40 -07:00
Leonardo de Moura
5b898aa3ed refactor(util/trie): modify interface to avoid the creation of many temporary optional values and inc/dec reference counters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-05 12:40:51 -07:00
Leonardo de Moura
220f94d36e feat(library/kernel_bindings): expose instantiate_levels
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-04 16:26:26 -07:00
Leonardo de Moura
1c96373c1a feat(library/kernel_bindings): expose replace_fn in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-04 15:26:55 -07:00
Leonardo de Moura
bab430af43 chore(kernel/expr): cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-04 14:51:36 -07:00
Leonardo de Moura
3354832c21 perf(kernel/expr_eq_fn): delay cache allocation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 17:03:09 -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
45a3ab5141 refactor(library/aliases): it is bad design to instantiate parameter using the parameter name, the parameter names have no semantic value
Moreover, we could create type incorrect aliases by "accident".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 15:20:14 -07:00
Leonardo de Moura
1f6cfce05c refactor(library/placeholder): use different names for different placeholders, it is bad design to assume that two structurally identical expressions are different when they are allocated twice (this design is not compatible with any form of hash-consing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 14:59:00 -07:00
Leonardo de Moura
fc4b6a92cc fix(util/lru_cache): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 14:59:00 -07:00
Leonardo de Moura
b81d536946 fix(util/stackinfo): make sure check_stack can be invoked before 'main' (i.e., during initialization)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 14:57:32 -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
02df63b85e fix(kernel/level): add workaround for clang++ bug: memory leak at thread_local
The fix has an advantage. There is only one copy of level Zero in the system even when multiple threads are used.
Moreover, it does no require any form of synchronization, and modules can be initialized in any order.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 10:37:50 -07:00
Leonardo de Moura
076414693a feat(library/kernel_bindings): improve argument validation in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 10:17:12 -07:00
Leonardo de Moura
a9a38675cb feat(util/lua): add helper functions for checking expected number of arguments in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 10:16:27 -07:00
Leonardo de Moura
7dba2c29d2 feat(library): add token set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 02:34:12 -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
ab5f570924 refactor(kernel/constraint): remove choice constraints from the kernel, the kernel does not use them, we will implement them in elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 00:46:28 -07:00
Leonardo de Moura
931ebf9637 chore(util/rb_tree): cleanup code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 00:40:52 -07:00
Leonardo de Moura
536b7539c6 chore(kernel/inductive): cleanup code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-03 00:38:45 -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
f816487f4b fix(kernel/level): add (trivial) case for is_geq predicate: l >= 0 for any l
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:13:50 -07:00
Leonardo de Moura
045fa911d1 fix(library/kernel_bindings): missing kind in lean_kind
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:12:02 -07:00
Leonardo de Moura
ab7469c175 fix(library/scope): warning message, and old comment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 18:08:46 -07:00
Leonardo de Moura
1467bb256e chore(library): remove unnecessary code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 16:22:38 -07:00
Leonardo de Moura
33bbcd9526 chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 16:20:34 -07:00
Leonardo de Moura
82e1f87e08 feat(kernel): add function param_names_to_levels
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 16:17:04 -07:00
Leonardo de Moura
96f639811c chore(kernel/level): remove unnecessary code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 15:42:37 -07:00
Leonardo de Moura
712c10f818 fix(library/scope): make sure the local universe names do not conflict with universe parameter names when close a section, add declaration parameter name sanitizers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 15:39:57 -07:00
Leonardo de Moura
f82658f213 feat(library): add helper functions for 'updating' declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 15:13:38 -07:00
Leonardo de Moura
e155708dda feat(util): add (functional) name_map
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 14:46:13 -07:00
Leonardo de Moura
dcacf6fbca refactor(util): rename name_map to name_hash_map
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 14:34:22 -07:00
Leonardo de Moura
b6d2328c1d fix(library/scope): make sure local levels are added in the beginning of the universe parameter list
The idea is to make sure it is consistent with the behavior used for regular local parameters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 14:06:31 -07:00
Leonardo de Moura
e9664cb042 fix(kernel/type_checker): check if the declaration contains duplicate universe level parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 13:57:43 -07:00
Leonardo de Moura
9b6b162a7c fix(library/scope): bug when abstracting inductive declaration in the end of a section
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 13:46:16 -07:00
Leonardo de Moura
6ee272477a fix(library/private): bug when preserving private names at end_section
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 11:32:14 -07:00
Leonardo de Moura
936ca80b9b fix(library/scope): bug in add_definition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 11:04:34 -07:00
Leonardo de Moura
e56307f006 fix(library/scope): bug in end_scope procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 10:43:28 -07:00
Leonardo de Moura
6e113206b6 feat(library/scope): add support for inductive datatypes in sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-02 10:28:07 -07:00
Leonardo de Moura
d36ef5dcbe feat(library/private): preserve 'hidden/private name => user name' map when section is closed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-01 18:09:11 -07:00
Leonardo de Moura
585f3adde1 feat(library/scope): add sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-01 17:55:11 -07:00
Leonardo de Moura
286d7f0e64 feat(library): add namespace management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 15:41:01 -07:00
Leonardo de Moura
3145cee51f refactor(library/aliases): move replace_prefix to util/name
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 15:11:22 -07:00
Leonardo de Moura
f7b3061a66 feat(library/module): improve 'import module' error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:52:06 -07:00
Leonardo de Moura
75abcea83f fix(library/kernel_bindings): Lua API consistency, environment:add method also register declaration in the export table
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:20:57 -07:00
Leonardo de Moura
7bd10c2d2d feat(library/module): export global universe level declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-31 12:12:41 -07:00
Leonardo de Moura
1b5366cfb7 feat(library): add module for implementing aliases and 'using' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 21:42:40 -07:00
Leonardo de Moura
6902d8cb05 feat(library): add simple placeholder module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 20:28:28 -07:00
Leonardo de Moura
72f9e26dab refactor(library/private): add hidden_to_user_name and user_to_hidden_name functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-30 17:52:01 -07:00
Leonardo de Moura
128d668f03 feat(library): add support for creating 'private/hidden' names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 18:37:09 -07:00
Leonardo de Moura
13f9db26b7 refactor(library): add module namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:58:47 -07:00
Leonardo de Moura
fc7d5461b1 feat(library/kernel_bindings): add to_io_state_ext helper function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:35:11 -07:00
Leonardo de Moura
f8e71f711f feat(library/expr_lt): add expr_quick_cmp functional object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:34:16 -07:00
Leonardo de Moura
88440cbb3e feat(util/name): add optional<name> helper functions for implementing Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 13:33:42 -07:00
Leonardo de Moura
bfa9b90af0 feat(library/kernel_bindings): used 'named' parameters in import_modules API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 11:03:44 -07:00
Leonardo de Moura
ade5d99023 feat(library/modules): add option for discarding the proof of imported theorems (after checking them)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-29 10:56:28 -07:00
Leonardo de Moura
28b9d17a14 perf(library/module): do not use multiple threads when skipping type checking, add flag to disable/enable type checking theorems asynchronously
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-28 10:04:42 -07:00
Leonardo de Moura
e206fcc1af perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications
We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 23:16:52 -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
0f894f4618 chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 17:47:53 -07:00
Leonardo de Moura
4cbcc73bb6 feat(build): add GPROF compilation mode for using gprof
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 10:21:03 -07:00
Leonardo de Moura
6129cccc66 perf(library/shared_environment): replace shared_mutex with simple mutex, the shared_mutex is just overhead and impacts negatively on performance tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 08:34:44 -07:00
Leonardo de Moura
045a83153c doc(lua): update Lua API documentation, and reactivate doc tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-27 08:09:54 -07:00
Leonardo de Moura
75117bede8 fix(library/kernel_bindings): use standard environment in import_modules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 15:54:08 -07:00
Leonardo de Moura
eca906b074 feat(library/module): add inductive decls to .olean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 15:38:09 -07:00
Leonardo de Moura
49e1f78a33 feat(library/kernel_serializer): add serializer/deserializer for inductive decls
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 15:37:53 -07:00
Leonardo de Moura
bb9830f10c test(shell): add command line tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 04:53:04 -07:00
Leonardo de Moura
2d31c6c0b2 feat(library/coercion): improve get_user_coercions API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 11:35:47 -07:00
Leonardo de Moura
e058839d24 fix(library/coercion): allow cycles in the coercion graph
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 11:08:49 -07:00
Leonardo de Moura
71b555ab15 test(lua): coercion module error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 10:01:04 -07:00
Leonardo de Moura
ef14c3d67e fix(library/coercion): coercion replacement
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 09:49:26 -07:00
Leonardo de Moura
eb6d72a20c fix(library/coercion): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 08:55:20 -07:00
Leonardo de Moura
fc1819aadd test(lua): coercion serialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 08:38:50 -07:00
Leonardo de Moura
f598c6a110 fix(library/coercion): bug in coercion to function-class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 08:21:53 -07:00
Leonardo de Moura
118eae2733 fix(library/coercion): bug add_coercion
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 07:45:49 -07:00
Leonardo de Moura
e9e61fec51 feat(library/coercion): add for_each_coercion procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 07:45:49 -07:00
Leonardo de Moura
a408883c92 fix(library/coercion): bug in de-Bruijn indices
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 07:45:49 -07:00
Leonardo de Moura
f050308df7 feat(kernel/instantiate): relax apply_beta pre-conditions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 07:45:41 -07:00
Leonardo de Moura
1ee6bb48fc fix(library/coercion): bug in add_coercion_trans
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 06:25:31 -07:00
Leonardo de Moura
6536232107 feat(library/coercion): expose coercion module in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-25 06:05:31 -07:00
Leonardo de Moura
2be9bcef78 feat(library/coercion): add coercion management implementation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-24 19:28:42 -07:00
Leonardo de Moura
1cff37a084 feat(library/module): use io_state to report warning messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-24 14:08:15 -07:00
Leonardo de Moura
5df2331159 feat(library/io_state): add constructor for copying io_state, but replacing channels
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-24 13:51:39 -07:00
Leonardo de Moura
49b2bb209d refactor(kernel/formatter): formatter_cell object should not perform destructive updates
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-24 13:51:39 -07:00
Leonardo de Moura
f8255ddac6 fix(library/module): deadlock
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 16:46:53 -07:00
Leonardo de Moura
d30c600eb2 fix(library/module): bug in module import
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 16:23:47 -07:00
Leonardo de Moura
879572ee7e fix(kernel/module): non-termination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 15:12:47 -07:00
Leonardo de Moura
902b6160fa fix(kernel/module): deadlock
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 14:43:03 -07:00
Leonardo de Moura
2344fb9476 feat(kernel/expr): use the expression depth in the hash code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 14:16:51 -07:00
Leonardo de Moura
a3b0200d32 feat(library/module): do not use threads when lean is not compiled with LEAN_MULTI_THREAD
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 11:32:24 -07:00
Leonardo de Moura
b68b9ccc05 fix(kernel/environment): bug in extension id checking
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 11:24:00 -07:00
Leonardo de Moura
be96dc2ddf fix(library/module): bug in next_task method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 11:13:38 -07:00
Leonardo de Moura
c593247fcc fix(library/kernel_serializer): bug in declaration serialization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 11:11:16 -07:00
Leonardo de Moura
61b662151e fix(library/module): bug in export_module procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 10:57:11 -07:00
Leonardo de Moura
6bbb9d3667 feat(library/kernel_bindings): declarations added with the function add_decl are automatically registered in the to-export list
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 10:52:47 -07:00
Leonardo de Moura
1a663afda4 feat(library/module): add extra function for adding uncertified declarations when trust_lvl > LEAN_BELIEVER_TRUST_LEVEL
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 10:50:34 -07:00
Leonardo de Moura
a0a70bcea7 feat(library/kernel_bindings): expose import/export functions in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-23 09:35:32 -07:00
Leonardo de Moura
21905289fa feat(library/module): add module import procedure
The modules are processed in parallel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-22 18:15:44 -07:00
Leonardo de Moura
76177d7765 feat(library/kernel_bindings): improve type_checker:check Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-22 14:10:25 -07:00
Leonardo de Moura
6246fae32c fix(kernel/inductive): inductive datatype declaration validation bug pointed out by Cody Roux
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 16:29:25 -07:00
Leonardo de Moura
a45dc0bb86 chore(kernel): remove dead code, we don't have level constraints anymore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 15:46:17 -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
e39feabb72 feat(library/module): add declaration reader
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:54:29 -07:00
Leonardo de Moura
9f4bae6856 feat(library/kernel_bindings): add hott_environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:49:30 -07:00
Leonardo de Moura
45d473d44e feat(kernel): add mk_hott_environment function for creating HoTT compatible environments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:31:34 -07:00
Leonardo de Moura
4d1fecb21d refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:24:24 -07:00
Leonardo de Moura
f08a852da8 feat(library/kernel_bindings): expose environment::add(declaration) method in the Lua API, and add example to demonstrate its usage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:12:55 -07:00
Leonardo de Moura
9b9041fa2e feat(kernel/environment): add method for adding declarations that were not type checked (if trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:12:26 -07:00
Leonardo de Moura
8ffe66dc4f feat(library): add module system API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 18:35:59 -07:00
Leonardo de Moura
dd3edcb19f feat(library): add shared environment object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 15:42:52 -07:00
Leonardo de Moura
11fc917102 test(lua): add tests for improving kernel_bindings coverage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 12:16:12 -07:00
Leonardo de Moura
c5e8c10c9d fix(library/normalize): bug in normalize
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 11:53:58 -07:00