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

4355 commits

Author SHA1 Message Date
Leonardo de Moura
264cedb3a6 fix(frontends/lean/rewrite_tactic): incorrect assertion 2015-02-05 20:02:49 -08:00
Leonardo de Moura
e17ba27596 fix(library/tactic/rewrite_tactic): adjust the behavior of class resolution in rewriter 
The solution is not very satisfactory. I should investigate it more.
 2015-02-05 19:08:47 -08:00
Leonardo de Moura
ffe0d1186e feat(library/tactic/rewrite_tactic): add "reduce_to" step at rewrite tactic 2015-02-05 13:59:55 -08:00
Leonardo de Moura
116c65bff5 feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic 2015-02-05 13:42: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
7cdc88701d feat(library/tactic/rewrite_tactic): add "reduction" step to rewrite tactic 2015-02-05 13:16:05 -08:00
Leonardo de Moura
808521223b feat(library/tactic/rewrite_tactic): support constant unfolding in rewrite tactic 2015-02-05 12:58:30 -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
d6958be7e7 fix(library/tactic/location): replace cache must not be used when only a subset of all occurrences should be replaced at replace_occurrences 2015-02-05 10:50:40 -08:00
Leonardo de Moura
bc8bb1dbd3 feat(kernel/replace_fn): add use_cache flag to replace function 2015-02-05 10:49:18 -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
941b493835 chore(library/tactic/rewrite_tactic): modify param name 2015-02-05 10:04:03 -08:00
Leonardo de Moura
0abfa30ead fix(library/tactic/rewrite_tactic): elaboration bug in the rewrite tactic steps/elements 2015-02-05 10:01:18 -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
14c72e82f6 feat(library/tactic/rewrite_tactic): add support for rewriting hypotheses 2015-02-04 20:04:19 -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
55fb678db2 fix(library/tactic/location): clang++ 3.3 compilation problem 2015-02-04 18:48:23 -08:00
Leonardo de Moura
42c2f7eb11 fix(library/tactic/rewrite_tactic): memory leak 2015-02-04 18:40:11 -08:00
Leonardo de Moura
89fde9d829 feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic 
The idea is to avoid nontermination.
 2015-02-04 16:13:15 -08:00
Soonho Kong
ca16381892 feat(bin): add linja.in and LEAN_BIN_DEP cmake option 
see the discussion in issue #422
 2015-02-04 15:46:08 -08:00
Leonardo de Moura
dc297865d4 chore(library/tactic/rewrite_tactic): fix compilation warnings 2015-02-04 15:34:02 -08:00
Leonardo de Moura
ee079d12f4 feat(library/tactic/rewrite_tactic): remove trivial goal in rewrite_tactic 2015-02-04 15:29:52 -08:00
Leonardo de Moura
f0fac1ae0e feat(library/constants): add eq.intro 2015-02-04 15:27:18 -08:00
Leonardo de Moura
e5381679d6 feat(library/tactic/rewrite_tactic): rewrite goal 2015-02-04 15:17:58 -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
09818adf90 feat(library/tactic/rewrite_tactic): elaborate rewrite rule using unifier 2015-02-04 13:51:32 -08:00
Leonardo de Moura
49323ab598 feat(library/util): add mk_symm 2015-02-04 13:44:55 -08:00
Leonardo de Moura
ccae014ef9 feat(library/tactic/rewrite_tactic): ignore inst_implicit arguments when matching applications of declarations which contain them 2015-02-04 12:14:47 -08:00
Leonardo de Moura
0e05c239a5 feat(library/tactic/rewrite_tactic): add custom matcher pluging for rewriter 2015-02-04 11:51:39 -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
d6a7ec4621 chore(library/tactic/rewrite_tactic): fix style 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
180cda304e feat(library/tactic): add rewrite tactic skeleton 
The tactic has not been implemented yet, but this commit adds all the
support for storing arguments, serializing and deserializing them.
 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
8a78adc9af feat(library/tactic): add auxiliary object "location" 
This object will used to specify the scope of application of tactics
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
2a6ccb252e test(tests/lean/extra): add regression tests for issue #422 2015-02-04 10:55:03 -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
420da8fd3f feat(library/projection): store bit saying whether a projection is for a class or not. 2015-02-04 08:54:20 -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
0e06f4aedc feat(library/match): extend match_plugin interface 2015-02-03 18:10:38 -08:00
Leonardo de Moura
44e575c895 feat(library/match): improve match_app_core 2015-02-03 17:37:22 -08:00
Leonardo de Moura
790fd9c24b chore(library/match): remove unused procedure 2015-02-03 15:20:26 -08:00
Leonardo de Moura
f79f43c702 refactor(library/match): use "special" meta-variables instead of free variables to represent placholders in the higher-order matcher 2015-02-03 15:15:04 -08:00
Leonardo de Moura
fc6d9878c9 refactor(kernel): add expr_cache 
It is the old instantiate_metavars_cache.
 2015-02-03 14:59:55 -08:00
Jeremy Avigad
dc7b432482 feat(src/emacs/README.md): tell user that packages will be installed automatically. Closes #423. 2015-02-03 13:50:59 -08:00
Jeremy Avigad
875869fdbc fix(src/emacs/README.md): make minor grammatical corrections 2015-02-03 13:50:59 -08:00
Leonardo de Moura
45e62031e2 fix(library/match): bug in matcher 2015-02-03 13:46:19 -08:00
Leonardo de Moura
9d1e312c12 test(tests/lean/extra): add extra tests for 'print' command 2015-02-01 20:20:26 -08:00
Leonardo de Moura
7d9d89bae6 test(tests/lean/extra): add test for saving recursive equation pre-terms 2015-02-01 19:49:14 -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
4c7a17cc4a refactor(library/tactic/class_instance_synth): move has_expr_metavar_relaxed to util 2015-02-01 10:59:27 -08:00
Leonardo de Moura
c311e0aba6 chore(library/tactic/inversion_tactic): cleanup 2015-02-01 10:47:32 -08:00
Leonardo de Moura
143143e94c fix(library/tactic/inversion_tactic): missing normalization step in the inversion_tactic 2015-02-01 10:38:30 -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
27741e4fd7 chore(CMakeLists.txt): move Lean logo to make sure we can test leanemacs without installing Lean 2015-01-31 17:38:49 -08:00
Leonardo de Moura
099111db32 fix(CMakeLists.txt): option ==> set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-01-30 14:49:20 -08:00
Leonardo de Moura
fbb543fdcf feat(CMakeLists.txt): add alternative image formats 2015-01-30 14:26:46 -08:00
Leonardo de Moura
6456c2b89a feat(CMakeLists.txt): add leanemacs.bat for Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-01-30 14:16:57 -08:00
Soonho Kong
7bed63a03e doc(emacs/README.md): fix typos 
[skip ci]
 2015-01-30 16:10:21 -05:00
Leonardo de Moura
c8cb9aa3d2 fix(emacs/load-lean): typo 2015-01-30 13:05:30 -08:00
Leonardo de Moura
2c926478dd feat(bin): add leanemacs startup script 2015-01-30 13:05:30 -08:00
Leonardo de Moura
9910547913 feat(emacs): add script for loading lean mode and its dependencies 2015-01-30 13:05:30 -08:00
Leonardo de Moura
a57251913a feat(emacs): assume lua-mode and mmm-mode are available 2015-01-30 13:05:30 -08:00
Leonardo de Moura
d0ce4cf62f fix(CMakeLists.txt): path to ninja 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-01-30 10:37:49 -08:00
Leonardo de Moura
a44fec6eb4 fix(CMakeLists.txt): path to ninja 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-01-30 10:32:35 -08:00
Leonardo de Moura
1ee52a3ddc feat(CMakeLists.txt): include ninja in Windows binary distribution package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-01-30 09:59:55 -08:00
Leonardo de Moura
7c59c959db fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms" 2015-01-30 09:52:42 -08:00
Soonho Kong
d98f04fd3a chore(emacs/README.md): add numbering on configuration 
[skip ci]
 2015-01-30 03:08:11 -05:00
Soonho Kong
04249a292c feat(emacs/README.md): add per-installation-method configurations 2015-01-30 03:05:35 -05:00
Soonho Kong
ce0aed12ec fix(emacs/Cask): add GNU package repository 
Related issue #410
 2015-01-30 02:52:55 -05:00
Soonho Kong
d69505a092 doc(emacs/README.md): add GNU package repository 
flycheck uses let-alist package which is in GNU repository. @awody reported a problem and I hope that this can help (I'll test it later).

Reference: https://github.com/flycheck/flycheck/issues/551

Related issue: #410
 2015-01-30 02:52:05 -05:00
Leonardo de Moura
f04e462bf3 test(tests/lean/interactive): add more tests for lean server 2015-01-29 16:30:07 -08:00
Leonardo de Moura
e9e1f86b7f fix(library/app_builder): many bugs, add use_cache option, add tests 2015-01-29 15:30:31 -08:00
Leonardo de Moura
e6f022e3f2 fix(library/match): index out of bounds 2015-01-29 14:41:38 -08:00
Leonardo de Moura
b5d1f4e54c feat(library/match): add low-level match API 2015-01-29 14:09:09 -08:00
Leonardo de Moura
f587cc3e1d feat(library/app_builder): expose app_builder API in Lua 2015-01-29 11:38:56 -08:00
Leonardo de Moura
5efd91e435 fix(library/app_builder): missing initialization 2015-01-29 11:38:28 -08:00
Leonardo de Moura
5bb2a41c64 feat(library/reducible): expose Lua API for reducible hints 2015-01-29 10:37:15 -08:00
Leonardo de Moura
4cf2dcaa7e feat(library/app_builder): add helper class for creating applications efficiently using type inference 
The idea is to use this class in the simplifier.
For example, we will use to create: symmetry, reflexivity, transitivity
and congruence proof steps.
 2015-01-28 18:40:21 -08:00
Leonardo de Moura
4e08cc0659 feat(library/match): add flag for tracking whether matcher assigned anything 2015-01-28 18:39:50 -08:00
Leonardo de Moura
dbc8e9e13a refactor(*): add method get_num_univ_params 2015-01-28 17:22:18 -08:00
Leonardo de Moura
5aaade47d8 feat(library/match): add new API 2015-01-28 16:42:42 -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
1119a8018a fix(util/buffer): destructor was not being invoked at erase and erase_elem 
This bug was producing a weird memory leak in the definition package.
The methods erase and erase_elem are not used very often. This is why
this bug was never detected.
 2015-01-27 18:48:02 -08:00
Leonardo de Moura
ad4c7c20f9 fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term 2015-01-27 11:22:14 -08:00
Leonardo de Moura
1dbe4b8fb7 feat(kernel/extension_context): add auxiliary method is_def_eq 2015-01-27 11:17:54 -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
a1eeb0a6a1 fix(library/print): typo in is_used_name 
closes #408
 2015-01-25 08:58:08 -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
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
Leonardo de Moura
d09bc95eaf feat(emacs): add Type0 highlight 2014-12-05 22:14:28 -08:00
Leonardo de Moura
effbf78d36 fix(shell): use --server for .hlean files 2014-12-05 16:13:29 -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
d52fc83274 fix(build): clean-olean target should also clean HoTT library 2014-12-05 14:42:37 -08:00