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

1637 commits

Author SHA1 Message Date
Leonardo de Moura
1e8a975daa feat(frontends/lean): extend parser: rewrite "fold" step 2015-02-06 15:22:34 -08:00
Leonardo de Moura
5b25da8c43 feat(frontends/lean): add esimp tactic based on rewrite tactic 
closes #358
 2015-02-06 14:13:32 -08:00
Leonardo de Moura
bc95f09828 feat(frontends/lean/decl_cmds): allow user to specify unfold-c hint 2015-02-06 12:56:52 -08:00
Leonardo de Moura
2e626b29fb feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step 2015-02-06 11:03:36 -08:00
Leonardo de Moura
56a46ae61e feat(frontends/lean/parse_tactic_location): make rewrite notation more uniform 2015-02-06 10:31:50 -08:00
Leonardo de Moura
38ab4e7b3a feat(frontends/lean/parse_rewrite_tactic): extend rewrite tactic parser 
Add support for reduction steps.
 2015-02-05 13:24:37 -08:00
Leonardo de Moura
5443609845 fix(frontends/lean/parse_rewrite_tactic): take namespaces into account when parsing constant to unfold 2015-02-05 12:41:11 -08:00
Leonardo de Moura
b6dd1269b9 feat(frontends/lean/builtin_exprs): make 'obtain' arguments visible by default 2015-02-05 10:38:45 -08:00
Leonardo de Moura
dfad24e3f5 feat(frontends/lean): polish rewrite tactic notation 2015-02-05 10:15:58 -08:00
Leonardo de Moura
15efadfbdc feat(frontends/lean/parse_rewrite_tactic): cleanup rewrite tactic notation 
Make a rewrite command sequence explicit.
 2015-02-04 20:16:24 -08:00
Leonardo de Moura
08dcc9e2fc feat(frontends/lean/parse_rewrite_tactic): polish rewrite tactic notation 2015-02-04 19:19:19 -08:00
Leonardo de Moura
599de0271b feat(frontends/lean/parse_tactic_location): validate occurrence index 2015-02-04 14:04:56 -08:00
Leonardo de Moura
8912c759dd fix(frontends/lean/parse_rewrite_tactic): corner case "rewrite ?(t)" 
The token '?(' is used to represent inaccessible terms in recursive
equations. In the rewriter tactic, we want "rewrite ?(t)" to be parsed
as "? (t)".
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
991d29b7f6 fix(frontends/lean/parse_rewrite_tactic): bugs in rewrite tactic parser 2015-02-04 11:51:39 -08:00
Leonardo de Moura
b4dd2cc729 refactor(library/tactic/rewrite_tactic): more general rewrite step 
The rule can be an arbitrary expression.
Allow user to provide a pattern that restricts the application of the rule.
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
461fd45efc feat(frontends/lean): allow a different location for each rewrite element 2015-02-04 11:51:39 -08:00
Leonardo de Moura
c845e44777 feat(frontends/lean): parse rewrite tactic 2015-02-04 11:51:39 -08:00
Leonardo de Moura
87bcec2e5e feat(frontends/lean): parse tactic location (i.e., scope of application) 2015-02-04 11:51:39 -08:00
Leonardo de Moura
0cea63651d fix(frontends/lean): store line/col information at snapshots, save snapshot before 'end' scope, and before "closing" open namespaces 
closes #422
 2015-02-04 10:40:36 -08:00
Leonardo de Moura
1ee47dc063 feat(frontends/lean/server): suppress projections from autocompletion 
closes #424
 2015-02-04 07:18:47 -08:00
Leonardo de Moura
c92f3bec65 refactor(library/definitional/projection): move projection "database" to library/projection 2015-02-04 07:18:43 -08:00
Leonardo de Moura
15716c1471 feat(frontends/lean/calc_proof_elaborator): reject proofs with metavariables in the calc-assistant 2015-02-01 11:11:27 -08:00
Leonardo de Moura
d52af105d7 feat(frontends/lean/decl_cmds): allow many constants to be set in the same attribute command 2015-01-31 23:55:14 -08:00
Leonardo de Moura
855050e623 feat(frontends/lean/calc_proof_elaborator): try conservative alternatives first 2015-01-31 21:29:34 -08:00
Leonardo de Moura
dbc8e9e13a refactor(*): add method get_num_univ_params 2015-01-28 17:22:18 -08:00
Leonardo de Moura
e4b5e07498 fix(frontends/lean/elaborator): apply substitution before compiling pre-tactics into tactics 
closes #415
 2015-01-28 13:32:56 -08:00
Leonardo de Moura
2a5658ebe2 fix(frontends/lean/elaborator_context): memory leak 2015-01-26 16:08:51 -08:00
Leonardo de Moura
e2c41fca75 feat(frontends/lean): modify syntax for local notation 
The idea is to make it uniform with the syntax for defining local
attributes.
 2015-01-26 11:51:17 -08:00
Leonardo de Moura
b4d6f6e3ed feat(frontends/lean): 'attribute' command is persistent by default 2015-01-26 11:51:17 -08:00
Leonardo de Moura
4f2e0c6d7f refactor(frontends/lean): add 'attribute' command 
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
 2015-01-24 20:23:21 -08:00
Leonardo de Moura
b5c4e603db feat(frontends/lean): allow parameters to be used in sections 
Restriction:
- coercions and notations cannot be defined in parametric sections

closes #401
 2015-01-23 17:42:19 -08:00
Leonardo de Moura
27f6bfd3f0 refactor(*): add file constants.txt with all constants used by the Lean binary 2015-01-23 16:50:32 -08:00
Leonardo de Moura
880faf89e0 feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command 
closes #354
 2015-01-21 18:12:29 -08:00
Leonardo de Moura
a53098385c refactor(frontends/lean/type_util): move infer_implicit_params to library 2015-01-21 17:22:41 -08:00
Leonardo de Moura
12674114a4 feat(shell): set default behavior to "trusted" 
closes #402
 2015-01-21 16:25:09 -08:00
Leonardo de Moura
01ce57e52e feat(library/definitional/projection): add projection macro 2015-01-20 16:21:50 -08:00
Leonardo de Moura
752b54085b refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used 
Now, we unfold untrusted macros outside of the Lean kernel.
 2015-01-20 12:36:56 -08:00
Leonardo de Moura
260795f981 fix(frontends/lean/structure_cmd): collect universe levels that only occur in structure parameters 
fixes #395
 2015-01-19 22:18:09 -08:00
Leonardo de Moura
002050fa97 feat(frontends/lean): increase binding power of ! and @ 
Remark: I did not add the constant "app".
Reason: It would break the standard library in many places.
Moreover, the current "max" is not just the binding power of
application, but also the binding power of identifiers, (, [, ...
It would be weird to call it "app"

closes #388
 2015-01-19 18:40:33 -08:00
Leonardo de Moura
dfbe6662be feat(frontends/lean/elaborator): add option 'elaborator.fail_if_missing_field' 2015-01-19 17:47:39 -08:00
Leonardo de Moura
2717adde94 feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant 2015-01-19 16:23:29 -08:00
Leonardo de Moura
d0e9e0e21c feat(library/definitional/projection): add auxiliary function for simplifying expressions containing projections and constructors 2015-01-18 20:58:40 -08:00
Leonardo de Moura
edcc92d9c7 feat(frontends/lean): remove 'using' from structure instance command 2015-01-17 09:38:10 -08:00
Leonardo de Moura
f9d7480f5c feat(frontends/lean): notation for creating structure instances 2015-01-16 17:14:30 -08:00
Leonardo de Moura
bfd679d52d feat(frontends/lean/structure_cmd): allow user to reference parent structures when defining new fields 
See new test for an example.

closes #371
 2015-01-16 13:04:48 -08:00
Leonardo de Moura
13660cfecd feat(frontends/lean/parser): add parse_qualified_expr 2015-01-16 12:42:42 -08:00
Leonardo de Moura
8ab775bd6f feat(*): distinguish between logical and runtime exceptions. 
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
 2015-01-15 16:54:55 -08:00
Leonardo de Moura
e48df78938 feat(frontends/lean/elaborator): do not apply delayed_coercions on equation lhs 
The variables in the equation lhs do not have type at preprocessing
time (i.e., their type is a metavariable). So, they may seem candidates
for delayed_coercions. If the coercions are injected, we will not be
able to pattern match. Thus, we disable coercions in this case.
 2015-01-13 18:05:22 -08:00
Leonardo de Moura
37e852ba61 feat(frontends/lean/elaborator): improve error message for metavariable in inaccessible position on equation lhs 2015-01-13 14:38:25 -08:00
Leonardo de Moura
41935906a8 chore(frontends/lean): use update_if_undef 2015-01-13 13:02:14 -08:00
Leonardo de Moura
4f519be55e fix(frontends/lean/elaborator): compilation problem 2015-01-11 20:58:41 -08:00
Leonardo de Moura
75d7e4ab9e feat(frontends/lean): add 'end' token to match expressions 2015-01-10 12:35:29 -08:00
Leonardo de Moura
5796640392 fix(frontends/lean): do report unassigned metavariables in equation lhs 2015-01-10 10:39:47 -08:00
Leonardo de Moura
b172229a72 feat(frontends/lean): add 'match' expressions 
We reuse the equations infrastructure to compile them.
 2015-01-10 10:11:13 -08:00
Leonardo de Moura
6df9ffe5f6 fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler 2015-01-10 09:18:27 -08:00
Leonardo de Moura
87d41e90fc fix(frontends/lean/decl_cmds): store equations positions 2015-01-07 18:50:56 -08:00
Leonardo de Moura
a9b6e20a22 fix(frontends/lean): save equations position 2015-01-06 15:55:04 -08:00
Leonardo de Moura
a3a6697f44 feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes 2015-01-06 14:07:17 -08:00
Leonardo de Moura
828ce3f8dc feat(frontends/lean/decl_cmds): minor modifications for supporting mutually recursive functions 2015-01-05 19:23:50 -08:00
Leonardo de Moura
0aa7e4a9f9 fix(frontends/lean/pp): option 'pp.private_names' should also affect private declarations defined in the current file 2014-12-28 14:22:36 -08:00
Leonardo de Moura
d2958044fd feat(frontends/lean): add multiple_instances command 
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command

          multiple_instances <class-name>

closes #370
 2014-12-21 17:28:44 -08:00
Leonardo de Moura
4421069e34 refactor(library/tactic): rename placeholder_elaborator to class_instance_synth 2014-12-19 19:57:38 -08:00
Leonardo de Moura
ded869b7e0 refactor(frontends/lean): move placeholder_elaborator to library/tactic 2014-12-19 15:23:22 -08:00
Leonardo de Moura
a22dc773b7 refactor(frontends/lean): move some auxiliary procedures to library/tactic 2014-12-19 15:19:45 -08:00
Leonardo de Moura
07d7ea2f4e refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean 2014-12-19 15:08:21 -08:00
Leonardo de Moura
69750c50c6 refactor(frontends/lean): move pp_options to library 2014-12-19 15:00:05 -08:00
Leonardo de Moura
caf0a4bf15 refactor(frontends/lean): move type_checker_ptr typedef to library 2014-12-19 14:40:15 -08:00
Leonardo de Moura
02de288a51 refactor(frontends/lean): move choice_iterator to library 2014-12-19 14:29:32 -08:00
Leonardo de Moura
6f78315aa4 refactor(*): add uniform names for "meta-objects" 2014-12-17 11:42:14 -08:00
Leonardo de Moura
8939351903 refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception 2014-12-15 19:22:17 -08:00
Leonardo de Moura
5cf8064269 refactor(library): rename exists_elim and exists_intro to exists.elim 
and exists.intro
 2014-12-15 19:07:38 -08:00
Leonardo de Moura
c291063f3a fix(frontends/lean/structure_cmd): simplify structure names 2014-12-13 14:18:02 -08:00
Leonardo de Moura
ab873cfff9 feat(frontends/lean/elaborator): replace metavariables in the equation lhs with fresh local constants before invoking compiler 2014-12-11 19:51:49 -08:00
Leonardo de Moura
91ce99d921 feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion 2014-12-11 18:13:35 -08:00
Leonardo de Moura
3d199d275d fix(frontends/lean/token_table): increase binding power of decreasing operator 2014-12-11 17:31:12 -08:00
Leonardo de Moura
287a444481 feat(frontends/lean/pp): add option 'pp.numerals' 2014-12-11 17:28:58 -08:00
Leonardo de Moura
b8f665e561 feat(frontends/lean): elaborate recursive equations 
Remark: we are not compiling them yet.
 2014-12-10 22:25:40 -08:00
Leonardo de Moura
756fae7c2a refactor(frontends/lean): move local_context to library 2014-12-10 12:43:32 -08:00
Leonardo de Moura
bf875d5778 feat(library/definitional/equations): add support for inaccessible patterns 2014-12-10 12:35:08 -08:00
Leonardo de Moura
d98aabe9ab refactor(library): move library/definitional/util module to library 2014-12-10 11:23:23 -08:00
Leonardo de Moura
ac664505e6 refactor(library): move class management to library module 2014-12-09 21:38:55 -08:00
Leonardo de Moura
05f27b8f0e feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures 
It seems most of the time these theorems are not used at all.
They are just polluting the namespace.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-12-09 12:40:09 -08:00
Leonardo de Moura
d67583df44 fix(frontends/lean/parser): do not generate error when 'exit' command is used 2014-12-09 10:14:14 -08:00
Leonardo de Moura
58432d0968 feat(library/definitional): add no_confusion construction that is compatible with the HoTT library 2014-12-08 22:11:48 -08:00
Leonardo de Moura
2bb51554d5 feat(library/definitional/util): add telescope equality for HoTT library 
This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.
 2014-12-07 18:35:55 -08:00
Leonardo de Moura
ec7f90cb16 feat(hott/init): make sure eq is universe polymorphic 
Jakob and Floris needed path equality to be universe polymorphic when
proving univalence.
 2014-12-06 09:43:42 -08:00
Leonardo de Moura
53d6d76162 fix(frontends/lean/parser): generate error when 'exit' command is used 
m_theorem_queue.join() method assumes there are no open namespaces/scopes
 2014-12-05 16:12:23 -08:00
Leonardo de Moura
eb87c18693 feat(*): add support for separate HoTT library 2014-12-05 14:34:02 -08:00
Leonardo de Moura
e868ecce36 feat(frontends/lean): parse recursive equations 2014-12-04 17:03:21 -08:00
Leonardo de Moura
7a6d674b8e refactor(frontends/lean/decl_cmds): cleanup definition_cmd 2014-12-04 16:03:29 -08:00
Leonardo de Moura
52334dca29 feat(frontends/lean): parse "decreasing" expressions 2014-12-04 15:11:23 -08:00
Leonardo de Moura
e72c4977f0 feat(frontends/lean): nicer notation for dependent if-then-else 2014-12-04 11:13:09 -08:00
Leonardo de Moura
0443c1e70c fix(frontends/lean): intro tactic + universe variables, fixes #362 2014-12-03 12:56:30 -08:00
Leonardo de Moura
fca97d5bb2 feat(library/definitional): add brec_on construction, closes #272 2014-12-03 10:39:32 -08:00
Leonardo de Moura
5b2d17e4ab feat(frontends/lean): add 'print notation' command 2014-12-02 12:04:18 -08:00
Leonardo de Moura
8c50048d1b chore(frontends/lean/pp): fix style 2014-12-01 17:15:30 -08:00
Leonardo de Moura
320971832d feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals 2014-12-01 16:07:55 -08:00
Leonardo de Moura
8dfd22e66c feat(frontends/lean): add 'prelude' command, and init directory 2014-11-30 17:03:08 -08:00
Leonardo de Moura
2281fb30c8 refactor(library): use "symbolic" precedences in the standard library 2014-11-29 19:08:37 -08:00
Leonardo de Moura
2c0472252e feat(frontends/lean): allow expressions to be used to define precedence, closes #335 2014-11-29 18:29:48 -08:00
Leonardo de Moura
2487e3b83d fix(frontends/lean/parser): user provided numeral notation should have precedence over the default based on 'num' 2014-11-29 17:29:03 -08:00
Leonardo de Moura
bc65aeb5e1 fix(frontends/lean/calc): add expected type for single-step calc expressions, fixes #357 
This is not an issue for calc expressions containing multiple steps,
since the transitivity step will "force" the expected type for the proofs.
 2014-11-29 15:35:09 -08:00
Leonardo de Moura
a97d7ffed7 feat(frontends/lean/builtin_cmds): display 'print' command output as flycheck information 2014-11-29 13:31:42 -08:00
Leonardo de Moura
366bf70ccd fix(frontends/lean/elaborator): do not display flycheck related messages when --flycheck is not on 2014-11-28 21:20:25 -08:00
Leonardo de Moura
8b804f1d22 feat(frontends/lean): add option 'elaborator.flycheck_goals' 2014-11-28 16:34:02 -08:00
Leonardo de Moura
9516cd9ee3 feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression 
Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
 2014-11-28 14:59:35 -08:00
Leonardo de Moura
4ec2101b06 feat(frontends/lean): add option 'pp.purify_locals' 2014-11-28 14:49:00 -08:00
Leonardo de Moura
db9fd53b80 fix(library/tactic): pretty printer for proof states 2014-11-27 09:43:58 -08:00
Leonardo de Moura
ffdeb0edc4 fix(frontends/lean/elaborator): unsolved metavariables, fix #329 2014-11-26 11:56:39 -08:00
Leonardo de Moura
24a15b6c46 fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343 2014-11-24 21:33:52 -08:00
Leonardo de Moura
a005c8f4d0 feat(frontends/lean): display eval/check/find_decl results using flycheck 2014-11-24 08:35:49 -08:00
Leonardo de Moura
d81a6259e8 feat(frontends/lean/find_cmd): add options for controlling find_decl 2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188 feat(frontends/lean): add 'find_decl' command 2014-11-23 23:00:59 -08:00
Leonardo de Moura
8c8bf41e39 feat(frontends/lean/server): do not unfold definitions in FINDG 2014-11-23 19:03:39 -08:00
Leonardo de Moura
44a2ef8f6f fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file 2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278 feat(frontends/lean): allow user to associate precedence to binders, closes #323 2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087 feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333 2014-11-23 17:30:46 -08:00
Leonardo de Moura
5d5fd2da50 fix(frontends/lean): tactic + section variables, fixes #332 2014-11-21 10:07:16 -08:00
Leonardo de Moura
28c63e685b feat(frontends/lean): add '[local]' notation, closes #322 2014-11-16 21:15:04 -08:00
Leonardo de Moura
ea640257bf feat(frontends/lean/structure_cmd): generate no_confusion for structures too 2014-11-15 16:00:09 -08:00
Leonardo de Moura
7685516d1e feat(frontends/lean): better default for atomic notation 2014-11-14 16:25:13 -08:00
Leonardo de Moura
488f989c46 fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop 2014-11-14 13:57:42 -08:00
Leonardo de Moura
58525905d0 fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command 2014-11-13 22:05:55 -08:00
Leonardo de Moura
6bc89f0916 feat(library/definitional): define ibelow and below 
These are helper definitions for brec_on and binduction_on
 2014-11-12 16:38:46 -08:00
Leonardo de Moura
a3066e3eaa fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator 2014-11-12 13:10:19 -08:00
Leonardo de Moura
5312afa7ec feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes 
The new test contains examples that required explicit levels.
 2014-11-12 10:52:32 -08:00
Leonardo de Moura
e2bfe6ee36 refactor(library/definitional/no_confusion): cleanup API 2014-11-11 16:12:44 -08:00
Leonardo de Moura
f6889951c6 fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion 2014-11-11 15:14:08 -08:00
Leonardo de Moura
902a551048 feat(definitional/brec_on): add 'mk_below' skeleton 2014-11-11 14:55:21 -08:00
Leonardo de Moura
1079d6b320 refactor(library/definitional): combine auxiliary functions used by definitional package in a single module 2014-11-11 13:46:36 -08:00
Leonardo de Moura
50973bb4f3 feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations 
To retrieve the previous behavior, we should use [strict] modifier
 2014-11-10 12:46:04 -08:00
Leonardo de Moura
95554a527c feat(frontends/lean/placeholder_elaborator): display instance trace header once per class-instance resolution problem 2014-11-09 15:00:13 -08:00
Leonardo de Moura
fa26c2301c fix(frontends/lean): fix pretty-printing spacing problem 2014-11-09 14:49:43 -08:00
Leonardo de Moura
3aac26d658 fix(frontends/lean): tactic + variables bug, fixes #315 2014-11-09 14:43:22 -08:00
Leonardo de Moura
eff3c6b774 feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314 
See tests/lean/fold.lean for examples
 2014-11-09 14:08:33 -08:00
Leonardo de Moura
ce889ddf60 feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1' 2014-11-09 12:55:13 -08:00
Leonardo de Moura
df5a17cdce feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace 2014-11-09 12:06:16 -08:00
Leonardo de Moura
1d9a0a6265 feat(frontends/lean/placeholder_elaborator): add option 'elaborator.instance_max_depth' 2014-11-09 11:59:44 -08:00
Leonardo de Moura
9b9ae128d5 feat(frontends/lean): include file-name and line/col numbers when displaying class-instance resolution trace 2014-11-09 11:47:01 -08:00
Leonardo de Moura
6362610411 fix(frontends/lean): include position information 2014-11-09 11:43:44 -08:00
Leonardo de Moura
76fb6893e1 feat(frontends/lean): add elaborator.trace_instances option 
When on this option allows us to visualize "class-instance resolution"
 2014-11-09 11:24:19 -08:00
Leonardo de Moura
0b8c44a94a feat(frontends/lean): add option pp.purify_metavars 
It is true by default. If the user sets it to false, then
the internal metavariable names are used in the pretty printer
 2014-11-09 11:04:22 -08:00
Leonardo de Moura
e8bc0f8249 feat(library/defitional): add no_confusion construction for inductive datatypes that are not propositions 2014-11-08 18:56:52 -08:00
Leonardo de Moura
b5da143fc0 feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions 2014-11-08 15:20:19 -08:00
Leonardo de Moura
c7992f2cac feat(frontends/lean): add [whnf] modifier to eval command 2014-11-08 10:19:29 -08:00
Leonardo de Moura
b5e0ded163 feat(frontends/lean): max precedence used by Lean is not max_uint anymore 
The motivation is to allow users to define notation with higher
precedence than function application.
 2014-11-07 07:57:11 -08:00
Leonardo de Moura
85d0521d48 feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305 2014-11-06 21:34:05 -08:00
Leonardo de Moura
be52d950f0 fix(frontends/lean): improve error message, addresses issue #299 2014-11-06 12:19:40 -08:00
Leonardo de Moura
8723f5b613 fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches. 
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).

This bug would confuse users and make them believe they define something
different.
 2014-11-05 23:12:00 -08:00
Leonardo de Moura
b3ad8c704a feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296 2014-11-05 15:01:05 -08:00
Leonardo de Moura
4650791108 feat(frontends/lean): add 'print fields' command 2014-11-05 14:06:54 -08:00
Leonardo de Moura
677e0aeef6 fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified 2014-11-05 12:02:52 -08:00
Leonardo de Moura
d6dc624ca8 fix(frontends/lean/structure_cmd): error parsing structure without parameters followed by ': Type' 2014-11-05 12:02:52 -08:00
Leonardo de Moura
defc2478b5 feat(frontends/lean): add 'record' as an alias for 'structure' command 2014-11-05 12:02:52 -08:00
Leonardo de Moura
5b87d060cf fix(frontends/lean/structure_cmd): universe level validation 2014-11-04 22:19:23 -08:00
Leonardo de Moura
6944c7d902 fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293 2014-11-04 18:41:27 -08:00
Leonardo de Moura
b5ad0fb504 refactor(frontends/lean/local_context): add 'const' modifier 2014-11-04 18:37:31 -08:00
Leonardo de Moura
3bfe5b0b7e fix(frontends/lean): type information for "atomic" notation declaration, fixes #292 2014-11-04 18:01:20 -08:00
Leonardo de Moura
fa405d7884 refactor(frontends/lean): combine info annotations in a single module 2014-11-04 18:01:20 -08:00
Leonardo de Moura
60eac0195d feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures 2014-11-04 09:10:25 -08:00
Leonardo de Moura
d58c3e498d feat(frontends/lean/builtin_cmds): add 'print prefix' command 2014-11-04 08:40:32 -08:00
Leonardo de Moura
3454e70017 fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289 
Fix incorrect line/column number information in error messages produced
during inductive datatype elaboration.
 2014-11-04 07:44:47 -08:00
Leonardo de Moura
b6722a5d33 feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures 
When it is used coercions/instances to parent structure are to registered
 2014-11-03 23:16:49 -08:00
Leonardo de Moura
b24165dc7b feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on' 2014-11-03 23:06:33 -08:00
Leonardo de Moura
7897e21a14 feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided 2014-11-03 22:55:51 -08:00
Leonardo de Moura
08b4ce2db9 feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided 2014-11-03 22:40:08 -08:00
Leonardo de Moura
8f3139231b feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header 2014-11-03 22:17:43 -08:00
Leonardo de Moura
91749d2364 fix(frontends/lean/structure_cmd): modify coercion generation 
The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
 2014-11-03 19:37:11 -08:00
Leonardo de Moura
c306bfa83c feat(frontends/lean/structure_cmd): add 'eta' theorem for structures 2014-11-03 18:33:44 -08:00
Leonardo de Moura
186d910d0b feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes) 2014-11-03 17:55:59 -08:00
Leonardo de Moura
9531203d9d feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used 2014-11-03 17:47:08 -08:00
Leonardo de Moura
b112f3c582 feat(frontends/lean/structure_cmd): add coercions to parent structures 2014-11-03 17:39:52 -08:00
Leonardo de Moura
922e66c42f fix(frontends/lean/decl_cmds): do not save 'examples' in .ilean file 2014-11-03 16:13:46 -08:00
Leonardo de Moura
7afa69577e feat(frontends/lean/structure_cmd): add aliases for structure decls 2014-11-03 15:50:41 -08:00
Leonardo de Moura
efe1105eb9 fix(frontends/lean): alias generation for composite names was not working 
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.

The commit also fix a bug in the generate of aliases for recursors
 2014-11-03 15:43:58 -08:00
Leonardo de Moura
594e3ea8fc fix(frontends/lean/structure_cmd): 'rec' must be marked as protected 2014-11-03 14:50:12 -08:00
Leonardo de Moura
5872c93eaf feat(frontends/lean/structure_cmd): add structure_cmd core 2014-11-03 14:14:40 -08:00
Leonardo de Moura
a2e75159c8 fix(frontends/lean): process choice-exprs at check_constant_next 2014-11-02 19:42:30 -08:00
Leonardo de Moura
df008dc3c3 feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype 2014-11-01 19:15:46 -07:00
Leonardo de Moura
ea55ec4090 feat(frontends/lean/decl_cmds): remove useless name from 'example' commad 2014-11-01 16:12:23 -07:00
Leonardo de Moura
1e6f7cdbb4 chore(frontends/lean/decl_cmds): add 'example' command 
It is like a theorem, but it is discarded after checking
 2014-11-01 11:37:39 -07:00
Leonardo de Moura
b1c2efecbb chore(frontends/lean/decl_cmds): add missing static 2014-11-01 11:18:10 -07:00
Leonardo de Moura
94cf10284a fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286 
The problem was that heq type is
    Pi {A : Type} (a : A) {B : Type} (b : B), Prop

The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.

The fix is to remove this assumption.
 2014-11-01 07:30:04 -07:00
Leonardo de Moura
2688ca38bf feat(frontends/lean/inductive_cmd): notation for enumeration types 2014-10-31 19:01:32 -07:00
Leonardo de Moura
57b19b787b feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if ! was used 2014-10-31 09:49:45 -07:00
Leonardo de Moura
dc7ab17d2a feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option 2014-10-31 09:49:45 -07:00
Leonardo de Moura
d7beabe91c fix(frontends/lean/calc_proof_elaborator): improve calc proof assistant 2014-10-31 09:49:45 -07:00
Leonardo de Moura
8a4d4409cd feat(frontends/lean/calc_proof_elaborator): add '{...⁻¹}' if needed in calc proofs, closes #268 
This commit also simplifies library/data/nat/basic.lean
 2014-10-31 01:02:49 -07:00
Leonardo de Moura
17df85f592 feat(frontends/lean/calc_proof_elaborator): add '{...}' if needed in calc proof steps 
This is part of #268
 2014-10-31 00:55:19 -07:00
Leonardo de Moura
42dba5cc98 feat(frontends/lean/calc): expose get_calc_subst_info and get_calc_refl_info APIs 2014-10-30 23:56:38 -07:00
Leonardo de Moura
591e566472 feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator 
This is part of #268
 2014-10-30 23:24:09 -07:00
Leonardo de Moura
c5a62f8abb feat(frontends/lean): insert ! in calculational proofs when needed 
This is part of #268
 2014-10-30 22:22:04 -07:00
Leonardo de Moura
407e35692b feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved 
Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268.

Remark: we don't wrap the proof if it is of the form

   - `by tactic`
   - `begin tactic-seq end`
   - `{ expr }`
 2014-10-30 18:33:47 -07:00
Leonardo de Moura
e79c7d9852 feat(frontends/lean): make set_option affect fingerprints 2014-10-30 14:45:35 -07:00
Leonardo de Moura
498b2f681e feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution 2014-10-30 14:44:58 -07:00
Leonardo de Moura
79f73c44dc feat(frontends/lean/placeholder_elaborator): add 'elaborator.unique_class_instances' flag, closes #265 
By default, it is false.
When it is true, class instance resolution generates an error if there
is more than one solution.
 2014-10-30 14:21:24 -07:00
Leonardo de Moura
64c3ba7b74 feat(frontends/lean): display metavariable application arguments in check command 
The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
 2014-10-30 13:28:25 -07:00
Leonardo de Moura
dcd7e53fa7 feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command 
We don't need it anymore after previous commit 2a16050
 2014-10-30 13:12:45 -07:00
Leonardo de Moura
2a160508c3 feat(frontends/lean): lean --server should display meta-variables using the approach used in check command, closes #280 2014-10-30 12:45:41 -07:00
Leonardo de Moura
a1ea087f8e fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element 2014-10-30 10:35:45 -07:00
Leonardo de Moura
6107da05db fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283 2014-10-29 19:47:14 -07:00
Leonardo de Moura
8e9f97e95e fix(frontends/lean): do not save identifier info 2014-10-29 17:38:59 -07:00
Leonardo de Moura
c1653a9fb4 feat(frontends/lean): only valid proof states should be displayed, closes #275 2014-10-29 17:29:40 -07:00
Leonardo de Moura
a98b12f067 fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276 2014-10-29 16:51:06 -07:00
Leonardo de Moura
1c9992800f fix(frontends/lean/info_manager): suppress useless tactic type information, closes #277 2014-10-29 16:51:06 -07:00
Leonardo de Moura
fe4ea48381 feat(library/definitional/projection): add projection generator, closes #257 2014-10-29 13:13:05 -07:00
Leonardo de Moura
0c185fc4ab fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274 2014-10-29 08:57:34 -07:00
Leonardo de Moura
a2ef835809 fix(frontends/lean): squiggle position for unary begin-end block 2014-10-28 23:26:24 -07:00
Leonardo de Moura
83e4c0fcec feat(frontends/lean): hide tactic "types" 
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
 2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508 feat(frontends/lean): modify begin-end semantics, closes #258 2014-10-28 22:15:38 -07:00
Leonardo de Moura
1c2bbcfebc feat(frontends/lean/info_manager): add separator -- when displaying PROOF_STATE info 
This feature was implemented to address issue #259
 2014-10-28 16:39:21 -07:00
Leonardo de Moura
60f32fa709 fix(frontends/lean): begin-end automatic tactic notation bug, fixes #262 2014-10-27 17:12:25 -07:00
Leonardo de Moura
7516fcad97 feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261 2014-10-27 13:16:50 -07:00
Leonardo de Moura
2e5ad274a5 fix(frontends/lean/elaborator): remove invalid assertions 
These assertions became invalid when we changed the behavior of undef
indentifiers at

8e6de93394
 2014-10-27 10:31:09 -07:00
Leonardo de Moura
ee5a982c01 feat(shell/lean): add '--server-trace' flag, closes #264 2014-10-27 10:26:29 -07:00
Leonardo de Moura
d66e5a6c41 fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming 2014-10-26 19:19:45 -07:00
Leonardo de Moura
81dc201bab fix(frontends/lean/elaborator): nested begin-end bug 2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders 2014-10-26 16:11:58 -07:00
Leonardo de Moura
cc6a96e8ba fix(frontends/lean): improve begin-end construct 2014-10-26 15:47:29 -07:00
Leonardo de Moura
aed9a88b38 fix(frontends/lean/parser): save identifier info for undef local 2014-10-26 10:19:44 -07:00
Leonardo de Moura
8e6de93394 fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant 2014-10-26 09:47:11 -07:00
Leonardo de Moura
707584376a fix(frontends/lean/inductive_cmd): include 'induction_on', 'cases_on', and 'rec_on' into .ilean index file 2014-10-25 17:56:22 -07:00
Leonardo de Moura
c7f6a6b94e feat(library/definitional/cases_on): automatically add 'cases_on' 2014-10-25 17:22:02 -07:00
Leonardo de Moura
cdcde661ef feat(library/definitional/induction_on): automatically add 'induction_on' 2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8 feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes 2014-10-25 13:08:59 -07:00
Leonardo de Moura
2bc034da2c feat(kernel/inductive): expose 'get_elim_name' API 2014-10-25 10:47:12 -07:00
Leonardo de Moura
5830da9e2d fix(frontends/lean/tokens): typo 2014-10-24 14:44:59 -07:00
Leonardo de Moura
7a033ac07e feat(frontends/lean): add 'print axioms' command, close #251 2014-10-24 14:35:03 -07:00
Leonardo de Moura
db25f933b0 feat(frontends/lean): use nice names for meta-variables when executing check c and c is a constant 2014-10-24 08:23:26 -07:00
Leonardo de Moura
f027acb5cb fix(frontends/lean): missing type info in expressions nested in tactics 2014-10-23 18:31:05 -07:00
Leonardo de Moura
a6571c3273 feat(frontends/lean): add 'print definition' command 2014-10-23 14:54:15 -07:00
Leonardo de Moura
22ae42d3af fix(frontends/lean/info_manager): use fresh formatter displaying each info object 
The formatter may cache results.
 2014-10-23 14:29:17 -07:00
Leonardo de Moura
20ab59c740 fix(frontends/lean/pp): avoid unnecessary parentheses when pretty printing delimited notation 2014-10-23 14:14:08 -07:00
Leonardo de Moura
212ae0b61c feat(frontends/lean): automatically add 'info' tactic in begin-end blocks 
Actually, the tactic is only added when Lean is in collect-info mode.
 2014-10-23 13:30:04 -07:00
Leonardo de Moura
e750c9b67a feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode 2014-10-23 13:18:30 -07:00
Leonardo de Moura
cadc9b3ff3 feat(frontends/lean/info_manager): add proof_state info 2014-10-23 10:40:07 -07:00
Leonardo de Moura
38a9aa2a98 feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions 2014-10-23 10:26:19 -07:00
Leonardo de Moura
2c330e704e fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures 2014-10-23 10:26:19 -07:00
Leonardo de Moura
f3fdc70400 refactor(library/tactic): add auxiliary module 'library/tactic/elaborate' 2014-10-23 10:26:11 -07:00
Leonardo de Moura
7c62446023 refactor(frontends/lean): remove dead code 2014-10-22 17:39:06 -07:00
Leonardo de Moura
eb2b59ce4f refactor(frontends/lean): remove unnecessary files 2014-10-22 17:33:16 -07:00
Leonardo de Moura
e95c7c5f70 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-22 17:29:50 -07:00
Leonardo de Moura
9a316092d1 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic 2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92 feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics 2014-10-22 17:29:50 -07:00
Leonardo de Moura
7c617955d0 refactor(library/tactic): move 'exact' tactic to separate module 2014-10-22 17:29:44 -07:00
Leonardo de Moura
6b89080b1a feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248 2014-10-21 16:28:36 -07:00
Leonardo de Moura
e24225fabf feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations 2014-10-21 15:39:47 -07:00
Leonardo de Moura
1896e6e273 feat(frontends/lean): allow 'reserve' inside namespaces 2014-10-21 15:39:47 -07:00
Leonardo de Moura
bb953b80aa feat(frontends/lean): reserve notation, closes #95 2014-10-21 15:39:47 -07:00
Leonardo de Moura
2f62a5e887 fix(frontends/lean/info_manager): disable notation pretty printer when displaying OVERLOAD information 
We need that otherwise the Lean emacs mode will display useless overload
information such as:

            [+] int.add : ℤ → ℤ → ℤ
            overloaded with #1 + #0, #1 + #0

Note that this only became an issue after we implemented the new pretty printer
 2014-10-20 22:06:33 -07:00
Leonardo de Moura
8a44dfc1df fix(frontends/lean/pp): bug in pretty printer notation match procedure 2014-10-20 18:58:27 -07:00
Leonardo de Moura
40fb66bf07 feat(frontends/lean): change default precedence to 1 2014-10-20 18:40:55 -07:00
Leonardo de Moura
e2fa981e89 fix(frontends/lean/pp): avoid parentheses around atomic notation 2014-10-20 18:08:13 -07:00
Leonardo de Moura
53a64ac767 refactor(library/tactic): move intros_tactic initialization to intros_tactic module 2014-10-20 17:47:52 -07:00
Leonardo de Moura
3c4419ff23 refactor(library/tactic): move rename_tactic to separate module 2014-10-20 17:41:40 -07:00
Leonardo de Moura
e68007a727 fix(frontends/lean/builtin_tactics): adjust tactics precedence 2014-10-20 17:10:16 -07:00
Leonardo de Moura
9b8f60b739 feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block 
This is useful when debugging proofs.
 2014-10-20 15:59:49 -07:00
Leonardo de Moura
a3aca96cb9 fix(frontends/lean/builtin_exprs): error position 2014-10-20 15:56:58 -07:00
Leonardo de Moura
fd40999909 feat(frontends/lean): uniform unsolved goals "error" position 2014-10-20 15:52:06 -07:00
Leonardo de Moura
7d0100a340 feat(library/tactic): add 'intros' tactic 2014-10-20 15:26:16 -07:00
Leonardo de Moura
33c4715f4c fix(frontends/lean/pp): suppress unnecessary '[annotation]' marks 2014-10-20 11:16:21 -07:00
Leonardo de Moura
f0cc17af87 fix(frontends/lean/elaborator): missing type information when ! operator (aka consume_args) is used 2014-10-20 08:31:36 -07:00
Leonardo de Moura
a1006073d4 feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence 2014-10-19 13:39:06 -07:00
Leonardo de Moura
469368f090 refactor(frontends/lean/scanner): move basic UTF8 procedures to separate module 2014-10-19 13:29:15 -07:00
Leonardo de Moura
4d4bc0551f feat(frontends/lean/pp): minimize number of spaces when pretty printing notation 2014-10-19 13:08:15 -07:00
Leonardo de Moura
ed1afe26bd feat(frontends/lean/pp): support scopedexpr notation in the pretty printer 2014-10-19 12:50:40 -07:00
Leonardo de Moura
f63d47fef3 feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer 2014-10-19 11:16:24 -07:00
Leonardo de Moura
100b3abf1d fix(frontends/lean/pp): bug in notation matching procedure 2014-10-19 10:48:41 -07:00
Leonardo de Moura
d7cc7cbd8c refactor(frontends/lean/pp): remove 'reverse' hack 2014-10-19 09:56:18 -07:00
Leonardo de Moura
eef1cc4ac2 fix(frontends/lean/pp): implicit arguments in notation 2014-10-19 09:04:43 -07:00
Leonardo de Moura
555d26aa61 feat(frontends/lean/pp): take notation declarations into account when pretty printing 
TODO: support foldl/foldr and binders
 2014-10-19 08:41:29 -07:00
Leonardo de Moura
6a31a79265 refactor(frontends/lean/inductive_cmd): move auxiliary method to expr.h 2014-10-18 15:11:26 -07:00
Leonardo de Moura
eb79af98ba feat(frontends/lean/parse_config): add get_notation_entries auxiliary function for returning the list of notation declarations that start with a given head symbol 
This API is need to take notation declarations into account when pretty
printing expressions.
 2014-10-18 11:49:27 -07:00
Leonardo de Moura
f17e67efcb feat(frontends/lean/parse_table): add get_head_index auxiliary function for indexing notation declarations 2014-10-18 10:55:39 -07:00
Leonardo de Moura
3b6b23c921 refactor(kernel/expr): remove silly overloads 2014-10-16 13:37:55 -07:00
Leonardo de Moura
28128e0330 fix(frontends/lean): EXTRA_TYPE info 2014-10-16 12:25:18 -07:00
Leonardo de Moura
8907dd5b91 refactor(frontends/lean): minimize the use of 'set_tag' 2014-10-15 13:17:09 -07:00
Leonardo de Moura
b94d121580 refactor(library): move flycheck "helper" classes to separate module 2014-10-15 09:08:04 -07:00
Leonardo de Moura
e6606ef2ac feat(library/tactic): add 'rename' hypothesis tactic 2014-10-14 18:19:34 -07:00
Leonardo de Moura
fc01edee4d fix(frontends/lean/elaborator): perform translation using "user-level" names 2014-10-14 17:53:24 -07:00
Leonardo de Moura
58c9421bab refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70 2014-10-14 17:18:40 -07:00
Leonardo de Moura
d75a9c840c fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244 2014-10-13 21:08:36 -07:00
Leonardo de Moura
b7c1b348d1 feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration 2014-10-13 20:53:09 -07:00
Leonardo de Moura
9edf780a00 feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem 2014-10-13 18:35:11 -07:00
Leonardo de Moura
2431de542f refactor(frontends/lean/parser): add missing 'const' 2014-10-13 13:07:42 -07:00
Leonardo de Moura
bc70e7244d feat(frontends/lean): add option '-X': discard all proofs after theorems are checked 
This option is useful for generating compact .olean files for web demos
 2014-10-13 10:05:38 -07:00
Leonardo de Moura
698dc0472d fix(frontends/lean/decl_cmds): error messages 2014-10-13 07:17:33 -07:00
Leonardo de Moura
a26618e0f2 feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied 2014-10-12 13:06:00 -07:00
Leonardo de Moura
549f24335e feat(frontends/lean): do not allow coercion definition in sections 2014-10-11 18:41:17 -07:00
Leonardo de Moura
78b8a67015 refactor(library/scoped_ext): sections are just "nameless" namespaces 2014-10-11 17:36:46 -07:00
Leonardo de Moura
158682219f feat(frontends/lean): allow parameters only in contexts 2014-10-11 17:13:56 -07:00
Leonardo de Moura
f984b51291 feat(frontends/lean/notation_cmd): remove the cleanup notation hack 2014-10-11 16:40:26 -07:00
Leonardo de Moura
334a4c84d1 refactor(frontends/lean): do not expose unnecessary functions 2014-10-11 16:40:26 -07:00
Leonardo de Moura
33ad41b93e refactor(frontends/lean): adjust function names to reflect how parameters/variables behave 2014-10-11 15:33:31 -07:00
Leonardo de Moura
ca632cca13 feat(frontends/lean): add 'universe variable' command 
We can declare variables anywhere. So, we must also be able do declare
"universe" variables anywhere. Here is a minimal example that requires
this feature

```
-- We want A and B to be in the same universe
universe variable l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```

The following doesn't work because A and B are in different universes
```
variable A : Type
variable B : Type
definition tst := A = B
```

The following works, but tst is not universe polymorphic, since l is
one *fixed* global universe
```
universe l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
 2014-10-11 14:22:33 -07:00
Leonardo de Moura
1cc8007b9a refactor(frontends/lean): rename parser methods is_section* to is_local* 2014-10-11 10:25:39 -07:00
Leonardo de Moura
b0f8d86f26 feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242 2014-10-10 18:08:03 -07:00
Leonardo de Moura
5e6ff3eef3 fix(frontends/lean/elaborator): bug when reporting error position 2014-10-10 17:31:12 -07:00
Leonardo de Moura
f0523a3465 feat(frontends/lean): namespaces also define scope for variables 2014-10-10 16:21:30 -07:00
Leonardo de Moura
0641ee33ce feat(frontends/lean): allow variables anywhere 2014-10-10 16:16:19 -07:00
Leonardo de Moura
4010767c20 feat(shell): add options --cpp and --discard 2014-10-10 15:55:08 -07:00
Leonardo de Moura
3d65b1c25c fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241 2014-10-10 15:41:55 -07:00
Leonardo de Moura
d61e6fdd89 refactor(frontends/lean/util): add auxiliary function 2014-10-10 15:21:08 -07:00
Leonardo de Moura
402a351937 feat(frontends/lean): add 'universes' command 2014-10-10 08:45:59 -07:00
Leonardo de Moura
052bc6ff20 fix(frontends/lean/elaborator): better specific universe detection 2014-10-09 14:43:07 -07:00
Leonardo de Moura
8947bf4347 feat(frontends/lean): display type of binders, closes #238 2014-10-08 22:54:10 -07:00
Leonardo de Moura
25fd370c51 fix(frontends/lean): bug when using nested sections and parameters 
see tests/lean/run/section4.lean
 2014-10-08 22:23:20 -07:00
Leonardo de Moura
f7bbe09db2 feat(frontends/lean): add helper function mk_section_local_ref 2014-10-08 22:23:20 -07:00
Leonardo de Moura
d445857f56 fix(frontends/lean): change how "as-is" expressions are handled 
Implicit arguments are consumed.
 2014-10-08 22:23:20 -07:00
Leonardo de Moura
0651496bf6 refactor(frontends/lean/notation_cmd): remove unnecessary uses of add_local_expr 2014-10-08 22:23:20 -07:00
Leonardo de Moura
57c85221fe fix(frontends/lean): collect used universe levels after elaboration in the check command 2014-10-08 22:23:19 -07:00
Leonardo de Moura
eab9321a3b fix(frontends/lean): make all variables/parameters visible for 'variables' command 2014-10-08 22:23:19 -07:00
Leonardo de Moura
3b23bec25b feat(frontends/lean): variables/parameters and check commands have access to all section variables/parameters, closes #231 2014-10-08 08:40:55 -07:00
Leonardo de Moura
5b9bd279af chore(frontends/lean/parser): minor cleanup 2014-10-08 08:40:55 -07:00
Leonardo de Moura
744cee8dd8 feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228 2014-10-07 18:02:15 -07:00
Leonardo de Moura
d8572e249d feat(frontends/lean/builtin_cmds): add 'print classes' command 2014-10-07 17:30:57 -07:00
Leonardo de Moura
c31c026f46 feat(frontends/lean/class): accept only inductive datatypes (and records) as classes 2014-10-07 17:30:57 -07:00
Leonardo de Moura
8fa171cb92 refactor(library/unifier): allow general 'unify' procedure to take an initial substitution as argument 2014-10-07 17:30:57 -07:00
Leonardo de Moura
16041e4948 fix(frontends/lean/elaborator): 'as-is' expressions 
The elaborator should not introduce implicit arguments on terms marked
as 'as-is'.
 2014-10-07 16:38:31 -07:00
Leonardo de Moura
531de7990d refactor(frontends/lean/tactic_hint): simplify tactic_hints 2014-10-07 11:34:58 -07:00
Leonardo de Moura
90ece4dd1b feat(frontends/lean): remove tactic hints for specific classes 
The idea is to separate class-instance resolution and tactic framework
as two independent engines.
 2014-10-07 09:44:01 -07:00
Leonardo de Moura
dc92f67588 feat(frontends/lean/server): CLEAR_CACHE forces buffer to be reprocessed 2014-10-06 08:42:20 -07:00
Leonardo de Moura
16562adb87 feat(frontends/lean): add 'coercions' and 'instances' to 'print' command, closes #71 2014-10-05 18:50:48 -07:00
Leonardo de Moura
a9741c5c30 chore(frontends/lean/placeholder_elaborator): indent code 2014-10-04 10:36:10 -07:00
Leonardo de Moura
0a288aec40 chore(frontends/lean/proof_qed_elaborator): remove obsolete comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-04 09:19:33 -07:00
Leonardo de Moura
64f6601fe3 fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost 2014-10-04 09:15:42 -07:00
Leonardo de Moura
bf01cfeec5 fix(frontends/lean): avoid superfluous local references of the form @-1 (@ f), 
This kind of term also confuses the elaborator
 2014-10-04 07:55:32 -07:00
Leonardo de Moura
e71d4548de fix(frontends/lean): universe levels associated with section variables should not be fixed in the section 2014-10-04 07:13:19 -07:00
Leonardo de Moura
b9e7fecb1f fix(frontends/lean/elaborator): style 2014-10-03 16:26:28 -07:00
Leonardo de Moura
a1bb6d6017 refactor(frontends/lean/elaborator): expose elaborator class 2014-10-03 16:10:36 -07:00
Leonardo de Moura
dccf8a3a75 chore(frontends/lean/elaborator): fix field name 2014-10-03 15:34:23 -07:00
Leonardo de Moura
938e12baa1 feat(frontends/lean/notation_cmd): allow local numeric notation 2014-10-03 13:55:57 -07:00
Leonardo de Moura
dbb7f834af refactor(frontends/lean/parser_config): merge notation_ext and mpz_notation_ext 2014-10-03 13:55:57 -07:00
Leonardo de Moura
73eca1ef44 feat(frontends/lean/notation_cmd): notation defined in context overrides existing ones 2014-10-03 13:55:57 -07:00
Leonardo de Moura
c0725d1934 refactor(frontends/lean): remove 'including' expressions 2014-10-03 09:09:27 -07:00
Leonardo de Moura
01d4644026 fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored 2014-10-03 08:52:35 -07:00
Leonardo de Moura
284f300440 feat(frontends/lean): add 'include' and 'omit' commands, closes #184 2014-10-03 07:23:24 -07:00
Leonardo de Moura
6950b4aa9b fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables 2014-10-02 18:29:41 -07:00
Leonardo de Moura
d5cad765a0 feat(frontends/lean): enforce new semantics for section 'variables' 
The library file logic/core/connectives uses the new feature.
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
f006d93794 feat(frontends/lean): section variables occur after section parameters 2014-10-02 17:55:34 -07:00
Leonardo de Moura
0a13e7863a feat(frontends/lean): enforce rule section parameters cannot depend on section variables 2014-10-02 17:55:34 -07:00
Leonardo de Moura
bf081ed431 refactor(kernel): rename var_decl to constant_assumption 
Motivation: it matches the notation used to declare it.
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
4946f55290 refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
f78d831de3 refactor(frontends/lean): remove hardcoded Type', and define it using notation 2014-10-02 14:29:51 -07:00
Leonardo de Moura
4cb54ac825 feat(frontends/lean/elaborator): more strict test for bad universe solution 2014-10-02 14:29:51 -07:00
Leonardo de Moura
98e66586e9 feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit 2014-10-02 14:29:51 -07:00
Leonardo de Moura
db9671d7c3 fix(frontends/lean/decl_cmds): remove assertion that does not hold anymore 2014-10-02 09:19:40 -07:00
Leonardo de Moura
5bd8e9d141 fix(frontends/lean/decl_cmds): allow private transparent definitions 
Example:
section
  universe l
  private definition T := Type.{max 1 l}
  ...
end
 2014-10-02 07:56:01 -07:00
Leonardo de Moura
153e3927ac feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type. 2014-10-01 18:50:17 -07:00
Leonardo de Moura
ead827d6b7 feat(frontends/lean): add ! operator the "dual" of @, closes #220 2014-10-01 17:13:41 -07:00
Leonardo de Moura
c46ec6a548 fix(frontends/lean): missing type information for INFO, fixes #218 2014-10-01 14:29:07 -07:00
Leonardo de Moura
f863d82e69 fix(frontends/lean/pp): pp was not taking into account new namespace name resolution rules, fixes #216 2014-10-01 11:24:45 -07:00
Leonardo de Moura
263b081e69 fix(frontends/lean/inductive_cmd): temporary aliases must take explicit universes into account, fixes #215 2014-10-01 10:24:44 -07:00
Leonardo de Moura
71077f5c89 feat(frontends/lean/parser): allow _ at level expressions 2014-10-01 10:24:44 -07:00
Leonardo de Moura
2730e5163e feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message 
See new test for explanation.
 2014-09-30 18:04:04 -07:00
Leonardo de Moura
486839881c feat(*): use environment fingerprint to detect when the cache cannot be used because the configuration changed, closes #75 
We are not taking into the account the options object yet.
 2014-09-29 18:30:00 -07:00
Leonardo de Moura
530997638a feat(library/definition_cache): store the hashcode of direct dependencies 
Actually we store the has code of their types.
 2014-09-29 18:30:00 -07:00
Leonardo de Moura
113879a7dd feat(frontends/lean/server): sort exact matches by size in FINDP 2014-09-29 16:44:55 -07:00
Leonardo de Moura
334977b8bd fix(frontends/lean/info_manager): crash when accessing INFO in the end of the file 2014-09-29 16:44:55 -07:00
Leonardo de Moura
0d6d746d98 feat(frontends/lean): check modification time of imported files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-29 15:17:27 -07:00
Leonardo de Moura
6630ed8165 fix(frontends/lean/decl_cmds): warning message when compiling with clang++ 2014-09-29 12:34:00 -07:00
Leonardo de Moura
21be308884 feat(frontends/lean/inductive_cmd): infer implicit argument annotation after elaboration, allow user to disable it by using '()' annotation, closes #210 2014-09-29 11:11:17 -07:00
Leonardo de Moura
9c55bbb871 feat(frontends/lean/elaborator): report an error when Type becomes a Prop after elaboration, closes #208 2014-09-29 08:18:10 -07:00
Leonardo de Moura
fbbd1d25cd chore(frontends/lean/decl_cmds): disable incorrect warning message produced by gcc 2014-09-28 12:32:47 -07:00
Leonardo de Moura
397395bbc9 feat(frontends/lean): allow user to associate priorities to class-instances, closes #180 2014-09-28 12:20:42 -07:00
Leonardo de Moura
9f6a8827e0 refactor(*): use name_map 2014-09-28 10:23:11 -07:00
Leonardo de Moura
33fe409dc6 chore(frontends/lean/placeholder_elaborator): cleanup 2014-09-27 22:24:36 -07:00
Leonardo de Moura
22e47430b5 feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore 2014-09-27 21:50:39 -07:00
Leonardo de Moura
8e7aac1eb4 fix(frontends/lean): add 'eval' command 2014-09-26 20:16:03 -07:00
Leonardo de Moura
69f50adb2e fix(frontends/lean/server): must save the starting environment/options when reprocessing file, fixes #209 2014-09-26 15:36:47 -07:00
Leonardo de Moura
a3e38dc8a0 feat(frontends/lean): allow users to define "numeral notation" 2014-09-26 14:55:23 -07:00
Leonardo de Moura
6bf905aea8 fix(frontends/lean/pp): do not invoke type checker on expressions 
containing free variables.

This could happened when the pretty printer was used from Lua to print
nested subterms
 2014-09-26 09:38:36 -07:00
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