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
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
d536ee347d
chore(runtime/object): remove fixpoint* primitives
2019-03-27 13:17:25 -07:00
Leonardo de Moura
414c03363c
chore(stage0): update
2019-03-27 13:13:34 -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
1f11429f98
feat(frontends/lean): add partial keyword
2019-03-26 16:09:55 -07:00
Leonardo de Moura
4b83585103
chore(stage0, runtime): update stage0 and remove old String API
2019-03-26 15:51:13 -07:00
Leonardo de Moura
dd48d5ae18
feat(runtime/object): implement string primitives using Nat index
2019-03-26 15:27:14 -07:00
Leonardo de Moura
af16e79ed0
chore(stage0): update
2019-03-26 14:52:24 -07:00
Leonardo de Moura
f1f2994781
chore(library/compiler/emit_cpp): update
2019-03-26 14:51:14 -07:00
Leonardo de Moura
0d5ac5288a
feat(runtime): increase small nat size
...
In 64-bit machines, the max small nat value should now be (2^63 - 1), and on 32-bit
machines (2^32 - 1).
The main motivation for this modification are the array indexing
operations. With the new representation, if a Nat index is not small,
then it must not be a valid index. This was not true in 64-bit
machines. Example: an array of size 2^33 would fit in memory, and but
an index `i` > 2^32 - 1 would not be a small nat value.
2019-03-26 14:21:03 -07:00
Leonardo de Moura
b0da4360d0
chore(runtime, library/init/data/string/basic): prepare to change String.Pos
2019-03-26 12:25:12 -07:00
Leonardo de Moura
d7bf1821a6
chore(stage0): update
2019-03-26 11:11:47 -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
Sebastian Ullrich
2df060be44
feat(frontends/lean/elaborator): node!: support parameterized parsers
2019-03-26 11:21:53 +01:00
Leonardo de Moura
b10e824d94
chore(stage0): update
2019-03-25 16:48:11 -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
