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

965 commits

Author SHA1 Message Date
Leonardo de Moura
480bc639ea feat(build): add IGNORE_SORRY cmake option 
It allows us to perform nightly builds and avoid distracting warning
messages on CDASH.
 2014-09-26 08:55:54 -07:00
Leonardo de Moura
d02ab15c88 fix(frontends/lean/proof_qed_elaborator): must also create 
metavar_closure before solving nested proof_qed

The bug was exposed by the new policy for handling class-instance
resolution. In the new policy, we reject partial solutions.
The bug fixed in this commit was being masked by a partial solution that
was being "completed" later.
 2014-09-25 20:07:51 -07:00
Leonardo de Moura
c775da16ec feat(frontends/lean/elaborator): discard partial solution during 
class-instance resolution, use only tactic_hints associated with
classes, enforce is_strict
 2014-09-25 19:46:08 -07:00
Leonardo de Moura
318fec43a4 feat(frontends/lean/elaborator): use tactic_hints for unsolved placeholders 2014-09-25 17:54:10 -07:00
Leonardo de Moura
bb1c6d44ac fix(frontends/lean/elaborator): missing register_meta 2014-09-25 17:52:36 -07:00
Leonardo de Moura
bcb30f6232 fix(frontends/lean/placeholder_elaborator): missing 'return' 2014-09-25 15:00:06 -07:00
Leonardo de Moura
23ddacad19 perf(frontends/lean/class): improve is_ext_class procedure 2014-09-25 12:26:09 -07:00
Leonardo de Moura
8747f12118 refactor(frontends/lean/elaborator): remove unnecessary 
set_local_context_for method
 2014-09-25 10:21:31 -07:00
Leonardo de Moura
b8eb65aac2 perf(frontends/lean/placeholder_elaborator): reuse local_context, this 
is possible now because local_context is a mainly "functional object"
 2014-09-25 10:11:41 -07:00
Leonardo de Moura
2e2d2d21f1 refactor(local_context): local_context::scope auxiliary object is not 
needed anymore
 2014-09-25 09:59:27 -07:00
Leonardo de Moura
09162e5fea refactor(frontends/lean/local_context): remove name_generator from local_context 2014-09-25 09:44:34 -07:00
Leonardo de Moura
354c456639 refactor(frontends/lean/local_context): move mvar2meta mapping to elaborator 2014-09-25 09:31:03 -07:00
Leonardo de Moura
fce1113b80 refactor(frontends/lean/coercion_elaborator): simplify 
coercion_elaborator interface
 2014-09-25 08:48:31 -07:00
Leonardo de Moura
a61b95a87e refactor(frontends/lean/proof_qed_elaborator): simplify 
proof_qed_elaborator interface
 2014-09-25 08:38:02 -07:00
Leonardo de Moura
18cfce60b9 refactor(frontends/lean/local_context): simplify local_context representation 2014-09-25 08:13:27 -07:00
Leonardo de Moura
8466115665 fix(frontends/lean/class): missing explicit initialization/finalization 2014-09-24 10:12:29 -07:00
Leonardo de Moura
dbe1763b1a refactor(frontends/lean/server): explicit initialization/finalization 2014-09-24 10:12:29 -07:00
Leonardo de Moura
358074ae3d refactor(kernel/record): remove kernel extension for records, we will 
implement it outside of the kernel on top of the inductive datatypes
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
da481c3274 refactor(kernel): explicit initialization/finalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
29d6bff785 refactor(frontends/lean): explicit initialization/finalization 2014-09-23 10:00:36 -07:00
Leonardo de Moura
4437a65d0b refactor(frontends/lean/builtin_cmds): explicit token initialization 2014-09-22 19:22:53 -07:00
Leonardo de Moura
531046626a refactor(*): explicit initialization/finalization for environment extensions 2014-09-22 17:30:29 -07:00
Leonardo de Moura
b6781711b1 refactor(*): explicit initialization/finalization for serialization 
modules, expression annotations, and tactics
 2014-09-22 15:26:41 -07:00
Leonardo de Moura
b1ee888aae refactor(*): start move to explicit initialization/finalization, 
explicitly initialize/finalize options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-22 10:41:07 -07:00
Leonardo de Moura
8fe7465ade fix(frontends/lean/pp): when formatting a coercion to function-class 
that contains implicit arguments
 2014-09-20 09:56:46 -07:00
Leonardo de Moura
fd5daa8fda feat(frontends/lean): use coercions to function-class and sort-class in 
function arguments, closes #203
 2014-09-20 09:00:10 -07:00
Leonardo de Moura
e430dc8bab feat(frontends/lean): add 'irreducible' as syntax sugar for 'reducible [off]' 2014-09-19 15:54:32 -07:00
Leonardo de Moura
4e2377ddfc refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
5d8c7fbdf1 refactor(frontends/lean): replace '[private]' modifier with 'private 
definition' and 'private theorem', '[private]' is not a hint.
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
97b1998def refactor(frontends/lean): replace '[opaque]' modifier with 'opaque 
definition', '[opaque]' is not a hint, but a kind of definition
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
08ccd58eb6 feat(frontends/lean): add 'reducible' modifier for controlling which 
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
48dbd13eef feat(frontends/lean): allow transient classes/instances, i.e., 
classes/instances that are not saved in .olean files
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
93c2c30310 feat(frontends/lean): allow transient coercions, i.e., coercions that 
are not saved in .olean files
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
b53b1825ae fix(frontends/lean/info_manager): get_closest_env_opts 2014-09-18 17:03:59 -07:00
Leonardo de Moura
9e29602934 fix(frontends/lean/info_manager): make sure env_info is not lost when 
starting parser in the middle of the 'file'
 2014-09-18 16:51:59 -07:00
Leonardo de Moura
970ad72bc3 fix(frontends/lean/pp): protect pretty printer from exceptions 2014-09-18 16:21:20 -07:00
Leonardo de Moura
b3e05a2fe9 refactor(frontends/lean/scanner): remove dependency to seekg and unget 
methods

It is not safe to use seekg for textual files. Here is a fragment from a
C++ manual:

seekg() and seekp()

This pair of functions serve respectively to change the position of stream pointers get and put. Both functions are overloaded with two different prototypes:

     seekg ( pos_type position );
     seekp ( pos_type position );

Using this prototype the stream pointer is changed to an absolute position from the beginning of the file. The type required is the same as that returned by functions tellg and tellp.

      seekg ( off_type offset, seekdir direction );
      seekp ( off_type offset, seekdir direction );

Using this prototype, an offset from a concrete point determined by
parameter direction can be specified. It can be:

          ios::beg	offset specified from the beginning of the stream
          ios::cur	offset specified from the current position of the stream pointer
          ios::end	offset specified from the end of the stream

The values of both stream pointers get and put are counted in different
ways for text files than for binary files, since in text mode files some
modifications to the appearance of some special characters can
occur. For that reason it is advisable to use only the first prototype
of seekg and seekp with files opened in text mode and always use
non-modified values returned by tellg or tellp. With binary files, you
can freely use all the implementations for these functions. They should
not have any unexpected behavior.
 2014-09-18 15:24:48 -07:00
Leonardo de Moura
9733401c20 fix(frontends/lean/tactic_hint): failure when compiling lean terms into 
tactics: mismatch on the number of universe parameters
 2014-09-17 15:23:10 -07:00
Leonardo de Moura
2b0623c0a1 fix(frontends/lean): assertion violations 2014-09-16 18:59:51 -07:00
Leonardo de Moura
78ad24a697 feat(frontends/lean/server): add SYNC command, closes #199 2014-09-16 18:42:34 -07:00
Leonardo de Moura
e3e2370a38 feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-16 18:03:40 -07:00
Leonardo de Moura
4b51d50ad4 fix(frontends/lean/elaborator): coercion overloading 2014-09-16 15:12:20 -07:00
Leonardo de Moura
dffe9a6f17 fix(frontends/lean/elaborator): more robust support for coercions to 
function-class that contains implicit arguments
 2014-09-16 13:08:34 -07:00
Leonardo de Moura
d0d23eb525 fix(frontends/lean/inductive_cmd): improve name resolution in inductive 
command

The new test demonstrates the problem being fixed by this commit
 2014-09-16 09:48:51 -07:00
Leonardo de Moura
af2c3b1815 fix(frontends/lean/info_manager): bug in save_environment_options, 
server was displaying old results
 2014-09-15 16:05:17 -07:00
Leonardo de Moura
93e83baa1b fix(frontends/lean/parser): commit_upto invocation after 'import' 2014-09-15 16:05:17 -07:00
Leonardo de Moura
feb4993f9c fix(frontends/lean/server): '[anonymous]' entry being displayed by FINDP 
This could happen when there is a declaration (e.g., nat) whose type is
equal to an active namespace.
 2014-09-15 16:05:17 -07:00
Leonardo de Moura
d47412d201 fix(frontends/lean/parser): error line numbers for lua code, fixes #194 2014-09-14 21:03:09 -07:00
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
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
b7dcb8f833 fix(frontends/lean/elaborator): remove annotation left-over 2014-09-12 16:12:23 -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
80fd14b39e refactor(frontends/lean): replace collect_metavars with metavar_closure helper class 2014-09-11 14:49:35 -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
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
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
Leonardo de Moura
b82092a123 fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172 2014-09-10 08:39:39 -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
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
2d94584816 feat(frontends/lean/pp): add 'pp.beta' option, closes #154 2014-09-09 14:10:20 -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
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
c88bfc0c02 chore(frontends/lean/server.cpp): add BEGIN/END for WAIT command 2014-09-08 16:04:19 -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
da701eb6de fix(frontends/lean/elaborator): bug in recent change 2014-09-07 19:08:31 -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
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
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
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
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
898021c1b8 fix(frontends/lean/server): cleanup info in modified line 2014-09-05 01:36:17 -07:00