Leonardo de Moura
c4dc338d7d
feat(library/compiler): add eager_lambda_lifting skeleton
...
The current commit only detects lambda expressions that should be
lifted eagerly.
@kha I added a comment describing why this optimization is useful.
Right now, we are not writing code that benefits from this optimization,
but it seems very useful for implementing combinators that return
a tuple containing functions. I think this is a useful idiom, for
example, the combinator may have two parts: one that is the actual
action, and another that collects "static properties".
Last summer, if I remember correctly, you considered building this
kind of combinator for the new Lean parser, but gave up because we
did not have compiler support for it. In your case, the "static
property" would be the set of tokens. It could also contain the left
most token for initializing the Pratt parser table, etc.
This commit is the first step to make this kind of code efficient.
It will also improve the experiment at `tests/playground/parser/`
2019-04-17 14:18:47 -07:00
Leonardo de Moura
ad2e7a2d60
chore(library/compiler/specialize): remove dead code
...
In LCNF, a type `ty` at `let x : ty := v in t` must not be irrelevant.
2019-04-17 08:11:39 -07:00
Leonardo de Moura
d662f312df
fix(library/compiler/util): loose bvars
2019-04-17 07:57:30 -07:00
Leonardo de Moura
f12e580ac2
chore(library/compiler/csimp): compilation error in debug mode
2019-04-17 07:41:48 -07:00
Leonardo de Moura
32a309c566
fix(library/compiler/specialize): make sure specialize generates valid LCNF
2019-04-17 07:34:42 -07:00
Leonardo de Moura
5e9f2e4e6a
chore(library/compiler/specialize): remove leftover that is now a noop
2019-04-17 07:14:35 -07:00
Leonardo de Moura
8612c1ecae
chore(library/compiler/util): add debugging helper function
2019-04-16 17:12:09 -07:00
Leonardo de Moura
6b53700d60
test(tests/playground/parser/test1): improve
2019-04-13 08:15:56 -07:00
Leonardo de Moura
a716528067
fix(tests/playground/parser/parser): reset position
2019-04-13 08:07:29 -07:00
Leonardo de Moura
68e8faeef1
test(tests/playground/parser/parser): add sepBy and sepBy1
2019-04-13 07:56:35 -07:00
Leonardo de Moura
52fa06ad38
fix(tests/playground/parser/parser): fix tryFn
2019-04-13 07:36:48 -07:00
Leonardo de Moura
2377b10c2c
test(tests/playground/parser): minor
2019-04-12 09:05:22 -07:00
Leonardo de Moura
52b72c85bf
fix(library/init/data/array/basic): typo
2019-04-12 09:03:20 -07:00
Leonardo de Moura
d7de85e1e7
fix(tests/playground/parser/parser): small bugs
2019-04-12 08:58:02 -07:00
Leonardo de Moura
48ba69775a
fix(tests/playground/parser/syntax): initialization
2019-04-12 08:25:47 -07:00
Leonardo de Moura
bfbdddad1a
fix(library/compiler/emit_cpp): initialization bug
2019-04-12 08:24:06 -07:00
Leonardo de Moura
e53cb81255
test(tests/playground/parser): replace parser.lean with parser2.lean
2019-04-12 07:50:50 -07:00
Leonardo de Moura
87690217c6
test(tests/playground/parser/parser2): add missing definitions
2019-04-12 07:30:43 -07:00
Leonardo de Moura
4aa3036e14
chore(library/init/lean/parser/trie): add HasEmptyc instance
2019-04-12 07:30:06 -07:00
Leonardo de Moura
376830bd0d
chore(tests/playground/parser): missing files and small issues
2019-04-12 07:29:46 -07:00
Leonardo de Moura
da00dae9df
fix(library/compiler/util): typo at has_inline2_attribute
2019-04-11 14:28:54 -07:00
Leonardo de Moura
7461bf9d1d
fix(library/compiler/extract_closed): do not inline closed constants that have been extracted
2019-04-11 14:12:13 -07:00
Leonardo de Moura
b46f5f3eca
fix(library/compiler/reduce_arity): bug at arity_was_reduced
...
It was retuning true for declarations such as
```lean
def f (n : Nat) :=
g._rarg n
```
It should only return true if the nested application is of the form
`f._rarg ...`
2019-04-11 14:12:13 -07:00
Leonardo de Moura
be328bd8e9
test(tests/playground/parser/parser2): add symbol BasicParser
2019-04-10 08:58:41 -07:00
Leonardo de Moura
804ff74350
feat(library/init/data/array/basic): add Array.back
2019-04-10 08:56:42 -07:00
Leonardo de Moura
1c73a4d089
test(tests/playground/parser): add identFn
2019-04-09 09:16:12 -07:00
Leonardo de Moura
0a1b751efd
chore(library/init/data/string/basic): naming consistency
2019-04-09 08:18:29 -07:00
Leonardo de Moura
67ba4d25b1
test(tests/playground/parser/parser2): add number parser
2019-04-09 07:20:35 -07:00
Leonardo de Moura
ab5519c7fe
test(tests/playground/parser/parser2): add recurse
2019-04-08 07:57:45 -07:00
Leonardo de Moura
b633b32f2c
test(tests/playground/parser/parser2): add whitespace and strLit
2019-04-08 07:39:55 -07:00
Leonardo de Moura
363f4449e4
test(tests/playground/parser/parser2): add optional combinator
2019-04-08 06:37:41 -07:00
Leonardo de Moura
deba610203
test(tests/playground/parser/parser2): add many and many1 combinators
2019-04-07 13:41:22 -07:00
Leonardo de Moura
16f9d1a5b6
test(tests/playground/parser/parser2): add node combinator
2019-04-07 13:26:25 -07:00
Leonardo de Moura
9c81cd7f1d
feat(library/init/data/array/basic): add Array.extract
2019-04-07 13:08:23 -07:00
Leonardo de Moura
d7035497f3
test(tests/playground/parser): continue experiment
2019-04-07 12:45:11 -07:00
Leonardo de Moura
8d2d43beb2
feat(library/init/data/array/basic): add shrink
2019-04-07 12:42:56 -07:00
Leonardo de Moura
97ebe4603b
test(tests/playground/parser): add syntax.lean with flat nodes and arrays
2019-04-06 19:36:04 -07:00
Leonardo de Moura
4d3689ea33
feat(library/init/data/array/basic): add new array functions
...
@kha I renamed the homogeneous `map` to `hmap`, and added the
heterogeneous one as `map`. As soon as we add user-defined rewriting
rules, we will be able to replace `map` with `hmap` whenever the types
are the same.
2019-04-06 19:25:32 -07:00
Leonardo de Moura
0c9fe3c7d4
feat(library/compiler): add [inline2] attribute, and stage2 inlining
...
This feature is useful since it allows us to perform inlining
after lambda lifting has been performed.
2019-04-06 08:00:58 -07:00
Leonardo de Moura
d3afb41f51
feat(library/compiler/lambda_lifting): add function detecting lambda_lifting aux declarations
2019-04-06 07:42:45 -07:00
Leonardo de Moura
c54589007e
feat(library/compiler): extract closed terms after caching stage2 decls
2019-04-06 07:19:19 -07:00
Leonardo de Moura
23febc9977
test(tests/playground/parser/parser2): more experiments
2019-04-05 18:09:13 -07:00
Leonardo de Moura
69fb157ff7
chore(tests/playground/parser/parser2): update TODO list
2019-04-05 17:25:36 -07:00
Leonardo de Moura
50d2488946
fix(library/compiler/csimp): cases-merging was failing when scrutinee was a constant
2019-04-05 17:24:01 -07:00
Leonardo de Moura
d603baea70
test(tests/compiler): add new test
2019-04-05 16:58:47 -07:00
Leonardo de Moura
1bb920322d
feat(library/init/lean/compiler/constfolding): constant folding for strictAnd and strictOr
2019-04-05 16:51:29 -07:00
Leonardo de Moura
2cd3954198
chore(library/init/core): remove misleading annotation
...
The compiler will not try to inline definitions tagged as `@[extern]`.
`strictOr` and `strictAnd` must be handled using the constant folding module.
2019-04-05 16:29:44 -07:00
Leonardo de Moura
da9ceea0e5
chore(stage0): update
2019-04-05 16:16:46 -07:00
Leonardo de Moura
1e198ca72e
fix(library/compiler/csimp): missing optimization opportunity
2019-04-05 16:16:24 -07:00
Leonardo de Moura
7b835f3d02
feat(library/compiler/csimp): keep simplifying if cse and elim_dead_let reduced expression
...
Both `cse` and `elim_dead_let` may create new simplification opportunities for `csimp`.
2019-04-05 15:39:43 -07:00
