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

337 commits

Author SHA1 Message Date
Sebastian Ullrich
78ced9ffcf refactor(library/module_mgr): minimize parser interface 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
af99f153f8 refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
904d7c4a88 chore(*): remove old task API and task queues 2018-09-11 13:55:25 -07:00
Sebastian Ullrich
38208802c6 refactor(*): replace log_tree with simple message_log list, make module_mgr synchronous 2018-09-11 13:55:25 -07:00
Leonardo de Moura
130b419371 chore(frontends/lean): remove break_at_pos support 
We have already removed auto-completion support.
This change allowed me to remove another old_type_checker dependency.
 2018-09-07 08:34:19 -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
Sebastian Ullrich
14a5246695 fix(frontends/lean/elaborator): nested parser should reset imports 2018-08-22 14:32:03 -07:00
Sebastian Ullrich
eda9e4bb3f feat(library/derive_attribute): temporary, hacky C++ implementation of @[derive] 2018-08-01 18:44:23 -07:00
Sebastian Ullrich
d8122a7284 feat(src/frontends/lean/structure_cmd): allow default values in field parameters 2018-07-12 17:40:45 +02: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
fd5bfc7dfe refactor(kernel): simplify binder_info 
Now, it is an enumeration type like its Lean counterpart.
 2018-06-20 15:31:40 -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
75c63ec921 refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -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
28d6326228 refactor(frontends/lean/parser): add name_generator 2018-02-21 15:04:19 -08:00
Leonardo de Moura
f36fca875c feag(frontends/lean): explicit delimiters in declaration parameters 
Comment from parser.h

This commit makes sure that all declaration parameters must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
The goal is to avoid counter-intuitive declarations such as:

              example p : false := trivial
              def main proof : false := trivial

which would be parsed as

              example (p : false) : _ := trivial

              def main (proof : false) : _ := trivial

where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel.

Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to write

               fun x : t, s
           or
               fun x, s

instead of

               fun (x : t), s
 2017-09-15 10:07:09 -07:00
Gabriel Ebner
867bc46d99 feat(library/vm/vm_parser): expose parse_command_like to the vm 2017-08-14 11:41:48 +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
Gabriel Ebner
68ee9396c6 fix(frontends/lean/parser): support backtracking from empty expressions 
Fixes #1745.
 2017-07-15 11:12:09 +01: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
Leonardo de Moura
bf0d785888 feat(library/messages, frontends/lean): optional end position for messages 
We need this information to be able to fix issues with the transient
message boxes feature (#1667).
 2017-06-15 10:47:58 -07:00
Sebastian Ullrich
56995348d3 hack(frontends/lean/parser): allow input to be substituted and use it to implement interpolating format macro 2017-06-07 10:09:38 -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
Gabriel Ebner
ce44566c7d fix(frontends/lean/parser): do not skip command tokens after error recovery 2017-05-23 11:14:31 -07:00
Gabriel Ebner
345cd1bc2a feat(frontends/lean/parser): error recovery in interactive tactics 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
Gabriel Ebner
1468461c47 feat(frontends/lean): recover from many parser errors 2017-05-23 11:14:30 -07:00
Sebastian Ullrich
669c4130b1 fix(frontends/lean/builtin_expr): no field notation after @/@@ 2017-03-31 09:40:49 -07:00
Sebastian Ullrich
b92af074c0 feat(kernel/pos_info_provider): add save_pos_info 
Allows the elaborator to contribute new info locations
 2017-03-31 09:40:48 -07:00
Leonardo de Moura
ad859817b1 feat(frontends/lean): allow local decls to shadow namespaces 2017-03-29 16:09:45 -07:00
Leonardo de Moura
6183c7676e feat(frontends/lean): use . for field access 2017-03-28 15:29:54 -07:00
Leonardo de Moura
cefe1dd294 chore(frontends/lean/parser): update comments 2017-03-28 12:10:11 -07:00
Leonardo de Moura
07c29c0779 chore(library/abstract_parser,frontends/lean/parser): remove dead code 2017-03-28 11:51:50 -07:00
Gabriel Ebner
318910f99b refactor(frontends/lean/parser): store snapshots in a lazy async list 2017-03-27 14:00:53 -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
Gabriel Ebner
595cbb8fe9 refactor(*): task<T>, log_tree, cancellation_token 2017-03-23 08:57:52 +01:00
Sebastian Ullrich
524a381f22 refactor(lean/tactic_notation): better goal info tweak on , 2017-03-22 07:54:12 -07:00
Sebastian Ullrich
2394f1faa5 fix(frontends/lean/util): do not fall back to current position 2017-03-06 11:02:51 -08:00
Sebastian Ullrich
5d68938a9c feat(frontends/lean): expr literals ```(...) 2017-03-05 08:37:16 -08:00
Leonardo de Moura
077176b82f feat(frontends/lean): add Haskell-like for converting infix notation into functions 
Examples:

 qsort (<) [20, 5, 10, 3, 2, 14, 1]

 foldl (+) 0 [1, 2, 3]
 2017-02-17 22:51:50 -08:00
Sebastian Ullrich
9d8c84713c refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
Sebastian Ullrich
d15591a2d8 feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters 2017-02-17 13:45:56 +01:00
Leonardo de Moura
6334ff24eb fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...] 
See new test for understanding the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2017-02-09 19:06:56 -08:00
Leonardo de Moura
aa5eea6416 feat(frontends/lean): add scope management to parser_state, remove unnecessary undef_ids 2017-02-08 11:58:14 -08:00
Leonardo de Moura
54f7bf9391 fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 
Summary:

We minimize the number of "'sorry' used warning messages".  We also
re-target the error to the main declaration. Example: foo._main ==> foo
We do not report for auxiliary declarations such as "_example" and
"foo.equations._eqn_1"

Get rid of the redundant error message "error : failed" for tactics.
We added "silent failures" in the tactic framework.

We do not store line/col information for tactics nested in notation
declarations.  Before this commit, we would have tactics such
as (tactic.save_info line col) nested inside of notation declarations.
 2017-02-07 20:25:28 -08:00
Gabriel Ebner
95068e4e79 feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
Leonardo de Moura
36dc796f6c refactor(frontends/lean): add more parser_state methods 2017-02-04 11:37:26 -08:00