feat(library/init/lean/compiler/ir): add persistent field to inc/dec
If `persistent == true`, then object is known to be persistent at compilation time. `emitc` omits `inc/dec` operations to persistent objects. The interpreter does not to avoid memory leaks.
This commit is contained in:
Leonardo de Moura
parent
f5062b6d71
commit
7dfec3c724
14 changed files with 2597 additions and 2250 deletions
|
|
@ -226,10 +226,12 @@ inductive FnBody
|
|||
/- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
|
||||
`ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/
|
||||
| sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody)
|
||||
/- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
|
||||
| inc (x : VarId) (n : Nat) (c : Bool) (b : FnBody)
|
||||
/- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
|
||||
| dec (x : VarId) (n : Nat) (c : Bool) (b : FnBody)
|
||||
/- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
|
||||
If `persistent == true` then `x` is statically known to be a persistent object. -/
|
||||
| inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
|
||||
/- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not.
|
||||
If `persistent == true` then `x` is statically known to be a persistent object. -/
|
||||
| dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody)
|
||||
| del (x : VarId) (b : FnBody)
|
||||
| mdata (d : MData) (b : FnBody)
|
||||
| case (tid : Name) (x : VarId) (cs : Array (AltCore FnBody))
|
||||
|
|
@ -272,8 +274,8 @@ def FnBody.body : FnBody → FnBody
|
|||
| FnBody.uset _ _ _ b => b
|
||||
| FnBody.sset _ _ _ _ _ b => b
|
||||
| FnBody.setTag _ _ b => b
|
||||
| FnBody.inc _ _ _ b => b
|
||||
| FnBody.dec _ _ _ b => b
|
||||
| FnBody.inc _ _ _ _ b => b
|
||||
| FnBody.dec _ _ _ _ b => b
|
||||
| FnBody.del _ b => b
|
||||
| FnBody.mdata _ b => b
|
||||
| other => other
|
||||
|
|
@ -285,8 +287,8 @@ def FnBody.setBody : FnBody → FnBody → FnBody
|
|||
| FnBody.uset x i y _, b => FnBody.uset x i y b
|
||||
| FnBody.sset x i o y t _, b => FnBody.sset x i o y t b
|
||||
| FnBody.setTag x i _, b => FnBody.setTag x i b
|
||||
| FnBody.inc x n c _, b => FnBody.inc x n c b
|
||||
| FnBody.dec x n c _, b => FnBody.dec x n c b
|
||||
| FnBody.inc x n c p _, b => FnBody.inc x n c p b
|
||||
| FnBody.dec x n c p _, b => FnBody.dec x n c p b
|
||||
| FnBody.del x _, b => FnBody.del x b
|
||||
| FnBody.mdata d _, b => FnBody.mdata d b
|
||||
| other, b => other
|
||||
|
|
@ -514,8 +516,8 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
|
|||
| ρ, FnBody.sset x₁ i₁ o₁ y₁ t₁ b₁, FnBody.sset x₂ i₂ o₂ y₂ t₂ b₂ =>
|
||||
aeqv ρ x₁ x₂ && i₁ = i₂ && o₁ = o₂ && aeqv ρ y₁ y₂ && t₁ == t₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.setTag x₁ i₁ b₁, FnBody.setTag x₂ i₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.inc x₁ n₁ c₁ b₁, FnBody.inc x₂ n₂ c₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.dec x₁ n₁ c₁ b₁, FnBody.dec x₂ n₂ c₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.inc x₁ n₁ c₁ p₁ b₁, FnBody.inc x₂ n₂ c₂ p₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && p₁ == p₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.dec x₁ n₁ c₁ p₁ b₁, FnBody.dec x₂ n₂ c₂ p₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && p₁ == p₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.del x₁ b₁, FnBody.del x₂ b₂ => aeqv ρ x₁ x₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.mdata m₁ b₁, FnBody.mdata m₂ b₂ => m₁ == m₂ && FnBody.alphaEqv ρ b₁ b₂
|
||||
| ρ, FnBody.case n₁ x₁ alts₁, FnBody.case n₂ x₂ alts₂ => n₁ == n₂ && aeqv ρ x₁ x₂ && Array.isEqv alts₁ alts₂ (fun alt₁ alt₂ =>
|
||||
|
|
|
|||
|
|
@ -108,8 +108,8 @@ partial def checkFnBody : FnBody → M Unit
|
|||
| FnBody.uset x _ y b => checkVar x *> checkVar y *> checkFnBody b
|
||||
| FnBody.sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b
|
||||
| FnBody.setTag x _ b => checkVar x *> checkFnBody b
|
||||
| FnBody.inc x _ _ b => checkVar x *> checkFnBody b
|
||||
| FnBody.dec x _ _ b => checkVar x *> checkFnBody b
|
||||
| FnBody.inc x _ _ _ b => checkVar x *> checkFnBody b
|
||||
| FnBody.dec x _ _ _ b => checkVar x *> checkFnBody b
|
||||
| FnBody.del x b => checkVar x *> checkFnBody b
|
||||
| FnBody.mdata _ b => checkFnBody b
|
||||
| FnBody.jmp j ys => checkJP j *> checkArgs ys
|
||||
|
|
|
|||
|
|
@ -591,8 +591,8 @@ partial def emitBlock (emitBody : FnBody → M Unit) : FnBody → M Unit
|
|||
| FnBody.jdecl j xs v b => emitBlock b
|
||||
| d@(FnBody.vdecl x t v b) =>
|
||||
do ctx ← read; if isTailCallTo ctx.mainFn d then emitTailCall v else emitVDecl x t v *> emitBlock b
|
||||
| FnBody.inc x n c b => emitInc x n c *> emitBlock b
|
||||
| FnBody.dec x n c b => emitDec x n c *> emitBlock b
|
||||
| FnBody.inc x n c p b => unless p (emitInc x n c) *> emitBlock b
|
||||
| FnBody.dec x n c p b => unless p (emitDec x n c) *> emitBlock b
|
||||
| FnBody.del x b => emitDel x *> emitBlock b
|
||||
| FnBody.setTag x i b => emitSetTag x i *> emitBlock b
|
||||
| FnBody.set x i y b => emitSet x i y *> emitBlock b
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ partial def consumed (x : VarId) : FnBody → Bool
|
|||
match v with
|
||||
| Expr.reuse y _ _ _ => x == y || consumed b
|
||||
| _ => consumed b
|
||||
| FnBody.dec y _ _ b => x == y || consumed b
|
||||
| FnBody.dec y _ _ _ b => x == y || consumed b
|
||||
| FnBody.case _ _ alts => alts.all $ fun alt => consumed alt.body
|
||||
| e => !e.isTerminal && consumed e.body
|
||||
|
||||
|
|
@ -65,7 +65,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
|
|||
match b with
|
||||
| (FnBody.vdecl _ _ (Expr.sproj _ _ _) _) => keepInstr b
|
||||
| (FnBody.vdecl _ _ (Expr.uproj _ _) _) => keepInstr b
|
||||
| (FnBody.inc z n c _) =>
|
||||
| (FnBody.inc z n c p _) =>
|
||||
if n == 0 then done () else
|
||||
let b' := bs.get (bs.size - 2);
|
||||
match b' with
|
||||
|
|
@ -81,7 +81,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
|
|||
let bs := bs.pop.pop;
|
||||
let mask := mask.set i (some z);
|
||||
let keep := keep.push b';
|
||||
let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c FnBody.nil);
|
||||
let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil);
|
||||
eraseProjIncForAux bs mask keep
|
||||
else done ()
|
||||
| other => done ()
|
||||
|
|
@ -94,9 +94,9 @@ eraseProjIncForAux y bs (mkArray n none) Array.empty
|
|||
|
||||
/- Replace `reuse x ctor ...` with `ctor ...`, and remoce `dec x` -/
|
||||
partial def reuseToCtor (x : VarId) : FnBody → FnBody
|
||||
| FnBody.dec y n c b =>
|
||||
| FnBody.dec y n c p b =>
|
||||
if x == y then b -- n must be 1 since `x := reset ...`
|
||||
else FnBody.dec y n c (reuseToCtor b)
|
||||
else FnBody.dec y n c p (reuseToCtor b)
|
||||
| FnBody.vdecl z t v b =>
|
||||
match v with
|
||||
| Expr.reuse y c u xs =>
|
||||
|
|
@ -128,10 +128,10 @@ and `b'` is `b` where we removed `dec x` and replaced `reuse x ctor_i ...` with
|
|||
-/
|
||||
def mkSlowPath (x y : VarId) (mask : Mask) (b : FnBody) : FnBody :=
|
||||
let b := reuseToCtor x b;
|
||||
let b := FnBody.dec y 1 true b;
|
||||
let b := FnBody.dec y 1 true false b;
|
||||
mask.foldl
|
||||
(fun b m => match m with
|
||||
| some z => FnBody.inc z 1 true b
|
||||
| some z => FnBody.inc z 1 true false b
|
||||
| none => b)
|
||||
b
|
||||
|
||||
|
|
@ -146,7 +146,7 @@ mask.size.mfold
|
|||
| some _ => pure b -- code took ownership of this field
|
||||
| none => do
|
||||
fld ← mkFresh;
|
||||
pure (FnBody.vdecl fld IRType.object (Expr.proj i y) (FnBody.dec fld 1 true b)))
|
||||
pure (FnBody.vdecl fld IRType.object (Expr.proj i y) (FnBody.dec fld 1 true false b)))
|
||||
b
|
||||
|
||||
def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody :=
|
||||
|
|
@ -197,9 +197,9 @@ partial def removeSelfSet (ctx : Context) : FnBody → FnBody
|
|||
instr.setBody b
|
||||
|
||||
partial def reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody
|
||||
| FnBody.dec z n c b =>
|
||||
| FnBody.dec z n c p b =>
|
||||
if x == z then FnBody.del y b
|
||||
else FnBody.dec z n c (reuseToSet b)
|
||||
else FnBody.dec z n c p (reuseToSet b)
|
||||
| FnBody.vdecl z t v b =>
|
||||
match v with
|
||||
| Expr.reuse w c u zs =>
|
||||
|
|
|
|||
|
|
@ -84,8 +84,8 @@ partial def formatFnBody (indent : Nat := 2) : FnBody → Format
|
|||
| FnBody.uset x i y b => "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.sset x i o y ty b => "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.setTag x cidx b => "setTag " ++ format x ++ " := " ++ format cidx ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.inc x n c b => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.dec x n c b => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.inc x n c _ b => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.dec x n c _ b => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.del x b => "del " ++ format x ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.mdata d b => "mdata " ++ format d ++ ";" ++ Format.line ++ formatFnBody b
|
||||
| FnBody.case tid x cs => "case " ++ format x ++ " of" ++ cs.foldl (fun r c => r ++ Format.line ++ formatAlt formatFnBody indent c) Format.nil
|
||||
|
|
|
|||
|
|
@ -64,8 +64,8 @@ partial def collectFnBody : FnBody → Collector
|
|||
| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b
|
||||
| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b
|
||||
| FnBody.setTag x _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.inc x _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.dec x _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.inc x _ _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.dec x _ _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.del x b => collectVar x >> collectFnBody b
|
||||
| FnBody.mdata _ b => collectFnBody b
|
||||
| FnBody.case _ x alts => collectVar x >> collectAlts collectFnBody alts
|
||||
|
|
@ -159,8 +159,8 @@ partial def collectFnBody : FnBody → Collector
|
|||
| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b
|
||||
| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b
|
||||
| FnBody.setTag x _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.inc x _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.dec x _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.inc x _ _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.dec x _ _ _ b => collectVar x >> collectFnBody b
|
||||
| FnBody.del x b => collectVar x >> collectFnBody b
|
||||
| FnBody.mdata _ b => collectFnBody b
|
||||
| FnBody.case _ x alts => collectVar x >> collectAlts collectFnBody alts
|
||||
|
|
@ -217,8 +217,8 @@ partial def visitFnBody (w : Index) : FnBody → Bool
|
|||
| FnBody.uset x _ y b => visitVar w x || visitVar w y || visitFnBody b
|
||||
| FnBody.sset x _ _ y _ b => visitVar w x || visitVar w y || visitFnBody b
|
||||
| FnBody.setTag x _ b => visitVar w x || visitFnBody b
|
||||
| FnBody.inc x _ _ b => visitVar w x || visitFnBody b
|
||||
| FnBody.dec x _ _ b => visitVar w x || visitFnBody b
|
||||
| FnBody.inc x _ _ _ b => visitVar w x || visitFnBody b
|
||||
| FnBody.dec x _ _ _ b => visitVar w x || visitFnBody b
|
||||
| FnBody.del x b => visitVar w x || visitFnBody b
|
||||
| FnBody.mdata _ b => visitFnBody b
|
||||
| FnBody.jmp j ys => visitJP w j || visitArgs w ys
|
||||
|
|
|
|||
|
|
@ -53,8 +53,8 @@ partial def visitFnBody (w : Index) : FnBody → M Bool
|
|||
| FnBody.uset x _ y b => visitVar w x <||> visitVar w y <||> visitFnBody b
|
||||
| FnBody.sset x _ _ y _ b => visitVar w x <||> visitVar w y <||> visitFnBody b
|
||||
| FnBody.setTag x _ b => visitVar w x <||> visitFnBody b
|
||||
| FnBody.inc x _ _ b => visitVar w x <||> visitFnBody b
|
||||
| FnBody.dec x _ _ b => visitVar w x <||> visitFnBody b
|
||||
| FnBody.inc x _ _ _ b => visitVar w x <||> visitFnBody b
|
||||
| FnBody.dec x _ _ _ b => visitVar w x <||> visitFnBody b
|
||||
| FnBody.del x b => visitVar w x <||> visitFnBody b
|
||||
| FnBody.mdata _ b => visitFnBody b
|
||||
| FnBody.jmp j ys => visitArgs w ys <||> do {
|
||||
|
|
@ -141,8 +141,8 @@ partial def collectFnBody : FnBody → JPLiveVarMap → Collector
|
|||
| FnBody.setTag x _ b, m => collectVar x ∘ collectFnBody b m
|
||||
| FnBody.uset x _ y b, m => collectVar x ∘ collectVar y ∘ collectFnBody b m
|
||||
| FnBody.sset x _ _ y _ b, m => collectVar x ∘ collectVar y ∘ collectFnBody b m
|
||||
| FnBody.inc x _ _ b, m => collectVar x ∘ collectFnBody b m
|
||||
| FnBody.dec x _ _ b, m => collectVar x ∘ collectFnBody b m
|
||||
| FnBody.inc x _ _ _ b, m => collectVar x ∘ collectFnBody b m
|
||||
| FnBody.dec x _ _ _ b, m => collectVar x ∘ collectFnBody b m
|
||||
| FnBody.del x b, m => collectVar x ∘ collectFnBody b m
|
||||
| FnBody.mdata _ b, m => collectFnBody b m
|
||||
| FnBody.ret x, m => collectArg x
|
||||
|
|
|
|||
|
|
@ -106,8 +106,8 @@ partial def normFnBody : FnBody → N FnBody
|
|||
| FnBody.uset x i y b => do x ← normVar x; y ← normVar y; FnBody.uset x i y <$> normFnBody b
|
||||
| FnBody.sset x i o y t b => do x ← normVar x; y ← normVar y; FnBody.sset x i o y t <$> normFnBody b
|
||||
| FnBody.setTag x i b => do x ← normVar x; FnBody.setTag x i <$> normFnBody b
|
||||
| FnBody.inc x n c b => do x ← normVar x; FnBody.inc x n c <$> normFnBody b
|
||||
| FnBody.dec x n c b => do x ← normVar x; FnBody.dec x n c <$> normFnBody b
|
||||
| FnBody.inc x n c p b => do x ← normVar x; FnBody.inc x n c p <$> normFnBody b
|
||||
| FnBody.dec x n c p b => do x ← normVar x; FnBody.dec x n c p <$> normFnBody b
|
||||
| FnBody.del x b => do x ← normVar x; FnBody.del x <$> normFnBody b
|
||||
| FnBody.mdata d b => FnBody.mdata d <$> normFnBody b
|
||||
| FnBody.case tid x alts => do
|
||||
|
|
@ -162,8 +162,8 @@ as.map (mapArg f)
|
|||
| FnBody.setTag x i b => FnBody.setTag (f x) i (mapFnBody b)
|
||||
| FnBody.uset x i y b => FnBody.uset (f x) i (f y) (mapFnBody b)
|
||||
| FnBody.sset x i o y t b => FnBody.sset (f x) i o (f y) t (mapFnBody b)
|
||||
| FnBody.inc x n c b => FnBody.inc (f x) n c (mapFnBody b)
|
||||
| FnBody.dec x n c b => FnBody.dec (f x) n c (mapFnBody b)
|
||||
| FnBody.inc x n c p b => FnBody.inc (f x) n c p (mapFnBody b)
|
||||
| FnBody.dec x n c p b => FnBody.dec (f x) n c p (mapFnBody b)
|
||||
| FnBody.del x b => FnBody.del (f x) (mapFnBody b)
|
||||
| FnBody.mdata d b => FnBody.mdata d (mapFnBody b)
|
||||
| FnBody.case tid x alts => FnBody.case tid (f x) (alts.map (fun alt => alt.modifyBody mapFnBody))
|
||||
|
|
|
|||
|
|
@ -52,13 +52,15 @@ match ctx.jpLiveVarMap.find j with
|
|||
|
||||
def mustConsume (ctx : Context) (x : VarId) : Bool :=
|
||||
let info := getVarInfo ctx x;
|
||||
info.ref && !info.persistent && info.consume
|
||||
info.ref && info.consume
|
||||
|
||||
@[inline] def addInc (x : VarId) (b : FnBody) (n := 1) : FnBody :=
|
||||
if n == 0 then b else FnBody.inc x n true b
|
||||
@[inline] def addInc (ctx : Context) (x : VarId) (b : FnBody) (n := 1) : FnBody :=
|
||||
let info := getVarInfo ctx x;
|
||||
if n == 0 then b else FnBody.inc x n true info.persistent b
|
||||
|
||||
@[inline] def addDec (x : VarId) (b : FnBody) : FnBody :=
|
||||
FnBody.dec x 1 true b
|
||||
@[inline] def addDec (ctx : Context) (x : VarId) (b : FnBody) : FnBody :=
|
||||
let info := getVarInfo ctx x;
|
||||
FnBody.dec x 1 true info.persistent b
|
||||
|
||||
private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : Context :=
|
||||
if c.isRef then ctx
|
||||
|
|
@ -70,7 +72,7 @@ else let m := ctx.varMap;
|
|||
|
||||
private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) (b : FnBody) : FnBody :=
|
||||
caseLiveVars.fold
|
||||
(fun b x => if !altLiveVars.contains x && mustConsume ctx x then addDec x b else b)
|
||||
(fun b x => if !altLiveVars.contains x && mustConsume ctx x then addDec ctx x b else b)
|
||||
b
|
||||
|
||||
/- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/
|
||||
|
|
@ -115,7 +117,7 @@ xs.size.fold
|
|||
| Arg.irrelevant => b
|
||||
| Arg.var x =>
|
||||
let info := getVarInfo ctx x;
|
||||
if !info.ref || info.persistent || !isFirstOcc xs i then b
|
||||
if !info.ref || !isFirstOcc xs i then b
|
||||
else
|
||||
let numConsuptions := getNumConsumptions x xs consumeParamPred; -- number of times the argument is
|
||||
let numIncs :=
|
||||
|
|
@ -127,7 +129,7 @@ xs.size.fold
|
|||
-- dbgTrace ("addInc " ++ toString x ++ " nconsumptions: " ++ toString numConsuptions ++ " incs: " ++ toString numIncs
|
||||
-- ++ " consume: " ++ toString info.consume ++ " live: " ++ toString (liveVarsAfter.contains x)
|
||||
-- ++ " borrowParam : " ++ toString (isBorrowParamAux x xs consumeParamPred)) $ fun _ =>
|
||||
addInc x b numIncs)
|
||||
addInc ctx x b numIncs)
|
||||
b
|
||||
|
||||
private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
|
||||
|
|
@ -145,7 +147,7 @@ xs.size.fold
|
|||
Remark: `x` may occur multiple times in the application (e.g., `f x y x`).
|
||||
This is why we check whether it is the first occurrence. -/
|
||||
if mustConsume ctx x && isFirstOcc xs i && isBorrowParam x xs ps && !bLiveVars.contains x then
|
||||
addDec x b
|
||||
addDec ctx x b
|
||||
else b)
|
||||
b
|
||||
|
||||
|
|
@ -154,9 +156,9 @@ addIncBeforeAux ctx xs (fun i => true) b liveVarsAfter
|
|||
|
||||
/- Add `dec` instructions for parameters that are references, are not alive in `b`, and are not borrow.
|
||||
That is, we must make sure these parameters are consumed. -/
|
||||
private def addDecForDeadParams (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
|
||||
private def addDecForDeadParams (ctx : Context) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
|
||||
ps.foldl
|
||||
(fun b p => if !p.borrow && p.ty.isObj && !bLiveVars.contains p.x then addDec p.x b else b)
|
||||
(fun b p => if !p.borrow && p.ty.isObj && !bLiveVars.contains p.x then addDec ctx p.x b else b)
|
||||
b
|
||||
|
||||
private def isPersistent : Expr → Bool
|
||||
|
|
@ -186,7 +188,7 @@ private def updateVarInfo (ctx : Context) (x : VarId) (t : IRType) (v : Expr) :
|
|||
.. ctx }
|
||||
|
||||
private def addDecIfNeeded (ctx : Context) (x : VarId) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
|
||||
if mustConsume ctx x && !bLiveVars.contains x then addDec x b else b
|
||||
if mustConsume ctx x && !bLiveVars.contains x then addDec ctx x b else b
|
||||
|
||||
private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody × LiveVarSet :=
|
||||
-- dbgTrace ("processVDecl " ++ toString z ++ " " ++ toString (format v)) $ fun _ =>
|
||||
|
|
@ -195,7 +197,7 @@ let b := match v with
|
|||
| (Expr.reuse _ _ _ ys) => addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars
|
||||
| (Expr.proj _ x) =>
|
||||
let b := addDecIfNeeded ctx x b bLiveVars;
|
||||
let b := if (getVarInfo ctx x).consume then addInc z b else b;
|
||||
let b := if (getVarInfo ctx x).consume then addInc ctx z b else b;
|
||||
(FnBody.vdecl z t v b)
|
||||
| (Expr.uproj _ x) => FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
|
||||
| (Expr.sproj _ _ x) => FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars)
|
||||
|
|
@ -226,7 +228,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
|
|||
processVDecl ctx x t v b bLiveVars
|
||||
| FnBody.jdecl j xs v b, ctx =>
|
||||
let (v, vLiveVars) := visitFnBody v (updateVarInfoWithParams ctx xs);
|
||||
let v := addDecForDeadParams xs v vLiveVars;
|
||||
let v := addDecForDeadParams ctx xs v vLiveVars;
|
||||
let ctx := { jpLiveVarMap := updateJPLiveVarMap j xs v ctx.jpLiveVarMap, .. ctx };
|
||||
let (b, bLiveVars) := visitFnBody b ctx;
|
||||
(FnBody.jdecl j xs v b, bLiveVars)
|
||||
|
|
@ -260,7 +262,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
|
|||
match x with
|
||||
| Arg.var x =>
|
||||
let info := getVarInfo ctx x;
|
||||
if info.ref && !info.persistent && !info.consume then (addInc x b, mkLiveVarSet x) else (b, mkLiveVarSet x)
|
||||
if info.ref && !info.consume then (addInc ctx x b, mkLiveVarSet x) else (b, mkLiveVarSet x)
|
||||
| _ => (b, {})
|
||||
| b@(FnBody.jmp j xs), ctx =>
|
||||
let jLiveVars := getJPLiveVars ctx j;
|
||||
|
|
@ -276,7 +278,7 @@ partial def visitDecl (env : Environment) (decls : Array Decl) : Decl → Decl
|
|||
let ctx : Context := { env := env, decls := decls };
|
||||
let ctx := updateVarInfoWithParams ctx xs;
|
||||
let (b, bLiveVars) := visitFnBody b ctx;
|
||||
let b := addDecForDeadParams xs b bLiveVars;
|
||||
let b := addDecForDeadParams ctx xs b bLiveVars;
|
||||
Decl.fdecl f xs t b
|
||||
| other => other
|
||||
|
||||
|
|
|
|||
|
|
@ -1679,96 +1679,100 @@ return x_1;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_42; lean_object* x_43; uint8_t x_44; lean_object* x_45;
|
||||
lean_object* x_42; lean_object* x_43; uint8_t x_44; uint8_t x_45; lean_object* x_46;
|
||||
x_42 = lean_ctor_get(x_1, 0);
|
||||
x_43 = lean_ctor_get(x_1, 1);
|
||||
x_44 = lean_ctor_get_uint8(x_1, sizeof(void*)*3);
|
||||
x_45 = lean_ctor_get_uint8(x_1, sizeof(void*)*3 + 1);
|
||||
lean_inc(x_43);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_1);
|
||||
x_45 = lean_alloc_ctor(6, 3, 1);
|
||||
lean_ctor_set(x_45, 0, x_42);
|
||||
lean_ctor_set(x_45, 1, x_43);
|
||||
lean_ctor_set(x_45, 2, x_2);
|
||||
lean_ctor_set_uint8(x_45, sizeof(void*)*3, x_44);
|
||||
return x_45;
|
||||
x_46 = lean_alloc_ctor(6, 3, 2);
|
||||
lean_ctor_set(x_46, 0, x_42);
|
||||
lean_ctor_set(x_46, 1, x_43);
|
||||
lean_ctor_set(x_46, 2, x_2);
|
||||
lean_ctor_set_uint8(x_46, sizeof(void*)*3, x_44);
|
||||
lean_ctor_set_uint8(x_46, sizeof(void*)*3 + 1, x_45);
|
||||
return x_46;
|
||||
}
|
||||
}
|
||||
case 7:
|
||||
{
|
||||
uint8_t x_46;
|
||||
x_46 = !lean_is_exclusive(x_1);
|
||||
if (x_46 == 0)
|
||||
uint8_t x_47;
|
||||
x_47 = !lean_is_exclusive(x_1);
|
||||
if (x_47 == 0)
|
||||
{
|
||||
lean_object* x_47;
|
||||
x_47 = lean_ctor_get(x_1, 2);
|
||||
lean_dec(x_47);
|
||||
lean_object* x_48;
|
||||
x_48 = lean_ctor_get(x_1, 2);
|
||||
lean_dec(x_48);
|
||||
lean_ctor_set(x_1, 2, x_2);
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_48; lean_object* x_49; uint8_t x_50; lean_object* x_51;
|
||||
x_48 = lean_ctor_get(x_1, 0);
|
||||
x_49 = lean_ctor_get(x_1, 1);
|
||||
x_50 = lean_ctor_get_uint8(x_1, sizeof(void*)*3);
|
||||
lean_object* x_49; lean_object* x_50; uint8_t x_51; uint8_t x_52; lean_object* x_53;
|
||||
x_49 = lean_ctor_get(x_1, 0);
|
||||
x_50 = lean_ctor_get(x_1, 1);
|
||||
x_51 = lean_ctor_get_uint8(x_1, sizeof(void*)*3);
|
||||
x_52 = lean_ctor_get_uint8(x_1, sizeof(void*)*3 + 1);
|
||||
lean_inc(x_50);
|
||||
lean_inc(x_49);
|
||||
lean_inc(x_48);
|
||||
lean_dec(x_1);
|
||||
x_51 = lean_alloc_ctor(7, 3, 1);
|
||||
lean_ctor_set(x_51, 0, x_48);
|
||||
lean_ctor_set(x_51, 1, x_49);
|
||||
lean_ctor_set(x_51, 2, x_2);
|
||||
lean_ctor_set_uint8(x_51, sizeof(void*)*3, x_50);
|
||||
return x_51;
|
||||
x_53 = lean_alloc_ctor(7, 3, 2);
|
||||
lean_ctor_set(x_53, 0, x_49);
|
||||
lean_ctor_set(x_53, 1, x_50);
|
||||
lean_ctor_set(x_53, 2, x_2);
|
||||
lean_ctor_set_uint8(x_53, sizeof(void*)*3, x_51);
|
||||
lean_ctor_set_uint8(x_53, sizeof(void*)*3 + 1, x_52);
|
||||
return x_53;
|
||||
}
|
||||
}
|
||||
case 8:
|
||||
{
|
||||
uint8_t x_52;
|
||||
x_52 = !lean_is_exclusive(x_1);
|
||||
if (x_52 == 0)
|
||||
uint8_t x_54;
|
||||
x_54 = !lean_is_exclusive(x_1);
|
||||
if (x_54 == 0)
|
||||
{
|
||||
lean_object* x_53;
|
||||
x_53 = lean_ctor_get(x_1, 1);
|
||||
lean_dec(x_53);
|
||||
lean_object* x_55;
|
||||
x_55 = lean_ctor_get(x_1, 1);
|
||||
lean_dec(x_55);
|
||||
lean_ctor_set(x_1, 1, x_2);
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_54; lean_object* x_55;
|
||||
x_54 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_54);
|
||||
lean_object* x_56; lean_object* x_57;
|
||||
x_56 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_56);
|
||||
lean_dec(x_1);
|
||||
x_55 = lean_alloc_ctor(8, 2, 0);
|
||||
lean_ctor_set(x_55, 0, x_54);
|
||||
lean_ctor_set(x_55, 1, x_2);
|
||||
return x_55;
|
||||
x_57 = lean_alloc_ctor(8, 2, 0);
|
||||
lean_ctor_set(x_57, 0, x_56);
|
||||
lean_ctor_set(x_57, 1, x_2);
|
||||
return x_57;
|
||||
}
|
||||
}
|
||||
case 9:
|
||||
{
|
||||
uint8_t x_56;
|
||||
x_56 = !lean_is_exclusive(x_1);
|
||||
if (x_56 == 0)
|
||||
uint8_t x_58;
|
||||
x_58 = !lean_is_exclusive(x_1);
|
||||
if (x_58 == 0)
|
||||
{
|
||||
lean_object* x_57;
|
||||
x_57 = lean_ctor_get(x_1, 1);
|
||||
lean_dec(x_57);
|
||||
lean_object* x_59;
|
||||
x_59 = lean_ctor_get(x_1, 1);
|
||||
lean_dec(x_59);
|
||||
lean_ctor_set(x_1, 1, x_2);
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_58; lean_object* x_59;
|
||||
x_58 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_58);
|
||||
lean_object* x_60; lean_object* x_61;
|
||||
x_60 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_60);
|
||||
lean_dec(x_1);
|
||||
x_59 = lean_alloc_ctor(9, 2, 0);
|
||||
lean_ctor_set(x_59, 0, x_58);
|
||||
lean_ctor_set(x_59, 1, x_2);
|
||||
return x_59;
|
||||
x_61 = lean_alloc_ctor(9, 2, 0);
|
||||
lean_ctor_set(x_61, 0, x_60);
|
||||
lean_ctor_set(x_61, 1, x_2);
|
||||
return x_61;
|
||||
}
|
||||
}
|
||||
default:
|
||||
|
|
@ -12264,67 +12268,118 @@ case 6:
|
|||
{
|
||||
if (lean_obj_tag(x_3) == 6)
|
||||
{
|
||||
lean_object* x_103; lean_object* x_104; uint8_t x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; uint8_t x_109; lean_object* x_110; uint8_t x_111;
|
||||
lean_object* x_103; lean_object* x_104; uint8_t x_105; uint8_t x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; uint8_t x_110; uint8_t x_111; lean_object* x_112; uint8_t x_113; uint8_t x_120;
|
||||
x_103 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_103);
|
||||
x_104 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_104);
|
||||
x_105 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_106 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_106);
|
||||
lean_dec(x_2);
|
||||
x_107 = lean_ctor_get(x_3, 0);
|
||||
x_106 = lean_ctor_get_uint8(x_2, sizeof(void*)*3 + 1);
|
||||
x_107 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_107);
|
||||
x_108 = lean_ctor_get(x_3, 1);
|
||||
lean_dec(x_2);
|
||||
x_108 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_108);
|
||||
x_109 = lean_ctor_get_uint8(x_3, sizeof(void*)*3);
|
||||
x_110 = lean_ctor_get(x_3, 2);
|
||||
lean_inc(x_110);
|
||||
x_109 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_109);
|
||||
x_110 = lean_ctor_get_uint8(x_3, sizeof(void*)*3);
|
||||
x_111 = lean_ctor_get_uint8(x_3, sizeof(void*)*3 + 1);
|
||||
x_112 = lean_ctor_get(x_3, 2);
|
||||
lean_inc(x_112);
|
||||
lean_dec(x_3);
|
||||
x_111 = l_Lean_IR_VarId_alphaEqv(x_1, x_103, x_107);
|
||||
lean_dec(x_107);
|
||||
lean_dec(x_103);
|
||||
if (x_111 == 0)
|
||||
{
|
||||
uint8_t x_112;
|
||||
lean_dec(x_110);
|
||||
x_120 = l_Lean_IR_VarId_alphaEqv(x_1, x_103, x_108);
|
||||
lean_dec(x_108);
|
||||
lean_dec(x_106);
|
||||
lean_dec(x_103);
|
||||
if (x_120 == 0)
|
||||
{
|
||||
uint8_t x_121;
|
||||
lean_dec(x_112);
|
||||
lean_dec(x_109);
|
||||
lean_dec(x_107);
|
||||
lean_dec(x_104);
|
||||
lean_dec(x_1);
|
||||
x_112 = 0;
|
||||
return x_112;
|
||||
x_121 = 0;
|
||||
return x_121;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_113;
|
||||
x_113 = lean_nat_dec_eq(x_104, x_108);
|
||||
lean_dec(x_108);
|
||||
uint8_t x_122;
|
||||
x_122 = lean_nat_dec_eq(x_104, x_109);
|
||||
lean_dec(x_109);
|
||||
lean_dec(x_104);
|
||||
if (x_122 == 0)
|
||||
{
|
||||
uint8_t x_123;
|
||||
lean_dec(x_112);
|
||||
lean_dec(x_107);
|
||||
lean_dec(x_1);
|
||||
x_123 = 0;
|
||||
return x_123;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_105 == 0)
|
||||
{
|
||||
if (x_110 == 0)
|
||||
{
|
||||
uint8_t x_124;
|
||||
x_124 = 1;
|
||||
x_113 = x_124;
|
||||
goto block_119;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_125;
|
||||
x_125 = 0;
|
||||
x_113 = x_125;
|
||||
goto block_119;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_110 == 0)
|
||||
{
|
||||
uint8_t x_126;
|
||||
x_126 = 0;
|
||||
x_113 = x_126;
|
||||
goto block_119;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_127;
|
||||
x_127 = 1;
|
||||
x_113 = x_127;
|
||||
goto block_119;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
block_119:
|
||||
{
|
||||
if (x_113 == 0)
|
||||
{
|
||||
uint8_t x_114;
|
||||
lean_dec(x_110);
|
||||
lean_dec(x_106);
|
||||
lean_dec(x_112);
|
||||
lean_dec(x_107);
|
||||
lean_dec(x_1);
|
||||
x_114 = 0;
|
||||
return x_114;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_105 == 0)
|
||||
if (x_106 == 0)
|
||||
{
|
||||
if (x_109 == 0)
|
||||
if (x_111 == 0)
|
||||
{
|
||||
x_2 = x_106;
|
||||
x_3 = x_110;
|
||||
x_2 = x_107;
|
||||
x_3 = x_112;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_116;
|
||||
lean_dec(x_110);
|
||||
lean_dec(x_106);
|
||||
lean_dec(x_112);
|
||||
lean_dec(x_107);
|
||||
lean_dec(x_1);
|
||||
x_116 = 0;
|
||||
return x_116;
|
||||
|
|
@ -12332,19 +12387,19 @@ return x_116;
|
|||
}
|
||||
else
|
||||
{
|
||||
if (x_109 == 0)
|
||||
if (x_111 == 0)
|
||||
{
|
||||
uint8_t x_117;
|
||||
lean_dec(x_110);
|
||||
lean_dec(x_106);
|
||||
lean_dec(x_112);
|
||||
lean_dec(x_107);
|
||||
lean_dec(x_1);
|
||||
x_117 = 0;
|
||||
return x_117;
|
||||
}
|
||||
else
|
||||
{
|
||||
x_2 = x_106;
|
||||
x_3 = x_110;
|
||||
x_2 = x_107;
|
||||
x_3 = x_112;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
|
|
@ -12353,99 +12408,150 @@ goto _start;
|
|||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_119;
|
||||
uint8_t x_128;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_119 = 0;
|
||||
return x_119;
|
||||
x_128 = 0;
|
||||
return x_128;
|
||||
}
|
||||
}
|
||||
case 7:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 7)
|
||||
{
|
||||
lean_object* x_120; lean_object* x_121; uint8_t x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; uint8_t x_126; lean_object* x_127; uint8_t x_128;
|
||||
x_120 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_120);
|
||||
x_121 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_121);
|
||||
x_122 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_123 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_123);
|
||||
lean_object* x_129; lean_object* x_130; uint8_t x_131; uint8_t x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; uint8_t x_136; uint8_t x_137; lean_object* x_138; uint8_t x_139; uint8_t x_146;
|
||||
x_129 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_129);
|
||||
x_130 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_130);
|
||||
x_131 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_132 = lean_ctor_get_uint8(x_2, sizeof(void*)*3 + 1);
|
||||
x_133 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_133);
|
||||
lean_dec(x_2);
|
||||
x_124 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_124);
|
||||
x_125 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_125);
|
||||
x_126 = lean_ctor_get_uint8(x_3, sizeof(void*)*3);
|
||||
x_127 = lean_ctor_get(x_3, 2);
|
||||
lean_inc(x_127);
|
||||
x_134 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_134);
|
||||
x_135 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_135);
|
||||
x_136 = lean_ctor_get_uint8(x_3, sizeof(void*)*3);
|
||||
x_137 = lean_ctor_get_uint8(x_3, sizeof(void*)*3 + 1);
|
||||
x_138 = lean_ctor_get(x_3, 2);
|
||||
lean_inc(x_138);
|
||||
lean_dec(x_3);
|
||||
x_128 = l_Lean_IR_VarId_alphaEqv(x_1, x_120, x_124);
|
||||
lean_dec(x_124);
|
||||
lean_dec(x_120);
|
||||
if (x_128 == 0)
|
||||
x_146 = l_Lean_IR_VarId_alphaEqv(x_1, x_129, x_134);
|
||||
lean_dec(x_134);
|
||||
lean_dec(x_129);
|
||||
if (x_146 == 0)
|
||||
{
|
||||
uint8_t x_129;
|
||||
lean_dec(x_127);
|
||||
lean_dec(x_125);
|
||||
lean_dec(x_123);
|
||||
lean_dec(x_121);
|
||||
uint8_t x_147;
|
||||
lean_dec(x_138);
|
||||
lean_dec(x_135);
|
||||
lean_dec(x_133);
|
||||
lean_dec(x_130);
|
||||
lean_dec(x_1);
|
||||
x_129 = 0;
|
||||
return x_129;
|
||||
x_147 = 0;
|
||||
return x_147;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_130;
|
||||
x_130 = lean_nat_dec_eq(x_121, x_125);
|
||||
lean_dec(x_125);
|
||||
lean_dec(x_121);
|
||||
if (x_130 == 0)
|
||||
uint8_t x_148;
|
||||
x_148 = lean_nat_dec_eq(x_130, x_135);
|
||||
lean_dec(x_135);
|
||||
lean_dec(x_130);
|
||||
if (x_148 == 0)
|
||||
{
|
||||
uint8_t x_131;
|
||||
lean_dec(x_127);
|
||||
lean_dec(x_123);
|
||||
uint8_t x_149;
|
||||
lean_dec(x_138);
|
||||
lean_dec(x_133);
|
||||
lean_dec(x_1);
|
||||
x_131 = 0;
|
||||
return x_131;
|
||||
x_149 = 0;
|
||||
return x_149;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_122 == 0)
|
||||
if (x_131 == 0)
|
||||
{
|
||||
if (x_126 == 0)
|
||||
if (x_136 == 0)
|
||||
{
|
||||
x_2 = x_123;
|
||||
x_3 = x_127;
|
||||
uint8_t x_150;
|
||||
x_150 = 1;
|
||||
x_139 = x_150;
|
||||
goto block_145;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_151;
|
||||
x_151 = 0;
|
||||
x_139 = x_151;
|
||||
goto block_145;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_136 == 0)
|
||||
{
|
||||
uint8_t x_152;
|
||||
x_152 = 0;
|
||||
x_139 = x_152;
|
||||
goto block_145;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_153;
|
||||
x_153 = 1;
|
||||
x_139 = x_153;
|
||||
goto block_145;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
block_145:
|
||||
{
|
||||
if (x_139 == 0)
|
||||
{
|
||||
uint8_t x_140;
|
||||
lean_dec(x_138);
|
||||
lean_dec(x_133);
|
||||
lean_dec(x_1);
|
||||
x_140 = 0;
|
||||
return x_140;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_132 == 0)
|
||||
{
|
||||
if (x_137 == 0)
|
||||
{
|
||||
x_2 = x_133;
|
||||
x_3 = x_138;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_133;
|
||||
lean_dec(x_127);
|
||||
lean_dec(x_123);
|
||||
uint8_t x_142;
|
||||
lean_dec(x_138);
|
||||
lean_dec(x_133);
|
||||
lean_dec(x_1);
|
||||
x_133 = 0;
|
||||
return x_133;
|
||||
x_142 = 0;
|
||||
return x_142;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (x_126 == 0)
|
||||
if (x_137 == 0)
|
||||
{
|
||||
uint8_t x_134;
|
||||
lean_dec(x_127);
|
||||
lean_dec(x_123);
|
||||
uint8_t x_143;
|
||||
lean_dec(x_138);
|
||||
lean_dec(x_133);
|
||||
lean_dec(x_1);
|
||||
x_134 = 0;
|
||||
return x_134;
|
||||
x_143 = 0;
|
||||
return x_143;
|
||||
}
|
||||
else
|
||||
{
|
||||
x_2 = x_123;
|
||||
x_3 = x_127;
|
||||
x_2 = x_133;
|
||||
x_3 = x_138;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
|
|
@ -12454,241 +12560,241 @@ goto _start;
|
|||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_136;
|
||||
uint8_t x_154;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_136 = 0;
|
||||
return x_136;
|
||||
x_154 = 0;
|
||||
return x_154;
|
||||
}
|
||||
}
|
||||
case 8:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 8)
|
||||
{
|
||||
lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; uint8_t x_141;
|
||||
x_137 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_137);
|
||||
x_138 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_138);
|
||||
lean_dec(x_2);
|
||||
x_139 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_139);
|
||||
x_140 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_140);
|
||||
lean_dec(x_3);
|
||||
x_141 = l_Lean_IR_VarId_alphaEqv(x_1, x_137, x_139);
|
||||
lean_dec(x_139);
|
||||
lean_dec(x_137);
|
||||
if (x_141 == 0)
|
||||
{
|
||||
uint8_t x_142;
|
||||
lean_dec(x_140);
|
||||
lean_dec(x_138);
|
||||
lean_dec(x_1);
|
||||
x_142 = 0;
|
||||
return x_142;
|
||||
}
|
||||
else
|
||||
{
|
||||
x_2 = x_138;
|
||||
x_3 = x_140;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_144;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_144 = 0;
|
||||
return x_144;
|
||||
}
|
||||
}
|
||||
case 9:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 9)
|
||||
{
|
||||
lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; uint8_t x_149;
|
||||
x_145 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_145);
|
||||
x_146 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_146);
|
||||
lean_dec(x_2);
|
||||
x_147 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_147);
|
||||
x_148 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_148);
|
||||
lean_dec(x_3);
|
||||
x_149 = l_Lean_KVMap_eqv(x_145, x_147);
|
||||
lean_dec(x_147);
|
||||
lean_dec(x_145);
|
||||
if (x_149 == 0)
|
||||
{
|
||||
uint8_t x_150;
|
||||
lean_dec(x_148);
|
||||
lean_dec(x_146);
|
||||
lean_dec(x_1);
|
||||
x_150 = 0;
|
||||
return x_150;
|
||||
}
|
||||
else
|
||||
{
|
||||
x_2 = x_146;
|
||||
x_3 = x_148;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_152;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_152 = 0;
|
||||
return x_152;
|
||||
}
|
||||
}
|
||||
case 10:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 10)
|
||||
{
|
||||
lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; uint8_t x_159;
|
||||
x_153 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_153);
|
||||
x_154 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_154);
|
||||
x_155 = lean_ctor_get(x_2, 2);
|
||||
lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; uint8_t x_159;
|
||||
x_155 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_155);
|
||||
lean_dec(x_2);
|
||||
x_156 = lean_ctor_get(x_3, 0);
|
||||
x_156 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_156);
|
||||
x_157 = lean_ctor_get(x_3, 1);
|
||||
lean_dec(x_2);
|
||||
x_157 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_157);
|
||||
x_158 = lean_ctor_get(x_3, 2);
|
||||
x_158 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_158);
|
||||
lean_dec(x_3);
|
||||
x_159 = lean_name_dec_eq(x_153, x_156);
|
||||
lean_dec(x_156);
|
||||
lean_dec(x_153);
|
||||
x_159 = l_Lean_IR_VarId_alphaEqv(x_1, x_155, x_157);
|
||||
lean_dec(x_157);
|
||||
lean_dec(x_155);
|
||||
if (x_159 == 0)
|
||||
{
|
||||
uint8_t x_160;
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_157);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_154);
|
||||
lean_dec(x_156);
|
||||
lean_dec(x_1);
|
||||
x_160 = 0;
|
||||
return x_160;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_161;
|
||||
x_161 = l_Lean_IR_VarId_alphaEqv(x_1, x_154, x_157);
|
||||
lean_dec(x_157);
|
||||
lean_dec(x_154);
|
||||
if (x_161 == 0)
|
||||
x_2 = x_156;
|
||||
x_3 = x_158;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_162;
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_162 = 0;
|
||||
return x_162;
|
||||
}
|
||||
}
|
||||
case 9:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 9)
|
||||
{
|
||||
lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; uint8_t x_167;
|
||||
x_163 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_163);
|
||||
x_164 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_164);
|
||||
lean_dec(x_2);
|
||||
x_165 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_165);
|
||||
x_166 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_166);
|
||||
lean_dec(x_3);
|
||||
x_167 = l_Lean_KVMap_eqv(x_163, x_165);
|
||||
lean_dec(x_165);
|
||||
lean_dec(x_163);
|
||||
if (x_167 == 0)
|
||||
{
|
||||
uint8_t x_168;
|
||||
lean_dec(x_166);
|
||||
lean_dec(x_164);
|
||||
lean_dec(x_1);
|
||||
x_168 = 0;
|
||||
return x_168;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_163;
|
||||
x_163 = l_Array_isEqv___at_Lean_IR_FnBody_alphaEqv___main___spec__1(x_1, x_155, x_158);
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_155);
|
||||
return x_163;
|
||||
}
|
||||
x_2 = x_164;
|
||||
x_3 = x_166;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_164;
|
||||
uint8_t x_170;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_164 = 0;
|
||||
return x_164;
|
||||
x_170 = 0;
|
||||
return x_170;
|
||||
}
|
||||
}
|
||||
case 10:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 10)
|
||||
{
|
||||
lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; uint8_t x_177;
|
||||
x_171 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_171);
|
||||
x_172 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_172);
|
||||
x_173 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_173);
|
||||
lean_dec(x_2);
|
||||
x_174 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_174);
|
||||
x_175 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_175);
|
||||
x_176 = lean_ctor_get(x_3, 2);
|
||||
lean_inc(x_176);
|
||||
lean_dec(x_3);
|
||||
x_177 = lean_name_dec_eq(x_171, x_174);
|
||||
lean_dec(x_174);
|
||||
lean_dec(x_171);
|
||||
if (x_177 == 0)
|
||||
{
|
||||
uint8_t x_178;
|
||||
lean_dec(x_176);
|
||||
lean_dec(x_175);
|
||||
lean_dec(x_173);
|
||||
lean_dec(x_172);
|
||||
lean_dec(x_1);
|
||||
x_178 = 0;
|
||||
return x_178;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_179;
|
||||
x_179 = l_Lean_IR_VarId_alphaEqv(x_1, x_172, x_175);
|
||||
lean_dec(x_175);
|
||||
lean_dec(x_172);
|
||||
if (x_179 == 0)
|
||||
{
|
||||
uint8_t x_180;
|
||||
lean_dec(x_176);
|
||||
lean_dec(x_173);
|
||||
lean_dec(x_1);
|
||||
x_180 = 0;
|
||||
return x_180;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_181;
|
||||
x_181 = l_Array_isEqv___at_Lean_IR_FnBody_alphaEqv___main___spec__1(x_1, x_173, x_176);
|
||||
lean_dec(x_176);
|
||||
lean_dec(x_173);
|
||||
return x_181;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_182;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_182 = 0;
|
||||
return x_182;
|
||||
}
|
||||
}
|
||||
case 11:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 11)
|
||||
{
|
||||
lean_object* x_165; lean_object* x_166; uint8_t x_167;
|
||||
x_165 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_165);
|
||||
lean_object* x_183; lean_object* x_184; uint8_t x_185;
|
||||
x_183 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_183);
|
||||
lean_dec(x_2);
|
||||
x_166 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_166);
|
||||
x_184 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_184);
|
||||
lean_dec(x_3);
|
||||
x_167 = l_Lean_IR_Arg_alphaEqv(x_1, x_165, x_166);
|
||||
lean_dec(x_166);
|
||||
lean_dec(x_165);
|
||||
x_185 = l_Lean_IR_Arg_alphaEqv(x_1, x_183, x_184);
|
||||
lean_dec(x_184);
|
||||
lean_dec(x_183);
|
||||
lean_dec(x_1);
|
||||
return x_167;
|
||||
return x_185;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_168;
|
||||
uint8_t x_186;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_168 = 0;
|
||||
return x_168;
|
||||
x_186 = 0;
|
||||
return x_186;
|
||||
}
|
||||
}
|
||||
case 12:
|
||||
{
|
||||
if (lean_obj_tag(x_3) == 12)
|
||||
{
|
||||
lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; uint8_t x_173;
|
||||
x_169 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_169);
|
||||
x_170 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_170);
|
||||
lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; uint8_t x_191;
|
||||
x_187 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_187);
|
||||
x_188 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_188);
|
||||
lean_dec(x_2);
|
||||
x_171 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_171);
|
||||
x_172 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_172);
|
||||
x_189 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_189);
|
||||
x_190 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_190);
|
||||
lean_dec(x_3);
|
||||
x_173 = lean_nat_dec_eq(x_169, x_171);
|
||||
lean_dec(x_171);
|
||||
lean_dec(x_169);
|
||||
if (x_173 == 0)
|
||||
x_191 = lean_nat_dec_eq(x_187, x_189);
|
||||
lean_dec(x_189);
|
||||
lean_dec(x_187);
|
||||
if (x_191 == 0)
|
||||
{
|
||||
uint8_t x_174;
|
||||
lean_dec(x_172);
|
||||
lean_dec(x_170);
|
||||
uint8_t x_192;
|
||||
lean_dec(x_190);
|
||||
lean_dec(x_188);
|
||||
lean_dec(x_1);
|
||||
x_174 = 0;
|
||||
return x_174;
|
||||
x_192 = 0;
|
||||
return x_192;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_175;
|
||||
x_175 = l_Array_isEqv___at_Lean_IR_args_alphaEqv___spec__1(x_1, x_170, x_172);
|
||||
lean_dec(x_172);
|
||||
lean_dec(x_170);
|
||||
return x_175;
|
||||
uint8_t x_193;
|
||||
x_193 = l_Array_isEqv___at_Lean_IR_args_alphaEqv___spec__1(x_1, x_188, x_190);
|
||||
lean_dec(x_190);
|
||||
lean_dec(x_188);
|
||||
return x_193;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_176;
|
||||
uint8_t x_194;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_176 = 0;
|
||||
return x_176;
|
||||
x_194 = 0;
|
||||
return x_194;
|
||||
}
|
||||
}
|
||||
default:
|
||||
|
|
@ -12696,16 +12802,16 @@ default:
|
|||
lean_dec(x_1);
|
||||
if (lean_obj_tag(x_3) == 13)
|
||||
{
|
||||
uint8_t x_177;
|
||||
x_177 = 1;
|
||||
return x_177;
|
||||
uint8_t x_195;
|
||||
x_195 = 1;
|
||||
return x_195;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_178;
|
||||
uint8_t x_196;
|
||||
lean_dec(x_3);
|
||||
x_178 = 0;
|
||||
return x_178;
|
||||
x_196 = 0;
|
||||
return x_196;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19592,419 +19592,493 @@ return x_111;
|
|||
}
|
||||
case 6:
|
||||
{
|
||||
lean_object* x_112; lean_object* x_113; uint8_t x_114; lean_object* x_115; lean_object* x_116;
|
||||
x_112 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_112);
|
||||
x_113 = lean_ctor_get(x_2, 1);
|
||||
uint8_t x_112;
|
||||
x_112 = lean_ctor_get_uint8(x_2, sizeof(void*)*3 + 1);
|
||||
if (x_112 == 0)
|
||||
{
|
||||
lean_object* x_113; lean_object* x_114; uint8_t x_115; lean_object* x_116; lean_object* x_117;
|
||||
x_113 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_113);
|
||||
x_114 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_115 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_115);
|
||||
x_114 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_114);
|
||||
x_115 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_116 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_116);
|
||||
lean_dec(x_2);
|
||||
x_116 = l_Lean_IR_EmitC_emitInc(x_112, x_113, x_114, x_3, x_4);
|
||||
if (lean_obj_tag(x_116) == 0)
|
||||
x_117 = l_Lean_IR_EmitC_emitInc(x_113, x_114, x_115, x_3, x_4);
|
||||
if (lean_obj_tag(x_117) == 0)
|
||||
{
|
||||
uint8_t x_117;
|
||||
x_117 = !lean_is_exclusive(x_116);
|
||||
if (x_117 == 0)
|
||||
uint8_t x_118;
|
||||
x_118 = !lean_is_exclusive(x_117);
|
||||
if (x_118 == 0)
|
||||
{
|
||||
lean_object* x_118; lean_object* x_119;
|
||||
x_118 = lean_ctor_get(x_116, 0);
|
||||
lean_dec(x_118);
|
||||
x_119 = lean_box(0);
|
||||
lean_ctor_set(x_116, 0, x_119);
|
||||
x_2 = x_115;
|
||||
x_4 = x_116;
|
||||
lean_object* x_119; lean_object* x_120;
|
||||
x_119 = lean_ctor_get(x_117, 0);
|
||||
lean_dec(x_119);
|
||||
x_120 = lean_box(0);
|
||||
lean_ctor_set(x_117, 0, x_120);
|
||||
x_2 = x_116;
|
||||
x_4 = x_117;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_121; lean_object* x_122; lean_object* x_123;
|
||||
x_121 = lean_ctor_get(x_116, 1);
|
||||
lean_inc(x_121);
|
||||
lean_object* x_122; lean_object* x_123; lean_object* x_124;
|
||||
x_122 = lean_ctor_get(x_117, 1);
|
||||
lean_inc(x_122);
|
||||
lean_dec(x_117);
|
||||
x_123 = lean_box(0);
|
||||
x_124 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_124, 0, x_123);
|
||||
lean_ctor_set(x_124, 1, x_122);
|
||||
x_2 = x_116;
|
||||
x_4 = x_124;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_126;
|
||||
lean_dec(x_116);
|
||||
x_122 = lean_box(0);
|
||||
x_123 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_123, 0, x_122);
|
||||
lean_ctor_set(x_123, 1, x_121);
|
||||
x_2 = x_115;
|
||||
x_4 = x_123;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_125;
|
||||
lean_dec(x_115);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_125 = !lean_is_exclusive(x_116);
|
||||
if (x_125 == 0)
|
||||
x_126 = !lean_is_exclusive(x_117);
|
||||
if (x_126 == 0)
|
||||
{
|
||||
return x_116;
|
||||
return x_117;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_126; lean_object* x_127; lean_object* x_128;
|
||||
x_126 = lean_ctor_get(x_116, 0);
|
||||
x_127 = lean_ctor_get(x_116, 1);
|
||||
lean_object* x_127; lean_object* x_128; lean_object* x_129;
|
||||
x_127 = lean_ctor_get(x_117, 0);
|
||||
x_128 = lean_ctor_get(x_117, 1);
|
||||
lean_inc(x_128);
|
||||
lean_inc(x_127);
|
||||
lean_inc(x_126);
|
||||
lean_dec(x_116);
|
||||
x_128 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_128, 0, x_126);
|
||||
lean_ctor_set(x_128, 1, x_127);
|
||||
return x_128;
|
||||
lean_dec(x_117);
|
||||
x_129 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_129, 0, x_127);
|
||||
lean_ctor_set(x_129, 1, x_128);
|
||||
return x_129;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_130; uint8_t x_131;
|
||||
x_130 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_130);
|
||||
lean_dec(x_2);
|
||||
x_131 = !lean_is_exclusive(x_4);
|
||||
if (x_131 == 0)
|
||||
{
|
||||
lean_object* x_132; lean_object* x_133;
|
||||
x_132 = lean_ctor_get(x_4, 0);
|
||||
lean_dec(x_132);
|
||||
x_133 = lean_box(0);
|
||||
lean_ctor_set(x_4, 0, x_133);
|
||||
x_2 = x_130;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_135; lean_object* x_136; lean_object* x_137;
|
||||
x_135 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_135);
|
||||
lean_dec(x_4);
|
||||
x_136 = lean_box(0);
|
||||
x_137 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_137, 0, x_136);
|
||||
lean_ctor_set(x_137, 1, x_135);
|
||||
x_2 = x_130;
|
||||
x_4 = x_137;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 7:
|
||||
{
|
||||
lean_object* x_129; lean_object* x_130; uint8_t x_131; lean_object* x_132; lean_object* x_133;
|
||||
x_129 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_129);
|
||||
x_130 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_130);
|
||||
x_131 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_132 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_132);
|
||||
uint8_t x_139;
|
||||
x_139 = lean_ctor_get_uint8(x_2, sizeof(void*)*3 + 1);
|
||||
if (x_139 == 0)
|
||||
{
|
||||
lean_object* x_140; lean_object* x_141; uint8_t x_142; lean_object* x_143; lean_object* x_144;
|
||||
x_140 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_140);
|
||||
x_141 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_141);
|
||||
x_142 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_143 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_143);
|
||||
lean_dec(x_2);
|
||||
x_133 = l_Lean_IR_EmitC_emitDec(x_129, x_130, x_131, x_3, x_4);
|
||||
if (lean_obj_tag(x_133) == 0)
|
||||
x_144 = l_Lean_IR_EmitC_emitDec(x_140, x_141, x_142, x_3, x_4);
|
||||
if (lean_obj_tag(x_144) == 0)
|
||||
{
|
||||
uint8_t x_134;
|
||||
x_134 = !lean_is_exclusive(x_133);
|
||||
if (x_134 == 0)
|
||||
uint8_t x_145;
|
||||
x_145 = !lean_is_exclusive(x_144);
|
||||
if (x_145 == 0)
|
||||
{
|
||||
lean_object* x_135; lean_object* x_136;
|
||||
x_135 = lean_ctor_get(x_133, 0);
|
||||
lean_dec(x_135);
|
||||
x_136 = lean_box(0);
|
||||
lean_ctor_set(x_133, 0, x_136);
|
||||
x_2 = x_132;
|
||||
x_4 = x_133;
|
||||
lean_object* x_146; lean_object* x_147;
|
||||
x_146 = lean_ctor_get(x_144, 0);
|
||||
lean_dec(x_146);
|
||||
x_147 = lean_box(0);
|
||||
lean_ctor_set(x_144, 0, x_147);
|
||||
x_2 = x_143;
|
||||
x_4 = x_144;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_138; lean_object* x_139; lean_object* x_140;
|
||||
x_138 = lean_ctor_get(x_133, 1);
|
||||
lean_inc(x_138);
|
||||
lean_dec(x_133);
|
||||
x_139 = lean_box(0);
|
||||
x_140 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_140, 0, x_139);
|
||||
lean_ctor_set(x_140, 1, x_138);
|
||||
x_2 = x_132;
|
||||
x_4 = x_140;
|
||||
lean_object* x_149; lean_object* x_150; lean_object* x_151;
|
||||
x_149 = lean_ctor_get(x_144, 1);
|
||||
lean_inc(x_149);
|
||||
lean_dec(x_144);
|
||||
x_150 = lean_box(0);
|
||||
x_151 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_151, 0, x_150);
|
||||
lean_ctor_set(x_151, 1, x_149);
|
||||
x_2 = x_143;
|
||||
x_4 = x_151;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_142;
|
||||
lean_dec(x_132);
|
||||
uint8_t x_153;
|
||||
lean_dec(x_143);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_142 = !lean_is_exclusive(x_133);
|
||||
if (x_142 == 0)
|
||||
x_153 = !lean_is_exclusive(x_144);
|
||||
if (x_153 == 0)
|
||||
{
|
||||
return x_133;
|
||||
return x_144;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_143; lean_object* x_144; lean_object* x_145;
|
||||
x_143 = lean_ctor_get(x_133, 0);
|
||||
x_144 = lean_ctor_get(x_133, 1);
|
||||
lean_inc(x_144);
|
||||
lean_inc(x_143);
|
||||
lean_dec(x_133);
|
||||
x_145 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_145, 0, x_143);
|
||||
lean_ctor_set(x_145, 1, x_144);
|
||||
return x_145;
|
||||
lean_object* x_154; lean_object* x_155; lean_object* x_156;
|
||||
x_154 = lean_ctor_get(x_144, 0);
|
||||
x_155 = lean_ctor_get(x_144, 1);
|
||||
lean_inc(x_155);
|
||||
lean_inc(x_154);
|
||||
lean_dec(x_144);
|
||||
x_156 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_156, 0, x_154);
|
||||
lean_ctor_set(x_156, 1, x_155);
|
||||
return x_156;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_157; uint8_t x_158;
|
||||
x_157 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_157);
|
||||
lean_dec(x_2);
|
||||
x_158 = !lean_is_exclusive(x_4);
|
||||
if (x_158 == 0)
|
||||
{
|
||||
lean_object* x_159; lean_object* x_160;
|
||||
x_159 = lean_ctor_get(x_4, 0);
|
||||
lean_dec(x_159);
|
||||
x_160 = lean_box(0);
|
||||
lean_ctor_set(x_4, 0, x_160);
|
||||
x_2 = x_157;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_162; lean_object* x_163; lean_object* x_164;
|
||||
x_162 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_162);
|
||||
lean_dec(x_4);
|
||||
x_163 = lean_box(0);
|
||||
x_164 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_164, 0, x_163);
|
||||
lean_ctor_set(x_164, 1, x_162);
|
||||
x_2 = x_157;
|
||||
x_4 = x_164;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 8:
|
||||
{
|
||||
lean_object* x_146; lean_object* x_147; lean_object* x_148;
|
||||
x_146 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_146);
|
||||
x_147 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_147);
|
||||
lean_object* x_166; lean_object* x_167; lean_object* x_168;
|
||||
x_166 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_166);
|
||||
x_167 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_167);
|
||||
lean_dec(x_2);
|
||||
x_148 = l_Lean_IR_EmitC_emitDel(x_146, x_3, x_4);
|
||||
if (lean_obj_tag(x_148) == 0)
|
||||
x_168 = l_Lean_IR_EmitC_emitDel(x_166, x_3, x_4);
|
||||
if (lean_obj_tag(x_168) == 0)
|
||||
{
|
||||
uint8_t x_149;
|
||||
x_149 = !lean_is_exclusive(x_148);
|
||||
if (x_149 == 0)
|
||||
uint8_t x_169;
|
||||
x_169 = !lean_is_exclusive(x_168);
|
||||
if (x_169 == 0)
|
||||
{
|
||||
lean_object* x_150; lean_object* x_151;
|
||||
x_150 = lean_ctor_get(x_148, 0);
|
||||
lean_dec(x_150);
|
||||
x_151 = lean_box(0);
|
||||
lean_ctor_set(x_148, 0, x_151);
|
||||
x_2 = x_147;
|
||||
x_4 = x_148;
|
||||
lean_object* x_170; lean_object* x_171;
|
||||
x_170 = lean_ctor_get(x_168, 0);
|
||||
lean_dec(x_170);
|
||||
x_171 = lean_box(0);
|
||||
lean_ctor_set(x_168, 0, x_171);
|
||||
x_2 = x_167;
|
||||
x_4 = x_168;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_153; lean_object* x_154; lean_object* x_155;
|
||||
x_153 = lean_ctor_get(x_148, 1);
|
||||
lean_inc(x_153);
|
||||
lean_dec(x_148);
|
||||
x_154 = lean_box(0);
|
||||
x_155 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_155, 0, x_154);
|
||||
lean_ctor_set(x_155, 1, x_153);
|
||||
x_2 = x_147;
|
||||
x_4 = x_155;
|
||||
lean_object* x_173; lean_object* x_174; lean_object* x_175;
|
||||
x_173 = lean_ctor_get(x_168, 1);
|
||||
lean_inc(x_173);
|
||||
lean_dec(x_168);
|
||||
x_174 = lean_box(0);
|
||||
x_175 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_175, 0, x_174);
|
||||
lean_ctor_set(x_175, 1, x_173);
|
||||
x_2 = x_167;
|
||||
x_4 = x_175;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_157;
|
||||
lean_dec(x_147);
|
||||
uint8_t x_177;
|
||||
lean_dec(x_167);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_157 = !lean_is_exclusive(x_148);
|
||||
if (x_157 == 0)
|
||||
x_177 = !lean_is_exclusive(x_168);
|
||||
if (x_177 == 0)
|
||||
{
|
||||
return x_148;
|
||||
return x_168;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_158; lean_object* x_159; lean_object* x_160;
|
||||
x_158 = lean_ctor_get(x_148, 0);
|
||||
x_159 = lean_ctor_get(x_148, 1);
|
||||
lean_inc(x_159);
|
||||
lean_inc(x_158);
|
||||
lean_dec(x_148);
|
||||
x_160 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_160, 0, x_158);
|
||||
lean_ctor_set(x_160, 1, x_159);
|
||||
return x_160;
|
||||
lean_object* x_178; lean_object* x_179; lean_object* x_180;
|
||||
x_178 = lean_ctor_get(x_168, 0);
|
||||
x_179 = lean_ctor_get(x_168, 1);
|
||||
lean_inc(x_179);
|
||||
lean_inc(x_178);
|
||||
lean_dec(x_168);
|
||||
x_180 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_180, 0, x_178);
|
||||
lean_ctor_set(x_180, 1, x_179);
|
||||
return x_180;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 9:
|
||||
{
|
||||
lean_object* x_161;
|
||||
x_161 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_161);
|
||||
lean_object* x_181;
|
||||
x_181 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_181);
|
||||
lean_dec(x_2);
|
||||
x_2 = x_161;
|
||||
x_2 = x_181;
|
||||
goto _start;
|
||||
}
|
||||
case 10:
|
||||
{
|
||||
lean_object* x_163; lean_object* x_164; lean_object* x_165;
|
||||
x_163 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_163);
|
||||
x_164 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_164);
|
||||
lean_object* x_183; lean_object* x_184; lean_object* x_185;
|
||||
x_183 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_183);
|
||||
x_184 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_184);
|
||||
lean_dec(x_2);
|
||||
x_165 = l_Lean_IR_EmitC_emitCase(x_1, x_163, x_164, x_3, x_4);
|
||||
return x_165;
|
||||
x_185 = l_Lean_IR_EmitC_emitCase(x_1, x_183, x_184, x_3, x_4);
|
||||
return x_185;
|
||||
}
|
||||
case 11:
|
||||
{
|
||||
lean_object* x_166; uint8_t x_167;
|
||||
lean_object* x_186; uint8_t x_187;
|
||||
lean_dec(x_1);
|
||||
x_166 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_166);
|
||||
x_186 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_186);
|
||||
lean_dec(x_2);
|
||||
x_167 = !lean_is_exclusive(x_4);
|
||||
if (x_167 == 0)
|
||||
{
|
||||
lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173;
|
||||
x_168 = lean_ctor_get(x_4, 1);
|
||||
x_169 = lean_ctor_get(x_4, 0);
|
||||
lean_dec(x_169);
|
||||
x_170 = l_Lean_IR_EmitC_emitBlock___main___closed__1;
|
||||
x_171 = lean_string_append(x_168, x_170);
|
||||
x_172 = lean_box(0);
|
||||
lean_ctor_set(x_4, 1, x_171);
|
||||
lean_ctor_set(x_4, 0, x_172);
|
||||
x_173 = l_Lean_IR_EmitC_emitArg(x_166, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
if (lean_obj_tag(x_173) == 0)
|
||||
{
|
||||
uint8_t x_174;
|
||||
x_174 = !lean_is_exclusive(x_173);
|
||||
if (x_174 == 0)
|
||||
{
|
||||
lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180;
|
||||
x_175 = lean_ctor_get(x_173, 1);
|
||||
x_176 = lean_ctor_get(x_173, 0);
|
||||
lean_dec(x_176);
|
||||
x_177 = l_Lean_IR_formatFnBody___main___closed__3;
|
||||
x_178 = lean_string_append(x_175, x_177);
|
||||
x_179 = l_IO_println___rarg___closed__1;
|
||||
x_180 = lean_string_append(x_178, x_179);
|
||||
lean_ctor_set(x_173, 1, x_180);
|
||||
lean_ctor_set(x_173, 0, x_172);
|
||||
return x_173;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186;
|
||||
x_181 = lean_ctor_get(x_173, 1);
|
||||
lean_inc(x_181);
|
||||
lean_dec(x_173);
|
||||
x_182 = l_Lean_IR_formatFnBody___main___closed__3;
|
||||
x_183 = lean_string_append(x_181, x_182);
|
||||
x_184 = l_IO_println___rarg___closed__1;
|
||||
x_185 = lean_string_append(x_183, x_184);
|
||||
x_186 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_186, 0, x_172);
|
||||
lean_ctor_set(x_186, 1, x_185);
|
||||
return x_186;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_187;
|
||||
x_187 = !lean_is_exclusive(x_173);
|
||||
x_187 = !lean_is_exclusive(x_4);
|
||||
if (x_187 == 0)
|
||||
{
|
||||
return x_173;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_188; lean_object* x_189; lean_object* x_190;
|
||||
x_188 = lean_ctor_get(x_173, 0);
|
||||
x_189 = lean_ctor_get(x_173, 1);
|
||||
lean_inc(x_189);
|
||||
lean_inc(x_188);
|
||||
lean_dec(x_173);
|
||||
x_190 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_190, 0, x_188);
|
||||
lean_ctor_set(x_190, 1, x_189);
|
||||
return x_190;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196;
|
||||
x_191 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_191);
|
||||
lean_dec(x_4);
|
||||
x_192 = l_Lean_IR_EmitC_emitBlock___main___closed__1;
|
||||
x_193 = lean_string_append(x_191, x_192);
|
||||
x_194 = lean_box(0);
|
||||
x_195 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_195, 0, x_194);
|
||||
lean_ctor_set(x_195, 1, x_193);
|
||||
x_196 = l_Lean_IR_EmitC_emitArg(x_166, x_3, x_195);
|
||||
lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193;
|
||||
x_188 = lean_ctor_get(x_4, 1);
|
||||
x_189 = lean_ctor_get(x_4, 0);
|
||||
lean_dec(x_189);
|
||||
x_190 = l_Lean_IR_EmitC_emitBlock___main___closed__1;
|
||||
x_191 = lean_string_append(x_188, x_190);
|
||||
x_192 = lean_box(0);
|
||||
lean_ctor_set(x_4, 1, x_191);
|
||||
lean_ctor_set(x_4, 0, x_192);
|
||||
x_193 = l_Lean_IR_EmitC_emitArg(x_186, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
if (lean_obj_tag(x_196) == 0)
|
||||
if (lean_obj_tag(x_193) == 0)
|
||||
{
|
||||
lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203;
|
||||
x_197 = lean_ctor_get(x_196, 1);
|
||||
lean_inc(x_197);
|
||||
if (lean_is_exclusive(x_196)) {
|
||||
lean_ctor_release(x_196, 0);
|
||||
lean_ctor_release(x_196, 1);
|
||||
x_198 = x_196;
|
||||
} else {
|
||||
lean_dec_ref(x_196);
|
||||
x_198 = lean_box(0);
|
||||
}
|
||||
x_199 = l_Lean_IR_formatFnBody___main___closed__3;
|
||||
x_200 = lean_string_append(x_197, x_199);
|
||||
x_201 = l_IO_println___rarg___closed__1;
|
||||
x_202 = lean_string_append(x_200, x_201);
|
||||
if (lean_is_scalar(x_198)) {
|
||||
x_203 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_203 = x_198;
|
||||
}
|
||||
lean_ctor_set(x_203, 0, x_194);
|
||||
lean_ctor_set(x_203, 1, x_202);
|
||||
return x_203;
|
||||
uint8_t x_194;
|
||||
x_194 = !lean_is_exclusive(x_193);
|
||||
if (x_194 == 0)
|
||||
{
|
||||
lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200;
|
||||
x_195 = lean_ctor_get(x_193, 1);
|
||||
x_196 = lean_ctor_get(x_193, 0);
|
||||
lean_dec(x_196);
|
||||
x_197 = l_Lean_IR_formatFnBody___main___closed__3;
|
||||
x_198 = lean_string_append(x_195, x_197);
|
||||
x_199 = l_IO_println___rarg___closed__1;
|
||||
x_200 = lean_string_append(x_198, x_199);
|
||||
lean_ctor_set(x_193, 1, x_200);
|
||||
lean_ctor_set(x_193, 0, x_192);
|
||||
return x_193;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207;
|
||||
x_204 = lean_ctor_get(x_196, 0);
|
||||
lean_inc(x_204);
|
||||
x_205 = lean_ctor_get(x_196, 1);
|
||||
lean_inc(x_205);
|
||||
if (lean_is_exclusive(x_196)) {
|
||||
lean_ctor_release(x_196, 0);
|
||||
lean_ctor_release(x_196, 1);
|
||||
x_206 = x_196;
|
||||
} else {
|
||||
lean_dec_ref(x_196);
|
||||
x_206 = lean_box(0);
|
||||
lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206;
|
||||
x_201 = lean_ctor_get(x_193, 1);
|
||||
lean_inc(x_201);
|
||||
lean_dec(x_193);
|
||||
x_202 = l_Lean_IR_formatFnBody___main___closed__3;
|
||||
x_203 = lean_string_append(x_201, x_202);
|
||||
x_204 = l_IO_println___rarg___closed__1;
|
||||
x_205 = lean_string_append(x_203, x_204);
|
||||
x_206 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_206, 0, x_192);
|
||||
lean_ctor_set(x_206, 1, x_205);
|
||||
return x_206;
|
||||
}
|
||||
if (lean_is_scalar(x_206)) {
|
||||
x_207 = lean_alloc_ctor(1, 2, 0);
|
||||
} else {
|
||||
x_207 = x_206;
|
||||
}
|
||||
lean_ctor_set(x_207, 0, x_204);
|
||||
lean_ctor_set(x_207, 1, x_205);
|
||||
return x_207;
|
||||
else
|
||||
{
|
||||
uint8_t x_207;
|
||||
x_207 = !lean_is_exclusive(x_193);
|
||||
if (x_207 == 0)
|
||||
{
|
||||
return x_193;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_208; lean_object* x_209; lean_object* x_210;
|
||||
x_208 = lean_ctor_get(x_193, 0);
|
||||
x_209 = lean_ctor_get(x_193, 1);
|
||||
lean_inc(x_209);
|
||||
lean_inc(x_208);
|
||||
lean_dec(x_193);
|
||||
x_210 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_210, 0, x_208);
|
||||
lean_ctor_set(x_210, 1, x_209);
|
||||
return x_210;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216;
|
||||
x_211 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_211);
|
||||
lean_dec(x_4);
|
||||
x_212 = l_Lean_IR_EmitC_emitBlock___main___closed__1;
|
||||
x_213 = lean_string_append(x_211, x_212);
|
||||
x_214 = lean_box(0);
|
||||
x_215 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_215, 0, x_214);
|
||||
lean_ctor_set(x_215, 1, x_213);
|
||||
x_216 = l_Lean_IR_EmitC_emitArg(x_186, x_3, x_215);
|
||||
lean_dec(x_3);
|
||||
if (lean_obj_tag(x_216) == 0)
|
||||
{
|
||||
lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223;
|
||||
x_217 = lean_ctor_get(x_216, 1);
|
||||
lean_inc(x_217);
|
||||
if (lean_is_exclusive(x_216)) {
|
||||
lean_ctor_release(x_216, 0);
|
||||
lean_ctor_release(x_216, 1);
|
||||
x_218 = x_216;
|
||||
} else {
|
||||
lean_dec_ref(x_216);
|
||||
x_218 = lean_box(0);
|
||||
}
|
||||
x_219 = l_Lean_IR_formatFnBody___main___closed__3;
|
||||
x_220 = lean_string_append(x_217, x_219);
|
||||
x_221 = l_IO_println___rarg___closed__1;
|
||||
x_222 = lean_string_append(x_220, x_221);
|
||||
if (lean_is_scalar(x_218)) {
|
||||
x_223 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_223 = x_218;
|
||||
}
|
||||
lean_ctor_set(x_223, 0, x_214);
|
||||
lean_ctor_set(x_223, 1, x_222);
|
||||
return x_223;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_224; lean_object* x_225; lean_object* x_226; lean_object* x_227;
|
||||
x_224 = lean_ctor_get(x_216, 0);
|
||||
lean_inc(x_224);
|
||||
x_225 = lean_ctor_get(x_216, 1);
|
||||
lean_inc(x_225);
|
||||
if (lean_is_exclusive(x_216)) {
|
||||
lean_ctor_release(x_216, 0);
|
||||
lean_ctor_release(x_216, 1);
|
||||
x_226 = x_216;
|
||||
} else {
|
||||
lean_dec_ref(x_216);
|
||||
x_226 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_226)) {
|
||||
x_227 = lean_alloc_ctor(1, 2, 0);
|
||||
} else {
|
||||
x_227 = x_226;
|
||||
}
|
||||
lean_ctor_set(x_227, 0, x_224);
|
||||
lean_ctor_set(x_227, 1, x_225);
|
||||
return x_227;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 12:
|
||||
{
|
||||
lean_object* x_208; lean_object* x_209; lean_object* x_210;
|
||||
lean_object* x_228; lean_object* x_229; lean_object* x_230;
|
||||
lean_dec(x_1);
|
||||
x_208 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_208);
|
||||
x_209 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_209);
|
||||
x_228 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_228);
|
||||
x_229 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_229);
|
||||
lean_dec(x_2);
|
||||
x_210 = l_Lean_IR_EmitC_emitJmp(x_208, x_209, x_3, x_4);
|
||||
x_230 = l_Lean_IR_EmitC_emitJmp(x_228, x_229, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_209);
|
||||
return x_210;
|
||||
lean_dec(x_229);
|
||||
return x_230;
|
||||
}
|
||||
default:
|
||||
{
|
||||
uint8_t x_211;
|
||||
uint8_t x_231;
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_211 = !lean_is_exclusive(x_4);
|
||||
if (x_211 == 0)
|
||||
x_231 = !lean_is_exclusive(x_4);
|
||||
if (x_231 == 0)
|
||||
{
|
||||
lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218;
|
||||
x_212 = lean_ctor_get(x_4, 1);
|
||||
x_213 = lean_ctor_get(x_4, 0);
|
||||
lean_dec(x_213);
|
||||
x_214 = l_Lean_IR_EmitC_emitBlock___main___closed__2;
|
||||
x_215 = lean_string_append(x_212, x_214);
|
||||
x_216 = l_IO_println___rarg___closed__1;
|
||||
x_217 = lean_string_append(x_215, x_216);
|
||||
x_218 = lean_box(0);
|
||||
lean_ctor_set(x_4, 1, x_217);
|
||||
lean_ctor_set(x_4, 0, x_218);
|
||||
lean_object* x_232; lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; lean_object* x_238;
|
||||
x_232 = lean_ctor_get(x_4, 1);
|
||||
x_233 = lean_ctor_get(x_4, 0);
|
||||
lean_dec(x_233);
|
||||
x_234 = l_Lean_IR_EmitC_emitBlock___main___closed__2;
|
||||
x_235 = lean_string_append(x_232, x_234);
|
||||
x_236 = l_IO_println___rarg___closed__1;
|
||||
x_237 = lean_string_append(x_235, x_236);
|
||||
x_238 = lean_box(0);
|
||||
lean_ctor_set(x_4, 1, x_237);
|
||||
lean_ctor_set(x_4, 0, x_238);
|
||||
return x_4;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225;
|
||||
x_219 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_219);
|
||||
lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245;
|
||||
x_239 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_239);
|
||||
lean_dec(x_4);
|
||||
x_220 = l_Lean_IR_EmitC_emitBlock___main___closed__2;
|
||||
x_221 = lean_string_append(x_219, x_220);
|
||||
x_222 = l_IO_println___rarg___closed__1;
|
||||
x_223 = lean_string_append(x_221, x_222);
|
||||
x_224 = lean_box(0);
|
||||
x_225 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_225, 0, x_224);
|
||||
lean_ctor_set(x_225, 1, x_223);
|
||||
return x_225;
|
||||
x_240 = l_Lean_IR_EmitC_emitBlock___main___closed__2;
|
||||
x_241 = lean_string_append(x_239, x_240);
|
||||
x_242 = l_IO_println___rarg___closed__1;
|
||||
x_243 = lean_string_append(x_241, x_242);
|
||||
x_244 = lean_box(0);
|
||||
x_245 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_245, 0, x_244);
|
||||
lean_ctor_set(x_245, 1, x_243);
|
||||
return x_245;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -941,207 +941,309 @@ goto block_10;
|
|||
}
|
||||
case 6:
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; uint8_t x_26;
|
||||
x_22 = lean_ctor_get(x_19, 0);
|
||||
lean_inc(x_22);
|
||||
x_23 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_23);
|
||||
x_24 = lean_ctor_get_uint8(x_19, sizeof(void*)*3);
|
||||
lean_dec(x_19);
|
||||
x_25 = lean_unsigned_to_nat(0u);
|
||||
x_26 = lean_nat_dec_eq(x_23, x_25);
|
||||
if (x_26 == 0)
|
||||
uint8_t x_22;
|
||||
x_22 = !lean_is_exclusive(x_19);
|
||||
if (x_22 == 0)
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28; lean_object* x_29;
|
||||
x_27 = lean_nat_sub(x_16, x_17);
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
|
||||
x_23 = lean_ctor_get(x_19, 0);
|
||||
x_24 = lean_ctor_get(x_19, 1);
|
||||
x_25 = lean_ctor_get(x_19, 2);
|
||||
lean_dec(x_25);
|
||||
x_26 = lean_unsigned_to_nat(0u);
|
||||
x_27 = lean_nat_dec_eq(x_24, x_26);
|
||||
if (x_27 == 0)
|
||||
{
|
||||
lean_object* x_28; lean_object* x_29; lean_object* x_30;
|
||||
x_28 = lean_nat_sub(x_16, x_17);
|
||||
lean_dec(x_16);
|
||||
x_28 = l_Lean_IR_Inhabited;
|
||||
x_29 = lean_array_get(x_28, x_2, x_27);
|
||||
lean_dec(x_27);
|
||||
if (lean_obj_tag(x_29) == 0)
|
||||
x_29 = l_Lean_IR_Inhabited;
|
||||
x_30 = lean_array_get(x_29, x_2, x_28);
|
||||
lean_dec(x_28);
|
||||
if (lean_obj_tag(x_30) == 0)
|
||||
{
|
||||
lean_object* x_30;
|
||||
x_30 = lean_ctor_get(x_29, 1);
|
||||
lean_inc(x_30);
|
||||
if (lean_obj_tag(x_30) == 3)
|
||||
{
|
||||
lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34;
|
||||
x_31 = lean_ctor_get(x_29, 0);
|
||||
lean_object* x_31;
|
||||
x_31 = lean_ctor_get(x_30, 1);
|
||||
lean_inc(x_31);
|
||||
if (lean_obj_tag(x_31) == 3)
|
||||
{
|
||||
lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
|
||||
x_32 = lean_ctor_get(x_30, 0);
|
||||
lean_inc(x_32);
|
||||
x_33 = lean_ctor_get(x_30, 1);
|
||||
x_33 = lean_ctor_get(x_31, 0);
|
||||
lean_inc(x_33);
|
||||
lean_dec(x_30);
|
||||
x_34 = lean_nat_dec_eq(x_31, x_22);
|
||||
x_34 = lean_ctor_get(x_31, 1);
|
||||
lean_inc(x_34);
|
||||
lean_dec(x_31);
|
||||
if (x_34 == 0)
|
||||
x_35 = lean_nat_dec_eq(x_32, x_23);
|
||||
lean_dec(x_32);
|
||||
if (x_35 == 0)
|
||||
{
|
||||
lean_object* x_35;
|
||||
lean_object* x_36;
|
||||
lean_dec(x_34);
|
||||
lean_dec(x_33);
|
||||
lean_dec(x_32);
|
||||
lean_dec(x_29);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
x_35 = lean_box(0);
|
||||
x_5 = x_35;
|
||||
goto block_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_36;
|
||||
x_36 = lean_nat_dec_eq(x_1, x_33);
|
||||
lean_dec(x_33);
|
||||
if (x_36 == 0)
|
||||
{
|
||||
lean_object* x_37;
|
||||
lean_dec(x_32);
|
||||
lean_dec(x_29);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
x_37 = lean_box(0);
|
||||
x_5 = x_37;
|
||||
goto block_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; uint8_t x_43;
|
||||
x_38 = lean_array_pop(x_2);
|
||||
x_39 = lean_array_pop(x_38);
|
||||
lean_inc(x_22);
|
||||
x_40 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_40, 0, x_22);
|
||||
x_41 = lean_array_set(x_3, x_32, x_40);
|
||||
lean_dec(x_32);
|
||||
lean_inc(x_29);
|
||||
x_42 = lean_array_push(x_4, x_29);
|
||||
x_43 = !lean_is_exclusive(x_29);
|
||||
if (x_43 == 0)
|
||||
{
|
||||
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48;
|
||||
x_44 = lean_ctor_get(x_29, 2);
|
||||
lean_dec(x_44);
|
||||
x_45 = lean_ctor_get(x_29, 1);
|
||||
lean_dec(x_45);
|
||||
x_46 = lean_ctor_get(x_29, 0);
|
||||
lean_dec(x_46);
|
||||
x_47 = lean_unsigned_to_nat(1u);
|
||||
x_48 = lean_nat_dec_eq(x_23, x_47);
|
||||
if (x_48 == 0)
|
||||
{
|
||||
lean_object* x_49; lean_object* x_50; lean_object* x_51;
|
||||
x_49 = lean_nat_sub(x_23, x_47);
|
||||
lean_dec(x_23);
|
||||
x_50 = lean_box(13);
|
||||
lean_ctor_set_tag(x_29, 6);
|
||||
lean_ctor_set(x_29, 2, x_50);
|
||||
lean_ctor_set(x_29, 1, x_49);
|
||||
lean_ctor_set(x_29, 0, x_22);
|
||||
lean_ctor_set_uint8(x_29, sizeof(void*)*3, x_24);
|
||||
x_51 = lean_array_push(x_42, x_29);
|
||||
x_2 = x_39;
|
||||
x_3 = x_41;
|
||||
x_4 = x_51;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_free_object(x_29);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
x_2 = x_39;
|
||||
x_3 = x_41;
|
||||
x_4 = x_42;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_54; uint8_t x_55;
|
||||
lean_dec(x_29);
|
||||
x_54 = lean_unsigned_to_nat(1u);
|
||||
x_55 = lean_nat_dec_eq(x_23, x_54);
|
||||
if (x_55 == 0)
|
||||
{
|
||||
lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
|
||||
x_56 = lean_nat_sub(x_23, x_54);
|
||||
lean_dec(x_23);
|
||||
x_57 = lean_box(13);
|
||||
x_58 = lean_alloc_ctor(6, 3, 1);
|
||||
lean_ctor_set(x_58, 0, x_22);
|
||||
lean_ctor_set(x_58, 1, x_56);
|
||||
lean_ctor_set(x_58, 2, x_57);
|
||||
lean_ctor_set_uint8(x_58, sizeof(void*)*3, x_24);
|
||||
x_59 = lean_array_push(x_42, x_58);
|
||||
x_2 = x_39;
|
||||
x_3 = x_41;
|
||||
x_4 = x_59;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
x_2 = x_39;
|
||||
x_3 = x_41;
|
||||
x_4 = x_42;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_62;
|
||||
lean_dec(x_30);
|
||||
lean_dec(x_29);
|
||||
lean_free_object(x_19);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
x_62 = lean_box(0);
|
||||
x_5 = x_62;
|
||||
x_36 = lean_box(0);
|
||||
x_5 = x_36;
|
||||
goto block_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_37;
|
||||
x_37 = lean_nat_dec_eq(x_1, x_34);
|
||||
lean_dec(x_34);
|
||||
if (x_37 == 0)
|
||||
{
|
||||
lean_object* x_38;
|
||||
lean_dec(x_33);
|
||||
lean_dec(x_30);
|
||||
lean_free_object(x_19);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
x_38 = lean_box(0);
|
||||
x_5 = x_38;
|
||||
goto block_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45;
|
||||
x_39 = lean_array_pop(x_2);
|
||||
x_40 = lean_array_pop(x_39);
|
||||
lean_inc(x_23);
|
||||
x_41 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_41, 0, x_23);
|
||||
x_42 = lean_array_set(x_3, x_33, x_41);
|
||||
lean_dec(x_33);
|
||||
x_43 = lean_array_push(x_4, x_30);
|
||||
x_44 = lean_unsigned_to_nat(1u);
|
||||
x_45 = lean_nat_dec_eq(x_24, x_44);
|
||||
if (x_45 == 0)
|
||||
{
|
||||
lean_object* x_46; lean_object* x_47; lean_object* x_48;
|
||||
x_46 = lean_nat_sub(x_24, x_44);
|
||||
lean_dec(x_24);
|
||||
x_47 = lean_box(13);
|
||||
lean_ctor_set(x_19, 2, x_47);
|
||||
lean_ctor_set(x_19, 1, x_46);
|
||||
x_48 = lean_array_push(x_43, x_19);
|
||||
x_2 = x_40;
|
||||
x_3 = x_42;
|
||||
x_4 = x_48;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_free_object(x_19);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
x_2 = x_40;
|
||||
x_3 = x_42;
|
||||
x_4 = x_43;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_51;
|
||||
lean_dec(x_31);
|
||||
lean_dec(x_30);
|
||||
lean_free_object(x_19);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
x_51 = lean_box(0);
|
||||
x_5 = x_51;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_52;
|
||||
lean_dec(x_30);
|
||||
lean_free_object(x_19);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
x_52 = lean_box(0);
|
||||
x_5 = x_52;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_53;
|
||||
lean_free_object(x_19);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_16);
|
||||
x_53 = lean_box(0);
|
||||
x_5 = x_53;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_54; lean_object* x_55; uint8_t x_56; uint8_t x_57; lean_object* x_58; uint8_t x_59;
|
||||
x_54 = lean_ctor_get(x_19, 0);
|
||||
x_55 = lean_ctor_get(x_19, 1);
|
||||
x_56 = lean_ctor_get_uint8(x_19, sizeof(void*)*3);
|
||||
x_57 = lean_ctor_get_uint8(x_19, sizeof(void*)*3 + 1);
|
||||
lean_inc(x_55);
|
||||
lean_inc(x_54);
|
||||
lean_dec(x_19);
|
||||
x_58 = lean_unsigned_to_nat(0u);
|
||||
x_59 = lean_nat_dec_eq(x_55, x_58);
|
||||
if (x_59 == 0)
|
||||
{
|
||||
lean_object* x_60; lean_object* x_61; lean_object* x_62;
|
||||
x_60 = lean_nat_sub(x_16, x_17);
|
||||
lean_dec(x_16);
|
||||
x_61 = l_Lean_IR_Inhabited;
|
||||
x_62 = lean_array_get(x_61, x_2, x_60);
|
||||
lean_dec(x_60);
|
||||
if (lean_obj_tag(x_62) == 0)
|
||||
{
|
||||
lean_object* x_63;
|
||||
lean_dec(x_29);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
x_63 = lean_box(0);
|
||||
x_5 = x_63;
|
||||
x_63 = lean_ctor_get(x_62, 1);
|
||||
lean_inc(x_63);
|
||||
if (lean_obj_tag(x_63) == 3)
|
||||
{
|
||||
lean_object* x_64; lean_object* x_65; lean_object* x_66; uint8_t x_67;
|
||||
x_64 = lean_ctor_get(x_62, 0);
|
||||
lean_inc(x_64);
|
||||
x_65 = lean_ctor_get(x_63, 0);
|
||||
lean_inc(x_65);
|
||||
x_66 = lean_ctor_get(x_63, 1);
|
||||
lean_inc(x_66);
|
||||
lean_dec(x_63);
|
||||
x_67 = lean_nat_dec_eq(x_64, x_54);
|
||||
lean_dec(x_64);
|
||||
if (x_67 == 0)
|
||||
{
|
||||
lean_object* x_68;
|
||||
lean_dec(x_66);
|
||||
lean_dec(x_65);
|
||||
lean_dec(x_62);
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_54);
|
||||
x_68 = lean_box(0);
|
||||
x_5 = x_68;
|
||||
goto block_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_69;
|
||||
x_69 = lean_nat_dec_eq(x_1, x_66);
|
||||
lean_dec(x_66);
|
||||
if (x_69 == 0)
|
||||
{
|
||||
lean_object* x_70;
|
||||
lean_dec(x_65);
|
||||
lean_dec(x_62);
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_54);
|
||||
x_70 = lean_box(0);
|
||||
x_5 = x_70;
|
||||
goto block_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; uint8_t x_77;
|
||||
x_71 = lean_array_pop(x_2);
|
||||
x_72 = lean_array_pop(x_71);
|
||||
lean_inc(x_54);
|
||||
x_73 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_73, 0, x_54);
|
||||
x_74 = lean_array_set(x_3, x_65, x_73);
|
||||
lean_dec(x_65);
|
||||
x_75 = lean_array_push(x_4, x_62);
|
||||
x_76 = lean_unsigned_to_nat(1u);
|
||||
x_77 = lean_nat_dec_eq(x_55, x_76);
|
||||
if (x_77 == 0)
|
||||
{
|
||||
lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81;
|
||||
x_78 = lean_nat_sub(x_55, x_76);
|
||||
lean_dec(x_55);
|
||||
x_79 = lean_box(13);
|
||||
x_80 = lean_alloc_ctor(6, 3, 2);
|
||||
lean_ctor_set(x_80, 0, x_54);
|
||||
lean_ctor_set(x_80, 1, x_78);
|
||||
lean_ctor_set(x_80, 2, x_79);
|
||||
lean_ctor_set_uint8(x_80, sizeof(void*)*3, x_56);
|
||||
lean_ctor_set_uint8(x_80, sizeof(void*)*3 + 1, x_57);
|
||||
x_81 = lean_array_push(x_75, x_80);
|
||||
x_2 = x_72;
|
||||
x_3 = x_74;
|
||||
x_4 = x_81;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_54);
|
||||
x_2 = x_72;
|
||||
x_3 = x_74;
|
||||
x_4 = x_75;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_84;
|
||||
lean_dec(x_63);
|
||||
lean_dec(x_62);
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_54);
|
||||
x_84 = lean_box(0);
|
||||
x_5 = x_84;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_64;
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_22);
|
||||
lean_dec(x_16);
|
||||
x_64 = lean_box(0);
|
||||
x_5 = x_64;
|
||||
lean_object* x_85;
|
||||
lean_dec(x_62);
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_54);
|
||||
x_85 = lean_box(0);
|
||||
x_5 = x_85;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_86;
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_54);
|
||||
lean_dec(x_16);
|
||||
x_86 = lean_box(0);
|
||||
x_5 = x_86;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_65;
|
||||
lean_object* x_87;
|
||||
lean_dec(x_19);
|
||||
lean_dec(x_16);
|
||||
x_65 = lean_box(0);
|
||||
x_5 = x_65;
|
||||
x_87 = lean_box(0);
|
||||
x_5 = x_87;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_66;
|
||||
lean_object* x_88;
|
||||
lean_dec(x_16);
|
||||
x_66 = lean_box(0);
|
||||
x_5 = x_66;
|
||||
x_88 = lean_box(0);
|
||||
x_5 = x_88;
|
||||
goto block_10;
|
||||
}
|
||||
block_10:
|
||||
|
|
@ -1439,72 +1541,74 @@ return x_44;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_47; lean_object* x_48; uint8_t x_49; lean_object* x_50; uint8_t x_51;
|
||||
lean_object* x_47; lean_object* x_48; uint8_t x_49; uint8_t x_50; lean_object* x_51; uint8_t x_52;
|
||||
x_47 = lean_ctor_get(x_2, 0);
|
||||
x_48 = lean_ctor_get(x_2, 1);
|
||||
x_49 = lean_ctor_get_uint8(x_2, sizeof(void*)*3);
|
||||
x_50 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_50);
|
||||
x_50 = lean_ctor_get_uint8(x_2, sizeof(void*)*3 + 1);
|
||||
x_51 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_51);
|
||||
lean_inc(x_48);
|
||||
lean_inc(x_47);
|
||||
lean_dec(x_2);
|
||||
x_51 = lean_nat_dec_eq(x_1, x_47);
|
||||
if (x_51 == 0)
|
||||
x_52 = lean_nat_dec_eq(x_1, x_47);
|
||||
if (x_52 == 0)
|
||||
{
|
||||
lean_object* x_52; lean_object* x_53;
|
||||
x_52 = l_Lean_IR_ExpandResetReuse_reuseToCtor___main(x_1, x_50);
|
||||
x_53 = lean_alloc_ctor(7, 3, 1);
|
||||
lean_ctor_set(x_53, 0, x_47);
|
||||
lean_ctor_set(x_53, 1, x_48);
|
||||
lean_ctor_set(x_53, 2, x_52);
|
||||
lean_ctor_set_uint8(x_53, sizeof(void*)*3, x_49);
|
||||
return x_53;
|
||||
lean_object* x_53; lean_object* x_54;
|
||||
x_53 = l_Lean_IR_ExpandResetReuse_reuseToCtor___main(x_1, x_51);
|
||||
x_54 = lean_alloc_ctor(7, 3, 2);
|
||||
lean_ctor_set(x_54, 0, x_47);
|
||||
lean_ctor_set(x_54, 1, x_48);
|
||||
lean_ctor_set(x_54, 2, x_53);
|
||||
lean_ctor_set_uint8(x_54, sizeof(void*)*3, x_49);
|
||||
lean_ctor_set_uint8(x_54, sizeof(void*)*3 + 1, x_50);
|
||||
return x_54;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_48);
|
||||
lean_dec(x_47);
|
||||
return x_50;
|
||||
return x_51;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 10:
|
||||
{
|
||||
uint8_t x_54;
|
||||
x_54 = !lean_is_exclusive(x_2);
|
||||
if (x_54 == 0)
|
||||
uint8_t x_55;
|
||||
x_55 = !lean_is_exclusive(x_2);
|
||||
if (x_55 == 0)
|
||||
{
|
||||
lean_object* x_55; lean_object* x_56; lean_object* x_57;
|
||||
x_55 = lean_ctor_get(x_2, 2);
|
||||
x_56 = lean_unsigned_to_nat(0u);
|
||||
x_57 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToCtor___main___spec__1(x_1, x_56, x_55);
|
||||
lean_ctor_set(x_2, 2, x_57);
|
||||
lean_object* x_56; lean_object* x_57; lean_object* x_58;
|
||||
x_56 = lean_ctor_get(x_2, 2);
|
||||
x_57 = lean_unsigned_to_nat(0u);
|
||||
x_58 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToCtor___main___spec__1(x_1, x_57, x_56);
|
||||
lean_ctor_set(x_2, 2, x_58);
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
|
||||
x_58 = lean_ctor_get(x_2, 0);
|
||||
x_59 = lean_ctor_get(x_2, 1);
|
||||
x_60 = lean_ctor_get(x_2, 2);
|
||||
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64;
|
||||
x_59 = lean_ctor_get(x_2, 0);
|
||||
x_60 = lean_ctor_get(x_2, 1);
|
||||
x_61 = lean_ctor_get(x_2, 2);
|
||||
lean_inc(x_61);
|
||||
lean_inc(x_60);
|
||||
lean_inc(x_59);
|
||||
lean_inc(x_58);
|
||||
lean_dec(x_2);
|
||||
x_61 = lean_unsigned_to_nat(0u);
|
||||
x_62 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToCtor___main___spec__1(x_1, x_61, x_60);
|
||||
x_63 = lean_alloc_ctor(10, 3, 0);
|
||||
lean_ctor_set(x_63, 0, x_58);
|
||||
lean_ctor_set(x_63, 1, x_59);
|
||||
lean_ctor_set(x_63, 2, x_62);
|
||||
return x_63;
|
||||
x_62 = lean_unsigned_to_nat(0u);
|
||||
x_63 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToCtor___main___spec__1(x_1, x_62, x_61);
|
||||
x_64 = lean_alloc_ctor(10, 3, 0);
|
||||
lean_ctor_set(x_64, 0, x_59);
|
||||
lean_ctor_set(x_64, 1, x_60);
|
||||
lean_ctor_set(x_64, 2, x_63);
|
||||
return x_64;
|
||||
}
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_64;
|
||||
x_64 = lean_box(0);
|
||||
x_3 = x_64;
|
||||
lean_object* x_65;
|
||||
x_65 = lean_box(0);
|
||||
x_3 = x_65;
|
||||
goto block_10;
|
||||
}
|
||||
}
|
||||
|
|
@ -1591,18 +1695,20 @@ goto _start;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; uint8_t x_12; lean_object* x_13;
|
||||
lean_object* x_11; uint8_t x_12; uint8_t x_13; lean_object* x_14;
|
||||
x_11 = lean_ctor_get(x_7, 0);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_7);
|
||||
x_12 = 1;
|
||||
x_13 = lean_alloc_ctor(6, 3, 1);
|
||||
lean_ctor_set(x_13, 0, x_11);
|
||||
lean_ctor_set(x_13, 1, x_8);
|
||||
lean_ctor_set(x_13, 2, x_4);
|
||||
lean_ctor_set_uint8(x_13, sizeof(void*)*3, x_12);
|
||||
x_13 = 0;
|
||||
x_14 = lean_alloc_ctor(6, 3, 2);
|
||||
lean_ctor_set(x_14, 0, x_11);
|
||||
lean_ctor_set(x_14, 1, x_8);
|
||||
lean_ctor_set(x_14, 2, x_4);
|
||||
lean_ctor_set_uint8(x_14, sizeof(void*)*3, x_12);
|
||||
lean_ctor_set_uint8(x_14, sizeof(void*)*3 + 1, x_13);
|
||||
x_3 = x_9;
|
||||
x_4 = x_13;
|
||||
x_4 = x_14;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
|
|
@ -1611,18 +1717,20 @@ goto _start;
|
|||
lean_object* l_Lean_IR_ExpandResetReuse_mkSlowPath(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
lean_object* x_5; lean_object* x_6; uint8_t x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
x_5 = l_Lean_IR_ExpandResetReuse_reuseToCtor___main(x_1, x_4);
|
||||
x_6 = lean_unsigned_to_nat(1u);
|
||||
x_7 = 1;
|
||||
x_8 = lean_alloc_ctor(7, 3, 1);
|
||||
lean_ctor_set(x_8, 0, x_2);
|
||||
lean_ctor_set(x_8, 1, x_6);
|
||||
lean_ctor_set(x_8, 2, x_5);
|
||||
lean_ctor_set_uint8(x_8, sizeof(void*)*3, x_7);
|
||||
x_9 = lean_unsigned_to_nat(0u);
|
||||
x_10 = l_Array_miterateAux___main___at_Lean_IR_ExpandResetReuse_mkSlowPath___spec__1(x_3, x_3, x_9, x_8);
|
||||
return x_10;
|
||||
x_8 = 0;
|
||||
x_9 = lean_alloc_ctor(7, 3, 2);
|
||||
lean_ctor_set(x_9, 0, x_2);
|
||||
lean_ctor_set(x_9, 1, x_6);
|
||||
lean_ctor_set(x_9, 2, x_5);
|
||||
lean_ctor_set_uint8(x_9, sizeof(void*)*3, x_7);
|
||||
lean_ctor_set_uint8(x_9, sizeof(void*)*3 + 1, x_8);
|
||||
x_10 = lean_unsigned_to_nat(0u);
|
||||
x_11 = l_Array_miterateAux___main___at_Lean_IR_ExpandResetReuse_mkSlowPath___spec__1(x_3, x_3, x_10, x_9);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_miterateAux___main___at_Lean_IR_ExpandResetReuse_mkSlowPath___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
|
|
@ -1693,7 +1801,7 @@ x_14 = lean_box(0);
|
|||
x_15 = lean_array_get(x_14, x_2, x_13);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23;
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; uint8_t x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24;
|
||||
x_16 = l_Lean_IR_ExpandResetReuse_mkFresh___rarg(x_7);
|
||||
x_17 = lean_ctor_get(x_16, 0);
|
||||
lean_inc(x_17);
|
||||
|
|
@ -1705,20 +1813,22 @@ x_19 = lean_alloc_ctor(3, 2, 0);
|
|||
lean_ctor_set(x_19, 0, x_13);
|
||||
lean_ctor_set(x_19, 1, x_1);
|
||||
x_20 = 1;
|
||||
x_21 = 0;
|
||||
lean_inc(x_17);
|
||||
x_21 = lean_alloc_ctor(7, 3, 1);
|
||||
lean_ctor_set(x_21, 0, x_17);
|
||||
lean_ctor_set(x_21, 1, x_10);
|
||||
lean_ctor_set(x_21, 2, x_5);
|
||||
lean_ctor_set_uint8(x_21, sizeof(void*)*3, x_20);
|
||||
x_22 = 7;
|
||||
x_23 = lean_alloc_ctor(0, 3, 1);
|
||||
lean_ctor_set(x_23, 0, x_17);
|
||||
lean_ctor_set(x_23, 1, x_19);
|
||||
lean_ctor_set(x_23, 2, x_21);
|
||||
lean_ctor_set_uint8(x_23, sizeof(void*)*3, x_22);
|
||||
x_22 = lean_alloc_ctor(7, 3, 2);
|
||||
lean_ctor_set(x_22, 0, x_17);
|
||||
lean_ctor_set(x_22, 1, x_10);
|
||||
lean_ctor_set(x_22, 2, x_5);
|
||||
lean_ctor_set_uint8(x_22, sizeof(void*)*3, x_20);
|
||||
lean_ctor_set_uint8(x_22, sizeof(void*)*3 + 1, x_21);
|
||||
x_23 = 7;
|
||||
x_24 = lean_alloc_ctor(0, 3, 1);
|
||||
lean_ctor_set(x_24, 0, x_17);
|
||||
lean_ctor_set(x_24, 1, x_19);
|
||||
lean_ctor_set(x_24, 2, x_22);
|
||||
lean_ctor_set_uint8(x_24, sizeof(void*)*3, x_23);
|
||||
x_4 = x_11;
|
||||
x_5 = x_23;
|
||||
x_5 = x_24;
|
||||
x_7 = x_18;
|
||||
goto _start;
|
||||
}
|
||||
|
|
@ -1732,13 +1842,13 @@ goto _start;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_26;
|
||||
lean_object* x_27;
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
x_26 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_26, 0, x_5);
|
||||
lean_ctor_set(x_26, 1, x_7);
|
||||
return x_26;
|
||||
x_27 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_27, 0, x_5);
|
||||
lean_ctor_set(x_27, 1, x_7);
|
||||
return x_27;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2756,76 +2866,78 @@ return x_61;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_62; lean_object* x_63; uint8_t x_64; lean_object* x_65; uint8_t x_66;
|
||||
lean_object* x_62; lean_object* x_63; uint8_t x_64; uint8_t x_65; lean_object* x_66; uint8_t x_67;
|
||||
x_62 = lean_ctor_get(x_4, 0);
|
||||
x_63 = lean_ctor_get(x_4, 1);
|
||||
x_64 = lean_ctor_get_uint8(x_4, sizeof(void*)*3);
|
||||
x_65 = lean_ctor_get(x_4, 2);
|
||||
lean_inc(x_65);
|
||||
x_65 = lean_ctor_get_uint8(x_4, sizeof(void*)*3 + 1);
|
||||
x_66 = lean_ctor_get(x_4, 2);
|
||||
lean_inc(x_66);
|
||||
lean_inc(x_63);
|
||||
lean_inc(x_62);
|
||||
lean_dec(x_4);
|
||||
x_66 = lean_nat_dec_eq(x_2, x_62);
|
||||
if (x_66 == 0)
|
||||
x_67 = lean_nat_dec_eq(x_2, x_62);
|
||||
if (x_67 == 0)
|
||||
{
|
||||
lean_object* x_67; lean_object* x_68;
|
||||
x_67 = l_Lean_IR_ExpandResetReuse_reuseToSet___main(x_1, x_2, x_3, x_65);
|
||||
x_68 = lean_alloc_ctor(7, 3, 1);
|
||||
lean_ctor_set(x_68, 0, x_62);
|
||||
lean_ctor_set(x_68, 1, x_63);
|
||||
lean_ctor_set(x_68, 2, x_67);
|
||||
lean_ctor_set_uint8(x_68, sizeof(void*)*3, x_64);
|
||||
return x_68;
|
||||
lean_object* x_68; lean_object* x_69;
|
||||
x_68 = l_Lean_IR_ExpandResetReuse_reuseToSet___main(x_1, x_2, x_3, x_66);
|
||||
x_69 = lean_alloc_ctor(7, 3, 2);
|
||||
lean_ctor_set(x_69, 0, x_62);
|
||||
lean_ctor_set(x_69, 1, x_63);
|
||||
lean_ctor_set(x_69, 2, x_68);
|
||||
lean_ctor_set_uint8(x_69, sizeof(void*)*3, x_64);
|
||||
lean_ctor_set_uint8(x_69, sizeof(void*)*3 + 1, x_65);
|
||||
return x_69;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_69;
|
||||
lean_object* x_70;
|
||||
lean_dec(x_63);
|
||||
lean_dec(x_62);
|
||||
x_69 = lean_alloc_ctor(8, 2, 0);
|
||||
lean_ctor_set(x_69, 0, x_3);
|
||||
lean_ctor_set(x_69, 1, x_65);
|
||||
return x_69;
|
||||
x_70 = lean_alloc_ctor(8, 2, 0);
|
||||
lean_ctor_set(x_70, 0, x_3);
|
||||
lean_ctor_set(x_70, 1, x_66);
|
||||
return x_70;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 10:
|
||||
{
|
||||
uint8_t x_70;
|
||||
x_70 = !lean_is_exclusive(x_4);
|
||||
if (x_70 == 0)
|
||||
uint8_t x_71;
|
||||
x_71 = !lean_is_exclusive(x_4);
|
||||
if (x_71 == 0)
|
||||
{
|
||||
lean_object* x_71; lean_object* x_72; lean_object* x_73;
|
||||
x_71 = lean_ctor_get(x_4, 2);
|
||||
x_72 = lean_unsigned_to_nat(0u);
|
||||
x_73 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToSet___main___spec__1(x_1, x_2, x_3, x_72, x_71);
|
||||
lean_ctor_set(x_4, 2, x_73);
|
||||
lean_object* x_72; lean_object* x_73; lean_object* x_74;
|
||||
x_72 = lean_ctor_get(x_4, 2);
|
||||
x_73 = lean_unsigned_to_nat(0u);
|
||||
x_74 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToSet___main___spec__1(x_1, x_2, x_3, x_73, x_72);
|
||||
lean_ctor_set(x_4, 2, x_74);
|
||||
return x_4;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79;
|
||||
x_74 = lean_ctor_get(x_4, 0);
|
||||
x_75 = lean_ctor_get(x_4, 1);
|
||||
x_76 = lean_ctor_get(x_4, 2);
|
||||
lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80;
|
||||
x_75 = lean_ctor_get(x_4, 0);
|
||||
x_76 = lean_ctor_get(x_4, 1);
|
||||
x_77 = lean_ctor_get(x_4, 2);
|
||||
lean_inc(x_77);
|
||||
lean_inc(x_76);
|
||||
lean_inc(x_75);
|
||||
lean_inc(x_74);
|
||||
lean_dec(x_4);
|
||||
x_77 = lean_unsigned_to_nat(0u);
|
||||
x_78 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToSet___main___spec__1(x_1, x_2, x_3, x_77, x_76);
|
||||
x_79 = lean_alloc_ctor(10, 3, 0);
|
||||
lean_ctor_set(x_79, 0, x_74);
|
||||
lean_ctor_set(x_79, 1, x_75);
|
||||
lean_ctor_set(x_79, 2, x_78);
|
||||
return x_79;
|
||||
x_78 = lean_unsigned_to_nat(0u);
|
||||
x_79 = l_Array_ummapAux___main___at_Lean_IR_ExpandResetReuse_reuseToSet___main___spec__1(x_1, x_2, x_3, x_78, x_77);
|
||||
x_80 = lean_alloc_ctor(10, 3, 0);
|
||||
lean_ctor_set(x_80, 0, x_75);
|
||||
lean_ctor_set(x_80, 1, x_76);
|
||||
lean_ctor_set(x_80, 2, x_79);
|
||||
return x_80;
|
||||
}
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_80;
|
||||
x_80 = lean_box(0);
|
||||
x_5 = x_80;
|
||||
lean_object* x_81;
|
||||
x_81 = lean_box(0);
|
||||
x_5 = x_81;
|
||||
goto block_12;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue