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

15382 commits

Author SHA1 Message Date
Sebastian Ullrich
037144d3bd refactor: Delaborator.Builtins: eliminate remainder of manual syntax 2020-12-08 17:53:58 +01:00
Sebastian Ullrich
3c9619ed09 feat: Syntax.isNone: return true on missing 2020-12-08 17:33:51 +01:00
Sebastian Ullrich
e6493755e9 chore: stdlib: match_syntax ~> match 2020-12-08 17:32:02 +01:00
Sebastian Ullrich
290e1cf15f feat: syntax_match: check arity only for nullKind nodes 2020-12-08 17:20:36 +01:00
Sebastian Ullrich
00e167b2f0 feat: match_syntax ~> match 2020-12-08 17:20:36 +01:00
Sebastian Ullrich
6fac0c0b16 feat: support syntax patterns in do 2020-12-08 17:20:36 +01:00
Sebastian Ullrich
93a9d79088 refactor: move around quotation helpers once more 2020-12-08 17:20:36 +01:00
Sebastian Ullrich
32eeac88c8 fix: ensure matchAlts have same shape with and without optionalFirstBar 2020-12-08 17:13:32 +01:00
Sebastian Ullrich
6fc03d0f29 feat: quotation scopes in match_syntax 2020-12-08 17:13:32 +01:00
Sebastian Ullrich
c63b770a7c refactor: reduce dependencies on Lean.Elab.Quotation 2020-12-08 17:13:32 +01:00
Sebastian Ullrich
b12be950bf feat: support complex antiquotations in antiquotation scopes 2020-12-08 17:13:32 +01:00
Leonardo de Moura
ae5aa51712 chore: add explicit discard 2020-12-08 06:18:18 -08: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
Leonardo de Moura
6dddcde25c chore: increase priority of defaultInstance for heterogeneous operators 
@Kha The motivation is to allow users to define default instances such as
```lean
@[defaultInstance 1]
instance : OfScientific Real where
  ...
```
Then, numerals such as `1.2` and `3.4e10` will be `Real` by default instead of `Float`.
 2020-12-07 16:58:34 -08:00
Leonardo de Moura
7e4b7e1400 fix: getFunBinderIds 2020-12-07 12:15:55 -08:00
Leonardo de Moura
cbf2b6c0db feat: change synthinstance threshold 
Before this commit, the threshold was the amount of "fuel".
Now, it is the maximum number of instances used to solve a TC problem.
We have two thresholds
- `maxInstSize`: default 128
- `maxCoeSize`: default 16. It is similar to `maxInstSize`, but used for automatic coercions.

cc @Kha
 2020-12-07 10:45:08 -08:00
Leonardo de Moura
6af3eac142 feat: add MonadStateCacheT based on StateT 2020-12-06 19:07:28 -08:00
Leonardo de Moura
906cb81319 feat: improve inferAppType 
See comment at `Expr.instantiateRevRange`
 2020-12-06 19:01:23 -08:00
Leonardo de Moura
91dec25a35 fix: bug at runST and runEST 2020-12-06 18:52:28 -08:00
Leonardo de Moura
265b7571b4 chore: change checkCache type 2020-12-06 16:24:51 -08:00
Leonardo de Moura
d25f520143 feat: elaborate #reduce command 2020-12-06 10:54:57 -08:00
Leonardo de Moura
1c0943ad82 feat: add #reduce command parser 2020-12-06 09:32:25 -08:00
Leonardo de Moura
f15986a25d fix: use levelMVarToParam at #check command 2020-12-06 09:28:41 -08:00
Leonardo de Moura
f33473a39e chore: use exists notation 2020-12-05 16:50:01 -08:00
Leonardo de Moura
1aaf7c0778 feat: add SimpleScopedEnvExtension 
`ParserExtension` will probably be the only case where we need the
general case.
 2020-12-05 16:38:35 -08:00
Leonardo de Moura
f0372f724c chore: remove unused attribute 2020-12-05 16:28:58 -08:00
Leonardo de Moura
44d0fe993a feat: ensure scoped instances cannot be used outside namespaces 2020-12-05 16:26:31 -08:00
Leonardo de Moura
533192c369 feat: implement instanceExtension using ScopedEnvExtension 2020-12-05 16:04:37 -08:00
Leonardo de Moura
fdc2c9f281 feat: process local instance ... and scoped instance ... commands 2020-12-05 15:46:25 -08:00
Leonardo de Moura
d27770ea0e chore: prepare to add scoped and local instances 2020-12-05 15:36:23 -08:00
Leonardo de Moura
1af03901da feat: scoped and local unification hints 2020-12-05 14:34:14 -08:00
Leonardo de Moura
1faed06dc1 feat: new attrKind syntax 2020-12-05 13:59:08 -08:00
Leonardo de Moura
f1f8c2482f feat: prepare to change attrKind parser 
We want to add a proper node and kind.
 2020-12-05 13:49:59 -08:00
Leonardo de Moura
32d5ef8b78 feat: scoped and local unification hints 2020-12-05 13:49:36 -08:00
Leonardo de Moura
d43a65aed0 feat: elaboarate local syntax, infix and notation commands 2020-12-05 08:05:40 -08:00
Leonardo de Moura
10102bf370 chore: remove "local" before attribute command 
`local` is now part of the `Term.attrInstance` parser.
 2020-12-05 07:47:28 -08:00
Leonardo de Moura
9389bca624 feat: elaborate attrKind 2020-12-05 07:40:55 -08:00
Leonardo de Moura
bcf4ffdd1a feat: local modifier at @[...] 2020-12-05 07:24:55 -08:00
Leonardo de Moura
c6ab0b4d2c feat: allow local modifier at infix, notation, and syntax commands 2020-12-05 07:00:06 -08:00
Leonardo de Moura
4d428c8660 feat: add ScopedEnvExtension.addLocalEntry 2020-12-05 06:54:03 -08:00
Leonardo de Moura
b37213e378 chore: remove workaround 2020-12-04 18:11:53 -08:00
Leonardo de Moura
752578a64c chore: temporary staging workaround 2020-12-04 18:07:09 -08:00
Leonardo de Moura
aad8ea9c76 feat: stable parser names 
```
syntax term "+" term : term              -- generates `term_+_`
syntax "[" sepBy(term, ", ") "]"  : term -- generates `term[_,]`
syntax "done" : tactic                   -- generates `tacticDone`
```

cc @Kha
 2020-12-04 18:00:51 -08:00
Leonardo de Moura
c2cfbf2cdd chore: remove workaround 2020-12-04 16:22:45 -08:00
Leonardo de Moura
2ef84a1b64 chore: temporary staging workaround 
@Kha It seems the new builtin antiquotation notation you added depends
on the array literal notation that is not builtin. I got the following
error after `update-stage0`

```
Lean/PrettyPrinter/Delaborator/Builtins.lean:455:2: error: elaboration function for '_kind.term._@.Init.Data.Array.Basic._hyg.3391' has not been implemented
```

The base name changed from `_kind.term` to `termKind`. I had to change
it because every parser we were defining was in the artificial (sub-)namespace
`_kind` :)
We didn't notive because we didn't have scoped parsers.
 2020-12-04 16:22:44 -08:00
Leonardo de Moura
0749cb9fa9 fix: avoid artificial hierarchical name at parser declarations 2020-12-04 16:22:43 -08:00
Leonardo de Moura
0ab368581a refactor: ScopedEnvExtension 
1) `ScopedEnvExtension` module now mananges the push/pop/activate
methods. Motivations:
  - Easier to add attributes
  - One `ScopedEnvExtension` may be shared between multiple
  attributes (e.g., parsers)

2) Add `AttributeKind`
 2020-12-04 16:22:43 -08:00
Leonardo de Moura
02e13081a9 feat: implement AttributeImpl scoping methods for parsers 2020-12-04 16:22:43 -08:00
Sebastian Ullrich
04f09cc34f perf: avoid redundant token collections from antiquotation scopes 2020-12-04 22:43:31 +01:00
Leonardo de Moura
5a772c6cae feat: expand scoped notation into scoped attribute modifier 2020-12-04 11:39:00 -08:00