Leonardo de Moura
870de844dc
chore: annotate relevant monadic code with [alwaysInline]
...
TODO: after we delete old code generator, we should replace
`@[alwaysInline, inline]` with `@[alwaysInline]`.
Remainder: we want the old code generator to ignore `@[alwaysInline]`
annotations, in particular, the new ones on `instance` commands that
are actually annotations for the instance methods.
2022-10-12 19:48:02 -07:00
Gabriel Ebner
38d3e37c75
perf: improve Unhygienic.run code
2022-10-12 19:36:05 -07:00
Leonardo de Moura
b9f174604d
feat: check new alwaysInline attribute
2022-10-12 16:55:16 -07:00
Leonardo de Moura
49a6f8c105
chore: add horrible hack for Decidable in the new code generator
...
cc @gebner
2022-10-12 16:53:29 -07:00
Leonardo de Moura
7308fa0e7d
feat: ensure lambda lifter is creating unused names
2022-10-12 16:35:55 -07:00
Leonardo de Moura
8fe4b75c48
feat: do not inline definitions occurring in instances at the base phase
2022-10-12 16:24:16 -07:00
Leonardo de Moura
5606b4e59e
feat: add [alwaysInline] attribute
...
We are planning to ignore the `[inline]` attribute when the "inlining
quota" has been exhausted in the new code generator.
2022-10-12 16:08:37 -07:00
Gabriel Ebner
fb6cb05465
feat: support let_fun in new compiler
2022-10-12 11:52:28 -07:00
Gabriel Ebner
79569c9003
chore: replace let by have in stx matches
2022-10-12 11:52:28 -07:00
Mario Carneiro
c06cffa54f
refactor: rename isExitCommand -> isTerminalCommand
2022-10-12 11:11:31 -07:00
Mario Carneiro
8dfae9eb38
feat: import command stub
2022-10-12 11:11:31 -07:00
Leonardo de Moura
aa845dee98
feat: cache lambda lifted functions
2022-10-11 21:28:03 -07:00
Leonardo de Moura
767bda2c28
chore: preparing to change the semantics of @[inline] instance
...
In the new code generator, we are going to lambda lift the instance
methods before saving the code at the end of the base phase. The goal is to make instance
ligth weight and cheap to inline. The anotation `@[inline]` is going
to be an annotation for the lambda lifted methods.
2022-10-11 20:35:56 -07:00
Gabriel Ebner
c8bb2ea3cf
chore: post-bootstrap cleanup
2022-10-11 17:24:35 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Gabriel Ebner
45c4f2faa0
refactor: remove _aux_discr
2022-10-11 17:24:35 -07:00
Gabriel Ebner
0d3d05bd3a
feat: clear%
2022-10-11 17:24:35 -07:00
Mario Carneiro
f4b04216eb
feat: go to duplicate definition
2022-10-11 10:07:49 +02:00
Leonardo de Moura
02a3dcb1dd
feat: hash for LCNF.Code
2022-10-10 20:34:12 -07:00
Leonardo de Moura
3f24ce71ab
feat: add another floatLetIn pass at mono phase
2022-10-10 17:19:40 -07:00
Henrik Böving
dd3c0f77f1
feat: FloatLetIn compiler pass
2022-10-10 23:56:20 +02:00
Henrik Böving
d132551829
feat: extend FVarUtil framework
2022-10-10 23:32:36 +02:00
Henrik Böving
e15e6bfaee
chore: address PR comments
2022-10-10 23:32:36 +02:00
Leonardo de Moura
0041de5d1d
fix: congr tactic should not try to synthesize instance implicit arguments that have been inferred when applying congr theorem
...
see #1711
2022-10-10 07:24:27 -07:00
Leonardo de Moura
b20e208867
chore: pretty print LCNF cases result type
2022-10-09 20:13:17 -07:00
Leonardo de Moura
6f023a44ad
fix: let _x.i := _x.j simplification at LCNF simp
2022-10-09 18:38:28 -07:00
Leonardo de Moura
72d3840f0c
feat: add simpCast?
2022-10-09 18:29:12 -07:00
Leonardo de Moura
6c5475725e
feat: (lcCast _ _ g) a_1 ... a_n => g a_1 ... a_n if type correct
2022-10-09 17:45:15 -07:00
Leonardo de Moura
30bd019a7f
chore: simplify SimpValue.lean
2022-10-09 17:35:13 -07:00
Leonardo de Moura
54944819a0
feat: add simpCastCast?
2022-10-09 16:43:33 -07:00
Leonardo de Moura
cd303cd8e5
fix: do not apply simpAppApp? over cast
2022-10-09 16:43:10 -07:00
Leonardo de Moura
cf313d2101
chore: improve eqvTypes
2022-10-09 16:42:55 -07:00
Leonardo de Moura
43fe67c41a
chore: helper pass for debugging purposes
2022-10-09 16:41:54 -07:00
Leonardo de Moura
9feb4d8ab7
fix: do not generate code for [extern] functions
2022-10-09 15:35:29 -07:00
Leonardo de Moura
11fcdb7bf4
feat: add cast at exit points if necessary when inlining code
2022-10-09 13:01:10 -07:00
Leonardo de Moura
ef2d17120c
chore: fix note
2022-10-09 12:25:45 -07:00
Leonardo de Moura
cc09afc5e1
fix: type error introducing when inlining LCNF functions
...
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20LCNF.20errors/near/303142516
2022-10-09 12:10:11 -07:00
Leonardo de Moura
f61ec4929f
chore: add low-level normExprCore
2022-10-09 12:10:11 -07:00
Leonardo de Moura
e81673366a
chore: remove leftover
2022-10-09 12:10:11 -07:00
Leonardo de Moura
613c8027d7
fix: missing instantiateParamsLevelParams
2022-10-09 12:10:11 -07:00
Leonardo de Moura
827ef94486
feat: add eqvTypes
2022-10-09 12:10:11 -07:00
Leonardo de Moura
c14d07fe2e
feat: include def/fun/jp resulting type in the LCNF pretty printer
2022-10-09 12:10:11 -07:00
Leonardo de Moura
eeb98d9cf4
refactor: rename FixedArgs => FixedParams
2022-10-09 12:10:11 -07:00
Leonardo de Moura
37a61568bc
feat: improve fixed parameter analyzer
2022-10-09 12:10:11 -07:00
Leonardo de Moura
8e6cb25cbf
chore: temporarily disable eager lambda lifting
...
We need a better heuristic for deciding which functions in instances
should be eagerly lambda lifted. Otherwise, it will have to keep
chasing which instances we have to annotate with `[inline]`.
2022-10-08 19:51:19 -07:00
Leonardo de Moura
1148392f45
fix: Closure.lean
2022-10-08 19:51:19 -07:00
Leonardo de Moura
2efb1dbdf1
doc: lambda lifting
2022-10-08 19:51:19 -07:00
Leonardo de Moura
b7d4fd03a3
feat: eager lambda lifting
2022-10-08 19:51:19 -07:00
Leonardo de Moura
878e72b2f9
feat: lambda lifting
2022-10-08 19:51:19 -07:00
Leonardo de Moura
3c90b2fd3e
feat: add Decl.save
2022-10-08 19:51:19 -07:00
