Skip to content

Instantly share code, notes, and snippets.

@bollu

bollu/log

Last active April 3, 2024 14:14
Show Gist options
  • Save bollu/0783b677f73d3a2c17a5e5ff48fd3ad2 to your computer and use it in GitHub Desktop.
Save bollu/0783b677f73d3a2c17a5e5ff48fd3ad2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
log
Lean (version 4.8.0, commit 1f4dea858243, Release)
Lean (version 4.8.0, commit 5281a01ae3a9, Release)
Raw
minified.diff
16c16,17
< let x_13 : usize := ptrAddrUnsafe ◾ x_9;
---
> let x_13 : obj := proj[1] x_10;
> let x_14 : usize := ptrAddrUnsafe ◾ x_9;
18,20c19,21
< let x_14 : usize := ptrAddrUnsafe ◾ x_12;
< let x_15 : u8 := USize.decEq x_13 x_14;
< case x_15 : u8 of
---
> let x_15 : usize := ptrAddrUnsafe ◾ x_12;
> let x_16 : u8 := USize.decEq x_14 x_15;
> case x_16 : u8 of
22,23c23,24
< let x_16 : u8 := isShared x_1;
< case x_16 : u8 of
---
> let x_17 : u8 := isShared x_1;
> case x_17 : u8 of
25,27c26
< let x_17 : obj := proj[1] x_1;
< dec x_17;
< let x_18 : obj := proj[0] x_1;
---
> let x_18 : obj := proj[1] x_1;
29,31c28,34
< set x_1[1] := x_12;
< set x_10[0] := x_1;
< ret x_10
---
> let x_19 : obj := proj[0] x_1;
> dec x_19;
> set x_10[1] := x_12;
> set x_10[0] := x_8;
> set x_1[1] := x_13;
> set x_1[0] := x_10;
> ret x_1
34,36c37,40
< let x_19 : obj := ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_12;
< set x_10[0] := x_19;
< ret x_10
---
> set x_10[1] := x_12;
> set x_10[0] := x_8;
> let x_20 : obj := ctor_0[EStateM.Result.ok] x_10 x_13;
> ret x_20
38,40c42,44
< let x_20 : usize := ptrAddrUnsafe ◾ x_8;
< let x_21 : u8 := USize.decEq x_20 x_20;
< case x_21 : u8 of
---
> let x_21 : usize := ptrAddrUnsafe ◾ x_8;
> let x_22 : u8 := USize.decEq x_21 x_21;
> case x_22 : u8 of
42,43c46,47
< let x_22 : u8 := isShared x_1;
< case x_22 : u8 of
---
> let x_23 : u8 := isShared x_1;
> case x_23 : u8 of
45,47c49
< let x_23 : obj := proj[1] x_1;
< dec x_23;
< let x_24 : obj := proj[0] x_1;
---
> let x_24 : obj := proj[1] x_1;
49,51c51,57
< set x_1[1] := x_12;
< set x_10[0] := x_1;
< ret x_10
---
> let x_25 : obj := proj[0] x_1;
> dec x_25;
> set x_10[1] := x_12;
> set x_10[0] := x_8;
> set x_1[1] := x_13;
> set x_1[0] := x_10;
> ret x_1
54,56c60,63
< let x_25 : obj := ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_12;
< set x_10[0] := x_25;
< ret x_10
---
> set x_10[1] := x_12;
> set x_10[0] := x_8;
> let x_26 : obj := ctor_0[EStateM.Result.ok] x_10 x_13;
> ret x_26
63,64c70,72
< let x_26 : obj := proj[0] x_10;
< let x_27 : obj := proj[1] x_10;
---
> let x_27 : obj := proj[0] x_10;
> let x_28 : obj := proj[1] x_10;
> inc x_28;
66d73
< inc x_26;
68c75
< let x_28 : usize := ptrAddrUnsafe ◾ x_9;
---
> let x_29 : usize := ptrAddrUnsafe ◾ x_9;
70,72c77,79
< let x_29 : usize := ptrAddrUnsafe ◾ x_26;
< let x_30 : u8 := USize.decEq x_28 x_29;
< case x_30 : u8 of
---
> let x_30 : usize := ptrAddrUnsafe ◾ x_27;
> let x_31 : u8 := USize.decEq x_29 x_30;
> case x_31 : u8 of
74,77c81,84
< let x_31 : obj := reset[2] x_1;
< let x_32 : obj := reuse x_31 in ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_26;
< let x_33 : obj := ctor_0[EStateM.Result.ok] x_32 x_27;
< ret x_33
---
> let x_32 : obj := reset[2] x_1;
> let x_33 : obj := ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_27;
> let x_34 : obj := reuse x_32 in ctor_0[EStateM.Result.ok] x_33 x_28;
> ret x_34
79,81c86,88
< let x_34 : usize := ptrAddrUnsafe ◾ x_8;
< let x_35 : u8 := USize.decEq x_34 x_34;
< case x_35 : u8 of
---
> let x_35 : usize := ptrAddrUnsafe ◾ x_8;
> let x_36 : u8 := USize.decEq x_35 x_35;
> case x_36 : u8 of
83,86c90,93
< let x_36 : obj := reset[2] x_1;
< let x_37 : obj := reuse x_36 in ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_26;
< let x_38 : obj := ctor_0[EStateM.Result.ok] x_37 x_27;
< ret x_38
---
> let x_37 : obj := reset[2] x_1;
> let x_38 : obj := ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_27;
> let x_39 : obj := reuse x_37 in ctor_0[EStateM.Result.ok] x_38 x_28;
> ret x_39
88c95
< dec x_26;
---
> dec x_27;
90,91c97,98
< let x_39 : obj := ctor_0[EStateM.Result.ok] x_1 x_27;
< ret x_39
---
> let x_40 : obj := ctor_0[EStateM.Result.ok] x_1 x_28;
> ret x_40
96,97c103,104
< let x_40 : u8 := isShared x_10;
< case x_40 : u8 of
---
> let x_41 : u8 := isShared x_10;
> case x_41 : u8 of
101,102c108,110
< let x_41 : obj := proj[0] x_10;
< let x_42 : obj := proj[1] x_10;
---
> let x_42 : obj := proj[0] x_10;
> let x_43 : obj := proj[1] x_10;
> inc x_43;
104d111
< inc x_41;
106,107c113,114
< let x_43 : obj := ctor_1[EStateM.Result.error] x_41 x_42;
< ret x_43
---
> let x_44 : obj := ctor_1[EStateM.Result.error] x_42 x_43;
> ret x_44
109,111c116
< let x_44 : obj := proj[0] x_1;
< inc x_44;
< let x_45 : obj := proj[1] x_1;
---
> let x_45 : obj := proj[0] x_1;
113c118
< let x_46 : obj := proj[4] x_44;
---
> let x_46 : obj := proj[1] x_1;
114a120,121
> let x_47 : obj := proj[4] x_45;
> inc x_47;
120,121c127,128
< let x_47 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_46 x_2 x_3 x_4 x_5 x_6 x_7;
< case x_47 : obj of
---
> let x_48 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_47 x_2 x_3 x_4 x_5 x_6 x_7;
> case x_48 : obj of
123,125c130
< let x_48 : obj := proj[0] x_47;
< inc x_48;
< let x_49 : obj := proj[1] x_47;
---
> let x_49 : obj := proj[0] x_48;
127,128c132
< dec x_47;
< let x_50 : obj := proj[3] x_44;
---
> let x_50 : obj := proj[1] x_48;
130c134,135
< let x_51 : obj := proj[2] x_44;
---
> dec x_48;
> let x_51 : obj := proj[3] x_45;
132,138c137,138
< inc x_44;
< let x_52 : obj := _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp x_44 x_50 x_51 x_48 x_3 x_4 x_5 x_6 x_49;
< let x_53 : obj := proj[0] x_52;
< inc x_53;
< let x_54 : obj := proj[1] x_52;
< inc x_54;
< dec x_52;
---
> let x_52 : obj := proj[2] x_45;
> inc x_52;
140,151c140,151
< let x_55 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_45 x_2 x_3 x_4 x_5 x_6 x_54;
< case x_55 : obj of
< EStateM.Result.ok →
< let x_56 : u8 := isShared x_55;
< case x_56 : u8 of
< Bool.false →
< let x_57 : obj := proj[0] x_55;
< let x_58 : usize := ptrAddrUnsafe ◾ x_45;
< dec x_45;
< let x_59 : usize := ptrAddrUnsafe ◾ x_57;
< let x_60 : u8 := USize.decEq x_58 x_59;
< case x_60 : u8 of
---
> let x_53 : obj := _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp x_45 x_51 x_52 x_49 x_3 x_4 x_5 x_6 x_50;
> let x_54 : u8 := isShared x_53;
> case x_54 : u8 of
> Bool.false →
> let x_55 : obj := proj[0] x_53;
> let x_56 : obj := proj[1] x_53;
> inc x_46;
> let x_57 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_46 x_2 x_3 x_4 x_5 x_6 x_56;
> case x_57 : obj of
> EStateM.Result.ok →
> let x_58 : u8 := isShared x_57;
> case x_58 : u8 of
153,155c153,159
< dec x_44;
< let x_61 : u8 := isShared x_1;
< case x_61 : u8 of
---
> let x_59 : obj := proj[0] x_57;
> let x_60 : obj := proj[1] x_57;
> let x_61 : usize := ptrAddrUnsafe ◾ x_46;
> dec x_46;
> let x_62 : usize := ptrAddrUnsafe ◾ x_59;
> let x_63 : u8 := USize.decEq x_61 x_62;
> case x_63 : u8 of
157,165c161
< let x_62 : obj := proj[1] x_1;
< dec x_62;
< let x_63 : obj := proj[0] x_1;
< dec x_63;
< set x_1[1] := x_57;
< set x_1[0] := x_53;
< set x_55[0] := x_1;
< ret x_55
< Bool.true →
---
> dec x_45;
167,169c163,188
< let x_64 : obj := ctor_1[Lean.Compiler.LCNF.Code.fun] x_53 x_57;
< set x_55[0] := x_64;
< ret x_55
---
> setTag x_57 := 1;
> set x_57[1] := x_59;
> set x_57[0] := x_55;
> set x_53[1] := x_60;
> set x_53[0] := x_57;
> ret x_53
> Bool.true →
> let x_64 : usize := ptrAddrUnsafe ◾ x_45;
> dec x_45;
> let x_65 : usize := ptrAddrUnsafe ◾ x_55;
> let x_66 : u8 := USize.decEq x_64 x_65;
> case x_66 : u8 of
> Bool.false →
> dec x_1;
> setTag x_57 := 1;
> set x_57[1] := x_59;
> set x_57[0] := x_55;
> set x_53[1] := x_60;
> set x_53[0] := x_57;
> ret x_53
> Bool.true →
> dec x_59;
> del x_53;
> dec x_55;
> set x_57[0] := x_1;
> ret x_57
171,175c190,199
< let x_65 : usize := ptrAddrUnsafe ◾ x_44;
< dec x_44;
< let x_66 : usize := ptrAddrUnsafe ◾ x_53;
< let x_67 : u8 := USize.decEq x_65 x_66;
< case x_67 : u8 of
---
> let x_67 : obj := proj[0] x_57;
> let x_68 : obj := proj[1] x_57;
> inc x_68;
> inc x_67;
> dec x_57;
> let x_69 : usize := ptrAddrUnsafe ◾ x_46;
> dec x_46;
> let x_70 : usize := ptrAddrUnsafe ◾ x_67;
> let x_71 : u8 := USize.decEq x_69 x_70;
> case x_71 : u8 of
177,178c201,212
< let x_68 : u8 := isShared x_1;
< case x_68 : u8 of
---
> dec x_45;
> dec x_1;
> let x_72 : obj := ctor_1[Lean.Compiler.LCNF.Code.fun] x_55 x_67;
> set x_53[1] := x_68;
> set x_53[0] := x_72;
> ret x_53
> Bool.true →
> let x_73 : usize := ptrAddrUnsafe ◾ x_45;
> dec x_45;
> let x_74 : usize := ptrAddrUnsafe ◾ x_55;
> let x_75 : u8 := USize.decEq x_73 x_74;
> case x_75 : u8 of
180,188d213
< let x_69 : obj := proj[1] x_1;
< dec x_69;
< let x_70 : obj := proj[0] x_1;
< dec x_70;
< set x_1[1] := x_57;
< set x_1[0] := x_53;
< set x_55[0] := x_1;
< ret x_55
< Bool.true →
190,202c215,226
< let x_71 : obj := ctor_1[Lean.Compiler.LCNF.Code.fun] x_53 x_57;
< set x_55[0] := x_71;
< ret x_55
< Bool.true →
< dec x_57;
< dec x_53;
< set x_55[0] := x_1;
< ret x_55
< Bool.true →
< let x_72 : obj := proj[0] x_55;
< let x_73 : obj := proj[1] x_55;
< inc x_73;
< inc x_72;
---
> let x_76 : obj := ctor_1[Lean.Compiler.LCNF.Code.fun] x_55 x_67;
> set x_53[1] := x_68;
> set x_53[0] := x_76;
> ret x_53
> Bool.true →
> dec x_67;
> del x_53;
> dec x_55;
> let x_77 : obj := ctor_0[EStateM.Result.ok] x_1 x_68;
> ret x_77
> EStateM.Result.error →
> del x_53;
204c228
< let x_74 : usize := ptrAddrUnsafe ◾ x_45;
---
> dec x_46;
206,208c230,262
< let x_75 : usize := ptrAddrUnsafe ◾ x_72;
< let x_76 : u8 := USize.decEq x_74 x_75;
< case x_76 : u8 of
---
> dec x_1;
> let x_78 : u8 := isShared x_57;
> case x_78 : u8 of
> Bool.false →
> ret x_57
> Bool.true →
> let x_79 : obj := proj[0] x_57;
> let x_80 : obj := proj[1] x_57;
> inc x_80;
> inc x_79;
> dec x_57;
> let x_81 : obj := ctor_1[EStateM.Result.error] x_79 x_80;
> ret x_81
> Bool.true →
> let x_82 : obj := proj[0] x_53;
> let x_83 : obj := proj[1] x_53;
> inc x_83;
> inc x_82;
> dec x_53;
> inc x_46;
> let x_84 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_46 x_2 x_3 x_4 x_5 x_6 x_83;
> case x_84 : obj of
> EStateM.Result.ok →
> let x_85 : obj := proj[0] x_84;
> inc x_85;
> let x_86 : obj := proj[1] x_84;
> inc x_86;
> let x_87 : obj := reset[2] x_84;
> let x_88 : usize := ptrAddrUnsafe ◾ x_46;
> dec x_46;
> let x_89 : usize := ptrAddrUnsafe ◾ x_85;
> let x_90 : u8 := USize.decEq x_88 x_89;
> case x_90 : u8 of
210,214c264,268
< dec x_44;
< let x_77 : obj := reset[2] x_1;
< let x_78 : obj := reuse x_77 in ctor_1[Lean.Compiler.LCNF.Code.fun] x_53 x_72;
< let x_79 : obj := ctor_0[EStateM.Result.ok] x_78 x_73;
< ret x_79
---
> dec x_45;
> dec x_1;
> let x_91 : obj := reuse! x_87 in ctor_1[Lean.Compiler.LCNF.Code.fun] x_82 x_85;
> let x_92 : obj := ctor_0[EStateM.Result.ok] x_91 x_86;
> ret x_92
216,220c270,274
< let x_80 : usize := ptrAddrUnsafe ◾ x_44;
< dec x_44;
< let x_81 : usize := ptrAddrUnsafe ◾ x_53;
< let x_82 : u8 := USize.decEq x_80 x_81;
< case x_82 : u8 of
---
> let x_93 : usize := ptrAddrUnsafe ◾ x_45;
> dec x_45;
> let x_94 : usize := ptrAddrUnsafe ◾ x_82;
> let x_95 : u8 := USize.decEq x_93 x_94;
> case x_95 : u8 of
222,225c276,279
< let x_83 : obj := reset[2] x_1;
< let x_84 : obj := reuse x_83 in ctor_1[Lean.Compiler.LCNF.Code.fun] x_53 x_72;
< let x_85 : obj := ctor_0[EStateM.Result.ok] x_84 x_73;
< ret x_85
---
> dec x_1;
> let x_96 : obj := reuse! x_87 in ctor_1[Lean.Compiler.LCNF.Code.fun] x_82 x_85;
> let x_97 : obj := ctor_0[EStateM.Result.ok] x_96 x_86;
> ret x_97
227,247c281,296
< dec x_72;
< dec x_53;
< let x_86 : obj := ctor_0[EStateM.Result.ok] x_1 x_73;
< ret x_86
< EStateM.Result.error →
< dec x_53;
< dec x_45;
< dec x_44;
< dec x_1;
< let x_87 : u8 := isShared x_55;
< case x_87 : u8 of
< Bool.false →
< ret x_55
< Bool.true →
< let x_88 : obj := proj[0] x_55;
< let x_89 : obj := proj[1] x_55;
< inc x_89;
< inc x_88;
< dec x_55;
< let x_90 : obj := ctor_1[EStateM.Result.error] x_88 x_89;
< ret x_90
---
> dec x_85;
> dec x_82;
> let x_98 : obj := reuse x_87 in ctor_0[EStateM.Result.ok] x_1 x_86;
> ret x_98
> EStateM.Result.error →
> dec x_82;
> dec x_46;
> dec x_45;
> dec x_1;
> let x_99 : obj := proj[0] x_84;
> inc x_99;
> let x_100 : obj := proj[1] x_84;
> inc x_100;
> let x_101 : obj := reset[2] x_84;
> let x_102 : obj := reuse x_101 in ctor_1[EStateM.Result.error] x_99 x_100;
> ret x_102
248a298
> dec x_46;
250d299
< dec x_44;
257,258c306,307
< let x_91 : u8 := isShared x_47;
< case x_91 : u8 of
---
> let x_103 : u8 := isShared x_48;
> case x_103 : u8 of
260c309
< ret x_47
---
> ret x_48
262,268c311,317
< let x_92 : obj := proj[0] x_47;
< let x_93 : obj := proj[1] x_47;
< inc x_93;
< inc x_92;
< dec x_47;
< let x_94 : obj := ctor_1[EStateM.Result.error] x_92 x_93;
< ret x_94
---
> let x_104 : obj := proj[0] x_48;
> let x_105 : obj := proj[1] x_48;
> inc x_105;
> inc x_104;
> dec x_48;
> let x_106 : obj := ctor_1[EStateM.Result.error] x_104 x_105;
> ret x_106
270,278c319,327
< let x_95 : obj := proj[0] x_1;
< inc x_95;
< let x_96 : obj := proj[1] x_1;
< inc x_96;
< let x_97 : obj := proj[0] x_95;
< inc x_97;
< let x_98 : obj := Lean.RBNode.find._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goAnalyze._spec_1 x_2 x_97;
< dec x_97;
< case x_98 : obj of
---
> let x_107 : obj := proj[0] x_1;
> inc x_107;
> let x_108 : obj := proj[1] x_1;
> inc x_108;
> let x_109 : obj := proj[0] x_107;
> inc x_109;
> let x_110 : obj := Lean.RBNode.find._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goAnalyze._spec_1 x_2 x_109;
> dec x_109;
> case x_110 : obj of
280,282c329,331
< inc x_96;
< let x_99 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_96 x_2 x_3 x_4 x_5 x_6 x_7;
< case x_99 : obj of
---
> inc x_108;
> let x_111 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_108 x_2 x_3 x_4 x_5 x_6 x_7;
> case x_111 : obj of
284,285c333,334
< let x_100 : u8 := isShared x_99;
< case x_100 : u8 of
---
> let x_112 : u8 := isShared x_111;
> case x_112 : u8 of
287,292c336,342
< let x_101 : obj := proj[0] x_99;
< let x_102 : usize := ptrAddrUnsafe ◾ x_96;
< dec x_96;
< let x_103 : usize := ptrAddrUnsafe ◾ x_101;
< let x_104 : u8 := USize.decEq x_102 x_103;
< case x_104 : u8 of
---
> let x_113 : obj := proj[0] x_111;
> let x_114 : obj := proj[1] x_111;
> let x_115 : usize := ptrAddrUnsafe ◾ x_108;
> dec x_108;
> let x_116 : usize := ptrAddrUnsafe ◾ x_113;
> let x_117 : u8 := USize.decEq x_115 x_116;
> case x_117 : u8 of
294,295c344,345
< let x_105 : u8 := isShared x_1;
< case x_105 : u8 of
---
> let x_118 : u8 := isShared x_1;
> case x_118 : u8 of
297,303c347,357
< let x_106 : obj := proj[1] x_1;
< dec x_106;
< let x_107 : obj := proj[0] x_1;
< dec x_107;
< set x_1[1] := x_101;
< set x_99[0] := x_1;
< ret x_99
---
> let x_119 : obj := proj[1] x_1;
> dec x_119;
> let x_120 : obj := proj[0] x_1;
> dec x_120;
> setTag x_111 := 2;
> set x_111[1] := x_113;
> set x_111[0] := x_107;
> setTag x_1 := 0;
> set x_1[1] := x_114;
> set x_1[0] := x_111;
> ret x_1
306,308c360,364
< let x_108 : obj := ctor_2[Lean.Compiler.LCNF.Code.jp] x_95 x_101;
< set x_99[0] := x_108;
< ret x_99
---
> setTag x_111 := 2;
> set x_111[1] := x_113;
> set x_111[0] := x_107;
> let x_121 : obj := ctor_0[EStateM.Result.ok] x_111 x_114;
> ret x_121
310,312c366,368
< let x_109 : usize := ptrAddrUnsafe ◾ x_95;
< let x_110 : u8 := USize.decEq x_109 x_109;
< case x_110 : u8 of
---
> let x_122 : usize := ptrAddrUnsafe ◾ x_107;
> let x_123 : u8 := USize.decEq x_122 x_122;
> case x_123 : u8 of
314,315c370,371
< let x_111 : u8 := isShared x_1;
< case x_111 : u8 of
---
> let x_124 : u8 := isShared x_1;
> case x_124 : u8 of
317,323c373,383
< let x_112 : obj := proj[1] x_1;
< dec x_112;
< let x_113 : obj := proj[0] x_1;
< dec x_113;
< set x_1[1] := x_101;
< set x_99[0] := x_1;
< ret x_99
---
> let x_125 : obj := proj[1] x_1;
> dec x_125;
> let x_126 : obj := proj[0] x_1;
> dec x_126;
> setTag x_111 := 2;
> set x_111[1] := x_113;
> set x_111[0] := x_107;
> setTag x_1 := 0;
> set x_1[1] := x_114;
> set x_1[0] := x_111;
> ret x_1
326,328c386,390
< let x_114 : obj := ctor_2[Lean.Compiler.LCNF.Code.jp] x_95 x_101;
< set x_99[0] := x_114;
< ret x_99
---
> setTag x_111 := 2;
> set x_111[1] := x_113;
> set x_111[0] := x_107;
> let x_127 : obj := ctor_0[EStateM.Result.ok] x_111 x_114;
> ret x_127
330,333c392,395
< dec x_101;
< dec x_95;
< set x_99[0] := x_1;
< ret x_99
---
> dec x_113;
> dec x_107;
> set x_111[0] := x_1;
> ret x_111
335,344c397,406
< let x_115 : obj := proj[0] x_99;
< let x_116 : obj := proj[1] x_99;
< inc x_116;
< inc x_115;
< dec x_99;
< let x_117 : usize := ptrAddrUnsafe ◾ x_96;
< dec x_96;
< let x_118 : usize := ptrAddrUnsafe ◾ x_115;
< let x_119 : u8 := USize.decEq x_117 x_118;
< case x_119 : u8 of
---
> let x_128 : obj := proj[0] x_111;
> let x_129 : obj := proj[1] x_111;
> inc x_129;
> inc x_128;
> dec x_111;
> let x_130 : usize := ptrAddrUnsafe ◾ x_108;
> dec x_108;
> let x_131 : usize := ptrAddrUnsafe ◾ x_128;
> let x_132 : u8 := USize.decEq x_130 x_131;
> case x_132 : u8 of
346,349c408,411
< let x_120 : obj := reset[2] x_1;
< let x_121 : obj := reuse x_120 in ctor_2[Lean.Compiler.LCNF.Code.jp] x_95 x_115;
< let x_122 : obj := ctor_0[EStateM.Result.ok] x_121 x_116;
< ret x_122
---
> let x_133 : obj := reset[2] x_1;
> let x_134 : obj := ctor_2[Lean.Compiler.LCNF.Code.jp] x_107 x_128;
> let x_135 : obj := reuse! x_133 in ctor_0[EStateM.Result.ok] x_134 x_129;
> ret x_135
351,353c413,415
< let x_123 : usize := ptrAddrUnsafe ◾ x_95;
< let x_124 : u8 := USize.decEq x_123 x_123;
< case x_124 : u8 of
---
> let x_136 : usize := ptrAddrUnsafe ◾ x_107;
> let x_137 : u8 := USize.decEq x_136 x_136;
> case x_137 : u8 of
355,358c417,420
< let x_125 : obj := reset[2] x_1;
< let x_126 : obj := reuse x_125 in ctor_2[Lean.Compiler.LCNF.Code.jp] x_95 x_115;
< let x_127 : obj := ctor_0[EStateM.Result.ok] x_126 x_116;
< ret x_127
---
> let x_138 : obj := reset[2] x_1;
> let x_139 : obj := ctor_2[Lean.Compiler.LCNF.Code.jp] x_107 x_128;
> let x_140 : obj := reuse! x_138 in ctor_0[EStateM.Result.ok] x_139 x_129;
> ret x_140
360,363c422,425
< dec x_115;
< dec x_95;
< let x_128 : obj := ctor_0[EStateM.Result.ok] x_1 x_116;
< ret x_128
---
> dec x_128;
> dec x_107;
> let x_141 : obj := ctor_0[EStateM.Result.ok] x_1 x_129;
> ret x_141
365,366c427,428
< dec x_96;
< dec x_95;
---
> dec x_108;
> dec x_107;
368,369c430,431
< let x_129 : u8 := isShared x_99;
< case x_129 : u8 of
---
> let x_142 : u8 := isShared x_111;
> case x_142 : u8 of
371c433
< ret x_99
---
> ret x_111
373,379c435,441
< let x_130 : obj := proj[0] x_99;
< let x_131 : obj := proj[1] x_99;
< inc x_131;
< inc x_130;
< dec x_99;
< let x_132 : obj := ctor_1[EStateM.Result.error] x_130 x_131;
< ret x_132
---
> let x_143 : obj := proj[0] x_111;
> let x_144 : obj := proj[1] x_111;
> inc x_144;
> inc x_143;
> dec x_111;
> let x_145 : obj := ctor_1[EStateM.Result.error] x_143 x_144;
> ret x_145
381,389c443,451
< let x_133 : obj := proj[0] x_98;
< inc x_133;
< dec x_98;
< let x_134 : obj := proj[2] x_95;
< inc x_134;
< let x_135 : obj := Array.size ◾ x_134;
< let x_136 : obj := 0;
< let x_137 : u8 := Nat.decLt x_136 x_135;
< case x_137 : u8 of
---
> let x_146 : obj := proj[0] x_110;
> inc x_146;
> dec x_110;
> let x_147 : obj := proj[2] x_107;
> inc x_147;
> let x_148 : obj := Array.size ◾ x_147;
> let x_149 : obj := 0;
> let x_150 : u8 := Nat.decLt x_149 x_148;
> case x_150 : u8 of
391,393c453,455
< dec x_134;
< let x_138 : obj := proj[4] x_95;
< inc x_138;
---
> dec x_147;
> let x_151 : obj := proj[4] x_107;
> inc x_151;
399,400c461,462
< let x_139 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_138 x_2 x_3 x_4 x_5 x_6 x_7;
< case x_139 : obj of
---
> let x_152 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_151 x_2 x_3 x_4 x_5 x_6 x_7;
> case x_152 : obj of
402,407c464,469
< let x_140 : obj := proj[0] x_139;
< inc x_140;
< let x_141 : obj := proj[1] x_139;
< inc x_141;
< dec x_139;
< let x_142 : u8 := 0;
---
> let x_153 : obj := proj[0] x_152;
> inc x_153;
> let x_154 : obj := proj[1] x_152;
> inc x_154;
> dec x_152;
> let x_155 : u8 := 0;
412,413c474,475
< let x_143 : obj := Lean.Compiler.LCNF.normCodeImp x_142 x_140 x_133 x_3 x_4 x_5 x_6 x_141;
< case x_143 : obj of
---
> let x_156 : obj := Lean.Compiler.LCNF.normCodeImp x_155 x_153 x_146 x_3 x_4 x_5 x_6 x_154;
> case x_156 : obj of
415,424c477,486
< let x_144 : obj := proj[0] x_143;
< inc x_144;
< let x_145 : obj := proj[1] x_143;
< inc x_145;
< dec x_143;
< let x_146 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_2;
< let x_147 : u8 := Nat.beq x_146 x_135;
< dec x_135;
< dec x_146;
< case x_147 : u8 of
---
> let x_157 : obj := proj[0] x_156;
> inc x_157;
> let x_158 : obj := proj[1] x_156;
> inc x_158;
> dec x_156;
> let x_159 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_2;
> let x_160 : u8 := Nat.beq x_159 x_148;
> dec x_148;
> dec x_159;
> case x_160 : u8 of
430,432c492,494
< inc x_144;
< let x_148 : obj := Lean.Compiler.LCNF.Code.inferType x_144 x_3 x_4 x_5 x_6 x_145;
< case x_148 : obj of
---
> inc x_157;
> let x_161 : obj := Lean.Compiler.LCNF.Code.inferType x_157 x_3 x_4 x_5 x_6 x_158;
> case x_161 : obj of
434,439c496,501
< let x_149 : obj := proj[0] x_148;
< inc x_149;
< let x_150 : obj := proj[1] x_148;
< inc x_150;
< dec x_148;
< let x_151 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
---
> let x_162 : obj := proj[0] x_161;
> inc x_162;
> let x_163 : obj := proj[1] x_161;
> inc x_163;
> dec x_161;
> let x_164 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
444,446c506,508
< inc x_151;
< let x_152 : obj := Lean.Compiler.LCNF.mkForallParams x_151 x_149 x_3 x_4 x_5 x_6 x_150;
< case x_152 : obj of
---
> inc x_164;
> let x_165 : obj := Lean.Compiler.LCNF.mkForallParams x_164 x_162 x_3 x_4 x_5 x_6 x_163;
> case x_165 : obj of
448,454c510,516
< let x_153 : obj := proj[0] x_152;
< inc x_153;
< let x_154 : obj := proj[1] x_152;
< inc x_154;
< dec x_152;
< let x_155 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_96 x_95 x_151 x_144 x_1 x_153 x_2 x_3 x_4 x_5 x_6 x_154;
< ret x_155
---
> let x_166 : obj := proj[0] x_165;
> inc x_166;
> let x_167 : obj := proj[1] x_165;
> inc x_167;
> dec x_165;
> let x_168 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_108 x_107 x_164 x_157 x_1 x_166 x_2 x_3 x_4 x_5 x_6 x_167;
> ret x_168
456,459c518,521
< dec x_151;
< dec x_144;
< dec x_96;
< dec x_95;
---
> dec x_164;
> dec x_157;
> dec x_108;
> dec x_107;
466,467c528,529
< let x_156 : u8 := isShared x_152;
< case x_156 : u8 of
---
> let x_169 : u8 := isShared x_165;
> case x_169 : u8 of
469c531
< ret x_152
---
> ret x_165
471,477c533,539
< let x_157 : obj := proj[0] x_152;
< let x_158 : obj := proj[1] x_152;
< inc x_158;
< inc x_157;
< dec x_152;
< let x_159 : obj := ctor_1[EStateM.Result.error] x_157 x_158;
< ret x_159
---
> let x_170 : obj := proj[0] x_165;
> let x_171 : obj := proj[1] x_165;
> inc x_171;
> inc x_170;
> dec x_165;
> let x_172 : obj := ctor_1[EStateM.Result.error] x_170 x_171;
> ret x_172
479,481c541,543
< dec x_144;
< dec x_96;
< dec x_95;
---
> dec x_157;
> dec x_108;
> dec x_107;
488,489c550,551
< let x_160 : u8 := isShared x_148;
< case x_160 : u8 of
---
> let x_173 : u8 := isShared x_161;
> case x_173 : u8 of
491c553
< ret x_148
---
> ret x_161
493,499c555,561
< let x_161 : obj := proj[0] x_148;
< let x_162 : obj := proj[1] x_148;
< inc x_162;
< inc x_161;
< dec x_148;
< let x_163 : obj := ctor_1[EStateM.Result.error] x_161 x_162;
< ret x_163
---
> let x_174 : obj := proj[0] x_161;
> let x_175 : obj := proj[1] x_161;
> inc x_175;
> inc x_174;
> dec x_161;
> let x_176 : obj := ctor_1[EStateM.Result.error] x_174 x_175;
> ret x_176
501,505c563,567
< let x_164 : obj := proj[3] x_95;
< inc x_164;
< let x_165 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
< let x_166 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_96 x_95 x_165 x_144 x_1 x_164 x_2 x_3 x_4 x_5 x_6 x_145;
< ret x_166
---
> let x_177 : obj := proj[3] x_107;
> inc x_177;
> let x_178 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
> let x_179 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_108 x_107 x_178 x_157 x_1 x_177 x_2 x_3 x_4 x_5 x_6 x_158;
> ret x_179
507,509c569,571
< dec x_135;
< dec x_96;
< dec x_95;
---
> dec x_148;
> dec x_108;
> dec x_107;
516,517c578,579
< let x_167 : u8 := isShared x_143;
< case x_167 : u8 of
---
> let x_180 : u8 := isShared x_156;
> case x_180 : u8 of
519c581
< ret x_143
---
> ret x_156
521,527c583,589
< let x_168 : obj := proj[0] x_143;
< let x_169 : obj := proj[1] x_143;
< inc x_169;
< inc x_168;
< dec x_143;
< let x_170 : obj := ctor_1[EStateM.Result.error] x_168 x_169;
< ret x_170
---
> let x_181 : obj := proj[0] x_156;
> let x_182 : obj := proj[1] x_156;
> inc x_182;
> inc x_181;
> dec x_156;
> let x_183 : obj := ctor_1[EStateM.Result.error] x_181 x_182;
> ret x_183
529,532c591,594
< dec x_135;
< dec x_133;
< dec x_96;
< dec x_95;
---
> dec x_148;
> dec x_146;
> dec x_108;
> dec x_107;
539,540c601,602
< let x_171 : u8 := isShared x_139;
< case x_171 : u8 of
---
> let x_184 : u8 := isShared x_152;
> case x_184 : u8 of
542c604
< ret x_139
---
> ret x_152
544,550c606,612
< let x_172 : obj := proj[0] x_139;
< let x_173 : obj := proj[1] x_139;
< inc x_173;
< inc x_172;
< dec x_139;
< let x_174 : obj := ctor_1[EStateM.Result.error] x_172 x_173;
< ret x_174
---
> let x_185 : obj := proj[0] x_152;
> let x_186 : obj := proj[1] x_152;
> inc x_186;
> inc x_185;
> dec x_152;
> let x_187 : obj := ctor_1[EStateM.Result.error] x_185 x_186;
> ret x_187
552,553c614,615
< let x_175 : u8 := Nat.decLe x_135 x_135;
< case x_175 : u8 of
---
> let x_188 : u8 := Nat.decLe x_148 x_148;
> case x_188 : u8 of
555,557c617,619
< dec x_134;
< let x_176 : obj := proj[4] x_95;
< inc x_176;
---
> dec x_147;
> let x_189 : obj := proj[4] x_107;
> inc x_189;
563,564c625,626
< let x_177 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_176 x_2 x_3 x_4 x_5 x_6 x_7;
< case x_177 : obj of
---
> let x_190 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_189 x_2 x_3 x_4 x_5 x_6 x_7;
> case x_190 : obj of
566,571c628,633
< let x_178 : obj := proj[0] x_177;
< inc x_178;
< let x_179 : obj := proj[1] x_177;
< inc x_179;
< dec x_177;
< let x_180 : u8 := 0;
---
> let x_191 : obj := proj[0] x_190;
> inc x_191;
> let x_192 : obj := proj[1] x_190;
> inc x_192;
> dec x_190;
> let x_193 : u8 := 0;
576,577c638,639
< let x_181 : obj := Lean.Compiler.LCNF.normCodeImp x_180 x_178 x_133 x_3 x_4 x_5 x_6 x_179;
< case x_181 : obj of
---
> let x_194 : obj := Lean.Compiler.LCNF.normCodeImp x_193 x_191 x_146 x_3 x_4 x_5 x_6 x_192;
> case x_194 : obj of
579,588c641,650
< let x_182 : obj := proj[0] x_181;
< inc x_182;
< let x_183 : obj := proj[1] x_181;
< inc x_183;
< dec x_181;
< let x_184 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_2;
< let x_185 : u8 := Nat.beq x_184 x_135;
< dec x_135;
< dec x_184;
< case x_185 : u8 of
---
> let x_195 : obj := proj[0] x_194;
> inc x_195;
> let x_196 : obj := proj[1] x_194;
> inc x_196;
> dec x_194;
> let x_197 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_2;
> let x_198 : u8 := Nat.beq x_197 x_148;
> dec x_148;
> dec x_197;
> case x_198 : u8 of
594,596c656,658
< inc x_182;
< let x_186 : obj := Lean.Compiler.LCNF.Code.inferType x_182 x_3 x_4 x_5 x_6 x_183;
< case x_186 : obj of
---
> inc x_195;
> let x_199 : obj := Lean.Compiler.LCNF.Code.inferType x_195 x_3 x_4 x_5 x_6 x_196;
> case x_199 : obj of
598,603c660,665
< let x_187 : obj := proj[0] x_186;
< inc x_187;
< let x_188 : obj := proj[1] x_186;
< inc x_188;
< dec x_186;
< let x_189 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
---
> let x_200 : obj := proj[0] x_199;
> inc x_200;
> let x_201 : obj := proj[1] x_199;
> inc x_201;
> dec x_199;
> let x_202 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
608,610c670,672
< inc x_189;
< let x_190 : obj := Lean.Compiler.LCNF.mkForallParams x_189 x_187 x_3 x_4 x_5 x_6 x_188;
< case x_190 : obj of
---
> inc x_202;
> let x_203 : obj := Lean.Compiler.LCNF.mkForallParams x_202 x_200 x_3 x_4 x_5 x_6 x_201;
> case x_203 : obj of
612,618c674,680
< let x_191 : obj := proj[0] x_190;
< inc x_191;
< let x_192 : obj := proj[1] x_190;
< inc x_192;
< dec x_190;
< let x_193 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_96 x_95 x_189 x_182 x_1 x_191 x_2 x_3 x_4 x_5 x_6 x_192;
< ret x_193
---
> let x_204 : obj := proj[0] x_203;
> inc x_204;
> let x_205 : obj := proj[1] x_203;
> inc x_205;
> dec x_203;
> let x_206 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_108 x_107 x_202 x_195 x_1 x_204 x_2 x_3 x_4 x_5 x_6 x_205;
> ret x_206
620,623c682,685
< dec x_189;
< dec x_182;
< dec x_96;
< dec x_95;
---
> dec x_202;
> dec x_195;
> dec x_108;
> dec x_107;
630,631c692,693
< let x_194 : u8 := isShared x_190;
< case x_194 : u8 of
---
> let x_207 : u8 := isShared x_203;
> case x_207 : u8 of
633c695
< ret x_190
---
> ret x_203
635,641c697,703
< let x_195 : obj := proj[0] x_190;
< let x_196 : obj := proj[1] x_190;
< inc x_196;
< inc x_195;
< dec x_190;
< let x_197 : obj := ctor_1[EStateM.Result.error] x_195 x_196;
< ret x_197
---
> let x_208 : obj := proj[0] x_203;
> let x_209 : obj := proj[1] x_203;
> inc x_209;
> inc x_208;
> dec x_203;
> let x_210 : obj := ctor_1[EStateM.Result.error] x_208 x_209;
> ret x_210
643,645c705,707
< dec x_182;
< dec x_96;
< dec x_95;
---
> dec x_195;
> dec x_108;
> dec x_107;
652,653c714,715
< let x_198 : u8 := isShared x_186;
< case x_198 : u8 of
---
> let x_211 : u8 := isShared x_199;
> case x_211 : u8 of
655c717
< ret x_186
---
> ret x_199
657,663c719,725
< let x_199 : obj := proj[0] x_186;
< let x_200 : obj := proj[1] x_186;
< inc x_200;
< inc x_199;
< dec x_186;
< let x_201 : obj := ctor_1[EStateM.Result.error] x_199 x_200;
< ret x_201
---
> let x_212 : obj := proj[0] x_199;
> let x_213 : obj := proj[1] x_199;
> inc x_213;
> inc x_212;
> dec x_199;
> let x_214 : obj := ctor_1[EStateM.Result.error] x_212 x_213;
> ret x_214
665,669c727,731
< let x_202 : obj := proj[3] x_95;
< inc x_202;
< let x_203 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
< let x_204 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_96 x_95 x_203 x_182 x_1 x_202 x_2 x_3 x_4 x_5 x_6 x_183;
< ret x_204
---
> let x_215 : obj := proj[3] x_107;
> inc x_215;
> let x_216 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
> let x_217 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_108 x_107 x_216 x_195 x_1 x_215 x_2 x_3 x_4 x_5 x_6 x_196;
> ret x_217
671,673c733,735
< dec x_135;
< dec x_96;
< dec x_95;
---
> dec x_148;
> dec x_108;
> dec x_107;
680,681c742,743
< let x_205 : u8 := isShared x_181;
< case x_205 : u8 of
---
> let x_218 : u8 := isShared x_194;
> case x_218 : u8 of
683c745
< ret x_181
---
> ret x_194
685,691c747,753
< let x_206 : obj := proj[0] x_181;
< let x_207 : obj := proj[1] x_181;
< inc x_207;
< inc x_206;
< dec x_181;
< let x_208 : obj := ctor_1[EStateM.Result.error] x_206 x_207;
< ret x_208
---
> let x_219 : obj := proj[0] x_194;
> let x_220 : obj := proj[1] x_194;
> inc x_220;
> inc x_219;
> dec x_194;
> let x_221 : obj := ctor_1[EStateM.Result.error] x_219 x_220;
> ret x_221
693,696c755,758
< dec x_135;
< dec x_133;
< dec x_96;
< dec x_95;
---
> dec x_148;
> dec x_146;
> dec x_108;
> dec x_107;
703,704c765,766
< let x_209 : u8 := isShared x_177;
< case x_209 : u8 of
---
> let x_222 : u8 := isShared x_190;
> case x_222 : u8 of
706c768
< ret x_177
---
> ret x_190
708,714c770,776
< let x_210 : obj := proj[0] x_177;
< let x_211 : obj := proj[1] x_177;
< inc x_211;
< inc x_210;
< dec x_177;
< let x_212 : obj := ctor_1[EStateM.Result.error] x_210 x_211;
< ret x_212
---
> let x_223 : obj := proj[0] x_190;
> let x_224 : obj := proj[1] x_190;
> inc x_224;
> inc x_223;
> dec x_190;
> let x_225 : obj := ctor_1[EStateM.Result.error] x_223 x_224;
> ret x_225
716,727c778,789
< let x_213 : usize := 0;
< let x_214 : usize := USize.ofNat x_135;
< let x_215 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
< let x_216 : obj := Array.foldlMUnsafe.fold._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_2 x_133 x_134 x_213 x_214 x_215 x_2 x_3 x_4 x_5 x_6 x_7;
< dec x_134;
< let x_217 : obj := proj[0] x_216;
< inc x_217;
< let x_218 : obj := proj[1] x_216;
< inc x_218;
< dec x_216;
< let x_219 : obj := proj[4] x_95;
< inc x_219;
---
> let x_226 : usize := 0;
> let x_227 : usize := USize.ofNat x_148;
> let x_228 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
> let x_229 : obj := Array.foldlMUnsafe.fold._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_2 x_146 x_147 x_226 x_227 x_228 x_2 x_3 x_4 x_5 x_6 x_7;
> dec x_147;
> let x_230 : obj := proj[0] x_229;
> inc x_230;
> let x_231 : obj := proj[1] x_229;
> inc x_231;
> dec x_229;
> let x_232 : obj := proj[4] x_107;
> inc x_232;
733,734c795,796
< let x_220 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_219 x_2 x_3 x_4 x_5 x_6 x_218;
< case x_220 : obj of
---
> let x_233 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_232 x_2 x_3 x_4 x_5 x_6 x_231;
> case x_233 : obj of
736,741c798,803
< let x_221 : obj := proj[0] x_220;
< inc x_221;
< let x_222 : obj := proj[1] x_220;
< inc x_222;
< dec x_220;
< let x_223 : u8 := 0;
---
> let x_234 : obj := proj[0] x_233;
> inc x_234;
> let x_235 : obj := proj[1] x_233;
> inc x_235;
> dec x_233;
> let x_236 : u8 := 0;
746,747c808,809
< let x_224 : obj := Lean.Compiler.LCNF.normCodeImp x_223 x_221 x_133 x_3 x_4 x_5 x_6 x_222;
< case x_224 : obj of
---
> let x_237 : obj := Lean.Compiler.LCNF.normCodeImp x_236 x_234 x_146 x_3 x_4 x_5 x_6 x_235;
> case x_237 : obj of
749,758c811,820
< let x_225 : obj := proj[0] x_224;
< inc x_225;
< let x_226 : obj := proj[1] x_224;
< inc x_226;
< dec x_224;
< let x_227 : obj := Array.size ◾ x_217;
< let x_228 : u8 := Nat.beq x_227 x_135;
< dec x_135;
< dec x_227;
< case x_228 : u8 of
---
> let x_238 : obj := proj[0] x_237;
> inc x_238;
> let x_239 : obj := proj[1] x_237;
> inc x_239;
> dec x_237;
> let x_240 : obj := Array.size ◾ x_230;
> let x_241 : u8 := Nat.beq x_240 x_148;
> dec x_148;
> dec x_240;
> case x_241 : u8 of
764,766c826,828
< inc x_225;
< let x_229 : obj := Lean.Compiler.LCNF.Code.inferType x_225 x_3 x_4 x_5 x_6 x_226;
< case x_229 : obj of
---
> inc x_238;
> let x_242 : obj := Lean.Compiler.LCNF.Code.inferType x_238 x_3 x_4 x_5 x_6 x_239;
> case x_242 : obj of
768,772c830,834
< let x_230 : obj := proj[0] x_229;
< inc x_230;
< let x_231 : obj := proj[1] x_229;
< inc x_231;
< dec x_229;
---
> let x_243 : obj := proj[0] x_242;
> inc x_243;
> let x_244 : obj := proj[1] x_242;
> inc x_244;
> dec x_242;
777,779c839,841
< inc x_217;
< let x_232 : obj := Lean.Compiler.LCNF.mkForallParams x_217 x_230 x_3 x_4 x_5 x_6 x_231;
< case x_232 : obj of
---
> inc x_230;
> let x_245 : obj := Lean.Compiler.LCNF.mkForallParams x_230 x_243 x_3 x_4 x_5 x_6 x_244;
> case x_245 : obj of
781,787c843,849
< let x_233 : obj := proj[0] x_232;
< inc x_233;
< let x_234 : obj := proj[1] x_232;
< inc x_234;
< dec x_232;
< let x_235 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_96 x_95 x_217 x_225 x_1 x_233 x_2 x_3 x_4 x_5 x_6 x_234;
< ret x_235
---
> let x_246 : obj := proj[0] x_245;
> inc x_246;
> let x_247 : obj := proj[1] x_245;
> inc x_247;
> dec x_245;
> let x_248 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_108 x_107 x_230 x_238 x_1 x_246 x_2 x_3 x_4 x_5 x_6 x_247;
> ret x_248
789,792c851,854
< dec x_225;
< dec x_217;
< dec x_96;
< dec x_95;
---
> dec x_238;
> dec x_230;
> dec x_108;
> dec x_107;
799,800c861,862
< let x_236 : u8 := isShared x_232;
< case x_236 : u8 of
---
> let x_249 : u8 := isShared x_245;
> case x_249 : u8 of
802c864
< ret x_232
---
> ret x_245
804,810c866,872
< let x_237 : obj := proj[0] x_232;
< let x_238 : obj := proj[1] x_232;
< inc x_238;
< inc x_237;
< dec x_232;
< let x_239 : obj := ctor_1[EStateM.Result.error] x_237 x_238;
< ret x_239
---
> let x_250 : obj := proj[0] x_245;
> let x_251 : obj := proj[1] x_245;
> inc x_251;
> inc x_250;
> dec x_245;
> let x_252 : obj := ctor_1[EStateM.Result.error] x_250 x_251;
> ret x_252
812,815c874,877
< dec x_225;
< dec x_217;
< dec x_96;
< dec x_95;
---
> dec x_238;
> dec x_230;
> dec x_108;
> dec x_107;
822,823c884,885
< let x_240 : u8 := isShared x_229;
< case x_240 : u8 of
---
> let x_253 : u8 := isShared x_242;
> case x_253 : u8 of
825c887
< ret x_229
---
> ret x_242
827,833c889,895
< let x_241 : obj := proj[0] x_229;
< let x_242 : obj := proj[1] x_229;
< inc x_242;
< inc x_241;
< dec x_229;
< let x_243 : obj := ctor_1[EStateM.Result.error] x_241 x_242;
< ret x_243
---
> let x_254 : obj := proj[0] x_242;
> let x_255 : obj := proj[1] x_242;
> inc x_255;
> inc x_254;
> dec x_242;
> let x_256 : obj := ctor_1[EStateM.Result.error] x_254 x_255;
> ret x_256
835,838c897,900
< let x_244 : obj := proj[3] x_95;
< inc x_244;
< let x_245 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_96 x_95 x_217 x_225 x_1 x_244 x_2 x_3 x_4 x_5 x_6 x_226;
< ret x_245
---
> let x_257 : obj := proj[3] x_107;
> inc x_257;
> let x_258 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._lambda_1 x_108 x_107 x_230 x_238 x_1 x_257 x_2 x_3 x_4 x_5 x_6 x_239;
> ret x_258
840,843c902,905
< dec x_217;
< dec x_135;
< dec x_96;
< dec x_95;
---
> dec x_230;
> dec x_148;
> dec x_108;
> dec x_107;
850,851c912,913
< let x_246 : u8 := isShared x_224;
< case x_246 : u8 of
---
> let x_259 : u8 := isShared x_237;
> case x_259 : u8 of
853c915
< ret x_224
---
> ret x_237
855,861c917,923
< let x_247 : obj := proj[0] x_224;
< let x_248 : obj := proj[1] x_224;
< inc x_248;
< inc x_247;
< dec x_224;
< let x_249 : obj := ctor_1[EStateM.Result.error] x_247 x_248;
< ret x_249
---
> let x_260 : obj := proj[0] x_237;
> let x_261 : obj := proj[1] x_237;
> inc x_261;
> inc x_260;
> dec x_237;
> let x_262 : obj := ctor_1[EStateM.Result.error] x_260 x_261;
> ret x_262
863,867c925,929
< dec x_217;
< dec x_135;
< dec x_133;
< dec x_96;
< dec x_95;
---
> dec x_230;
> dec x_148;
> dec x_146;
> dec x_108;
> dec x_107;
874,875c936,937
< let x_250 : u8 := isShared x_220;
< case x_250 : u8 of
---
> let x_263 : u8 := isShared x_233;
> case x_263 : u8 of
877c939
< ret x_220
---
> ret x_233
879,885c941,947
< let x_251 : obj := proj[0] x_220;
< let x_252 : obj := proj[1] x_220;
< inc x_252;
< inc x_251;
< dec x_220;
< let x_253 : obj := ctor_1[EStateM.Result.error] x_251 x_252;
< ret x_253
---
> let x_264 : obj := proj[0] x_233;
> let x_265 : obj := proj[1] x_233;
> inc x_265;
> inc x_264;
> dec x_233;
> let x_266 : obj := ctor_1[EStateM.Result.error] x_264 x_265;
> ret x_266
887,892c949,954
< let x_254 : obj := proj[0] x_1;
< inc x_254;
< let x_255 : obj := proj[1] x_1;
< inc x_255;
< block_299 (x_256 : obj) (x_257 : obj) (x_258 : obj) :=
< block_286 (x_259 : obj) :=
---
> let x_267 : obj := proj[0] x_1;
> inc x_267;
> let x_268 : obj := proj[1] x_1;
> inc x_268;
> block_333 (x_269 : obj) (x_270 : obj) (x_271 : obj) :=
> block_320 (x_272 : obj) :=
893a956,976
> Lean.Compiler.LCNF.Code.let →
> dec x_272;
> dec x_267;
> let x_273 : u8 := isShared x_1;
> case x_273 : u8 of
> Bool.false →
> let x_274 : obj := proj[1] x_1;
> dec x_274;
> let x_275 : obj := proj[0] x_1;
> dec x_275;
> let x_276 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_5;
> let x_277 : obj := panic._at._private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp._spec_1 x_276;
> set x_1[1] := x_271;
> set x_1[0] := x_277;
> ret x_1
> Bool.true →
> dec x_1;
> let x_278 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_5;
> let x_279 : obj := panic._at._private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp._spec_1 x_278;
> let x_280 : obj := ctor_0[EStateM.Result.ok] x_279 x_271;
> ret x_280
895,906c978,989
< let x_260 : obj := proj[0] x_1;
< inc x_260;
< let x_261 : obj := proj[1] x_1;
< inc x_261;
< let x_262 : obj := Array.size ◾ x_259;
< let x_263 : usize := USize.ofNat x_262;
< dec x_262;
< let x_264 : usize := 0;
< let x_265 : obj := Array.mapMUnsafe.map._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_3 x_263 x_264 x_259;
< let x_266 : u8 := Lean.Name.beq x_260 x_254;
< dec x_260;
< case x_266 : u8 of
---
> let x_281 : obj := proj[0] x_1;
> inc x_281;
> let x_282 : obj := proj[1] x_1;
> inc x_282;
> let x_283 : obj := Array.size ◾ x_272;
> let x_284 : usize := USize.ofNat x_283;
> dec x_283;
> let x_285 : usize := 0;
> let x_286 : obj := Array.mapMUnsafe.map._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_3 x_284 x_285 x_272;
> let x_287 : u8 := Lean.Name.beq x_281 x_267;
> dec x_281;
> case x_287 : u8 of
908,910c991,993
< dec x_261;
< let x_267 : u8 := isShared x_1;
< case x_267 : u8 of
---
> dec x_282;
> let x_288 : u8 := isShared x_1;
> case x_288 : u8 of
912,918c995,1015
< let x_268 : obj := proj[1] x_1;
< dec x_268;
< let x_269 : obj := proj[0] x_1;
< dec x_269;
< set x_1[1] := x_265;
< let x_270 : obj := ctor_0[EStateM.Result.ok] x_1 x_258;
< ret x_270
---
> let x_289 : obj := proj[1] x_1;
> dec x_289;
> let x_290 : obj := proj[0] x_1;
> dec x_290;
> let x_291 : u8 := isShared x_1;
> case x_291 : u8 of
> Bool.false →
> let x_292 : obj := proj[1] x_1;
> dec x_292;
> let x_293 : obj := proj[0] x_1;
> dec x_293;
> set x_1[1] := x_286;
> setTag x_1 := 0;
> set x_1[1] := x_271;
> set x_1[0] := x_1;
> ret x_1
> Bool.true →
> dec x_1;
> set x_1[1] := x_286;
> let x_294 : obj := ctor_0[EStateM.Result.ok] x_1 x_271;
> ret x_294
921,923c1018,1021
< let x_271 : obj := ctor_3[Lean.Compiler.LCNF.Code.jmp] x_254 x_265;
< let x_272 : obj := ctor_0[EStateM.Result.ok] x_271 x_258;
< ret x_272
---
> let x_295 : obj := reset[2] x_1;
> let x_296 : obj := ctor_3[Lean.Compiler.LCNF.Code.jmp] x_267 x_286;
> let x_297 : obj := reuse! x_295 in ctor_0[EStateM.Result.ok] x_296 x_271;
> ret x_297
925,929c1023,1027
< let x_273 : usize := ptrAddrUnsafe ◾ x_261;
< dec x_261;
< let x_274 : usize := ptrAddrUnsafe ◾ x_265;
< let x_275 : u8 := USize.decEq x_273 x_274;
< case x_275 : u8 of
---
> let x_298 : usize := ptrAddrUnsafe ◾ x_282;
> dec x_282;
> let x_299 : usize := ptrAddrUnsafe ◾ x_286;
> let x_300 : u8 := USize.decEq x_298 x_299;
> case x_300 : u8 of
931,932c1029,1030
< let x_276 : u8 := isShared x_1;
< case x_276 : u8 of
---
> let x_301 : u8 := isShared x_1;
> case x_301 : u8 of
934,940c1032,1052
< let x_277 : obj := proj[1] x_1;
< dec x_277;
< let x_278 : obj := proj[0] x_1;
< dec x_278;
< set x_1[1] := x_265;
< let x_279 : obj := ctor_0[EStateM.Result.ok] x_1 x_258;
< ret x_279
---
> let x_302 : obj := proj[1] x_1;
> dec x_302;
> let x_303 : obj := proj[0] x_1;
> dec x_303;
> let x_304 : u8 := isShared x_1;
> case x_304 : u8 of
> Bool.false →
> let x_305 : obj := proj[1] x_1;
> dec x_305;
> let x_306 : obj := proj[0] x_1;
> dec x_306;
> set x_1[1] := x_286;
> setTag x_1 := 0;
> set x_1[1] := x_271;
> set x_1[0] := x_1;
> ret x_1
> Bool.true →
> dec x_1;
> set x_1[1] := x_286;
> let x_307 : obj := ctor_0[EStateM.Result.ok] x_1 x_271;
> ret x_307
943,945c1055,1058
< let x_280 : obj := ctor_3[Lean.Compiler.LCNF.Code.jmp] x_254 x_265;
< let x_281 : obj := ctor_0[EStateM.Result.ok] x_280 x_258;
< ret x_281
---
> let x_308 : obj := reset[2] x_1;
> let x_309 : obj := ctor_3[Lean.Compiler.LCNF.Code.jmp] x_267 x_286;
> let x_310 : obj := reuse! x_308 in ctor_0[EStateM.Result.ok] x_309 x_271;
> ret x_310
947,950c1060,1063
< dec x_265;
< dec x_254;
< let x_282 : obj := ctor_0[EStateM.Result.ok] x_1 x_258;
< ret x_282
---
> dec x_286;
> dec x_267;
> let x_311 : obj := ctor_0[EStateM.Result.ok] x_1 x_271;
> ret x_311
952,968c1065,1095
< dec x_259;
< dec x_254;
< dec x_1;
< let x_283 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_5;
< let x_284 : obj := panic._at._private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp._spec_1 x_283;
< let x_285 : obj := ctor_0[EStateM.Result.ok] x_284 x_258;
< ret x_285;
< let x_287 : obj := proj[2] x_257;
< inc x_287;
< dec x_257;
< let x_288 : obj := Array.zip._rarg x_287 x_255;
< dec x_255;
< dec x_287;
< let x_289 : obj := Array.size ◾ x_288;
< let x_290 : obj := 0;
< let x_291 : u8 := Nat.decLt x_290 x_289;
< case x_291 : u8 of
---
> dec x_272;
> dec x_267;
> let x_312 : u8 := isShared x_1;
> case x_312 : u8 of
> Bool.false →
> let x_313 : obj := proj[1] x_1;
> dec x_313;
> let x_314 : obj := proj[0] x_1;
> dec x_314;
> let x_315 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_5;
> let x_316 : obj := panic._at._private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp._spec_1 x_315;
> setTag x_1 := 0;
> set x_1[1] := x_271;
> set x_1[0] := x_316;
> ret x_1
> Bool.true →
> dec x_1;
> let x_317 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_5;
> let x_318 : obj := panic._at._private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp._spec_1 x_317;
> let x_319 : obj := ctor_0[EStateM.Result.ok] x_318 x_271;
> ret x_319;
> let x_321 : obj := proj[2] x_270;
> inc x_321;
> dec x_270;
> let x_322 : obj := Array.zip._rarg x_321 x_268;
> dec x_268;
> dec x_321;
> let x_323 : obj := Array.size ◾ x_322;
> let x_324 : obj := 0;
> let x_325 : u8 := Nat.decLt x_324 x_323;
> case x_325 : u8 of
970,974c1097,1101
< dec x_289;
< dec x_288;
< dec x_256;
< let x_292 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
< jmp block_286 x_292
---
> dec x_323;
> dec x_322;
> dec x_269;
> let x_326 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
> jmp block_320 x_326
976,977c1103,1104
< let x_293 : u8 := Nat.decLe x_289 x_289;
< case x_293 : u8 of
---
> let x_327 : u8 := Nat.decLe x_323 x_323;
> case x_327 : u8 of
979,983c1106,1110
< dec x_289;
< dec x_288;
< dec x_256;
< let x_294 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
< jmp block_286 x_294
---
> dec x_323;
> dec x_322;
> dec x_269;
> let x_328 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
> jmp block_320 x_328
985,994c1112,1121
< let x_295 : usize := 0;
< let x_296 : usize := USize.ofNat x_289;
< dec x_289;
< let x_297 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
< let x_298 : obj := Array.foldlMUnsafe.fold._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_4 x_256 x_288 x_295 x_296 x_297;
< dec x_288;
< dec x_256;
< jmp block_286 x_298;
< inc x_254;
< let x_300 : obj := Lean.Compiler.LCNF.getFunDecl x_254 x_3 x_4 x_5 x_6 x_7;
---
> let x_329 : usize := 0;
> let x_330 : usize := USize.ofNat x_323;
> dec x_323;
> let x_331 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._closed_1;
> let x_332 : obj := Array.foldlMUnsafe.fold._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_4 x_269 x_322 x_329 x_330 x_331;
> dec x_322;
> dec x_269;
> jmp block_320 x_332;
> inc x_267;
> let x_334 : obj := Lean.Compiler.LCNF.getFunDecl x_267 x_3 x_4 x_5 x_6 x_7;
999c1126
< let x_301 : obj := Lean.RBNode.find._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goAnalyze._spec_1 x_2 x_254;
---
> let x_335 : obj := Lean.RBNode.find._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goAnalyze._spec_1 x_2 x_267;
1001c1128
< case x_301 : obj of
---
> case x_335 : obj of
1003c1130
< case x_300 : obj of
---
> case x_334 : obj of
1005,1012c1132,1139
< let x_302 : obj := proj[0] x_300;
< inc x_302;
< let x_303 : obj := proj[1] x_300;
< inc x_303;
< dec x_300;
< let x_304 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.isInJpScope._closed_3;
< let x_305 : obj := panic._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_5 x_304;
< jmp block_299 x_305 x_302 x_303
---
> let x_336 : obj := proj[0] x_334;
> inc x_336;
> let x_337 : obj := proj[1] x_334;
> inc x_337;
> dec x_334;
> let x_338 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.isInJpScope._closed_3;
> let x_339 : obj := panic._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_5 x_338;
> jmp block_333 x_339 x_336 x_337
1014,1015c1141,1142
< dec x_255;
< dec x_254;
---
> dec x_268;
> dec x_267;
1017,1018c1144,1145
< let x_306 : u8 := isShared x_300;
< case x_306 : u8 of
---
> let x_340 : u8 := isShared x_334;
> case x_340 : u8 of
1020c1147
< ret x_300
---
> ret x_334
1022,1028c1149,1155
< let x_307 : obj := proj[0] x_300;
< let x_308 : obj := proj[1] x_300;
< inc x_308;
< inc x_307;
< dec x_300;
< let x_309 : obj := ctor_1[EStateM.Result.error] x_307 x_308;
< ret x_309
---
> let x_341 : obj := proj[0] x_334;
> let x_342 : obj := proj[1] x_334;
> inc x_342;
> inc x_341;
> dec x_334;
> let x_343 : obj := ctor_1[EStateM.Result.error] x_341 x_342;
> ret x_343
1030c1157
< case x_300 : obj of
---
> case x_334 : obj of
1032,1040c1159,1167
< let x_310 : obj := proj[0] x_301;
< inc x_310;
< dec x_301;
< let x_311 : obj := proj[0] x_300;
< inc x_311;
< let x_312 : obj := proj[1] x_300;
< inc x_312;
< dec x_300;
< jmp block_299 x_310 x_311 x_312
---
> let x_344 : obj := proj[0] x_335;
> inc x_344;
> dec x_335;
> let x_345 : obj := proj[0] x_334;
> inc x_345;
> let x_346 : obj := proj[1] x_334;
> inc x_346;
> dec x_334;
> jmp block_333 x_344 x_345 x_346
1042,1044c1169,1171
< dec x_301;
< dec x_255;
< dec x_254;
---
> dec x_335;
> dec x_268;
> dec x_267;
1046,1047c1173,1174
< let x_313 : u8 := isShared x_300;
< case x_313 : u8 of
---
> let x_347 : u8 := isShared x_334;
> case x_347 : u8 of
1049c1176
< ret x_300
---
> ret x_334
1051,1057c1178,1184
< let x_314 : obj := proj[0] x_300;
< let x_315 : obj := proj[1] x_300;
< inc x_315;
< inc x_314;
< dec x_300;
< let x_316 : obj := ctor_1[EStateM.Result.error] x_314 x_315;
< ret x_316
---
> let x_348 : obj := proj[0] x_334;
> let x_349 : obj := proj[1] x_334;
> inc x_349;
> inc x_348;
> dec x_334;
> let x_350 : obj := ctor_1[EStateM.Result.error] x_348 x_349;
> ret x_350
1059,1062c1186,1189
< let x_317 : obj := proj[0] x_1;
< inc x_317;
< let x_318 : u8 := isShared x_317;
< case x_318 : u8 of
---
> let x_351 : obj := proj[0] x_1;
> inc x_351;
> let x_352 : u8 := isShared x_351;
> case x_352 : u8 of
1064,1074c1191,1201
< let x_319 : obj := proj[0] x_317;
< let x_320 : obj := proj[1] x_317;
< let x_321 : obj := proj[2] x_317;
< let x_322 : obj := proj[3] x_317;
< let x_323 : obj := Array.size ◾ x_322;
< let x_324 : usize := USize.ofNat x_323;
< dec x_323;
< let x_325 : usize := 0;
< inc x_322;
< let x_326 : obj := Array.mapMUnsafe.map._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_7 x_324 x_325 x_322 x_2 x_3 x_4 x_5 x_6 x_7;
< case x_326 : obj of
---
> let x_353 : obj := proj[0] x_351;
> let x_354 : obj := proj[1] x_351;
> let x_355 : obj := proj[2] x_351;
> let x_356 : obj := proj[3] x_351;
> let x_357 : obj := Array.size ◾ x_356;
> let x_358 : usize := USize.ofNat x_357;
> dec x_357;
> let x_359 : usize := 0;
> inc x_356;
> let x_360 : obj := Array.mapMUnsafe.map._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_7 x_358 x_359 x_356 x_2 x_3 x_4 x_5 x_6 x_7;
> case x_360 : obj of
1076,1077c1203,1204
< let x_327 : u8 := isShared x_326;
< case x_327 : u8 of
---
> let x_361 : u8 := isShared x_360;
> case x_361 : u8 of
1079,1084c1206,1211
< let x_328 : obj := proj[0] x_326;
< let x_329 : usize := ptrAddrUnsafe ◾ x_322;
< dec x_322;
< let x_330 : usize := ptrAddrUnsafe ◾ x_328;
< let x_331 : u8 := USize.decEq x_329 x_330;
< case x_331 : u8 of
---
> let x_362 : obj := proj[0] x_360;
> let x_363 : usize := ptrAddrUnsafe ◾ x_356;
> dec x_356;
> let x_364 : usize := ptrAddrUnsafe ◾ x_362;
> let x_365 : u8 := USize.decEq x_363 x_364;
> case x_365 : u8 of
1086,1087c1213,1214
< let x_332 : u8 := isShared x_1;
< case x_332 : u8 of
---
> let x_366 : u8 := isShared x_1;
> case x_366 : u8 of
1089,1093c1216,1220
< let x_333 : obj := proj[0] x_1;
< dec x_333;
< set x_317[3] := x_328;
< set x_326[0] := x_1;
< ret x_326
---
> let x_367 : obj := proj[0] x_1;
> dec x_367;
> set x_351[3] := x_362;
> set x_360[0] := x_1;
> ret x_360
1096,1099c1223,1226
< set x_317[3] := x_328;
< let x_334 : obj := ctor_4[Lean.Compiler.LCNF.Code.cases] x_317;
< set x_326[0] := x_334;
< ret x_326
---
> set x_351[3] := x_362;
> let x_368 : obj := ctor_4[Lean.Compiler.LCNF.Code.cases] x_351;
> set x_360[0] := x_368;
> ret x_360
1101,1103c1228,1230
< let x_335 : usize := ptrAddrUnsafe ◾ x_320;
< let x_336 : u8 := USize.decEq x_335 x_335;
< case x_336 : u8 of
---
> let x_369 : usize := ptrAddrUnsafe ◾ x_354;
> let x_370 : u8 := USize.decEq x_369 x_369;
> case x_370 : u8 of
1105,1106c1232,1233
< let x_337 : u8 := isShared x_1;
< case x_337 : u8 of
---
> let x_371 : u8 := isShared x_1;
> case x_371 : u8 of
1108,1112c1235,1239
< let x_338 : obj := proj[0] x_1;
< dec x_338;
< set x_317[3] := x_328;
< set x_326[0] := x_1;
< ret x_326
---
> let x_372 : obj := proj[0] x_1;
> dec x_372;
> set x_351[3] := x_362;
> set x_360[0] := x_1;
> ret x_360
1115,1118c1242,1245
< set x_317[3] := x_328;
< let x_339 : obj := ctor_4[Lean.Compiler.LCNF.Code.cases] x_317;
< set x_326[0] := x_339;
< ret x_326
---
> set x_351[3] := x_362;
> let x_373 : obj := ctor_4[Lean.Compiler.LCNF.Code.cases] x_351;
> set x_360[0] := x_373;
> ret x_360
1120,1121c1247,1248
< let x_340 : u8 := Lean.Name.beq x_321 x_321;
< case x_340 : u8 of
---
> let x_374 : u8 := Lean.Name.beq x_355 x_355;
> case x_374 : u8 of
1123,1124c1250,1251
< let x_341 : u8 := isShared x_1;
< case x_341 : u8 of
---
> let x_375 : u8 := isShared x_1;
> case x_375 : u8 of
1126,1130c1253,1257
< let x_342 : obj := proj[0] x_1;
< dec x_342;
< set x_317[3] := x_328;
< set x_326[0] := x_1;
< ret x_326
---
> let x_376 : obj := proj[0] x_1;
> dec x_376;
> set x_351[3] := x_362;
> set x_360[0] := x_1;
> ret x_360
1133,1136c1260,1263
< set x_317[3] := x_328;
< let x_343 : obj := ctor_4[Lean.Compiler.LCNF.Code.cases] x_317;
< set x_326[0] := x_343;
< ret x_326
---
> set x_351[3] := x_362;
> let x_377 : obj := ctor_4[Lean.Compiler.LCNF.Code.cases] x_351;
> set x_360[0] := x_377;
> ret x_360
1138,1144c1265,1271
< dec x_328;
< del x_317;
< dec x_321;
< dec x_320;
< dec x_319;
< set x_326[0] := x_1;
< ret x_326
---
> dec x_362;
> del x_351;
> dec x_355;
> dec x_354;
> dec x_353;
> set x_360[0] := x_1;
> ret x_360
1146,1155c1273,1282
< let x_344 : obj := proj[0] x_326;
< let x_345 : obj := proj[1] x_326;
< inc x_345;
< inc x_344;
< dec x_326;
< let x_346 : usize := ptrAddrUnsafe ◾ x_322;
< dec x_322;
< let x_347 : usize := ptrAddrUnsafe ◾ x_344;
< let x_348 : u8 := USize.decEq x_346 x_347;
< case x_348 : u8 of
---
> let x_378 : obj := proj[0] x_360;
> let x_379 : obj := proj[1] x_360;
> inc x_379;
> inc x_378;
> dec x_360;
> let x_380 : usize := ptrAddrUnsafe ◾ x_356;
> dec x_356;
> let x_381 : usize := ptrAddrUnsafe ◾ x_378;
> let x_382 : u8 := USize.decEq x_380 x_381;
> case x_382 : u8 of
1157,1161c1284,1288
< let x_349 : obj := reset[1] x_1;
< set x_317[3] := x_344;
< let x_350 : obj := reuse x_349 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_317;
< let x_351 : obj := ctor_0[EStateM.Result.ok] x_350 x_345;
< ret x_351
---
> let x_383 : obj := reset[1] x_1;
> set x_351[3] := x_378;
> let x_384 : obj := reuse x_383 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_351;
> let x_385 : obj := ctor_0[EStateM.Result.ok] x_384 x_379;
> ret x_385
1163,1165c1290,1292
< let x_352 : usize := ptrAddrUnsafe ◾ x_320;
< let x_353 : u8 := USize.decEq x_352 x_352;
< case x_353 : u8 of
---
> let x_386 : usize := ptrAddrUnsafe ◾ x_354;
> let x_387 : u8 := USize.decEq x_386 x_386;
> case x_387 : u8 of
1167,1171c1294,1298
< let x_354 : obj := reset[1] x_1;
< set x_317[3] := x_344;
< let x_355 : obj := reuse x_354 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_317;
< let x_356 : obj := ctor_0[EStateM.Result.ok] x_355 x_345;
< ret x_356
---
> let x_388 : obj := reset[1] x_1;
> set x_351[3] := x_378;
> let x_389 : obj := reuse x_388 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_351;
> let x_390 : obj := ctor_0[EStateM.Result.ok] x_389 x_379;
> ret x_390
1173,1174c1300,1301
< let x_357 : u8 := Lean.Name.beq x_321 x_321;
< case x_357 : u8 of
---
> let x_391 : u8 := Lean.Name.beq x_355 x_355;
> case x_391 : u8 of
1176,1180c1303,1307
< let x_358 : obj := reset[1] x_1;
< set x_317[3] := x_344;
< let x_359 : obj := reuse x_358 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_317;
< let x_360 : obj := ctor_0[EStateM.Result.ok] x_359 x_345;
< ret x_360
---
> let x_392 : obj := reset[1] x_1;
> set x_351[3] := x_378;
> let x_393 : obj := reuse x_392 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_351;
> let x_394 : obj := ctor_0[EStateM.Result.ok] x_393 x_379;
> ret x_394
1182,1188c1309,1315
< dec x_344;
< del x_317;
< dec x_321;
< dec x_320;
< dec x_319;
< let x_361 : obj := ctor_0[EStateM.Result.ok] x_1 x_345;
< ret x_361
---
> dec x_378;
> del x_351;
> dec x_355;
> dec x_354;
> dec x_353;
> let x_395 : obj := ctor_0[EStateM.Result.ok] x_1 x_379;
> ret x_395
1190,1194c1317,1321
< del x_317;
< dec x_322;
< dec x_321;
< dec x_320;
< dec x_319;
---
> del x_351;
> dec x_356;
> dec x_355;
> dec x_354;
> dec x_353;
1196,1197c1323,1324
< let x_362 : u8 := isShared x_326;
< case x_362 : u8 of
---
> let x_396 : u8 := isShared x_360;
> case x_396 : u8 of
1199c1326
< ret x_326
---
> ret x_360
1201,1207c1328,1334
< let x_363 : obj := proj[0] x_326;
< let x_364 : obj := proj[1] x_326;
< inc x_364;
< inc x_363;
< dec x_326;
< let x_365 : obj := ctor_1[EStateM.Result.error] x_363 x_364;
< ret x_365
---
> let x_397 : obj := proj[0] x_360;
> let x_398 : obj := proj[1] x_360;
> inc x_398;
> inc x_397;
> dec x_360;
> let x_399 : obj := ctor_1[EStateM.Result.error] x_397 x_398;
> ret x_399
1209,1224c1336,1351
< let x_366 : obj := proj[0] x_317;
< let x_367 : obj := proj[1] x_317;
< let x_368 : obj := proj[2] x_317;
< let x_369 : obj := proj[3] x_317;
< inc x_369;
< inc x_368;
< inc x_367;
< inc x_366;
< dec x_317;
< let x_370 : obj := Array.size ◾ x_369;
< let x_371 : usize := USize.ofNat x_370;
< dec x_370;
< let x_372 : usize := 0;
< inc x_369;
< let x_373 : obj := Array.mapMUnsafe.map._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_7 x_371 x_372 x_369 x_2 x_3 x_4 x_5 x_6 x_7;
< case x_373 : obj of
---
> let x_400 : obj := proj[0] x_351;
> let x_401 : obj := proj[1] x_351;
> let x_402 : obj := proj[2] x_351;
> let x_403 : obj := proj[3] x_351;
> inc x_403;
> inc x_402;
> inc x_401;
> inc x_400;
> dec x_351;
> let x_404 : obj := Array.size ◾ x_403;
> let x_405 : usize := USize.ofNat x_404;
> dec x_404;
> let x_406 : usize := 0;
> inc x_403;
> let x_407 : obj := Array.mapMUnsafe.map._at.Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce._spec_7 x_405 x_406 x_403 x_2 x_3 x_4 x_5 x_6 x_7;
> case x_407 : obj of
1226,1235c1353,1362
< let x_374 : obj := proj[0] x_373;
< inc x_374;
< let x_375 : obj := proj[1] x_373;
< inc x_375;
< let x_376 : obj := reset[2] x_373;
< let x_377 : usize := ptrAddrUnsafe ◾ x_369;
< dec x_369;
< let x_378 : usize := ptrAddrUnsafe ◾ x_374;
< let x_379 : u8 := USize.decEq x_377 x_378;
< case x_379 : u8 of
---
> let x_408 : obj := proj[0] x_407;
> inc x_408;
> let x_409 : obj := proj[1] x_407;
> inc x_409;
> let x_410 : obj := reset[2] x_407;
> let x_411 : usize := ptrAddrUnsafe ◾ x_403;
> dec x_403;
> let x_412 : usize := ptrAddrUnsafe ◾ x_408;
> let x_413 : u8 := USize.decEq x_411 x_412;
> case x_413 : u8 of
1237,1241c1364,1368
< let x_380 : obj := reset[1] x_1;
< let x_381 : obj := ctor_0[Lean.Compiler.LCNF.CasesCore.mk] x_366 x_367 x_368 x_374;
< let x_382 : obj := reuse x_380 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_381;
< let x_383 : obj := reuse x_376 in ctor_0[EStateM.Result.ok] x_382 x_375;
< ret x_383
---
> let x_414 : obj := reset[1] x_1;
> let x_415 : obj := ctor_0[Lean.Compiler.LCNF.CasesCore.mk] x_400 x_401 x_402 x_408;
> let x_416 : obj := reuse x_414 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_415;
> let x_417 : obj := reuse x_410 in ctor_0[EStateM.Result.ok] x_416 x_409;
> ret x_417
1243,1245c1370,1372
< let x_384 : usize := ptrAddrUnsafe ◾ x_367;
< let x_385 : u8 := USize.decEq x_384 x_384;
< case x_385 : u8 of
---
> let x_418 : usize := ptrAddrUnsafe ◾ x_401;
> let x_419 : u8 := USize.decEq x_418 x_418;
> case x_419 : u8 of
1247,1251c1374,1378
< let x_386 : obj := reset[1] x_1;
< let x_387 : obj := ctor_0[Lean.Compiler.LCNF.CasesCore.mk] x_366 x_367 x_368 x_374;
< let x_388 : obj := reuse x_386 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_387;
< let x_389 : obj := reuse x_376 in ctor_0[EStateM.Result.ok] x_388 x_375;
< ret x_389
---
> let x_420 : obj := reset[1] x_1;
> let x_421 : obj := ctor_0[Lean.Compiler.LCNF.CasesCore.mk] x_400 x_401 x_402 x_408;
> let x_422 : obj := reuse x_420 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_421;
> let x_423 : obj := reuse x_410 in ctor_0[EStateM.Result.ok] x_422 x_409;
> ret x_423
1253,1254c1380,1381
< let x_390 : u8 := Lean.Name.beq x_368 x_368;
< case x_390 : u8 of
---
> let x_424 : u8 := Lean.Name.beq x_402 x_402;
> case x_424 : u8 of
1256,1260c1383,1387
< let x_391 : obj := reset[1] x_1;
< let x_392 : obj := ctor_0[Lean.Compiler.LCNF.CasesCore.mk] x_366 x_367 x_368 x_374;
< let x_393 : obj := reuse x_391 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_392;
< let x_394 : obj := reuse x_376 in ctor_0[EStateM.Result.ok] x_393 x_375;
< ret x_394
---
> let x_425 : obj := reset[1] x_1;
> let x_426 : obj := ctor_0[Lean.Compiler.LCNF.CasesCore.mk] x_400 x_401 x_402 x_408;
> let x_427 : obj := reuse x_425 in ctor_4[Lean.Compiler.LCNF.Code.cases] x_426;
> let x_428 : obj := reuse x_410 in ctor_0[EStateM.Result.ok] x_427 x_409;
> ret x_428
1262,1267c1389,1394
< dec x_374;
< dec x_368;
< dec x_367;
< dec x_366;
< let x_395 : obj := reuse x_376 in ctor_0[EStateM.Result.ok] x_1 x_375;
< ret x_395
---
> dec x_408;
> dec x_402;
> dec x_401;
> dec x_400;
> let x_429 : obj := reuse x_410 in ctor_0[EStateM.Result.ok] x_1 x_409;
> ret x_429
1269,1272c1396,1399
< dec x_369;
< dec x_368;
< dec x_367;
< dec x_366;
---
> dec x_403;
> dec x_402;
> dec x_401;
> dec x_400;
1274,1280c1401,1407
< let x_396 : obj := proj[0] x_373;
< inc x_396;
< let x_397 : obj := proj[1] x_373;
< inc x_397;
< let x_398 : obj := reset[2] x_373;
< let x_399 : obj := reuse x_398 in ctor_1[EStateM.Result.error] x_396 x_397;
< ret x_399
---
> let x_430 : obj := proj[0] x_407;
> inc x_430;
> let x_431 : obj := proj[1] x_407;
> inc x_431;
> let x_432 : obj := reset[2] x_407;
> let x_433 : obj := reuse x_432 in ctor_1[EStateM.Result.error] x_430 x_431;
> ret x_433
1287,1288c1414,1415
< let x_400 : obj := ctor_0[EStateM.Result.ok] x_1 x_7;
< ret x_400
---
> let x_434 : obj := ctor_0[EStateM.Result.ok] x_1 x_7;
> ret x_434
Raw
miscompile.lean
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.LCNF.PullFunDecls
import Lean.Compiler.LCNF.FVarUtil
import Lean.Compiler.LCNF.ScopeM
import Lean.Compiler.LCNF.InferType
namespace Lean.Compiler.LCNF
namespace JoinPointFinder
open ScopeM
/--
Info about a join point candidate (a `fun` declaration) during the find phase.
-/
structure CandidateInfo where
/--
The arity of the candidate
-/
arity : Nat
/--
The set of candidates that rely on this candidate to be a join point.
For a more detailed explanation see the documentation of `find`
-/
associated : HashSet FVarId
deriving Inhabited
/--
The state for the join point candidate finder.
-/
structure FindState where
/--
All current join point candidates accessible by their `FVarId`.
-/
candidates : HashMap FVarId CandidateInfo := .empty
/--
The `FVarId`s of all `fun` declarations that were declared within the
current `fun`.
-/
scope : HashSet FVarId := .empty
abbrev ReplaceCtx := HashMap FVarId Name
abbrev FindM := ReaderT (Option FVarId) StateRefT FindState ScopeM
abbrev ReplaceM := ReaderT ReplaceCtx CompilerM
/--
Attempt to find a join point candidate by its `FVarId`.
-/
private def findCandidate? (fvarId : FVarId) : FindM (Option CandidateInfo) := do
return (← get).candidates.find? fvarId
/--
Erase a join point candidate as well as all the ones that depend on it
by its `FVarId`, no error is thrown is the candidate does not exist.
-/
private partial def eraseCandidate (fvarId : FVarId) : FindM Unit := do
if let some info ← findCandidate? fvarId then
modify (fun state => { state with candidates := state.candidates.erase fvarId })
info.associated.forM eraseCandidate
/--
Combinator for modifying the candidates in `FindM`.
-/
private def modifyCandidates (f : HashMap FVarId CandidateInfo → HashMap FVarId CandidateInfo) : FindM Unit :=
modify (fun state => {state with candidates := f state.candidates })
/--
Remove all join point candidates contained in `a`.
-/
private partial def removeCandidatesInArg (a : Arg) : FindM Unit := do
forFVarM eraseCandidate a
/--
Remove all join point candidates contained in `a`.
-/
private partial def removeCandidatesInLetValue (e : LetValue) : FindM Unit := do
forFVarM eraseCandidate e
/--
Add a new join point candidate to the state.
-/
private def addCandidate (fvarId : FVarId) (arity : Nat) : FindM Unit := do
let cinfo := { arity, associated := .empty }
modifyCandidates (fun cs => cs.insert fvarId cinfo )
/--
Add a new join point dependency from `src` to `dst`.
-/
private def addDependency (src : FVarId) (target : FVarId) : FindM Unit := do
if let some targetInfo ← findCandidate? target then
modifyCandidates (fun cs => cs.insert target { targetInfo with associated := targetInfo.associated.insert src })
else
eraseCandidate src
/--
Find all `fun` declarations that qualify as a join point, that is:
- are always fully applied
- are always called in tail position
Where a `fun` `f` is in tail position iff it is called as follows:
```
let res := f arg
res
```
The majority (if not all) tail calls will be brought into this form
by the simplifier pass.
Furthermore a `fun` disqualifies as a join point if turning it into a join
point would turn a call to it into an out of scope join point.
This can happen if we have something like:
```
def test (b : Bool) (x y : Nat) : Nat :=
fun myjp x => Nat.add x (Nat.add x x)
fun f y =>
let x := Nat.add y y
myjp x
fun f y =>
let x := Nat.mul y y
myjp x
cases b (f x) (g y)
```
`f` and `g` can be detected as a join point right away, however
`myjp` can only ever be detected as a join point after we have established
this. This is because otherwise the calls to `myjp` in `f` and `g` would
produce out of scope join point jumps.
-/
partial def find (decl : Decl) : CompilerM FindState := do
let (_, candidates) ← go decl.value |>.run none |>.run {} |>.run' {}
return candidates
where
go : Code → FindM Unit
| .let decl k => do
match k, decl.value with
| .return valId, .fvar fvarId args =>
args.forM removeCandidatesInArg
if let some candidateInfo ← findCandidate? fvarId then
-- Erase candidate that are not fully applied or applied outside of tail position
if valId != decl.fvarId || args.size != candidateInfo.arity then
eraseCandidate fvarId
-- Out of scope join point candidate handling
else if let some upperCandidate ← read then
if !(← isInScope fvarId) then
addDependency fvarId upperCandidate
else
eraseCandidate fvarId
| _, _ =>
removeCandidatesInLetValue decl.value
go k
| .fun decl k => do
withReader (fun _ => some decl.fvarId) do
withNewScope do
go decl.value
addCandidate decl.fvarId decl.getArity
addToScope decl.fvarId
go k
| .jp decl k => do
go decl.value
go k
| .jmp _ args => args.forM removeCandidatesInArg
| .return val => eraseCandidate val
| .cases c => do
eraseCandidate c.discr
c.alts.forM (·.forCodeM go)
| .unreach .. => return ()
/--
Replace all join point candidate `fun` declarations with `jp` ones
and all calls to them with `jmp`s.
-/
partial def replace (decl : Decl) (state : FindState) : CompilerM Decl := do
let mapper := fun acc cname _ => do return acc.insert cname (← mkFreshJpName)
let replaceCtx : ReplaceCtx ← state.candidates.foldM (init := .empty) mapper
let newValue ← go decl.value |>.run replaceCtx
return { decl with value := newValue }
where
go (code : Code) : ReplaceM Code := do
match code with
| .let decl k =>
match k, decl.value with
| .return valId, .fvar fvarId args =>
if valId == decl.fvarId then
if (← read).contains fvarId then
eraseLetDecl decl
return .jmp fvarId args
else
return code
else
return code
| _, _ => return Code.updateLet! code decl (← go k)
| .fun decl k =>
if let some replacement := (← read).find? decl.fvarId then
let newDecl := { decl with
binderName := replacement,
value := (← go decl.value)
}
modifyLCtx fun lctx => lctx.addFunDecl newDecl
return .jp newDecl (← go k)
else
let newDecl ← decl.updateValue (← go decl.value)
return Code.updateFun! code newDecl (← go k)
| .jp decl k =>
let newDecl ← decl.updateValue (← go decl.value)
return Code.updateFun! code newDecl (← go k)
| .cases cs =>
return Code.updateCases! code cs.resultType cs.discr (← cs.alts.mapM (·.mapCodeM go))
| .jmp .. | .return .. | .unreach .. =>
return code
end JoinPointFinder
namespace JoinPointContextExtender
open ScopeM
/--
The context managed by `ExtendM`.
-/
structure ExtendContext where
/--
The `FVarId` of the current join point if we are currently inside one.
-/
currentJp? : Option FVarId := none
/--
The list of valid candidates for extending the context. This will be
all `let` and `fun` declarations as well as all `jp` parameters up
until the last `fun` declaration in the tree.
-/
candidates : FVarIdSet := {}
/--
The state managed by `ExtendM`.
-/
structure ExtendState where
/--
A map from join point `FVarId`s to a respective map from free variables
to `Param`s. The free variables in this map are the once that the context
of said join point will be extended by by passing in the respective parameter.
-/
fvarMap : HashMap FVarId (HashMap FVarId Param) := {}
/--
The monad for the `extendJoinPointContext` pass.
-/
abbrev ExtendM := ReaderT ExtendContext StateRefT ExtendState ScopeM
/--
Replace a free variable if necessary, that is:
- It is in the list of candidates
- We are currently within a join point (if we are within a function there
cannot be a need to replace them since we dont extend their context)
- Said join point actually has a replacement parameter registered.
otherwise just return `fvar`.
-/
def replaceFVar (fvar : FVarId) : ExtendM FVarId := do
if (← read).candidates.contains fvar then
if let some currentJp := (← read).currentJp? then
if let some replacement := (← get).fvarMap.find! currentJp |>.find? fvar then
return replacement.fvarId
return fvar
/--
Add a new candidate to the current scope + to the list of candidates
if we are currently within a join point. Then execute `x`.
-/
def withNewCandidate (fvar : FVarId) (x : ExtendM α) : ExtendM α := do
addToScope fvar
if (← read).currentJp?.isSome then
withReader (fun ctx => { ctx with candidates := ctx.candidates.insert fvar }) do
x
else
x
/--
Same as `withNewCandidate` but with multiple `FVarId`s.
-/
def withNewCandidates (fvars : Array FVarId) (x : ExtendM α) : ExtendM α := do
if (← read).currentJp?.isSome then
let candidates := (← read).candidates
let folder (acc : FVarIdSet) (val : FVarId) := do
addToScope val
return acc.insert val
let newCandidates ← fvars.foldlM (init := candidates) folder
withReader (fun ctx => { ctx with candidates := newCandidates }) do
x
else
x
/--
Extend the context of the current join point (if we are within one)
by `fvar` if necessary.
This is necessary if:
- `fvar` is not in scope (that is, was declared outside of the current jp)
- we have not already extended the context by `fvar`
- the list of candidates contains `fvar`. This is because if we have something
like:
```
let x := ..
fun f a =>
jp j b =>
let y := x
y
```
There is no point in extending the context of `j` by `x` because we
cannot lift a join point outside of a local function declaration.
-/
def extendByIfNecessary (fvar : FVarId) : ExtendM Unit := do
if let some currentJp := (← read).currentJp? then
let mut translator := (← get).fvarMap.find! currentJp
let candidates := (← read).candidates
if !(← isInScope fvar) && !translator.contains fvar && candidates.contains fvar then
let typ ← getType fvar
let newParam ← mkAuxParam typ
translator := translator.insert fvar newParam
modify fun s => { s with fvarMap := s.fvarMap.insert currentJp translator }
/--
Merge the extended context of two join points if necessary. That is
if we have a structure such as:
```
jp j.1 ... =>
jp j.2 .. =>
...
...
```
And we are just done visiting `j.2` we want to extend the context of
`j.1` by all free variables that the context of `j.2` was extended by
as well because we need to drag these variables through at the call sites
of `j.2` in `j.1`.
-/
def mergeJpContextIfNecessary (jp : FVarId) : ExtendM Unit := do
if (← read).currentJp?.isSome then
let additionalArgs := (← get).fvarMap.find! jp |>.toArray
for (fvar, _) in additionalArgs do
extendByIfNecessary fvar
/--
We call this whenever we enter a new local function. It clears both the
current join point and the list of candidates since we can't lift join
points outside of functions as explained in `mergeJpContextIfNecessary`.
-/
def withNewFunScope (x : ExtendM α): ExtendM α := do
withReader (fun ctx => { ctx with currentJp? := none, candidates := {} }) do
withNewScope do
x
/--
We call this whenever we enter a new join point. It will set the current
join point and extend the list of candidates by all of the parameters of
the join point. This is so in the case of nested join points that refer
to parameters of the current one we extend the context of the nested
join points by said parameters.
-/
def withNewJpScope (decl : FunDecl) (x : ExtendM α): ExtendM α := do
withReader (fun ctx => { ctx with currentJp? := some decl.fvarId }) do
modify fun s => { s with fvarMap := s.fvarMap.insert decl.fvarId {} }
withNewScope do
withNewCandidates (decl.params.map (·.fvarId)) do
x
/--
We call this whenever we visit a new arm of a cases statement.
It will back up the current scope (since we are doing a case split
and want to continue with other arms afterwards) and add all of the
parameters of the match arm to the list of candidates.
-/
def withNewAltScope (alt : Alt) (x : ExtendM α) : ExtendM α := do
withBackTrackingScope do
withNewCandidates (alt.getParams.map (·.fvarId)) do
x
/--
Use all of the above functions to find free variables declared outside
of join points that said join points can be reasonaly extended by. Reasonable
meaning that in case the current join point is nested within a function
declaration we will not extend it by free variables declared before the
function declaration because we cannot lift join points outside of function
declarations.
All of this is done to eliminate dependencies of join points onto their
position within the code so we can pull them out as far as possible, hopefully
enabling new inlining possibilities in the next simplifier run.
-/
partial def extend (decl : Decl) : CompilerM Decl := do
let newValue ← go decl.value |>.run {} |>.run' {} |>.run' {}
let decl := { decl with value := newValue }
decl.pullFunDecls
where
goFVar (fvar : FVarId) : ExtendM FVarId := do
extendByIfNecessary fvar
replaceFVar fvar
go (code : Code) : ExtendM Code := do
match code with
| .let decl k =>
let decl ← decl.updateValue (← mapFVarM goFVar decl.value)
withNewCandidate decl.fvarId do
return Code.updateLet! code decl (← go k)
| .jp decl k =>
let decl ← withNewJpScope decl do
let value ← go decl.value
let additionalParams := (← get).fvarMap.find! decl.fvarId |>.toArray |>.map Prod.snd
let newType := additionalParams.foldr (init := decl.type) (fun val acc => .forallE val.binderName val.type acc .default)
decl.update newType (additionalParams ++ decl.params) value
mergeJpContextIfNecessary decl.fvarId
withNewCandidate decl.fvarId do
return Code.updateFun! code decl (← go k)
| .fun decl k =>
let decl ← withNewFunScope do
decl.updateValue (← go decl.value)
withNewCandidate decl.fvarId do
return Code.updateFun! code decl (← go k)
| .cases cs =>
extendByIfNecessary cs.discr
let discr ← replaceFVar cs.discr
let visitor := fun alt => do
withNewAltScope alt do
alt.mapCodeM go
let alts ← cs.alts.mapM visitor
return Code.updateCases! code cs.resultType discr alts
| .jmp fn args =>
let mut newArgs ← args.mapM (mapFVarM goFVar)
let additionalArgs := (← get).fvarMap.find! fn |>.toArray |>.map Prod.fst
if let some _currentJp := (← read).currentJp? then
let f := fun arg => do
return .fvar (← goFVar arg)
newArgs := (←additionalArgs.mapM f) ++ newArgs
else
newArgs := (additionalArgs.map .fvar) ++ newArgs
return Code.updateJmp! code fn newArgs
| .return var =>
extendByIfNecessary var
return Code.updateReturn! code (← replaceFVar var)
| .unreach .. => return code
end JoinPointContextExtender
namespace JoinPointCommonArgs
/--
Context for `ReduceAnalysisM`.
-/
structure AnalysisCtx where
/--
The variables that are in scope at the time of the definition of
the join point.
-/
jpScopes : FVarIdMap FVarIdSet := {}
/--
State for `ReduceAnalysisM`.
-/
structure AnalysisState where
/--
A map, that for each join point id contains a map from all (so far)
duplicated argument ids to the respective duplicate value
-/
jpJmpArgs : FVarIdMap FVarSubst := {}
abbrev ReduceAnalysisM := ReaderT AnalysisCtx StateRefT AnalysisState ScopeM
abbrev ReduceActionM := ReaderT AnalysisState CompilerM
def isInJpScope (jp : FVarId) (var : FVarId) : ReduceAnalysisM Bool := do
return (← read).jpScopes.find! jp |>.contains var
open ScopeM
set_option trace.compiler.ir.result true in
partial def reduce (decl : Decl) : CompilerM Decl := do
let (_, analysis) ← goAnalyze decl.value |>.run {} |>.run {} |>.run' {}
let newValue ← goReduce decl.value |>.run analysis
return { decl with value := newValue }
where
goAnalyzeFunDecl (fn : FunDecl) : ReduceAnalysisM Unit := do
withNewScope do
fn.params.forM (addToScope ·.fvarId)
goAnalyze fn.value
goAnalyze (code : Code) : ReduceAnalysisM Unit := do
match code with
| .let decl k =>
addToScope decl.fvarId
goAnalyze k
| .jp decl k =>
goAnalyzeFunDecl decl
let scope ← getScope
withReader (fun ctx => { ctx with jpScopes := ctx.jpScopes.insert decl.fvarId scope }) do
addToScope decl.fvarId
goAnalyze k
| .fun decl k =>
goAnalyzeFunDecl decl
addToScope decl.fvarId
goAnalyze k
| .cases cs =>
let visitor alt := do
withNewScope do
alt.getParams.forM (addToScope ·.fvarId)
goAnalyze alt.getCode
cs.alts.forM visitor
| .jmp fn args =>
let decl ← getFunDecl fn
if let some knownArgs := (← get).jpJmpArgs.find? fn then
let mut newArgs := knownArgs
for (param, arg) in decl.params.zip args do
if let some knownVal := newArgs.find? param.fvarId then
if arg.toExpr != knownVal then
newArgs := newArgs.erase param.fvarId
modify fun s => { s with jpJmpArgs := s.jpJmpArgs.insert fn newArgs }
else
let folder := fun acc (param, arg) => do
if (← allFVarM (isInJpScope fn) arg) then
return acc.insert param.fvarId arg.toExpr
else
return acc
let interestingArgs ← decl.params.zip args |>.foldlM (init := {}) folder
modify fun s => { s with jpJmpArgs := s.jpJmpArgs.insert fn interestingArgs }
| .return .. | .unreach .. => return ()
goReduce (code : Code) : ReduceActionM Code := do
match code with
| .jp decl k =>
if let some reducibleArgs := (← read).jpJmpArgs.find? decl.fvarId then
let filter param := do
let erasable := reducibleArgs.contains param.fvarId
if erasable then
eraseParam param
return !erasable
let newParams ← decl.params.filterM filter
let mut newValue ← goReduce decl.value
newValue ← replaceFVars newValue reducibleArgs false
let newType ←
if newParams.size != decl.params.size then
mkForallParams newParams (← newValue.inferType)
else
pure decl.type
let k ← goReduce k
let decl ← decl.update newType newParams newValue
return Code.updateFun! code decl k
else
return Code.updateFun! code decl (← goReduce k)
| .jmp fn args =>
let reducibleArgs := (← read).jpJmpArgs.find! fn
let decl ← getFunDecl fn
let newParams := decl.params.zip args
|>.filter (!reducibleArgs.contains ·.fst.fvarId)
|>.map Prod.snd
return Code.updateJmp! code fn newParams
| .let decl k =>
return Code.updateLet! code decl (← goReduce k)
| .fun decl k =>
let decl ← decl.updateValue (← goReduce decl.value)
return Code.updateFun! code decl (← goReduce k)
| .cases cs =>
let alts ← cs.alts.mapM (·.mapCodeM goReduce)
return Code.updateCases! code cs.resultType cs.discr alts
| .return .. | .unreach .. => return code
end JoinPointCommonArgs
end Lean.Compiler.LCNF
Raw
out-enable-all
def Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) (x_5 : obj) (x_6 : obj) (x_7 : obj) : obj :=
case x_1 : obj of
Lean.Compiler.LCNF.Code.let →
let x_8 : obj := proj[0] x_1;
inc x_8;
let x_9 : obj := proj[1] x_1;
inc x_9;
inc x_9;
let x_10 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_9 x_2 x_3 x_4 x_5 x_6 x_7;
case x_10 : obj of
EStateM.Result.ok →
let x_11 : u8 := isShared x_10;
case x_11 : u8 of
Bool.false →
let x_12 : obj := proj[0] x_10;
let x_13 : obj := proj[1] x_10;
let x_14 : usize := ptrAddrUnsafe ◾ x_9;
dec x_9;
let x_15 : usize := ptrAddrUnsafe ◾ x_12;
let x_16 : u8 := USize.decEq x_14 x_15;
case x_16 : u8 of
Bool.false →
let x_17 : u8 := isShared x_1;
case x_17 : u8 of
Bool.false →
let x_18 : obj := proj[1] x_1;
dec x_18;
let x_19 : obj := proj[0] x_1;
dec x_19;
set x_10[1] := x_12;
set x_10[0] := x_8;
set x_1[1] := x_13;
set x_1[0] := x_10;
ret x_1
Bool.true →
dec x_1;
set x_10[1] := x_12;
set x_10[0] := x_8;
let x_20 : obj := ctor_0[EStateM.Result.ok] x_10 x_13;
ret x_20
Bool.true →
let x_21 : usize := ptrAddrUnsafe ◾ x_8;
let x_22 : u8 := USize.decEq x_21 x_21;
case x_22 : u8 of
Bool.false →
let x_23 : u8 := isShared x_1;
case x_23 : u8 of
Bool.false →
let x_24 : obj := proj[1] x_1;
dec x_24;
let x_25 : obj := proj[0] x_1;
dec x_25;
set x_10[1] := x_12;
set x_10[0] := x_8;
set x_1[1] := x_13;
set x_1[0] := x_10;
ret x_1 -- out0
Bool.true →
dec x_1;
set x_10[1] := x_12;
set x_10[0] := x_8;
let x_26 : obj := ctor_0[EStateM.Result.ok] x_10 x_13;
ret x_26
Bool.true →
dec x_12;
dec x_8;
set x_10[0] := x_1;
ret x_10
Bool.true →
let x_27 : obj := proj[0] x_10;
let x_28 : obj := proj[1] x_10;
inc x_28;
inc x_27;
dec x_10;
let x_29 : usize := ptrAddrUnsafe ◾ x_9;
dec x_9;
let x_30 : usize := ptrAddrUnsafe ◾ x_27;
let x_31 : u8 := USize.decEq x_29 x_30;
case x_31 : u8 of
Bool.false →
let x_32 : obj := reset[2] x_1;
let x_33 : obj := ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_27;
let x_34 : obj := reuse x_32 in ctor_0[EStateM.Result.ok] x_33 x_28;
ret x_34
Bool.true →
let x_35 : usize := ptrAddrUnsafe ◾ x_8;
let x_36 : u8 := USize.decEq x_35 x_35;
case x_36 : u8 of
Bool.false →
let x_37 : obj := reset[2] x_1;
let x_38 : obj := ctor_0[Lean.Compiler.LCNF.Code.let] x_8 x_27;
let x_39 : obj := reuse x_37 in ctor_0[EStateM.Result.ok] x_38 x_28;
ret x_39
Bool.true →
dec x_27;
dec x_8;
let x_40 : obj := ctor_0[EStateM.Result.ok] x_1 x_28;
ret x_40
EStateM.Result.error →
dec x_9;
dec x_8;
dec x_1;
let x_41 : u8 := isShared x_10;
case x_41 : u8 of
Bool.false →
ret x_10
Bool.true →
let x_42 : obj := proj[0] x_10;
let x_43 : obj := proj[1] x_10;
inc x_43;
inc x_42;
dec x_10;
let x_44 : obj := ctor_1[EStateM.Result.error] x_42 x_43;
ret x_44
Lean.Compiler.LCNF.Code.fun →
let x_45 : obj := proj[0] x_1;
inc x_45;
let x_46 : obj := proj[1] x_1;
inc x_46;
let x_47 : obj := proj[4] x_45;
inc x_47;
inc x_6;
inc x_5;
inc x_4;
inc x_3;
inc x_2;
let x_48 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_47 x_2 x_3 x_4 x_5 x_6 x_7;
case x_48 : obj of
EStateM.Result.ok →
let x_49 : obj := proj[0] x_48;
inc x_49;
let x_50 : obj := proj[1] x_48;
inc x_50;
dec x_48;
let x_51 : obj := proj[3] x_45;
inc x_51;
let x_52 : obj := proj[2] x_45;
inc x_52;
inc x_45;
let x_53 : obj := _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.updateFunDeclImp x_45 x_51 x_52 x_49 x_3 x_4 x_5 x_6 x_50;
let x_54 : u8 := isShared x_53;
case x_54 : u8 of
Bool.false →
let x_55 : obj := proj[0] x_53;
let x_56 : obj := proj[1] x_53;
inc x_46;
let x_57 : obj := Lean.Compiler.LCNF.JoinPointCommonArgs.reduce.goReduce x_46 x_2 x_3 x_4 x_5 x_6 x_56;
case x_57 : obj of
EStateM.Result.ok →
let x_58 : u8 := isShared x_57;
case x_58 : u8 of
Bool.false →
let x_59 : obj := proj[0] x_57;
let x_60 : obj := proj[1] x_57;
let x_61 : usize := ptrAddrUnsafe ◾ x_46;
dec x_46;
let x_62 : usize := ptrAddrUnsafe ◾ x_59;
let x_63 : u8 := USize.decEq x_61 x_62;
case x_63 : u8 of
Bool.false →
dec x_45;
dec x_1;
setTag x_57 := 1;
set x_57[1] := x_59;
set x_57[0] := x_55;
set x_53[1] := x_60;
set x_53[0] := x_57;
ret x_53
Bool.true →
let x_64 : usize := ptrAddrUnsafe ◾ x_45;
dec x_45;
let x_65 : usize := ptrAddrUnsafe ◾ x_55;
let x_66 : u8 := USize.decEq x_64 x_65;
case x_66 : u8 of
Bool.false →
dec x_1;