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
Leonardo de Moura
3310eb3dfc
feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-07 12:29:32 -07:00
Soonho Kong
6b5e67e063
fix(emacs/lean-info): fix eldoc-error at end of buffer
2014-09-07 11:40:28 -07:00
Leonardo de Moura
6d2df80a17
feat(frontends/lean/server): use '?a' instead of '?M_i' for implicit arguments when displaying FINDP and FINDG matches
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-07 09:36:03 -07:00
Leonardo de Moura
1bc31d7df0
feat(frontends/lean/server): instantiate implicit arguments with metavariables when generating FINDP and FINDG output
2014-09-06 13:17:26 -07:00
Leonardo de Moura
87d7391d7a
fix(frontends/lean/server): do not fail if file does not exist in 'VISIT file'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 12:34:20 -07:00
Leonardo de Moura
5549295c47
fix(frontends/lean/inductive_cmd): bug when elaborating inductive tyoe parameters
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:38:32 -07:00
Leonardo de Moura
bbff564a1c
feat(frontends/lean): persistent notation in sections
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:14:20 -07:00
Leonardo de Moura
d6491399b9
fix(emacs/lean-syntax): weird syntax-hightlight problem"
2014-09-06 10:49:16 -07:00
Soonho Kong
6b5831d894
feat(emacs/lean-info): show extra-type info for expr in parens
...
Close #135
2014-09-06 09:26:11 -07:00
Soonho Kong
d793b09c0f
feat(emacs/lean-cmd): extend info to have column-number
2014-09-06 09:26:11 -07:00
Leonardo de Moura
3bbbd43b03
chore(emacs): minor adjustments to synthax hightlight and input mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 08:32:05 -07:00
Soonho Kong
303b86e165
refactor(emacs/lean-flycheck): clean up unused code
2014-09-05 23:08:19 -07:00
Soonho Kong
0476591992
fix(emacs/lean-company): override company--window-width
...
Override 'company--window-width' to be 0.95 * window-body-width.
This partially solves the problem of issue #137 .
2014-09-05 23:08:19 -07:00
Soonho Kong
bd17d07ebc
fix(emacs/lean-server): limit the number of NAY retries
...
Also, only retry when there is no continuation other than the current
one.
2014-09-05 23:08:19 -07:00
Leonardo de Moura
bdb91f6783
feat(frontends/lean/server): give preference to prefix matches
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 21:57:35 -07:00
Leonardo de Moura
629feb77ef
feat(frontends/lean/server): ingore keywords and commands in FINDP
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 20:59:14 -07:00
Leonardo de Moura
b5f595c432
fix(frontends/lean/inductive_cmd): bugs when declarating inductive datatypes in sections, fixes #141 , fixes #142
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 19:17:09 -07:00
Soonho Kong
e4a687c5ea
fix(emacs/lean-tags): use the same linja option for tags-gen and flycheck
2014-09-05 19:11:49 -07:00
Leonardo de Moura
8610330cc4
chore(emacs/lean-syntax): highlight 'import/section/end/namespace/open' arguments
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 18:38:41 -07:00
Leonardo de Moura
d48dbccb00
fix(shell): allow multiple spaces after -D option
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 18:07:54 -07:00
Leonardo de Moura
a8361f128f
feat(frontends/lean/server): sort fuzzy matches by number of errors
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 18:03:04 -07:00
Leonardo de Moura
f1436d78ca
feat(frontends/lean/server): using fuzzy matching
2014-09-05 18:01:18 -07:00
Leonardo de Moura
a31a25798c
feat(util): add fuzzy string search procedure
2014-09-05 18:01:09 -07:00
Soonho Kong
f958e534bd
feat(emacs/lean-settings): pass 'pp.width' to lean via linja
...
Close #28
2014-09-05 16:35:01 -07:00
Soonho Kong
50f16ad591
feat(emacs/lean-flycheck): delete flycheck temporaries after check
...
Close #140
2014-09-05 16:09:45 -07:00
Soonho Kong
a1e00bb216
refactor(emacs/lean-server): restructure async queue handling routine
2014-09-05 16:09:45 -07:00
Soonho Kong
a72df90022
feat(emacs/lean-server): add debug-mode, trace-mode
2014-09-05 15:33:59 -07:00
Soonho Kong
70ac5ec15e
feat(emacs/README.md): add instruction for unicode font
2014-09-05 15:33:59 -07:00
Soonho Kong
e77966932d
feat(emacs/lean-server): scroll debug buffer
2014-09-05 15:33:59 -07:00
Soonho Kong
db60a56056
feat(emacs/lean-company): truncate string if it's longer than 90% of window-width
...
Also add "..." in the end
Close #137
2014-09-05 08:49:05 -07:00
Soonho Kong
3b574ef31d
feat(emacs/lean-server): kill the server before emacs exit
...
Close #138
2014-09-05 07:49:19 -07:00
Soonho Kong
37e514e114
feat(emacs/lean-tags): block emacs until ltags finishes
2014-09-05 06:59:02 -07:00
Soonho Kong
fc364566bf
feat(emacs/lean-company): truncate type info in auto-complete
...
Close #137
2014-09-05 06:59:02 -07:00
Soonho Kong
64bae94d3a
fix(emacs/lean-company): enable auto-complete if prefix has '.' or '_'
2014-09-05 06:59:02 -07:00
Soonho Kong
3ba4e553fe
refactor(emacs/lean-server): clean up
2014-09-05 06:59:01 -07:00
Leonardo de Moura
898021c1b8
fix(frontends/lean/server): cleanup info in modified line
2014-09-05 01:36:17 -07:00
Leonardo de Moura
613c035ff8
fix(frontends/lean): missing pre_info for type incorrect declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 01:12:08 -07:00
Leonardo de Moura
5fa1c0a5fb
feat(frontends/lean/server): take current namespace into account when processing FINDP command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 00:40:34 -07:00
Leonardo de Moura
6632a50015
refactor(library): add namespaces 'or', 'and' and 'iff'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 21:25:21 -07:00
Leonardo de Moura
364bba2129
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Soonho Kong
0652198eca
feat(emacs/lean-server): add sync/async send-cmd
2014-09-04 16:32:08 -07:00
Soonho Kong
cc89cd051a
feat(emacs/lean-company): add lean-company
2014-09-04 16:32:07 -07:00
Soonho Kong
e7f6228001
feat(emacs): use lean-server-send-cmd-async
2014-09-04 16:32:07 -07:00
Soonho Kong
677f4af801
feat(emacs/lean-server): add debug print
2014-09-04 16:32:07 -07:00
Soonho Kong
2fa8c1c709
chore(emacs/lean-info): fix indentation
2014-09-04 16:32:07 -07:00
Soonho Kong
cae2ab7dfb
feat(emacs/lean-cmd): add FINDP cmd
2014-09-04 16:32:07 -07:00
Leonardo de Moura
8743394627
refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
ffc871ea8c
feat(frontends/lean/server): only display 'EXTRA_TYPE' info when the column number is provided to the 'INFO' command, closes #133
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 14:02:53 -07:00
Leonardo de Moura
37c36e8b4e
feat(shell): add -D command line option for setting configuration options, closes #130
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 13:33:00 -07:00
Leonardo de Moura
d75a4739e4
refactor(util/name): move string_to_name to name module
2014-09-04 13:09:42 -07:00
Leonardo de Moura
b5b68613b1
feat(shell): remove '--server' command line option when compiling with -DMULTI_THREAD=OFF
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 12:43:14 -07:00
Leonardo de Moura
de8a71bc5b
perf(frontends/lean): do not create extra_info annotation when we are not collecting info
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 11:25:41 -07:00
Leonardo de Moura
d76218e9d1
fix(frontends/lean/elaborator): bug when elaborating expressions with multiple annotations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 11:23:58 -07:00
Leonardo de Moura
9876d07094
chore(frontends/lean): use consistent filename convention
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 09:59:24 -07:00
Leonardo de Moura
b94ec07b29
feat(frontends/lean): associate type information with left '('
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 09:56:27 -07:00
Leonardo de Moura
c532dcfaac
feat(library/declaration_index): add 'a|abbreviation-name|declaration-name' entries in .ilean files
2014-09-04 09:30:25 -07:00
Leonardo de Moura
d3ec5ccac1
refactor(library/declaration_index): store declarations in a map
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 07:42:18 -07:00
Leonardo de Moura
f9a90b9920
feat(frontends/lean): add 'export' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 18:37:01 -07:00
Leonardo de Moura
5e18e6609c
feat(frontends/lean): add 'as' clause to 'open' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 17:37:02 -07:00
Leonardo de Moura
e51c4ad2e9
feat(frontends/lean): rename 'using' command to 'open'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 16:00:38 -07:00
Leonardo de Moura
6a6f6ed439
feat(emacs/lean-syntax): add syntax-highlight for declaration modifiers
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 15:26:21 -07:00
Leonardo de Moura
e14814d4bf
feat(frontends/lean): add '[protected]' modifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 15:01:13 -07:00
Leonardo de Moura
5a203d1c75
feat(frontends/lean): add '?' for inspecting the type of any expression, it produces a EXTRA_TYPE info entry
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 11:54:42 -07:00
Leonardo de Moura
9702a66a29
feat(frontends/lean/server): use alias (if available) in FINDG command output
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 11:54:42 -07:00
Soonho Kong
327e3a58bf
fix(emacs/lean-info): print stale when info is available
...
fix #127
2014-09-03 10:28:37 -07:00
Soonho Kong
25a48be470
feat(emacs/lean-info): improve coercion display
...
close #124
2014-09-03 10:12:18 -07:00
Soonho Kong
fdc20800ca
chore(emacs/lean-server): clean up debugging message
2014-09-03 10:12:17 -07:00
Leonardo de Moura
ef1912eddf
feat(frontends/lean): improve COERCION info
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 09:34:13 -07:00
Leonardo de Moura
8c3d839968
feat(frontends/lean/server): add FINDG command (find declarations that can be used to fill a placeholder)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 08:57:57 -07:00
Leonardo de Moura
060093cbab
refactor(library): add type_util module, and move get_expect_num_args to it
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 08:40:03 -07:00
Soonho Kong
e802883b03
feat(emacs/lean-option): show the current value of an option
...
close #125
2014-09-03 08:09:41 -07:00
Soonho Kong
975841e53b
feat(emacs): use lexical scope for lean-info and lean-server
2014-09-03 00:54:42 -07:00
Soonho Kong
b25288545e
feat(emacs/lean-info): add coercion and stale in type info
...
Close #124
2014-09-03 00:50:31 -07:00
Soonho Kong
88410bf278
feat(emacs/lean-server): support SHOW and VALID
...
Implement lean-server-show and lean-server-valid functions.
Close #116
2014-09-03 00:50:31 -07:00
Soonho Kong
72e1dfa296
feat(emacs): implement non-blocking communication
...
The key idea is to pass a continuation function when we call
lean-server-send-cmd function. The passed continuation function is
called by lean-server-event-handler. Until the buffer is ready, the
event handler will be called in interval (lean-server-retry-time, 0.1
sec by default). When we have 'NAY' for INFO command, it will re-send
INFO commands to lean-server until we have one without 'NAY'.
Close #123
2014-09-03 00:50:31 -07:00
Soonho Kong
53390faebc
chore(emacs/lean-mode): remove lean-tab function
2014-09-03 00:50:31 -07:00
Leonardo de Moura
36674eb8d9
feat(frontends/lean/server): add NAY and STALE status to --BEGININFO
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 19:04:01 -07:00
Leonardo de Moura
974a0a4217
feat(frontends/lean/elaborator): generate COERCION info
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 18:39:06 -07:00
Leonardo de Moura
24fc89ff70
refactor(frontends/lean/server): move option display_value to option_declarations
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 17:42:21 -07:00
Leonardo de Moura
b8c34eceed
feat(frontends/lean/server): display current option value instead of default value
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 17:29:49 -07:00
Leonardo de Moura
40cd50b1ca
fix(frontends/lean/pp): add necessary '@' when pp.implicit is true, otherwise produced output will not even type check
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 17:11:26 -07:00
Leonardo de Moura
fc0f12101c
fix(frontends/lean/pp): bug when pretty printing arrows
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 15:55:14 -07:00
Soonho Kong
78437331c2
fix(emacs/lean-syntax.el): highlight "parameter (" properly
...
fix #122
2014-09-02 15:09:49 -07:00
Leonardo de Moura
0f9478d91e
feat(frontends/lean): add 'class' command back
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 15:04:23 -07:00
Soonho Kong
b05aeb112b
fix(emacs/lean-mode): Bind TAB with lean-tab-indent-or-compliete
2014-09-02 17:02:35 -04:00
Leonardo de Moura
bbdb13172e
feat(frontends/lean/server): add 'FINDP' command
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 12:59:48 -07:00
Soonho Kong
b4a80f83af
feat(emacs/lean-server): accept "BEGININFO .*" pattern
2014-09-02 10:37:03 -07:00
Soonho Kong
cec2f8e466
feat(emacs/lean-mmm-lua.el): add mmm-mode to syntax-highlight lua code
...
in lean-mode
Close #74
2014-09-02 10:37:03 -07:00
Soonho Kong
a08ad99dba
feat(emacs/lean-cmd): add lean-clear-cache
...
Close #99
2014-09-01 22:58:52 -07:00
Leonardo de Moura
87926b774f
fix(frontends/lean/info_manager): user provided options override saved options, fixes #119
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-01 18:44:43 -07:00
Soonho Kong
50465a2d06
feat(emacs/lean-option): provide candidates and validation for lean-set-option
...
Close #106
2014-09-01 18:31:12 -07:00
Soonho Kong
fc2cbbe216
chore(emacs/lean-mode): add package info
2014-09-01 18:28:15 -07:00
Soonho Kong
246d4224bc
feat(emacs/lean-tags): call "linja TAGS" to make TAGS
...
fix #117
2014-08-30 14:58:48 -07:00
Soonho Kong
26d548a069
feat(emacs/lean-mode): add lean-tab-indent-or-complete
...
Close #105
2014-08-30 14:57:34 -07:00
Soonho Kong
d393771d8a
feat(emacs/eri.el): add eri.el (from agda mode)
2014-08-30 14:57:34 -07:00
Leonardo de Moura
b7d7f12b8e
fix(frontends/lean/info_manager): several bugs: invalid flag was not being reset for empty lines, merge with overwrite=false was adding 'poluting' state, --NAY generation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-30 10:35:36 -07:00
Leonardo de Moura
658e0780a6
feat(util/rb_tree): add max (element) method
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-30 10:25:12 -07:00
Soonho Kong
a47dada27f
feat(emacs/lean-server): add 'SLEEP ms' for trace
2014-08-30 07:51:53 -07:00
Soonho Kong
ad1111cb21
feat(emacs/lean-server): add *lean-server-trace* buffer
...
Fix #115 .
2014-08-30 07:38:12 -07:00
Leonardo de Moura
231039ad26
chore(frontends/lean/inductive_cmd): add auxiliary assertion for debugging
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 22:28:22 -07:00
Soonho Kong
543fdf840e
fix(emacs/lean-mode): add comment-start "--"
...
fix #113
2014-08-29 20:12:22 -07:00
Leonardo de Moura
373bda0c74
fix(frontends/lean/server): in valid line tracking, add 'VALID' command similar to show, but marks invalid lines with a '*'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 18:17:07 -07:00
Leonardo de Moura
cb27407fcb
feat(frontends/lean): add SHOW and SLEEP debugging support commands, fixes worker interrupted bug, and LEAN_SERVER_DIAGNOSTIC compilation mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 18:17:07 -07:00
Soonho Kong
36c632f48d
doc(emacs/README.md): clean up
...
[skip ci]
2014-08-29 15:22:06 -07:00
Leonardo de Moura
9a4472cff5
fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 14:32:53 -07:00
Leonardo de Moura
5ebebb30a8
feat(shell): remove --permissive option, closes #107
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 13:26:07 -07:00
Leonardo de Moura
eeffb498b8
feat(frontends/lean/dependencies): send all missing files to standard error, closes #111
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 13:20:25 -07:00
Leonardo de Moura
d7da307f85
feat(frontends/lean/server): add 'OPTIONS' command to 'lean --server'
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 12:59:22 -07:00
Leonardo de Moura
bd3fb3489b
feat(frontends/lean/dependencies): do not stop computing dependencies at error, compute as many as possible, and sign error in the end
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 12:34:37 -07:00
Leonardo de Moura
3f50fd3ddd
feat(build): invoke linja from lean build
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 12:15:07 -07:00
Leonardo de Moura
b9489ce585
fix(frontends/let): let-expression pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 10:58:27 -07:00
Soonho Kong
e966aa3145
feat(emacs/lean-settings): use linja for flycheck
2014-08-29 10:31:16 -07:00
Leonardo de Moura
d8548369e7
feat(frontends/lean/pp): improve let-expr pretty printer
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-29 07:46:58 -07:00
Leonardo de Moura
2ce92feae1
fix(frontends/lean/pp): remove unreachable code: elaborator eliminates typed_expr macros
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 18:30:33 -07:00
Leonardo de Moura
be56fcf0bd
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 18:20:58 -07:00
Leonardo de Moura
662345e2af
fix(frontends/lean/elaborator): missing '\n' in error message
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 18:17:00 -07:00
Leonardo de Moura
b9628842cf
feat(library/unifier): remove mk_macro_imitation, we instead expand the macro before solving flex-rigid constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 17:34:03 -07:00
Leonardo de Moura
1e80a9dfe9
feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 16:27:52 -07:00
Leonardo de Moura
79acd3e1b7
fix(kernel/converter): missing case
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 15:21:57 -07:00
Leonardo de Moura
641624a277
fix(library/unifier): bug in expand_rhs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 14:35:11 -07:00
Leonardo de Moura
e303651dee
refactor(library/unifier): cleanup mk_macro_imitation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 13:19:19 -07:00
Leonardo de Moura
d9fa9f1039
feat(src/emacs/lean-syntax.el): add commonly used operators
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 13:03:22 -07:00
Leonardo de Moura
f98ab2a8ff
fix(src/emacs/lean-syntax.el): remove obsolete command set_opaque
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 11:16:29 -07:00
Leonardo de Moura
b3615d5c8b
fix(src/emacs): add 'begin' reserved keyword
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 09:33:09 -07:00
Leonardo de Moura
823a3a7c56
feat(frontends/lean/server): add ECHO command for debugging purposes
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 07:40:02 -07:00
Leonardo de Moura
1a8eb9799e
feat(frontends/lean/server): preserve info that occurs in columns before first changed column
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 21:09:52 -07:00
Leonardo de Moura
8df5fc0623
fix(frontends/lean/server): compilation warning
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 17:53:00 -07:00
Leonardo de Moura
8719dff361
fix(frontends/lean): distribute '@' over choice
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 16:31:18 -07:00
Leonardo de Moura
19c14fcca7
refactor(frontends/lean/server): refactor lean info server, closes #90 , closes #69
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 14:53:16 -07:00
Leonardo de Moura
c7e9e238ec
fix(frontends/lean/server): ignore output produced by worker thread, fixes #98
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:46:49 -07:00
Leonardo de Moura
fab4eb0d69
feat(frontends/lean/server): add CLEAR_CACHE command, closes #100
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:31:01 -07:00
Leonardo de Moura
f4c7154825
feat(util/lean_path): throws an exception if there is an ambiguity when importing a module
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 10:18:35 -07:00
Leonardo de Moura
9484ab6a04
fix(util/lean_path): if directory 'foo' does not contain 'default.lean', then we should also check whether the file 'foo.lean' exists or not, fixes #102
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 09:04:03 -07:00
Soonho Kong
f8d2ed7936
feat(emacs/lean-type): maintain nay-retry timer
2014-08-27 00:48:55 -07:00
Soonho Kong
224a4feba2
fix(emacs/lean-type): problem with lean-eldoc-nay-retry-time
...
If (current-idle-time) is non-zero, we need to set a timer to run
eldoc-documentation-function again when idle-time = (current-idle-time)
+ retry-delay.
2014-08-26 23:58:02 -07:00
Soonho Kong
a1a14cf425
fix(emacs/lean-info): handle when both identifier and symbol info exist
...
Example: library/data/int/basic.lean file (398, 22)
The '+' symbol is attached with both of identifier info and symbol info
-- SYMBOL|398|22
+
-- ACK
-- IDENTIFIER|398|22
int.add
-- ACK
2014-08-26 22:32:57 -07:00
Soonho Kong
b9c1b1e186
fix(emacs/lean-info): type of a symbol at the end of buffer
2014-08-26 22:32:57 -07:00
Leonardo de Moura
dd99e60a00
refactor(frontends/lean/info_manager): store environment+options in the info_manager, fixes #96
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:07:09 -07:00
Soonho Kong
1de515f693
feat(emacs/lean-mode): clean up old generic-mode
2014-08-26 17:16:16 -07:00
Soonho Kong
665a8f3ecb
feat(emacs/lean-server): handle signal
2014-08-26 17:16:16 -07:00
Soonho Kong
0426d04cb9
feat(emacs/README.md): add elisp which installs required packages
2014-08-26 17:16:16 -07:00
Soonho Kong
83f05e104a
fix(emacs/lean-server): fix ERROR regex pattern
2014-08-26 16:22:32 -07:00
Soonho Kong
682b13a906
feat(emacs/lean-mode): run eldoc-documentation-function at openning
2014-08-26 16:22:32 -07:00
Soonho Kong
c77e5c6b34
feat(emacs/lean-tags): try to find TAGS file upward and use it without asking
2014-08-26 16:22:32 -07:00
Soonho Kong
dfab827d22
feat(emacs/lean-tags): attach advice to tag functions to run ltags
2014-08-26 16:22:32 -07:00
Soonho Kong
1f0bfb67b0
feat(emacs/lean-tags): use full-name to look up tags
2014-08-26 16:22:32 -07:00
Soonho Kong
3d3669e45e
feat(emacs/lean-mode): add key-bindings, deps
2014-08-26 16:22:32 -07:00
Soonho Kong
dd5231d6a7
fix(emacs/lean-server): check current-file before send EVAL
2014-08-26 16:22:32 -07:00
Soonho Kong
f7ff5ec3d6
fix(emacs/lean-server): when handle dead lean-server
2014-08-26 16:22:32 -07:00
Soonho Kong
5965bcc10b
refactor(emacs/lean-server): lean-server-check-current-file takes file-name
2014-08-26 16:22:31 -07:00
Soonho Kong
cc1d44e541
feat(emacs/lean-type): implement lean-set-option and lean-eval-cmd
...
close #55
2014-08-26 16:22:31 -07:00
Soonho Kong
50063b659b
refactor(lean-variable): init server-buffer and current-file-name with nil
2014-08-26 16:22:31 -07:00
Soonho Kong
f82f0377ff
feat(emacs/lean-cmd): add cmd-to-string for SET/EVAL
2014-08-26 16:22:31 -07:00
Soonho Kong
292750c4c9
feat(emacs/lean-type): add SET/EVAL commands
2014-08-26 16:22:31 -07:00
Soonho Kong
679a034277
feat(emacs/lean-mode): use define-derived-mode
2014-08-26 16:22:31 -07:00
Soonho Kong
c1ed9b1293
refactor(emacs/lean-type): clean up eldoc-function and fill-placeholder
2014-08-26 16:22:31 -07:00
Soonho Kong
7ea5c9541d
feat(emacs/lean-info): use cl-struct lean-info-record
2014-08-26 16:22:31 -07:00
Soonho Kong
ccc1f89f61
refactor(emacs/lean-server): use global-server-message-to-process
...
We are using asynchronous process mechanism to communicate between
lean-server and emacs. A sender function like
lean-eldoc-documentation-function sends a command and waits until
lean-global-server-message-to-process is non-nil. When a message is
received from lean-server, a filter function lean-server-output-filter
is triggered. This filter function concatenates a received message to
the buffer until it sees the end of message markers (--
END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer
messages into pre, body, and post parts. Then it assembles a message to
process and attaches the message to
lean-global-server-message-to-process variable. A sender function which
is watching for the variable will recognize it, exit the polling, and
process the message.
2014-08-26 16:22:31 -07:00
Soonho Kong
fc44c7242c
feat(emacs/lean-settings): add eldoc-use and eldoc-nay-retry-time
...
close #51
2014-08-26 16:22:31 -07:00
Soonho Kong
10fb60e4dd
refactor(emacs/lean-util): remove unused functions
...
- take-first-n/last-n => use -take, -drop (from dash.el)
- string-join => use one in flycheck
- remove other unused functions
2014-08-26 16:22:31 -07:00
Soonho Kong
812934f31f
refactor(emacs/lean-flycheck): remove lean-flycheck-initialized
2014-08-26 16:22:31 -07:00
Soonho Kong
495809d86d
feat(emacs/lean-syntax): support multi-line comments /- ... -/
2014-08-26 16:22:30 -07:00
Soonho Kong
c0762333bd
feat(emacs/lean-cmd): add set and eval cmds
2014-08-26 16:22:30 -07:00
Leonardo de Moura
b8b5a59117
fix(frontends/lean/info_manager): do not rely on typeid::before, the behavior is a platform specific
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 14:23:12 -07:00
Leonardo de Moura
11711a2409
fix(util/rb_tree): do not use thread local storage in template when compiling on OSX with clang++ without Boost
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 12:46:24 -07:00
Leonardo de Moura
4c9723e5ed
fix(library/unifier): assertion violation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 09:07:34 -07:00
Leonardo de Moura
44c597724b
fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 09:01:17 -07:00
Leonardo de Moura
02b7f980b0
fix(library/num): bug in to_pos_num, missing test
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 08:18:07 -07:00
Leonardo de Moura
3903be34a4
feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 21:26:17 -07:00
Leonardo de Moura
04d9eb17d1
feat(kernel/conveter): improve support for proof irrelevant in the converter
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 11:19:18 -07:00
Leonardo de Moura
82a7de83cc
feat(frontends/lean/pp_options): use a more effective get_distinguishing_pp_options
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 10:23:28 -07:00
Leonardo de Moura
fbf13994d8
refactor(*): use + for concatenating format objects
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 09:35:25 -07:00
Leonardo de Moura
eb794f7491
refactor(shell): remove obsolete tests
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:12:19 -07:00
Leonardo de Moura
dbaf81e16d
refactor(library): remove unnecessary 'standard' subdirectory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Leonardo de Moura
df60ab4ada
fix(frontends/lean/calc): allow calc_subst to be defined for multiple operators, allow calc cmds to be organized into namespaces, fixes #65
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 16:45:04 -07:00
Leonardo de Moura
2f699fa53a
feat(*): make sections 'permanent', and add 'transient' contexts, closes #88
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 15:45:15 -07:00
Leonardo de Moura
b13851ba13
feat(frontends/lean): add kind and type to index, closes #89
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 12:39:59 -07:00
Leonardo de Moura
01736bf82a
feat(util/sexpr/format): expose flatten
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 12:00:32 -07:00
Leonardo de Moura
e602c4ba49
feat(frontends/lean): change multicomment to /- ... -/
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:55:13 -07:00
Leonardo de Moura
c5a44aca44
fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 17:07:12 -07:00
Leonardo de Moura
2ada3af405
fix(frontends/lean/info_manager): add instantiate method to synth_info_data, fixes #94
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:55:15 -07:00
Leonardo de Moura
a5f0593df1
feat(*): change inductive datatype syntax
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:46:10 -07:00
Leonardo de Moura
01000ff7df
feat(library): add typed_expr macro
...
We use it to enforce that a let-variable has the expected type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 11:26:06 -07:00
Leonardo de Moura
d4ac482d76
refactor(kernel): move annotation to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:38:10 -07:00
Leonardo de Moura
b746492ac8
refactor(library/simple_formatter): rename simple_formatter to print
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:32:08 -07:00
Leonardo de Moura
7d987df429
refactor(kernel/formatter): move simple_formatter to library
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 10:26:45 -07:00
Leonardo de Moura
937c465685
fix(library/unifier): too much reduction
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 21:37:51 -07:00
Leonardo de Moura
07bc0727e2
feat(frontends/lean): 'let [inline]' is the default
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 18:24:22 -07:00
Leonardo de Moura
6cf73b51e2
fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 17:56:18 -07:00
Leonardo de Moura
3498d7ad61
fix(frontends/lean/parser): missing identifier information, fixes #83
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
2071a5986f
fix(frontends/lean/server): crash: uninitialized memory
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
bb6dbe0e6f
fix(library/unifier): we should preprocess choice constraints before we start solving any constraint, fixes #85
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Leonardo de Moura
725f5ba0a0
feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Soonho Kong
f4dfec548d
fix(emacs/lean-mode): add missing flycheck-init
2014-08-21 10:05:14 -07:00
Soonho Kong
39f9826dca
fix(emacs/lean-mode): enable company-etags in lean-mode
2014-08-21 10:05:14 -07:00
Soonho Kong
272c463182
fix(emacs/lean-info): temporary fix for NAY problem
2014-08-21 10:05:14 -07:00
Soonho Kong
09b6fb4f7c
fix(emacs): roll back to generic mode
2014-08-21 10:05:14 -07:00
Leonardo de Moura
359c72b02f
fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 09:28:07 -07:00
Soonho Kong
42c2fef0f2
fix(tests/util/sequence.cpp): clang build error
2014-08-20 21:20:17 -07:00
Leonardo de Moura
e5057ed155
fix(library/unifier): remove incorrect assertion, a local constant may occur in the type of a metavariable that was not instantiated yet
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 18:22:43 -07:00
Jeremy Avigad
6264fb52d6
fix(lean/library/standard): fix tests, more cleanup
2014-08-20 18:04:31 -07:00
Leonardo de Moura
f5987b7bda
refactor(library/unifier): make it easier to add new options to the unifier
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 17:30:08 -07:00
Leonardo de Moura
0450e81392
feat(library/unifier): allow computation when solving flex-rigid constraints
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:20 -07:00
Leonardo de Moura
fa342c8ea7
fix(library/unifier): missing set_conflict
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
9588336c15
refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
4cf3d32e0c
chore(*): create alias for std::pair
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
fcf1778ee0
feat(util): add sequence object with O(1) concatenation operation
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Soonho Kong
51b86b219b
feat(emacs/lean): add multi-line comments
...
This is related with issue #63 .
There are two known issues:
- Emacs behaves as if the multi-line comment start/end symols are "(-"
and "-)" instead of "(--" and "--)". As a result, it shows all the
correct lean comments as it is. However, it will show some examples
such as "(-5)" as a part of comment even if Lean doesn't interpret it
as it is. Technically, it's because we are using a syntax-table based
method to define comments. For more information read a documentation
of 'modify-syntax-entry' function.
- Somehow, the matching parens are broken. When we type "--)" to close
a multi-line comment. Emacs warns "Mismatched Parentheses".
2014-08-19 15:03:51 -07:00
Soonho Kong
c27a379f28
feat(emacs): add company mode (via etags)
2014-08-19 15:03:51 -07:00
Leonardo de Moura
f0d50e0d33
feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias)
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
08ae17650b
feat(frontends/lean): try overloaded notation and declarations in the order they were defined
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
919f02983e
feat(frontends/lean/elaborator): case-split on coercions that cannot be resolved by postponing
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
4a96fefd96
fix(library/unifier): bug in unifier priority queue
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Soonho Kong
608b66c323
fix(emacs/lean-server): check buffer-modified-p before create a process
...
fix #57
2014-08-18 14:18:11 -07:00
Soonho Kong
7a8796a4ca
feat(emacs/lean-info): add identifier/symbol/nay
2014-08-18 14:17:44 -07:00
Soonho Kong
ea4cfe5e7d
refactor(emacs/lean-type): clean up
2014-08-18 13:34:13 -07:00
Soonho Kong
46013b6ad2
feat(emacs): define lean-mode as a derived-mode of prog-mode
...
Fix #52
2014-08-18 13:32:58 -07:00
Soonho Kong
5fa2b9c057
fix(emacs/lean-util): add missing 'cl-' prefix
2014-08-17 18:09:01 -07:00