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

818 commits

Author SHA1 Message Date
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
d7cb1952ae feat(kernel): simplify choice_fn, and make its interface closer to the unifier_plugin interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 12:47:33 -07:00
Leonardo de Moura
b94ce412ae fix(library/unifier): non-termination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 10:32:01 -07:00
Leonardo de Moura
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
4cb5f97038 refactor(library/tactic): simplify tactic framework, no more proof builders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:11:19 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 11:37:46 -07:00
Leonardo de Moura
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
9fb8fd0e7b test(tests/lua): add simple tactic framework test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 18:51:55 -07:00
Leonardo de Moura
5524c6c3d8 refactor(library/tactic/proof_state): simplify proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 14:49:48 -07:00
Leonardo de Moura
aaa7960b75 refactor(library/tactic/goal): use local names for hypotheses 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 11:11:12 -07:00
Leonardo de Moura
e55b4bf86d fix(library/unifier): bug in flex_rigid case: binding imitation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 20:43:49 -07:00
Leonardo de Moura
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
1da4ed5d80 fix(tests/lua/test.sh): update old script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:47:07 -07:00
Leonardo de Moura
d027c90bd0 fix(tests/lua/tc_bug1): update test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 16:50:30 -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
2c0f596665 fix(library/choice): avoid assertion violation when Lua API is misused 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 12:14:38 -07:00
Leonardo de Moura
3169f8c126 feat(library): add mk_explicit/is_explicit procedures for '@'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 12:11:27 -07:00
Leonardo de Moura
d915f0cc32 refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 09:00:14 -07:00
Leonardo de Moura
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
7df397fe63 test(lua): add universe constraint unifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 14:19:02 -07:00
Leonardo de Moura
60c60c6cf5 feat(library/kernel_bindings): add mk_choice_cnstr to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 13:39:21 -07:00
Leonardo de Moura
2fa5b17592 feat(library/unifier): add unifier.max_steps unifier.use_exceptions options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 12:38:57 -07:00
Leonardo de Moura
7b188ea37e feat(library/unifier): implement flex-rigid case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 11:00:35 -07:00
Leonardo de Moura
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
c8a07dee53 feat(library/unifier): add unifier_plugin support, and unit test with plugin implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 16:27:04 -07:00
Leonardo de Moura
b936c4d860 test(lua): add type checker test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 14:13:30 -07:00
Leonardo de Moura
29a00c46d0 feat(library/unifier): add main loop and resolve_conflict 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 11:57:10 -07:00
Leonardo de Moura
644c387cfe refactor(kernel/constraint): rename: level constraints are also equality constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:50:47 -07:00
Leonardo de Moura
1c47bd4847 fix(kernel/converter): remove temporary workaround, and temporarily disable unit test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:39:22 -07:00
Leonardo de Moura
3953d4d122 feat(kernel/type_checker): add push/pop methods to type_checker, they control the cache, and allow the type checker to reuse results even when it is used inside of a backtracking search 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:58:05 -07:00
Leonardo de Moura
eca22edda3 fix(kernel/type_checker): restore type checker cache when a failure occurs, do not send constraints to add_cnstr_fn when a type checker failure occurrs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:00:32 -07:00
Leonardo de Moura
9c745057b4 feat(library/unifier): add unify_fn skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 20:08:39 -07:00
Leonardo de Moura
bf8f3318d8 feat(library): add unifier module skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 13:38:17 -07:00
Leonardo de Moura
37bee8c852 refactor(kernel/type_checker): simplify replace constraint_handler with closure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
67088b130e refactor(kernel/constraint): simplify constraint interface, and add choice constraint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
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
5c17411a86 fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 09:46:58 -07:00
Leonardo de Moura
bdab979e09 feat(frontends/lean): add inductive_cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 16:00:59 -07:00