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

68 commits

Author SHA1 Message Date
Leonardo de Moura
5d3f421e70 feat(library/init/lean/parser/parsec): avoid unnecessary [alternative m] dependencies 2018-07-26 15:51:00 -07:00
Leonardo de Moura
35b100bb94 feat(library/init/lean/parser/parsec): implement not_followed_by using catch 2018-07-26 15:47:19 -07:00
Sebastian Ullrich
134d27dbec feat(library/init/lean/parser/parsec): longest_match should return all longest parses 
In the case of overlapping notations, we will return a choice node of all
possible parses.
 2018-07-25 18:07:56 -07:00
Sebastian Ullrich
18b4456a84 Revert "refactor(library/init/lean/parser/parsec): monad_parsec: move from monad_lift/monad_map to direct primitives" 
This reverts commit 9db0724bf1.
 2018-07-25 13:53:29 -07:00
Sebastian Ullrich
218af640bb fix(library/init/lean/parser/reader/term): add missing file 2018-07-20 18:44:37 +02:00
Sebastian Ullrich
1c561726de feat(library/init/lean/parser/reader/module): basic notation command 2018-07-18 17:45:37 +02:00
Sebastian Ullrich
8444a7412e feat(library/init/lean/parser/reader/basic): add a small monad transformer for managing recursion and use it to implement recursive section parsing 2018-07-16 18:39:23 +02:00
Sebastian Ullrich
5b55600e71 feat(library/init/lean/parser/reader/module): open command 2018-07-16 12:38:27 +02:00
Sebastian Ullrich
9e5ae42625 chore(library/init/lean/parser/reader/token): improve error messages 2018-07-13 16:10:13 +02:00
Sebastian Ullrich
09a0397648 fix(library/init/lean/parser/reader/token): fix keyword parsing using longest_match 2018-07-13 15:51:48 +02:00
Sebastian Ullrich
8707773872 feat(library/init/lean/parser/parsec): introduce observing and longest_match primitive parser combinators 2018-07-13 15:51:00 +02:00
Sebastian Ullrich
9db0724bf1 refactor(library/init/lean/parser/parsec): monad_parsec: move from monad_lift/monad_map to direct primitives 
This breaks the code for variable-length tokens that depended on lifting
`parsec` into `read_m`. Either `read_m` could be parameterized by its state,
or we just hard-code all variable-length tokens.
 2018-07-12 17:53:43 +02:00
Sebastian Ullrich
5955e3fce8 chore(library/init/lean/parser/parsec): proper namespacing 2018-07-12 10:35:22 +02:00
Sebastian Ullrich
72b255d4e1 chore(library/init/lean/parser/parser_t): rename module and type to parsec to avoid nested use of parser 2018-07-12 10:35:20 +02:00
Sebastian Ullrich
e57117a9b3 chore(library/init/lean/parser/parser_t): revert introduction of parser_t 2018-07-11 18:44:04 +02:00
Sebastian Ullrich
6fa4e56fbe feat(library/init/lean/parser/syntax): add and test reprinter 2018-07-11 14:34:50 +02:00
Sebastian Ullrich
b2f9b2c180 feat(library/init/lean/parser/{syntax,reader}): store whitespace around tokens 2018-07-11 14:34:50 +02:00
Sebastian Ullrich
67d93ff051 fix(library/init/lean/parser/reader/token): fix loops running out of fuel 2018-07-06 15:56:01 +02:00
Sebastian Ullrich
ab19966d65 feat(library/init/lean/parser/reader): automatically promote tokens through readers 2018-07-05 18:01:17 +02:00
Sebastian Ullrich
fbdb73665f test(tests/lean/reader1): start testing the tokenizer on core.lean and fix a comment bug 2018-07-05 16:51:48 +02:00
Sebastian Ullrich
6b6c16b6d6 chore(library/init/lean/parser/reader/module): remove theory command 
We plan to allow `noncomputable`, as well as more modifiers, on `namespace/section`
 2018-07-05 10:42:52 +02:00
Sebastian Ullrich
8ef87818ce feat(library/init/lean/parser/reader): implement basic tokenizer 2018-07-05 10:42:37 +02:00
Sebastian Ullrich
d0e53be0dd feat(library/init/lean/parser/parser_t): improve str's error message and allow error messages without 'unexpected' part 
Showing the expected string at the initial position is much more helpful than
showing "unexpected <char>"
 2018-07-05 10:20:25 +02:00
Sebastian Ullrich
47f18661c5 refactor(library/init/lean/parser/parser_t): remove some uses of lift 2018-06-29 16:39:45 +02:00
Sebastian Ullrich
70970ce5e0 feat(library/init/lean/parser/reader): add simplistic implementation of a tiny initial part of the Lean reader 
Maybe 'reader' isn't the best name.
 2018-06-18 19:23:58 +02:00
Sebastian Ullrich
bf9bf19215 doc(library/init/lean/parser/parser_t): some monad_parser documentation 2018-06-18 13:50:05 +02:00
Sebastian Ullrich
7ae87705c2 feat(library/init/lean/parser/parser_t): introduce monad_parser 2018-06-15 17:48:20 +02:00
Sebastian Ullrich
b1aff14650 feat(library/init/lean/parser/syntax.lean): simplify syntax debug output 2018-06-07 14:57:13 +02:00
Sebastian Ullrich
613b6805b3 chore(library/init/lean/parser/parser_t.lean): fix comments 2018-06-07 14:57:13 +02:00
Sebastian Ullrich
bdfdd1288e feat(library/init/lean/parser/macro): allow expanders to be skipped dynamically 2018-06-07 14:57:13 +02:00
Sebastian Ullrich
1c380037d3 refactor(library/init/lean/parser/syntax): replace syntax.lst with syntax.node, remove span field from syntax_node 2018-06-06 15:46:39 +02:00
Sebastian Ullrich
732c823646 feat(library/init/lean/parser): remove syntax_id, use De Bruijn indices instead 2018-06-06 15:36:28 +02:00
Leonardo de Moura
1bae8f8eab refactor(library/init/lean/ir/parser): parser.lean => parser_t.lean 2018-06-05 08:00:13 -07:00
Sebastian Ullrich
0f7c0ac8bf feat(init/lean/parser/parser): make a monad transformer 
Also move parser combinators into the more specific namespace `init.lean.parser.parser_t`.
 2018-06-04 12:57:23 +02:00
Sebastian Ullrich
6a0f3056f4 chore(library/init/lean/parser/syntax): cleanup 2018-06-04 11:02:45 +02:00
Sebastian Ullrich
c4d7eb7949 feat(init/lean/parser/macro): global names can be overloaded 2018-05-29 16:43:32 +02:00
Sebastian Ullrich
4a7c2fcafc test(tests/lean/macro1): add examples from prototype 2018-05-17 17:45:02 +02:00
Leonardo de Moura
b7f194d389 feat(library/init/lean/ir): allow arbitrary C++ identifiers to be assigned to declarations 2018-05-13 11:04:42 -07:00
Leonardo de Moura
3be7540efe chore(library/init): use mfor instead of mmap' 2018-05-09 15:41:53 -07:00
Leonardo de Moura
3f883bd949 chore(library/init/lean/parser/parser): add monad_fail instance 2018-05-09 09:19:14 -07:00
Leonardo de Moura
d5fe509c36 chore(*): remove end after each match-expression 
`end` is not optional anymore
 2018-05-04 11:30:06 -07:00
Leonardo de Moura
0d49ae3f69 feat(library/init/lean/parser): add not_followed_by and not_followed_by_sat 
The new parsers are useful to implement the longest match rule.
 2018-05-02 15:55:57 -07:00
Leonardo de Moura
f44bfb3e59 feat(library/init/lean/parser/parser): use dlist to implement expected messages 
The idiom `p1 <|> p2 <|> ... <|> pn` generates many append operations.
`dlist` provides an O(1) append.
 2018-05-02 12:43:21 -07:00
Leonardo de Moura
4d6cbf62a2 refactor(library/init/lean/parser/parser): we don't need to store the whole message in ok_eps 
In the original parsec paper, they store messages in OK silent/epsilon
results too. This is not necessary, we only need the "expected" field
for the `ok_eps` constructor.
 2018-05-02 11:37:57 -07:00
Leonardo de Moura
6672cc2a34 fix(library/init/lean/parser/parser): bug 2018-05-01 17:15:12 -07:00
Leonardo de Moura
619394f3da feat(library/init/lean/parser/string): parser for string literals 2018-05-01 16:17:16 -07:00
Leonardo de Moura
ffdc6cca8a refactor(library/init/lean/ir): move reserved set to different file 2018-05-01 15:27:25 -07:00
Leonardo de Moura
263391bdbb refactor(library/init/lean): add init/lean/parser/identifier 2018-05-01 11:53:55 -07:00
Leonardo de Moura
7305a7a65e feat(library/init/lean): identifier parser 2018-05-01 10:29:34 -07:00
Leonardo de Moura
ba8b85f4c0 chore(library/init/lean/parser/parser): adjust variable names 2018-04-30 16:36:09 -07:00