Leonardo de Moura
61f8b4ef07
feat: add support for maximum recursion depth checks at MacroM
2020-08-10 16:50:12 -07:00
Leonardo de Moura
fe5927927a
feat: elaborate match type
2020-08-10 13:53:08 -07:00
Leonardo de Moura
25fd5d0a9a
fix: ambiguity at match
...
```lean
match x : t with
| ...
```
Two possible intepretations for `x : t`:
1- The discriminant `t` where `x` is the name for the equality proofs `t = ...` in each alternative.
2- The discriminant `x` with a expected type `t` (aka motive) for the match.
This commit resolves the ambiguity by forcing no space before `:` in
the first interpretation.
cc @Kha
2020-08-10 13:47:09 -07:00
Leonardo de Moura
f974521783
fix: missing node
2020-08-10 11:15:44 -07:00
Leonardo de Moura
3ce794c58a
feat: allow h : annotation on match discriminants
2020-08-10 10:12:24 -07:00
Leonardo de Moura
c8ab63ea75
feat: mark auxiliary eliminators as [inline]
2020-08-10 09:41:55 -07:00
Leonardo de Moura
43317d5598
fix: nullary minor premises must be thunks
2020-08-08 16:23:50 -07:00
Leonardo de Moura
d2206dcab2
feat: as-patterns x@pattern
2020-08-08 16:12:44 -07:00
Leonardo de Moura
0ca83699d7
fix: array literal support at DepElim
2020-08-08 15:21:35 -07:00
Leonardo de Moura
0fa404ead2
feat: add support for array literals in the pattern matching compiler
2020-08-07 17:13:15 -07:00
Leonardo de Moura
e1be008516
feat: add caseArraySizes
...
An auxiliary tactic for pattern matching array literals.
2020-08-07 16:04:57 -07:00
Leonardo de Moura
b624fa78d7
fix: another subst issue
2020-08-07 16:04:01 -07:00
Leonardo de Moura
6b18f486d1
feat: add mkLt and mkLe
2020-08-07 14:47:11 -07:00
Leonardo de Moura
3b0ec1b20a
feat: add mkDecideProof
2020-08-07 13:48:37 -07:00
Leonardo de Moura
77e51306c5
fix: missing substitution
2020-08-07 13:37:38 -07:00
Leonardo de Moura
c59fda4c19
feat: add assertExt
2020-08-07 12:06:53 -07:00
Leonardo de Moura
feda5e746f
chore: improve error message
2020-08-07 11:50:08 -07:00
Leonardo de Moura
57ac1751cb
feat: expose mkElimCore
...
`mkElimCore` allows caller to pick the motive.
2020-08-07 06:41:47 -07:00
Leonardo de Moura
aa972878d8
feat: add processValue
2020-08-06 16:34:37 -07:00
Leonardo de Moura
fd9be5e8ae
feat: add caseValues tactic
...
It is an auxiliary tactic for compiling pattern matching.
2020-08-06 15:37:00 -07:00
Leonardo de Moura
e423533bca
chore: improve DepElim trace messages
2020-08-06 11:02:57 -07:00
Leonardo de Moura
d09eb82c4c
feat: add Meta.EqnCompiler trace class
2020-08-06 10:47:26 -07:00
Leonardo de Moura
7342cab0e5
feat: add (ref : Syntax) to Meta.Exception.tactic
...
cc @Kha
2020-08-06 10:14:32 -07:00
Leonardo de Moura
1eff4be172
feat: use Meta.Example.other ref : Syntax if it contains position information
2020-08-06 10:06:24 -07:00
Leonardo de Moura
b1023872b3
refactor: MVarSubst => MVarRenaming
2020-08-06 09:49:42 -07:00
Leonardo de Moura
f934a86646
feat: add (ref : Syntax) to Meta.Exception.other
...
@Kha The Syntax is here just to provide possition information. The
goal is to improve error message location information in code such as `DepElim`.
2020-08-06 09:40:16 -07:00
Sebastian Ullrich
a0b0dbd0ac
fix: formatStx
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
3f6de2af06
refactor: simplify processing of antiquotations in pretty-printer
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
eded953022
feat: formatter: escape identifiers
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
c43e6624f9
fix: Lean.Elab.Command with new parser
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
093f0553e7
chore: add formatter module docstring
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
75b41af122
fix: formatter: further fixes
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
5f4d991a17
fix: formatter: backtracking on identifiers
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
1d725f7c83
feat: almost activate new pretty printer by default
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
19563961e2
feat: more whitespace in term parsers
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
e6442d3177
feat: force whitespace in sort applications
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
01456b1b00
fix: Term.app: force whitespace in front of each argument
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
e8ca2e3f62
feat: formatter: push space at checkWsBefore
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
07928f301f
feat: formatter: separate tokens where necessary
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
33a963d82b
refactor: make formatter stack-based, much like the parser
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
37d890b950
fix: atoms might need backtracking as well, e.g. in fieldIdx <|> ident
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
c9d6636eae
feat: first, trivial formatter implementation
...
No actual token separation yet
2020-08-06 09:27:12 -07:00
Sebastian Ullrich
b6b5f4c9c9
refactor: move whnf-eval functions into Lean.Meta.ReduceEval
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
52b6317d3c
chore: remove obsolete function
2020-08-06 09:26:49 -07:00
Sebastian Ullrich
ebe1e6d181
chore: remove misleading default for ParserCache.tokenCache
2020-08-06 09:26:48 -07:00
Sebastian Ullrich
0e8ef0cb8c
chore: document Format fields
2020-08-06 09:26:48 -07:00
Sebastian Ullrich
6f7a557e5a
feat: add --root flag to set package root directory
2020-08-06 09:21:52 -07:00
Leonardo de Moura
e818368c96
refactor: move EqnCompiler to Meta folder
2020-08-06 09:10:01 -07:00
Leonardo de Moura
9084c4fafc
feat: add DepElim.lean
2020-08-05 16:03:33 -07:00
