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