fix(library/init/lean/compiler/ir/borrow): visit join point body
This commit is contained in:
Leonardo de Moura
parent
fe0141918a
commit
3e76e43843
2 changed files with 190 additions and 176 deletions
|
|
@ -10,9 +10,14 @@ import init.lean.compiler.ir.normids
|
|||
|
||||
namespace Lean
|
||||
namespace IR
|
||||
|
||||
namespace Borrow
|
||||
/- We perform borrow inference in a block of mutually recursive functions.
|
||||
Join points are viewed as local functions, and are identified using
|
||||
their local id + the name of the surrounding function.
|
||||
|
||||
We keep a mapping from function and joint points to parameters (`Array Param`).
|
||||
Recall that `Param` contains the field `borrow`.
|
||||
The type `Key` is the the key of this map. -/
|
||||
inductive Key
|
||||
| decl (name : FunId)
|
||||
| jp (name : FunId) (jpid : JoinPointId)
|
||||
|
|
@ -63,9 +68,10 @@ ps.hmap $ λ p, { borrow := p.ty.isObj, .. p }
|
|||
def initBorrowIfNotExported (exported : Bool) (ps : Array Param) : Array Param :=
|
||||
if exported then ps else initBorrow ps
|
||||
|
||||
partial def visitFnBody (exported : Bool) (fnid : FunId) : FnBody → State ParamMap Unit
|
||||
partial def visitFnBody (fnid : FunId) : FnBody → State ParamMap Unit
|
||||
| (FnBody.jdecl j xs v b) := do
|
||||
modify $ λ m, m.insert (Key.jp fnid j) (initBorrowIfNotExported exported xs),
|
||||
modify $ λ m, m.insert (Key.jp fnid j) (initBorrow xs),
|
||||
visitFnBody v,
|
||||
visitFnBody b
|
||||
| e :=
|
||||
unless (e.isTerminal) $ do
|
||||
|
|
@ -77,17 +83,20 @@ decls.mfor $ λ decl, match decl with
|
|||
| Decl.fdecl f xs _ b := do
|
||||
let exported := isExport env f,
|
||||
modify $ λ m, m.insert (Key.decl f) (initBorrowIfNotExported exported xs),
|
||||
visitFnBody exported f b
|
||||
visitFnBody f b
|
||||
| _ := pure ()
|
||||
end InitParamMap
|
||||
|
||||
def mkInitParamMap (env : Environment) (decls : Array Decl) : ParamMap :=
|
||||
(InitParamMap.visitDecls env decls *> get).run' {}
|
||||
|
||||
/- Apply the inferred borrow annotations stored at `ParamMap` to a block of mutually
|
||||
recursive functions. -/
|
||||
namespace ApplyParamMap
|
||||
|
||||
partial def visitFnBody : FnBody → FunId → ParamMap → FnBody
|
||||
| (FnBody.jdecl j xs v b) fnid map :=
|
||||
let v := visitFnBody v fnid map in
|
||||
let b := visitFnBody b fnid map in
|
||||
match map.find (Key.jp fnid j) with
|
||||
| some ys := FnBody.jdecl j ys v b
|
||||
|
|
@ -115,10 +124,17 @@ def applyParamMap (decls : Array Decl) (map : ParamMap) : Array Decl :=
|
|||
ApplyParamMap.visitDecls decls map
|
||||
|
||||
structure BorrowInfCtx :=
|
||||
(env : Environment) (currFn : FunId := default _) (paramSet : IndexSet := {})
|
||||
(env : Environment)
|
||||
(currFn : FunId := default _) -- Function being analyzed.
|
||||
(paramSet : IndexSet := {}) -- Set of all function parameters in scope. This is used to implement the heuristic at `ownArgsUsingParams`
|
||||
|
||||
structure BorrowInfState :=
|
||||
(map : ParamMap) (owned : IndexSet := {}) (modifiedOwned : Bool := false) (modifiedParamMap : Bool := false)
|
||||
/- `map` is a mapping storing the inferred borrow annotations for all functions (and joint points) in a mutually recursive declaration. -/
|
||||
(map : ParamMap)
|
||||
/- Set of variables that must be `owned`. -/
|
||||
(owned : IndexSet := {})
|
||||
(modifiedOwned : Bool := false)
|
||||
(modifiedParamMap : Bool := false)
|
||||
|
||||
abbrev M := ReaderT BorrowInfCtx (State BorrowInfState)
|
||||
|
||||
|
|
@ -143,6 +159,7 @@ def isOwned (x : VarId) : M Bool :=
|
|||
do s ← get,
|
||||
pure $ s.owned.contains x.idx
|
||||
|
||||
/- Updates `map[k]` using the current set of `owned` variables. -/
|
||||
def updateParamMap (k : Key) : M Unit :=
|
||||
do
|
||||
s ← get,
|
||||
|
|
@ -234,10 +251,11 @@ def updateParamSet (ctx : BorrowInfCtx) (ps : Array Param) : BorrowInfCtx :=
|
|||
{ paramSet := ps.foldl (λ s p, s.insert p.x.idx) ctx.paramSet, .. ctx }
|
||||
|
||||
partial def collectFnBody : FnBody → M Unit
|
||||
| (FnBody.jdecl j ys _ b) := do
|
||||
adaptReader (λ ctx, updateParamSet ctx ys) (collectFnBody b),
|
||||
| (FnBody.jdecl j ys v b) := do
|
||||
adaptReader (λ ctx, updateParamSet ctx ys) (collectFnBody v),
|
||||
ctx ← read,
|
||||
updateParamMap (Key.jp ctx.currFn j)
|
||||
updateParamMap (Key.jp ctx.currFn j),
|
||||
collectFnBody b
|
||||
| (FnBody.vdecl x _ v b) := collectFnBody b *> collectExpr x v *> preserveTailCall x v b
|
||||
| (FnBody.jmp j ys) := do
|
||||
ctx ← read,
|
||||
|
|
|
|||
330
src/stage0/init/lean/compiler/ir/borrow.cpp
generated
330
src/stage0/init/lean/compiler/ir/borrow.cpp
generated
|
|
@ -93,9 +93,8 @@ uint8 nat_dec_lt(obj*, obj*);
|
|||
obj* l_Lean_IR_inferBorrow(obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main(obj*, obj*, obj*);
|
||||
uint8 l_Lean_IR_FnBody_isTerminal___main(obj*);
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(uint8, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(obj*, obj*, obj*);
|
||||
obj* l_Array_miterateAux___main___at_Lean_IR_formatParams___spec__2(obj*, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___main___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_HashMapImp_insert___at_Lean_IR_Borrow_InitParamMap_visitFnBody___main___spec__1(obj*, obj*, obj*);
|
||||
obj* l_RBNode_insert___at_Lean_IR_UniqueIds_checkId___spec__2(obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_ownParamsUsingArgs___boxed(obj*, obj*, obj*, obj*);
|
||||
|
|
@ -178,7 +177,6 @@ namespace lean {
|
|||
usize usize_of_nat(obj*);
|
||||
}
|
||||
obj* l_Lean_IR_Borrow_mkInitParamMap___closed__1;
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___boxed(obj*, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_Key_beq___main___boxed(obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_collectDecls___boxed(obj*, obj*, obj*);
|
||||
uint8 l_Lean_IR_Borrow_Key_beq___main(obj*, obj*);
|
||||
|
|
@ -192,7 +190,7 @@ obj* nat_mul(obj*, obj*);
|
|||
obj* l_Array_hmmapAux___main___at_Lean_IR_Borrow_updateParamMap___spec__1___boxed(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_HasToString(obj*);
|
||||
obj* l_Lean_IR_Borrow_collectFnBody___main(obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody(uint8, obj*, obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody(obj*, obj*, obj*);
|
||||
obj* l_HashMapImp_expand___at_Lean_IR_Borrow_InitParamMap_visitFnBody___main___spec__3(obj*, obj*);
|
||||
obj* l_Lean_IR_Borrow_mkInitParamMap(obj*, obj*);
|
||||
obj* l_AssocList_find___main___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main___spec__2(obj*, obj*);
|
||||
|
|
@ -928,62 +926,70 @@ return x_26;
|
|||
}
|
||||
}
|
||||
}
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(uint8 x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
switch (lean::obj_tag(x_2)) {
|
||||
obj* x_3;
|
||||
switch (lean::obj_tag(x_1)) {
|
||||
case 1:
|
||||
{
|
||||
obj* x_6; obj* x_8; obj* x_10; obj* x_14; obj* x_15; obj* x_16;
|
||||
x_6 = lean::cnstr_get(x_2, 0);
|
||||
lean::inc(x_6);
|
||||
x_8 = lean::cnstr_get(x_2, 1);
|
||||
lean::inc(x_8);
|
||||
x_10 = lean::cnstr_get(x_2, 3);
|
||||
lean::inc(x_10);
|
||||
lean::dec(x_2);
|
||||
lean::inc(x_1);
|
||||
x_14 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_14, 0, x_1);
|
||||
lean::cnstr_set(x_14, 1, x_6);
|
||||
x_15 = l_Lean_IR_Borrow_InitParamMap_initBorrowIfNotExported(x_0, x_8);
|
||||
x_16 = l_HashMapImp_insert___at_Lean_IR_Borrow_InitParamMap_visitFnBody___main___spec__1(x_3, x_14, x_15);
|
||||
x_2 = x_10;
|
||||
x_3 = x_16;
|
||||
obj* x_5; obj* x_7; obj* x_9; obj* x_11; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_20; obj* x_21;
|
||||
x_5 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_5);
|
||||
x_7 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_7);
|
||||
x_9 = lean::cnstr_get(x_1, 2);
|
||||
lean::inc(x_9);
|
||||
x_11 = lean::cnstr_get(x_1, 3);
|
||||
lean::inc(x_11);
|
||||
lean::dec(x_1);
|
||||
lean::inc(x_0);
|
||||
x_15 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_15, 0, x_0);
|
||||
lean::cnstr_set(x_15, 1, x_5);
|
||||
x_16 = lean::mk_nat_obj(0ul);
|
||||
x_17 = l_Array_hmmapAux___main___at_Lean_IR_Borrow_InitParamMap_initBorrow___spec__1(x_16, x_7);
|
||||
x_18 = l_HashMapImp_insert___at_Lean_IR_Borrow_InitParamMap_visitFnBody___main___spec__1(x_2, x_15, x_17);
|
||||
lean::inc(x_0);
|
||||
x_20 = l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(x_0, x_9, x_18);
|
||||
x_21 = lean::cnstr_get(x_20, 1);
|
||||
lean::inc(x_21);
|
||||
lean::dec(x_20);
|
||||
x_1 = x_11;
|
||||
x_2 = x_21;
|
||||
goto _start;
|
||||
}
|
||||
default:
|
||||
{
|
||||
obj* x_18;
|
||||
x_18 = lean::box(0);
|
||||
x_4 = x_18;
|
||||
goto lbl_5;
|
||||
obj* x_25;
|
||||
x_25 = lean::box(0);
|
||||
x_3 = x_25;
|
||||
goto lbl_4;
|
||||
}
|
||||
}
|
||||
lbl_5:
|
||||
lbl_4:
|
||||
{
|
||||
uint8 x_20;
|
||||
lean::dec(x_4);
|
||||
x_20 = l_Lean_IR_FnBody_isTerminal___main(x_2);
|
||||
if (x_20 == 0)
|
||||
uint8 x_27;
|
||||
lean::dec(x_3);
|
||||
x_27 = l_Lean_IR_FnBody_isTerminal___main(x_1);
|
||||
if (x_27 == 0)
|
||||
{
|
||||
obj* x_21;
|
||||
x_21 = l_Lean_IR_FnBody_body___main(x_2);
|
||||
lean::dec(x_2);
|
||||
x_2 = x_21;
|
||||
obj* x_28;
|
||||
x_28 = l_Lean_IR_FnBody_body___main(x_1);
|
||||
lean::dec(x_1);
|
||||
x_1 = x_28;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_26; obj* x_27;
|
||||
obj* x_33; obj* x_34;
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
x_26 = lean::box(0);
|
||||
x_27 = lean::alloc_cnstr(0, 2, 0);
|
||||
lean::cnstr_set(x_27, 0, x_26);
|
||||
lean::cnstr_set(x_27, 1, x_3);
|
||||
return x_27;
|
||||
lean::dec(x_0);
|
||||
x_33 = lean::box(0);
|
||||
x_34 = lean::alloc_cnstr(0, 2, 0);
|
||||
lean::cnstr_set(x_34, 0, x_33);
|
||||
lean::cnstr_set(x_34, 1, x_2);
|
||||
return x_34;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -999,30 +1005,12 @@ lean::dec(x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___main___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8 x_4; obj* x_5;
|
||||
x_4 = lean::unbox(x_0);
|
||||
x_5 = l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(x_4, x_1, x_2, x_3);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody(uint8 x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
x_4 = l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(x_0, x_1, x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_Lean_IR_Borrow_InitParamMap_visitFnBody___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8 x_4; obj* x_5;
|
||||
x_4 = lean::unbox(x_0);
|
||||
x_5 = l_Lean_IR_Borrow_InitParamMap_visitFnBody(x_4, x_1, x_2, x_3);
|
||||
return x_5;
|
||||
obj* x_3;
|
||||
x_3 = l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(x_0, x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_Array_mforAux___main___at_Lean_IR_Borrow_InitParamMap_visitDecls___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
|
|
@ -1065,7 +1053,7 @@ x_23 = lean::alloc_cnstr(0, 1, 0);
|
|||
lean::cnstr_set(x_23, 0, x_14);
|
||||
x_24 = l_Lean_IR_Borrow_InitParamMap_initBorrowIfNotExported(x_21, x_16);
|
||||
x_25 = l_HashMapImp_insert___at_Lean_IR_Borrow_InitParamMap_visitFnBody___main___spec__1(x_3, x_23, x_24);
|
||||
x_26 = l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(x_21, x_14, x_18, x_25);
|
||||
x_26 = l_Lean_IR_Borrow_InitParamMap_visitFnBody___main(x_14, x_18, x_25);
|
||||
x_27 = lean::cnstr_get(x_26, 1);
|
||||
lean::inc(x_27);
|
||||
lean::dec(x_26);
|
||||
|
|
@ -1210,7 +1198,7 @@ obj* x_3;
|
|||
switch (lean::obj_tag(x_0)) {
|
||||
case 1:
|
||||
{
|
||||
obj* x_5; obj* x_7; obj* x_9; obj* x_11; obj* x_13; obj* x_15; obj* x_17; obj* x_18;
|
||||
obj* x_5; obj* x_7; obj* x_9; obj* x_11; obj* x_13; obj* x_15; obj* x_17; obj* x_19; obj* x_20;
|
||||
x_5 = lean::cnstr_get(x_0, 0);
|
||||
x_7 = lean::cnstr_get(x_0, 1);
|
||||
x_9 = lean::cnstr_get(x_0, 2);
|
||||
|
|
@ -1230,68 +1218,70 @@ if (lean::is_exclusive(x_0)) {
|
|||
x_13 = lean::box(0);
|
||||
}
|
||||
lean::inc(x_1);
|
||||
x_15 = l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main(x_11, x_1, x_2);
|
||||
x_15 = l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main(x_9, x_1, x_2);
|
||||
lean::inc(x_1);
|
||||
x_17 = l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main(x_11, x_1, x_2);
|
||||
lean::inc(x_5);
|
||||
x_17 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_17, 0, x_1);
|
||||
lean::cnstr_set(x_17, 1, x_5);
|
||||
x_18 = l_HashMapImp_find___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main___spec__1(x_2, x_17);
|
||||
lean::dec(x_17);
|
||||
if (lean::obj_tag(x_18) == 0)
|
||||
x_19 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_19, 0, x_1);
|
||||
lean::cnstr_set(x_19, 1, x_5);
|
||||
x_20 = l_HashMapImp_find___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main___spec__1(x_2, x_19);
|
||||
lean::dec(x_19);
|
||||
if (lean::obj_tag(x_20) == 0)
|
||||
{
|
||||
obj* x_20;
|
||||
obj* x_22;
|
||||
if (lean::is_scalar(x_13)) {
|
||||
x_20 = lean::alloc_cnstr(1, 4, 0);
|
||||
x_22 = lean::alloc_cnstr(1, 4, 0);
|
||||
} else {
|
||||
x_20 = x_13;
|
||||
x_22 = x_13;
|
||||
}
|
||||
lean::cnstr_set(x_20, 0, x_5);
|
||||
lean::cnstr_set(x_20, 1, x_7);
|
||||
lean::cnstr_set(x_20, 2, x_9);
|
||||
lean::cnstr_set(x_20, 3, x_15);
|
||||
return x_20;
|
||||
lean::cnstr_set(x_22, 0, x_5);
|
||||
lean::cnstr_set(x_22, 1, x_7);
|
||||
lean::cnstr_set(x_22, 2, x_15);
|
||||
lean::cnstr_set(x_22, 3, x_17);
|
||||
return x_22;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_22; obj* x_25;
|
||||
obj* x_24; obj* x_27;
|
||||
lean::dec(x_7);
|
||||
x_22 = lean::cnstr_get(x_18, 0);
|
||||
lean::inc(x_22);
|
||||
lean::dec(x_18);
|
||||
x_24 = lean::cnstr_get(x_20, 0);
|
||||
lean::inc(x_24);
|
||||
lean::dec(x_20);
|
||||
if (lean::is_scalar(x_13)) {
|
||||
x_25 = lean::alloc_cnstr(1, 4, 0);
|
||||
x_27 = lean::alloc_cnstr(1, 4, 0);
|
||||
} else {
|
||||
x_25 = x_13;
|
||||
x_27 = x_13;
|
||||
}
|
||||
lean::cnstr_set(x_25, 0, x_5);
|
||||
lean::cnstr_set(x_25, 1, x_22);
|
||||
lean::cnstr_set(x_25, 2, x_9);
|
||||
lean::cnstr_set(x_25, 3, x_15);
|
||||
return x_25;
|
||||
lean::cnstr_set(x_27, 0, x_5);
|
||||
lean::cnstr_set(x_27, 1, x_24);
|
||||
lean::cnstr_set(x_27, 2, x_15);
|
||||
lean::cnstr_set(x_27, 3, x_17);
|
||||
return x_27;
|
||||
}
|
||||
}
|
||||
default:
|
||||
{
|
||||
obj* x_26;
|
||||
x_26 = lean::box(0);
|
||||
x_3 = x_26;
|
||||
obj* x_28;
|
||||
x_28 = lean::box(0);
|
||||
x_3 = x_28;
|
||||
goto lbl_4;
|
||||
}
|
||||
}
|
||||
lbl_4:
|
||||
{
|
||||
uint8 x_28;
|
||||
uint8 x_30;
|
||||
lean::dec(x_3);
|
||||
x_28 = l_Lean_IR_FnBody_isTerminal___main(x_0);
|
||||
if (x_28 == 0)
|
||||
x_30 = l_Lean_IR_FnBody_isTerminal___main(x_0);
|
||||
if (x_30 == 0)
|
||||
{
|
||||
obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33;
|
||||
x_29 = l_Lean_IR_FnBody_body___main(x_0);
|
||||
x_30 = lean::box(12);
|
||||
x_31 = l_Lean_IR_FnBody_setBody___main(x_0, x_30);
|
||||
x_32 = l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main(x_29, x_1, x_2);
|
||||
x_33 = l_Lean_IR_FnBody_setBody___main(x_31, x_32);
|
||||
return x_33;
|
||||
obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35;
|
||||
x_31 = l_Lean_IR_FnBody_body___main(x_0);
|
||||
x_32 = lean::box(12);
|
||||
x_33 = l_Lean_IR_FnBody_setBody___main(x_0, x_32);
|
||||
x_34 = l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___main(x_31, x_1, x_2);
|
||||
x_35 = l_Lean_IR_FnBody_setBody___main(x_33, x_34);
|
||||
return x_35;
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -2767,102 +2757,108 @@ return x_25;
|
|||
}
|
||||
case 1:
|
||||
{
|
||||
obj* x_29; obj* x_31; obj* x_33; obj* x_37; obj* x_39; obj* x_40; obj* x_43; obj* x_45; obj* x_46;
|
||||
obj* x_29; obj* x_31; obj* x_33; obj* x_35; obj* x_39; obj* x_41; obj* x_42; obj* x_45; obj* x_47; obj* x_48; obj* x_49;
|
||||
x_29 = lean::cnstr_get(x_0, 0);
|
||||
lean::inc(x_29);
|
||||
x_31 = lean::cnstr_get(x_0, 1);
|
||||
lean::inc(x_31);
|
||||
x_33 = lean::cnstr_get(x_0, 3);
|
||||
x_33 = lean::cnstr_get(x_0, 2);
|
||||
lean::inc(x_33);
|
||||
x_35 = lean::cnstr_get(x_0, 3);
|
||||
lean::inc(x_35);
|
||||
lean::dec(x_0);
|
||||
lean::inc(x_1);
|
||||
x_37 = l_Lean_IR_Borrow_updateParamSet(x_1, x_31);
|
||||
x_39 = l_Lean_IR_Borrow_updateParamSet(x_1, x_31);
|
||||
lean::dec(x_31);
|
||||
x_39 = l_Lean_IR_Borrow_collectFnBody___main(x_33, x_37, x_2);
|
||||
x_40 = lean::cnstr_get(x_39, 1);
|
||||
lean::inc(x_40);
|
||||
lean::dec(x_39);
|
||||
x_43 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_43);
|
||||
x_45 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_45, 0, x_43);
|
||||
lean::cnstr_set(x_45, 1, x_29);
|
||||
x_46 = l_Lean_IR_Borrow_updateParamMap(x_45, x_1, x_40);
|
||||
lean::dec(x_1);
|
||||
return x_46;
|
||||
x_41 = l_Lean_IR_Borrow_collectFnBody___main(x_33, x_39, x_2);
|
||||
x_42 = lean::cnstr_get(x_41, 1);
|
||||
lean::inc(x_42);
|
||||
lean::dec(x_41);
|
||||
x_45 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_45);
|
||||
x_47 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_47, 0, x_45);
|
||||
lean::cnstr_set(x_47, 1, x_29);
|
||||
x_48 = l_Lean_IR_Borrow_updateParamMap(x_47, x_1, x_42);
|
||||
x_49 = lean::cnstr_get(x_48, 1);
|
||||
lean::inc(x_49);
|
||||
lean::dec(x_48);
|
||||
x_0 = x_35;
|
||||
x_2 = x_49;
|
||||
goto _start;
|
||||
}
|
||||
case 9:
|
||||
{
|
||||
obj* x_48; obj* x_51; obj* x_52;
|
||||
x_48 = lean::cnstr_get(x_0, 2);
|
||||
lean::inc(x_48);
|
||||
obj* x_53; obj* x_56; obj* x_57;
|
||||
x_53 = lean::cnstr_get(x_0, 2);
|
||||
lean::inc(x_53);
|
||||
lean::dec(x_0);
|
||||
x_51 = lean::mk_nat_obj(0ul);
|
||||
x_52 = l_Array_mforAux___main___at_Lean_IR_Borrow_collectFnBody___main___spec__1(x_48, x_51, x_1, x_2);
|
||||
lean::dec(x_48);
|
||||
return x_52;
|
||||
x_56 = lean::mk_nat_obj(0ul);
|
||||
x_57 = l_Array_mforAux___main___at_Lean_IR_Borrow_collectFnBody___main___spec__1(x_53, x_56, x_1, x_2);
|
||||
lean::dec(x_53);
|
||||
return x_57;
|
||||
}
|
||||
case 11:
|
||||
{
|
||||
obj* x_54; obj* x_56; obj* x_59; obj* x_61; obj* x_62; obj* x_64; obj* x_66; obj* x_69; obj* x_70; obj* x_73;
|
||||
x_54 = lean::cnstr_get(x_0, 0);
|
||||
lean::inc(x_54);
|
||||
x_56 = lean::cnstr_get(x_0, 1);
|
||||
lean::inc(x_56);
|
||||
lean::dec(x_0);
|
||||
x_59 = lean::cnstr_get(x_1, 1);
|
||||
obj* x_59; obj* x_61; obj* x_64; obj* x_66; obj* x_67; obj* x_69; obj* x_71; obj* x_74; obj* x_75; obj* x_78;
|
||||
x_59 = lean::cnstr_get(x_0, 0);
|
||||
lean::inc(x_59);
|
||||
x_61 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_61, 0, x_59);
|
||||
lean::cnstr_set(x_61, 1, x_54);
|
||||
x_62 = l_Lean_IR_Borrow_getParamInfo(x_61, x_1, x_2);
|
||||
lean::dec(x_61);
|
||||
x_64 = lean::cnstr_get(x_62, 0);
|
||||
x_61 = lean::cnstr_get(x_0, 1);
|
||||
lean::inc(x_61);
|
||||
lean::dec(x_0);
|
||||
x_64 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_64);
|
||||
x_66 = lean::cnstr_get(x_62, 1);
|
||||
lean::inc(x_66);
|
||||
lean::dec(x_62);
|
||||
x_69 = l_Lean_IR_Borrow_ownArgsUsingParams(x_56, x_64, x_1, x_66);
|
||||
x_70 = lean::cnstr_get(x_69, 1);
|
||||
lean::inc(x_70);
|
||||
lean::dec(x_69);
|
||||
x_73 = l_Lean_IR_Borrow_ownParamsUsingArgs(x_56, x_64, x_1, x_70);
|
||||
x_66 = lean::alloc_cnstr(1, 2, 0);
|
||||
lean::cnstr_set(x_66, 0, x_64);
|
||||
lean::cnstr_set(x_66, 1, x_59);
|
||||
x_67 = l_Lean_IR_Borrow_getParamInfo(x_66, x_1, x_2);
|
||||
lean::dec(x_66);
|
||||
x_69 = lean::cnstr_get(x_67, 0);
|
||||
lean::inc(x_69);
|
||||
x_71 = lean::cnstr_get(x_67, 1);
|
||||
lean::inc(x_71);
|
||||
lean::dec(x_67);
|
||||
x_74 = l_Lean_IR_Borrow_ownArgsUsingParams(x_61, x_69, x_1, x_71);
|
||||
x_75 = lean::cnstr_get(x_74, 1);
|
||||
lean::inc(x_75);
|
||||
lean::dec(x_74);
|
||||
x_78 = l_Lean_IR_Borrow_ownParamsUsingArgs(x_61, x_69, x_1, x_75);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_64);
|
||||
lean::dec(x_56);
|
||||
return x_73;
|
||||
lean::dec(x_69);
|
||||
lean::dec(x_61);
|
||||
return x_78;
|
||||
}
|
||||
default:
|
||||
{
|
||||
obj* x_77;
|
||||
x_77 = lean::box(0);
|
||||
x_3 = x_77;
|
||||
obj* x_82;
|
||||
x_82 = lean::box(0);
|
||||
x_3 = x_82;
|
||||
goto lbl_4;
|
||||
}
|
||||
}
|
||||
lbl_4:
|
||||
{
|
||||
uint8 x_79;
|
||||
uint8 x_84;
|
||||
lean::dec(x_3);
|
||||
x_79 = l_Lean_IR_FnBody_isTerminal___main(x_0);
|
||||
if (x_79 == 0)
|
||||
x_84 = l_Lean_IR_FnBody_isTerminal___main(x_0);
|
||||
if (x_84 == 0)
|
||||
{
|
||||
obj* x_80;
|
||||
x_80 = l_Lean_IR_FnBody_body___main(x_0);
|
||||
obj* x_85;
|
||||
x_85 = l_Lean_IR_FnBody_body___main(x_0);
|
||||
lean::dec(x_0);
|
||||
x_0 = x_80;
|
||||
x_0 = x_85;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_85; obj* x_86;
|
||||
obj* x_90; obj* x_91;
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_0);
|
||||
x_85 = lean::box(0);
|
||||
x_86 = lean::alloc_cnstr(0, 2, 0);
|
||||
lean::cnstr_set(x_86, 0, x_85);
|
||||
lean::cnstr_set(x_86, 1, x_2);
|
||||
return x_86;
|
||||
x_90 = lean::box(0);
|
||||
x_91 = lean::alloc_cnstr(0, 2, 0);
|
||||
lean::cnstr_set(x_91, 0, x_90);
|
||||
lean::cnstr_set(x_91, 1, x_2);
|
||||
return x_91;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue