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

140 commits

Author SHA1 Message Date
Sebastian Ullrich
4a4b4c1ef4 fix: mkAtomFrom: generate synthetic position like other *From functions 
Also consistently use binders as reference position for an elided binder type.
Before, type errors were always given extent 1, the length of the
synthetic `_` token.
 2021-07-19 13:24:59 -07:00
Leonardo de Moura
953dd85c06 chore: avoid inline 2021-06-28 10:17:01 -07:00
Leonardo de Moura
ae6a28af52 chore: remove unnecessary specialize 2021-06-28 10:11:23 -07:00
Leonardo de Moura
712206f80e refactor: add BindersUtil.lean 2021-06-28 08:44:16 -07:00
Leonardo de Moura
7e1bb3e65b refactor: add MatchAltView.lean and PatternVar.lean 2021-06-28 08:29:47 -07:00
Sebastian Ullrich
720954d63a perf: Lean.Elab.Do: avoid code explosion 2021-06-17 12:51:23 -07:00
Daniel Selsam
ded51882a0
feat: pp motives and misc delab fixes 2021-06-13 00:06:27 +02:00
Leonardo de Moura
b91e22af2b fix: fixes #241 2021-05-22 19:10:07 -07:00
Leonardo de Moura
e5083f2521 fix: avoid unnecessary unfolding at do 2021-05-02 21:29:32 -07:00
Sebastian Ullrich
40b17bc364 refactor: introduce a few double-backtick quotations 2021-04-28 12:09:13 +02:00
Sebastian Ullrich
9301e05a7e feat: double-quoted quotation semantics and basic precheck hooks 2021-04-27 16:38:37 -07:00
Leonardo de Moura
c76820a251 fix: no method lift over let 2021-04-24 19:33:55 -07:00
Leonardo de Moura
1c23d68c6a feat: add (generalizing := true/false) optional attribute to match 2021-04-15 17:04:25 -07:00
Leonardo de Moura
36a4f337e9 fix: fixes #247 2021-04-15 12:33:45 -07:00
Leonardo de Moura
327eb1a96d fix: ensure ill-formed if do-statements do not trigger non termination 2021-04-13 15:51:20 -07:00
Leonardo de Moura
2384826933 chore: add loop prenvention code at do-expander 2021-04-13 15:46:47 -07:00
Leonardo de Moura
1df84e3a6d feat: allow haveDecl, sufficesDecl, letRecDecls in antiquotations 2021-03-12 17:40:16 -08:00
Leonardo de Moura
be841a7cad chore: throwError! => throwError, throwErrorAt! => throwErrorAt 
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
 2021-03-11 11:59:45 -08:00
Leonardo de Moura
1112ab6eff chore: use new notation 2021-03-11 11:19:33 -08:00
Leonardo de Moura
e7140959c4 chore: add elaborator for let_fun and let_delayed 2021-03-11 10:40:25 -08:00
Leonardo de Moura
164577d94e chore: remove parser! and tparser! 
The new macros are called "leading_parser` and `trailing_parser`.

cc @Kha
 2021-03-11 09:36:58 -08:00
Leonardo de Moura
68143ca8ba chore: trace[...]! ==> trace[...] 
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
 2021-03-10 18:44:43 -08:00
Leonardo de Moura
2d6b59f4bb feat: add dummy elabForIn 2021-02-05 17:02:57 -08:00
Leonardo de Moura
3d4bc9f991 chore: provide ambient monad to forIn 2021-02-04 18:31:28 -08:00
Leonardo de Moura
53539b1dff chore: use polymorphic method forIn 2021-02-04 18:13:01 -08:00
Leonardo de Moura
d956f0ae9f feat: use destructTuple to compile for in notation instead of pattern matchin 2021-02-04 17:17:51 -08:00
Leonardo de Moura
d7ca646071 fix: make sure mkUnit return Syntax that is a valid term and pattern 2021-01-28 11:27:28 -08:00
Sebastian Ullrich
79107a2316 feat: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
462e1d54a3 chore: replace uses of copyInfo with automatic position copying in syntax quotations 
We could introduce a `copyPos` alternative, but turns out we don't need it right now
 2021-01-20 16:48:50 +01:00
Leonardo de Moura
0672247ce8 chore: make comments VS Code friendly 2021-01-15 13:53:37 -08:00
Leonardo de Moura
791388400b feat: improve do error messages 
cc @Kha @Vtec234
 2021-01-14 14:18:56 -08:00
Leonardo de Moura
308c61027a feat: save doc strings 
We can now document `let rec` too.
 2021-01-10 07:13:33 -08:00
Leonardo de Moura
c94bb0fa2b fix: missing quotes in error messages 2020-12-26 09:01:45 -08:00
Leonardo de Moura
01f8127c16 fix: position information at expandDoIf? 2020-12-26 08:26:54 -08:00
Leonardo de Moura
e21ea53661 fix: position of failed to synthesize toStream ... error 2020-12-25 10:03:42 -08:00
Leonardo de Moura
14989f9758 chore: cleanup 2020-12-23 13:49:28 -08:00
Leonardo de Moura
4fb02df6e9 refactor: remove workaround 2020-12-23 13:35:21 -08:00
Sebastian Ullrich
3e77c7cdef fix: error position 2020-12-21 16:25:01 +01:00
Leonardo de Moura
e8e991064e chore: remove workaround at expandDoIf? 2020-12-20 17:53:19 -08:00
Sebastian Ullrich
bc3e9ce961 feat: if let pat ← ... 2020-12-20 23:58:29 +01:00
Sebastian Ullrich
90f747e346 fix: don't change antiquotations semantics in do if 2020-12-20 17:51:37 +01:00
Sebastian Ullrich
eeb0cad29e feat: if let 
/cc @leodemoura
 2020-12-20 16:46:03 +01:00
Leonardo de Moura
91f0e29285 feat: parallel for 2020-12-19 20:01:04 -08:00
Leonardo de Moura
0911936502 feat: parallel for notation 2020-12-19 19:26:53 -08:00
Sebastian Ullrich
f9dcbbddc4 refactor: remove optional leading pipe from match, use many1Indent instead of sepBy1 2020-12-16 18:27:05 +01:00
Leonardo de Moura
3b6d65c3c3 chore: use deriving Inhabited 2020-12-13 10:09:20 -08:00
Sebastian Ullrich
686a28fcc9 feat: allow do lifts inside unescaped antiquotations 
/cc @leodemoura
 2020-12-12 13:01:05 +01:00
Sebastian Ullrich
6fac0c0b16 feat: support syntax patterns in do 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
06ad52575a feat: force users to use discard when action result is not being bound and it is not PUnit 
After this commit, we have to use an explicit `discard` in code such as
```
def g (x : Nat) : IO Nat := ...
def f (x : Nat) : IO Unit := do
  discard <| g x   -- type error without the `discard`
  IO.println x
```

Motivation: prevent users from making mistakes such as
```
def f (xs : Array Nat) : IO Unit := do
  xs.set! 0 1
  IO.println xs
```
when they meant to write
```
def f (xs : Array Nat) : IO Unit := do
  let xs := xs.set! 0 1
  IO.println xs
```
 2020-12-08 06:14:48 -08:00