lean4-htt/tests/lean/computedFieldsCode.lean.expected.out

[Compiler.IR] [result]
    def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
      case x_1 : tobj of
      Exp.var._impl →
        dec x_3;
        let x_9 : u32 := sproj[0, 8] x_1;
        dec x_1;
        let x_10 : tobj := box x_9;
        let x_11 : tobj := app x_2 x_10;
        ret x_11
      Exp.app._impl →
        dec x_2;
        let x_12 : tobj := proj[0] x_1;
        inc x_12;
        let x_13 : tobj := proj[1] x_1;
        inc x_13;
        dec x_1;
        let x_14 : tobj := app x_3 x_12 x_13;
        ret x_14
      Exp.a1._impl →
        dec x_3;
        dec x_2;
        inc x_4;
        ret x_4
      Exp.a2._impl →
        dec x_3;
        dec x_2;
        inc x_5;
        ret x_5
      Exp.a3._impl →
        dec x_3;
        dec x_2;
        inc x_6;
        ret x_6
      Exp.a4._impl →
        dec x_3;
        dec x_2;
        inc x_7;
        ret x_7
      Exp.a5._impl →
        dec x_3;
        dec x_2;
        inc x_8;
        ret x_8
    def Exp.casesOn._override (x_1 : ◾) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
      case x_2 : tobj of
      Exp.var._impl →
        dec x_4;
        let x_10 : u32 := sproj[0, 8] x_2;
        dec x_2;
        let x_11 : tobj := box x_10;
        let x_12 : tobj := app x_3 x_11;
        ret x_12
      Exp.app._impl →
        dec x_3;
        let x_13 : tobj := proj[0] x_2;
        inc x_13;
        let x_14 : tobj := proj[1] x_2;
        inc x_14;
        dec x_2;
        let x_15 : tobj := app x_4 x_13 x_14;
        ret x_15
      Exp.a1._impl →
        dec x_4;
        dec x_3;
        inc x_5;
        ret x_5
      Exp.a2._impl →
        dec x_4;
        dec x_3;
        inc x_6;
        ret x_6
      Exp.a3._impl →
        dec x_4;
        dec x_3;
        inc x_7;
        ret x_7
      Exp.a4._impl →
        dec x_4;
        dec x_3;
        inc x_8;
        ret x_8
      Exp.a5._impl →
        dec x_4;
        dec x_3;
        inc x_9;
        ret x_9
    def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
      let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
      dec x_8;
      dec x_7;
      dec x_6;
      dec x_5;
      dec x_4;
      ret x_9
    def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
      let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
      dec x_9;
      dec x_8;
      dec x_7;
      dec x_6;
      dec x_5;
      ret x_10
[Compiler.IR] [result]
    def Exp.var._override (x_1 : u32) : tobj :=
      let x_2 : u64 := UInt32.toUInt64 x_1;
      let x_3 : u64 := 1000;
      let x_4 : u64 := UInt64.add x_2 x_3;
      let x_5 : obj := ctor_0.0.12[Exp.var._impl];
      sset x_5[0, 0] : u64 := x_4;
      sset x_5[0, 8] : u32 := x_1;
      ret x_5
    def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
      let x_3 : u64 := Exp.hash._override x_1;
      let x_4 : u64 := Exp.hash._override x_2;
      let x_5 : u64 := mixHash x_3 x_4;
      let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
      sset x_6[2, 0] : u64 := x_5;
      ret x_6
    def Exp.a1._override : tobj :=
      let x_1 : tagged := ctor_2[Exp.a1._impl];
      ret x_1
    def Exp.a2._override : tobj :=
      let x_1 : tagged := ctor_3[Exp.a2._impl];
      ret x_1
    def Exp.a3._override : tobj :=
      let x_1 : tagged := ctor_4[Exp.a3._impl];
      ret x_1
    def Exp.a4._override : tobj :=
      let x_1 : tagged := ctor_5[Exp.a4._impl];
      ret x_1
    def Exp.a5._override : tobj :=
      let x_1 : tagged := ctor_6[Exp.a5._impl];
      ret x_1
    def Exp.hash._override (x_1 : @& tobj) : u64 :=
      case x_1 : tobj of
      Exp.var._impl →
        let x_2 : u64 := sproj[0, 0] x_1;
        ret x_2
      Exp.app._impl →
        let x_3 : u64 := sproj[2, 0] x_1;
        ret x_3
      default →
        let x_4 : u64 := 42;
        ret x_4
    def Exp.var._override._boxed (x_1 : tobj) : tobj :=
      let x_2 : u32 := unbox x_1;
      dec x_1;
      let x_3 : tobj := Exp.var._override x_2;
      ret x_3
    def Exp.hash._override._boxed (x_1 : tobj) : tobj :=
      let x_2 : u64 := Exp.hash._override x_1;
      dec x_1;
      let x_3 : tobj := box x_2;
      ret x_3
[Compiler.IR] [result]
    def f._closed_0 : tobj :=
      let x_1 : u32 := 10;
      let x_2 : tobj := Exp.var._override x_1;
      ret x_2
    def f._closed_1 : tobj :=
      let x_1 : tagged := ctor_5[Exp.a4._impl];
      let x_2 : tobj := f._closed_0;
      let x_3 : tobj := Exp.app._override x_2 x_1;
      ret x_3
    def f._closed_2 : u64 :=
      let x_1 : tobj := f._closed_1;
      let x_2 : u64 := Exp.hash._override x_1;
      dec x_1;
      ret x_2
    def f : u64 :=
      let x_1 : u64 := f._closed_2;
      ret x_1
[Compiler.IR] [result]
    def g (x_1 : @& tobj) : u8 :=
      case x_1 : tobj of
      Exp.a3._impl →
        let x_2 : u8 := 1;
        ret x_2
      default →
        let x_3 : u8 := 0;
        ret x_3
    def g._boxed (x_1 : tobj) : tagged :=
      let x_2 : u8 := g x_1;
      dec x_1;
      let x_3 : tobj := box x_2;
      ret x_3
[Compiler.IR] [result]
    def hash' (x_1 : @& tobj) : tobj :=
      case x_1 : tobj of
      Exp.var._impl →
        let x_2 : u32 := sproj[0, 8] x_1;
        let x_3 : tobj := UInt32.toNat x_2;
        ret x_3
      Exp.app._impl →
        let x_4 : tobj := proj[0] x_1;
        let x_5 : tobj := proj[1] x_1;
        let x_6 : tobj := hash' x_4;
        let x_7 : tobj := hash' x_5;
        let x_8 : tobj := Nat.add x_6 x_7;
        dec x_7;
        dec x_6;
        ret x_8
      default →
        let x_9 : tagged := 42;
        ret x_9
    def hash'._boxed (x_1 : tobj) : tobj :=
      let x_2 : tobj := hash' x_1;
      dec x_1;
      ret x_2
[Compiler.IR] [result]
    def getAppFn (x_1 : @& tobj) : tobj :=
      case x_1 : tobj of
      Exp.app._impl →
        let x_2 : tobj := proj[0] x_1;
        let x_3 : tobj := getAppFn x_2;
        ret x_3
      default →
        inc x_1;
        ret x_1
    def getAppFn._boxed (x_1 : tobj) : tobj :=
      let x_2 : tobj := getAppFn x_1;
      dec x_1;
      ret x_2
[Compiler.IR] [result]
    def Exp.f (x_1 : @& tobj) : tobj :=
      let x_2 : tobj := getAppFn x_1;
      ret x_2
    def Exp.f._boxed (x_1 : tobj) : tobj :=
      let x_2 : tobj := Exp.f x_1;
      dec x_1;
      ret x_2