Leonardo de Moura
a2631ce037
fix: panic when Syntax.missing
...
I got a panic error message today in VS Code because of this function.
It is weird because, as far as I can tell, this function is only used by
the `register_simp_attr` macro, and this macro was not being used in
the files I was editing.
I think the fix is resonable for a `Syntax.missing` case.
cc @gebner
2022-09-12 16:10:14 -07:00
Leonardo de Moura
506cf01d94
fix: bug at simpCasesOnCtor?
2022-09-12 16:02:19 -07:00
Leonardo de Moura
b777d411ec
feat: add useRaw parameter at constructorApp?
...
and document this API.
2022-09-12 15:56:36 -07:00
Leonardo de Moura
e08d48c591
feat: track ground let-declarations at Specialize.lean
2022-09-12 14:05:45 -07:00
Leonardo de Moura
ec2372e8d4
feat: add Specialize.lean skeleton
2022-09-11 20:19:44 -07:00
Leonardo de Moura
44c67f72c1
feat: add LCNF/SpecInfo.lean
2022-09-11 20:19:44 -07:00
Leonardo de Moura
54f1193739
chore: add maybeTypeFormerType
2022-09-11 20:19:44 -07:00
Leonardo de Moura
f0d75258ae
feat: treat erased arguments as fixed arguments
...
It also renames `Lean.Expr.erased` => `Lean.Expr.isErased`
2022-09-11 20:19:44 -07:00
Leonardo de Moura
613523e1f6
feat: store borrow flag at Param
...
It is more robust that using `Expr.mdata`, and we save the information at `toLCNF`.
2022-09-11 20:19:44 -07:00
Leonardo de Moura
e78820e6a5
feat: add mkFixedArgMap
2022-09-11 20:19:44 -07:00
Henrik Böving
a03ea65d73
refactor: monadic compiler test framework style + new pass manager
2022-09-10 15:00:05 -07:00
Henrik Böving
c6db1099d0
feat: add occurences and phases to PassManager
2022-09-10 14:58:49 -07:00
Leonardo de Moura
ca098d3769
feat: inline applications of the form inline (f ...)
...
The `inline` identity function is a directive for the compiler.
2022-09-10 13:28:49 -07:00
Leonardo de Moura
1953f5953f
chore: dangling file
2022-09-10 13:23:14 -07:00
Leonardo de Moura
f1c150228b
fix: fixes #1558
2022-09-09 15:27:51 -07:00
Leonardo de Moura
353eb0dd27
fix: disable auto implicit feature when running tactics
...
fixes #1569
2022-09-09 15:17:50 -07:00
Leonardo de Moura
9f134cad8e
chore: remove leftover
...
7c3826d3e9
2022-09-09 15:06:47 -07:00
Leonardo de Moura
abf514378b
fix: fixes #1575
2022-09-09 15:05:21 -07:00
Leonardo de Moura
7c3826d3e9
fix: fixes #1576
2022-09-09 14:29:48 -07:00
Henrik Böving
5514339ffd
fix: visit jp bodies in join point finder
2022-09-08 15:21:53 -07:00
Leonardo de Moura
e39c3af5bb
chore: remove [inline] from parser combinators
2022-09-08 14:50:27 -07:00
Leonardo de Moura
a40118c79d
chore: disable eager applyCasesOnImplementedBy
...
It must be performed at phase 2.
We still want to perform the regular `[implementedBy]` replacements at
phase 1 since they affect code specialization.
2022-09-08 14:50:27 -07:00
Leonardo de Moura
1c188b62cd
chore: typo
2022-09-08 14:50:27 -07:00
Gabriel Ebner
fb259f95db
feat: remove description argument from register_simp_attr
2022-09-08 14:49:43 -07:00
Leonardo de Moura
5b969b75bd
chore: fix build
2022-09-08 14:23:18 -07:00
Henrik Böving
f912349a29
fix: compiler test framework style
2022-09-08 14:09:14 -07:00
Henrik Böving
d2f7e724ac
feat: findJoinPoints pass
2022-09-08 14:09:14 -07:00
Leonardo de Moura
26e304261f
fix: PullFunDecls.lean
...
Use topological sort.
2022-09-07 22:41:05 -07:00
Leonardo de Moura
0a21603cdc
feat: apply implementedBy replacements at second simp pass
2022-09-07 20:38:16 -07:00
Leonardo de Moura
07bdab45d2
feat: apply casesOn implementedBy replacements
2022-09-07 20:37:09 -07:00
Leonardo de Moura
bd21583d4b
fix: ComputedFields.lean
...
`all` fields was not being set correctly.
TODO: check `all` fields in the kernel.
2022-09-07 20:35:59 -07:00
Leonardo de Moura
ea3235c551
fix: skip casesOn recursors at code generation
2022-09-07 18:46:48 -07:00
Leonardo de Moura
19f5fe6f42
feat: add getSpecializationArgs?
2022-09-07 16:08:45 -07:00
Leonardo de Moura
55171a893a
feat: elaborate specialization arguments
2022-09-07 15:22:56 -07:00
Leonardo de Moura
f611a6e52f
feat: add specialize attribute parser
2022-09-07 14:50:29 -07:00
Leonardo de Moura
735dabdb3f
refactor: use ParametricAttribute to implement [specialize]
2022-09-07 13:17:24 -07:00
Leonardo de Moura
661eb39bc8
feat: add inlinePartial config option
2022-09-06 20:46:17 -07:00
Leonardo de Moura
f4fbf92313
fix: make privateToUserNameAux more robust
2022-09-06 17:15:56 -07:00
Leonardo de Moura
85851d0c43
fix: bug at PullFunDecls
2022-09-06 17:15:56 -07:00
Leonardo de Moura
56f0d6c183
feat: specialize partial applications of local functions
2022-09-06 06:44:33 -07:00
Leonardo de Moura
c769808a4e
chore: add TODO
2022-09-05 19:35:17 -07:00
Leonardo de Moura
1812e86c7f
feat: eta expand partial applications of functions that take local instances as arguments
2022-09-05 19:33:22 -07:00
Leonardo de Moura
bf44e9fb2f
fix: bug at inferProjType for LCNF
2022-09-05 19:23:35 -07:00
Leonardo de Moura
3e210d9f26
chore: helper functions, missing instance
2022-09-05 19:20:31 -07:00
Leonardo de Moura
7113d71cd2
doc: LCNF/Simp.lean docstrings
2022-09-05 17:36:35 -07:00
Leonardo de Moura
1207e5e285
feat: erase cases when all alternatives are the same
2022-09-05 17:22:54 -07:00
Leonardo de Moura
58d8224d9e
feat: add LCNF cases default
2022-09-05 14:08:14 -07:00
Gabriel Ebner
451f6df5df
fix: IO.waitAny requires nonempty list
2022-09-05 08:52:46 -07:00
Leonardo de Moura
553addc078
feat: alpha equivalence for LCNF code
2022-09-05 08:06:05 -07:00
Leonardo de Moura
fde8d35bbb
refactor: declare passes when declaring transformations
2022-09-05 06:58:32 -07:00
