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

77 commits

Author SHA1 Message Date
Leonardo de Moura
0888dee25e chore(*): meta ==> unsafe 2019-03-15 15:04:40 -07:00
Leonardo de Moura
9cc41c4f3d chore(frontends/lean/inductive_cmds): disable broken check 
@kha I have disabled this check. It was implemented 2 years ago by
Daniel, and I don't want to fix it. It seems you have already fixed a
bug there. AFAICT, this check is just for improving error messages.
I believe we may not even need it since the kernel now supports nested
inductive types. AFAIR, Daniel implemented this check here because the
inductive compiler was introducing a lot of auxiliary declarations
that were making the kernel error messages unreadable.
 2019-03-04 11:05:21 -08:00
Sebastian Ullrich
cead81fcea fix(frontends/lean/inductive_cmds): set m_explicit_levels, and call collect_implicit_locals only after that 2019-01-15 16:47:28 +01:00
Sebastian Ullrich
7aa06338c9 feat(frontends/lean/vm_elaborator): implement inductive 2019-01-14 14:49:40 +01:00
Leonardo de Moura
2315bc4653 chore(library): remove documentation environment extension 2018-09-07 12:09:41 -07:00
Leonardo de Moura
58e91559d0 feat(*): use new inductive datatype module 2018-09-06 18:09:22 -07:00
Leonardo de Moura
208b932583 feat(library/constructions/brec_on): add brec_on and binduction_on for new inductive datatype module 
We don't support these constructions for nested inductive types, but we
do for mutual inductives.
 2018-09-05 14:46:03 -07:00
Leonardo de Moura
f335623530 feat(library/constructions/brec_on): add below and ibelow for new inductive datatype module 2018-09-05 14:46:03 -07:00
Sebastian Ullrich
3a4a052167 fix(frontends/lean/inductive_cmds): expand inductive fix to mutual inductives 2018-09-05 09:58:49 -07:00
Leonardo de Moura
4773a3be5f feat(library/constructions/no_confusion): add no_confusion_type for new inductive datatype module 2018-09-05 09:55:13 -07:00
Leonardo de Moura
d8e7941116 feat(library/constructions/rec_on): add rec_on for new inductive datatype module 2018-09-04 17:22:16 -07:00
Leonardo de Moura
8ed89c6ac3 chore(library): remove normalize.cpp 
The command `#reduce` was also temporarily removed.
 2018-09-04 10:51:14 -07:00
Leonardo de Moura
10a7eccecd feat(library/constructions/cases_on): add cases_on for new inductive datatype module 2018-09-04 09:26:16 -07:00
Leonardo de Moura
dd03747d22 chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
Sebastian Ullrich
39cdae50ee feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms 2018-09-02 18:08:41 -07:00
Leonardo de Moura
776c977742 refactor(kernel): continue constant_info/declaration refactoring 2018-08-27 17:23:26 -07:00
Leonardo de Moura
ae18cee0ea chore(library/module): remove pos_info tracking 
We will use a completely different approach in Lean4
 2018-08-27 15:55:57 -07:00
Leonardo de Moura
27ef29a50f refactor(kernel/declaration): continue constant_info/declaration refactoring 2018-08-27 13:22:10 -07:00
Leonardo de Moura
d334bb1fa7 chore(*): remove more stuff 2018-08-23 15:56:31 -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
bda46cc9ac feat(kernel): add inductive_decl type on top of runtime/object, and ajust kernel/inductive.cpp 2018-06-26 12:16:33 -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
bc57c66ae3 refactor(kernel/level): naming consistency 2018-06-22 10:29:56 -07:00
Leonardo de Moura
46a846dd99 chore(frontends/lean/inductive_cmds): fix nonsense 2018-06-14 13:51:09 -07:00
Leonardo de Moura
a632df3211 refactor(kernel/inductive): do not use ginductive inductive declaration format 
The format used by ginductive is more compact, but it forces the kernel
to implement the `infer_implicit_params`. It would also create problems
when we make inductive_decls a special case of declaration
 2018-06-11 12:52:44 -07:00
Leonardo de Moura
62788a9ca3 refactor(kernel): fix terminology: "free_var" is actually a loose bound variable 
We represent free variables uisng local constants.
We will fix this terminology too.
 2018-06-08 13:25:36 -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
c0e1d05199 chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
Leonardo de Moura
3d38923e07 feat(frontends/lean/inductive_cmds): add option for invoking future inductive module 2018-06-01 16:25:21 -07:00
Leonardo de Moura
de48d49b53 feat(kernel): preparing for adding new inductive datatype module 2018-06-01 14:47:49 -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
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
Leonardo de Moura
2ebf8ab8f1 chore(*): unnecessary #includes 2018-05-18 13:19:22 -07:00
Leonardo de Moura
0556412f8d refactor(*): add runtime folder 
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
 2018-05-14 14:23:56 -07:00
Leonardo de Moura
bdea7d420d chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
Leonardo de Moura
28d6326228 refactor(frontends/lean/parser): add name_generator 2018-02-21 15:04:19 -08:00
Leonardo de Moura
7106bcf7a5 chore(frontends/lean/inductive_cmds): remove app_builder dependency 2017-12-15 11:35:34 -08:00
Leonardo de Moura
51a87212fa chore(frontends/lean/inductive_cmds): remove copy&paste code 2017-12-04 15:56:04 -08:00
Sebastian Ullrich
2faad5114a chore(frontends/lean): enforce and document applying attributes last 2017-09-14 18:48:18 +02: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
Leonardo de Moura
eef4d95410 feat(frontends/lean/inductive_cmds): closes #1655 2017-06-20 16:25:18 -07:00
Sebastian Ullrich
91c77680c8 refactor(init/meta/coinductive_predicates,frontends/lean/inductive_cmds): declare coinductive in Lean 2017-06-19 11:27:12 -07:00
Sebastian Ullrich
492cb20438 feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env 2017-06-19 11:27:12 -07:00
Sebastian Ullrich
95b317fa64 refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
Johannes Hölzl
1352d4a5b3 feat(src/frontents/lean): support for coinduction command in frontend 2017-06-12 20:42:48 -07:00
Leonardo de Moura
748eb856c3 fix(frontends/lean): fixes #1649 
This issue is yet another reason for refactoring how parameters are
represented in Lean.
 2017-06-06 21:33:24 -07:00
Daniel Selsam
8b8814cfbe fix(frontends/lean/inductive_cmd.cpp): fixes #1525 2017-05-01 14:57:25 -07:00
Sebastian Ullrich
0d02136a09 fix(frontends/lean/inductive_cmds): do not whnf pre-exprs 
Fixes #1507
 2017-04-25 17:47:29 -07:00
Gabriel Ebner
5f872912e0 refactor(shell/lean): set exit status 1 iff at least one error was reported 2017-03-23 08:57:56 +01:00
Leonardo de Moura
a897fd3f17 fix(frontends/lean): pattern matching in the declaration header 2017-03-16 01:09:12 -07:00