Leonardo de Moura
3ad2d6c4e1
chore: add parser aliases
2020-11-17 11:15:17 -08:00
Leonardo de Moura
1d93eefada
feat: add ! x notation for notFollowedBy(x) in the syntax command
2020-11-17 10:57:15 -08:00
Leonardo de Moura
96db4985eb
feat: allow anonymous antiquotations at ParserDescr.nodeWithAntiquot
2020-11-17 10:48:22 -08:00
Leonardo de Moura
dfa0b97916
chore: remove notSymbol hacks
2020-11-17 10:45:55 -08:00
Leonardo de Moura
da23b96b43
feat: improve error messages for syntax command
2020-11-17 10:33:53 -08:00
Leonardo de Moura
af8d616d5a
feath: improve unary and binary parsers
2020-11-17 08:39:56 -08:00
Leonardo de Moura
360fa1638f
chore: rename Parser.try to Parser.atomic
...
Reason: `try` is a keyword.
cc @Kha
2020-11-17 08:25:01 -08:00
Leonardo de Moura
57670b633a
feat: improve smart unfolding
2020-11-16 15:44:52 -08:00
Leonardo de Moura
c81dbeb53c
feat: improve smart unfolding
2020-11-15 17:34:37 -08:00
Leonardo de Moura
f1b88e1304
feat: add option for disabling smart unfolding and fix tests
2020-11-15 17:00:51 -08:00
Leonardo de Moura
461c0786fd
feat: generate auxiliary declaration for "smart unfolding"
2020-11-15 16:31:40 -08:00
Leonardo de Moura
f5ba036d8f
chore: add support for reducing matchers
2020-11-15 15:07:53 -08:00
Leonardo de Moura
49e9064202
refactor: add MatcherInfo.lean
2020-11-15 14:22:05 -08:00
Leonardo de Moura
77eaf17a47
refactor: move idDelta to Prelude.lean, add idRhs
2020-11-15 12:54:29 -08:00
Leonardo de Moura
98cc4639a0
fix: nested recursive applications
2020-11-14 18:01:22 -08:00
Leonardo de Moura
db5fe843de
chore: add expandInterpolatedStr helper function, rename msg! => m!
2020-11-14 13:52:52 -08:00
Leonardo de Moura
cc7d7422db
fix: UInt ctors/fields in generated code
2020-11-14 12:50:32 -08:00
Leonardo de Moura
9acbc7bb7d
feat: declare subtype notation using syntax
2020-11-14 08:46:02 -08:00
Leonardo de Moura
0ddc2e5efb
chore: remove builtin subtype notation
2020-11-14 08:42:03 -08:00
Leonardo de Moura
17fb995348
feat: improve mkLevelMax'
2020-11-14 08:36:23 -08:00
Leonardo de Moura
e1551afbd8
feat: add macro "exists" xs:explicitBinders ", " b:term : term
...
The ASCII version
2020-11-14 08:21:47 -08:00
Leonardo de Moura
a80c7ff882
feat: add mkLevelMax' and mkLevelIMax'
2020-11-14 08:11:49 -08:00
Leonardo de Moura
99fad9fc4d
feat: goodies for writing notation with binders
2020-11-14 07:32:44 -08:00
Leonardo de Moura
bf242f434d
fix: missing case
2020-11-14 07:14:25 -08:00
Leonardo de Moura
bed1582844
chore: remove workaround of the workaround
2020-11-14 07:04:17 -08:00
Leonardo de Moura
155c377bc6
chore: cleanup depArrow
...
Cleanup hack used before we implemented: parsers have precedence not tokens
2020-11-14 07:00:10 -08:00
Sebastian Ullrich
9c6c568caf
fix: don't try to pretty-print underapplied matcher
...
Fixes #219
2020-11-14 13:19:21 +01:00
Leonardo de Moura
ffc4abed32
fix: UInt* and USize Inhabited instances
2020-11-13 16:30:48 -08:00
Leonardo de Moura
21bfb6a51e
chore: use mutual instead of old idiom: high order functions + specialize
...
Before we moved to the new frontend, we used to simulate mutual
recursion using high order functions + `[specialize]`. This is not
needed anymore, and the new generated code is more efficient and compact.
@Kha I don't usually indent `mutual` blocks, but I found it helpful
for big ones like this one. Not sure whether we should keep indenting
them or not.
2020-11-13 16:00:33 -08:00
Leonardo de Moura
cca9cceab0
chore: minor cleanup
2020-11-13 16:00:33 -08:00
Leonardo de Moura
5025d7eafd
chore: control generated code size
2020-11-13 16:00:33 -08:00
Leonardo de Moura
35f1844d16
feat: add ParserDescr.checkPrec
2020-11-13 16:00:31 -08:00
Leonardo de Moura
8c4ac7ccc1
refactor: rename LeanInit ==> Meta, and reduce dependencies
2020-11-13 16:00:31 -08:00
Leonardo de Moura
70385b87fa
feat: add instance MonadRef MacroM
2020-11-13 16:00:31 -08:00
Leonardo de Moura
396e767f3d
refactor: move Ref to Prelude and rename it to MonadRef
...
`MacroM` will implement `MonadRef` because
1- It will be easier to throw errors from macros
2- We will be able to `getRef` to retrieve the syntax node at macro
rules.
I renamed `Ref` to `MonadRef` to make it consistent with other classes
providing monadic methods (e.g. `MonadEnv`, `MonadState`, etc).
cc @Kha
2020-11-13 16:00:31 -08:00
Leonardo de Moura
71f62fe5cb
feat: use ParserDescr.nodeWithAntiquot at syntaxAbbrev
2020-11-13 16:00:31 -08:00
Leonardo de Moura
f64d6c4514
feat: add ParserDescr.nodeWithAntiquot
2020-11-13 16:00:31 -08:00
Leonardo de Moura
98ca335a85
chore: fix comment
2020-11-13 16:00:31 -08:00
Leonardo de Moura
51d0579e20
fix: bug at toParserDescr
2020-11-13 16:00:31 -08:00
Leonardo de Moura
d277b53c34
chore: remove dead code
2020-11-13 16:00:31 -08:00
Sebastian Ullrich
1add44916c
chore: remove broken & redundant "new parser Core.lean" benchmark
2020-11-13 21:08:46 +01:00
Sebastian Ullrich
fe03e70a8a
fix: robust linking of cyclically dependent libraries
2020-11-13 21:08:46 +01:00
Leonardo de Moura
b0e8183663
fix: error position for unsolved goals at cases and induction tactics
2020-11-13 07:59:50 -08:00
Leonardo de Moura
d137ecf4e8
feat: improve addLValArg
...
@Kha the module as classes test is now working.
2020-11-12 18:59:59 -08:00
Leonardo de Moura
61dfe2b1db
fix: letDecl
...
use `simpleBinderWithoutType` at `declSig` and `optDeclSig`
2020-11-12 16:22:57 -08:00
Leonardo de Moura
fc6c8e0348
fix: beta reduce value at processAssignmentFOApprox
2020-11-12 14:46:28 -08:00
Leonardo de Moura
367432defc
fix: fixes #217
2020-11-12 14:36:47 -08:00
Leonardo de Moura
cae6aa95dc
feat: support simpleBinder at letDecl
2020-11-12 13:25:38 -08:00
Leonardo de Moura
5c33440050
chore: update Init.lean
2020-11-12 13:23:18 -08:00
Leonardo de Moura
22ff6bb125
chore: process indent' without underscore hack
2020-11-12 12:05:00 -08:00
