Leonardo de Moura
ba9a10265e
feat(library/init/lean/compiler/ir/emitcpp): implement emitVDecl remaining cases
2019-05-21 14:55:11 -07:00
Leonardo de Moura
88cf3aa5e8
feat(library/init/lean/compiler/ir/emitcpp): emit different kinds of application
2019-05-21 14:30:45 -07:00
Leonardo de Moura
3b5093ebe0
fix(library/compiler/ir): fix ret irrelevant
2019-05-21 13:32:11 -07:00
Leonardo de Moura
5a72368967
feat(library/init/lean/compiler/ir): improve checker
2019-05-21 13:18:56 -07:00
Leonardo de Moura
5aa8647b18
feat(library/init/lean/compiler/ir/emitcpp): more cases
2019-05-21 10:54:58 -07:00
Leonardo de Moura
f3e13c18f8
fix(library/init/lean/compiler/ir): reset
2019-05-21 10:28:50 -07:00
Leonardo de Moura
cc4c26e8ab
feat(library/init/lean/compiler/ir/emitcpp): add some missing cases
2019-05-21 10:21:52 -07:00
Leonardo de Moura
510de7a3a9
feat(library/init/lean/compiler/ir/emitcpp): emitBlock
2019-05-21 09:20:19 -07:00
Leonardo de Moura
636415f645
chore(library/init/lean/compiler/ir/emitcpp): minor
2019-05-21 08:46:20 -07:00
Leonardo de Moura
49ef6e474a
feat(library/init/lean/compiler/ir/emitcpp): better error messages
2019-05-21 08:17:55 -07:00
Leonardo de Moura
f84ea28923
fix(library/init/lean/compiler/ir/emitutil): missing FnBody.case
2019-05-21 08:11:48 -07:00
Leonardo de Moura
4ed803c564
feat(library/init/lean/compiler/ir/emitcpp): emit skeletons
2019-05-20 19:08:21 -07:00
Leonardo de Moura
f852cd774f
feat(library/init/lean/compiler/ir): expose C++ primitives for accessing export and extern attributes
2019-05-20 15:49:03 -07:00
Leonardo de Moura
8c4a9116f6
feat(library/init/lean/compiler/ir/emitcpp): generate header and function decls
2019-05-20 14:47:54 -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
40ecbb7cbc
feat(library/init/control/monad): mark monadInhabited as an instance
2019-05-20 09:33:17 -07:00
Leonardo de Moura
ff74b9f44a
feat(library/init/lean/compiler/ir): add emitutil.lean and emitcpp.lean files
2019-05-20 09:25:16 -07:00
Leonardo de Moura
781dd60b19
fix(library/init/lean/compiler/ir/boxing): filename case
...
It seems OSX is case insensitive since I can compile it on my Mac.
2019-05-20 08:10:33 -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
0f8c5820d3
feat(library/init/lean/compiler/ir/livevars): helper functions for managing the set of live variables
2019-05-19 11:17:05 -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
b6ef6a796c
fix(library/init/lean/compiler/ir/borrow): consider borrow annotation only for references
2019-05-18 11:58:11 -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
d2f6befc15
chore(library/init/lean/compiler/ir): Context ==> LocalContext
2019-05-17 17:29: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
66d4995c56
feat(library/init/lean/compiler/ir/compilerm): add ' versions
2019-05-17 16:37:21 -07:00
Leonardo de Moura
999ba7670d
feat(library/init/lean/compiler/ir): add ExternEntry to Decl.extern constructor
2019-05-17 16:27:58 -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
78401f0eff
chore(library/init/lean/compiler/ir/resetreuse): add comment
2019-05-08 14:17:17 -07:00
Leonardo de Moura
a4e135790b
feat(library/init/lean/compiler/ir/normids): add Decl.uniqueIds predicate
2019-05-08 14:17:17 -07:00
Leonardo de Moura
0de9a92d4c
feat(library/init/lean/compiler/ir/boxing): missing case
2019-05-08 06:04:18 -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
a24a8361f5
feat(library/init/lean/compiler/ir/boxing): add some missing cases
2019-05-07 18:23:08 -07:00
Leonardo de Moura
6d4f7527a2
feat(library/init/lean/compiler/ir/boxing): explicit boxing and unboxing instructions
...
TODO: FnBody.vdecl case
2019-05-07 16:21:29 -07:00
Leonardo de Moura
2cea92b4c8
fix(library/init/lean/compiler/ir/resetreuse): do not use reset and reuse for 0-ary constructors
2019-05-07 16:13:35 -07:00
Leonardo de Moura
800569af5f
chore(library/init/lean/compiler/ir/basic): cleanup
2019-05-07 16:13:22 -07:00
Leonardo de Moura
b717177a1a
chore(library/init/data/array/basic): make sure Array.*foldl and List.*foldl have similar signatures
2019-05-07 15:23:03 -07:00
Leonardo de Moura
5d3c6dbac2
feat(library/init/lean/compiler/ir/basic): add IRType.isScalar
2019-05-07 15:06:55 -07:00
Leonardo de Moura
37c60da70d
refactor(library/init/lean/compiler/ir): cleanup Context
2019-05-07 14:41:08 -07:00
Leonardo de Moura
5b9936f38d
chore(library/init/lean/compiler/ir/resetreuse): add namespace ResetReuse
2019-05-07 12:31:32 -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
fd25827d3e
fix(library/init/lean/compiler/ir/resetreuse): must use livevars instead of freevars
...
The file badreset contains two functions where the new `reset/reuse`
insertion procedure implemented in Lean produces better results than the
one implemented in C++.
cc @kha
2019-05-07 11:09:51 -07:00
Leonardo de Moura
6a496844fd
chore(library/init/lean/compiler/ir/freevars): simplify code using "no shadowing" assumption
2019-05-06 18:38:03 -07:00
Leonardo de Moura
1295bf52bc
feat(library/init/lean/compiler/ir): add Decl.checker for debugging purposes
...
We have also added a new `Context` object, and modified our IR
invariant. Now, we assume there is no variable or join point shadowing.
2019-05-06 18:35:06 -07:00
