Sebastian Ullrich
1f447efa54
doc: update Lean.Parser.Basic
2022-11-11 14:17:21 +01:00
Sebastian Ullrich
7cdd8f81d7
refactor: simplify withCacheFn
2022-11-11 14:07:15 +01:00
Sebastian Ullrich
43767f8f35
fix: uncacheable syntax stack access in doIf
2022-11-11 13:45:41 +01:00
Sebastian Ullrich
4c11743f4b
refactor: split paren parser, part 2
2022-11-11 13:45:41 +01:00
Sebastian Ullrich
791fc70dd9
refactor: split paren parser
2022-11-11 13:45:41 +01:00
Sebastian Ullrich
30dd28480d
fix: suppressInsideQuot inside quotation
2022-11-11 13:45:41 +01:00
Sebastian Ullrich
f5c13f9db8
chore: parseQuotWithCurrentStage and quotPrecheck
2022-11-11 13:45:41 +01:00
Sebastian Ullrich
0dea086669
fix: reset lhsPrec, errorMsg in withCacheFn
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
22510db004
refactor: simplify parser code using withFn
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
e7bf1cd3dc
refactor: simplify adaptUncacheableContextFn
...
compiler.ir.result reports 0 allocations on happy path
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
fb941d0827
fix: ensure parser caching is sound re. syntax stack accesses
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
7410d00678
feat: Subarray.findRev?
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
12b267bd8c
refactor: categoryParserOfStack is dead
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
17782fba1a
fix: replace broken ptrEq cache sanity checks with private ParserContext constructor
...
The context is now manipulated using `adaptCacheableContext` and `adaptUncacheableContext`
and created using `ParserFn.run`.
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
d5255e94e8
perf: improve dynamicQuot caching
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
d3f7d0350f
refactor: move parser types into separate file
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
9a4626c495
fix: must cache stack of parser evals
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
36189cb51a
chore: simplify parser cache key computation, panic on environment/token table divergence
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
ed03ff9d00
perf: cache leading_parser and syntax as well
...
We better hope the `leading_parser`s are closed terms
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
da6efe1bca
fix: make parser caching sound (I hope?)
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
35509b5e98
refactor: more sensible ordering of declarations in Lean.Parser.Basic
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
246923886a
fix: do not create choice nodes for failed parses
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
57320712f0
fix: extraneous missing items on parser stack
2022-11-11 09:13:02 +01:00
Sebastian Ullrich
7e193a45ce
perf: cache category parses
2022-11-11 09:13:02 +01:00
Leonardo de Moura
8030aed56e
fix: fixes #1814
...
Missing `hasAssignableMVar` checks.
2022-11-10 20:42:02 -08:00
Leonardo de Moura
ca0fb21df4
fix: fixes #1813
...
Remark: modifies the value for the `mid` priority.
See new note at `Init/Notation.lean`
2022-11-10 16:09:21 -08:00
Leonardo de Moura
723b87ad63
chore: fix build
...
Incorrect assertion in the old code generator has been exposed by new test.
2022-11-10 15:27:43 -08:00
Leonardo de Moura
c147059fd7
fix: fixes #1812
2022-11-10 08:58:09 -08:00
Leonardo de Moura
9b02f982e2
chore: add ppCode'
2022-11-10 08:07:35 -08:00
Leonardo de Moura
2386c401d2
chore: use String.get' and String.next' at Parser/Basic.lean
...
This commit also cleans up old frontend legacy.
2022-11-09 17:06:22 -08:00
Leonardo de Moura
5eaa0fa2df
chore: leftovers
2022-11-09 17:03:08 -08:00
Leonardo de Moura
4f07c46956
fix: bug at lean_string_utf8_get_fast
2022-11-09 16:58:20 -08:00
Leonardo de Moura
1704debcd0
perf: add parseImports'
...
Faster version of `parserImports` for Lake
2022-11-09 14:50:11 -08:00
Leonardo de Moura
69bd25af4f
chore: add Repr and Inhabited instances for Import
2022-11-09 14:35:57 -08:00
Leonardo de Moura
3e33fcc4f8
chore: use lean_string_utf8_next_fast
2022-11-09 12:06:37 -08:00
Leonardo de Moura
92c03c0050
perf: prepare do add String.next'
2022-11-09 12:00:31 -08:00
Leonardo de Moura
20eeb4202f
perf: fast String.get' without runtime bounds check
...
TODO: naming convention `String.get'` should be called `String.get`,
and we should rename the old `String.get`
2022-11-09 12:00:30 -08:00
Adrien Champion
33aa1724f2
fix: rewrite by with strict indentation in a few struct-fields
2022-11-08 08:30:42 -08:00
Adrien Champion
5849fdc6c9
feat: require strict indentation on nested by-s
2022-11-08 08:30:42 -08:00
Mario Carneiro
4bf89dfa12
feat: allow doSeq in let x <- e | seq
...
fixes #1804
2022-11-08 08:29:21 -08:00
Sebastian Ullrich
9f2182fdd9
chore: update script/apply.lean semantics
2022-11-07 19:47:04 -08:00
Leonardo de Moura
95df68f3e4
chore: [elab_as_elim] at Eq.substr
...
Lean 3 compatibility issue.
see #1806
2022-11-07 19:44:11 -08:00
Leonardo de Moura
b4d13a8946
refactor: LetExpr => LetValue
...
We use "let value" in many other places in the code base.
2022-11-07 18:51:07 -08:00
Leonardo de Moura
e8b4a8875c
fix: type argument that is a fvar at FixedParams.lean
2022-11-07 18:18:07 -08:00
Leonardo de Moura
9399164201
fix: simpCasesOnCtor?
2022-11-07 18:18:06 -08:00
Leonardo de Moura
a5dadfdb7a
feat: activate all passes
2022-11-07 16:18:36 -08:00
Leonardo de Moura
828a815821
fix: simpAppApp?
2022-11-07 16:18:36 -08:00
Leonardo de Moura
92faeec832
fix: add Simp.findFunDecl'?
...
It may look like a simple optimization but affects the inlining
heuristics. Example:
```
fun f ... := ...
let x_1 := f
let x_2 := x_1 a
let x_3 := x_1 b
...
```
Before this commit, `f` was not being marked as being used multiple times.
2022-11-07 16:18:36 -08:00
Leonardo de Moura
f342d0ea35
fix: avoid unnecessary whitespace at LCNF pretty printer
2022-11-07 16:18:36 -08:00
Leonardo de Moura
cf13b29760
fix: nasty bug due to #1804
2022-11-07 16:18:36 -08:00
