1218 commits

Author	SHA1	Message	Date
Leonardo de Moura	f57fc33442	fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-31 16:46:16 -07:00
Leonardo de Moura	9637ceb86e	feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl' ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-30 15:04:44 -07:00
Leonardo de Moura	450131692a	fix(library/converter): missing constraint on eta expansion ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-30 10:43:47 -07:00
Leonardo de Moura	936bb2744b	fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 17:32:55 -07:00
Leonardo de Moura	320bc55e85	fix(frontends/lean/elaborator): use preprocessed expression when displaying errors ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 14:25:50 -07:00
Leonardo de Moura	b15f1bb8c7	fix(frontends/lean/elaborator): apply coercions in definitions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 13:55:39 -07:00
Leonardo de Moura	501cae37e5	fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-29 13:04:58 -07:00
Leonardo de Moura	105c29b51e	refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-28 19:59:38 -07:00
Leonardo de Moura	5f360cd8ec	feat(kernel/error_msgs): improve application type mismatch error messages ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-28 07:08:12 -07:00
Leonardo de Moura	4b2e403023	test(tests/lean/run): add more tests sent by Cody ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-27 12:17:38 -07:00
Leonardo de Moura	faee08591f	fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions ... This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not. The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-27 12:12:54 -07:00
Leonardo de Moura	6ca120bf77	test(tests/lean/run): add Cody's file to test suite ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-27 08:17:46 -07:00
Leonardo de Moura	0cdd4a267c	feat(frontends/lean/pp): pretty print 'show' expressions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 21:56:35 -07:00
Leonardo de Moura	60cc9ac8e2	feat(frontends/lean/pp): pretty print 'have' expressions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 21:35:26 -07:00
Leonardo de Moura	cf35c07786	fix(frontends/lean): fix 'let' annotation placement and pretty printer ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 21:00:22 -07:00
Leonardo de Moura	206206060f	test(tests/lean/hott): add some of Vladimir's definitions as tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 20:50:37 -07:00
Leonardo de Moura	70ef92cd5e	feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 10:53:44 -07:00
Leonardo de Moura	23af5ab217	fix(library/unifier): eager whnf application ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-26 10:37:02 -07:00
Leonardo de Moura	709b5ce90f	fix(kernel/justification): duplicate position ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 21:16:49 -07:00
Leonardo de Moura	70c887a0bd	fix(library/unifier): fix cryptic error message ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 21:10:32 -07:00
Leonardo de Moura	e79b0b11cf	test(tests/lean/run): another test for the unifier ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 20:55:05 -07:00
Leonardo de Moura	cf44c80ffb	fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 16:00:38 -07:00
Leonardo de Moura	7b84503133	fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 15:03:57 -07:00
Leonardo de Moura	0f12e5a35b	fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 13:49:45 -07:00
Leonardo de Moura	a59eec39b8	feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 09:44:40 -07:00
Leonardo de Moura	21176c61fe	fix(tests/lean): move crash.lean to different directory ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 08:48:35 -07:00
Leonardo de Moura	e7c7d5718a	fix(frontends/lean/pp): fix bug in the pretty printer ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-25 08:30:30 -07:00
Leonardo de Moura	15c1e39f88	feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-24 23:43:40 -07:00
Leonardo de Moura	905a1095f9	fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-24 23:41:23 -07:00
Leonardo de Moura	5529ef1056	feat(library/standard): add function 'helper' module ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-24 16:29:39 -07:00
Leonardo de Moura	d998bf9300	test(tests/lean/run): add some 'lost' tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-23 08:22:53 -07:00
Leonardo de Moura	b522ea6f2d	refactor(library/standard): rename bit to bool ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-22 09:49:54 -07:00
Leonardo de Moura	5eaf04518b	refactor(*): rename Bool to Prop ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-22 09:43:18 -07:00
Leonardo de Moura	a9f7d87aae	test(tests/lean/run/decidable): show implicit argument that is computed automatically ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-22 05:58:36 -07:00
Leonardo de Moura	5e8c128b00	feat(library/standard): add more decidable instances ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-20 01:10:49 +01:00
Leonardo de Moura	6b60db7b93	fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-19 09:55:34 +01:00
Leonardo de Moura	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	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	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	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	e432e23115	test(tests/lean/run/class5): improve test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-13 22:39:16 +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	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	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	6000270d35	chore(tests/lean): reactivate config.lean ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 23:32:23 +01:00
Leonardo de Moura	e9c17b154c	fix(tests/lean): define LEAN_PATH in tests scripts ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 23:26:55 +01:00
Leonardo de Moura	92bb046854	test(tests/lean/run): add nested let-expr test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 15:56:15 +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	06beff327f	test(tests/lean/run): add more universe tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-10 14:43:55 +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	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	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	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	2ad1a93657	test(tests/lean/run): add append tactic test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-08 18:21:22 -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	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	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	d30f387e72	feat(library/standard): add namespace 'pair' ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-07 14:48:19 -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	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	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	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	8e5ac54ae1	test(tests/lean/run): group experiments ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 22:31:57 -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	e68a3e5251	test(tests/lean/run): add another class-instance example ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-05 17:41:08 -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	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	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	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	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	a97f82be1a	fix(library/standard): orelse notation, avoid conflict with inductive datatype declaration ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-04 10:10:05 -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	855ffcba34	feat(library/standard): add pairs ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 20:43:16 -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	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	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	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	c1538bfc40	test(tests/lean/run): add 'apply subst' test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-07-03 09:07:56 -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	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	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	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	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	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	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	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	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	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	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	7d5522e36a	chore(tests): add missing tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:03:51 -07:00
Leonardo de Moura	f5f3816596	chore(tests): cleanup test scripts ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-29 09:03:39 -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	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	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	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	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	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	a7623845f9	test(tests/lean/run): add another example on how to deal with ambiguity ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 10:18:35 -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	cc21bfd01d	test(tests/lean/run): more tests on how to deal with ambiguity ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:26 -07:00
Leonardo de Moura	dc5553ea5c	test(tests/lean/run): add test demonstrating how to control ambiguity ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:19 -07:00
Leonardo de Moura	da6e92787a	test(tests/lean/run): add simple overloading test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-26 09:32:12 -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	4bc1f3cf81	test(lean/run): add elaborator tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 16:15:01 -07:00
Leonardo de Moura	49a6048060	test(lean/run): add another test for new elaborator ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-25 13:18:32 -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	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	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	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	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	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	3bb53810c5	test(lean/run): add notation test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-18 09:48:47 -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	813e033f54	test(lean): add simple example of notation implemented using Lua ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-17 22:37:22 -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	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	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	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	873a5c8605	test(lean): add 'let' expression test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-16 14:11: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	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	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	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	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	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	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	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	fad4780d72	test(lean/run): add overload test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-13 18:06:44 -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	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	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	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	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	3a0861bca7	test(lean): remove old test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 10:42:10 -07:00
Leonardo de Moura	9f06cd553e	test(lean): remove tests using Lean old syntax and kernel ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-17 10:38:53 -07: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	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	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	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	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	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	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	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	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	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	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	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	eab0456b27	test(tests/lean): test super opaque style ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 11:33:27 -08:00
Leonardo de Moura	fdc4c9b53c	test(tests/lean): add nested 'have' expression test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 08:13:04 -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	419fb7464e	fix(tests/lean): adjust tests to reflect recent changes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 21:04: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	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	413391b2b4	chore(tests/lean/sig2): remove unnecessary parenthesis from test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 11:37:08 -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	96c9c7505a	test(tests/lean): add another sigma-type test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 10:12:39 -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	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	640ebcc040	test(tests/lean/exp): add example for Steve ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 11:35:40 -08:00
Leonardo de Moura	e4afa3dc43	fix(tests/lean/map): incorrect output ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 00:05:19 -08:00
Leonardo de Moura	87f9c9b27e	fix(tests/lean/map): make sure the unit test produce the same result in different platforms ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-02 20:29:34 -08:00
Leonardo de Moura	e2add5c9f2	test(tests/lean): add heterogeneous equality simplification example ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-02 20:27:39 -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	2b7bc7b673	test(tests/lean/exp): simulating HOL constructions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-31 17:59:57 -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	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	0bb8fe75b3	test(tests/lean): new simplifier test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 14:21:18 -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	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	62408a6adc	test(tests/lean): move simp_loop test to slow subdirectory ... This example produces a stackoverflow on Valgrind. We don't execute Valgrind on tests in the slow subdirectory. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 10:32:48 -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	72c607846a	test(tests/lean): add Jeremy's proof to test suite ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 16:05:46 -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	db45d02078	fix(tests/lean): test discrepancy on OSX ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 23:31:35 -08:00
Leonardo de Moura	7b88d68afb	test(tests/lean): add test using simplifier monitor for tracking failures ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 15:11:16 -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	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	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	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	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	5b13ef1b90	test(tests/lean): new simplifier test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 10:56:49 -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	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	35ad156a46	fix(tests/lean): make sure pretty print and parse test passes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:23:55 -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	1a3660180e	test(tests/lean): add new simplifier test ... 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	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	cd87cb3de4	test(tests/lean): add test for congruence theorem that uses an argument before simplification ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-23 13:26:09 -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	5ba2525eab	test(tests/lean): add test disabling contextual simplifications ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-23 12:57:05 -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	331b5846c6	test(library/simplifier): add test for the single_pass option in the simplifier ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 13:47:54 -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	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	d1bd56b3d3	fix(tests/lean): adjust test to reflect recent changes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 14:47:03 -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	5224df56a3	test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 08:36:48 -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	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	bcede6925f	fix(tests/lean): add expected result file ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 16:31:35 -08:00
Leonardo de Moura	19f3c281c3	test(tests/lean): matrix multiplication example ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 16:29:32 -08:00
Leonardo de Moura	999984e701	fix(tests/lean): remove unnecessary theorems ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 12:55:33 -08:00
Leonardo de Moura	cc11b9e125	test(tests/lean): rewriting proof example ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 12:53:21 -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	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	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	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	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	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	57e58c598c	fix(tests/lean): adjust tests to reflect recent changes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 16:35:33 -08:00
Leonardo de Moura	91e1f9fc02	fix(tests/lean): adjust test to reflect recent changes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 10:20:35 -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	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	b85b45b40f	test(tests/lean): When and Cond tactical tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 20:43:39 -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	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	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	52e11dbbee	test(tests/lean): 'using' command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 12:21:14 -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	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	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	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	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	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	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	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	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	d29d23cade	test(tests/lean): alias command error ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:29:16 -08:00
Leonardo de Moura	9f4959fb64	test(tests/lean): kernel exception pp method ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:19:52 -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	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	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	8f3c97ca98	test(tests/lean): standard induction ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 10:18:31 -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	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	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	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	502d9f47ac	test(tests/lean): new test full of holes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 16:31:52 -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	430b75f38f	test(tests/lean): add version of the Nat library full of holes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 12:31:13 -08:00
Leonardo de Moura	e714bd7982	feat(frontends/lean): add syntax sugar for applying Subst in calculational proofs ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 11:23:55 -08:00
Leonardo de Moura	111949b9be	feat(frontends/lean): calculational proofs ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 10:53:14 -08:00
Leonardo de Moura	b2a8f4118d	feat(library/elaborator): process ho-match before normalizing ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 14:46:19 -08:00
Leonardo de Moura	7726ccad28	chore(builtin): rename nat, int and real modules to Nat, Int and Real. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 13:52:25 -08:00
Leonardo de Moura	d633622d90	feat(frontends/lean/parser): namespaces ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 12:28:18 -08:00
Leonardo de Moura	c423198a69	feat(builtin/kernel): add Not.*Elim theorems ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 11:35:21 -08:00
Leonardo de Moura	a8bc9fb4e0	refactor(builtin/kernel): mark exists as opaque after proving key theorems ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 11:00:32 -08:00
Leonardo de Moura	cbd1f98365	fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 03:02:41 -08:00
Leonardo de Moura	cd3bbb1ebf	fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-31 10:14:17 -08:00
Leonardo de Moura	390a78a8d2	chore(frontends/lean/parser): remove 'Skipped' message ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 15:35:12 -08:00
Leonardo de Moura	08718e33dc	refactor(builtin): only load the kernel and natural numbers by default ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 13:35:37 -08:00
Leonardo de Moura	ecd62a1783	refactor(builtin/basic): rename basic.lean to kernel.lean ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:46:03 -08:00
Leonardo de Moura	4401b390fe	refactor(library/arith): do not load specialfn by default ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:25:43 -08:00
Leonardo de Moura	46a8300a2d	refactor(library/arith): move real and special function declarations to .lean files ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:02:22 -08:00
Leonardo de Moura	c3bc6afb12	refactor(library/arith): move int and nat declarations to .lean files. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 10:32:14 -08:00
Leonardo de Moura	15621610e9	refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments ... This commit also fixes bugs in the Alias command. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 17:04:36 -08:00
Leonardo de Moura	a1a5fb101d	feat(frontends/lean): add Alias command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 16:25:45 -08:00
Leonardo de Moura	dfe46b9d25	refactor(kernel/builtin): move definition and axioms to basic.lean ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 14:01:30 -08:00
Leonardo de Moura	f8b82d854e	feat(builtin/basic): add TypeM alias ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 13:03:32 -08:00
Leonardo de Moura	411ebbc3c1	refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file ... This commit also adds several new theorems that are useful for implementing the simplifier. TODO: perhaps we should remove the declarations at basic_thms.h? Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 03:04:49 -08:00
Leonardo de Moura	41c1010043	feat(frontends/lean/parser): make Import command use binary Lean files ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 19:20:04 -08:00
Leonardo de Moura	1fd81dd3a1	feat(frontends/lean/parser): disable verbose messages when importing files ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 12:24:13 -08:00
Leonardo de Moura	44a31dd8fb	feat(frontends/lean/parser): improve Import command ... - The extension does not have to be provided. - It can also import Lua files. - Hierachical names can be used instead of strings. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 12:05:01 -08:00
Leonardo de Moura	8e86d6578c	fix(tests/lean): adjust tests to reflect modifications in the pp ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 18:38:45 -08:00
Leonardo de Moura	3f0279b88c	refactor(frontends/lua): replace lean.lua.h with util.lua ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 19:49:26 -08:00
Leonardo de Moura	275f022d79	fix(tests/lean): ignore lines containing 'executing external script' in test scripts, these lines contain references to the path where Lean was built ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 18:41:01 -08:00
Leonardo de Moura	f1b97b18b4	refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 15:54:53 -08:00
Leonardo de Moura	ef18cc4a92	fix(frontends/lean/parser): add existing command macros when creating parser object ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 13:38:14 -08:00
Leonardo de Moura	8e4560a866	feat(frontends/lean/parser): protect imported modules from Lua definitions and macros in the file importing the module ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 13:21:36 -08:00
Leonardo de Moura	ba02132a90	feat(frontends/lean/parser): add command macros ... The idea is to allow users to define their own commands using Lua. The builtin command Find is now written in Lua. This commit also fixes a bug in the get_formatter() Lua API. It also adds String arguments to macros. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 13:00:28 -08:00
Leonardo de Moura	480781d13e	feat(frontends/lean/parser): provide environment as an argument to macros, allow macros to parse tactics ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-26 11:15:45 -08:00
Leonardo de Moura	3673f2ac1d	feat(frontends/lean/parser): add Find command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 18:31:52 -08:00
Leonardo de Moura	a3dde29f3c	feat(frontends/lua/parser): allow users to specify the precedence of macros ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 12:27:56 -08:00
Leonardo de Moura	88235d2922	feat(library/tactic/apply_tactic): try other solutions produced by the elaborator ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-25 11:51:27 -08:00
Leonardo de Moura	8e45064f25	feat(library/tactic/apply_tactic): improved parametric apply_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 22:40:34 -08:00
Leonardo de Moura	c87e965f86	fix(tests/lean/tactic14.lean): typo ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 21:36:49 -08:00
Leonardo de Moura	cb95b14332	feat(library/tactic/apply_tactic): improve apply_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 14:23:06 -08:00
Leonardo de Moura	879ab6924a	tests(test/lean): remove 'Importing...' message, the tests using the Import command fail when running on a different machine ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-24 12:26:53 -08:00
Leonardo de Moura	00e89190c2	refactor(library/cast): use .lean file instead of .cpp file to define casting library ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 22:04:19 -08:00
Leonardo de Moura	8c8cefcb0c	feat(frontends/lean/parser): compact definitions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 21:24:50 -08:00
Leonardo de Moura	5043cc75f6	fix(frontends/lean/parser): allow parenthesis in level expressions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 13:31:55 -08:00
Leonardo de Moura	2c30b87f30	test(tests/lean): ExistsElim test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-23 12:57:25 -08:00
Leonardo de Moura	baf99779dc	feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 17:57:51 -08:00
Leonardo de Moura	65f7217935	fix(tests/lean/norm_tac): display implicit parameters to make sure output can be parsed ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 17:11:36 -08:00
Leonardo de Moura	3e32d9bef2	feat(library/tactic): add support for Pi's at to_proof_state ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 16:40:55 -08:00
Leonardo de Moura	104bd990e1	feat(library/tactic): add normalize_tac, eval_tac and trivial_tac ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 14:10:42 -08:00
Leonardo de Moura	4229e498d2	refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-22 11:51:38 -08:00
Leonardo de Moura	9128a437b8	refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 18:23:37 -08:00
Leonardo de Moura	df58eb132e	feat(frontends/lean): simplify explicit version names ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 17:05:25 -08:00
Leonardo de Moura	36b2ec9abb	fix(library/cast): bugs in Cast semantic attachment ... TODO: revise cast semantic attachment. It should be axioms instead of semantic attachments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 16:16:54 -08:00
Leonardo de Moura	aebff0b4d3	fix(library/type_inferer): bug in get_range method ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 14:55:07 -08:00
Leonardo de Moura	55d46b2f88	test(tests/lean): add new normalizer/elaborator test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 06:43:25 -08:00
Leonardo de Moura	9444c1f47f	test(tests/lean): add example that cannot be elaborated ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 04:19:53 -08:00
Leonardo de Moura	fddcdb8f40	fix(library/elaborator): bug in process_lower ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 04:13:14 -08:00
Leonardo de Moura	66f106da8c	test(tests/lean): new error msg test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-21 03:20:04 -08:00
Leonardo de Moura	ce84fe5d33	feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 22:00:50 -08:00
Leonardo de Moura	bb81311e0a	feat(frontends/lean/parser): include proof state in exception for tactic failure ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 17:15:12 -08:00
Leonardo de Moura	7772c16033	refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque ... After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms. If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions. If they are not, instead of throwing an error, we try again expanding the opaque terms. This seems to be the best of both worlds. The opaque flag is a hint for the type checker, but it would never prevent us from type checking a valid term. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 12:47:47 -08:00
Leonardo de Moura	812c1a2960	feat(library/elaborator): only expand definitions that are not marked as hidden ... The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics. For example, in one of the tests, the elaborator was producing the sub-expression (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤) After, this commit it produces (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) The expressions above are definitionally equal, but the second is easier to work with. Question: do we really need hidden definitions? Perhaps, we can use only the opaque flag. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-20 02:16:49 -08:00
Leonardo de Moura	c77464703f	feat(frontends/lean): macro definition using Lua ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 19:08:10 -08:00
Leonardo de Moura	b08c606696	fix(library/io_state): bug in the io_state Lua bindings ... This commit also includes a new test that exposes the problem. The options in the io_state object were being lost. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 16:39:42 -08:00
Leonardo de Moura	2648f41eaa	test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 16:16:56 -08:00
Leonardo de Moura	d9e692f506	feat(frontends/lean): improve coercion manangement ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 15:45:46 -08:00
Leonardo de Moura	f43db96e1f	fix(frontends/lean/pp): pretty printer for Type ... Add parenthesis around Type when it has a universe. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 15:24:45 -08:00
Leonardo de Moura	ae01d3818d	fix(frontends/lean/parser): parse_type method ... The parser had a nasty ambiguity. For example, f Type 1 had two possible interpretations (f (Type) (1)) or (f (Type 1)) To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis. Examples: (Type 1) (Type U) (Type M + 1) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 15:24:34 -08:00
Leonardo de Moura	46627289b8	fix(kernel/expr): avoid '_' as a binder name, we use '_' as a placeholder in the Lean frontend ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 14:47:53 -08:00
Leonardo de Moura	d3d24696f4	feat(frontends/lean): hide builtin object in the 'Show Environment' command ... The user can still display builtin objects by using Show Environment all Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 14:00:58 -08:00
Leonardo de Moura	ad3f771b1d	feat(frontends/lean): hide 'explicit' version of objects with implicit arguments ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 13:12:39 -08:00
Leonardo de Moura	bff5a6bfb2	fix(frontends/lean/pp): make sure pp and parser are using the same precedences ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-19 12:46:14 -08:00
Leonardo de Moura	dd72269b13	feat(frontends/lean): rename command Set to SetOption ... It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-18 21:18:48 -08:00
Leonardo de Moura	42cb5d1d3c	fix(tests/lean): typo ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-18 20:11:49 -08:00
Leonardo de Moura	79fa6e4940	feat(frontends/lean): Scopes in the default Lean frontend ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-18 17:40:21 -08:00
Leonardo de Moura	2aaa9a5273	feat(frontends/lean/parser): change function application precedence ... Now, we can write Pi (x y : A), R x y -> R y x instead of Pi (x y : A), (R x y) -> (R y x) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-18 12:44:15 -08:00
Leonardo de Moura	10f28c7bec	feat(kernel/replace_fn): non-recursive replace_fn ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-17 16:35:39 -08:00
Leonardo de Moura	c53233ea26	fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-17 14:33:42 -08:00
Leonardo de Moura	09b51a0fb7	fix(library/elaborator): missing condition ... The elaborator was missing solutions because of the missing condition at is_simple_ho_match. This commit also adds a new test that exposes the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-16 17:13:36 -08:00
Leonardo de Moura	5b29fd8d93	test(tests/lean): add ExistsElim test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-16 15:43:09 -08:00
Leonardo de Moura	8f5c2b7d9f	feat(library/basic_thms): add Refute theorem ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-16 12:03:31 -08:00
Leonardo de Moura	8f9405c8b3	fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive ... This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-16 09:39:02 -08:00
Leonardo de Moura	2972fb9d8c	test(tests/lean): new elaborator tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-15 22:00:26 -08:00
Leonardo de Moura	61bd27ff06	fix(library/elaborator): bug in simple_ho_match ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-15 21:48:55 -08:00
Leonardo de Moura	19ad39159e	feat(library/basic_thms): add ForallIntro theorem ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-15 17:35:31 -08:00
Leonardo de Moura	82dfb553d5	feat(library/basic_thms): add ExistsIntro theorem ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-15 16:26:23 -08:00
Leonardo de Moura	993bea8206	refactor(library/elaborator): improve elaborator state data-structure ... The "quota" hack used before this commit was inefficient, and too hackish. This commit uses two lists of constraints: active and delayed. The delayed constraints are only processed when there are no active constraints. We use a simple index to quickly find which delayed constraints have assigned metavariables. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> checkpoint Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-14 23:27:08 -08:00
Leonardo de Moura	3d30664611	feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-14 15:13:56 -08:00
Leonardo de Moura	4357c9196e	feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' ... This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-14 12:25:00 -08:00
Leonardo de Moura	bbaa83e16a	feat(frontends/lean): implement relaxed operator compatibility in the parser ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 15:42:43 -08:00
Leonardo de Moura	6b1b6c7bd1	feat(tests/lean): include standard error in the expected output ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 12:52:57 -08:00
Leonardo de Moura	90f88acf42	feat(frontends/lean): relax compatible_denotation predicate ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 12:42:29 -08:00
Leonardo de Moura	abe2cf2fb5	feat(frontends/lean): simplify how implicit parameters are marked ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 12:11:04 -08:00
Leonardo de Moura	78ec4b152b	feat(frontends/lean): relax restricitions on parsing applications of functions containing implicit arguments ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-10 09:48:24 -08:00
Leonardo de Moura	0cd8e3e76b	feat(split-stack): add support for split-stacks (no more stackoverflows) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 22:30:54 -08:00
Leonardo de Moura	0eaa98221b	fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-09 12:25:19 -08:00
Leonardo de Moura	68c2e5cc7d	fix(frontends/lean/parser): reachable code ... The new test nbug1.lean exposes the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 15:22:21 -08:00
Leonardo de Moura	04b67f8b14	refactor(kernel/object): remove 'null' object, and operator bool for kernel objects ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-08 14:37:38 -08:00
Leonardo de Moura	1ff6013594	fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes ... The test tactic14.lean exposes the problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 15:37:59 -08:00
Leonardo de Moura	e2999d3ff6	feat(*): add component name to check_stack and check_system ... I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 15:11:55 -08:00
Leonardo de Moura	33b72f1dd0	feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-07 13:09:39 -08:00
Leonardo de Moura	a75d05fdb4	fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 17:03:12 -08:00
Leonardo de Moura	daadff548e	fix(tests/lean): update expected result to reflect recent changes ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 16:31:13 -08:00
Leonardo de Moura	015bff8283	fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term ... This commit fixes a problem exposed by t13.lean. It has a theorem of the form: Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type). Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions. Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created A : Bool, B : Bool, assumption : A /\ B |- B /\ A That is, the lemmas are not available when solving B /\ A. Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used. Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj (Conjunct2 assumption) (Conjunct1 assumption) This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A After this commit, the proof for theorem T1 is Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1 as expected. Finally, this example suggests that the encoding Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 : A := (by auto), lemma2 : B := (by auto) in (show B /\ A by auto) is more efficient than Theorem T1 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, let lemma1 := (show A by auto), lemma2 := (show B by auto) in (show B /\ A by auto) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 16:14:25 -08:00
Leonardo de Moura	0390f3c39b	feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 15:01:54 -08:00
Leonardo de Moura	1df9d18891	feat(frontends/lean): allow 'tactic hints' to be associated with 'holes' ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 14:49:39 -08:00
Leonardo de Moura	2ddcc32c1d	fix(frontends/lean/notation): change the precedence of '->' ... It should match the precedence of the implication '=>'. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 13:23:24 -08:00
Leonardo de Moura	fa03ae2a26	fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints ... This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 13:04:34 -08:00
Leonardo de Moura	d46cf5fdd5	fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-06 05:13:29 -08:00
Leonardo de Moura	13f9454fe1	feat(library/tactic/proof_state): add option tactic::proof_state::goal_names ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 21:18:22 -08:00
Leonardo de Moura	e6fb6f7d1e	feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 20:08:51 -08:00
Leonardo de Moura	0c059a9917	feat(library/tactic): use _tac suffix instead of _tactic like Isabelle ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 20:06:32 -08:00
Leonardo de Moura	1b176204b4	feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 19:03:12 -08:00
Leonardo de Moura	e1d44eec6b	fix(frontends/lean/parser): bug in parse_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:40:55 -08:00
Leonardo de Moura	a564795fe6	fix(frontends/lean/parser): remove unnecessary '#' after error ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:27:08 -08:00
Leonardo de Moura	74a8b5f2f4	test(tests/lean/interactive): add back command test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:19:53 -08:00
Leonardo de Moura	e069ce640b	feat(frontends/lean/parser): add tactic abort command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 17:15:19 -08:00
Leonardo de Moura	34654ad06b	feat(tests/lean/interactive): add interactive mode test script ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 16:56:20 -08:00
Leonardo de Moura	e3848d43a2	feat(frontends/lean): improve tactic command parsing in interactive mode ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 16:28:08 -08:00
Leonardo de Moura	fa98c1358f	feat(library/tactic): add disj_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 04:49:06 -08:00
Leonardo de Moura	029ef57abd	feat(library/tactic): add apply_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-05 03:22:12 -08:00
Leonardo de Moura	e60e20a11d	feat(frontends/lean): add Exit command ... Remark: on Windows, Ctrl-D does not seem to work. So, this commit also changes the Lean startup message. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-04 10:40:22 -08:00
Leonardo de Moura	dd62af1641	feat(frontends/parser): simplified theorem definition using tactical proof ... When using tactics for proving theorems, a common pattern is Theorem T : <proposition> := _. apply <tactic>. ... done. This commit allows the user to write the simplified form: Theorem T : <proposition>. apply <tactic>. ... done. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 08:20:18 -08:00
Leonardo de Moura	25978118df	feat(library/tactic): add beta-reduction tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-02 08:10:51 -08:00
Leonardo de Moura	1ec8f9d536	feat(kernel): add abstraction (aka function extensionality) axiom ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 13:57:14 -08:00
Leonardo de Moura	09f98ecddc	feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 10:41:05 -08:00
Leonardo de Moura	ca53a5a1cc	feat(library/tactic): add unfold tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 08:51:56 -08:00
Leonardo de Moura	f91c4901e8	feat(library/tactic): add absurd_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 07:55:00 -08:00
Leonardo de Moura	bf2adb20e7	feat(library/tactic): add disj_hyp_tactic ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-01 07:55:00 -08:00
Leonardo de Moura	1a221d8bbe	feat(library/tactic): add focus tactical ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-30 11:28:38 -08:00
Leonardo de Moura	98897b467d	feat(frontends/lean/parser): add support for Lua expression code blocks ... In expression code blocks, we do not have to write a "return". After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **) instead of apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 10:21:24 -08:00
Leonardo de Moura	f9874cd675	feat(library/tactic): add to_tactic_ext, it allows functions that return tactics to be used where a tactic is expected ... For example, after this commit, we can write simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic instead of simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic() Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 09:40:21 -08:00
Leonardo de Moura	20a36e98ec	feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. ... Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-29 09:15:01 -08:00
Leonardo de Moura	b3f87e2e4f	feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 22:11:07 -08:00
Leonardo de Moura	5dfb3b8b56	feat(frontends/lean/parse): allow script-code blocks to be used in the apply command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 21:48:30 -08:00
Leonardo de Moura	c6b05bcfcb	feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 18:23:38 -08:00
Leonardo de Moura	e3f3ec5553	feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-28 18:17:15 -08:00
Leonardo de Moura	d87ad9eb7e	refactor(util/lua): propagate C++ Lean exceptions in Lua ... The following call sequence is possible: C++ -> Lua -> C++ -> Lua -> C++ The first block of C++ is the Lean main function. The main function invokes the Lua interpreter. The Lua interpreter invokes a C++ Lean API. Then the Lean API invokes a callback implemented in Lua. The Lua callback invokes another Lean API. Now, suppose the Lean API throws an exception. We want the C++ exception to propagate over the mixed C++/Lua call stack. We use the clone/rethrow exception idiom to achieve this goal. Before this commit, the C++ exceptions were converted into strings using the method what(), and then they were propagated over the Lua stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++. This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-27 12:25:29 -08:00
Leonardo de Moura	99a811a586	feat(bindings/lua): expose io_state object in the Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-26 12:54:47 -08:00
Leonardo de Moura	87775cbc07	chore(build): include incorrect output in the logs ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-18 15:39:55 -08:00
Soonho Kong	20756c382c	test(*): split leantests, leanslowtests, leanluatests, leanluadocs into singletons	2013-11-18 18:27:11 -05:00
Leonardo de Moura	69be5f6c94	feat(kernel/environment): track which modules were already imported ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-17 18:15:44 -08:00
Leonardo de Moura	590b14570f	feat(lua): improve error handling in Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 18:21:42 -08:00
Leonardo de Moura	390f7eaec8	test(kernel/typechecker): type checker ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-16 15:01:39 -08:00
Leonardo de Moura	9398ea5a59	feat(util/shared_mutex): add support for recursive lock at shared_mutex ... We need support for recursive locks. The main user of this class is the environment object. This commit adds a test that demonstrates that the shared_lock of the environment object may be recursively requested. Before this fix, the Lean was deadlocking in this example. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 22:01:11 -08:00
Leonardo de Moura	209a2d10f7	fix(lua): replace std::mutex with std::recursive_mutex, add test that demonstrates the problem that is being fixed ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 21:26:16 -08:00
Leonardo de Moura	8525e8534b	feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-15 16:11:26 -08:00
Leonardo de Moura	45858d54ae	test(frontends/lean): add missing expected output ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 15:51:47 -08:00
Leonardo de Moura	6b30ebab5e	test(lua): use simplified Const creation ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 15:17:00 -08:00
Leonardo de Moura	09bed4786c	feat(lua): add semantic attachments for builtin arithmetical values to Lua API, improve mk_constant ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-14 15:15:04 -08:00
Leonardo de Moura	c759fc93f7	test(lua): object Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 20:59:28 -08:00
Leonardo de Moura	ed3cf8152b	feat(lua): add for_each to expr Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 16:30:59 -08:00
Leonardo de Moura	3dea7ae0d6	test(frontends/lean): example mixing Lean and Lua ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 16:07:15 -08:00
Leonardo de Moura	8c52d47692	chore(lua): rename env() to get_env() ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-13 13:58:51 -08:00
Leonardo de Moura	be093ecf90	feat(lua): use formatter available in the state object to convert Lean objects into strings in the Lua API ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 16:56:30 -08:00
Leonardo de Moura	9a5f86fce6	feat(lua): use (** ... **) instead of {{ ... }} for nested Lua scripts ... The token }} is a bad delimiter for blocks of Lua script code nested in Lean files. The problem is that the sequence }} occurs very often in Lua code because Lua uses { and } to build tables/lists/arrays. Here is an example of Lua code that contains the sequence }} t = {{1, 2}, {2, 3}, {3, 4}} In Lean, (* ... *) is used to create comments. Thus, (** ... **) code blocks will not affect valid Lean files. It also looks reasonably good. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 16:05:49 -08:00
Leonardo de Moura	8190d4fed5	feat(lua): allow Lua scripts to update 'global' options ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-12 15:38:00 -08:00
Leonardo de Moura	8c140ff86f	feat(lua): allow lua scripts (embedded in Lean files) to access the environment ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-10 11:14:04 -08:00
Leonardo de Moura	57b9657bf0	feat(lua): add lua_exception for wrapping lua errors, and improve Lua error messages in the Lean frontend ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 15:19:26 -08:00
Leonardo de Moura	a9b2be0b9c	feat(frontends/lean): add support for embedded Lua scripts in Lean files ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 13:56:04 -08:00
Leonardo de Moura	9c60eed93c	refactor(kernel/metavar): avoid using unique names for default metavariable prefix ... The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file. Avoiding unique name feature in the default metavariable prefix avoids this problem. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-07 10:16:25 -08:00
Leonardo de Moura	bf998d8661	feat(frontends/lean/parser): allow 'typeless' definitions, the type is inferred by the system ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-11-01 08:51:49 -07:00
Leonardo de Moura	96dcd003c6	fix(frontends/lean/parser): associated position with 'type' placeholder ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-31 16:27:36 -07:00
Leonardo de Moura	aa99ac6618	feat(kernel/value): allow semantic attachments to use coercions when being pretty printed ... For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10". Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-30 11:42:26 -07:00
Leonardo de Moura	032f5cd7b3	feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-30 10:45:43 -07:00
Leonardo de Moura	bc92671ae4	fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 17:12:50 -07:00
Leonardo de Moura	e3228b1f5c	test(frontends/lean): add 'l = nil' test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 16:30:03 -07:00
Leonardo de Moura	4dd6cead83	refactor(equality): make homogeneous equality the default equality ... It was not a good idea to use heterogeneous equality as the default equality in Lean. It creates the following problems. - Heterogeneous equality does not propagate constraints in the elaborator. For example, suppose that l has type (List Int), then the expression l = nil will not propagate the type (List Int) to nil. - It is easy to write false. For example, suppose x has type Real, and the user writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce the coercion since x = 0 is a type correct expression. Homogeneous equality does not suffer from the problems above. We keep heterogeneous equality because it is useful for generating proof terms. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 16:20:06 -07:00
Leonardo de Moura	d0009d0242	feat(frontends/lean): make the first argument of if-expression implicit, add support for marking implicit arguments on builtin symbols (aka semantic attachments) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 15:53:50 -07:00
Leonardo de Moura	2d88922543	feat(frontends/lean/elaborator): solve easy overloads at preprocessing time ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 10:07:15 -07:00
Leonardo de Moura	7c8daf8974	fix(kernel/metavar): make sure the justification and substitution are always matching each other ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 02:39:52 -07:00
Leonardo de Moura	2c6d4d2225	fix(kernel/normalizer): do not apply substitutions in the normalizer ... It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-29 02:14:48 -07:00
Leonardo de Moura	dbefc91151	fix(kernel/metavar): add normalize assignment justification ... We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-27 11:02:34 -07:00
Leonardo de Moura	cb06d0a959	test(frontends/lean): add example showing higher order matching is working, and is useful ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 20:18:48 -07:00
Leonardo de Moura	02c22e509d	fix(tests/lean): remove obsolete comments ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 20:16:02 -07:00
Leonardo de Moura	250cf70410	test(frontends/lean): all 'bad' examples can be solved ... Move them to the main test directory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 20:12:58 -07:00
Leonardo de Moura	c1c1af4b98	fix(tests/lean): add parenthesis ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 20:04:50 -07:00
Leonardo de Moura	a5c3829d1b	feat(kernel): add unexpected_metavar_occurrence exception ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 19:56:44 -07:00
Leonardo de Moura	46b9b2114a	fix(tests/lean): adjust error messages in the expected output ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 19:27:26 -07:00
Leonardo de Moura	e55fb4f165	fix(tests/lean): adjust expected results, the new result is also acceptable ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 17:54:09 -07:00
Leonardo de Moura	d2f9c24d3c	fix(tests/lean): adjust tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 15:42:17 -07:00
Leonardo de Moura	a7f94b55db	fix(frontends/lean/elaborator): fix bugs and adjust tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-24 15:29:56 -07:00
Leonardo de Moura	29ad71f9fc	test(conversion): add more conversion tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-10-15 15:35:08 -07:00
Leonardo de Moura	99a163f11d	Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower' ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-16 19:32:28 -07:00
Leonardo de Moura	63e102055e	Move metavariables to the kernel. This is the first step for implementing the new elaborator. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-15 12:09:01 -07:00
Leonardo de Moura	4c67721d32	Fix test error on Cygwin ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-09 18:35:11 -07:00
Leonardo de Moura	d912c9cd09	Add more 'bad' examples ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-09 09:19:49 -07:00
Leonardo de Moura	0a08494f4d	Add another bad example for current elaborator ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 23:21:43 -07:00
Leonardo de Moura	2ca30571b4	Display the input term in the output of the Check command. It is useful to see the fully elaborated term. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 22:55:21 -07:00
Leonardo de Moura	59a589037e	Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 11:23:46 -07:00
Leonardo de Moura	df116f88e0	Improve pretty printer for Pi's ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-08 11:04:07 -07:00
Leonardo de Moura	6bb9fc859e	Add examples that demonstrate limitations of the current elaborator. The new design, we are working on, will be able to solve them. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-07 19:40:40 -07:00
Leonardo de Moura	b92bbeb83b	Add casting propagation and normalization ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 20:45:26 -07:00
Leonardo de Moura	c0c2f52087	Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 18:32:15 -07:00
Leonardo de Moura	b62816cc25	Fix problem with pretty printer. Add another test for elaborator ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 18:01:11 -07:00
Leonardo de Moura	edafd519e1	Add missing case to elaborator ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 17:43:08 -07:00
Leonardo de Moura	26bf7bcaac	Fix bug in the elaborator. Move character ' to class A ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 17:12:35 -07:00
Leonardo de Moura	8840b37258	Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 11:02:00 -07:00
Leonardo de Moura	2459c4ae7c	Add (optional) type to let declarations ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 10:06:26 -07:00
Leonardo de Moura	6da194334e	Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 08:48:12 -07:00
Leonardo de Moura	6f3b0c30fb	Add 'Variables' command. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 08:48:12 -07:00
Leonardo de Moura	3dc55c452c	Parse decimal values ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-06 08:48:12 -07:00
Leonardo de Moura	87d3961158	Improve elaborator error messages ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 16:36:58 -07:00
Leonardo de Moura	613d83cdf4	Improve application type mismatch errors. We also show the implicit arguments (not just their types) ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 16:36:58 -07:00
Leonardo de Moura	be7fa0932a	Add unicode name for the types: Nat, Int and Real ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 09:03:41 -07:00
Leonardo de Moura	e955c054ca	Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-04 08:30:04 -07:00
Leonardo de Moura	fc9e395818	Define absolute value function and notation for it. Add new example. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 20:39:54 -07:00
Leonardo de Moura	3992c4b8f9	Define divides, and add examples ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 20:18:20 -07:00
Leonardo de Moura	51422fe654	Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0' ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 17:24:05 -07:00
Leonardo de Moura	6f3fa63ccb	Add missing test ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 14:51:34 -07:00
Leonardo de Moura	a341643335	Fix unit tests for Windows ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 10:44:51 -07:00
Leonardo de Moura	544229e5d3	Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-03 10:11:45 -07:00
Leonardo de Moura	e031d7bc10	Improve error messages when overloads+coercions do not work ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 20:05:47 -07:00
Leonardo de Moura	fd44ec8d79	Improve application type mismatch error messages ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 18:28:12 -07:00
Leonardo de Moura	72188691de	Add hyperbolic functions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 17:28:43 -07:00
Leonardo de Moura	4eaba93591	Add trigonometric functions ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 17:03:02 -07:00
Leonardo de Moura	395513258e	Define mod and unary minus ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 16:31:44 -07:00
Leonardo de Moura	abc939382b	Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 13:20:00 -07:00
Leonardo de Moura	e218b92a9d	Modify verbose message for Set command ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 12:29:21 -07:00
Leonardo de Moura	0a67679afb	Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U. ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-02 12:24:29 -07:00
Leonardo de Moura	c97e669f0c	Add coercion support in the elaborator and pretty printer ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 19:09:07 -07:00
Leonardo de Moura	42be7a4989	Add coercion declarations ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 18:11:28 -07:00
Leonardo de Moura	d27680d7fc	Add support for overloads in the elaborator ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 14:54:02 -07:00
Leonardo de Moura	a3bbd9fbb5	Minimize use the colors in tests. The colors make the diff hard to read ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 10:34:57 -07:00
Leonardo de Moura	598daa40bc	Refactor elaborator for supporting overloads ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 10:24:10 -07:00
Leonardo de Moura	447bb6db0e	Make sure we have unlimited stack space for testing the scripts ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-09-01 07:58:58 -07:00
Leonardo de Moura	51640ecff8	Move files in examples directory to tests directory. They are not real examples ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 19:16:30 -07:00
Leonardo de Moura	a5adddaf14	Add more tests ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 18:46:18 -07:00
Leonardo de Moura	389f23f356	Add test script ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-08-31 18:31:39 -07:00