michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
3310 commits 3 branches 0 tags 28 MiB
Commit graph

2807 commits

Author SHA1 Message Date
Leonardo de Moura
5c5dea7c8e feat(kernel/expr): add has_expr_metavar_strict 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 19:54:04 -07:00
Leonardo de Moura
5bf3197306 refactor(frontends/lean): create theorem_queue class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 15:00:51 -07:00
Leonardo de Moura
78a1670905 refactor(frontends/lean): cleanup add_delayed_theorem method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 14:01:20 -07:00
Leonardo de Moura
70ef92cd5e feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 10:53:44 -07:00
Leonardo de Moura
23af5ab217 fix(library/unifier): eager whnf application 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 10:37:02 -07:00
Leonardo de Moura
556861c8d6 fix(library/unifier): remove incorrect assertion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 07:52:10 -07:00
Leonardo de Moura
c1b523d642 feat(util/worker_queue): allow main thread to process tasks while waiting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 23:24:04 -07:00
Leonardo de Moura
3ec30bf537 feat(frontends/lean): add parallel_import option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 22:46:49 -07:00
Leonardo de Moura
709b5ce90f fix(kernel/justification): duplicate position 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 21:16:49 -07:00
Leonardo de Moura
70c887a0bd fix(library/unifier): fix cryptic error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 21:10:32 -07:00
Leonardo de Moura
01cec1e1f1 fix(library/unifier): more bugs in the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 20:05:37 -07:00
Leonardo de Moura
cf44c80ffb fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 16:00:38 -07:00
Leonardo de Moura
7b84503133 fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 15:03:57 -07:00
Leonardo de Moura
1c191c1ec7 fix(frontends/lean/elaborator): instantiate assigned metavariables before collecting unassigned ones 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 15:02:33 -07:00
Leonardo de Moura
0f12e5a35b fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 13:49:45 -07:00
Leonardo de Moura
a450ad5a95 feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:24:01 -07:00
Leonardo de Moura
a5b9a7b296 fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:10:45 -07:00
Leonardo de Moura
811f46e97b feat(frontends/lean/pp): add option for displaying internal names associated with private declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:03:54 -07:00
Leonardo de Moura
0c668a31fe fix(frontends/lean/pp): display private 'internal' names in a human readable way 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 10:58:13 -07:00
Leonardo de Moura
cd522ff670 feat(emacs): improve font highlighting in emacs mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 10:54:06 -07:00
Leonardo de Moura
a59eec39b8 feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:44:40 -07:00
Leonardo de Moura
022a151cf7 feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:33:31 -07:00
Leonardo de Moura
736b219e65 fix(frontends/lean/elaborator): pretty print placeholders as '_' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:46:03 -07:00
Leonardo de Moura
e7c7d5718a fix(frontends/lean/pp): fix bug in the pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:30:30 -07:00
Leonardo de Moura
15c1e39f88 feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 23:43:40 -07:00
Leonardo de Moura
48b902dc37 feat(library/unifier): solve constraints of the form '(max l1 l2) =?= 0' and '(imax l1 l2) =?= 0' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 20:30:51 -07:00
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