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

4159 commits

Author SHA1 Message Date
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
Favonia
2d69444da5 fix(cmake/Modules/cpplint.py): python3 compatible without six 2015-01-22 13:05:56 -08:00
Favonia
c1bfafd2a7 style(cmake/Modules/cpplint.py) 2015-01-22 13:05:56 -08:00
Favonia
a2f30322a9 fix(cmake/Modules/cpplint.py): delete ending colon 
Delete the erroneous ending colon.
 2015-01-22 13:05:56 -08:00
Favonia
51c771f334 revert(cmake/Modules/cpplint.py): roll back to python2 version 
This reverts commit 65cc4d3c08.
 2015-01-22 13:05:42 -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
Soonho Kong
65cc4d3c08 fix(cmake/Modules/cpplint.py): roll back to python2 version 2015-01-21 19:26:38 -05:00
Leonardo de Moura
12674114a4 feat(shell): set default behavior to "trusted" 
closes #402
 2015-01-21 16:25:09 -08:00
Favonia
073c1d1c31 feat(python): add python 3 compatibility 
Add Python 3 compatibility through python-six library.

Closes #393.
 2015-01-21 17:13:55 -05:00
Leonardo de Moura
1d6ff5f761 feat(library/definitional/projection): throw exception if unsupported case occurs 
The user can workaround it by using trust-level 0 (i.e., no option -t num or -T)
 2015-01-20 17:42:34 -08:00
Leonardo de Moura
01ce57e52e feat(library/definitional/projection): add projection macro 2015-01-20 16:21:50 -08:00
Leonardo de Moura
b6750e9d29 feat(library/util): add auxiliary functions 2015-01-20 15:44:58 -08:00
Leonardo de Moura
c51e2ac428 feat(kernel/type_checker): expose get_arity function 2015-01-20 14:25:07 -08:00
Leonardo de Moura
c43b2c8640 feat(kernel/extension_context): add auxiliary methods 2015-01-20 14:23:10 -08:00
Leonardo de Moura
8355ed55d7 refactor(library/definitional/projection): remove dead code 2015-01-20 13:40:09 -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
5ab7ff62b5 feat(CMakeLists): add --Trust option when building standard/hott libraries 2015-01-20 11:11:35 -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
858d21f20b feat(library/definitional/projection): store projection information 2015-01-18 16:26:56 -08:00
Soonho Kong
901c9bf67a refactor: rename ltags => leantags 
fix #394
 2015-01-18 13:44:41 +09: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
6c07ca5d41 perf(library/print): improve is_used_name 2015-01-15 19:01:13 -08:00
Leonardo de Moura
c6290f01d0 perf(kernel/free_vars): improve has_free_var 2015-01-15 18:42:56 -08:00
Leonardo de Moura
f397da111a perf(kernel/error_msgs): avoid unnecessary work 2015-01-15 18:32:52 -08:00
Leonardo de Moura
ce0b1d17a2 perf(kernel/free_vars): improve has_free_var 2015-01-15 18:31:43 -08:00
Leonardo de Moura
ddcc8de09e fix(shell/lean): catch errors when loading bad cache file 2015-01-15 18:06:22 -08:00
Leonardo de Moura
30817aa2b1 feat(emacs): allow user to provide extra commands to lean-server 2015-01-15 16:54:55 -08:00
Leonardo de Moura
907f90096e feat(kernel): add memory consumption checks at replace_fn and for_each_fn 2015-01-15 16:54:55 -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
3a865e95fe feat(shell/lean): add option '-M' to limit amount of memory consumed 2015-01-15 16:54:55 -08:00
Leonardo de Moura
5c9a277dea feat(CMakeLists): include runtime files in Windows binary distribution package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-01-14 12:37:25 -08:00
Leonardo de Moura
730e038dd3 feat(CMakeLists): add basic example to binary distribution package 2015-01-14 10:39:07 -08:00
Leonardo de Moura
0509baa64a feat(CMakeLists): add README file for binary distribution packages 2015-01-14 10:35:51 -08:00
Leonardo de Moura
ee98523c2a feat(shell/lean): add option '-T' alias for '-t 1025' 2015-01-14 10:21:57 -08:00
Leonardo de Moura
3813aeede5 fix(util/lean_path): relative position of library files in binary 
distribution packages
 2015-01-14 10:14:17 -08:00
Leonardo de Moura
c9132648a2 feat(CMakeLists): include HoTT library in binary package 2015-01-14 10:00:35 -08:00
Leonardo de Moura
ef529c660f fix(library/definitional/no_confusion): mark no_confusion as reducible 
Auxiliary definitions should be marked as reducible
 2015-01-13 18:44:47 -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
e9338669dc feat(library/definitional/equations): show implicit arguments (by default) in equations compiler error messages 2015-01-13 13:30:12 -08:00
Leonardo de Moura
41935906a8 chore(frontends/lean): use update_if_undef 2015-01-13 13:02:14 -08:00
Leonardo de Moura
e5a8c67d22 fix(library/definitional/equations): assertion violation 2015-01-13 11:57:14 -08:00
Leonardo de Moura
1fbfe59a9a feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line 
closes #391
 2015-01-13 11:14:44 -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
a3bc1b0cd5 fix(library/definitional/equations): add more equation validation to avoid obscure error message 2015-01-09 18:52:21 -08:00
Leonardo de Moura
2e4a2451e6 refactor(library/reducible): simplify reducible/irreducible semantics 2015-01-08 18:52:18 -08:00
Leonardo de Moura
698754b2bb feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases 2015-01-08 12:00:47 -08:00
Leonardo de Moura
4fef19230d feat(util/sexpr/options): add update_if_undef method 2015-01-08 11:55:30 -08:00
Leonardo de Moura
f344dd75c4 feat(library/pp_options): add get_pp_purify_locals_name 2015-01-08 11:55:08 -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
5c118127ae fix(library/definitional/equations): memory access violation 2015-01-07 17:06:41 -08:00
Leonardo de Moura
597f7385e8 fix(library/unifier): incorrect fix 2015-01-07 16:57:02 -08:00
Leonardo de Moura
15b5344626 feat(library/definitional/equations): copy tags 2015-01-07 14:00:46 -08:00
Leonardo de Moura
2990a6d029 fix(library/unifier): missing "set_conflict" in process_delta 2015-01-07 12:41:01 -08:00
Leonardo de Moura
a9b6e20a22 fix(frontends/lean): save equations position 2015-01-06 15:55:04 -08:00
Leonardo de Moura
760dc2162a chore(library/definitional/equations): cleanup 2015-01-06 14:53:21 -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
559ee3e3e1 fix(util/buffer): bug in expand method 
fixes #385
 2015-01-06 11:42:40 -08:00
Leonardo de Moura
5f182dc1cc fix(util/lean_path): memory leak 2015-01-06 10:22:45 -08:00
Leonardo de Moura
c33928f202 fix(library/pp_options): memory leak 2015-01-06 10:22:23 -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
322cdb8a98 feat(library/definitional/equations): add 'equations_result' macro used to wrap multiple functions being defined by recursive equations 
This is only useful when compiling "mutually recursive" functions.
 2015-01-05 19:09:20 -08:00
Leonardo de Moura
3325d791de fix(library/definitional/equations): bug in recursive application elimination 2015-01-05 17:17:14 -08:00
Leonardo de Moura
eedc31f7e9 fix(library/definitional/equations): bug in "complete" transition 2015-01-05 16:27:29 -08:00
Leonardo de Moura
3889b60152 feat(library/definitional/equations): allow inductive datatype parameters in recursive equations 2015-01-05 15:56:28 -08:00
Leonardo de Moura
6eba4b4ac1 chore(library/definitional/equations): cleanup 2015-01-05 13:57:13 -08:00
Leonardo de Moura
b46c377aa2 feat(library/definitional/equations): add "complete" transition for overlapping patterns 2015-01-05 11:49:27 -08:00
Leonardo de Moura
fdef3e5407 feat(library/definitional/equations): add support for reflexive datatypes in the definitional package 2015-01-05 11:13:35 -08:00
Leonardo de Moura
5e228d92d2 fix(library/definitional/equations): missing case 2015-01-04 20:49:53 -08:00
Leonardo de Moura
576c053c25 fix(library/tactic/inversion_tactic): bug at implementation_list update 2015-01-04 19:56:10 -08:00
Leonardo de Moura
faf78ce3e6 feat(library/definitional/equations): brec_on compilation 2015-01-04 17:45:13 -08:00
Leonardo de Moura
98a856373d feat(library/util): add dec_level auxiliary procedure 2015-01-04 13:25:58 -08:00
Leonardo de Moura
926c140e17 fix(library/definitional/equations): fix clang compilation problems 2015-01-04 10:18:19 -08:00
Leonardo de Moura
bdfa919098 feat(library/definitional/equations): add brec_on based compilation 2015-01-03 22:23:37 -08:00
Leonardo de Moura
42354cd4fa feat(library/locals): add auxiliary templates 2015-01-03 22:23:08 -08:00
Leonardo de Moura
376126241e fix(library/definitional/equations): typo and bug 2015-01-03 15:29:34 -08:00
Leonardo de Moura
21a9cd58a3 fix(library/definitional/equations): bug when compiling in proof relevant kernels 2015-01-02 23:17:33 -08:00
Leonardo de Moura
7f7d318b22 feat(library/definitional/equations): add dependent pattern matching compilation 2015-01-02 22:06:40 -08:00
Leonardo de Moura
762a515a5b feat(library/tactic/inversion_tactic): mark new arguments that have been "unified" into terms 2015-01-02 22:02:15 -08:00
Leonardo de Moura
3fb2d8bbc0 feat(library/tactic/inversion_tactic): use the "simpler" compilation approach in more cases 
The approach implemented in the commit 8974d70c11ef7b9b2c5d can be
extended to indexed inductive families. See comments in the code.
 2015-01-01 19:33:15 -08:00
Leonardo de Moura
be9e2500ce feat(library/tactic/inversion_tactic): add more efficient "compilation" for non-indexed inductive datatypes 2015-01-01 19:33:14 -08:00
Leonardo de Moura
9be67bc0b1 feat(util/buffer): add method erase_elem 2015-01-01 19:33:14 -08:00
Leonardo de Moura
57490a6431 feat(library/tactic/inversion_tactic): avoid unnecessary eq.rec's 2015-01-01 19:33:14 -08:00
Leonardo de Moura
58f052b1bb fix(library/normalize): unitialized variable 2015-01-01 19:33:14 -08:00
Leonardo de Moura
761810f350 feat(library/tactic/inversion_tactic): generate auxiliary information 2015-01-01 19:33:14 -08:00
Leonardo de Moura
e76ef18980 feat(util/name_map): add rename_map 2015-01-01 19:33:14 -08:00
Leonardo de Moura
1f13bfa4f7 feat(library/tactic/inversion_tactic): add inversion::apply procedure 
The new procedure is essentially a "customized" version of the
inversion (aka cases) tactic for the equations package
 2015-01-01 19:33:14 -08:00
Soonho Kong
f370871574 fix(emacs/lean-syntax): highlight axioms 
fix #382
 2014-12-30 14:25:19 -05: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
d082fb7402 fix(shell/lean): crash when trying to read file without extension 2014-12-28 14:22:36 -08:00
Leonardo de Moura
1d79cb9c07 fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library 2014-12-22 09:40:15 -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
5efadb09cc feat(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT library 
This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.

The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
 2014-12-21 15:19:25 -08:00
Leonardo de Moura
677ec2a2fe feat(library/tactic/inversion_tactic): adjust inversion tactic to HoTT lib 2014-12-20 11:32:27 -08:00
Leonardo de Moura
7a75325416 feat(kernel/abstract): add new abstract_local procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-12-20 11:31:48 -08:00
Leonardo de Moura
2070ac849c feat(library/util): add get_intro_rule_names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-12-20 11:31:48 -08:00
Leonardo de Moura
d9d822baa7 feat(library/tactic/class_instance_synth): add mk_hset_instance procedure 2014-12-19 22:00:25 -08:00
Leonardo de Moura
8c63045492 feat(library/util): add more auxiliary procedures 2014-12-19 22:00:25 -08:00
Leonardo de Moura
d6f79423e9 feat(library/tactic/class_instance_synth): add mk_class_instance procedures 2014-12-19 20:09:09 -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
9bd74689be feat(library/util): add mk_refl 2014-12-19 13:54:12 -08:00
Leonardo de Moura
a97bef7df2 feat(library/util): add mk_heq 2014-12-19 13:54:12 -08:00
Leonardo de Moura
1ca8723c54 refactor(library/util): allow mk_telescopic_eq to be used with (terms, locals) 2014-12-19 13:54:12 -08:00
Leonardo de Moura
aedf74e80a feat(util/list): add to_list from buffer 2014-12-19 13:54:12 -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
5a9cd9eed4 fix(library/normalize): bug in the "eval" command 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
f0b002d5a7 fix(library/aliases): aliases in sections and contexts 2014-12-13 14:57:15 -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
eb184984c0 feat(util/buffer): add insert method 2014-12-11 19:31:54 -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
8b3e97d285 feat(kernel/type_checker): add ensure_type variant 2014-12-11 17:32:17 -08:00
Leonardo de Moura
e897bbdeb9 feat(library/util): add auxiliary functions for creating tuples (using sigma types) 2014-12-11 17:31:47 -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
2867789bec fix(library/unifier): handle missing first-order flex-flex case 2014-12-10 22:11:30 -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
6736f58548 refactor(library/definitional/util): cleanup 2014-12-07 16:41:28 -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
93d5d43f71 fix(util/lean_path): typo 2014-12-05 22:15:07 -08:00