Commit graph

53 commits

Author SHA1 Message Date
Leonardo de Moura
9fa89a73df feat: add helper functions for syntax match
Motivation: improve error recovery.
2021-04-05 18:38:57 -07:00
Leonardo de Moura
9a5f239513 refactor: remove Monad Option and Alternative Option
We should use `OptionM` instead.
`Option` still implements `Functor` and `OrElse`.

cc @Kha
2021-03-20 18:25:25 -07:00
Sebastian Ullrich
cb5050bb7f doc: Syntax.topDown 2021-03-16 16:41:32 -07:00
Leonardo de Moura
1112ab6eff chore: use new notation 2021-03-11 11:19:33 -08:00
Sebastian Ullrich
7b9f9e806f feat: Syntax.topDown 2021-03-11 13:22:18 +01:00
Leonardo de Moura
5662e2e745 refactor: move ToString Syntax and BEq Syntax to Init 2021-02-26 13:21:04 -08:00
Sebastian Ullrich
0c91b3769e chore: replace variables in src/ 2021-01-22 14:36:05 +01:00
Sebastian Ullrich
a9f96ace3e chore: naming 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
79107a2316 feat: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
07c7638fd7 feat: token source info antiquotations tk%$id
/cc @leodemoura
2020-12-22 13:11:04 +01:00
Leonardo de Moura
15335efae2 refactor: move Format to Init package
We are going to use it to define `Repr` class.
2020-12-18 11:21:30 -08:00
Sebastian Ullrich
29c2023410 fix: adapt to new matchAlt syntax 2020-12-16 18:52:56 +01:00
Sebastian Ullrich
d22d639fcb refactor: rename "antiquot scope" ~> "antiquot splice" 2020-12-16 17:44:20 +01:00
Sebastian Ullrich
0316c872b9 feat: macro: use appropriate antiquotation kind dependent on bound syntax
/cc @leodemoura
2020-12-14 13:54:34 +01:00
Sebastian Ullrich
8dfa588983 feat: introduce SepArray and use it for sepBy antiquotation splices 2020-12-12 16:02:15 +01:00
Sebastian Ullrich
9e06680541 chore: remove old antiquotations splice syntax 2020-12-12 14:57:14 +01:00
Sebastian Ullrich
a13f129312 feat: antiquotation suffix splices such as $x:k,*
/cc @leodemoura
2020-12-12 14:57:14 +01:00
Sebastian Ullrich
591392840c fix: accept dynamic quotations in match 2020-12-11 21:34:30 +01:00
Sebastian Ullrich
f4267c9bf8 chore: revise Syntax.Traverser changes 2020-12-09 10:38:22 +01:00
Leonardo de Moura
702c258773 fix: index out of bounds
@Kha Please take a look at `Traverser` and check whether the
workaround is appropriate or not.
2020-12-08 11:44:10 -08:00
Sebastian Ullrich
93a9d79088 refactor: move around quotation helpers once more 2020-12-08 17:20:36 +01:00
Sebastian Ullrich
c63b770a7c refactor: reduce dependencies on Lean.Elab.Quotation 2020-12-08 17:13:32 +01:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
9023e93b3e refactor: move Array.set to Prelude 2020-11-25 11:02:25 -08:00
Leonardo de Moura
d6f778bec4 refactor: arbitrary without explicit arguments
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
2020-11-25 09:07:38 -08:00
Sebastian Ullrich
871cd105dc feat: Syntax.updateLeading: also choose "nicer" splits 2020-11-25 11:30:24 +01:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
396e767f3d refactor: move Ref to Prelude and rename it to MonadRef
`MacroM` will implement `MonadRef` because
1- It will be easier to throw errors from macros
2- We will be able to `getRef` to retrieve the syntax node at macro
rules.

I renamed `Ref` to `MonadRef` to make it consistent with other classes
providing monadic methods (e.g. `MonadEnv`, `MonadState`, etc).

cc @Kha
2020-11-13 16:00:31 -08:00
Leonardo de Moura
df5b7fdc24 chore: naming convention
Use namespaces (e.g., `mkStxLit` ==> `Syntax.mkLit`)

cc @Kha
2020-11-11 09:55:23 -08:00
Leonardo de Moura
a8a457b355 refactor: move getTailInfo/copyTailInfo/etc to LeanInit 2020-11-08 11:52:14 -08:00
Leonardo de Moura
13a3215d0d chore: use Subarray combinators 2020-10-28 19:52:59 -07:00
Leonardo de Moura
4ba21ea10c chore: cleanup src/Array/Basic.lean 2020-10-28 19:35:42 -07:00
Leonardo de Moura
c59f673f60 chore: cleanup 2020-10-28 09:33:19 -07:00
Leonardo de Moura
898a08a0c1 chore: avoid Has prefix in type classes
closes #203
2020-10-27 18:29:19 -07:00
Leonardo de Moura
ff493751b5 chore: HasFormat ==> ToFormat 2020-10-27 16:19:14 -07:00
Leonardo de Moura
10c32fcf94 chore: HasToString => ToString 2020-10-27 16:11:48 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
af968c60e6 chore: cleanup 2020-10-22 07:32:23 -07:00
Leonardo de Moura
faa59ead97 chore: move to new frontend 2020-10-20 13:46:16 -07:00
Leonardo de Moura
9810b405d9 feat: add CodeBlock to Syntax converter 2020-10-04 16:19:09 -07:00
Leonardo de Moura
f4aabaecae refactor: move Lean.quote to LeanInit
cc @Kha
2020-09-17 08:15:58 -07:00
Leonardo de Moura
35b11d582d chore: naming convention 2020-08-30 14:26:03 -07:00
Sebastian Ullrich
eb5a171764 feat: adjust semantics to new syntax 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
3bddb90bd0 refactor: move isQuot/isAntiquot 2020-08-19 09:56:23 -07:00
Leonardo de Moura
58c4d8bfc0 refactor: add MonadStateOf
@Kha I tried to remove `MonadExceptOf` by adding `HasThrow` and
`HasCatch`, but this change impacts our ability to define polymorphic
methods such as `finally` which is parametrized by `[MonadExcept]`.
If we remove the `outParam` from `[MonadExcept]`, then we will need to
know the exception at `finally`, or add two instances `[HasCatch]` and
`[HasThrow]`. So, it seems it is more convenient to have
`[MonadExceptOf]` and `[MonadExcept]`. Thus, I applied this approach
to `[MonadState]`
2020-08-18 16:35:33 -07:00
Leonardo de Moura
5605735137 feat: remove outparam from MonadState
We add helper classes with `outParam`.

@Kha This is similar to the `MonadExceptOf` modification.
Motivation: the new `StateRefT` (state monad implemented using
`IO.Ref`) makes is it quite cheap to have multiple states on the
stack. But, we need a mechanism for accessing the different states in
a convenient way.
Note that, I did not add a `MonadStateOf` class, but helper classes
such as `HasGet` which uses `outParam`. I will do the same for `MonadExcept`.

Summary:
- `get` gets the state on the top of the Monad stack
- `getThe σ` gets the state with type `σ`
- `modify f` modifies the state on the top of the Monad stack.
   We use `modify fun s => { s with ... }` quite often, and we cannot
   infer type of `s` here.
- `modifyThe σ f` allows us to select which state on the stack we are modifying.
- I didn't add `setThe`, since we usually can infer the state type at
  `set s`. In the whole codebase, we have only one instance where this
  is not true.
2020-08-18 15:15:31 -07:00
Leonardo de Moura
fe5927927a feat: elaborate match type 2020-08-10 13:53:08 -07:00
Sebastian Ullrich
a0b0dbd0ac fix: formatStx 2020-08-06 09:27:12 -07:00
Sebastian Ullrich
c5d226ba36 feat: HasBeq for Syntax, Substring 2020-08-06 09:26:49 -07:00
Sebastian Ullrich
d23625324c refactor: move Syntax.Traverser 2020-07-29 15:18:00 +02:00