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
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
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
8ec95767d7
chore(stage0): update
2019-04-05 14:18:50 -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
de880dc15f
chore(stage0): update
2019-04-04 15:26:43 -07:00
Leonardo de Moura
861a292d8f
chore(stage0): update
2019-04-03 13:29:09 -07:00
Leonardo de Moura
273a0775d6
perf(library/init/data/array): mkArray in Lean doesn't seem to buy us anything
...
The primitive implementation combines all `inc`'s into a single one.
2019-04-03 10:27:58 -07:00
Leonardo de Moura
2c72888af4
chore(stage0): update
2019-04-03 05:59:37 -07:00
Leonardo de Moura
ee050431e0
feat(runtime): add primitive hash functions
2019-04-03 04:01:36 -07:00
Leonardo de Moura
a46e27a3d7
feat(runtime/hash): use size_t instead of unsigned
2019-04-03 03:19:50 -07:00
Leonardo de Moura
02e6f953c8
chore(stage0): update
2019-04-03 03:02:20 -07:00
Leonardo de Moura
9745f70fe2
chore(stage0): update
2019-04-02 17:22:19 -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
9d62e9ef79
chore(stage0): update
2019-04-02 11:18:55 -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
c4ad8f3dbc
chore(stage0): update
2019-04-02 09:54:32 -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
498758bdfc
chore(stage0): update
2019-04-02 09:41:18 -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
1be1f3c4ea
fix(stage0): missing file
2019-03-29 11:42:16 -07:00
Leonardo de Moura
c134617ee3
fix(library/init/data/array/basic): mkEmpty
2019-03-29 11:20:45 -07:00
Leonardo de Moura
229e4a25b3
refactor(library/init/array): implement mkArray in Lean, add allow mkEmpty to set initial capacity
2019-03-29 10:19:21 -07:00
Sebastian Ullrich
21f1d231b8
fix(runtime/object): do not return temporary borrowed reference from a builtin
2019-03-29 14:32:15 +01:00
Sebastian Ullrich
5b8c2574ed
feat(shell/CMakeLists): build stdlib using -g in debug mode
2019-03-29 14:32:12 +01: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
cd21793b53
fix(frontends/lean/elaborator): assertion violation
...
Prevent assertion violation when processing examples such as:
```
@[pattern] def badPattern (x : Nat) : Nat := 0
def tst (y : Nat) : Nat :=
match y with
| (@badPattern _) := 1
| _ := 2
```
The `x` is not used in `badPattern`. Thus, the elaborator fails to
synthesize the metavariable corresponding to `_` at `@badPattern _`.
The fix detects this kind of instance, but I commented the code the
throws the error because we would prevent us from compiling `term.lean`.
The assertion violation was originally triggered by the pattern definition
```
@[pattern] def «explicitBinderContent» (requireType : optParam.{1} Bool Bool.false) :=
{SyntaxNodeKind . name := `Lean.Parser.Term.explicitBinderContent}
at
...
view := fun stx, let (stx, i) := match stx.asNode : _ -> Prod Syntax Nat with
| some {kind := @«explicitBinderContent» requireType, -- << HERE
args := [stx], ..} := ...
```
These definitions were generated by the node choice macro.
cc @kha
2019-03-27 16:42:59 -07:00
Leonardo de Moura
ea3a38c5d3
chore(runtime/object): style
2019-03-27 14:08:10 -07:00
Leonardo de Moura
af05e7257d
chore(stage0): update
2019-03-27 13:55:08 -07:00
