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

1355 commits

Author SHA1 Message Date
Leonardo de Moura
7fc216183e feat(library/tactic): produce better error message when a tactic fails 
closes #348
 2015-02-16 18:42:15 -08:00
Leonardo de Moura
4248ad644d fix(frontends/lean): priority expressions parser 2015-02-14 12:26:06 -08:00
Leonardo de Moura
c532a4a4b8 feat(frontends/lean/server): add option 'auto_completion.max_results' 
Default value is 100
 2015-02-13 12:58:11 -08:00
Leonardo de Moura
db71a29c81 feat(frontends/lean/parse_rewrite_tactic): improve esimp tactic 2015-02-13 12:22:17 -08:00
Leonardo de Moura
8ffadce4ab feat(frontends/lean): add "premise" and "premises" command 
It is just an alternative notation for "variable" and "variables"

closes #429
 2015-02-11 18:46:03 -08:00
Leonardo de Moura
30d20e8029 chore(frontends/lean/parser): remove dead code 2015-02-11 16:29:58 -08:00
Leonardo de Moura
04e92e1e96 feat(frontends/lean/parser): reject explicit universe levels in variables and parameters 
This modification was motivated by issue #427
 2015-02-11 16:25:06 -08:00
Leonardo de Moura
a35cce38b3 feat(frontends/lean): new semantics for "protected" declarations 
closes #426
 2015-02-11 14:09:25 -08:00
Leonardo de Moura
eceed03044 feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command 2015-02-11 11:02:59 -08:00
Leonardo de Moura
1832fb6f54 feat(*): uniform metaclass names, metaclass validation at 'open' command 2015-02-11 10:35:04 -08:00
Leonardo de Moura
9d1cd073c5 feat(frontends/lean): add 'print metaclasses' command 2015-02-11 10:13:20 -08:00
Leonardo de Moura
60fca7575c fix(frontends/lean/pp): bugs when pretty printing abbreviations 2015-02-10 19:06:09 -08:00
Leonardo de Moura
bd304e1911 chore(*): style 2015-02-10 18:31:17 -08:00
Leonardo de Moura
43f849bf95 feat(frontends/lean/pp): add support for abbreviations in the pretty printer 
closes #365
 2015-02-10 18:27:02 -08:00
Leonardo de Moura
565cd835af feat(frontends/lean): add 'abbreviation' command 2015-02-10 17:31:40 -08:00
Leonardo de Moura
014271da8b feat(frontends/lean): better error messages for ill-terminated declarations 2015-02-10 14:38:00 -08:00
Leonardo de Moura
666f697d24 fix(frontends/lean/builtin_exprs): 'using' expression should make local constant available for tactics 2015-02-08 17:27:22 -08:00
Leonardo de Moura
c04c0e8381 refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation 2015-02-07 15:19:41 -08:00
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