/
IR.lean
88 lines (81 loc) · 2.88 KB
/
IR.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Compiler.IR.Basic
import Lean.Compiler.IR.Format
import Lean.Compiler.IR.CompilerM
import Lean.Compiler.IR.PushProj
import Lean.Compiler.IR.ElimDeadVars
import Lean.Compiler.IR.SimpCase
import Lean.Compiler.IR.ResetReuse
import Lean.Compiler.IR.NormIds
import Lean.Compiler.IR.Checker
import Lean.Compiler.IR.Borrow
import Lean.Compiler.IR.Boxing
import Lean.Compiler.IR.RC
import Lean.Compiler.IR.ExpandResetReuse
import Lean.Compiler.IR.UnboxResult
import Lean.Compiler.IR.ElimDeadBranches
import Lean.Compiler.IR.EmitC
import Lean.Compiler.IR.CtorLayout
import Lean.Compiler.IR.Sorry
namespace Lean.IR
register_builtin_option compiler.reuse : Bool := {
defValue := true
descr := "heuristically insert reset/reuse instruction pairs"
}
private def compileAux (decls : Array Decl) : CompilerM Unit := do
logDecls `init decls
checkDecls decls
let mut decls ← elimDeadBranches decls
logDecls `elim_dead_branches decls
decls := decls.map Decl.pushProj
logDecls `push_proj decls
if compiler.reuse.get (← read) then
decls := decls.map Decl.insertResetReuse
logDecls `reset_reuse decls
decls := decls.map Decl.elimDead
logDecls `elim_dead decls
decls := decls.map Decl.simpCase
logDecls `simp_case decls
decls := decls.map Decl.normalizeIds
decls ← inferBorrow decls
logDecls `borrow decls
decls ← explicitBoxing decls
logDecls `boxing decls
decls ← explicitRC decls
logDecls `rc decls
if compiler.reuse.get (← read) then
decls := decls.map Decl.expandResetReuse
logDecls `expand_reset_reuse decls
decls := decls.map Decl.pushProj
logDecls `push_proj decls
decls ← updateSorryDep decls
logDecls `result decls
checkDecls decls
addDecls decls
@[export lean_ir_compile]
def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) :=
match (compileAux decls opts).run { env := env } with
| EStateM.Result.ok _ s => (s.log, Except.ok s.env)
| EStateM.Result.error msg s => (s.log, Except.error msg)
def addBoxedVersionAux (decl : Decl) : CompilerM Unit := do
let env ← getEnv
if !ExplicitBoxing.requiresBoxedVersion env decl then
pure ()
else
let decl := ExplicitBoxing.mkBoxedVersion decl
let decls : Array Decl := #[decl]
let decls ← explicitRC decls
decls.forM fun decl => modifyEnv fun env => addDeclAux env decl
pure ()
-- Remark: we are ignoring the `Log` here. This should be fine.
@[export lean_ir_add_boxed_version]
def addBoxedVersion (env : Environment) (decl : Decl) : Except String Environment :=
match (addBoxedVersionAux decl Options.empty).run { env := env } with
| EStateM.Result.ok _ s => Except.ok s.env
| EStateM.Result.error msg _ => Except.error msg
end Lean.IR