Leonardo de Moura
14b611af96
refactor: move buffer.h and *_ref.h files to runtime
2021-08-16 15:39:38 -07:00
Leonardo de Moura
485034bbba
fix: bug at ir.cpp
2020-04-03 17:39:28 -07:00
Leonardo de Moura
60d84660e6
feat: add support for Float in the compiler
2020-04-03 16:39:29 -07:00
Leonardo de Moura
7496296c1e
fix: "filler" fields
2020-02-25 13:49:18 -08: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
81847302a7
feat(library/compiler): replace @[effectful] with @[neverExtract]
2019-10-01 14:06:08 -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
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
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
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
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
Leonardo de Moura
16d423dab6
feat(frontends/lean): switch to [extern] implemented in Lean
...
This commit also changes how we represent attribute parameters as
Syntax objects.
2019-06-26 10:57:33 -07:00
Leonardo de Moura
5148497e8c
feat(library/init/lean/compiler/externattr): add mkExternAttr skeleton
2019-06-25 13:16:11 -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
3b5093ebe0
fix(library/compiler/ir): fix ret irrelevant
2019-05-21 13:32:11 -07:00
Leonardo de Moura
63d2c03403
fix(library/compiler/ir): lambda IR translator
2019-05-21 13:01:43 -07:00
Leonardo de Moura
dbe2bebc06
fix(library/compiler/extern_attribute): register extern constructors in the new IR compiler
2019-05-21 08:09:05 -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
b0c6d1c6a7
fix(library/compiler/ir): assertion violation
2019-05-18 11:33:35 -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
9d7191feca
chore(library/compiler): remove support for fully boxed
2019-05-16 15:48:33 -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
74fb8e627a
feat(library/init/lean/compiler/ir/checker): improve IR checker
2019-05-08 05:47:25 -07:00
Leonardo de Moura
b41d7ec98b
chore(library/compiler/ir): style
2019-05-07 15:20:56 -07:00
Leonardo de Moura
2363fdf544
refactor(library/init/lean/compiler/ir): remove redundant field from FnBody.jdecl
...
The result type of a join point is always equal to the function return
type. Moreover, the extra bookkeeping introduces extra work, and doesn't
really help.
2019-05-07 12:26:11 -07:00
Leonardo de Moura
76a49ec256
chore(library/compiler): add ir::test
2019-05-02 14:40:04 -07:00
Leonardo de Moura
e52e787ad5
fix(library/init/lean/compiler/pushproj): bug and cleanup
2019-05-01 21:01:03 -07:00
Leonardo de Moura
45d09d3044
fix(library/compiler/ir): bug at LLNF -> IR
2019-05-01 17:38:44 -07:00
Leonardo de Moura
ed5e461130
feat(library/init/lean/compiler/ir): add maxVar
2019-05-01 17:38:44 -07:00
Leonardo de Moura
2614b95a8b
refactor(library/init/lean/compiler/ir): use Nat instead of Name for local vars
2019-05-01 17:38:44 -07:00
Leonardo de Moura
0c9fa13763
feat(library/init/lean/compiler): convert LLNF into Lean IR
2019-04-30 17:55:43 -07:00
Leonardo de Moura
952eb0f515
feat(library/compiler): C++ API for Lean IR
2019-04-29 18:23:19 -07:00
Leonardo de Moura
b55b1deaf5
chore(library/compiler): remove ir.cpp
...
There is only one missing transformation: insert explicit reference counting instructions.
We will implement this transformation at `llnf.cpp`. After that, we are
ready to emit C++ code.
2018-11-15 16:53:44 -08:00
Leonardo de Moura
c108fc95cb
feat(library/compiler/ir): basics
2018-11-05 17:04:23 -08:00
Leonardo de Moura
8de7637f75
feat(library/compiler): add to_ir skeleton
2018-11-05 17:04:23 -08:00
