Leonardo de Moura
bb06fbaa8a
test: smart unfolding
2020-11-15 16:36:22 -08:00
Leonardo de Moura
717178392c
chore: update stage0
2020-11-15 16:35:46 -08:00
Leonardo de Moura
461c0786fd
feat: generate auxiliary declaration for "smart unfolding"
2020-11-15 16:31:40 -08:00
Leonardo de Moura
0ca7dabb2a
chore: update stage0
2020-11-15 15:08:26 -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
0bf703b17c
chore: remove misleading comment
...
It doesn't loop in Lean 4.
2020-11-14 18:07:19 -08:00
Leonardo de Moura
73dec1be45
test: add tests for Lean3 bugs
2020-11-14 18:04:22 -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
a6c3a17702
chore: update stage0
2020-11-14 08:42:44 -08:00
Leonardo de Moura
0ddc2e5efb
chore: remove builtin subtype notation
2020-11-14 08:42:03 -08:00
Leonardo de Moura
1a8dafccc5
chore: update stage0
2020-11-14 08:36:57 -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
053e09c5e6
chore: fix test
2020-11-14 08:16:47 -08:00
Leonardo de Moura
b2cf4751d7
chore: update stage0
2020-11-14 08:12:51 -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
db56a5132e
chore: update stage0
2020-11-14 07:04:57 -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
646f2bdefe
chore: update stage0
2020-11-13 16:32:05 -08:00
Leonardo de Moura
ffc4abed32
fix: UInt* and USize Inhabited instances
2020-11-13 16:30:48 -08:00
Leonardo de Moura
b9f1999e32
chore: update stage0
2020-11-13 16:00:33 -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
25a887ff35
chore: update stage0
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
dfce991368
chore: update stage0
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
99d788665e
chore: update stage0
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
75120000ff
chore: update stage0
2020-11-12 19:02:13 -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
