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