lean2

Author	SHA1	Message	Date
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
Leonardo de Moura	8872d4a531	refactor(kernel): rename definition class to declaration The name was misleading since not every declaration is a definition. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-20 10:41:38 -07:00
Leonardo de Moura	00b1a84051	feat(library/kernel_bindings): expose environment::for_each method in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-20 10:16:19 -07:00
Leonardo de Moura	34a9c8304a	feat(kernel/environment): add for_each method for traversing environment declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-20 10:15:28 -07:00
Leonardo de Moura	8a8c5a2b84	feat(library/kernel_bindings): add normalize, whnf, type_check, infer_type methods to environment object Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-20 09:40:50 -07:00
Leonardo de Moura	11793e7998	feat(library): add simple normalization procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-20 09:40:30 -07:00
Leonardo de Moura	4103c85ce3	feat(library/kernel_bindings): improve Fun/Pi Lua APIs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-20 09:00:19 -07:00
Leonardo de Moura	bcb9965844	feat(library/kernel_bindings): improve Fun/Pi Lua APIs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 17:07:20 -07:00
Leonardo de Moura	9de8249d8f	feat(kernel): let Pi/Fun also take local constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 17:03:48 -07:00
Leonardo de Moura	df9c935f0a	fix(kernel/inductive): remove unused argument, bug in is_rec_argument (free variable occurrence) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 17:02:20 -07:00
Leonardo de Moura	3e3d3c8380	feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 15:44:15 -07:00
Leonardo de Moura	a7aacaa782	feat(library/kernel_bindings): improve list_level support in the Lua interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 15:18:48 -07:00
Leonardo de Moura	a1086e440d	feat(kernel/inductive): use non-dependent elimination for Bool/Prop only if it is proof irrelevant Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 13:33:29 -07:00
Leonardo de Moura	eb92f3722f	fix(kernel/inductive): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 13:27:05 -07:00
Leonardo de Moura	f3ed20a229	feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 12:52:25 -07:00
Leonardo de Moura	edc8af7bb3	refactor(kernel): reduce code duplication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 11:11:19 -07:00
Leonardo de Moura	0e582675d9	feat(kernel/inductive): store computational rules in an environment extension Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 10:45:52 -07:00
Leonardo de Moura	90d83fa2ad	fix(kernel/environment): bug in get_extension Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 10:41:22 -07:00
Leonardo de Moura	1a9122f158	doc(kernel/inductive): improve module documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 10:04:28 -07:00
Leonardo de Moura	2aacb769dd	feat(kernel/inductive): generate computational rules RHS for inductive datatypes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 09:08:19 -07:00
Leonardo de Moura	eb409a9ce3	feat(kernel/abstract): add more Fun functions for simplifying the creation lambda-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 09:01:20 -07:00
Leonardo de Moura	5566186c34	feat(util/list_fn): add get_ith function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 09:00:09 -07:00
Leonardo de Moura	2daad71d47	fix(kernel/type_checker): memory access violation, closures (for printing error messages) had a uninteded reference to the type_checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 08:59:32 -07:00
Leonardo de Moura	39e101d323	feat(kernel/formatter): improve simple printer support for Pi and lambda Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-19 08:16:32 -07:00
Leonardo de Moura	28b70b4e04	feat(kernel/inductive): use nondependent elimination when the datatype is in Bool/Prop Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-18 15:39:48 -07:00
Leonardo de Moura	45252e2229	feat(kernel/inductive): add eliminator/recursor for inductive datatype declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-18 14:17:57 -07:00
Leonardo de Moura	f826e98196	feat(kernel/formatter): avoid hierarchical names when printing local constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-18 13:50:29 -07:00
Leonardo de Moura	405b24861c	feat(util/name): add methods append_after and append_before Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-18 13:49:24 -07:00
Leonardo de Moura	7bf0011905	feat(kernel/expr): add additional template for mk_app Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-18 13:15:58 -07:00
Leonardo de Moura	08aa4afb3e	feat(kernel/abstract): add more Pi functions for simplifying the creation Pi-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-18 13:15:00 -07:00
Leonardo de Moura	950d69b977	test(lua): add tests for exercising datatype validation code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 20:10:45 -07:00
Leonardo de Moura	ff3a7bd734	fix(kernel/type_checker): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 19:21:09 -07:00
Leonardo de Moura	8fcb84c8f2	feat(kernel/inductive): finish inductive datatype declaration validation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 19:19:32 -07:00
Leonardo de Moura	5c7d3c79c4	feat(kernel/expr): improve get_app_args interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 19:19:10 -07:00
Leonardo de Moura	28e8299f6d	feat(kernel/type_checker): add swap method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 19:18:46 -07:00
Leonardo de Moura	4325b126d4	feat(util/list): add map2 for list<T1> -> list<T2>, where T1 and T2 may be different, we still keep map because compiler can automatically infer all template arguments, this is not the case for map2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 19:18:18 -07:00
Leonardo de Moura	f818c1a63e	feat(kernel/inductive): add more inductive datatype validation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 14:47:06 -07:00
Leonardo de Moura	d03e35aaac	feat(kernel/inductive): add datatype and introduction rules declarations to environment, and fix tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 13:59:06 -07:00
Leonardo de Moura	f7bc5ac514	fix(library/kernel_bindings): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 13:44:51 -07:00
Leonardo de Moura	d0e7c88ea8	feat(library/kernel_bindings): improve universe level Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 13:40:35 -07:00
Leonardo de Moura	18a17cd48b	feat(kernel/level): add is_geq predicate, we need it for implementing the inductive datatype validation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 13:39:54 -07:00
Leonardo de Moura	4348d5e63f	refactor(kernel): remove unnecessary module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 12:35:41 -07:00
Leonardo de Moura	a85a6b685b	feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 12:30:03 -07:00
Leonardo de Moura	5ce134e24e	chore(kernel): binder => binding where appropriate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 11:37:27 -07:00
Leonardo de Moura	33ae79cd9e	refactor(kernel): move shallow copy function to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 11:20:24 -07:00
Leonardo de Moura	d625c9a26c	refactor(kernel): move max_sharing to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 11:15:08 -07:00
Leonardo de Moura	aafdd98acb	refactor(kernel): remove telescope type, and procedures Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 10:51:40 -07:00
Leonardo de Moura	36b070cb5b	refactor(kernel/inductive): simplify inductive datatype API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 09:24:34 -07:00
Leonardo de Moura	4ec89e8561	feat(library/kernel_bindings): add sugar for level expressions in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 08:10:36 -07:00
Leonardo de Moura	5fc0f06a8d	feat(library/kernel_bindings): add Lua API for declaring datatypes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 18:08:50 -07:00
Leonardo de Moura	ace5dee63d	feat(kernel/inductive): add getters for inductive decls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 17:47:37 -07:00
Leonardo de Moura	6dedb480ec	fix(kernel/abstract): bug in abstract for telescopes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 17:47:04 -07:00
Leonardo de Moura	e6c52d17a6	fix(kernel/expr): memory leak introduced today Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 16:21:31 -07:00
Leonardo de Moura	7d76278506	fix(kernel/abstract): compilation warnining Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 15:39:19 -07:00
Leonardo de Moura	a0abbf7662	feat(kernel/formatter): make simple_formatter display Type instead of Bool if impredicativity is disabled Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 15:31:19 -07:00
Leonardo de Moura	69e72c278d	feat(kernel): add proof irrelevance for classes We can use this feature to implement proof irrelevance for Identity types. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 15:30:32 -07:00
Leonardo de Moura	193aa4a83f	feat(library/kernel_bindings): improve Pi and Fun Lua APIs, and allow users to provide binder information Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 14:09:00 -07:00
Leonardo de Moura	862c5e354d	feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 13:08:09 -07:00
Leonardo de Moura	28329a55b0	feat(util/name): use '.' instead of '::' as hierarchical name separator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 12:35:43 -07:00
Leonardo de Moura	91a1b62b9e	feat(kernel): add telescope abstract procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 11:56:44 -07:00
Leonardo de Moura	9a689ab0c3	feat(kernel): add telescope instantiate procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 11:56:20 -07:00
Leonardo de Moura	40b3129e7b	refactor(kernel): improve names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 11:28:05 -07:00
Leonardo de Moura	d6d72ba80e	refactor(kernel): add binder structure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 10:51:54 -07:00
Leonardo de Moura	eb0abf557d	feat(kernel/inductive): add inductive datatype kernel extension module interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-16 09:53:51 -07:00
Leonardo de Moura	c0d8a3195c	fix(library/kernel_serializer): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 18:00:09 -07:00
Leonardo de Moura	660b9299ad	refactor(kernel): (de)serialization procedures don't need to be in the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 17:23:36 -07:00
Leonardo de Moura	2e3ffea2ec	feat(library): add new coercion API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 16:50:12 -07:00
Leonardo de Moura	e79e0302d0	fix(frontends/lean): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 16:09:21 -07:00
Leonardo de Moura	391b2fe739	refactor(builtin): remove old library, we will build a new one for Lean 0.2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 15:56:28 -07:00
Leonardo de Moura	c6af56260e	refactor(frontends/lean): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 15:51:41 -07:00
Leonardo de Moura	16553e77fa	fix(kernel/type_checker): avoid assertion violation due to API misuse Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 14:17:34 -07:00
Leonardo de Moura	1be758e4ef	feat(library/resolve_macro.cpp): add macro to encode propositional resolution proofs compactly This is also a test for the macro_definition infrastructure that we have in the kernel. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:11 -07:00
Leonardo de Moura	e644419463	feat(library/bin_app): add simpler is_bin_app predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:11 -07:00
Leonardo de Moura	7c0cc3111a	fix(kernel/type_checker): we must use different caches for infer_type and check The new test tc4.lua exposes the problem being fixed. We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:11 -07:00
Leonardo de Moura	687639a599	fix[kernel/justification.cpp]: style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:11 -07:00
Leonardo de Moura	494874fbab	fix(kernel/type_checker): trust level test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	24d8092a73	feat(library): add goodies for binary functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	830537a58b	feat(kernel/justification): add function for creating simple justification objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	d58b8a8102	refactor(kernel): move delayed_justification to justification.h Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	84c1cf9600	feat(kernel/kernel_exception): add new auxiliary functions for throwing kernel exceptions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	3a19d9fee1	refactor(kernel): revise macro_definition API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	6d30141a31	fix(kernel/formatter): remove unnecessary parenthesis Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	6f8f074f20	feat(library/kernel_bindings): make mk_arrow nary in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	08ac9c1f05	feat(kernel): add is_def_eq predicate in the extension_context API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	a6dc6060e2	fix(kernel/formatter): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-15 13:53:10 -07:00
Leonardo de Moura	0edcea55de	fix(library/kernel_bindings): clang++ compilation error Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 17:48:04 -07:00
Leonardo de Moura	6e78256b87	feat(library/kernel_bindings): expose is_bi_equal predicate in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 17:24:49 -07:00
Leonardo de Moura	606e6226c2	fix(kernel/type_checker): the type checker cache was not taking into account binder information Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 17:14:57 -07:00
Leonardo de Moura	d5184a1751	feat(kernel/formatter): print binder_info in simple formater Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 16:51:49 -07:00
Leonardo de Moura	5d61d23bf6	refactor(kernel): move mk_tele_pi to expr.h, and rename it mk_pi Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 16:24:55 -07:00
Leonardo de Moura	9c5dfc387b	refactor(kernel/replace_visitor): remove context from replace_visitor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 15:53:09 -07:00
Leonardo de Moura	2e1a0bd50c	feat(kernel/expr): add is_contextual binder info Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 14:54:27 -07:00
Leonardo de Moura	ab1a89e24c	refactor(library): remove dead files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 14:44:52 -07:00
Leonardo de Moura	893e4d4ae2	fix(kernel/expr): bug in m_free_var_range let-expr field Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 14:28:47 -07:00
Leonardo de Moura	956b775c48	feat(library/kernel_bindings): add let field accessors in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 14:17:30 -07:00
Leonardo de Moura	2bb537f3fb	feat(library/kernel_bindings): add sugar for creating Let expressions from Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 12:28:10 -07:00
Leonardo de Moura	cf55a1bcc2	fix(kernel/type_checker): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 10:35:42 -07:00
Leonardo de Moura	277e0e6d49	feat(kernel/formatter): prefix metavars with '?' and local vars with '!' in the simple formatter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 10:16:54 -07:00
Leonardo de Moura	f903626b78	feat(library/kernel_bindings): allow a list of level params/globals to be provided to declarations (instead of a list of names) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 09:45:48 -07:00
Leonardo de Moura	a8124b41d0	feat(util/name): expose is_list_name function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-14 09:44:58 -07:00
Leonardo de Moura	01eda46b69	feat(util/trie): add for_each and display methods Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-13 18:23:27 -07:00
Leonardo de Moura	bfa6193bfe	feat(util/trie): add merge method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-13 17:59:20 -07:00
Leonardo de Moura	479685cb97	feat(util): add basic trie datastructure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-13 17:40:33 -07:00
Leonardo de Moura	9ed700a5a6	feat(kernel/environment): add forget method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-13 08:40:46 -07:00
Leonardo de Moura	7b15e558a2	refactor(kernel/converter): implement eta in whnf instead of is_def_eq. Without cumulativity, we do not have problems with Eta at whnf anymore. When we had cumulativity, we could not not simply reduce (fun x : A, f x) ==> f This step is correct only if domain(f) was definitionally equal to f. Here is a problematic example for systems with cumulativity Given, f : Type.{2} -> Bool (fun x : Type.{1}, f x) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 17:49:53 -07:00
Leonardo de Moura	c883c638d6	feat(library/kernel_bindings): expose expression tags in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 16:50:43 -07:00
Leonardo de Moura	3bc83fae56	refactor(kernel/type_checker): remove trace capability, we get it for free with tags Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 16:38:53 -07:00
Leonardo de Moura	2593f65ce1	feat(kernel): add tag to kernel expressions Frontends can used tags to associate expressions with line number information. The update_* procedures automatically propagate tags. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 16:33:25 -07:00
Leonardo de Moura	3196cd19dc	chore(util/thread): add atomic_uint type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 16:14:31 -07:00
Leonardo de Moura	2e753e2cc0	fix(kernel/error_msgs): application type mismatch error message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 14:49:42 -07:00
Leonardo de Moura	b18263a014	feat(kernel/formatter): adjust simple formatter to the new convention for displaying universe levels Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 14:42:01 -07:00
Leonardo de Moura	d4922daedf	fix(kernel/level): add missing LEAN_THREAD_LOCAL directive Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 14:39:37 -07:00
Leonardo de Moura	a8a6bb1b7f	fix(kernel/level): bug in get_undef_global Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 14:34:24 -07:00
Leonardo de Moura	89d6a1e691	fix(kernel/type_checker): check for undefined global/local levels Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 14:23:04 -07:00
Leonardo de Moura	b6d6df161f	fix(kernel/level): bug in get_undef_param Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 14:22:23 -07:00
Leonardo de Moura	ad2b1d0d91	chore(util/lua_list): improve error message in table_to_list aux function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 12:58:10 -07:00
Leonardo de Moura	1244a951f2	fix(kernel/type_checker): add missing test: number of universe level parameters Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 12:57:27 -07:00
Leonardo de Moura	6f03064c46	fix(library/kernel_bindings): bug in mk_definition Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 12:56:50 -07:00
Leonardo de Moura	0eaf1bb2cf	fix(util/lua_named_param): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-12 12:21:48 -07:00
Leonardo de Moura	ff9004dae2	refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-11 18:05:02 -07:00
Leonardo de Moura	7176181b42	refactor(kernel/converter): cleanup and remove universe cumulativity support Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 20:43:11 -07:00
Leonardo de Moura	e942aecca6	refactor(kernel/type_checker): remove method is_conv Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 20:29:35 -07:00
Leonardo de Moura	9d96f24766	refactor(kernel): remove convertability constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 20:25:27 -07:00
Leonardo de Moura	d4400d6135	refactor(library/kernel_bindings): remove level_cnstrs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 20:16:51 -07:00
Leonardo de Moura	aaea298839	refactor(library/kernel_bindings): remove level pair and list of level pairs from Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 20:13:10 -07:00
Leonardo de Moura	7b6d555433	refactor(kernel): remove level constraints from definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 20:11:50 -07:00
Leonardo de Moura	23ed003389	refactor(kernel): remove diff_cnstrs module We don't need them anymore. We will drop universe cumulativity from the kernel. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 19:58:25 -07:00
Leonardo de Moura	a650a4f9b5	fix(library/kernel_bindings): bug in mk_app, add expr_lt tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 19:54:52 -07:00
Leonardo de Moura	6493ff5388	fix(kernel/formatter): print level parameters Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-09 19:50:04 -07:00
Leonardo de Moura	813eba6b3a	chore(build): add Lua thread tests to test suite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 18:53:36 -07:00
Leonardo de Moura	9676f48470	feat(library/kernel_bindings): add list of certified_definitions in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 18:51:34 -07:00
Leonardo de Moura	bc1a91496a	feat(util/lua_list): allow Lua list objects to be moved between states Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 18:49:27 -07:00
Leonardo de Moura	fca65a9d69	fix(kernel/environment): is_descendant optimization Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 18:48:25 -07:00
Leonardo de Moura	c843243f64	feat(library/kernel_bindings): add add_decl and type_check functions to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 18:08:32 -07:00
Leonardo de Moura	5a7f181efc	feat(util/name_set): improve name_set Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 17:17:00 -07:00
Leonardo de Moura	95262fb68d	feat(library/kernel_bindings): add remaining type_checker constructors in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 17:13:06 -07:00
Leonardo de Moura	3aa1afdf51	refactor(util): file name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 14:15:28 -07:00
Leonardo de Moura	1e4c5f1761	feat(util/lua_named_param): add new functions for handling named parameters in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 14:12:15 -07:00
Leonardo de Moura	bf57f951ea	refactor(util): move Lua named parameter support to a different file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-08 13:20:37 -07:00
Leonardo de Moura	f3c7bc948a	feat(library/kernel_bindings): type_checker Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 19:04:15 -07:00
Leonardo de Moura	1a8d75c4f0	feat(util): name_set Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 18:32:53 -07:00
Leonardo de Moura	7fe61bc69c	feat(util): name_generator Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 17:28:11 -07:00
Leonardo de Moura	62db010ba3	feat(library/kernel_bindings): add optional arguments to empty_environment Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 17:06:27 -07:00
Leonardo de Moura	4c5f88e63b	feat(library/kernel_bindings): global level constructor/accessor/recognizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 16:22:45 -07:00
Leonardo de Moura	db39458c30	fix(kernel/level): predicate is_param_core Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 16:22:08 -07:00
Leonardo de Moura	8ae0e46e9d	feat(library/kernel_bindings): add new global level methods to environment Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 16:17:04 -07:00
Leonardo de Moura	9c760132e2	feat(kernel): add global levels to environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 16:07:31 -07:00
Leonardo de Moura	208384b5b6	fix(util/rb_tree): missing const Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 14:07:15 -07:00
Leonardo de Moura	2424cf7ece	fix(kernel/expr): old comment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-07 13:07:17 -07:00
Leonardo de Moura	503d8dfa9e	feat(kernel): add global universe level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-06 16:13:29 -07:00
Leonardo de Moura	8095783c36	refactor(library/kernel_bindings): use new functions for simulating python-like named arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-05 14:42:16 -07:00
Leonardo de Moura	f568ed97b8	feat(util/lua): add functions for simulating python-like named arguments using Lua tables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-05 14:41:33 -07:00
Leonardo de Moura	850ec69538	feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-05 14:09:17 -07:00
Leonardo de Moura	10d8840cac	feat(library/kernel_bindings): add environment Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 17:53:32 -07:00
Leonardo de Moura	4f3fad5d65	feat(library/kernel_bindings): add certified_definition Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 17:46:59 -07:00
Leonardo de Moura	8f5491447a	feat(library/kernel_bindings): add environment_id Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 17:42:27 -07:00
Leonardo de Moura	fc2d5f1595	feat(library/kernel_bindings): add definition Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 17:00:59 -07:00
Leonardo de Moura	b928f313d3	feat(util): add macro for exposing the type std::pair<T1, T2> in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 16:30:17 -07:00
Leonardo de Moura	b83410f042	fix(library/kernel_bindings): g++ compilation error Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 14:34:56 -07:00
Leonardo de Moura	dc627c9965	test(lua): add constraint API tests, and fix minor bugs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 13:37:46 -07:00
Leonardo de Moura	91069c5f7f	feat(util/list_lua): add length method to list Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 13:37:15 -07:00
Leonardo de Moura	107f139764	fix(util/list_lua): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 13:33:49 -07:00
Leonardo de Moura	6ef161824d	feat(library/kernel_bindings): constraint Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 13:17:00 -07:00
Leonardo de Moura	802edd77d1	feat(kernel/justification): add is_eqp predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 12:15:29 -07:00
Leonardo de Moura	e4f69bd780	fix(kernel/justification): bug in depends_on Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 12:15:01 -07:00
Leonardo de Moura	94ca82ec85	fix(library/kernel_bindings): incorrect use of pushinteger, and improve justification Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 12:03:43 -07:00
Leonardo de Moura	50089dc64e	feat(kernel/error_msgs): expose pp_indent_expr Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-02 12:03:12 -07:00
Soonho Kong	468abb72b8	tests(util/rb_tree): wrap tst6 with #if !defined	2014-05-02 01:39:13 -04:00
Leonardo de Moura	a5229e5283	chore(util/lua): name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 18:40:18 -07:00
Leonardo de Moura	7cd892464f	feat(library/definition): macro definition and application Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 18:29:34 -07:00
Leonardo de Moura	65486b2dec	refactor(kernel/expr): add macro_definition smart pointer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 18:05:46 -07:00
Leonardo de Moura	9f5122b4c7	feat(library/kernel_bindings): justification Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 16:04:30 -07:00
Leonardo de Moura	340c0e0945	feat(library/kernel_bindings): substitution Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 15:30:30 -07:00
Leonardo de Moura	0bc101ac28	fix(kernel/metavar): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 15:28:34 -07:00
Leonardo de Moura	739f98b642	fix(util/script_state): deadlock Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 14:10:57 -07:00
Leonardo de Moura	ddd980aa63	fix(kernel/level): warning messages when compiling in release mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 13:06:00 -07:00
Leonardo de Moura	120c24319e	fix(tests/kernel/metavar): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 12:58:09 -07:00
Leonardo de Moura	027614cebb	fix(kernel/metavar): wierd memory leak that only happens when compiling with clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 12:55:55 -07:00
Leonardo de Moura	9452d164ec	feat(util/script_state): use recursive_mutex instead of mutex Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 12:27:12 -07:00
Leonardo de Moura	686c307976	feat(library/kernel_bindings): expr Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 12:25:49 -07:00
Leonardo de Moura	305815cb56	feat(library/kernel_bindings): expose expr_binder_info in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 11:23:37 -07:00
Leonardo de Moura	6fb7039746	refactor(kernel): use structural hashing in type_checker and converter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 10:41:53 -07:00
Leonardo de Moura	a5ae4b6570	feat(kernel): add binder annotations (implicit, cast) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 10:35:02 -07:00
Leonardo de Moura	2b97474958	test(util/rb_tree): reduce test time for rb_tree Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-01 10:08:18 -07:00
Leonardo de Moura	b0e0e82350	refactor(kernel): separate type_checker and converter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-30 18:42:01 -07:00
Leonardo de Moura	884b3f9b53	refactor(library/kernel_bindings): part of expr Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-30 16:37:26 -07:00
Leonardo de Moura	dbf327bad9	feat(util): expose list<name> in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-30 16:32:10 -07:00
Leonardo de Moura	03a32dcc77	feat(util): add macro for exposing the type list<T> in Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-30 16:31:44 -07:00
Leonardo de Moura	aba5b65319	feat(util/lua): add macro pushnil Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-30 10:29:08 -07:00
Leonardo de Moura	3e222e2f22	refactor(kernel/formatter): add environment as an extra argument to the formatter Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-30 10:28:07 -07:00
Leonardo de Moura	fd034521dc	feat(library/kernel_bindings): cleanup level Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 17:05:25 -07:00
Leonardo de Moura	93a61748e9	fix(kernel/level): bug in optional<level>() constructor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 17:00:57 -07:00
Leonardo de Moura	cd30bb49c1	chore(library/arith): remove unnecessary library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 16:14:15 -07:00
Leonardo de Moura	984048f40d	feat(library/kernel_bindings): new level Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 15:08:58 -07:00
Leonardo de Moura	097f562016	refactor(*): add pushinteger and pushnumeral inline functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 14:47:08 -07:00
Leonardo de Moura	412a3797f4	refactor(*): add pushboolean inline function, and replace lua_pushboolean with it Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 14:37:16 -07:00
Leonardo de Moura	f7e705badb	refactor(library/kernel_bindings): reactive some of the kernel Lua bindings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 11:52:09 -07:00
Leonardo de Moura	a6116e3156	test(lua): reactivate some of the Lua unit tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 10:36:57 -07:00
Leonardo de Moura	49e626a0e0	refactor(kernel/metavar): switch to functional substitution datastructure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-29 10:22:36 -07:00
Leonardo de Moura	af927ecb7a	refactor(frontends/lua): reactivate some of the Lua extensions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 17:57:39 -07:00
Leonardo de Moura	5fdd2fe3a9	refactor(util/script_state): replace splay_map with rb_map in the Lua environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 17:53:34 -07:00
Leonardo de Moura	2a59beee0a	feat(shell): reactivate lean shell, only Lua frontend is working Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 17:49:23 -07:00
Leonardo de Moura	cdae3ee780	fix(kernel/type_checker): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 14:17:34 -07:00
Leonardo de Moura	1681dc2389	test(kernel): add new environment tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 14:04:05 -07:00
Leonardo de Moura	b70bac0e8d	feat(kernel/type_checker): add backtracking trick to minimize the number of delta-reduction steps Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 14:03:46 -07:00
Leonardo de Moura	e62254fbb3	fix(kernel/expr): relax macro_definition interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 14:02:48 -07:00
Leonardo de Moura	1b9e2efb0c	fix(kernel/environment): relax normalizer_extesion interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 14:01:44 -07:00
Leonardo de Moura	f320277248	feat(kernel/definition): add mk_definition procedure that automatically computes the weight Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 12:48:21 -07:00
Leonardo de Moura	6c3a796119	fix(kernel/type_checker): bug in whnf method, and missing call to max_sharing in is_conv and is_def_eq methods Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 12:09:23 -07:00
Leonardo de Moura	4e893d3902	fix(kernel/constraint): printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 12:02:59 -07:00
Leonardo de Moura	54936c201a	fix(kernel/kernel_exception): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 11:31:39 -07:00
Leonardo de Moura	6dfeff92f8	fix(kernel/constraint): add dealloc method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 11:13:51 -07:00
Leonardo de Moura	e3b79730ba	fix(kernel/level): initialization error Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 11:03:23 -07:00
Leonardo de Moura	2ddadfc920	fix(kernel/environment): compilation errors Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 10:58:14 -07:00
Leonardo de Moura	9f57ec059a	fix(kernel/constraint): missing inline directive Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 10:53:53 -07:00
Leonardo de Moura	272463bd66	feat(kernel/type_checker): add check function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-28 10:47:50 -07:00
Leonardo de Moura	e769c26800	refactor(kernel): move files that don't need to be in the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 18:30:40 -07:00
Leonardo de Moura	b2518f873d	feat(kernel/type_checker): handle ensure_pi when whnf is a meta application Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 18:17:32 -07:00
Leonardo de Moura	6b05146eca	fix(kernel/type_checker): preserve bound variable name when inferring type of a lambda expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 17:29:47 -07:00
Leonardo de Moura	63b6564b78	refactor(kernel): define extension_context API for normalizer_extesions and macro_definitions A particular macro definition may use the extra information to retrieve information necessary to expand/type a given macro application. Example: it may need to invoke whnf. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 15:43:17 -07:00
Leonardo de Moura	4842ae4fc7	refactor(kernel): store macro arguments in the macro_expr Before this commit, we "stored" macro arguments using applications. This representation had some issues. Suppose we use [m a] to denote a macro application. In the old representation, ([m a] b) and [m a b] would have the same representation. Another problem is that some procedures (e.g., type inference) would not have a clean implementation. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 15:02:56 -07:00
Leonardo de Moura	9d5ed2bae1	chore(kernel/type_checker): fix style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 12:04:14 -07:00
Leonardo de Moura	a39a5b4195	refactor(kernel): remove normalizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 12:02:33 -07:00
Leonardo de Moura	a55c3c617d	feat(kernel/type_checker): add infer_type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 11:58:29 -07:00
Leonardo de Moura	3e122ed355	feat(kernel/error_msgs): add error message for unsatisfied level constraints, remove messages for dependent pairs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-25 10:47:05 -07:00
Leonardo de Moura	508bccb0c5	fix(kernel/max_sharing): add example exposing bug in max_sharing_fn, and fix it Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-24 15:55:48 -07:00
Leonardo de Moura	1c8e78e3ae	fix(kernel/justification): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-24 15:08:10 -07:00
Leonardo de Moura	4be4f21de6	fix(kernel/type_checker): bug in quick_is_conv, it was not converting free variables to local constants. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-24 12:46:31 -07:00
Leonardo de Moura	7eb9496643	feat(util): add missing lbool.* files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-24 12:27:19 -07:00
Leonardo de Moura	0d7902f9eb	feat(kernel/type_checker): finish is_convertible predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-23 20:16:14 -07:00
Leonardo de Moura	e78de448aa	feat(kernel/type_checker): add is_convertible predicate (and support for proof irrelevance and eta-reduction) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-23 19:21:26 -07:00
Leonardo de Moura	cdbef0bf15	fix(kernel/type_checker): is_opaque predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-23 10:51:39 -07:00
Leonardo de Moura	a3554c85fe	fix(kernel/definition): clang compilation warning, and add module_idx typedef Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-23 10:50:55 -07:00
Leonardo de Moura	ed37bf650d	chore(kernel/environment): fix style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 18:34:55 -07:00
Leonardo de Moura	04a61bdffe	feat(kernel/type_checker): remove dead code, add basic whnf procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 18:32:50 -07:00
Leonardo de Moura	188da7e4c6	feat(kernel/max_sharing): add method already_processed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 18:30:07 -07:00
Leonardo de Moura	f99444b130	chore(tests): move max_sharing unit tests to tests/kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 16:01:30 -07:00
Leonardo de Moura	9fda7e2529	fix(kernel): incorrect optimization in max_sharing_fn class The resultant expression may failed to be fully shared. Add an example that demonstrates the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 15:38:22 -07:00
Leonardo de Moura	086dd6b1a1	chore(kernel/environment): fix style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 15:36:52 -07:00
Leonardo de Moura	3b78af0db5	chore(tests/library): enable old tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 12:05:49 -07:00
Leonardo de Moura	ad43d9177b	refactor(util/name_set): implement name_sets using red black trees instead of hashtables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-22 11:09:13 -07:00
Leonardo de Moura	cc1cfba8ad	refactor(kernel/type_checker): new API for type checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-21 16:12:47 -07:00
Leonardo de Moura	6417c79569	feat(kernel/environment): add is_descendant method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-21 14:28:50 -07:00
Leonardo de Moura	bfeb51ce58	feat(kernel/environment): add trust level field Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-21 13:39:47 -07:00
Leonardo de Moura	ee58a83e25	chore(kernel): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-18 14:25:09 -07:00
Leonardo de Moura	d0dc16355b	chore(kernel): remove unnecessary file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-18 14:23:32 -07:00
Leonardo de Moura	582352d647	refactor(kernel/environment): simplified (functional) environment object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-18 14:21:49 -07:00
Leonardo de Moura	234abb1238	feat(kernel/definition): default constructor for definitions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-18 13:10:05 -07:00
Leonardo de Moura	984ac03ac7	refactor(kernel): replace kernel object with definition, disable affected files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 16:10:47 -07:00
Leonardo de Moura	cb479a75ae	fix(kernel/expr): make sure we cannot create a free variable with index uint_max, reason: get_free_var_range would return an incorrect value Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 13:25:21 -07:00
Leonardo de Moura	3712da0b54	refactor(kernel/instantiate): use get_free_var_range to improve instantiate, remove instantiate_with_closed, fix index overflow bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 13:12:49 -07:00
Leonardo de Moura	1fd5e9682d	refactor(kernel/free_vars): use get_free_var_range to improve lift_free_vars and lower_free_vars performance Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 12:41:06 -07:00
Leonardo de Moura	4ae958af56	refactor(kernel/free_vars): use get_free_var_range to improve has_free_var_in_range performance Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 12:18:19 -07:00
Leonardo de Moura	dc864bf7b9	feat(kernel): store free variable range in composite expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 11:31:48 -07:00
Leonardo de Moura	1fd447b451	chore(util): fix style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 10:54:10 -07:00
Leonardo de Moura	bc8379256a	refactor(kernel): remove pairs from kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 10:52:07 -07:00
Leonardo de Moura	9a3959eed1	feat(util): add method get_rc (mainly for debugging purposes) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-04-17 10:36:54 -07:00
Leonardo de Moura	c78e6787aa	test(util/rb_tree): multi-thread test for rb trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-20 10:20:28 -07:00
Leonardo de Moura	fb2ec8fb12	fix(kernel): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	9b161b825f	refactor(kernel): instantiate_params Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	3651b4ecd0	refactor(kernel): replace_fn functional object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	3939b93c2d	refactor(kernel): substitution Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	25948ac534	refactor(kernel): cleanup interfaces Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	08087ea9c6	refactor(kernel): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	eb487e44c1	refactor(kernel): use names instead of unsigned integers to encode level parameters Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	ddbb3a7944	refactor(kernel): add error msg formatters, remove unnecessary files, add new type_checker interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	916301bdfb	refactor(kernel): parametric kernel objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	54801bbd05	refactor(kernel): constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	aa4a7acccf	feat(kernel/level): is_trivial predicate for level constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	0b3599851d	refactor(library): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	d836e45452	refactor(library): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:57 -07:00
Leonardo de Moura	4b7fe064fe	refactor(kernel): finish formatter interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	28516a8dc2	refactor(library): remove unnecessary file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	e0ef6b2e9a	refactor(library): monotonic total order on terms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	8cd78e00f1	refactor(library): deep_copy procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	41782c0894	test(kernel/metavar): add metavar tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	bf13441bd7	fix(kernel): bugs in justification module, add missing metavar methods, add basic metavar tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	4c30ea9251	fix(kernel/justification): none is the unit of mk_composite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	3c6002e969	refactor(kernel): add mk_rev_app, update_rev_app, implement instantiate_metavars functions, modify instantiate (free vars) API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	42e253c962	fix(*): style and clang warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	968c0d799f	refactor(kernel): implement substitution methods Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	5f4b1cf47e	feat(kernel): define metavar substitution based on red-black trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	f855dbb7b0	feat(util): add maps based on red-black trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	54d5088c98	feat(util/rb_tree): add check_invariant for red black trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	1ab12eb105	refactor(util/splay_map): remove unnecessary operation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	528ea367ad	feat(util): add red-black trees Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	fdde12e6af	refactor(kernel): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	2a73389ed3	refactor(kernel): justification objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	50300126a5	refactor(util/name_generator): make sure there is no risk of overflow, name generators will be extensively used in version 0.2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	501435f6fc	feat(kernel): add has_local predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	e1f4f1f0d1	feat(util/thread): add atomic_uchar Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	997f32378c	refactor(kernel): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	6baa59376c	refactor(kernel): normalizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:56 -07:00
Leonardo de Moura	eb046c11fb	refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	410d5cc8ed	fix(kernel): remove unnecessary file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	16aa1ebbac	refactor(kernel): replace_visitor Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	101888e079	refactor(kernel): delete update_expr Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	b5f0f28009	refactor(kernel): environment, kernel object and exceptions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	3c8ccdd33d	test(util/exception): experiment with exceptions with nested std::function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	737fe6830f	test(tests/kernel): adjust expr tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	f986963a95	refactor(kernel): serializer and deserializer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	74f74d2f79	refactor(kernel): shallow copy procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	5da501d538	fix(kernel): style warnings Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	73c8bf4436	refactor(tests/kernel): move tests to new kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	565dbe1700	fix(kernel/instantiate): bug in new head_beta_reduce Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	d17990ed78	refactor(kernel): add formatter and simplify contexts Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	53ee205dc6	fix(kernel): memory corruption bugs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	72e1678ad9	refactor(kernel): cleanup instantiate and abstract procedures, implement update procedures Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	db31cc37a1	refactor(kernel/free_vars): cleanup free_vars procedures Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	533f44e224	refactor(kernel/expr): for_each_fn, replace_fn, and find_fn without templates Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:55 -07:00
Leonardo de Moura	69b9f2dd37	refactor(kernel/expr): for_each and find functional objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	23988f528c	refactor(kernel/expr): add expr constructors, and expression equality test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	9d3db8de1f	fix(kernel/diff_cnstrs): missing include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	02413d7c44	refactor(kernel/expr): adding suport for universe polymorphism, and simplify metavariable representation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	13cfd60622	fix(kernel/diff_cnstrs): copyright msg Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	76b1ddb967	feat(kernel): add difference constraint solver with backtracking support, and justification generation, this solver will be used to check the satisfiability of universe level constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	9f93b5d97e	feat(kernel/level): new universe level datastructure for universe level polymorphism Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	1b6b33b3f5	refactor(kernel): start version 0.2, new kernel with universe polymorphism and better/cleaner support for metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-18 10:27:54 -07:00
Leonardo de Moura	0c1674ab70	feat(builtin): quotient types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-12 00:20:46 -07:00
Leonardo de Moura	e0eacd1f9f	feat(builtin): simpler encoding of sum types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-03-03 18:30:45 -08:00
Leonardo de Moura	1d10953da4	fix(library/elaborator): add hack for experimenting with algebraic hierarchy Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-25 11:20:40 -08:00
Leonardo de Moura	aa8240985a	test(examples/lean): small version of algebraic hierarchy (proof of concept) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-24 20:51:19 -08:00
Leonardo de Moura	309e7ba880	fix(library/elaborator): temporary fix for bug reported by Jeremy Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-24 15:26:21 -08:00
Leonardo de Moura	16844fff73	feat(builtin): simulate binary encoding Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-20 20:44:05 -08:00
Leonardo de Moura	d79e9af210	fix(frontends/lean): help msg Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-18 09:31:30 -08:00
Leonardo de Moura	f781ad823c	doc(builtin): Diaconescu’s theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-18 09:12:09 -08:00
Leonardo de Moura	e9dada5e14	refactor(builtin/kernel): use standard definition for 'or' and 'and' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-17 12:05:34 -08:00
Leonardo de Moura	4692e04d70	feat(builtin/proof_irrel): prove proof irrelevance Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-16 18:06:10 -08:00
Leonardo de Moura	c526e5ec00	feat(builtin/kernel): prove false_elim without using case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-15 14:26:13 -08:00
Leonardo de Moura	1739b5c153	fix(kernel/type_checker): caching bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-12 10:43:01 -08:00
Leonardo de Moura	c740d9d799	fix(builtin/num): bug in the factorial definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-12 10:04:32 -08:00
Leonardo de Moura	45a0dbcc34	feat(builtin/num): define fact and exp Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-12 09:51:49 -08:00
Leonardo de Moura	368fcb5ff9	refactor(builtin/kernel): rename refute to by_contradiction Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-12 08:49:19 -08:00
Leonardo de Moura	69bccb6014	feat(builtin): define list, cons, nil and prove basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-11 21:32:05 -08:00
Leonardo de Moura	bfe64a7031	fix(library/elaborator): hack for fixing a bug due to pairs/projs, this is temporary fix until we build a new elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-11 21:30:26 -08:00
Leonardo de Moura	0878b44fc7	feat(frontends/lean): allow user to import several theories using a single import Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-11 17:15:12 -08:00
Leonardo de Moura	11a2b3016f	fix(builtin/num): remove hacks for making the elaborator happy Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 14:05:51 -08:00
Leonardo de Moura	b7b868de85	fix(library/elaborator): bug reported by Jeremy Avigad Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 14:01:22 -08:00
Leonardo de Moura	a2d2e36f04	refactor(frontends/lean): remove notation for creating tuples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 09:03:42 -08:00
Leonardo de Moura	4e08a3233e	fix(builtin): build dependency issue Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-10 08:33:07 -08:00
Leonardo de Moura	273f78d1cb	feat(builtin/num): prove strong induction and other theorems for num Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 21:09:50 -08:00
Leonardo de Moura	b119c11473	feat(builtin/tactic): add simp_no_assump tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 20:28:30 -08:00
Leonardo de Moura	4317f67bd2	fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 18:57:33 -08:00
Leonardo de Moura	57982135d9	fix(library/simplifier): bug using congr1 theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 16:24:29 -08:00
Leonardo de Moura	c45c1748d8	refactor(builtin/kernel): reorder congr1 arguments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 16:15:44 -08:00
Leonardo de Moura	fd6f8b1945	refactor(builtin/num): simplify proofs using 'by simp' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 15:03:45 -08:00
Leonardo de Moura	2d70e2f4f2	fix(library/tactic/goal): bug in the proof builder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 15:02:36 -08:00
Leonardo de Moura	4c76f6abb9	chore(builtin/num): remove leftover Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 11:39:26 -08:00
Leonardo de Moura	8df7c7b02d	feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker We should not rely on this feature. It can be quite expensive. We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as is_convertible(num, Nat) If is_convertible starts unfolding opaque definitions, we would keep expanding num. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 11:31:24 -08:00
Leonardo de Moura	4c4c8b3e0d	feat(builtin/num): prove basic theorems using simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 11:24:53 -08:00
Leonardo de Moura	633ed6bb69	fix(frontends/lean/parser): bug in add_rewrite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 09:46:56 -08:00
Leonardo de Moura	b24c085cb0	feat(frontends/lean): avoid warning message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 09:26:51 -08:00
Leonardo de Moura	d6167eae32	feat(builtin/num): define add and mul Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 22:28:15 -08:00
Leonardo de Moura	cc4148a98d	feat(builtin/num): primitive recursion theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 22:05:57 -08:00
Leonardo de Moura	f28c56b188	feat(builtin/num): add auxiliary definitions and theorems for proving the primitive recursion theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 19:36:17 -08:00
Leonardo de Moura	fa4b60963b	feat(builtin/num): define lt predicate, and prove basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 10:57:17 -08:00
Leonardo de Moura	1f3e0f7a38	chore(builtin/num): update object file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 09:16:52 -08:00
Leonardo de Moura	aeaa803f9a	feat(builtin): add num type (the base type that will be used to build nat, int, real) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 09:12:53 -08:00
Leonardo de Moura	1c43020fc9	fix(library/tactic/goal): bug creating main proof builder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 09:11:07 -08:00
Leonardo de Moura	24528ff685	fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 18:02:08 -08:00
Leonardo de Moura	1ec01f5757	refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 16:04:44 -08:00
Leonardo de Moura	ad7b13104f	feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 15:03:16 -08:00
Leonardo de Moura	6d7ec9d7b6	refactor(kernel): add heterogeneous equality back to expr The main motivation is that we will be able to move equalities between universes. For example, suppose we have A : (Type i) B : (Type i) H : @eq (Type j) A B where j > i We didn't find any trick for deducing (@eq (Type i) A B) from H. Before this commit, heterogeneous equality as a constant with type heq : {A B : (Type U)} : A -> B -> Bool So, from H, we would only be able to deduce (@heq (Type j) (Type j) A B) Not being able to move the equality back to a smaller universe is problematic in several cases. I list some instances in the end of the commit message. With this commit, Heterogeneous equality is a special kind of expression. It is not a constant anymore. From H, we can deduce H1 : A == B That is, we are essentially "erasing" the universes when we move to heterogeneous equality. Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is (to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B) So, it remains to explain why we need this feature. For example, suppose we want to state the Pi extensionality axiom. axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous equality as a constant. The conclusion (∀ x, B x) == (∀ x, B' x) is syntax sugar for (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x)) Even if A, A', B, B' live in a much smaller universe. As I described above, it doesn't seem to be a way to move this equality back to a smaller universe. So, if we wanted to keep the heterogeneous equality as a constant, it seems we would have to support axiom schemas. That is, hpiext would be parametrized by the universes where A, A', B and B'. Another possibility would be to have universe polymorphism like Agda. None of the solutions seem attractive. So, we decided to have heterogeneous equality as a special kind of expression. And use the trick above to move equalities back to the right universe. BTW, the parser is not creating the new heterogeneous equalities yet. Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous equality as a constant. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 10:28:10 -08:00
Leonardo de Moura	354d5607af	chore(builtin/sum): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 21:25:57 -08:00
Leonardo de Moura	d4b08fcf96	feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx \|- ?m[inst:i v] == T and ctx \|- (?m a1 ... an) == T are delayed by elaborator because the produce case-splits. On the other hand, the step that puts terms is head-normal form is eagerly applied. This is a bad idea for constraints like the two above. The elaborator will put T in head normal form before executing process_meta_app and process_meta_inst. This is just wasted work, and creates fully unfolded terms for solvers and provers. The new test demonstrates the problem. In this test, we mark several terms as non-opaque. Without this commit, the produced goal is a huge term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 21:08:00 -08:00
Leonardo de Moura	ff955f9830	chore(frontends/lean/parser): update comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	593f1f2ebd	fix(frontends/lean): allow user set constants defined in other namespaces as opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	363c4dc5c2	feat(library/elaborator): improve support for dependent pairs in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -08:00
Leonardo de Moura	4b4b5e3345	fix(frontends/lean): import explicit versions when using the command 'using' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:33:58 -08:00
Leonardo de Moura	ea06bb2885	feat(frontends/lean/pp): change how lift local entries are pretty printed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00
Leonardo de Moura	a51139e63b	feat(frontends/lean): position information in error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00
Leonardo de Moura	e85b1f1ac0	feat(library/elaborator): expose elaborator configuration options Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:26:38 -08:00
Leonardo de Moura	e4579b93e4	fix(library/elaborator): try first projection before imitation in the higher-order unifier Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 13:35:05 -08:00
Leonardo de Moura	ef321e730f	feat(builtin/tactic): add the 'skip' (bogus) tactic for ignoring a proof hole in a big proof Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 12:47:23 -08:00
Leonardo de Moura	581ae0c83b	chore(build): fix build dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 09:30:33 -08:00
Leonardo de Moura	db3bcdba55	refactor(builtin): move pair definition and theorems to pair.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 09:20:52 -08:00
Leonardo de Moura	daf7075ce4	refactor(builtin/sum): use new 'have' expression to formalize optional-types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 09:15:12 -08:00
Leonardo de Moura	5d698a60a7	refactor(builtin/sum): use new 'have' expression to formalize sum-types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 08:59:05 -08:00
Leonardo de Moura	1d23d93e60	feat(frontends/lean): new 'have' expression Add 'have' notation suggested by Jeremy Avigad. Add his example to the test suite. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 08:03:59 -08:00
Leonardo de Moura	ba9a8f9d98	feat(frontends/lean): add 'show' expression syntax sugar Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 07:50:22 -08:00
Leonardo de Moura	90f5a4f813	feat(builtin/sum): cleanup, and avoid unicode character that is not available in some platforms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 00:20:49 -08:00
Leonardo de Moura	c01f82aeb7	feat(builtin): add sum types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 23:04:44 -08:00
Leonardo de Moura	87da23649b	feat(builtin/optional): prove dichotomy and induction theorems for optional types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 19:49:50 -08:00
Leonardo de Moura	30570c843f	feat(builtin): add optional type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 17:33:06 -08:00
Leonardo de Moura	aec9c84d0d	fix(util/lua): deadlock Errors in the Lua library produce longjmps. The longjmp will not unwind the C++ stack. In the new test, the lock was not being released, and the system was deadlocking in the next call that tried to lock the environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 15:16:29 -08:00
Leonardo de Moura	f4ec874c6e	refactor(builtin): remove dead module heq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 14:42:28 -08:00
Leonardo de Moura	0283887ee9	refactor(builtin/kernel): move the heq axioms into kernel.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 14:17:34 -08:00
Leonardo de Moura	493007b7bc	fix(frontends/lean/pp): bug in tuple/pair pretty printing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 13:58:01 -08:00
Leonardo de Moura	f03c09c10b	feat(library/elaborator): add support for proj/pair/sigma in the the higher-order unification procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 13:53:30 -08:00
Leonardo de Moura	c9b72df34b	fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 11:36:26 -08:00
Leonardo de Moura	9dc86e3cf5	fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 10:06:29 -08:00
Leonardo de Moura	9a677331da	feat(builtin): simulate subtypes using sigma types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 01:46:50 -08:00
Leonardo de Moura	61d0c792ff	fix(frontends/lean/parser): bug in tuple/proj1/proj2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 22:46:29 -08:00
Leonardo de Moura	4fcc292332	feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 22:10:01 -08:00
Leonardo de Moura	cc96b50644	feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 20:53:11 -08:00
Leonardo de Moura	5c991f8fbf	feat(frontends/lean): parse and pretty print tuples/pairs This commit also fixes a bug in the type checker when processing dependent pairs. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 20:10:30 -08:00
Leonardo de Moura	5e5ab1429d	feat(frontends/lean): parse and pretty print sigma types This commit also fixes some bugs in the implementation of Sigma types. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 18:16:00 -08:00
Leonardo de Moura	8eec289ce1	feat(kernel): add dependent pairs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 16:52:49 -08:00
Leonardo de Moura	6be50f0133	refactor(builtin/heq): merge cast and heq modules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-02 15:01:48 -08:00
Leonardo de Moura	c56df132b8	refactor(kernel): remove semantic attachments from the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-02 14:48:27 -08:00
Leonardo de Moura	e3dc552c39	fix(library/simplifier): nontermination The example tests/lua/simp1.lua demonstrates the issue. The higher-order matcher matches closed terms that are definitionally equal. So, given a definition definition a := 1 it will match 'a' with '1' since they are definitionally equal. Then, if we have a theorem theorem a_eq_1 : a = 1 as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a" a --> 1 --> 1 --> 1 ... The first simplification is expected. The other ones are not. The problem is that "1" is definitionally equal to "a", and they match. The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side. To avoid this loop, we test if the new expression is not equal to the previous one. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-31 15:55:21 -08:00
Leonardo de Moura	1d85267d26	fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-31 15:38:22 -08:00
Leonardo de Moura	110ca84984	feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-31 13:49:24 -08:00
Leonardo de Moura	0ed35e2133	fix(build): kernel.lean depends on tactic.lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 23:15:44 -08:00
Leonardo de Moura	2aaded261e	fix(kernel/environment): imported predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 23:02:19 -08:00
Leonardo de Moura	bc2d504ccc	feat(builtin/kernel): add rewrite rules for if-then-else Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 22:38:35 -08:00
Leonardo de Moura	b444756d20	fix(library/simplifier): missing condition in implication simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 22:14:01 -08:00
Leonardo de Moura	4d533c6a25	feat(builtin/kernel): add nonempty_range theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 22:13:34 -08:00
Leonardo de Moura	ddaf948c72	feat(builtin/kernel): add nonempty_fun theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 19:38:51 -08:00
Leonardo de Moura	759aa61f70	refactor(builtin/kernel): define if-then-else using Hilbert's operator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 19:28:42 -08:00
Leonardo de Moura	b45ab9dc30	feat(library/elaborator): use equality constraints instead of convertability constraints on definitions Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 14:13:21 -08:00
Leonardo de Moura	8c1f6b9055	fix(kernel/typechecker): allow elaborator to infer (Type U+1) In the new test elab8.lean, the parameter B is in (Type U+1). Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 14:00:01 -08:00
Leonardo de Moura	41f5e2a067	feat(library/simplifier): statically check (conditional) equations (aka rewrite rules) to verify whether we can skip type checking when using them in the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 18:32:40 -08:00
Leonardo de Moura	01259b1e84	feat(kernel): make sure U is the maximal universe Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 16:31:00 -08:00
Leonardo de Moura	ea6bf224e5	feat(frontends/lean): make the parser accept (Type -> ...) Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 15:23:20 -08:00
Leonardo de Moura	4f3127d3d5	fix(library/simplifier): check if the given types are convertible to ceq expected types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 15:15:55 -08:00
Leonardo de Moura	a19f9d4846	feat(library/simplifier): discard conditional equations that are clearly non-terminating Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 13:56:45 -08:00
Leonardo de Moura	dd6aae378f	fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 13:29:20 -08:00
Leonardo de Moura	4dc3aa46c3	feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 12:02:12 -08:00
Leonardo de Moura	069e5edf6b	fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 12:01:01 -08:00
Leonardo de Moura	f0a2d3627e	refactor(frontends/lean): use ascii prefix for auxiliary let-declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 11:58:09 -08:00
Leonardo de Moura	92ba4e8b2d	feat(library/simplifier): add support for metavariables in conditional rewrite rules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 08:34:04 -08:00
Leonardo de Moura	f101554e93	fix(util/script_exception): make sure a script_nested_exception may have a nested script_nested_exception, use LEAN_THREAD_LOCAL macro instead of thread_local Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 08:07:52 -08:00
Leonardo de Moura	24452289dd	feat(library/simplifier): make sure the simplifier can handle meta-variables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 20:30:47 -08:00
Leonardo de Moura	ee4344076e	feat(library/simplifier): improve error message when simplifier is looping Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 19:36:31 -08:00
Leonardo de Moura	b6985bd713	feat(builtin/kernel): add another rewrite rule Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 15:56:26 -08:00
Leonardo de Moura	e2540b68db	fix(src/builtin/tactic): add default rule set if none is provided Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 15:56:01 -08:00
Leonardo de Moura	7f53cb9601	feat(frontends/lean/parser): add_rewrite take the 'using' command into account Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 01:15:28 -08:00
Leonardo de Moura	b31ef34787	feat(library/simplifier): preserve binder names when applying higher-order rewrite rules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 00:50:27 -08:00
Leonardo de Moura	6da1b447f0	fix(library/hop_match): do not match iff with = Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 00:21:05 -08:00
Leonardo de Moura	dbdbd211e3	fix(library/simplifier): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 23:29:53 -08:00
Leonardo de Moura	55fde28954	feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 17:47:03 -08:00
Leonardo de Moura	160dc71cb5	refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 17:38:06 -08:00
Leonardo de Moura	05b4d8411b	refactor(kernel/normalizer): normalizer only needs read access to metavariable environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 17:03:36 -08:00
Leonardo de Moura	3b152d1a9e	refactor(kernel): use ro_metavar_env instead of metavar_env in places where we only need to read the metavariable environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 16:44:43 -08:00
Leonardo de Moura	8bccfb947a	feat(library/simplifier): expose simplier and simplifier_monitor objects in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 15:02:05 -08:00
Leonardo de Moura	c088825ef0	feat(library/simplifier): add simplifier_monitor interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 11:46:28 -08:00
Leonardo de Moura	b26035fcf6	feat(kernel/type_checker): improve application type mismatch error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 09:45:17 -08:00
Leonardo de Moura	579b751e01	fix(library/simplifier): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 23:16:24 -08:00
Leonardo de Moura	ceff335bb8	doc(doc/lean/tutorial): update tutorial Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 22:58:44 -08:00
Leonardo de Moura	4d25cb7f47	feat(library/tactic): add simplify_tactic based on the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 18:53:18 -08:00
Leonardo de Moura	5e6c1d4904	refactor(builtin/heq): remove axiom hpiext since we don't use it anymore Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 13:11:17 -08:00
Leonardo de Moura	50df761d90	refactor(library/simplifier): remove the is_typem hack, it is not needed anymore now that we don't use hpiext anymore Now, we are again using the following invariant for simplifier_fn::result The type of in the equality of the result is definitionally equal to the type of the resultant expression. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 12:21:23 -08:00
Leonardo de Moura	29e448f034	fix(library/simplifier): remove support in the simplifier for (forall x : A, B x) when it is not a proposition, the problem is that hpiext axiom produces an equality in a too big universe For example, in the hpiext axiom, the resultant equality if for (Type M+1) axiom hpiext {A A' : TypeM} {B : A -> TypeM} {B' : A' -> TypeM} : A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x) even if the actual arguments A, A’, B, B’ "live" in a much smaller universe (e.g., Type). So, it would be great if we could move the resultant equality back to the right universe. I don't see how to do it right now. The other solution would require a major rewrite of the code base. We would have to support universe level arguments like Agda, and write the axiom hpiext as: axiom hpiext {l : level} {A A' : (Type l)} {B : A -> (Type l)} {B' : A' -> (Type l)} : A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x) This is the first instance I found where it is really handy to have this feature. I think this would be a super clean solution, but it would require a big rewrite in the code base. Another problem is that the actual semantics that Agda has for this kind of construction is not clear to me. For instance, sometimes Agda reports that the type of an expression is (Set omega). An easier to implement hack is to support "axiom templates". We create instances of hipext "on-demand" for different universe levels. This is essentially what Coq does, since the universe levels are implicit in Coq. This is not as clean as the Agda approach, but it is much easier to implement. A super dirty trick is to include some instances of hpiext for commonly used universes (e.g., Type and (Type 1)). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 12:10:34 -08:00
Leonardo de Moura	52ee9b35dd	feat(library/simplifier): add support for simplifying even when heq module is not available Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 11:29:36 -08:00
Leonardo de Moura	fafaa7e78e	fix(library/simplifier): remove hack for handling some constants that expect an argument of type TypeU, the new approach is general Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 10:10:57 -08:00
Leonardo de Moura	89bb5fbf19	chore(library/simplifier): fix style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 00:36:17 -08:00
Leonardo de Moura	844572c382	feat(library/simplifier): support for dependent simplification in Pi/forall expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 00:32:05 -08:00
Leonardo de Moura	e8bba1ebf3	fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f. For example, if we had variable f {A : Type} : A -> Bool Then, the definition of @f was definition @f (A : Type) (a : A) : Bool := f A a This definition is equivalent to fun A a, f A a which is not definitionally equal to f since definitionally equality in Lean ignores Eta conversion. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 20:34:28 -08:00
Leonardo de Moura	6bc1537e25	feat(frontends/lean/parser): allow the user to write (Type) without providing a level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 20:17:36 -08:00
Leonardo de Moura	9fb3ccb4c0	feat(library/simplifier): support for dependent simplification in lambda expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 16:54:42 -08:00
Leonardo de Moura	7015089734	fix(library/simplifier): move to locally nameless approach in the simplifier. Contextual simplification may add rewriting rules with free variables, and it is a mess to manage them when using de Bruijn indices Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 10:49:44 -08:00
Leonardo de Moura	df3129e80d	fix(library/hop_match): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 10:08:53 -08:00
Leonardo de Moura	7a4eb4b8ed	feat(library/simplifier): contextual simplification for A -> B Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 22:32:55 -08:00
Leonardo de Moura	c2381e43f1	fix(library/simplifier): bug in cast elimination Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 21:25:09 -08:00
Leonardo de Moura	2bb33c55fe	feat(builtin/kernel): add more theorems useful for simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 18:52:50 -08:00
Leonardo de Moura	8f455f5965	fix(frontends/lean): bug in scope construct Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:23:29 -08:00
Leonardo de Moura	7f3e2b3ef4	fix(frontends/lean/parser): bug in 'using' construct Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:09:46 -08:00
Leonardo de Moura	8e0888828d	fix(library/simplifier): missing check in mk_hcongr_th Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:09:46 -08:00
Leonardo de Moura	26bea77721	fix(library/simplifier): bug in heterogeneous equality support, and universe commutativity support in the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:09:46 -08:00
Leonardo de Moura	009217b499	feat(builtin/hep): replace hallext axiom with theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:09:20 -08:00
Leonardo de Moura	dbc100cc2e	feat(library/simplifier): cast elimination in the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-23 17:28:14 -08:00
Leonardo de Moura	180be5c4a2	feat(library/simplifier): improve contextual simplifications Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-23 13:11:58 -08:00
Leonardo de Moura	33193e1ab3	feat(library/simplifier): improve contextual simplifications Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-23 12:54:29 -08:00
Leonardo de Moura	d6692264e8	feat(library/simplifier): contextual simplifications Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-23 12:23:22 -08:00
Leonardo de Moura	1638a7bb02	fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 21:44:24 -08:00
Leonardo de Moura	17cce340f6	fix(library/elaborator): in optimization for metavariable free terms The optimization was incorrect if the term indirectly contained a metavariable. It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable. This commit also adds a new test that exposes the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 18:06:00 -08:00
Leonardo de Moura	8214c7add4	feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer Before this commit, the elaborator was solving constraints of the form ctx \|- (?m x) == (f x) as ?m <- (fun x : A, f x) where A is the domain of f. In our kernel, the terms f and (fun x, f x) are not definitionally equal. So, the solution above is not the only one. Another possible solution is ?m <- f Depending of the circumstances we want ?m <- (fun x : A, f x) OR ?m <- f. For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used: ?m <- (fun x : A, f x) When we are elaborating the axiom_of_choice theorem, we need to use the second one: ?m <- f Of course, we can always provide the parameters explicitly and bypass the elaborator. However, this goes against the idea that the elaborator can do mechanical steps for us. This commit addresses this issue by creating a case-split ?m <- (fun x : A, f x) OR ?m <- f Another solution is to implement eta-expanded normal forms in the Kernel. With this change, we were able to cleanup the following "hacks" in kernel.lean: @eps_ax A (nonempty_ex_intro H) P w Hw @axiom_of_choice A B P H where we had to explicitly provided the implicit arguments This commit also improves the imitation step for Pi-terms that are actually arrows. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 13:28:54 -08:00
Leonardo de Moura	6cb4d165c9	feat(builtin/kernel): dependent version of axiom of choice Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 11:04:27 -08:00
Leonardo de Moura	88b6778a1f	fix(emacs): syntax highlight Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 09:44:12 -08:00
Leonardo de Moura	66553268d0	feat(builtin/kernel): add skolem_th, we need it to justify skolemization preprocessing step Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 09:41:07 -08:00
Leonardo de Moura	d9b5ebc738	refactor(builtin/kernel): cleanup Hilbert operator definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 09:18:40 -08:00
Leonardo de Moura	bcf60db23b	fix(builtin/kernel): Hilbert operator only for non-empty types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 08:52:31 -08:00
Leonardo de Moura	94a3136904	feat(builtin/kernel): add Hilbert's operator, and derive axiom of choice using it Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 08:21:11 -08:00
Leonardo de Moura	425d31f513	chore(library/simplifier): fix style warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 21:45:55 -08:00
Leonardo de Moura	cca15f1390	feat(library/simplifier): congruence theorem compilation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 21:16:23 -08:00
Leonardo de Moura	029d74ec11	chore(kernel): remove comment, we decided to have Eta as a simplification rule Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:35:05 -08:00
Leonardo de Moura	95b6e61738	feat(kernel/max_sharing): check for imminent stack overflows and interruptions in the expression sharing maximizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:33:49 -08:00
Leonardo de Moura	2089b85532	refactor(kernel/instantiate): remove code duplication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:30:38 -08:00
Leonardo de Moura	7299b2d5d6	chore(kernel): remove dead file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:21:13 -08:00
Leonardo de Moura	fbaf6e887f	refactor(builtin/kernel): put the congruence theorems in a format that is easier for the simplifier to process Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:03:51 -08:00
Leonardo de Moura	ead54bbf57	feat(library/simplifier): enforce max_steps option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 12:12:17 -08:00
Leonardo de Moura	1ccfac5873	feat(library/simplifier): conditional rewriting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 21:15:46 -08:00
Leonardo de Moura	6bcd8e3ee5	fix(library/expr_lt): use expression depth instead of size to obtain a monotonic total order on terms It is not incorrect to use size, but it can easily overflow due to sharing. The following script demonstrates the problem: local f = Const("f") local a = Const("a") function mk_shared(d) if d == 0 then return a else local c = mk_shared(d-1) return f(c, c) end end print(mk_shared(33):size()) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 17:40:49 -08:00
Leonardo de Moura	cd19d4da01	feat(library/simplifier): memoize intermediate results Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 17:03:44 -08:00
Leonardo de Moura	97ead50a3e	feat(builtin/Nat): flip orientation of associativity axioms for + and * Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 15:38:00 -08:00
Leonardo de Moura	ad219d43d9	refactor(*): semantic attachment parsing and simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 14:44:45 -08:00
Leonardo de Moura	217e56ea03	feat(kernel/expr): make sure semantic attachments are smaller than other kinds of expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 14:10:44 -08:00
Leonardo de Moura	abfeacb8f0	fix(tests/library/expr_lt): adjust is_lt unit tests to reflect recent modifications Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:44:44 -08:00
Leonardo de Moura	56f5657ee7	fix(library/simplifier): ordered rewriting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:13:16 -08:00
Leonardo de Moura	5060bdbf14	fix(kernel/expr): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:12:49 -08:00
Leonardo de Moura	6a63ef3bc5	feat(library/expr_lt): make sure the total order on terms is monotonic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:07:18 -08:00
Leonardo de Moura	ac9f8f340d	feat(kernel/expr): add efficient get_size() function for expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 12:28:37 -08:00
Leonardo de Moura	913d893204	feat(library/simplifier): add support for 'permutation' rewrite rules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 08:29:31 -08:00
Leonardo de Moura	8e90d17a0b	fix(library/hop_match): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 23:28:12 -08:00
Leonardo de Moura	69d7ee316f	feat(library/simplifier): improve simplification by evaluation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 23:26:34 -08:00
Leonardo de Moura	08053c1172	feat(library/hop_match): make the higher order pattern matcher slightly stronger It now can handle (?m t) where t is not a locally bound variable, but ?m and all free variables in t are assigned. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 20:35:50 -08:00
Leonardo de Moura	90ffb9d5ec	fix(frontends/lean/pp): bug in pp_abstraction_core Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 19:47:40 -08:00
Leonardo de Moura	6db10c577b	feat(builtin/kernel): add proof irrelevance axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 12:20:09 -08:00
Leonardo de Moura	d322f63113	feat(frontends/lea): add commands for creating and managing rewrite rule sets Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 12:03:59 -08:00
Leonardo de Moura	bbf6e6a256	feat(builtin/kernel): create default rule set in the kernel, and adjust unit tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 11:24:20 -08:00
Leonardo de Moura	3bbadddc94	chore(library/simplifier): cleanup and add comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:54:09 -08:00
Leonardo de Moura	7492fd5a2c	feat(library/simplifier): add support for simplification by evaluation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:34:55 -08:00
Leonardo de Moura	475df3d94e	chore(builtin/kernel): add theorem for rewriter/simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:34:18 -08:00
Leonardo de Moura	e512241c8f	fix(emacs): missing keyword Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:32:45 -08:00
Leonardo de Moura	11719713ec	feat(library/hop_match): optionally unfold constants when performing higher order matching Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:32:06 -08:00
Leonardo de Moura	39c3b17eb7	feat(library/simplifier): add support for Eta-reduction in the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 00:40:35 -08:00
Leonardo de Moura	ed009f4c88	feat(kernel/simplifier): add support for Beta-reduction in the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 00:40:20 -08:00
Leonardo de Moura	7a3aab60c6	chore(builtin/kernel): remove \bowtie as notation for transitivity Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 21:11:12 -08:00
Leonardo de Moura	2753a0ffc0	fix(builtin/kernel): add ascii notation for transitivity Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 20:56:35 -08:00
Leonardo de Moura	32c5bc25e3	refactor(library/simplifier): cleanup rewrite_rule_set, and use it in the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 20:52:33 -08:00
Leonardo de Moura	466285c577	refactor(library/simplifier): rewriter_rule_set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 17:26:01 -08:00
Leonardo de Moura	feea96e84d	feat(library/simplifier): add rewrite_rule_set extension for managing rewrite rules in an environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 15:43:24 -08:00
Leonardo de Moura	eae79877ae	feat(library/simplifier): add rewrite_rule_set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 12:50:46 -08:00
Leonardo de Moura	27ab49ae9d	feat(library/simplifier): bottom-up simplifier skeleton Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 12:49:41 -08:00
Leonardo de Moura	40b7ed13c2	fix(tests/lean): adjust tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 19:27:32 -08:00
Leonardo de Moura	534838a36c	chore(build): update automatically generated files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 18:30:45 -08:00
Leonardo de Moura	d711ca4d1b	feat(builtin/heq): add heq C++/Lean interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 18:30:21 -08:00
Leonardo de Moura	20c8b91d07	feat(builtin/if_then_else): add more theorems for rewriting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 18:11:23 -08:00
Leonardo de Moura	2434024272	fix(library/rewriter): warning in release mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 15:46:49 -08:00
Leonardo de Moura	ba88a3b05a	chore(builtin/heq): remove unnecessary import Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 15:40:56 -08:00
Leonardo de Moura	70828af6db	refactor(builtin/heq): cleanup universes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 14:52:09 -08:00
Leonardo de Moura	fc4c6454a7	chore(tests/lean): adjust tests to reflect recent changes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 14:36:55 -08:00
Leonardo de Moura	0660cdbdb7	feat(builtin/cast): use heq in the cast library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 14:31:45 -08:00
Leonardo de Moura	52756c50fc	fix(builtin/heq): extensionality axioms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 12:56:36 -08:00
Leonardo de Moura	64795c6c42	feat(builtin): add heterogeneous equality theory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 12:32:49 -08:00
Leonardo de Moura	baed98d5be	chore(builtin/kernel): adjust emacs mode and fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 10:14:57 -08:00
Leonardo de Moura	5bee259a00	refactor(kernel): remove unnecessary universe Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 18:06:25 -08:00
Leonardo de Moura	a43020b31b	refactor(kernel): remove heterogeneous equality Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 17:39:12 -08:00
Leonardo de Moura	1da4294793	refactor(builtin): more theorems, fix iff notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 09:26:50 -08:00
Leonardo de Moura	398d83b6d5	chore(builtin/Nat): use iff Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 02:06:53 -08:00
Leonardo de Moura	4dc98bc73b	refactor(builtin/kernel): use iff instead of = for Booleans Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 02:05:09 -08:00
Leonardo de Moura	d063828ff9	feat(library/kernel_bindings): expose abst_name, abst_domain and abst_body in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 00:03:16 -08:00
Leonardo de Moura	8d73fb5699	fix(library/hop_match): Lua bindings gotcha See http://www.luafaq.org/gotchas.html#T6.4 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 23:51:26 -08:00
Leonardo de Moura	14c6218bdc	chore(kernel): file name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 20:06:29 -08:00
Leonardo de Moura	3238c7e2a0	feat(library/simplifier): add is_permutation_ceq predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 19:53:52 -08:00
Leonardo de Moura	7fb0aa4800	chore(kernel/expr): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:24:31 -08:00
Leonardo de Moura	438fa8251b	test(kernel/expr): check if the serializer works for metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:15:56 -08:00
Leonardo de Moura	5058e403b5	test(kernel/expr): check if the serializer works for applications with many argumets Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:09:46 -08:00
Leonardo de Moura	c096eec1d6	chore(kernel/expr): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:09:04 -08:00
Leonardo de Moura	8c2f78a756	feat(builtin): minimize use of heterogenous equality in the kernel, add simpler version of congruence theorems for non-dependent types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 16:34:23 -08:00
Leonardo de Moura	c73398a0b8	refactor(library/simplifier): relax rule for conditional equalities The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference. For example, we will be able to have the eta theorem as rewrite rule: theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f := funext (λ x : A, refl (f x)) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 16:06:00 -08:00
Leonardo de Moura	3daac17ea8	feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 15:30:16 -08:00
Leonardo de Moura	1176093afa	refactor(library/simplifier): simplifier should only use homogeneous equalities Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 14:58:32 -08:00
Leonardo de Moura	f177c8d1ec	fix(library/elaborator): missing condition The elaborator was failing in the following higher-order constraint ctx \|- (?M a) = (?M b) This constraint has solution, but the missing condition was making the elaborator to reduce this problem to ctx \|- a = b That does not have a solution. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 14:11:36 -08:00
Leonardo de Moura	c651d3ea2d	feat(library/simplifier): filter out propositions that cannot be used as conditional equations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 12:06:27 -08:00
Leonardo de Moura	94fa987814	fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool The method is_proposition was using an optimization that became incorrect after we identified Pi and forall. It was assuming that any Pi expression is not a proposition. This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 11:02:52 -08:00
Leonardo de Moura	3ab2d2a441	fix(frontends/lean/parser): memory leak due to g++ bug g++ implementation of std::initializer_list has bug. http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html This commit memory leaks triggered by this bug. It also adds minimal tests to expose three different instances of the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 10:15:04 -08:00
Leonardo de Moura	83efa644d1	fix(frontends/lean/parser): uninitialized var error reported by valgrind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 08:43:43 -08:00
Leonardo de Moura	28eb980484	fix(build): C++ module dependency problem, and style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 18:30:31 -08:00
Leonardo de Moura	c8e1ec87d2	feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 18:30:19 -08:00
Leonardo de Moura	7c2a4211a8	feat(kernel): expose imported predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 16:41:40 -08:00
Leonardo de Moura	07059b0531	feat(library): add if_then_else Lean/C++ interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 16:10:49 -08:00
Leonardo de Moura	8217a544cc	fix(library/hop_match): bugs in the higher-order matching procedure, add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 14:37:28 -08:00
Leonardo de Moura	acfb11e290	fix(kernel/instantiate): relax apply_beta pre-condition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 14:36:51 -08:00
Leonardo de Moura	a968a43487	fix(kernel/free_vars): make sure has_free_var does not return incorrect result due to arithmetic overflows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 14:36:14 -08:00
Leonardo de Moura	f8eaae7218	feat(builtin/kernel): add new useful theorems for the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 18:21:22 -08:00
Leonardo de Moura	4595c50f7e	fix(library/hop_match): in locally bound variable management Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 18:06:23 -08:00
Leonardo de Moura	ccb9faf065	refactor(*): error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 16:54:21 -08:00
Leonardo de Moura	55aa4cbfa3	feat(frontends/lean): improve error message for expressions containing unsolved metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 13:21:44 -08:00
Leonardo de Moura	12451e4a35	feat(frontends/lean/pp): display implicit arguments when expression contains metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 12:42:05 -08:00
Leonardo de Moura	35bacf95fc	feat(shell): provide the default environment when parsing Lua files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 18:21:14 -08:00
Leonardo de Moura	7f818ecd92	feat(library): match procedure for higher-order patterns Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:45:24 -08:00
Leonardo de Moura	e6c322d97f	feat(kernel/free_vars): make free_vars module functions more robust Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:44:28 -08:00
Leonardo de Moura	29fec3fecc	fix(builtin/util): bug incorrect encoding of \t and \n in regular expression, and missing local Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:40:41 -08:00
Leonardo de Moura	915644f3b3	fix(util/debug): avoid infinite loop when Ctrl-D is pressed after an assertion violation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:20:35 -08:00
Leonardo de Moura	5d9a95addd	refactor(kernel/free_vars): replace max_free_var with relaxed free_var_range Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:06:57 -08:00
Leonardo de Moura	582569b793	feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 16:46:53 -08:00
Leonardo de Moura	4d9eb4ac6c	feat(kernel): add max_free_var function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 16:45:34 -08:00
Leonardo de Moura	6508e63a17	feat(builtin/macros): add assume/take macros for making proof scripts more readable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 18:36:37 -08:00
Leonardo de Moura	781720a26a	feat(builtin/kernel): add left_comm theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 18:08:08 -08:00
Leonardo de Moura	a1a467a65f	refactor(builtin): move congruence theorems to kernel/if_then_else modules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 13:48:28 -08:00
Leonardo de Moura	a0a92f11b7	feat(builtin/congr): add congruence theorems for contextual simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 13:37:36 -08:00
Leonardo de Moura	53537d0684	feat(builtin/kernel): 'implication' simplification theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 13:35:20 -08:00
Leonardo de Moura	50f281b430	feat(builtin/kernel): add eqf_intro and eqf_elim theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 11:13:54 -08:00
Leonardo de Moura	4057f0d2fe	feat(emacs): minor improvements to emacs mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 11:13:20 -08:00
Leonardo de Moura	745c702ffb	fix(build): dependency problem on some platforms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-10 19:06:15 -08:00
Leonardo de Moura	d4a7d796a5	feat(builtin): prove strong induction theorem, add < theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-10 18:46:33 -08:00
Leonardo de Moura	5fb718c03a	fix(build): broken dependencies between lean executable and .olean, _decls.cpp and _decls.h files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-10 10:58:35 -08:00
Leonardo de Moura	9e8b083673	feat(emacs): more highlighting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 20:44:01 -08:00
Leonardo de Moura	3008cad151	feat(emacs): highlight tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 20:10:57 -08:00
Leonardo de Moura	2cf73fc4d2	feat(emacs): useful abbreviations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 19:57:00 -08:00
Leonardo de Moura	65bdb9c7e0	fix(frontends/lean): unprotected call to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 19:56:20 -08:00
Leonardo de Moura	411f14415d	feat(builtin): automatically generate Lean/C++ interface for builtin theories Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 18:09:53 -08:00
Leonardo de Moura	a339a53f50	feat(util/options): 'verbose' as a system option, add -q (quiet) option Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 15:31:58 -08:00
Leonardo de Moura	8c41b4e899	feat(build): run tests using -t Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 14:12:32 -08:00
Leonardo de Moura	2179e57db3	refactor(builtin): move if_then_else to its own module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 14:08:39 -08:00
Leonardo de Moura	fdeb457a81	feat(kernel/pos_info_provider): add support for file names in pos_info_provider The idea is to include the file name when displaying justification objects. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 12:19:30 -08:00
Leonardo de Moura	dff0b9011b	chore(builtin/cast): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 12:06:22 -08:00
Leonardo de Moura	3e18cdfeec	feat(util/format): do not use colors by default Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:56:58 -08:00
Leonardo de Moura	6fe362ef07	feat(emacs): include lean-mode Emacs files in the distribution Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:50:07 -08:00
Leonardo de Moura	84e211b81b	fix(frontends/lean): missing ':' in error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:19:58 -08:00
Leonardo de Moura	f7c7dd4ed4	feat(frontends/lean): include filename in error messages, use GNU error message style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:01:27 -08:00
Leonardo de Moura	87b238efcd	chore(builtin/kernel): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 09:00:05 -08:00
Leonardo de Moura	57c0006916	chore(*): cleanup lean builtin symbols, replace :: with _ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 08:33:52 -08:00
Leonardo de Moura	25086947fa	fix(builtin/kernel): incorrect comment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 19:14:11 -08:00
Leonardo de Moura	e42b616438	fix(kernel/normalizer): equality between semantic attachments Given a heterogenous equality: a == b The normalizer will only reduce it if a and b are objects of the same kind. Now, 1 == true is not reduced to false anymore. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 19:10:30 -08:00
Leonardo de Moura	8e9d88c2cf	refactor(builtin/kernel): prove iff::intro, and add a new name for it boolext (Boolean extensionality) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 18:31:45 -08:00
Leonardo de Moura	a4b3d6d6c8	refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 17:25:14 -08:00
Leonardo de Moura	9c8026b86e	refactor(builtin/macros): remove 'take', 'discharge' and 'instantiate' macros Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:58:01 -08:00
Leonardo de Moura	bdec4c8799	refactor(builtin/Nat): mark constants as opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:53:08 -08:00
Leonardo de Moura	2e3b92ef36	refactor(builtin/kernel): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:52:43 -08:00
Leonardo de Moura	a6e0dcc96c	fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:19:11 -08:00
Leonardo de Moura	57640ecf19	fix(library/elaborator): array bounds Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 13:18:49 -08:00
Leonardo de Moura	2b2aa228e3	refactor(builtin/kernel): start with small universes The universe constraint manager is more flexible now. We don't need to start with a huge universe U >= 512. We can start small, and increase it on demand. If module mod1 needs it, it can always add universe U >= 3 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 12:35:00 -08:00
Leonardo de Moura	cfe576f551	fix(library/elaborator): bug in the elaborator The elaborator was not handling correctly constraints of the form ctx \|- ?m << (Pi x : A, B) and ctx \|- (Pi x : A, B) << ?m Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 12:10:50 -08:00
Leonardo de Moura	dd6c13abb0	fix(util/buffer): warning produced by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 11:27:11 -08:00
Leonardo de Moura	85de05e5cf	chore(kernel/unification_constraint): update max_constraint comment to reflect its new semantics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 01:09:47 -08:00
Leonardo de Moura	abf61be8f6	chore(library/tactic): remove imp_tac, it is not needed anymore Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 00:57:04 -08:00
Leonardo de Moura	048151487e	feat(kernel): use Pi as forall/implication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 00:38:39 -08:00
Leonardo de Moura	e12d6e44cd	fix(util/name): bug in Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:52:51 -08:00
Leonardo de Moura	8ce6266e6b	feat(library/kernel_bindings): add new predicates for kernel objects in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:36:54 -08:00
Leonardo de Moura	6f4ca7bd2a	feat(frontends/lean): expose is_explicit function in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:36:27 -08:00
Leonardo de Moura	4fdc0406be	feat(util/name): additional methods to name Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:35:34 -08:00
Leonardo de Moura	248d55d454	chore(util/script_state): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 16:59:50 -08:00
Leonardo de Moura	2cd2527d9f	refactor(shell): move read-eval-loop script to repl.lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 16:56:22 -08:00
Leonardo de Moura	0bc2c51c9c	fix(build): put back the dependency on lean executable for .olean files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 16:13:58 -08:00
Leonardo de Moura	d12d0f036f	feat(kernel/environment): universe variables now live in their own namespace Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:57:36 -08:00
Leonardo de Moura	95515ca5df	chore(*): fix warnings produced by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:39:49 -08:00
Leonardo de Moura	a3af87f8d3	chore(frontends/lean/frontend): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:28:21 -08:00
Leonardo de Moura	0363faeec8	fix(frontends/lean/scanner): assertion violation, and add more tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:12:34 -08:00
Leonardo de Moura	fb73514913	fix(frontends/lean/parser): parser aborted if the scanner throws an exception in the first call to scan(); position information was being shown twice for scanner exceptions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:04:30 -08:00
Leonardo de Moura	f12a76a5cd	test(frontends/lean/scanner): missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:03:46 -08:00
Leonardo de Moura	c7338a8eab	chore(frontends/lean/scanner): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:37:28 -08:00
Leonardo de Moura	29db6accb8	test(tests/lean): new tests for exercising the environment object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:34:21 -08:00
Leonardo de Moura	f67eab000b	fix(util/serializer): nontermination on corrupted files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:21:54 -08:00
Leonardo de Moura	d5ddb186d9	feat(library/kernel_bindings): add load method to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:21:24 -08:00
Leonardo de Moura	6077dc61b7	feat(builtin): remove lean executable as a dependency for builtin .lean files Otherwise, we have to rebuild all .lean files whenever we change the executable. This commit also adds a test for each .lean file. This is useful for increasing coverage and having a log on how long does it take to process these files. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 13:53:30 -08:00
Leonardo de Moura	0a20356a51	fix(kernel/environment): we should not add an universe contraint object to the set of object when an integer overflow occurs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 13:43:22 -08:00
Leonardo de Moura	17c4cce89c	fix(library/elaborator): remove_detail procedure was keeping a lot of details when typeof_mvar_justification was being used Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 13:24:46 -08:00
Leonardo de Moura	0f1737d62c	fix(frontends/lean): more precise position information for infix operators Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 13:19:26 -08:00
Leonardo de Moura	0bdecb6aa4	style(builtin/Nat): name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 00:05:51 -08:00
Leonardo de Moura	c5d13abd6f	refactor(builtin/Nat): rename destruct to discriminate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 23:05:27 -08:00
Leonardo de Moura	abb9b8af83	fix(frontends/lean): bug in pop::context command, and add new tests for the universe command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 17:14:07 -08:00
Leonardo de Moura	4424a314e0	feat(kernel): add get_universe_distance method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 17:13:13 -08:00
Leonardo de Moura	5fe8c32da9	feat(kernel): use new universe contraints in the environment, allow new constraints to be added Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 16:46:11 -08:00
Leonardo de Moura	b5a30855f8	feat(kernel/universe_constraints): add new class for managing universe constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 15:01:28 -08:00
Leonardo de Moura	68832dc6f2	fix(builtin/macros): comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 12:07:13 -08:00
Leonardo de Moura	929a536e2f	fix(builtin/README): update documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 12:03:11 -08:00
Leonardo de Moura	62bb2ab2f9	fix(builtin/Nat): name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:14 -08:00
Leonardo de Moura	645e748302	feat(frontends/lean): add 'using' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:14 -08:00
Leonardo de Moura	8c956280d9	chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:03 -08:00
Leonardo de Moura	7222a2d1a9	feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 21:39:31 -08:00
Leonardo de Moura	935c2a03a3	feat(*): change name conventions for Lean builtin libraries Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 19:21:44 -08:00
Leonardo de Moura	771b099c0c	fix(frontends/lean): must invoke lua GC before closing a scope, reason: we may still have references to the current environment inside of the Lua state object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 16:38:29 -08:00
Leonardo de Moura	9d6bd7501c	feat(doc/lean): include lean documentation scripts in the test set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 13:16:47 -08:00
Leonardo de Moura	4ba097a141	feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 13:06:36 -08:00
Leonardo de Moura	6569b07b7c	feat(frontends/lean/parser): rename 'show' expression to 'have' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 11:25:58 -08:00
Leonardo de Moura	0b4bdceb10	feat(builtin/macros): rename 'For' macro to 'take' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 11:08:55 -08:00
Leonardo de Moura	9f08156a73	feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 11:03:35 -08:00
Leonardo de Moura	ce1213a020	feat(frontends/lean): use '(* ... )' instead of '(* ... **)' for script code blocks Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 10:32:47 -08:00
Leonardo de Moura	028a9bd9bd	feat(frontends/lean/scanner): use Lua style comments in Lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 08:53:27 -08:00
Leonardo de Moura	f5cc2458a9	fix(frontends/lean/parser_calc): missing save calls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 18:26:30 -08:00
Leonardo de Moura	fbe0bccf51	chore(*): name convention, proof construnction functions/macros start with upper-case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 18:11:01 -08:00
Leonardo de Moura	9eb4dc4a81	feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend This commit affects different modules. I used the following approach: 1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure. 2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads. 3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 17:18:23 -08:00
Leonardo de Moura	66ec538c63	doc(doc/lean/calc.md): calculational proof documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 11:52:21 -08:00
Leonardo de Moura	5b5cebe750	refactor(builtin/Nat): use obtain-from instead of ExistsElim, and use more user-friendly argument order for Induction Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 10:33:57 -08:00
Leonardo de Moura	9f3706e365	feat(builtin/macros): add obtain-from macro for ExistsElim Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 10:32:49 -08:00
Leonardo de Moura	d7efdff83d	feat(builtin/Nat): add more leq theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 22:48:10 -08:00
Leonardo de Moura	cf35e7bed7	feat(frontends/lean): add support for disequalities in calculational proofs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 22:47:45 -08:00
Leonardo de Moura	6329d1828d	feat(frontends/lean): reuse name expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 20:08:21 -08:00
Leonardo de Moura	92c7145d7f	feat(kernel/expr): maximize sharing before serializing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 20:03:42 -08:00
Leonardo de Moura	2d5800ace4	feat(builtin/Nat): leq axiom, and some theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 18:24:32 -08:00
Leonardo de Moura	9620b00e24	feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator. For example, suppose we have the constraint ctx \|- ?M1[inst:0 ?M2] == a If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions: ?M1 == a or ?M1 == #0 and ?M2 == a On the other hand, if ?M2 is assigned to b, then we can ignore the second case. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 16:08:38 -08:00
Leonardo de Moura	ecc5d1bc3a	refactor(kernel): move printer to library, cleanup io_state interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:37:50 -08:00

... 22 23 24 25 26 ...

3817 commits