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

2977 commits

Author SHA1 Message Date
Leonardo de Moura
9f3f42f6a5 feat(frontends/lean/server): add SET command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 14:40:46 -07:00
Leonardo de Moura
4bbabfe6d4 feat(shell/lean): add --permissive command line option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 14:01:59 -07:00
Soonho Kong
24220a5f9e feat(emacs): show synth information 2014-08-14 13:22:24 -07:00
Leonardo de Moura
8afd433f34 feat(frontends/lean/parser): allow parser to continue even if there are errors importing files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 11:28:44 -07:00
Leonardo de Moura
0d97fff280 feat(library/module): include name of corrupted .olean file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 11:28:44 -07:00
Leonardo de Moura
d1c645977d fix(frontends/lean/info_manager): add missing method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 11:28:44 -07:00
Soonho Kong
99e77db8ad feat(emacs/lean-flycheck): override flycheck-try-parse-error-with-pattern 
For lean-mode, we override flycheck-try-parse-error-with-pattern to
increase column number by 1. It uses defadvice.
 2014-08-14 11:21:09 -07:00
Leonardo de Moura
be8ee8b3c0 feat(frontends/lean): add information about synthesized placeholders, closes #39 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 10:37:24 -07:00
Leonardo de Moura
28b7d87f1f feat(frontends/lean/pp): pretty print numerals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 09:12:22 -07:00
Leonardo de Moura
ebbca0d613 perf(library/num): avoid exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 09:12:22 -07:00
Leonardo de Moura
19537b72ee feat(frontends/lean/elaborator): generate type information for placeholders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 09:12:22 -07:00
Soonho Kong
a0a73463cc feat(emacs/lean-server.el): add lean-server-{kill,restart}-process 
[skip ci]
 2014-08-14 08:56:46 -07:00
Soonho Kong
c19bcad845 fix(emacs): add and use lean-string-join 2014-08-14 08:42:52 -07:00
Leonardo de Moura
ced0ed0eca fix(emacs): add missing 'require' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 08:21:42 -07:00
Soonho Kong
243cf2abb0 feat(emacs): show overload information 2014-08-14 07:23:15 -07:00
Leonardo de Moura
75be034d3d fix(frontends/lean/server): crash when INFO is invoked before VISIT/LOAD 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-13 18:31:47 -07:00
Leonardo de Moura
d30854829d refactor(frontends/lean): rename elaborator_env to elaborator_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-13 17:06:48 -07:00
Soonho Kong
28d23390a6 feat(emacs): implement lean-show-type 2014-08-13 17:02:49 -07:00
Soonho Kong
d2ef577a14 feat(emacs/lean-flycheck): customize checker name and options 2014-08-13 15:07:12 -07:00
Soonho Kong
3cd381b0f7 fix(emacs): remove lean-get-this-if-true-or-that 2014-08-13 15:07:12 -07:00
Leonardo de Moura
e5a36467dd fix(frontends/lean/scanner): wrong column information produced by scanner 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-13 12:32:37 -07:00
Leonardo de Moura
631e2395a3 refactor(frontends/lean/elaborator): add elaborator_env class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 18:43:56 -07:00
Leonardo de Moura
2f48552f06 fix(frontends/lean/server): disable cache, when a definition is reused from the cache, we loose type information, fixes #35 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
2869d9059f feat(frontends/lean): change 'proof-qed' semantics: no backtracking 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
b32d801116 refactor(frontends/lean/elaborator): remove unnecessary field: m_subst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
c5aea3eba7 refactor(frontends/lean/elaborator): remove m_accumulated and eager metavariable instantiation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
60ab6d3bd8 feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
562926e7ad refactor(kernel/instantiate): add functions instantiate_value_univ_params and instantiate_type_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Soonho Kong
0ca0ccb77d feat(frontend/lean/server.cpp): add "-- BEGININFO" header 2014-08-12 17:29:58 -07:00
Leonardo de Moura
d47d326cef fix(library/unifier): bug in mk_imitiation_arg 
Remove bogus constraint
     cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax));
This constraint is incorrect because 'type' may contain local constants that are not in 'locals'.

We just rely on
   cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax));
When maux is assigned, the system will inforce that its type (which is based on maux_type) must be type correct

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-11 15:44:23 -07:00
Leonardo de Moura
cb8185f016 feat(frontends/lean): add '#erase_cache' command (for debugging purposes) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-11 13:55:29 -07:00
Leonardo de Moura
faf2795a7b feat(frontends/lean/server): add VISIT and CHECK commands 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-11 10:40:18 -07:00
Leonardo de Moura
71583ba9c8 feat(frontends/lean/server): use definitions_cache in the server object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 20:02:50 -07:00
Leonardo de Moura
34f0dedf46 feat(frontends/lean/server): add 'INSERT' and 'REMOVE' commands to lean 'server', make sure all commands use the same convention for numbering lines, update server.org 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 19:57:24 -07:00
Leonardo de Moura
f319d084d4 feat(library/Makefile.common): use new --cache/-c option at Makefile.common 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 11:20:08 -07:00
Leonardo de Moura
f896771987 refactor(library/tactic/expr_to_tactic): use annotations for implementing 'by' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 11:16:46 -07:00
Leonardo de Moura
9d4c073618 feat(frontends/lean): add option --cache 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 11:04:16 -07:00
Leonardo de Moura
21b151bc98 chore(shell/lean): rename shortname for --luahook option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 10:00:04 -07:00
Leonardo de Moura
dc503e6e3d feat(library): add definitions_cache datastructure for implementing .clean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 09:53:13 -07:00
Leonardo de Moura
19daefaec5 fix(util/script_state): weird crash with Lua 5.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 23:13:30 -07:00
Leonardo de Moura
8ad0949269 fix(kernel/environment): initialization problem on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 16:14:35 -07:00
Leonardo de Moura
ee9be2837b refactor(library/unifier): remove redundant code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 15:04:34 -07:00
Leonardo de Moura
4bcde576b8 perf(kernel/abstract): improve mk_binding performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 14:14:14 -07:00
Leonardo de Moura
4986226e41 fix(kernel/converter): missing delay_check case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 08:07:41 -07:00
Leonardo de Moura
0af55beb56 perf(library/unifier): improve flex_rigid performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 08:07:15 -07:00
Leonardo de Moura
9d13f634f3 refactor(library/unifier): group flex_rigid case related methods in a functional object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-08 16:44:59 -07:00
Leonardo de Moura
49070895d1 perf(library/unifier): improve 'assign' method, keep old version 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 22:29:56 -07:00
Leonardo de Moura
24e8dca014 feat(library/explicit): allow 'as-is', 'explicit' and 'implicit' annotations to be saved in .olean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 19:13:48 -07:00
Leonardo de Moura
969afa8245 perf(library/unifier): improve check_imitation performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 18:28:23 -07:00
Leonardo de Moura
70c0eda9fc feat(frontends/lean): make sure all scopes are closed in the end of the module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 17:08:59 -07:00
Leonardo de Moura
1a67e69678 feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:59:08 -07:00
Leonardo de Moura
2486c483cf chore(kernel/error_msgs): change type mismatch error messages, closes #33 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:18:40 -07:00
Leonardo de Moura
9e6c5695be fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:09:45 -07:00
Soonho Kong
88ef5d68f9 feat(emacs): add lean-flycheck-turn-on/off/toggle 2014-08-07 14:03:08 -07:00
Soonho Kong
b684af5cdb feat(emacs): provide an option to disable lean-flycheck 2014-08-07 14:03:08 -07:00
Soonho Kong
209ecfd792 feat(emacs/lean-setting.el): add lean-rule-color custom-var 2014-08-07 14:03:08 -07:00
Soonho Kong
b6b40bb4ab feat(emacs): use optional package when required 2014-08-07 11:59:59 -07:00
Soonho Kong
5ecc872278 fix(emacs): use cl-case, require cl-lib 2014-08-07 11:59:59 -07:00
Soonho Kong
07e188acdb feat(emacs/README.md): add instr. for MELPA; add whitespace-cleanup-mode 2014-08-07 11:59:59 -07:00
Soonho Kong
a2867b3d06 feat(emacs/README.md): add README.md 2014-08-07 09:59:15 -07:00
Soonho Kong
f523c25c52 feat(emacs/lean-mode.el): use whitespace-cleanup-mode to fci-mode 2014-08-07 09:59:15 -07:00
Soonho Kong
f9f8c09143 refactor(emacs/lean-mode.el): clean up, add license 2014-08-07 09:59:15 -07:00
Soonho Kong
61f3897b0d feat(emacs/lean-util.el): add lean-util.el 2014-08-07 09:59:15 -07:00
Soonho Kong
164eab5574 feat(emacs/lean-settings.el): add customization-settings file 2014-08-07 09:59:15 -07:00
Soonho Kong
977ccc4631 feat(emacs/lean-flycheck.el): add lean-flycheck.el 2014-08-07 09:59:15 -07:00
Leonardo de Moura
9a6df02683 fix(util/name): avoid assertion violation when reading numeric names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 08:32:43 -07:00
Leonardo de Moura
6d6c62461f chore(library/kernel_serializer): add assertions for invalid uses of anonymous names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 08:32:32 -07:00
Leonardo de Moura
955d7d2659 fix(library/aliases): namespace and constant have the same name, and 'using' produces the 'empty' alias 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 08:32:21 -07:00
Leonardo de Moura
4ad7e709aa feat(frontends/lean): default for inductive types, closes #32 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 07:52:37 -07:00
Leonardo de Moura
b56233cbe3 fix(frontends/lean): make sure typing information is sorted, make sure the error messages contains line file name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 23:15:05 -07:00
Leonardo de Moura
c6f3232f81 feat(frontends/lean): provide 'partial' type information even when there are type errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 21:56:57 -07:00
Leonardo de Moura
1cbf40a5d2 fix(frontends/lean): remove duplicate info entries, fix bug in save_overload 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 21:23:37 -07:00
Leonardo de Moura
0af4a67881 feat(frontends/lean): save type information after elaboration, remove --flyinfo option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:35:26 -07:00
Leonardo de Moura
0276f4c1c0 feat(frontends/lean): store 'overload' information, remove #setline 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:13:09 -07:00
Leonardo de Moura
1ba9a92df2 feat(frontends/lean/parser): save snapshots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 18:31:53 -07:00
Leonardo de Moura
9b765a2a06 chore(frontends/lean): fix style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 18:10:33 -07:00
Leonardo de Moura
1a725574b1 refactor(frontends/lean): add 'server' module as a replacement for 'interactive' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 18:07:04 -07:00
Leonardo de Moura
2c3737bcc6 feat(frontends/lean): add info_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 15:25:28 -07:00
Leonardo de Moura
da616f69ea perf(library/unifier): do not explore branches that will trigger type errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 20:16:16 -07:00
Leonardo de Moura
bbc4380a52 fix(library/unifier): bug exposed by recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 19:02:30 -07:00
Leonardo de Moura
069f217215 fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 17:21:21 -07:00
Leonardo de Moura
d14cbfd7e9 refactor(frontends/lean/elaborator): local context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 16:25:54 -07:00
Leonardo de Moura
9cc2015caa feat(library/unifier): better error message for invalid local context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 16:25:22 -07:00
Leonardo de Moura
d1924097d5 feat(library/match): add 'local' backtracking 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51 feat(library/match): add basic match_plugin that just invokes whnf before failing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 08:37:03 -07:00
Leonardo de Moura
56d151ef7f feat(frontends/lean): 'partial' aliases. closes #24 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 22:08:10 -07:00
Leonardo de Moura
f4031b620f feat(library/match): extend match_plugin interface, and allow them to recursively invoke the matcher 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 18:30:30 -07:00
Leonardo de Moura
c34c2f4f5c feat(library/match): match universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 18:30:30 -07:00
Leonardo de Moura
b0a5ff7f93 refactor(library): rename hop_match to match 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 18:30:30 -07:00
Leonardo de Moura
0d5e346143 fix(library/expr_lt): make sure the builtin order is AC-compatible 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 15:51:10 -07:00
Leonardo de Moura
b9fadeb86e fix(util/realpath): realpath on cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 15:06:08 -07:00
Leonardo de Moura
5755ce4bfc fix(util/lean_path): use unix style paths when using cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 14:45:23 -07:00
Leonardo de Moura
53c7124c2b fix(util/realpath): rename realpath to lrealpath 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 14:42:44 -07:00
Leonardo de Moura
bc4cef9ecb feat(build): clean-olean target deletes .olean and .d files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 14:01:13 -07:00
Leonardo de Moura
59f6cb5962 fix(build): delete incorrect/old .d and .olean files, detect errors when generating .d files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:48 -07:00
Leonardo de Moura
d5bb7d45ec fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Leonardo de Moura
552be37d48 feat(library/hop_match): port higher-order (pattern) matcher to Lean 0.2, we still have to implement support for universe levels 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 16:03:58 -07:00
Leonardo de Moura
2dca68e645 chore(util/list): add inline functions for commonly used patterns in list processing code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 13:51:38 -07:00
Leonardo de Moura
5611c6a0a0 chore(util/lean_path): workaround 'spurious' warning produced by g++ in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 13:28:05 -07:00
Leonardo de Moura
50b0c17092 feat(library/unifier): add more information in error messages due to type errors when assigning metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 09:49:30 -07:00