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

1086 commits

Author SHA1 Message Date
Leonardo de Moura
76477aedd1 refactor(kernel): move is_stuck predicate to converter 2015-06-22 11:37:14 -07:00
Leonardo de Moura
54496709a2 refactor(kernel/default_converter): add virtual method reduce_def_eq 
The idea is to allow us to customize the default converter outside of
the kernel.
 2015-06-22 10:04:19 -07:00
Leonardo de Moura
a518a45239 refactor(kernel/default_converter): separate lazy_delta_reduction procedure 2015-06-22 08:45:05 -07:00
Leonardo de Moura
3626bd83bf refactor(util/sexpr/format): remove format constructors using std::initializer_list 
For some reason lean.js (Lean compiled using emscripten) crashes when
this kind of constructor is used.
 2015-06-20 14:02:18 -07:00
Leonardo de Moura
accc9dc38b chore(util/sexpr/format): remove unnecessary method 2015-06-19 20:11:42 -07:00
Leonardo de Moura
70fc05294b refactor(library/local_context): avoid hack in local_context 2015-06-18 15:41:00 -07:00
Leonardo de Moura
14c33c4e01 feat(kernel/error_msgs): add workaround for issue #669 
This issue should fix the new problem reported at #669.
It only disables beta-reduction in the pretty printer for application
type mismatch at (f n) when f is a lambda expression.
 2015-06-17 12:00:25 -07:00
Leonardo de Moura
d8620ef4c9 fix(kernel,library,frontends/lean): improve error messages 
see #669
 2015-06-14 19:44:00 -07:00
Leonardo de Moura
25cbc5c154 fix(kernel/expr): remove 'cast_binder_info' 
We should put it back when we decide to implement it.
We also fix the bogus comment at src/frontends/lean/parser.cpp.

see issue #667
 2015-06-11 18:11:22 -07:00
Leonardo de Moura
8b062b4448 feat(kernel/default_converter): add support for stuck terms at try_eta_expansion_core 2015-06-10 15:19:39 -07:00
Leonardo de Moura
f7dd85a935 chore(*): fix 'breif' typos 2015-06-08 16:54:55 -07:00
Leonardo de Moura
496189feed feat(kernel/default_converter): cache failures for (f t =?= f s) heuristic 
See item 4 at
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/oJXwW5wT2Ds/d1Dgr8B-pE0J

See also
https://github.com/leanprover/lean/pull/659
 2015-06-08 10:41:30 -07:00
Leonardo de Moura
0e099b5fd8 feat(library/tactic/rewrite_tactic): apply beta&eta reduction before rewriting steps, add option 'rewrite.beta_eta' (default true) to control new feature. 2015-06-06 20:43:52 -07:00
Leonardo de Moura
d0d3f9bb41 refactor(kernel,library,frontends/lean): add helper functions, and cleanup collect_locals 2015-06-05 17:29:36 -07:00
Leonardo de Moura
4d52d4c790 fix(library/init/quot): prove quot.exact 2015-06-05 08:04:55 -07:00
Floris van Doorn
ff01774fd7 renaming(hit): rename type_quotient to quotient, and quotient to set_quotient 
This renaming is because type_quotient is a nonstandard name.  I've had a discussion with Egbert
Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'.  I had to
make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid
name clash the standard library quotient, although I don't know whether that name clash would
matter).
 2015-06-04 20:14:13 -04:00
Leonardo de Moura
7a0e198147 feat(kernel,frontends/lean/builtin_cmds): allow kernel extensions to report their builtin constants 2015-05-29 16:28:16 -07:00
Leonardo de Moura
0ceedbe69e fix(library/normalize): fixes #640 2015-05-29 15:58:59 -07:00
Leonardo de Moura
004ea80e65 fix(library/tactic/rewrite_tactic): apply beta reduction when selecting patterns 2015-05-24 18:44:30 -07:00
Leonardo de Moura
f830bf54c2 refactor(*): clarify name_generator ownership 2015-05-21 14:32:36 -07:00
Leonardo de Moura
6a87239a5d chore(kernel/justification): fix compilation warning 2015-05-21 10:13:44 -07:00
Leonardo de Moura
76e7f2e7d8 feat(kernel/justification): make sure the code does not depend on the argument order of evaluation generated by a compiler 
see issue #618
 2015-05-21 07:42:10 -07:00
Leonardo de Moura
d5da659be7 feat(frontends/lean/elaborator): include overload information in error messages 2015-05-20 17:21:27 -07:00
Leonardo de Moura
bd28396be0 feat(kernel): transparent theorems 
closes #576
 2015-05-09 11:42:29 -07:00
Leonardo de Moura
f63c2d9393 feat(kernel/inductive/inductive): for datatypes that support K, we should try K before normalizing the major premise 2015-05-09 11:23:10 -07:00
Leonardo de Moura
d217655a62 fix(kernel/quotient/quotient): bug in reduction rule for quot.ind 2015-05-09 09:07:03 -07:00
Leonardo de Moura
cf7e60e5a6 refactor(kernel): remove "opaque" field from kernel declarations 
see issue #576
 2015-05-08 16:06:16 -07:00
Leonardo de Moura
57ea660963 refactor(*): start process for eliminating of opaque definitions from the kernel 
see issue #576
 2015-05-08 16:06:04 -07:00
Leonardo de Moura
061e26157e fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
Leonardo de Moura
45c8cdc626 fix(kernel/default_converter): discard constraints when optimization fails 2015-05-07 15:02:29 -07:00
Leonardo de Moura
16b7bc3922 fix(kernel/default_converter): broken optimization 
we must also check the universe levels when applying the optimization for
constraints of the form:

            f.{l_1 ... l_k} a_1 ... a_n  =?= f.{l_1' ... l_k'} b_1 ... b_n

The optimization tries to avoid unfolding f if we can establish that
a_i is definitionally equal to b_i for each i in [1, n]

closes #581
 2015-05-06 18:32:41 -07:00
Leonardo de Moura
701b0ae66f feat(library): export environment in textual format 
closes #577
 2015-05-04 18:05:00 -07:00
Leonardo de Moura
91abba3c3d refactor(kernel): rename method 2015-04-29 11:46:27 -07:00
Leonardo de Moura
b98c109f73 fix(kernel/hits/hits): bug in reduction rule 
closes #564
 2015-04-29 10:01:46 -07:00
Leonardo de Moura
051615712c fix(kernel/quotient/quotient): bug in reduction rule 2015-04-29 10:01:17 -07:00
Leonardo de Moura
16f237f042 feat(kernel/inductive): remove problematic check 
see discussion at issue #563

closes #563
 2015-04-28 17:21:41 -07:00
Leonardo de Moura
dcc94dde82 refactor(kernel): rename may_reduce_later to is_stuck, and make is_stuck more precise 
It now reflects the definition used in the elaboration paper.
 2015-04-27 11:20:15 -07:00
Leonardo de Moura
4a157ee676 refactor(kernel/justification): create "wrapper" justification 
It allows us to provide a different pretty printer.

This is a cleanup, and also helps to address issue #528
 2015-04-24 14:49:32 -07:00
Leonardo de Moura
8241863abe feat(kernel/hits): add two builtin HITs: type_quotient and trunc 2015-04-23 15:32:31 -07:00
Leonardo de Moura
47e37a3353 feat(kernel/metavar): add additional assertions 2015-04-20 17:46:06 -07:00
Leonardo de Moura
969d17fd12 fix(frontends/lean/elaborator): class inference in tactic mode with trunc 
closes #477
 2015-04-05 17:47:14 -07:00
Leonardo de Moura
ed1acd9fb0 feat(library/init): move propext to init/quot, add Jeremy's funext theorem 2015-04-01 12:36:33 -07:00
Leonardo de Moura
b960e123b1 feat(kernel): add experimental support for quotient types 2015-03-31 22:04:16 -07:00
Leonardo de Moura
88495f9d59 fix(*): remove unnecessary null pointer checks 
closes #514
 2015-03-28 12:16:39 -07:00
Leonardo de Moura
223ef58db9 fix(kernel/equiv_manager): typo 2015-03-27 10:44:09 -07:00
Leonardo de Moura
f33ad9d6f4 feat(kernel): add equivalence manager for speeding up is_def_eq 2015-03-27 10:34:54 -07:00
Leonardo de Moura
d69f829337 perf(kernel/justification): avoid redundant justification objects 2015-03-25 19:09:01 -07:00
Leonardo de Moura
f5811d6092 feat(frontends/lean): hide subterms that do not contain metavariables 
when generating "unresolved metavariables" error message

closes #473
 2015-03-13 12:42:57 -07:00
Leonardo de Moura
026622a790 refactor(src/kernel/replace_fn): remove stack-less replace_fn it is slower than the simple one 2015-03-12 16:22:49 -07:00
Leonardo de Moura
4ea323a2b2 refactor(library/tactic): cleanup common pattern 2015-03-12 14:52:41 -07:00