max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
14447 commits 1 branch 0 tags 5.3 GiB
Commit graph

168 commits

Author SHA1 Message Date
Leonardo de Moura
88c8c560a9 chore(library/equations_compiler): do not generate equation lemmas 2018-08-23 14:04:37 -07:00
Leonardo de Moura
82095cc018 refactor(kernel): split declaration into declaration and constant_info 
This is just another step towards the design described at commit 16598391a07d4a
 2018-08-22 17:53:11 -07:00
Leonardo de Moura
f3e99286bb chore(kernel): remove certified_declaration 2018-08-22 12:11:34 -07:00
Leonardo de Moura
ec1aa2553c refactor(kernel/declaration): implement definition/constant/axiom/theorem using runtime/object 
TODO: inductive, constructor, recursor
 2018-06-25 10:05:45 -07:00
Leonardo de Moura
e9f843ddf6 refactor(kernel/expr): remove mlocal_* functions 
The constructors `mvar` and `fvar` have different memory layouts.
 2018-06-22 14:25:31 -07:00
Leonardo de Moura
ede1a51d60 refactor(kernel/declaration): remove self_opt flag from reducibility hints 
This flag was used by the kernel to decide whether the following
heuristic should be used to avoid unfolding `f` at `is_def_eq`.

       f a =?= f b
       -----------
         a =?= b

This heuristic was introduced at Lean1 after a discussion with
Georges Gontier. Since this discussion, we added support for
caching failures of this heuristic. This proved to be much more
effective to attack the performance problems.
Moreover, we do not even use this flag in the `type_context::is_def_eq`
used during elaboration.

The current codebase contains only one place where this flag was set to
`false`: coercions generated at structure_cmd. This change was
made at commit
1c70514231
in the Lean2 codebase when we were not caching failures and
the kernel type checker was also used during elaboration.
 2018-06-22 09:02:50 -07:00
Leonardo de Moura
01ea596aea refactor(kernel/expr): implement expr using runtime/object 2018-06-21 16:05:33 -07:00
Leonardo de Moura
c5714c2fac chore(kernel): remove expr.macro constructor 
We are now ready to implement `expr` using `runtime/object`.
 2018-06-19 17:54:43 -07:00
Leonardo de Moura
4c370e4558 refactor(kernel/expr): fix binder_info 2018-06-13 12:20:58 -07:00
Leonardo de Moura
a6250840d5 chore(kernel): rename some expr functions 2018-06-09 07:18:24 -07:00
Leonardo de Moura
818170d780 refactor(kernel): remove tag from kernel expressions 
We are temporarily storing position information in a global table.
 2018-06-08 10:29:22 -07:00
Leonardo de Moura
2a79da1ab6 refactor(kernel): move formatting stuff out of the kernel 2018-06-07 16:28:54 -07:00
Leonardo de Moura
e90585737f refactor(*): use C++11 std::current_exception and std::rethrow_exception 
With these new C++11 APIs, we can delete the `clone` and `rethrow`
methods from our exception classes.
 2018-06-07 16:28:54 -07:00
Leonardo de Moura
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
9a671d7c7d chore(library/compiler): delete rec_fn_macro 2018-05-31 17:11:25 -07:00
Leonardo de Moura
3c1ccc9b74 refactor(kernel): use m_meta instead of m_trusted 2018-05-31 11:18:00 -07:00
Leonardo de Moura
12a03f7784 chore(frontends/lean/definition_cmds): remove dependency 2018-05-30 14:46:54 -07:00
Leonardo de Moura
1332fbabd6 feat(library,frontends): remove sorry macro 
Lean4 will not have macros.
 2018-05-24 14:00:30 -07:00
Leonardo de Moura
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
Leonardo de Moura
4af1f31877 feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels 2018-05-23 14:48:22 -07:00
Leonardo de Moura
1bc7c0812c chore(kernel,library): remove task from the kernel and library 2018-05-18 09:06:03 -07:00
Sebastian Ullrich
a7688a10b8 feat(frontends/lean/definition_cmds): elaborate a def's type separately when explicit return type is given 2018-04-20 09:59:09 -07:00
Leonardo de Moura
429edd7a5e fix(frontends/lean/definition_cmds): fixes #1956 2018-04-11 16:48:04 -07:00
Leonardo de Moura
c08a3bc557 refactor(library/typed_expr): move typed_expr to frontends/lean 2018-04-09 15:25:40 -07:00
Leonardo de Moura
bdea7d420d chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
Leonardo de Moura
7762dc381a feat(library/type_context): use context_cache interface 2018-02-21 15:04:20 -08:00
Sebastian Ullrich
f247363305 feat(library/time_task): print cumulative times on --profile 2018-02-19 09:13:24 -08:00
Sebastian Ullrich
2f2540dc3b fix(frontends/lean/definition_cmds): hide kernel exceptions triggered by error recovery 
They are never helpful compared to the original error
 2018-02-02 08:58:52 -08:00
Sebastian Ullrich
c600bca747 feat(frontends/lean/definition_cmds): hide scary kernel exception on duplicate declaration 2018-02-02 08:58:52 -08:00
Leonardo de Moura
0c5c1a27c6 refactor(frontends/lean, library/equations_compiler): move smart unfolding auxiliary function generation to equations_compiler module 2018-01-09 16:27:36 -08:00
Leonardo de Moura
a55b641651 chore(library/type_context): add mk_smart_unfolding_name_for 2018-01-09 16:19:59 -08:00
Leonardo de Moura
6ab792733d feat(library/type_context): smart unfolding 
closes #1794
 2018-01-09 15:09:08 -08:00
Leonardo de Moura
587540f11b feat(frontends/lean): add abbreviation command 
This command is not just a cosmetic feature.
We need it to defined `id_rhs` before the tactic framework is defined.
We want `id_rhs` to be used in all definitions generated by the equation
compiler. Right now, it is only used in definitions defined after the
tactic framework.
 2018-01-05 15:40:59 -08:00
Leonardo de Moura
15660c94f1 chore(frontends/lean/definition_cmds): remove workarounds for meta definitions 
The new approach used to compile meta (and mutual meta) definitions does
not require these hacks in the frontend anymore.
 2017-10-30 15:16:51 -07:00
Leonardo de Moura
482e06427b feat(library/equations_compiler): meta mutual definitions 
closes #1622
 2017-10-30 15:06:12 -07:00
Sebastian Ullrich
2faad5114a chore(frontends/lean): enforce and document applying attributes last 2017-09-14 18:48:18 +02:00
Leonardo de Moura
6781681ae5 feat(frontends/lean/definition_cmds): when the kernel fails to type check a declaration include the fully elaborated term in the error message 2017-09-13 16:43:54 -07:00
Leonardo de Moura
d428eca8a7 fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations 
fixes #1804

Remark: now, all auxiliary definitions in a private declaration share
the same "private" prefix.
 2017-09-11 16:46:56 -07:00
Gabriel Ebner
19777cf9eb fix(frontends/lean/definition_cmds): show trace messages in examples 2017-09-06 14:44:44 +02:00
Sebastian Ullrich
f255513fdc fix(frontends/lean/definition_cmds): apply attributes after declaring equational lemmas 
Fixes `@[simp] def ...`
 2017-09-01 13:36:53 +02:00
Leonardo de Moura
6315136279 fix(frontends/lean/definition_cmds): fixes #1790 2017-08-16 15:57:55 -07:00
Leonardo de Moura
9afb53fad5 feat(kernel/expr): allow metavariables to have user-facing names 
We need this feature for:
1) Defining nonlinear search patterns. Example: (?m <= ?m + 1)
2) Preprocessing recursive equations and support the pattern
refinement approach used in Agda. Example: in Agda, they accept
```
def append {A : Type} : Π (m n : nat), Vec A m -> Vec A n -> Vec A (m + n)
| m n nil            ys := ys
| m n (cons m' x xs) ys := cons x (append m' n xs ys)
```
These equations have to be refined. For example, `m` has to be
replaced with `0` (in the first equation), and `succ m'` in the
second. To implement this kind of refinement, we need to convert
the pattern variables (local constants) into metavariables during
elaboration. Then, the unassigned metavariables become local constants
again. This preprocessing step will fix some of the issues on #1594.
To completely fix #1594, we will need yet another preprocessing step
which will implement "complete transition" used in the equation
compiler before we start elim_match.cpp
 2017-07-16 07:16:41 -07:00
Gabriel Ebner
3392aa90b5 fix(frontends/lean/definition_cmds): support parameters in mutual defs 2017-07-13 15:14:46 +01:00
Leonardo de Moura
e63c79c81e feat(frontends/lean): enable hash_consing during tactic execution 
This commit is trying to address a memory consumption problem in
@dselsam project.
 2017-06-22 17:24:27 -07:00
Sebastian Ullrich
95b317fa64 refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
Leonardo de Moura
603bbe5987 fix(*): gcc 7 linking errors 2017-05-31 16:35:09 -07:00
Leonardo de Moura
4fbb65d9f1 feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs 2017-05-23 15:00:29 -07:00
Gabriel Ebner
eea61a1991 fix(frontends/lean/definition_cmds): fix trace messages in proofs 2017-05-23 11:14:31 -07:00
Gabriel Ebner
6b956ad658 fix(frontends/lean): prevent endless loops 2017-05-23 11:14:30 -07:00
Gabriel Ebner
00ac867ddf feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys 2017-05-23 11:14:30 -07:00