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

5825 commits

Author SHA1 Message Date
Leonardo de Moura
0c463e17f5 chore: update stage0 2019-10-26 16:37:56 -07:00
Leonardo de Moura
423b0fed3a refactor: use Array Expr at DelayedMVarAssignment 2019-10-25 12:03:09 -07:00
Leonardo de Moura
34acf2003c chore: rename assign delayed method 2019-10-25 10:44:42 -07:00
Leonardo de Moura
a50515e0d6 chore: use => instead of Lean3 , 2019-10-24 15:10:19 -07:00
Leonardo de Moura
b709979102 feat: improve arity guesser for IO extern primitives 2019-10-23 17:29:41 -07:00
Leonardo de Moura
f88561ae68 feat: add trace! macro 2019-10-22 16:08:37 -07:00
Leonardo de Moura
30571f12d4 chore: adjust runtime to new EState 2019-10-21 17:05:16 -07:00
Leonardo de Moura
65e5247944 chore: mark dead code 2019-10-21 10:25:38 -07:00
Leonardo de Moura
eb9f361232 chore: remove dead code 2019-10-21 10:14:19 -07:00
Leonardo de Moura
39e8499c7b fix: new offset at param_borrow 2019-10-11 16:27:29 -07:00
Leonardo de Moura
02ab51505c fix: adjust ir_interpreter 
IRType is not a scalar type anymore.
 2019-10-11 15:00:26 -07:00
Leonardo de Moura
7adf00666b feat: expose getCtorLayout 2019-10-11 14:34:30 -07:00
Leonardo de Moura
321d9a8a89 chore: update stage0 2019-10-11 10:57:51 -07:00
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