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

13789 commits

Author SHA1 Message Date
Leonardo de Moura
1ac65a0aeb feat: register exceptions ids 2020-08-21 13:19:30 -07:00
Leonardo de Moura
04eab3c705 chore: remove dead code 2020-08-21 13:08:49 -07:00
Leonardo de Moura
4faaa392b3 feat: add InternalExceptionId.lean 2020-08-21 13:06:31 -07:00
Leonardo de Moura
510cfb2a57 refactor: simplify Elab.Exception 
TODO: remove unnecessary `Exception` types.
 2020-08-21 12:53:01 -07:00
Leonardo de Moura
0fc30f83f6 chore: remove dead file 2020-08-21 12:11:42 -07:00
Leonardo de Moura
afed2bb827 chore: remove dead code 
`StateRefT` doesn't need a `MonadIO` instance anymore.
 2020-08-21 12:06:16 -07:00
Leonardo de Moura
ae5b4defb1 chore: simplify isExprDefEqStuck and isLevelDefEqStuck 2020-08-21 12:03:51 -07:00
Leonardo de Moura
32a55d5b9c refactor: remove special support for IO errors 
They are now just regular errors.
 2020-08-21 11:55:58 -07:00
Leonardo de Moura
97692be811 fix: throwError missing addContext 
This commit also remove `Exception.kernel`
 2020-08-21 11:24:46 -07:00
Leonardo de Moura
b39803f46d chore: cleanup liftTermElabM 2020-08-21 09:43:21 -07:00
Leonardo de Moura
916b395d1b chore: cleanup 2020-08-21 09:29:09 -07:00
Sebastian Ullrich
e5de32c2dd feat: auto-generate header formatter 2020-08-21 16:43:55 +02:00
Sebastian Ullrich
5f30d62d9b feat: [runParserAttributeHooks] 2020-08-21 16:38:41 +02:00
Sebastian Ullrich
14211cc932 refactor: more core 2020-08-21 15:51:37 +02:00
Sebastian Ullrich
786d90ac80 refactor: move parenthesizer and formatter into CoreM 
/cc @leodemoura
 2020-08-21 14:23:58 +02:00
Sebastian Ullrich
7a44ba7bdd fix: pretty printer knot arity 2020-08-21 10:27:43 +02:00
Leonardo de Moura
1aa8466b79 fix: liftCoreM and liftTermElabM 2020-08-20 19:07:22 -07:00
Leonardo de Moura
05a0e7f6d0 refactor: build all main monads on top of ECoreM 2020-08-20 18:36:04 -07:00
Leonardo de Moura
d85a28fc55 chore: remove unnecessary instance arguments 
`IO.Ref` operations are now in `EIO Empty`. Thus, they work for any
exception `ε`
 2020-08-20 15:59:28 -07:00
Leonardo de Moura
fad6235abb feat: give a name to EIO Empty 
@Kha I am calling it `ST` for lack of a better name. It makes some
sense since only the `IO.Ref` operations are in `EIO Empty` :)
That being said, it may confuse Haskell users.

BTW, I had to give the name to avoid a nontermination in the TC
procedure when using
```lean
instance EIOEmpty.monadLift {ε} : HasMonadLift (EIO Empty) (EIO ε) :=
{ monadLift := fun α => fromEmptyEIO }
```
 2020-08-20 15:47:27 -07:00
Leonardo de Moura
ca1982441f feat: add support for to be added ST 
`ST` will be `EIO Empty`
 2020-08-20 13:45:58 -07:00
Leonardo de Moura
eebc611391 chore: remove unnecessary workaround 2020-08-20 13:15:11 -07:00
Leonardo de Moura
968457ac1c feat: make sure StateRefT can be used with any base EIO Exception 2020-08-20 13:11:12 -07:00
Leonardo de Moura
d36ccb166c feat: use EIO Empty instead of IO at IO.Ref primitives 2020-08-20 12:54:15 -07:00
Leonardo de Moura
8349c72686 feat: add support for EIO 2020-08-20 12:48:39 -07:00
Leonardo de Moura
c55376a1ba chore: more conventional MonadIO 2020-08-20 11:13:10 -07:00
Leonardo de Moura
4e736bcca0 feat: use trick to inform compiler that a builtin doesn't throw exceptions 2020-08-20 11:05:11 -07:00
Leonardo de Moura
c0dbf60830 feat: remove IO.ref.reset 
`reset` was used to implement a "buggy" `IO.ref.modify`.
```lean
@[inline] def Ref.modify {α : Type} (r : Ref α) (f : α → α) : m Unit := do
v ← r.get;
r.reset;
r.set (f v)
```
`IO.Ref.reset` will store a nullptr in `r`.
Now, suppose another thread tries to read this reference,
it will get an `IO.error`.
It is not a crash, but it is really weird behavior.
 2020-08-20 10:07:15 -07:00
Sebastian Ullrich
ea266e48ab feat: unicodeSymbol.formatter: prefer symbol used in syntax tree 2020-08-20 18:57:08 +02:00
Sebastian Ullrich
95742ca17b fix: parenthesizer: take minimum of successive precedence checks for contPrec as well 
Otherwise, we would parenthesize `1 + 2 + 3` as `(1 + 2) + 3` since in
```
@[builtinTermParser] def add   := tparser! infixL " + "  65
```
there is an additional `checkPrec 1024` implied by `tparser!`. Now `contPrec` of this parser is (min 1024 65 = 65).
 2020-08-20 18:36:04 +02:00
Sebastian Ullrich
c2fbb3d307 fix: parenthesizer: parenthesize only because of subsequent parser if in same syntax category 
Otherwise, we would parenthesize `... : α → β := ...` as `... : (α → β) := ...` since in
```
def declValSimple    := parser! " := " >> termParser
```
there is an implicit `checkPrec 1024` from `parser!`.
 2020-08-20 18:36:04 +02:00
Sebastian Ullrich
4f5d1cf369 chore: finish formatter refactoring 2020-08-20 15:47:43 +02:00
Sebastian Ullrich
aa452b795d refactor: make formatter precompiled as well 2020-08-20 15:29:33 +02:00
Sebastian Ullrich
68b9a8e1d1 refactor: move parenthesizer compiler into separate file, generalize 2020-08-20 13:22:57 +02:00
Sebastian Ullrich
9fa6795a73 feat: add [combinatorFormatter] attribute 2020-08-20 11:21:01 +02:00
Leonardo de Moura
b5ed59ef61 chore: missing [inline] 2020-08-19 17:10:52 -07:00
Leonardo de Moura
68a4c145f7 refactor: implement attribute hooks using CoreM 
We were using a mix of `IO` and `Except`
 2020-08-19 14:44:54 -07:00
Leonardo de Moura
61d1846334 feat: add adaptTheReader 2020-08-19 10:23:11 -07:00
Leonardo de Moura
e28f68936d feat: add MonadReaderOf 2020-08-19 10:14:36 -07:00
Leonardo de Moura
57ed29e814 revert: panic! changes 
@Kha I am reverting this change for now.
I understand that the "default-value" approach is bad for debugging,
and it does not produce good error messages, but at least the frontend
will not "panic" when users add a bad macro.

After we switch to the new frontend, we can have a monadic `getArg`
and `getArgs` in the Elab and Macro monads which produces an
"unexpected syntax" error message. I say we wait for the new frontend
because we will be able to write `(<- s.getArg)` inside of
expressions.
 2020-08-19 09:57:58 -07:00
Sebastian Ullrich
1840b4b1ff fix: pretty printer with new syntax 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
203e5f76bd fix: bug found by getArg panic 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
4768ac2fbc chore: make Syntax.getArg(s) panic 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
eb5a171764 feat: adjust semantics to new syntax 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
6cbfe2359b chore: remove old syntax 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
3091bd71e7 feat: unwrap basic token parsers 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
3bddb90bd0 refactor: move isQuot/isAntiquot 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
d4952dc40b feat: use insideQuot parsers 2020-08-19 09:56:23 -07:00
Sebastian Ullrich
ed7edf5661 feat: add checkInsideQuot/checkOutsideQuot/toggleInsideQuot parsers 
One use case is to obtain fine-grained control over at what stage changed syntax is activated
 2020-08-19 09:56:23 -07:00
Leonardo de Moura
40ec0b7ae4 feat: add helper functions and generalize 2020-08-19 09:53:45 -07:00