Add some display logs

4 files changed, 684 insertions, 0 deletions

diff --git a/src/Specific/GF25519Reflective/Reified/AddDisplay.log b/src/Specific/GF25519Reflective/Reified/AddDisplay.log
new file mode 100644
index 000000000..156f0286e
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/AddDisplay.log
@@ -0,0 +1,45 @@
+raddW = 
+fun var : Syntax.base_type -> Type =>
+λ
+x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
+ x18 : var Syntax.TZ,
+Tbase Syntax.TZ x19 = x + x9;
+Tbase Syntax.TZ x20 = x0 + x10;
+Tbase Syntax.TZ x21 = x1 + x11;
+Tbase Syntax.TZ x22 = x2 + x12;
+Tbase Syntax.TZ x23 = x3 + x13;
+Tbase Syntax.TZ x24 = x4 + x14;
+Tbase Syntax.TZ x25 = x5 + x15;
+Tbase Syntax.TZ x26 = x6 + x16;
+Tbase Syntax.TZ x27 = x7 + x17;
+Tbase Syntax.TZ x28 = x8 + x18;
+(Return x19, Return x20, Return x21, Return x22, Return x23, 
+Return x24, Return x25, Return x26, Return x27, Return x28)
+     : forall var : Syntax.base_type -> Type,
+       expr Syntax.base_type Syntax.op
+         (Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ)
+
+Argument scope is [function_scope]
diff --git a/src/Specific/GF25519Reflective/Reified/AddJavaDisplay.log b/src/Specific/GF25519Reflective/Reified/AddJavaDisplay.log
new file mode 100644
index 000000000..156f0286e
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/AddJavaDisplay.log
@@ -0,0 +1,45 @@
+raddW = 
+fun var : Syntax.base_type -> Type =>
+λ
+x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
+ x18 : var Syntax.TZ,
+Tbase Syntax.TZ x19 = x + x9;
+Tbase Syntax.TZ x20 = x0 + x10;
+Tbase Syntax.TZ x21 = x1 + x11;
+Tbase Syntax.TZ x22 = x2 + x12;
+Tbase Syntax.TZ x23 = x3 + x13;
+Tbase Syntax.TZ x24 = x4 + x14;
+Tbase Syntax.TZ x25 = x5 + x15;
+Tbase Syntax.TZ x26 = x6 + x16;
+Tbase Syntax.TZ x27 = x7 + x17;
+Tbase Syntax.TZ x28 = x8 + x18;
+(Return x19, Return x20, Return x21, Return x22, Return x23, 
+Return x24, Return x25, Return x26, Return x27, Return x28)
+     : forall var : Syntax.base_type -> Type,
+       expr Syntax.base_type Syntax.op
+         (Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ)
+
+Argument scope is [function_scope]
diff --git a/src/Specific/GF25519Reflective/Reified/MulDisplay.log b/src/Specific/GF25519Reflective/Reified/MulDisplay.log
new file mode 100644
index 000000000..30f70a7a2
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/MulDisplay.log
@@ -0,0 +1,297 @@
+rmulW = 
+fun var : Syntax.base_type -> Type =>
+λ
+x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
+ x18 : var Syntax.TZ,
+Tbase Syntax.TZ x19 = x8 * x18;
+Tbase Syntax.TZ x20 = x17 * 0x2;
+Tbase Syntax.TZ x21 = x * x20;
+Tbase Syntax.TZ x22 = x0 * x16;
+Tbase Syntax.TZ x23 = x15 * 0x2;
+Tbase Syntax.TZ x24 = x1 * x23;
+Tbase Syntax.TZ x25 = x2 * x14;
+Tbase Syntax.TZ x26 = x13 * 0x2;
+Tbase Syntax.TZ x27 = x3 * x26;
+Tbase Syntax.TZ x28 = x4 * x12;
+Tbase Syntax.TZ x29 = x11 * 0x2;
+Tbase Syntax.TZ x30 = x5 * x29;
+Tbase Syntax.TZ x31 = x6 * x10;
+Tbase Syntax.TZ x32 = x9 * 0x2;
+Tbase Syntax.TZ x33 = x7 * x32;
+Tbase Syntax.TZ x34 = x31 + x33;
+Tbase Syntax.TZ x35 = x30 + x34;
+Tbase Syntax.TZ x36 = x28 + x35;
+Tbase Syntax.TZ x37 = x27 + x36;
+Tbase Syntax.TZ x38 = x25 + x37;
+Tbase Syntax.TZ x39 = x24 + x38;
+Tbase Syntax.TZ x40 = x22 + x39;
+Tbase Syntax.TZ x41 = x21 + x40;
+Tbase Syntax.TZ x42 = 0x13 * x41;
+Tbase Syntax.TZ x43 = x19 + x42;
+Tbase Syntax.TZ x44 = x43 >> 0x1a;
+Tbase Syntax.TZ x45 = x7 * x18;
+Tbase Syntax.TZ x46 = x8 * x17;
+Tbase Syntax.TZ x47 = x45 + x46;
+Tbase Syntax.TZ x48 = x * x16;
+Tbase Syntax.TZ x49 = x0 * x15;
+Tbase Syntax.TZ x50 = x1 * x14;
+Tbase Syntax.TZ x51 = x2 * x13;
+Tbase Syntax.TZ x52 = x3 * x12;
+Tbase Syntax.TZ x53 = x4 * x11;
+Tbase Syntax.TZ x54 = x5 * x10;
+Tbase Syntax.TZ x55 = x6 * x9;
+Tbase Syntax.TZ x56 = x54 + x55;
+Tbase Syntax.TZ x57 = x53 + x56;
+Tbase Syntax.TZ x58 = x52 + x57;
+Tbase Syntax.TZ x59 = x51 + x58;
+Tbase Syntax.TZ x60 = x50 + x59;
+Tbase Syntax.TZ x61 = x49 + x60;
+Tbase Syntax.TZ x62 = x48 + x61;
+Tbase Syntax.TZ x63 = 0x13 * x62;
+Tbase Syntax.TZ x64 = x47 + x63;
+Tbase Syntax.TZ x65 = x44 + x64;
+Tbase Syntax.TZ x66 = x65 >> 0x19;
+Tbase Syntax.TZ x67 = x6 * x18;
+Tbase Syntax.TZ x68 = x17 * 0x2;
+Tbase Syntax.TZ x69 = x7 * x68;
+Tbase Syntax.TZ x70 = x8 * x16;
+Tbase Syntax.TZ x71 = x69 + x70;
+Tbase Syntax.TZ x72 = x67 + x71;
+Tbase Syntax.TZ x73 = x15 * 0x2;
+Tbase Syntax.TZ x74 = x * x73;
+Tbase Syntax.TZ x75 = x0 * x14;
+Tbase Syntax.TZ x76 = x13 * 0x2;
+Tbase Syntax.TZ x77 = x1 * x76;
+Tbase Syntax.TZ x78 = x2 * x12;
+Tbase Syntax.TZ x79 = x11 * 0x2;
+Tbase Syntax.TZ x80 = x3 * x79;
+Tbase Syntax.TZ x81 = x4 * x10;
+Tbase Syntax.TZ x82 = x9 * 0x2;
+Tbase Syntax.TZ x83 = x5 * x82;
+Tbase Syntax.TZ x84 = x81 + x83;
+Tbase Syntax.TZ x85 = x80 + x84;
+Tbase Syntax.TZ x86 = x78 + x85;
+Tbase Syntax.TZ x87 = x77 + x86;
+Tbase Syntax.TZ x88 = x75 + x87;
+Tbase Syntax.TZ x89 = x74 + x88;
+Tbase Syntax.TZ x90 = 0x13 * x89;
+Tbase Syntax.TZ x91 = x72 + x90;
+Tbase Syntax.TZ x92 = x66 + x91;
+Tbase Syntax.TZ x93 = x92 >> 0x1a;
+Tbase Syntax.TZ x94 = x5 * x18;
+Tbase Syntax.TZ x95 = x6 * x17;
+Tbase Syntax.TZ x96 = x7 * x16;
+Tbase Syntax.TZ x97 = x8 * x15;
+Tbase Syntax.TZ x98 = x96 + x97;
+Tbase Syntax.TZ x99 = x95 + x98;
+Tbase Syntax.TZ x100 = x94 + x99;
+Tbase Syntax.TZ x101 = x * x14;
+Tbase Syntax.TZ x102 = x0 * x13;
+Tbase Syntax.TZ x103 = x1 * x12;
+Tbase Syntax.TZ x104 = x2 * x11;
+Tbase Syntax.TZ x105 = x3 * x10;
+Tbase Syntax.TZ x106 = x4 * x9;
+Tbase Syntax.TZ x107 = x105 + x106;
+Tbase Syntax.TZ x108 = x104 + x107;
+Tbase Syntax.TZ x109 = x103 + x108;
+Tbase Syntax.TZ x110 = x102 + x109;
+Tbase Syntax.TZ x111 = x101 + x110;
+Tbase Syntax.TZ x112 = 0x13 * x111;
+Tbase Syntax.TZ x113 = x100 + x112;
+Tbase Syntax.TZ x114 = x93 + x113;
+Tbase Syntax.TZ x115 = x114 >> 0x19;
+Tbase Syntax.TZ x116 = x4 * x18;
+Tbase Syntax.TZ x117 = x17 * 0x2;
+Tbase Syntax.TZ x118 = x5 * x117;
+Tbase Syntax.TZ x119 = x6 * x16;
+Tbase Syntax.TZ x120 = x15 * 0x2;
+Tbase Syntax.TZ x121 = x7 * x120;
+Tbase Syntax.TZ x122 = x8 * x14;
+Tbase Syntax.TZ x123 = x121 + x122;
+Tbase Syntax.TZ x124 = x119 + x123;
+Tbase Syntax.TZ x125 = x118 + x124;
+Tbase Syntax.TZ x126 = x116 + x125;
+Tbase Syntax.TZ x127 = x13 * 0x2;
+Tbase Syntax.TZ x128 = x * x127;
+Tbase Syntax.TZ x129 = x0 * x12;
+Tbase Syntax.TZ x130 = x11 * 0x2;
+Tbase Syntax.TZ x131 = x1 * x130;
+Tbase Syntax.TZ x132 = x2 * x10;
+Tbase Syntax.TZ x133 = x9 * 0x2;
+Tbase Syntax.TZ x134 = x3 * x133;
+Tbase Syntax.TZ x135 = x132 + x134;
+Tbase Syntax.TZ x136 = x131 + x135;
+Tbase Syntax.TZ x137 = x129 + x136;
+Tbase Syntax.TZ x138 = x128 + x137;
+Tbase Syntax.TZ x139 = 0x13 * x138;
+Tbase Syntax.TZ x140 = x126 + x139;
+Tbase Syntax.TZ x141 = x115 + x140;
+Tbase Syntax.TZ x142 = x141 >> 0x1a;
+Tbase Syntax.TZ x143 = x3 * x18;
+Tbase Syntax.TZ x144 = x4 * x17;
+Tbase Syntax.TZ x145 = x5 * x16;
+Tbase Syntax.TZ x146 = x6 * x15;
+Tbase Syntax.TZ x147 = x7 * x14;
+Tbase Syntax.TZ x148 = x8 * x13;
+Tbase Syntax.TZ x149 = x147 + x148;
+Tbase Syntax.TZ x150 = x146 + x149;
+Tbase Syntax.TZ x151 = x145 + x150;
+Tbase Syntax.TZ x152 = x144 + x151;
+Tbase Syntax.TZ x153 = x143 + x152;
+Tbase Syntax.TZ x154 = x * x12;
+Tbase Syntax.TZ x155 = x0 * x11;
+Tbase Syntax.TZ x156 = x1 * x10;
+Tbase Syntax.TZ x157 = x2 * x9;
+Tbase Syntax.TZ x158 = x156 + x157;
+Tbase Syntax.TZ x159 = x155 + x158;
+Tbase Syntax.TZ x160 = x154 + x159;
+Tbase Syntax.TZ x161 = 0x13 * x160;
+Tbase Syntax.TZ x162 = x153 + x161;
+Tbase Syntax.TZ x163 = x142 + x162;
+Tbase Syntax.TZ x164 = x163 >> 0x19;
+Tbase Syntax.TZ x165 = x2 * x18;
+Tbase Syntax.TZ x166 = x17 * 0x2;
+Tbase Syntax.TZ x167 = x3 * x166;
+Tbase Syntax.TZ x168 = x4 * x16;
+Tbase Syntax.TZ x169 = x15 * 0x2;
+Tbase Syntax.TZ x170 = x5 * x169;
+Tbase Syntax.TZ x171 = x6 * x14;
+Tbase Syntax.TZ x172 = x13 * 0x2;
+Tbase Syntax.TZ x173 = x7 * x172;
+Tbase Syntax.TZ x174 = x8 * x12;
+Tbase Syntax.TZ x175 = x173 + x174;
+Tbase Syntax.TZ x176 = x171 + x175;
+Tbase Syntax.TZ x177 = x170 + x176;
+Tbase Syntax.TZ x178 = x168 + x177;
+Tbase Syntax.TZ x179 = x167 + x178;
+Tbase Syntax.TZ x180 = x165 + x179;
+Tbase Syntax.TZ x181 = x11 * 0x2;
+Tbase Syntax.TZ x182 = x * x181;
+Tbase Syntax.TZ x183 = x0 * x10;
+Tbase Syntax.TZ x184 = x9 * 0x2;
+Tbase Syntax.TZ x185 = x1 * x184;
+Tbase Syntax.TZ x186 = x183 + x185;
+Tbase Syntax.TZ x187 = x182 + x186;
+Tbase Syntax.TZ x188 = 0x13 * x187;
+Tbase Syntax.TZ x189 = x180 + x188;
+Tbase Syntax.TZ x190 = x164 + x189;
+Tbase Syntax.TZ x191 = x190 >> 0x1a;
+Tbase Syntax.TZ x192 = x1 * x18;
+Tbase Syntax.TZ x193 = x2 * x17;
+Tbase Syntax.TZ x194 = x3 * x16;
+Tbase Syntax.TZ x195 = x4 * x15;
+Tbase Syntax.TZ x196 = x5 * x14;
+Tbase Syntax.TZ x197 = x6 * x13;
+Tbase Syntax.TZ x198 = x7 * x12;
+Tbase Syntax.TZ x199 = x8 * x11;
+Tbase Syntax.TZ x200 = x198 + x199;
+Tbase Syntax.TZ x201 = x197 + x200;
+Tbase Syntax.TZ x202 = x196 + x201;
+Tbase Syntax.TZ x203 = x195 + x202;
+Tbase Syntax.TZ x204 = x194 + x203;
+Tbase Syntax.TZ x205 = x193 + x204;
+Tbase Syntax.TZ x206 = x192 + x205;
+Tbase Syntax.TZ x207 = x * x10;
+Tbase Syntax.TZ x208 = x0 * x9;
+Tbase Syntax.TZ x209 = x207 + x208;
+Tbase Syntax.TZ x210 = 0x13 * x209;
+Tbase Syntax.TZ x211 = x206 + x210;
+Tbase Syntax.TZ x212 = x191 + x211;
+Tbase Syntax.TZ x213 = x212 >> 0x19;
+Tbase Syntax.TZ x214 = x0 * x18;
+Tbase Syntax.TZ x215 = x17 * 0x2;
+Tbase Syntax.TZ x216 = x1 * x215;
+Tbase Syntax.TZ x217 = x2 * x16;
+Tbase Syntax.TZ x218 = x15 * 0x2;
+Tbase Syntax.TZ x219 = x3 * x218;
+Tbase Syntax.TZ x220 = x4 * x14;
+Tbase Syntax.TZ x221 = x13 * 0x2;
+Tbase Syntax.TZ x222 = x5 * x221;
+Tbase Syntax.TZ x223 = x6 * x12;
+Tbase Syntax.TZ x224 = x11 * 0x2;
+Tbase Syntax.TZ x225 = x7 * x224;
+Tbase Syntax.TZ x226 = x8 * x10;
+Tbase Syntax.TZ x227 = x225 + x226;
+Tbase Syntax.TZ x228 = x223 + x227;
+Tbase Syntax.TZ x229 = x222 + x228;
+Tbase Syntax.TZ x230 = x220 + x229;
+Tbase Syntax.TZ x231 = x219 + x230;
+Tbase Syntax.TZ x232 = x217 + x231;
+Tbase Syntax.TZ x233 = x216 + x232;
+Tbase Syntax.TZ x234 = x214 + x233;
+Tbase Syntax.TZ x235 = x9 * 0x2;
+Tbase Syntax.TZ x236 = x * x235;
+Tbase Syntax.TZ x237 = 0x13 * x236;
+Tbase Syntax.TZ x238 = x234 + x237;
+Tbase Syntax.TZ x239 = x213 + x238;
+Tbase Syntax.TZ x240 = x239 >> 0x1a;
+Tbase Syntax.TZ x241 = x * x18;
+Tbase Syntax.TZ x242 = x0 * x17;
+Tbase Syntax.TZ x243 = x1 * x16;
+Tbase Syntax.TZ x244 = x2 * x15;
+Tbase Syntax.TZ x245 = x3 * x14;
+Tbase Syntax.TZ x246 = x4 * x13;
+Tbase Syntax.TZ x247 = x5 * x12;
+Tbase Syntax.TZ x248 = x6 * x11;
+Tbase Syntax.TZ x249 = x7 * x10;
+Tbase Syntax.TZ x250 = x8 * x9;
+Tbase Syntax.TZ x251 = x249 + x250;
+Tbase Syntax.TZ x252 = x248 + x251;
+Tbase Syntax.TZ x253 = x247 + x252;
+Tbase Syntax.TZ x254 = x246 + x253;
+Tbase Syntax.TZ x255 = x245 + x254;
+Tbase Syntax.TZ x256 = x244 + x255;
+Tbase Syntax.TZ x257 = x243 + x256;
+Tbase Syntax.TZ x258 = x242 + x257;
+Tbase Syntax.TZ x259 = x241 + x258;
+Tbase Syntax.TZ x260 = x240 + x259;
+Tbase Syntax.TZ x261 = x260 >> 0x19;
+Tbase Syntax.TZ x262 = 0x13 * x261;
+Tbase Syntax.TZ x263 = x43 & 0x3ffffff;
+Tbase Syntax.TZ x264 = x262 + x263;
+Tbase Syntax.TZ x265 = x264 >> 0x1a;
+Tbase Syntax.TZ x266 = x65 & 0x1ffffff;
+Tbase Syntax.TZ x267 = x265 + x266;
+Tbase Syntax.TZ x268 = x260 & 0x1ffffff;
+Tbase Syntax.TZ x269 = x239 & 0x3ffffff;
+Tbase Syntax.TZ x270 = x212 & 0x1ffffff;
+Tbase Syntax.TZ x271 = x190 & 0x3ffffff;
+Tbase Syntax.TZ x272 = x163 & 0x1ffffff;
+Tbase Syntax.TZ x273 = x141 & 0x3ffffff;
+Tbase Syntax.TZ x274 = x114 & 0x1ffffff;
+Tbase Syntax.TZ x275 = x267 >> 0x19;
+Tbase Syntax.TZ x276 = x92 & 0x3ffffff;
+Tbase Syntax.TZ x277 = x275 + x276;
+Tbase Syntax.TZ x278 = x267 & 0x1ffffff;
+Tbase Syntax.TZ x279 = x264 & 0x3ffffff;
+(Return x268, Return x269, Return x270, Return x271, 
+Return x272, Return x273, Return x274, Return x277, 
+Return x278, Return x279)
+     : forall var : Syntax.base_type -> Type,
+       expr Syntax.base_type Syntax.op
+         (Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ)
+
+Argument scope is [function_scope]
diff --git a/src/Specific/GF25519Reflective/Reified/MulJavaDisplay.log b/src/Specific/GF25519Reflective/Reified/MulJavaDisplay.log
new file mode 100644
index 000000000..d0d6c01b1
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/MulJavaDisplay.log
@@ -0,0 +1,297 @@
+rmulW = 
+fun var : Syntax.base_type -> Type =>
+λ
+x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17
+ x18 : var Syntax.TZ,
+Tbase Syntax.TZ x19 = x8 * x18;
+Tbase Syntax.TZ x20 = x17 * 0x2;
+Tbase Syntax.TZ x21 = x * x20;
+Tbase Syntax.TZ x22 = x0 * x16;
+Tbase Syntax.TZ x23 = x15 * 0x2;
+Tbase Syntax.TZ x24 = x1 * x23;
+Tbase Syntax.TZ x25 = x2 * x14;
+Tbase Syntax.TZ x26 = x13 * 0x2;
+Tbase Syntax.TZ x27 = x3 * x26;
+Tbase Syntax.TZ x28 = x4 * x12;
+Tbase Syntax.TZ x29 = x11 * 0x2;
+Tbase Syntax.TZ x30 = x5 * x29;
+Tbase Syntax.TZ x31 = x6 * x10;
+Tbase Syntax.TZ x32 = x9 * 0x2;
+Tbase Syntax.TZ x33 = x7 * x32;
+Tbase Syntax.TZ x34 = x31 + x33;
+Tbase Syntax.TZ x35 = x30 + x34;
+Tbase Syntax.TZ x36 = x28 + x35;
+Tbase Syntax.TZ x37 = x27 + x36;
+Tbase Syntax.TZ x38 = x25 + x37;
+Tbase Syntax.TZ x39 = x24 + x38;
+Tbase Syntax.TZ x40 = x22 + x39;
+Tbase Syntax.TZ x41 = x21 + x40;
+Tbase Syntax.TZ x42 = 0x13 * x41;
+Tbase Syntax.TZ x43 = x19 + x42;
+Tbase Syntax.TZ x44 = x43 >>> 0x1a;
+Tbase Syntax.TZ x45 = x7 * x18;
+Tbase Syntax.TZ x46 = x8 * x17;
+Tbase Syntax.TZ x47 = x45 + x46;
+Tbase Syntax.TZ x48 = x * x16;
+Tbase Syntax.TZ x49 = x0 * x15;
+Tbase Syntax.TZ x50 = x1 * x14;
+Tbase Syntax.TZ x51 = x2 * x13;
+Tbase Syntax.TZ x52 = x3 * x12;
+Tbase Syntax.TZ x53 = x4 * x11;
+Tbase Syntax.TZ x54 = x5 * x10;
+Tbase Syntax.TZ x55 = x6 * x9;
+Tbase Syntax.TZ x56 = x54 + x55;
+Tbase Syntax.TZ x57 = x53 + x56;
+Tbase Syntax.TZ x58 = x52 + x57;
+Tbase Syntax.TZ x59 = x51 + x58;
+Tbase Syntax.TZ x60 = x50 + x59;
+Tbase Syntax.TZ x61 = x49 + x60;
+Tbase Syntax.TZ x62 = x48 + x61;
+Tbase Syntax.TZ x63 = 0x13 * x62;
+Tbase Syntax.TZ x64 = x47 + x63;
+Tbase Syntax.TZ x65 = x44 + x64;
+Tbase Syntax.TZ x66 = x65 >>> 0x19;
+Tbase Syntax.TZ x67 = x6 * x18;
+Tbase Syntax.TZ x68 = x17 * 0x2;
+Tbase Syntax.TZ x69 = x7 * x68;
+Tbase Syntax.TZ x70 = x8 * x16;
+Tbase Syntax.TZ x71 = x69 + x70;
+Tbase Syntax.TZ x72 = x67 + x71;
+Tbase Syntax.TZ x73 = x15 * 0x2;
+Tbase Syntax.TZ x74 = x * x73;
+Tbase Syntax.TZ x75 = x0 * x14;
+Tbase Syntax.TZ x76 = x13 * 0x2;
+Tbase Syntax.TZ x77 = x1 * x76;
+Tbase Syntax.TZ x78 = x2 * x12;
+Tbase Syntax.TZ x79 = x11 * 0x2;
+Tbase Syntax.TZ x80 = x3 * x79;
+Tbase Syntax.TZ x81 = x4 * x10;
+Tbase Syntax.TZ x82 = x9 * 0x2;
+Tbase Syntax.TZ x83 = x5 * x82;
+Tbase Syntax.TZ x84 = x81 + x83;
+Tbase Syntax.TZ x85 = x80 + x84;
+Tbase Syntax.TZ x86 = x78 + x85;
+Tbase Syntax.TZ x87 = x77 + x86;
+Tbase Syntax.TZ x88 = x75 + x87;
+Tbase Syntax.TZ x89 = x74 + x88;
+Tbase Syntax.TZ x90 = 0x13 * x89;
+Tbase Syntax.TZ x91 = x72 + x90;
+Tbase Syntax.TZ x92 = x66 + x91;
+Tbase Syntax.TZ x93 = x92 >>> 0x1a;
+Tbase Syntax.TZ x94 = x5 * x18;
+Tbase Syntax.TZ x95 = x6 * x17;
+Tbase Syntax.TZ x96 = x7 * x16;
+Tbase Syntax.TZ x97 = x8 * x15;
+Tbase Syntax.TZ x98 = x96 + x97;
+Tbase Syntax.TZ x99 = x95 + x98;
+Tbase Syntax.TZ x100 = x94 + x99;
+Tbase Syntax.TZ x101 = x * x14;
+Tbase Syntax.TZ x102 = x0 * x13;
+Tbase Syntax.TZ x103 = x1 * x12;
+Tbase Syntax.TZ x104 = x2 * x11;
+Tbase Syntax.TZ x105 = x3 * x10;
+Tbase Syntax.TZ x106 = x4 * x9;
+Tbase Syntax.TZ x107 = x105 + x106;
+Tbase Syntax.TZ x108 = x104 + x107;
+Tbase Syntax.TZ x109 = x103 + x108;
+Tbase Syntax.TZ x110 = x102 + x109;
+Tbase Syntax.TZ x111 = x101 + x110;
+Tbase Syntax.TZ x112 = 0x13 * x111;
+Tbase Syntax.TZ x113 = x100 + x112;
+Tbase Syntax.TZ x114 = x93 + x113;
+Tbase Syntax.TZ x115 = x114 >>> 0x19;
+Tbase Syntax.TZ x116 = x4 * x18;
+Tbase Syntax.TZ x117 = x17 * 0x2;
+Tbase Syntax.TZ x118 = x5 * x117;
+Tbase Syntax.TZ x119 = x6 * x16;
+Tbase Syntax.TZ x120 = x15 * 0x2;
+Tbase Syntax.TZ x121 = x7 * x120;
+Tbase Syntax.TZ x122 = x8 * x14;
+Tbase Syntax.TZ x123 = x121 + x122;
+Tbase Syntax.TZ x124 = x119 + x123;
+Tbase Syntax.TZ x125 = x118 + x124;
+Tbase Syntax.TZ x126 = x116 + x125;
+Tbase Syntax.TZ x127 = x13 * 0x2;
+Tbase Syntax.TZ x128 = x * x127;
+Tbase Syntax.TZ x129 = x0 * x12;
+Tbase Syntax.TZ x130 = x11 * 0x2;
+Tbase Syntax.TZ x131 = x1 * x130;
+Tbase Syntax.TZ x132 = x2 * x10;
+Tbase Syntax.TZ x133 = x9 * 0x2;
+Tbase Syntax.TZ x134 = x3 * x133;
+Tbase Syntax.TZ x135 = x132 + x134;
+Tbase Syntax.TZ x136 = x131 + x135;
+Tbase Syntax.TZ x137 = x129 + x136;
+Tbase Syntax.TZ x138 = x128 + x137;
+Tbase Syntax.TZ x139 = 0x13 * x138;
+Tbase Syntax.TZ x140 = x126 + x139;
+Tbase Syntax.TZ x141 = x115 + x140;
+Tbase Syntax.TZ x142 = x141 >>> 0x1a;
+Tbase Syntax.TZ x143 = x3 * x18;
+Tbase Syntax.TZ x144 = x4 * x17;
+Tbase Syntax.TZ x145 = x5 * x16;
+Tbase Syntax.TZ x146 = x6 * x15;
+Tbase Syntax.TZ x147 = x7 * x14;
+Tbase Syntax.TZ x148 = x8 * x13;
+Tbase Syntax.TZ x149 = x147 + x148;
+Tbase Syntax.TZ x150 = x146 + x149;
+Tbase Syntax.TZ x151 = x145 + x150;
+Tbase Syntax.TZ x152 = x144 + x151;
+Tbase Syntax.TZ x153 = x143 + x152;
+Tbase Syntax.TZ x154 = x * x12;
+Tbase Syntax.TZ x155 = x0 * x11;
+Tbase Syntax.TZ x156 = x1 * x10;
+Tbase Syntax.TZ x157 = x2 * x9;
+Tbase Syntax.TZ x158 = x156 + x157;
+Tbase Syntax.TZ x159 = x155 + x158;
+Tbase Syntax.TZ x160 = x154 + x159;
+Tbase Syntax.TZ x161 = 0x13 * x160;
+Tbase Syntax.TZ x162 = x153 + x161;
+Tbase Syntax.TZ x163 = x142 + x162;
+Tbase Syntax.TZ x164 = x163 >>> 0x19;
+Tbase Syntax.TZ x165 = x2 * x18;
+Tbase Syntax.TZ x166 = x17 * 0x2;
+Tbase Syntax.TZ x167 = x3 * x166;
+Tbase Syntax.TZ x168 = x4 * x16;
+Tbase Syntax.TZ x169 = x15 * 0x2;
+Tbase Syntax.TZ x170 = x5 * x169;
+Tbase Syntax.TZ x171 = x6 * x14;
+Tbase Syntax.TZ x172 = x13 * 0x2;
+Tbase Syntax.TZ x173 = x7 * x172;
+Tbase Syntax.TZ x174 = x8 * x12;
+Tbase Syntax.TZ x175 = x173 + x174;
+Tbase Syntax.TZ x176 = x171 + x175;
+Tbase Syntax.TZ x177 = x170 + x176;
+Tbase Syntax.TZ x178 = x168 + x177;
+Tbase Syntax.TZ x179 = x167 + x178;
+Tbase Syntax.TZ x180 = x165 + x179;
+Tbase Syntax.TZ x181 = x11 * 0x2;
+Tbase Syntax.TZ x182 = x * x181;
+Tbase Syntax.TZ x183 = x0 * x10;
+Tbase Syntax.TZ x184 = x9 * 0x2;
+Tbase Syntax.TZ x185 = x1 * x184;
+Tbase Syntax.TZ x186 = x183 + x185;
+Tbase Syntax.TZ x187 = x182 + x186;
+Tbase Syntax.TZ x188 = 0x13 * x187;
+Tbase Syntax.TZ x189 = x180 + x188;
+Tbase Syntax.TZ x190 = x164 + x189;
+Tbase Syntax.TZ x191 = x190 >>> 0x1a;
+Tbase Syntax.TZ x192 = x1 * x18;
+Tbase Syntax.TZ x193 = x2 * x17;
+Tbase Syntax.TZ x194 = x3 * x16;
+Tbase Syntax.TZ x195 = x4 * x15;
+Tbase Syntax.TZ x196 = x5 * x14;
+Tbase Syntax.TZ x197 = x6 * x13;
+Tbase Syntax.TZ x198 = x7 * x12;
+Tbase Syntax.TZ x199 = x8 * x11;
+Tbase Syntax.TZ x200 = x198 + x199;
+Tbase Syntax.TZ x201 = x197 + x200;
+Tbase Syntax.TZ x202 = x196 + x201;
+Tbase Syntax.TZ x203 = x195 + x202;
+Tbase Syntax.TZ x204 = x194 + x203;
+Tbase Syntax.TZ x205 = x193 + x204;
+Tbase Syntax.TZ x206 = x192 + x205;
+Tbase Syntax.TZ x207 = x * x10;
+Tbase Syntax.TZ x208 = x0 * x9;
+Tbase Syntax.TZ x209 = x207 + x208;
+Tbase Syntax.TZ x210 = 0x13 * x209;
+Tbase Syntax.TZ x211 = x206 + x210;
+Tbase Syntax.TZ x212 = x191 + x211;
+Tbase Syntax.TZ x213 = x212 >>> 0x19;
+Tbase Syntax.TZ x214 = x0 * x18;
+Tbase Syntax.TZ x215 = x17 * 0x2;
+Tbase Syntax.TZ x216 = x1 * x215;
+Tbase Syntax.TZ x217 = x2 * x16;
+Tbase Syntax.TZ x218 = x15 * 0x2;
+Tbase Syntax.TZ x219 = x3 * x218;
+Tbase Syntax.TZ x220 = x4 * x14;
+Tbase Syntax.TZ x221 = x13 * 0x2;
+Tbase Syntax.TZ x222 = x5 * x221;
+Tbase Syntax.TZ x223 = x6 * x12;
+Tbase Syntax.TZ x224 = x11 * 0x2;
+Tbase Syntax.TZ x225 = x7 * x224;
+Tbase Syntax.TZ x226 = x8 * x10;
+Tbase Syntax.TZ x227 = x225 + x226;
+Tbase Syntax.TZ x228 = x223 + x227;
+Tbase Syntax.TZ x229 = x222 + x228;
+Tbase Syntax.TZ x230 = x220 + x229;
+Tbase Syntax.TZ x231 = x219 + x230;
+Tbase Syntax.TZ x232 = x217 + x231;
+Tbase Syntax.TZ x233 = x216 + x232;
+Tbase Syntax.TZ x234 = x214 + x233;
+Tbase Syntax.TZ x235 = x9 * 0x2;
+Tbase Syntax.TZ x236 = x * x235;
+Tbase Syntax.TZ x237 = 0x13 * x236;
+Tbase Syntax.TZ x238 = x234 + x237;
+Tbase Syntax.TZ x239 = x213 + x238;
+Tbase Syntax.TZ x240 = x239 >>> 0x1a;
+Tbase Syntax.TZ x241 = x * x18;
+Tbase Syntax.TZ x242 = x0 * x17;
+Tbase Syntax.TZ x243 = x1 * x16;
+Tbase Syntax.TZ x244 = x2 * x15;
+Tbase Syntax.TZ x245 = x3 * x14;
+Tbase Syntax.TZ x246 = x4 * x13;
+Tbase Syntax.TZ x247 = x5 * x12;
+Tbase Syntax.TZ x248 = x6 * x11;
+Tbase Syntax.TZ x249 = x7 * x10;
+Tbase Syntax.TZ x250 = x8 * x9;
+Tbase Syntax.TZ x251 = x249 + x250;
+Tbase Syntax.TZ x252 = x248 + x251;
+Tbase Syntax.TZ x253 = x247 + x252;
+Tbase Syntax.TZ x254 = x246 + x253;
+Tbase Syntax.TZ x255 = x245 + x254;
+Tbase Syntax.TZ x256 = x244 + x255;
+Tbase Syntax.TZ x257 = x243 + x256;
+Tbase Syntax.TZ x258 = x242 + x257;
+Tbase Syntax.TZ x259 = x241 + x258;
+Tbase Syntax.TZ x260 = x240 + x259;
+Tbase Syntax.TZ x261 = x260 >>> 0x19;
+Tbase Syntax.TZ x262 = 0x13 * x261;
+Tbase Syntax.TZ x263 = x43 & 0x3ffffff;
+Tbase Syntax.TZ x264 = x262 + x263;
+Tbase Syntax.TZ x265 = x264 >>> 0x1a;
+Tbase Syntax.TZ x266 = x65 & 0x1ffffff;
+Tbase Syntax.TZ x267 = x265 + x266;
+Tbase Syntax.TZ x268 = x260 & 0x1ffffff;
+Tbase Syntax.TZ x269 = x239 & 0x3ffffff;
+Tbase Syntax.TZ x270 = x212 & 0x1ffffff;
+Tbase Syntax.TZ x271 = x190 & 0x3ffffff;
+Tbase Syntax.TZ x272 = x163 & 0x1ffffff;
+Tbase Syntax.TZ x273 = x141 & 0x3ffffff;
+Tbase Syntax.TZ x274 = x114 & 0x1ffffff;
+Tbase Syntax.TZ x275 = x267 >>> 0x19;
+Tbase Syntax.TZ x276 = x92 & 0x3ffffff;
+Tbase Syntax.TZ x277 = x275 + x276;
+Tbase Syntax.TZ x278 = x267 & 0x1ffffff;
+Tbase Syntax.TZ x279 = x264 & 0x3ffffff;
+(Return x268, Return x269, Return x270, Return x271, 
+Return x272, Return x273, Return x274, Return x277, 
+Return x278, Return x279)
+     : forall var : Syntax.base_type -> Type,
+       expr Syntax.base_type Syntax.op
+         (Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Syntax.TZ ->
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
+          Tbase Syntax.TZ)
+
+Argument scope is [function_scope]