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

3325 commits

Author SHA1 Message Date
Leonardo de Moura
edcbe6fe10 feat(frontends/lean): allow multiple coercions from class A to B, closes #187 
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-14 12:59:43 -07:00
Leonardo de Moura
1b6d4460e9 chore(library/coercion): cleanup 2014-09-14 12:59:43 -07:00
Soonho Kong
765d9b032f feat(src/cmake/modules/CleanOlean.cmake): add CleanOlean.cmake 
Instead of using 'find -delete', use CMAKE's FILE GLOB_RECURSE and FILE
REMOVE to implement clean-olean.

Related issue: #166
 2014-09-14 01:40:21 -07:00
Soonho Kong
2d29d6d319 feat(emacs/lean-company): auto-completion for import 
Close #126
 2014-09-14 00:00:25 -07:00
Soonho Kong
bf9ff192ca chore(emacs/README.md): add 'f' as a required package for lean-mode 2014-09-13 23:35:38 -07:00
Leonardo de Moura
d647954f93 feat(frontends/lean/elaborator): constraints associated with 'proof-qed' 
blocks are solved independently, closes #82
 2014-09-13 10:21:10 -07:00
Leonardo de Moura
8c8c9d1c4a feat(frontends/lean/elaborator): cleanup and remove unnecessary code 2014-09-12 17:55:27 -07:00
Leonardo de Moura
0c50517058 refactor(frontends/lean/elaborator): do not save/restore cache 2014-09-12 17:39:11 -07:00
Leonardo de Moura
6db46e0505 fix(frontends/lean/server): std::unordered_map::insert does replace 
existing entry, fixes #188
 2014-09-12 16:50:06 -07:00
Leonardo de Moura
b7023ce1d8 fix(frontends/lean/placeholder_elaborator): do not truncate stream of 
solutions during class-instance resolution, closes #183

For example, in theorem inverse_unique at category.lean, implicit
arguments are synthesized for inverse_compose. The first solution H' is
not good, and produces a type incorrect solution
 2014-09-12 16:12:23 -07:00
Leonardo de Moura
b482f27543 fix(util/lazy_list): bug in filter operation 2014-09-12 16:12:23 -07:00
Leonardo de Moura
b7dcb8f833 fix(frontends/lean/elaborator): remove annotation left-over 2014-09-12 16:12:23 -07:00
Soonho Kong
563cfa73ec feat(emacs/lean-changes): handle before/after-revert 2014-09-12 14:25:08 -07:00
Soonho Kong
27ae03878c refactor(emacs/lean-server): rename flush-changed-lines to server-flush-changed-lines 2014-09-12 14:25:08 -07:00
Soonho Kong
c034c54f50 refactor(emacs/debug): rename lean-server-debug to lean-debug 2014-09-12 14:25:08 -07:00
Leonardo de Moura
029acbd1df feat(library/coercion): better support for coercions to function-class. closes #185 2014-09-12 13:17:20 -07:00
Leonardo de Moura
62585f1c56 fix(library/coercion): remove spurious '\n' 2014-09-12 13:08:47 -07:00
Leonardo de Moura
a2e36e97f2 fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes #186 2014-09-12 12:13:29 -07:00
Leonardo de Moura
010ecebfea feat(frontends/lean): add proof-qed expression 
Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.
 2014-09-11 18:14:49 -07:00
Leonardo de Moura
7ffe73b8ca fix(frontends/lean): name clash inside section, fixes #181 2014-09-11 16:37:23 -07:00
Leonardo de Moura
85f7132efe feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175, closes #173, closes #68 2014-09-11 14:49:35 -07:00
Leonardo de Moura
03902d4b45 refactor(library/unifier): add option m_discard too unifier, if m_discard == false, then unsolved flex-flex constraints are returned, the unifier also does not apply "last resource" techniques that may miss many solutions. 2014-09-11 14:49:35 -07:00
Leonardo de Moura
935ba35292 feat(library/unifier): keep normalization result when processing universe level unification constraints 2014-09-11 14:49:35 -07:00
Leonardo de Moura
c7c35becb2 feat(library/io_state): add default constructor to io_state 2014-09-11 14:49:35 -07:00
Leonardo de Moura
80fd14b39e refactor(frontends/lean): replace collect_metavars with metavar_closure helper class 2014-09-11 14:49:35 -07:00
Soonho Kong
b31edb2cee fix(emacs/lean-company): pass dummy continuation for WAIT 2014-09-11 13:46:07 -07:00
Soonho Kong
0b507777f9 fix(emacs/lean-company): repaint background in the candidate only when required 2014-09-11 13:44:54 -07:00
Soonho Kong
389fe02597 fix(emacs/lean-server): handle modified buffer only when process start 2014-09-11 12:40:10 -07:00
Soonho Kong
733c0e4a77 chore(emacs/lean-server): make trace-mode and debug-mode non-local vars 2014-09-11 12:34:23 -07:00
Soonho Kong
89f38b3945 test(emacs/features): add ecukes template 2014-09-11 12:33:49 -07:00
Soonho Kong
2ba43f1432 refactor(emacs): move tests in *.el files to 'test' directory 2014-09-11 12:29:32 -07:00
Soonho Kong
45b7327d63 doc(emacs/README.md): add contribution section 2014-09-11 12:29:00 -07:00
Soonho Kong
c879b2ce6d chore(emacs/Cask): add ert-runner, ecukes 2014-09-11 11:12:05 -07:00
Soonho Kong
4b556a41ed feat(emacs/lean-server): async task queue holds type of cmds as well 2014-09-11 04:09:21 -07:00
Soonho Kong
565402f3d6 feat(lean-server): handle signals (error/quit) in continuations 
Related with #158
 2014-09-11 04:07:50 -07:00
Soonho Kong
5b28480809 chore(emacs/lean-server): send signal info to lean-server-trace 2014-09-11 04:04:20 -07:00
Soonho Kong
92f8a22ea1 fix(emacs/lean-company): send dummy continuation when send wait 2014-09-11 04:03:23 -07:00
Leonardo de Moura
1e5ba9bd75 refactor(frontends/lean/elaborator): move coercion_elaborator to its own module 2014-09-10 16:42:49 -07:00
Leonardo de Moura
6bc41f8dde refactor(frontends/lean/elaborator): move placeholder_elaborator to its own module 2014-09-10 16:42:49 -07:00
Leonardo de Moura
9ce356e515 refactor(frontends/lean/local_context): do not use references in the local context 2014-09-10 16:42:49 -07:00
Soonho Kong
63c0510a05 feat(emacs/lean-tags): detect and support multiple TAGS 
Close #170
 2014-09-10 16:38:36 -07:00
Soonho Kong
1ea8b66a39 fix(emacs/lean-company): enable auto-complete when prefix length >= 1 
[skip ci]
 2014-09-10 16:21:44 -07:00
Soonho Kong
1c5497e632 feat(emacs/lean-project): add lean-project-create to imenu 
Related with #170
 2014-09-10 15:19:11 -07:00
Soonho Kong
b05ca1db0f fix(emacs/lean-tags): handle exceptions from find-tag 2014-09-10 14:14:42 -07:00
Soonho Kong
b51e8dd1b9 fix(emacs/lean-server): respect order of messages in check-buffer-and-partition 2014-09-10 14:14:42 -07:00
Soonho Kong
7c4debd1d1 feat(emacs/lean-server): handle modified buffer when send VISIT cmd 
Close #159
 2014-09-10 14:14:42 -07:00
Leonardo de Moura
669b1bff45 refactor(frontends/lean/elaborator): rename choice_elaborator to choice_iterator and move to separate module 2014-09-10 11:20:16 -07:00
Leonardo de Moura
e128610711 chore(tests): use option -t 100000 to speedup tests 2014-09-10 11:20:16 -07:00
Leonardo de Moura
4a4de27a6c refactor(frontends/lean/elaborator): move local_context to separate file 2014-09-10 11:20:16 -07:00
Leonardo de Moura
4ea322febc chore(frontends/lean/elaborator): minor cleanup 2014-09-10 11:20:16 -07:00
Soonho Kong
cab1811927 feat(emacs/lean-server): print out signal event to debug buffer 2014-09-10 09:07:16 -07:00
Leonardo de Moura
b82092a123 fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172 2014-09-10 08:39:39 -07:00
Soonho Kong
8fd938e142 fix(util/lean_path.cpp): get_exe_location follows symbolic link in OSX 
Previously, we had different behaviors on Linux and OSX when
get_exe_location finds a location of executable:

 - Linux: follow symbolic link
 - OSX: not follow symbolic link
 2014-09-10 07:41:14 -07:00
Leonardo de Moura
570879b55f feat(frontends/lean): add declaration to namespace without opening it, closes #161 2014-09-09 18:02:14 -07:00
Leonardo de Moura
e856a268a2 fix(frontends/lean): OVERLOAD info for overloaded notation, fixes #132 2014-09-09 17:44:19 -07:00
Leonardo de Moura
c92a9b8808 fix(frontends/lean/class): take whnf into account in add_instance 2014-09-09 16:09:05 -07:00
Leonardo de Moura
38058450d4 fix(frontends/lean/elaborator): whnf may produce assertion violation if term contains free variables 2014-09-09 16:09:05 -07:00
Soonho Kong
27fa0d0ae3 doc(emacs/README.md): update required/optional packages 2014-09-09 15:11:58 -07:00
Soonho Kong
60d14b50ab feat(emacs/lean-require): check lean-mode dependencies in initialization 
Close #91
 2014-09-09 15:11:57 -07:00
Soonho Kong
961dccf279 feat(emacs/Cask): add Cask file 
Close #92
 2014-09-09 15:11:57 -07:00
Leonardo de Moura
47e02342bb feat(frontends/lean/elaborator): use whnf in class-instance resolution, closes #160 2014-09-09 15:04:44 -07:00
Leonardo de Moura
bd1bc336fb feat(library/coercion): add simple trick for defining coercions to function-class in a convenient way, closes #31 2014-09-09 14:36:36 -07:00
Leonardo de Moura
abdd784729 feat(shell): start 'lean --server' with 'pp.beta = true' 2014-09-09 14:13:35 -07:00
Leonardo de Moura
2d94584816 feat(frontends/lean/pp): add 'pp.beta' option, closes #154 2014-09-09 14:10:20 -07:00
Leonardo de Moura
65000fa653 feat(library/coercion): rename class to 'coercions' 2014-09-09 14:03:45 -07:00
Soonho Kong
ba6dc59d5f fix(emacs/lean-server): missing 'rx' at the beginning of regex 2014-09-09 13:47:09 -07:00
Soonho Kong
70dcc2e122 fix(emacs): use looking-at instead of char-after 2014-09-09 13:22:58 -07:00
Soonho Kong
85bd112a37 fix(emacs/lean-company): color problem when showing auto-complete candidates 2014-09-09 13:22:58 -07:00
Soonho Kong
c26f39b86e feat(emacs/lean-company): "c-u TAB" asks filter for FINDG 2014-09-09 13:22:58 -07:00
Leonardo de Moura
ee196bbf1a fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151 2014-09-09 12:49:32 -07:00
Leonardo de Moura
d8caa294b5 fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-09 11:02:54 -07:00
Leonardo de Moura
0505be2aca feat(frontends/lean/server): unifier maximum number of steps error in FINDG, closes #155 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-09 10:36:41 -07:00
Leonardo de Moura
53292d8297 feat(frontends/lean/server): add timebound to WAIT command, closes #156 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-09 10:28:47 -07:00
Leonardo de Moura
187661aa6a feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs 2014-09-09 09:27:26 -07:00
Leonardo de Moura
a5698a55ec fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions 2014-09-09 09:27:26 -07:00
Leonardo de Moura
fd85d4702e refactor(library/unifier): move all_local outside of the class 2014-09-09 09:27:26 -07:00
Leonardo de Moura
ebde1bcfad feat(library/unifier): option 'unifier.computation true' will force elaborator to always consider an extra case-split when the right-hand-side of a flex-rigid constraint is not in weak-head-normal-form 2014-09-09 09:27:26 -07:00
Leonardo de Moura
d9afb3ca96 fix(frontends/lean/elaborator): missing constraint 2014-09-09 09:27:26 -07:00
Leonardo de Moura
4088cdc139 chore(frontend/lean/pp_options): use consistent name convention for pp option names 2014-09-09 09:27:26 -07:00
Soonho Kong
b460c02017 feat(emacs/lean-mode): add imenu support 
Close #97
 2014-09-09 09:04:31 -07:00
Soonho Kong
4eb8a9b192 feat(emacs/lean-flycheck): "real" .clean file instead of "flycheck_real.clean" 
Fix #140
 2014-09-08 23:49:02 -07:00
Soonho Kong
a9be084b1c feat(emacs/lean-settings): add lean-flycheck-pp-width and lean-flycheck-max-messages-to-display 2014-09-08 18:44:22 -07:00
Soonho Kong
3682ca32d2 feat(emacs/lean-company): call FINDG if cursor is at "_" 2014-09-08 16:04:20 -07:00
Soonho Kong
4f604544c4 feat(emacs/lean-cmd): add WAIT command 2014-09-08 16:04:19 -07:00
Soonho Kong
c88bfc0c02 chore(frontends/lean/server.cpp): add BEGIN/END for WAIT command 2014-09-08 16:04:19 -07:00
Soonho Kong
bc640510aa feat(emacs/lean-cmd): add FINDG cmd 2014-09-08 16:04:19 -07:00
Soonho Kong
0ac1ec1de3 feat(emacs/lean-settings): add lean-show-only-type-in-parens 
Fix #135
 2014-09-08 11:39:40 -07:00
Soonho Kong
a40894a712 fix(emacs/lean-tags): pass lean-flycheck-checker-options properly 
Fix #153
 2014-09-08 11:27:04 -07:00
Soonho Kong
c365f6b9ab fix(emacs/lean-company): only activate auto-completion when TAB is pressed 2014-09-08 10:52:22 -07:00
Soonho Kong
6c483467dd feat(emacs/lean-company): replace ?M in AC candidate with M and colorize 
close #149
 2014-09-08 09:47:51 -07:00
Leonardo de Moura
11addbb594 fix(frontend/lean/server): auto completion doesn't use prefix, fixes #147 2014-09-08 08:04:04 -07:00
Leonardo de Moura
b4793df653 feat(frontends/lean): rename '[fact]' to '[visible]' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-08 07:47:42 -07:00
Leonardo de Moura
cbdfb0dcdc feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77 2014-09-07 19:59:34 -07:00
Leonardo de Moura
2631979f5c fix(library/scoped_ext): section/context should not affect namespace 2014-09-07 19:59:34 -07:00
Soonho Kong
5c89e70a23 fix(emacs/lean-server): use process-query-on-exit-flag to kill 
lean-server automatically on exit

To fix a problem mentioned in #147
 2014-09-07 22:29:09 -04:00
Leonardo de Moura
da701eb6de fix(frontends/lean/elaborator): bug in recent change 2014-09-07 19:08:31 -07:00
Soonho Kong
fc2fbc41bb chore(emacs/lean-info): fix a bug passing a wrong argument 2014-09-07 18:44:11 -07:00
Leonardo de Moura
fea516af24 feat(frontends/lean/elaborator): allow Pi/forall local instances 2014-09-07 18:16:33 -07:00
Leonardo de Moura
c378a58cc2 feat(frontends/lean): add [class] modifier for inductive datatypes as a shortcut for 'class' command. 2014-09-07 18:16:33 -07:00
Soonho Kong
ba35ca5300 feat(emacs/lean-company): add company-lean--need-autocomplete 
This one partially addresses #150.
 2014-09-07 17:32:06 -07:00