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

5812 commits

Author SHA1 Message Date
Leonardo de Moura
4793cbfa9a feat: add #[elem1, elem2, ..] notation for creating arrays 
@kha @dselsam: I added this notation because I am tired of writing
`[elem1, elem2, ...].toArray`. BTW, the new notation is based on the
one available in SML.
 2019-10-07 15:36:44 -07:00
Leonardo de Moura
c81ab9759f feat: add elimDeadBranches 2019-10-07 13:59:00 -07:00
Leonardo de Moura
81847302a7 feat(library/compiler): replace @[effectful] with @[neverExtract] 2019-10-01 14:06:08 -07:00
Leonardo de Moura
261c0b9c24 feat(frontends/lean): add panic! macro 
cc @dselsam
 2019-09-30 17:16:19 -07:00
Leonardo de Moura
75bdc8712e feat(library/compiler): disable a few optimizations for declarations tagged with @[effectful] 
@kha @dselsam:
The main motivation for this change are functions such as `panic`.
I marked `panic` with the attribute `@[effectful]`.
Here is the summary of the changes. If `f` is marked as `@[effectful]`
1- Compiler will not perform common subexpression elimination on terms of the form `f ...`.
2- Compiler will not extract closed terms of the form `f ...`.
3- Compiler will throw an error if `f` is partially applied.
 2019-09-30 16:53:11 -07:00
Sebastian Ullrich
ce558b6a9e doc(library/compiler/ir_interpreter): update docs 2019-09-20 10:46:33 +02:00
Leonardo de Moura
0bd268fc96 fix(library/compiler/erase_irrelevant): add elim_array_cases 2019-09-19 10:47:05 -07:00
Sebastian Ullrich
31c170117e feat(frontends/lean/builtin_cmds,library/compiler/ir_interpreter): reimplement #eval 2019-09-19 17:52:18 +02:00
Sebastian Ullrich
61819bee6d refactor(library/compiler/ir_interpreter): make box_t/unbox_t total 2019-09-19 17:51:51 +02:00
Leonardo de Moura
8148136aa9 fix(util/nat): nat::get_small_value must return size_t since unbox now returns size_t 2019-09-18 17:13:46 -07:00
Leonardo de Moura
b36caf701a chore(library/print): minor improvements 2019-09-17 17:17:46 -07:00
Sebastian Ullrich
a083cab532 fix(library/compiler/ir_interpreter): fix UB sequencing found by GCC 2019-09-17 09:51:24 +02:00
Leonardo de Moura
06327238e6 fix(library/compiler/erase_irrelevant): assertion violation 
cc @Kha
 2019-09-16 07:21:19 -07:00
Leonardo de Moura
306ff7d7e5 fix(library/compiler): fixes #34 
`csimp` assumes constructors and `casesOn` applications match.  That
is, given `I.casesOn x ...`, then if `x` is an constructor, then it is
a constructor of the inductive datatype `I`.
The transformation `erase_irrelevant` was violating this property when
it mixes `Decidable` and `Bool`. We fix this issue by mapping
`Decidable.casesOn`, `Decidable.isTrue` and `Decidable.isFalse` to
`Bool.casesOn`, `Bool.true` and `Bool.false` respectively.
 2019-09-13 10:20:50 -07:00
Sebastian Ullrich
a1bc3164e8 refactor(library/compiler/ir_interpreter): remove case type inference 2019-09-12 18:38:10 +02:00
Sebastian Ullrich
6c4976e044 perf(library/compiler/ir_interpreter): push_frame: avoid frame copy 
6.4% speedup on unionfind
 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
7c6668d5c2 perf(library/compiler/ir_interpreter): no need for decl lookup at tail recursion 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
8dd851d64f perf(library/compiler/ir_interpreter): cache environment lookup in existing symbol cache 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
0c71a493d0 feat(library/compiler/ir_interpreter): check system at the start of each function 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
ea9a5de498 fix(library/compiler/ir_interpreter): values of unboxed types should be stored unboxed 
We previously boxed all such values to `object *`s. However, because this does not correspond to the IR types, there are
no `dec` instructions to actually free these values.
 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
79588d2ce6 refactor(library/compiler/ir_interpreter): replace C++ template with Python template 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
944de141d3 perf(library/compiler/ir_interpreter): use specialized stubs 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
693fc63702 fix(library/compiler/ir_interpreter): constants do not have to be persistent anymore, so stop leaking them 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
8da203b91a perf(compiler/ir_interpreter): do not allocate temp closure for saturated partial applications 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
237e4a4489 feat(library/compiler/ir_interpreter): multi-threading support 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
daae0f67bb fix(library/compiler/ir_interpreter): --run ignored first argument 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
c23e6829c0 refactor(library/compiler/ir_interpreter): move constant caching into load 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
2d04ecc704 refactor(util/object_ref): move and adjust cnstr_get_ref_t 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
3ee59aa17f feat(library/compiler/ir_interpreter): add Windows support 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
1732461a66 doc(library/compiler/ir_interpreter): add a few comments 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
d27cbe2dc5 perf(library/compiler/ir_interpreter): cache symbol lookup 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
2d4276e819 feat(library/compiler/ir_interpreter): tail recursion 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
bdb7152768 feat(library/compiler/ir_interpreter): cache constants 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
9015fc1e34 chore(library/compiler/ir_interpreter): add step-level trace 2019-09-12 18:26:15 +02:00
Sebastian Ullrich
558d9ad837 feat(library/compiler/ir_interpreter): add call-level trace 2019-09-12 18:22:02 +02:00
Sebastian Ullrich
795359ee49 feat(shell/lean): re-add --run flag 2019-09-12 18:22:02 +02:00
Sebastian Ullrich
99bc069fdd feat(library/compiler/ir_interpreter): implement IR interpreter 2019-09-12 18:22:02 +02:00
Leonardo de Moura
8e47b6396f chore(library/init/lean/compiler/ir): simplify mkCase, the xType field is set by explicitBoxing 2019-09-12 08:55:09 -07:00
Leonardo de Moura
0284d4a7a2 chore(library/compiler/ir): use new mkCase 2019-09-12 08:23:29 -07:00
Leonardo de Moura
3e6736b374 feat(library/compiler/util): add support for trivial structures at mk_runtime_type 2019-09-11 13:41:41 -07:00
Leonardo de Moura
1062dcbbea refactor(src/library/compiler/erase_irrelevant): move has_trivial_structure to util 2019-09-11 13:04:08 -07:00
Sebastian Ullrich
fdc30e3097 chore(library/type_context): revert "simple instance pre-filtering" 
This reverts commit ab2e66e4a3.

This hack is not immediately needed anymore and will hopefully be
replaced with a much better design in the future
 2019-09-11 19:51:25 +02:00
Leonardo de Moura
f7af9a73bd chore(library/init/lean/compiler/ir): move addBoxedVersion to entry point file 2019-09-09 10:35:52 -07:00
Leonardo de Moura
a188bb8497 chore(library/init/lean/compiler/ir): remove emitcpp 2019-09-07 19:46:22 -07:00
Leonardo de Moura
dcd15f3424 refactor(runtime): C backend 2019-08-24 07:40:38 -07:00
Leonardo de Moura
6d6cb14f9e feat(library/init/lean/compiler/ir/emitc,shell/lean): add --c=<filename> option 2019-08-20 10:13:40 -07:00
Leonardo de Moura
b2693962bd chore(library/init/lean): export as C functions 2019-08-17 07:30:07 -07:00
Leonardo de Moura
66304d83a0 chore(library/init/lean/compiler): export as C functions 2019-08-17 06:58:36 -07:00
Leonardo de Moura
4429aac0b3 chore(library/compiler/ir): remove box(13) hack 2019-08-16 20:58:30 -07:00
Leonardo de Moura
ec0e74f5f8 chore(library/init/lean): export as C functions 2019-08-16 20:52:10 -07:00