Commit graph

67 commits

Author SHA1 Message Date
Leonardo de Moura
7ea9a8c316 feat: add #print command parser 2020-07-28 14:56:10 -07:00
Leonardo de Moura
27c3e23c17 fix: type is optional in explicit fields
Reason: default value overriding notation.
2020-07-21 16:57:36 -07:00
Leonardo de Moura
a1fc824336 fix: field syntax 2020-07-17 10:12:43 -07:00
Leonardo de Moura
ba3f461505 chore: we decided to not support private parent structures, nor named parent structures
These are obscures features in Lean 3 that AFAIK nobody ever used.
2020-07-17 09:09:34 -07:00
Leonardo de Moura
bf88a35888 feat: add views for structure command 2020-07-16 16:35:00 -07:00
Leonardo de Moura
8a80887fb0 fix: structure command syntax 2020-07-16 16:00:31 -07:00
Leonardo de Moura
c421151e61 feat: allow users to annotate structure constructor and projections with declaration modifiers (e.g., private, protected, doc string, ...) 2020-07-16 10:27:06 -07:00
Leonardo de Moura
b247d4901c feat: allow commands such as variable and universe in the preamble of a mutual command block 2020-07-16 09:55:51 -07:00
Leonardo de Moura
3fc6d8ce61 chore: improve constructor syntax
I think
```
inductive Foo
| private mk : Foo -> Foo
```
looks better than
```
inductive Foo
private | mk : Foo -> Foo
```

cc @Kha
2020-07-13 16:22:48 -07:00
Leonardo de Moura
6e12987dd9 feat: add declModifiers to constructor declarations
The goal is to allow users to attach doc strings and
`private/protected` to constructor declarations.

TODO: reject non applicable modifiers such as `unsafe` and `partial`.

cc @Kha
2020-07-13 16:22:48 -07:00
Leonardo de Moura
667f2ed601 feat: resolve inductive and ctor names 2020-07-13 16:22:48 -07:00
Leonardo de Moura
30f03ad18c feat: add mutual syntax 2020-06-26 12:47:43 -07:00
Leonardo de Moura
cbb14673ef chore: move RBTree and RBMap to Std 2020-06-25 13:26:16 -07:00
Leonardo de Moura
1be221a1f4 chore: move PersistentHashMap and PersistentHashSet to Std 2020-06-25 11:56:00 -07:00
Leonardo de Moura
249bda16c0 chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Sebastian Ullrich
81376d3902 feat: allow capturing expected type in elab
/cc @leodemoura
2020-06-25 14:58:45 +02:00
Sebastian Ullrich
51e4b49ba6 feat: allow arbitrary syntax in macro/elab 2020-06-25 13:54:11 +02:00
Leonardo de Moura
cefbc27720 feat: add elab and elab_rules command syntax 2020-06-24 18:34:23 -07:00
Leonardo de Moura
18cd41f902 feat: add syntaxAbbrev 2020-06-16 15:18:10 -07:00
Leonardo de Moura
c6e7ea8fd5 feat: add ParserDescr.parser constructor for embedding parser definitions into parser descriptions 2020-06-16 14:06:46 -07:00
Leonardo de Moura
f61e4ffbbd chore: ParserDescr.parser ==> ParserDescr.cat 2020-06-16 13:40:16 -07:00
Sebastian Ullrich
b3d2e51aff feat: generalize tactic/command macro syntax 2020-06-16 19:21:48 +02:00
Sebastian Ullrich
1ccaadfcf0 feat: add #eval syntax 2020-06-16 10:56:47 +02:00
Leonardo de Moura
09eb27404f chore: remove <$ and $> notation
cc @Kha
2020-06-15 14:52:31 -07:00
Leonardo de Moura
6f0192581a feat: change precedence for fun and do parsing rules to maxPrec
Motivation: avoid `$`. See new test.

cc @Kha
2020-06-11 16:24:04 -07:00
Leonardo de Moura
7860f3645e doc: update comments to match new algorithm 2020-06-11 16:18:26 -07:00
Sebastian Ullrich
0afae3acc5 doc: adjust citation in Parser.lean 2020-06-11 15:55:53 -07:00
Leonardo de Moura
36bddc91cb chore: remove checkWsBeforeIfSymbol hack
Now the `app` parsing rule always require some whitespace before the
first argument.

cc @Kha
2020-06-11 14:58:29 -07:00
Leonardo de Moura
f0ebf426b7 chore: longestMatchFn parsers must produce exactly one Syntax node
Before this commit, we were handling the following two abnormal cases:

1- `p` did not produce any `Syntax` node. `runLongestMatchParser`
would insert a `Syntax.missing`.

2- `p` produced more than one `Syntax` node on the
stack. `runLongestMatchParser` would combine all of them using a
`nullKind` node.

This feature was never used since we only use `longestMatchFn` to
process leading and trailing parsers. In both case, we create a node.
Moreover, if a bad parser is manually created, I think it is better to
fail than accept using `Syntax.missing` or a `nullKind` node. We would
only be postponing the problem since we don't have elaboration
functions for them.

cc @Kha
2020-06-11 12:38:55 -07:00
Leonardo de Moura
8e4dc5bcf6 fix: longestMatchFn
Several combinators (e.g., `checkNoWsBefore`) access the "leading
term" by retrieving the element on the top of the syntax stack.
However, the `longestMatchFn` was accumulating successful matches on
the syntax stack too. This commit makes sure the `longestMatchFn`
always push the "leading term" before trying a parser.

This commit also eliminates the `orelseFn` hack at `trailingLoopStep`.
Now, we use `longestMatchFn` for all parsers. Note that we have to add
a new combinator (`checkWsBeforeIfSymbol`) to make sure that `a[i]`
cannot be parsed by the `app` parsing rule.
Before removing the hack from `trailingLoopStep`,
`a[i]` was correctly parsed as an `arrayRef`. After the change,
the `app` parser is tried and it succeeds (IF we don't use
`checkWsBeforeIfSymbol`). It is an application using the list literal
`[i]`.
The `checkWsBeforeIfSymbol` ensures that `a[i]` is not a valid `app`.

cc @Kha
2020-06-11 12:21:16 -07:00
Leonardo de Moura
de0a2fefa0 feat: add notationItem 2020-06-10 16:54:46 -07:00
Leonardo de Moura
610ced2de5 chore: appPrec => maxPrec 2020-06-10 16:50:09 -07:00
Leonardo de Moura
7269a721ff fix: parser! and tparser! syntax in the new frontend 2020-06-10 16:20:48 -07:00
Leonardo de Moura
1307405300 chore: make sure parser! and tparser! use a syntax similar to the one used at syntax for setting precedences
cc @Kha
2020-06-10 16:09:13 -07:00
Leonardo de Moura
243cda497e chore: remove leadingNodePrec and trailingNodePrec 2020-06-10 15:07:41 -07:00
Leonardo de Moura
1c09e63a29 chore: update trailingNode and leadingNode API 2020-06-10 15:02:12 -07:00
Leonardo de Moura
1477d23546 feat: remove ParserDescr.prec and update ParserDescr.trailingNode/ParserDescr.node 2020-06-10 14:57:55 -07:00
Leonardo de Moura
2125687d9c chore: remove unnecessary [appPrec] annotations 2020-06-10 14:44:54 -07:00
Leonardo de Moura
77e1260ed2 chore: simplify checkPrec 2020-06-10 14:34:58 -07:00
Leonardo de Moura
6d3aff97d5 chore: lbp and rbp ==> prec 2020-06-10 13:41:10 -07:00
Leonardo de Moura
f0a9e54a69 chore: make sure leading and trailing parsers use the same kind of check 2020-06-10 13:41:10 -07:00
Leonardo de Moura
85320d9cf0 chore: add support for old syntax 2020-06-09 14:11:34 -07:00
Leonardo de Moura
7ec23f9401 fix: macro command syntax 2020-06-09 14:11:34 -07:00
Leonardo de Moura
a4f19aac32 fix: macro command 2020-06-09 14:11:34 -07:00
Leonardo de Moura
7fce8b5d1f fix: notation command
@Kha Note that I had to write the weird pattern

```
match_syntax stx with
| `(notation:$prec $items* => $rhs)    => expandNotationAux stx prec items rhs
| `(notation $noprec* $items* => $rhs) => expandNotationAux stx none items rhs
| _ => Macro.throwUnsupported
```

with the weird `$noprec*` to match the case where the optional
precedence is not provided. I realized this is not a bug, but
I guess most users will be puzzled by this behavior. If we had a kind
for `notationItem`, I would be able to write
```
`(notation $items:notationItems* => $rhs)
```
2020-06-09 14:11:34 -07:00
Sebastian Ullrich
c8ee21747b chore: remove obsolete symbolAux, symbolNoWsAux 2020-06-09 10:37:00 +02:00
Leonardo de Moura
8972c7e666 feat: revised syntax commands 2020-06-08 16:12:06 -07:00
Leonardo de Moura
d2c2d95c47 chore: remove symbolAux 2020-06-08 16:12:06 -07:00
Leonardo de Moura
dd1aa2f271 chore: improve error message
cc @Kha
2020-06-08 16:12:05 -07:00
Leonardo de Moura
c6ea675cae chore: fix test
@Kha The error message changed. Not sure the new one is expected. It
is due to the change in `trailingLoop`. We can discuss it in the next
meeting.
2020-06-08 16:12:05 -07:00