max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
16273 commits 1 branch 0 tags 5.3 GiB
Commit graph

5602 commits

Author SHA1 Message Date
Leonardo de Moura
4bbecf93ed fix(library/compiler/eager_lambda_lifting): assertion violation 2019-04-17 18:02:48 -07:00
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
bfbdddad1a fix(library/compiler/emit_cpp): initialization bug 2019-04-12 08:24:06 -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
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
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
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
Leonardo de Moura
6c44a5d997 feat(library/compiler/csimp): add Thunk.get (Thunk.mk f) ==> f () simplification 2019-04-05 14:55:48 -07:00
Leonardo de Moura
48fbaefa2a chore(library/constants.txt): remove leftover 2019-04-05 14:29:51 -07:00
Leonardo de Moura
994ca779ef feat(library/compiler/csimp): improve try_inline_instance 2019-04-05 14:16:38 -07:00
Leonardo de Moura
3d393d9b1d fix(library/compiler/csimp): bug introduced earlier today 2019-04-02 17:21:25 -07:00
Leonardo de Moura
6ab935ebf6 feat(library/compiler/csimp): merge equal casesOn branches 2019-04-02 11:06:07 -07:00
Leonardo de Moura
95ca283854 chore(library/compiler/csimp): remove m_proj2var, we can use m_var2ctor instead 2019-04-02 10:05:20 -07:00
Leonardo de Moura
005d62185d feat(library/compiler/csimp): add "case merging" optimization 2019-04-02 09:41:53 -07:00
Leonardo de Moura
12595fb501 feat(library/compiler/specialize): cache whenever possible 
There were many opportunities for reusing previously specialized code at
stdlib
 2019-03-29 15:21:17 -07:00
Leonardo de Moura
9d325515d4 chore(library/compiler/util): reduce term size if possible 2019-03-28 17:35:12 -07:00
Leonardo de Moura
8c58314b84 fix(library/compiler/csimp): lc_unreachable simplifications 
The simplifications were introducing dangling free variables.
 2019-03-28 17:32:41 -07:00
Leonardo de Moura
1ebdb9f1b1 fix(library/compiler): do not inline definitions using unsafe inductives 
This commit also makes sure that `has_trivial_structure` returns false
for `unsafe` inductive datatypes.

See new test for further details.
 2019-03-28 16:07:57 -07:00
Leonardo de Moura
427d3b4d40 chore(library/compiler/specialize): reduce stack consumption 2019-03-28 15:05:48 -07:00
Leonardo de Moura
4dbae58646 fix(library/equations_compiler): make sure _unsafe_rec auxiliary definitions contain all local constants used in the safe one 
cc @kha
 2019-03-28 12:57:15 -07:00
Leonardo de Moura
1f197b5293 feat(library/equations_compiler/unbounded_rec): check whether f._unsafe_rec and f have the same type 
`f._unsafe_rec` is the auxiliary definition created by the equation
compiler to help the code generator to produce better code.
 2019-03-28 12:39:44 -07:00
Leonardo de Moura
b74a9b63de feat(library/equations_compiler/partial_rec): improve base case synthesis 2019-03-28 10:19:57 -07:00
Leonardo de Moura
0161ef8487 fix(library/compiler/name_mangling): bug 2019-03-28 08:23:38 -07:00
Leonardo de Moura
42fbe3c18c chore(library/init,runtime,library/compiler): add fix primitive back 
The new `partial def`s allow us to define `fix` in Lean, but the Lean
implementation is not as efficient as the native one. The native one
in C++ use weak pointers to prevent a closure allocation at every
recursive invocation.

This commit also fixes the `fixCore` helper functions that were broken
after we switched to camelCase.

We have updated the test `fix1.lean` to demonstrate the native
implementation is faster. Here are the numbers on my desktop.

```
./run.sh fix1.lean 24
721420279
Time for 'native fix': 816ms
721420279
Time for 'fix in lean': 1.34s
```
 2019-03-27 17:13:53 -07:00
Leonardo de Moura
9b47d134ae feat(library/equations_compiler/partial_rec): consider elements before : when constructing base case 2019-03-27 13:49:23 -07:00
Leonardo de Moura
a43a40b7f5 chore(library/init): remove fix.lean 
`partial def` is much more general
 2019-03-27 13:11:00 -07:00
Leonardo de Moura
62d7cc6b37 feat(library/init/wf): remove wf_term_hack 2019-03-27 12:41:16 -07:00
Leonardo de Moura
895bf2c91d feat(library/equations_compiler/partial_rec): try assumption if inhabitant could not be found 2019-03-27 12:24:24 -07:00
Leonardo de Moura
9a071c18e7 feat(library/equations_compiler): add support for partial definitions 2019-03-27 11:09:32 -07:00
Leonardo de Moura
ef5fac1481 chore(library/equations_compiler): add partial_rec skeleton 2019-03-27 08:37:59 -07:00
Leonardo de Moura
9ddc778ac3 feat(library/equations_compiler/equations): add m_is_partial to equation header 2019-03-26 16:18:43 -07:00
Leonardo de Moura
f1f2994781 chore(library/compiler/emit_cpp): update 2019-03-26 14:51:14 -07:00
Leonardo de Moura
681f3ec81b fix(library/compiler/llnf): constructor reuse 
We were not reusing constructor values for constructors that contained only
scalar values.
 2019-03-26 11:10:51 -07:00
Leonardo de Moura
3ad7d2ba81 fix(library/compiler/lcnf): disable transformation for Bool 
@kha Here is another motivation for re-implementing the equation compiler.
 2019-03-25 16:48:11 -07:00
Leonardo de Moura
7db4f60e50 feat(library/init/core): eagerly expanding Decidable.toBool seems to be a bad idea 
After we erase types and proofs, `Decidable.toBool` can be replaced with
the identity function since `Decidable A` and `Bool` have the same
runtime representation. By eagerly expanding `toBool`, we introduce
unnecessary `cases` expressions.
 2019-03-25 16:48:11 -07:00
Leonardo de Moura
87cab24a1d fix(library/compiler/csimp): at_most_once at elim_jp1_fn 
`elim_jp1_fn` was incorrectly expanding join points that were used more
than once. The issue is that the `foreach` combinator "may" skip nodes
that have already been visited.
 2019-03-25 14:19:11 -07:00
Leonardo de Moura
df9ce10623 feat(library/compiler): special support for initialization functions of the form def initFn : IO Unit 
We can now write
```
@[init] def initFn : IO Unit := ...
```
instead of
```
def initFn : IO Unit := ...
@[init initFn] constant execInitFn : Unit := ()
```
 2019-03-23 08:46:38 -07:00
Leonardo de Moura
3d52298c69 chore(util/sexpr): preparing to port options to Lean 2019-03-22 13:58:16 -07:00
Leonardo de Moura
50207e2c5a chore(library/constants.txt): remove dead variables 2019-03-22 13:26:48 -07:00