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

4109 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