Leonardo de Moura
fb77d71d23
feat(library/init/lean/attributes): export attribute API
2019-06-05 16:55:47 -07:00
Leonardo de Moura
d212abb9ee
feat(library/init/lean/syntax): export helper functions for creating syntax in C++
2019-06-05 16:49:58 -07:00
Leonardo de Moura
02847f6dc7
chore(stage0): update
2019-06-05 15:29:13 -07:00
Leonardo de Moura
fd29b7e45d
feat(util/io): add helper functions for consuming IO results in C++
2019-06-05 13:53:38 -07:00
Leonardo de Moura
642992eeca
chore(library/init/lean/attributes): missing @[export]
2019-06-05 13:30:26 -07:00
Leonardo de Moura
e379d58802
chore(stage0): update
2019-06-05 13:18:59 -07:00
Sebastian Ullrich
1f51a96794
chore(stage0): fix build
2019-06-05 10:54:01 +02:00
Leonardo de Moura
4ee3332763
chore(stage0): update
2019-06-04 16:56:53 -07:00
Leonardo de Moura
4a26f0028c
chore(library/init/lean/environment): remove unnecessary function
2019-06-03 15:17:40 -07:00
Leonardo de Moura
ed1a433d52
feat(library/init/lean/modifiers): add privatePrefix
2019-06-03 10:33:40 -07:00
Leonardo de Moura
224195a1fb
feat(library/init/lean/modifiers): environment extension for private declarations
2019-06-03 10:10:00 -07:00
Leonardo de Moura
cd73105dff
refactor(kernel/environment,library/private,library/init/lean/environment): move main module name to header
2019-06-03 09:14:23 -07:00
Leonardo de Moura
23029cb386
chore(stage0): update
2019-06-03 08:24:53 -07:00
Leonardo de Moura
c92fe75053
fix(library/init/lean/compiler/constfolding): Usize => USize
...
Camel case auto-conversion bug.
2019-06-01 09:42:22 -07:00
Leonardo de Moura
70c9733897
chore(stage0): update
2019-05-30 09:41:16 -07:00
Leonardo de Moura
8333e48037
chore(stage0): update
2019-05-30 09:16:09 -07:00
Leonardo de Moura
0e8abd81bb
chore(stage0): update
2019-05-25 16:35:43 -07:00
Leonardo de Moura
074002eb84
chore(stage0): update
2019-05-23 18:34:22 -07:00
Leonardo de Moura
c6f717e55b
chore(stage0): update
2019-05-23 18:20:12 -07:00
Leonardo de Moura
f9f4e6c14b
feat(library/init/lean/compiler/ir): add expandresetreuse
2019-05-23 08:58:16 -07:00
Leonardo de Moura
aede2476de
chore(stage0): update
...
We changed the IR representation, and the C++ code interacts with both
stage0 and stage1.
2019-05-23 08:22:36 -07:00
Leonardo de Moura
3e76e43843
fix(library/init/lean/compiler/ir/borrow): visit join point body
2019-05-22 17:31:56 -07:00
Leonardo de Moura
fe0141918a
fix(library/init/lean/compiler/ir) bug at addDecAfterFullApp
2019-05-22 16:30:42 -07:00
Leonardo de Moura
a570e35161
chore(stage0): update
2019-05-22 11:45:58 -07:00
Leonardo de Moura
2408d6dd80
fix(library/init/lean/compiler/ir/boxing): created boxed version for externs
2019-05-22 10:56:51 -07:00
Leonardo de Moura
fa3079f04e
chore(stage0): update
2019-05-22 10:36:36 -07:00
Leonardo de Moura
f1fbe5cd61
feat(library/compiler/ir): add boxed version for extern constants
2019-05-21 17:55:58 -07:00
Leonardo de Moura
89259d012b
fix(stage0): missing files
2019-05-21 16:39:07 -07:00
Leonardo de Moura
91745cd16b
fix(library/init/lean): remove hard coded file
2019-05-21 16:26:08 -07:00
Leonardo de Moura
8003ccec13
chore(stage0): update
2019-05-21 16:12:26 -07:00
Leonardo de Moura
db6933e3a4
chore(stage0): update
...
Make sure the new IR checker is used to validate generated code.
2019-05-21 13:45:49 -07:00
Leonardo de Moura
3ffe0e22c8
feat(shel/lean): add temporary option for testing new IR compiler code emitter
2019-05-20 10:19:09 -07:00
Leonardo de Moura
b0e7b05f63
feat(library/init/lean/compiler/ir/emitcpp): add entry point
2019-05-20 09:50:57 -07:00
Leonardo de Moura
905b94311b
fix(library/init/lean/compiler/ir/borrow): tail call preservation
2019-05-19 17:08:51 -07:00
Leonardo de Moura
83692eef6d
feat(library/init/lean/compiler/ir): explicit RC
2019-05-19 16:46:51 -07:00
Leonardo de Moura
300c251b49
feat(library/init/lean/compiler/ir): add explicitBoxing to new IR compiler stack
2019-05-19 08:10:45 -07:00
Leonardo de Moura
ca818e6850
feat(library/init/lean/compiler/ir): add borrow inference
2019-05-18 10:48:26 -07:00
Leonardo de Moura
c9bcd4990c
feat(library/compiler): register extern constants into the new IR
2019-05-17 17:12:51 -07:00
Leonardo de Moura
ac69f802e1
feat(library/compiler): interface with new IR compiler entry point
2019-05-16 15:41:47 -07:00
Leonardo de Moura
5482a11642
feat(library/init/lean/compiler/ir/default): add new entry point
2019-05-16 10:20:00 -07:00
Leonardo de Moura
2d065c7ded
feat(library/init/lean/compiler/ir): add Lean.IR.CompilerM
...
and environment extension for storing Lean IR declarations.
2019-05-16 10:20:00 -07:00
Leonardo de Moura
b87afdcbfd
chore(library/init/lean/compiler/closedtermcache): naming convention
2019-05-15 15:19:09 -07:00
Leonardo de Moura
09df708af2
feat(library/init/lean/compiler): implement close term cache env extension in Lean
2019-05-15 11:01:25 -07:00
Leonardo de Moura
89e01368cd
fix(library/init/lean/environment): throw error if environment already contains constant
2019-05-15 11:01:25 -07:00
Leonardo de Moura
3193e91aff
feat(library/init/lean/environment): add Environment.displayStats and --stats command line argument
2019-05-15 11:01:25 -07:00
Leonardo de Moura
bc809643ec
feat(library/init/lean/expr): add Expr.quickLt, Expr.eqv
2019-05-15 11:01:25 -07:00
Leonardo de Moura
8ab15536a7
perf(library/init/data/array/binsearch): add binSearchContains
2019-05-14 20:52:57 -07:00
Leonardo de Moura
45eda6d81b
perf(library/init/lean/modifiers): add only local entries to state
...
We can use `getModuleEntries` and `getModuleIdxFor` to test whether a
constant is protected or not.
2019-05-14 20:30:46 -07:00
Leonardo de Moura
dc71fafac1
feat(library/init/data/array): add Array.binSearch
2019-05-14 18:25:54 -07:00
Leonardo de Moura
2e4f5951e3
feat(library/init/data/array/qsort): simple quicksort
...
@kha I added `qsort` for sorting environment extension entries, but I am
wondering if we could use it as a benchmark in our paper. It is a pure implementation; it is
fast; it implements the real quick sort algorithm with in-place updates if the
input array is not shared. If the array is shared it performs
a single copy and then switches to in-place updates.
2019-05-14 17:46:34 -07:00
