Commit graph

2923 commits

Author SHA1 Message Date
Leonardo de Moura
33c77afc29 feat(frontends/lean/structure): add 'structure' command skeleton
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
2b4bd66081 feat(build): generate tests for all code blocks in org-files, and examples at ./examples/standard
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 12:06:11 -07:00
Leonardo de Moura
5f360cd8ec feat(kernel/error_msgs): improve application type mismatch error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 07:08:12 -07:00
Leonardo de Moura
555425539d refactor(kernel/error_msgs): remove dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 06:52:59 -07:00
Leonardo de Moura
864fdd37da refactor(library/aliases): aliases are from name to names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 21:01:59 -07:00
Leonardo de Moura
d1fe1286c0 fix(library/unifier): bug introduced today in consume_tc_cnstrs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 17:16:30 -07:00
Leonardo de Moura
bc0a8b8da4 feat(emacs): make lean-mode org-mode friendly
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 17:03:06 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:12:54 -07:00
Leonardo de Moura
83d38674c9 feat(kernel/error_msgs): improve cryptic type mismatch error messages where the types may seem identical because key information is being suppressed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 09:41:25 -07:00
Leonardo de Moura
0cdd4a267c feat(frontends/lean/pp): pretty print 'show' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 21:56:35 -07:00
Leonardo de Moura
60cc9ac8e2 feat(frontends/lean/pp): pretty print 'have' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 21:35:26 -07:00
Leonardo de Moura
cf35c07786 fix(frontends/lean): fix 'let' annotation placement and pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 21:00:22 -07:00
Leonardo de Moura
206206060f test(tests/lean/hott): add some of Vladimir's definitions as tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 20:50:37 -07:00
Leonardo de Moura
8e402ae862 fix(kernel/type_checker): error message position information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 20:33:44 -07:00
Leonardo de Moura
cb232f2a9b fix(kernel/inductive): use has_expr_metavar_strict instead of has_expr_metavar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 19:57:54 -07:00
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
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