Changeset 2717 for extracted/cminor_syntax.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_syntax.ml
r2649 r2717 29 29 open Division 30 30 31 open Exp 32 31 33 open Arithmetic 32 34 … … 90 92 91 93 open FrontEndOps 94 95 open BitVectorTrie 92 96 93 97 open CostLabel … … 111 115 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 112 116 > 'a1) > AST.typ > expr > 'a1 **) 113 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 0365= function114  Id (t, x_1 0367) > h_Id t x_10367115  Cst (t, x_1 0368) > h_Cst t x_10368116  Op1 (t, t', x_1 0370, x_10369) >117 h_Op1 t t' x_1 0370 x_10369118 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0369)119  Op2 (t1, t2, t', x_1 0373, x_10372, x_10371) >120 h_Op2 t1 t2 t' x_1 0373 x_10372 x_10371121 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 0372)122 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 0371)123  Mem (t, x_1 0374) >124 h_Mem t x_1 0374117 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13681 = function 118  Id (t, x_13683) > h_Id t x_13683 119  Cst (t, x_13684) > h_Cst t x_13684 120  Op1 (t, t', x_13686, x_13685) > 121 h_Op1 t t' x_13686 x_13685 122 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13685) 123  Op2 (t1, t2, t', x_13689, x_13688, x_13687) > 124 h_Op2 t1 t2 t' x_13689 x_13688 x_13687 125 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13688) 126 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13687) 127  Mem (t, x_13690) > 128 h_Mem t x_13690 125 129 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 126 x_1 0374)127  Cond (sz, sg, t, x_1 0377, x_10376, x_10375) >128 h_Cond sz sg t x_1 0377 x_10376 x_10375130 x_13690) 131  Cond (sz, sg, t, x_13693, x_13692, x_13691) > 132 h_Cond sz sg t x_13693 x_13692 x_13691 129 133 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 130 (sz, sg)) x_1 0377)131 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0376)132 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0375)133  Ecost (t, x_1 0379, x_10378) >134 h_Ecost t x_1 0379 x_10378135 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0378)134 (sz, sg)) x_13693) 135 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13692) 136 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13691) 137  Ecost (t, x_13695, x_13694) > 138 h_Ecost t x_13695 x_13694 139 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13694) 136 140 137 141 (** val expr_rect_Type3 : … … 143 147 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 144 148 > 'a1) > AST.typ > expr > 'a1 **) 145 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 0409= function146  Id (t, x_1 0411) > h_Id t x_10411147  Cst (t, x_1 0412) > h_Cst t x_10412148  Op1 (t, t', x_1 0414, x_10413) >149 h_Op1 t t' x_1 0414 x_10413150 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0413)151  Op2 (t1, t2, t', x_1 0417, x_10416, x_10415) >152 h_Op2 t1 t2 t' x_1 0417 x_10416 x_10415153 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 0416)154 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 0415)155  Mem (t, x_1 0418) >156 h_Mem t x_1 0418149 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13725 = function 150  Id (t, x_13727) > h_Id t x_13727 151  Cst (t, x_13728) > h_Cst t x_13728 152  Op1 (t, t', x_13730, x_13729) > 153 h_Op1 t t' x_13730 x_13729 154 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13729) 155  Op2 (t1, t2, t', x_13733, x_13732, x_13731) > 156 h_Op2 t1 t2 t' x_13733 x_13732 x_13731 157 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13732) 158 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13731) 159  Mem (t, x_13734) > 160 h_Mem t x_13734 157 161 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 158 x_1 0418)159  Cond (sz, sg, t, x_1 0421, x_10420, x_10419) >160 h_Cond sz sg t x_1 0421 x_10420 x_10419162 x_13734) 163  Cond (sz, sg, t, x_13737, x_13736, x_13735) > 164 h_Cond sz sg t x_13737 x_13736 x_13735 161 165 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 162 (sz, sg)) x_1 0421)163 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0420)164 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0419)165  Ecost (t, x_1 0423, x_10422) >166 h_Ecost t x_1 0423 x_10422167 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0422)166 (sz, sg)) x_13737) 167 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13736) 168 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13735) 169  Ecost (t, x_13739, x_13738) > 170 h_Ecost t x_13739 x_13738 171 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13738) 168 172 169 173 (** val expr_rect_Type2 : … … 175 179 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 176 180 > 'a1) > AST.typ > expr > 'a1 **) 177 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 0431= function178  Id (t, x_1 0433) > h_Id t x_10433179  Cst (t, x_1 0434) > h_Cst t x_10434180  Op1 (t, t', x_1 0436, x_10435) >181 h_Op1 t t' x_1 0436 x_10435182 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0435)183  Op2 (t1, t2, t', x_1 0439, x_10438, x_10437) >184 h_Op2 t1 t2 t' x_1 0439 x_10438 x_10437185 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 0438)186 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 0437)187  Mem (t, x_1 0440) >188 h_Mem t x_1 0440181 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13747 = function 182  Id (t, x_13749) > h_Id t x_13749 183  Cst (t, x_13750) > h_Cst t x_13750 184  Op1 (t, t', x_13752, x_13751) > 185 h_Op1 t t' x_13752 x_13751 186 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13751) 187  Op2 (t1, t2, t', x_13755, x_13754, x_13753) > 188 h_Op2 t1 t2 t' x_13755 x_13754 x_13753 189 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13754) 190 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13753) 191  Mem (t, x_13756) > 192 h_Mem t x_13756 189 193 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 190 x_1 0440)191  Cond (sz, sg, t, x_1 0443, x_10442, x_10441) >192 h_Cond sz sg t x_1 0443 x_10442 x_10441194 x_13756) 195  Cond (sz, sg, t, x_13759, x_13758, x_13757) > 196 h_Cond sz sg t x_13759 x_13758 x_13757 193 197 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 194 (sz, sg)) x_1 0443)195 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0442)196 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0441)197  Ecost (t, x_1 0445, x_10444) >198 h_Ecost t x_1 0445 x_10444199 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0444)198 (sz, sg)) x_13759) 199 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13758) 200 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13757) 201  Ecost (t, x_13761, x_13760) > 202 h_Ecost t x_13761 x_13760 203 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13760) 200 204 201 205 (** val expr_rect_Type1 : … … 207 211 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 208 212 > 'a1) > AST.typ > expr > 'a1 **) 209 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 0453= function210  Id (t, x_1 0455) > h_Id t x_10455211  Cst (t, x_1 0456) > h_Cst t x_10456212  Op1 (t, t', x_1 0458, x_10457) >213 h_Op1 t t' x_1 0458 x_10457214 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0457)215  Op2 (t1, t2, t', x_1 0461, x_10460, x_10459) >216 h_Op2 t1 t2 t' x_1 0461 x_10460 x_10459217 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 0460)218 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 0459)219  Mem (t, x_1 0462) >220 h_Mem t x_1 0462213 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13769 = function 214  Id (t, x_13771) > h_Id t x_13771 215  Cst (t, x_13772) > h_Cst t x_13772 216  Op1 (t, t', x_13774, x_13773) > 217 h_Op1 t t' x_13774 x_13773 218 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13773) 219  Op2 (t1, t2, t', x_13777, x_13776, x_13775) > 220 h_Op2 t1 t2 t' x_13777 x_13776 x_13775 221 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13776) 222 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13775) 223  Mem (t, x_13778) > 224 h_Mem t x_13778 221 225 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 222 x_1 0462)223  Cond (sz, sg, t, x_1 0465, x_10464, x_10463) >224 h_Cond sz sg t x_1 0465 x_10464 x_10463226 x_13778) 227  Cond (sz, sg, t, x_13781, x_13780, x_13779) > 228 h_Cond sz sg t x_13781 x_13780 x_13779 225 229 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 226 (sz, sg)) x_1 0465)227 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0464)228 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0463)229  Ecost (t, x_1 0467, x_10466) >230 h_Ecost t x_1 0467 x_10466231 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0466)230 (sz, sg)) x_13781) 231 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13780) 232 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13779) 233  Ecost (t, x_13783, x_13782) > 234 h_Ecost t x_13783 x_13782 235 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13782) 232 236 233 237 (** val expr_rect_Type0 : … … 239 243 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 240 244 > 'a1) > AST.typ > expr > 'a1 **) 241 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 0475= function242  Id (t, x_1 0477) > h_Id t x_10477243  Cst (t, x_1 0478) > h_Cst t x_10478244  Op1 (t, t', x_1 0480, x_10479) >245 h_Op1 t t' x_1 0480 x_10479246 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0479)247  Op2 (t1, t2, t', x_1 0483, x_10482, x_10481) >248 h_Op2 t1 t2 t' x_1 0483 x_10482 x_10481249 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 0482)250 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 0481)251  Mem (t, x_1 0484) >252 h_Mem t x_1 0484245 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13791 = function 246  Id (t, x_13793) > h_Id t x_13793 247  Cst (t, x_13794) > h_Cst t x_13794 248  Op1 (t, t', x_13796, x_13795) > 249 h_Op1 t t' x_13796 x_13795 250 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13795) 251  Op2 (t1, t2, t', x_13799, x_13798, x_13797) > 252 h_Op2 t1 t2 t' x_13799 x_13798 x_13797 253 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13798) 254 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13797) 255  Mem (t, x_13800) > 256 h_Mem t x_13800 253 257 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 254 x_1 0484)255  Cond (sz, sg, t, x_1 0487, x_10486, x_10485) >256 h_Cond sz sg t x_1 0487 x_10486 x_10485258 x_13800) 259  Cond (sz, sg, t, x_13803, x_13802, x_13801) > 260 h_Cond sz sg t x_13803 x_13802 x_13801 257 261 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 258 (sz, sg)) x_1 0487)259 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0486)260 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0485)261  Ecost (t, x_1 0489, x_10488) >262 h_Ecost t x_1 0489 x_10488263 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 0488)262 (sz, sg)) x_13803) 263 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13802) 264 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13801) 265  Ecost (t, x_13805, x_13804) > 266 h_Ecost t x_13805 x_13804 267 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13804) 264 268 265 269 (** val expr_inv_rect_Type4 : … … 373 377 let rec stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function 374 378  St_skip > h_St_skip 375  St_assign (t, x_1 0660, x_10659) > h_St_assign t x_10660 x_10659376  St_store (t, x_1 0662, x_10661) > h_St_store t x_10662 x_10661377  St_call (x_1 0665, x_10664, x_10663) > h_St_call x_10665 x_10664 x_10663378  St_seq (x_1 0667, x_10666) >379 h_St_seq x_1 0667 x_10666379  St_assign (t, x_13976, x_13975) > h_St_assign t x_13976 x_13975 380  St_store (t, x_13978, x_13977) > h_St_store t x_13978 x_13977 381  St_call (x_13981, x_13980, x_13979) > h_St_call x_13981 x_13980 x_13979 382  St_seq (x_13983, x_13982) > 383 h_St_seq x_13983 x_13982 380 384 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 381 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0667)385 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13983) 382 386 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 383 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0666)384  St_ifthenelse (sz, sg, x_1 0670, x_10669, x_10668) >385 h_St_ifthenelse sz sg x_1 0670 x_10669 x_10668387 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13982) 388  St_ifthenelse (sz, sg, x_13986, x_13985, x_13984) > 389 h_St_ifthenelse sz sg x_13986 x_13985 x_13984 386 390 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 387 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0669)391 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13985) 388 392 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 389 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0668)390  St_return x_1 0671 > h_St_return x_10671391  St_label (x_1 0673, x_10672) >392 h_St_label x_1 0673 x_10672393 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13984) 394  St_return x_13987 > h_St_return x_13987 395  St_label (x_13989, x_13988) > 396 h_St_label x_13989 x_13988 393 397 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 394 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0672)395  St_goto x_1 0674 > h_St_goto x_10674396  St_cost (x_1 0676, x_10675) >397 h_St_cost x_1 0676 x_10675398 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13988) 399  St_goto x_13990 > h_St_goto x_13990 400  St_cost (x_13992, x_13991) > 401 h_St_cost x_13992 x_13991 398 402 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 399 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0675)403 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13991) 400 404 401 405 (** val stmt_rect_Type3 : … … 410 414 let rec stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function 411 415  St_skip > h_St_skip 412  St_assign (t, x_1 0718, x_10717) > h_St_assign t x_10718 x_10717413  St_store (t, x_1 0720, x_10719) > h_St_store t x_10720 x_10719414  St_call (x_1 0723, x_10722, x_10721) > h_St_call x_10723 x_10722 x_10721415  St_seq (x_1 0725, x_10724) >416 h_St_seq x_1 0725 x_10724416  St_assign (t, x_14034, x_14033) > h_St_assign t x_14034 x_14033 417  St_store (t, x_14036, x_14035) > h_St_store t x_14036 x_14035 418  St_call (x_14039, x_14038, x_14037) > h_St_call x_14039 x_14038 x_14037 419  St_seq (x_14041, x_14040) > 420 h_St_seq x_14041 x_14040 417 421 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 418 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0725)422 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14041) 419 423 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 420 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0724)421  St_ifthenelse (sz, sg, x_1 0728, x_10727, x_10726) >422 h_St_ifthenelse sz sg x_1 0728 x_10727 x_10726424 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14040) 425  St_ifthenelse (sz, sg, x_14044, x_14043, x_14042) > 426 h_St_ifthenelse sz sg x_14044 x_14043 x_14042 423 427 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 424 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0727)428 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14043) 425 429 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 426 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0726)427  St_return x_1 0729 > h_St_return x_10729428  St_label (x_1 0731, x_10730) >429 h_St_label x_1 0731 x_10730430 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14042) 431  St_return x_14045 > h_St_return x_14045 432  St_label (x_14047, x_14046) > 433 h_St_label x_14047 x_14046 430 434 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 431 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0730)432  St_goto x_1 0732 > h_St_goto x_10732433  St_cost (x_1 0734, x_10733) >434 h_St_cost x_1 0734 x_10733435 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14046) 436  St_goto x_14048 > h_St_goto x_14048 437  St_cost (x_14050, x_14049) > 438 h_St_cost x_14050 x_14049 435 439 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 436 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0733)440 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049) 437 441 438 442 (** val stmt_rect_Type2 : … … 447 451 let rec stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function 448 452  St_skip > h_St_skip 449  St_assign (t, x_1 0747, x_10746) > h_St_assign t x_10747 x_10746450  St_store (t, x_1 0749, x_10748) > h_St_store t x_10749 x_10748451  St_call (x_1 0752, x_10751, x_10750) > h_St_call x_10752 x_10751 x_10750452  St_seq (x_1 0754, x_10753) >453 h_St_seq x_1 0754 x_10753453  St_assign (t, x_14063, x_14062) > h_St_assign t x_14063 x_14062 454  St_store (t, x_14065, x_14064) > h_St_store t x_14065 x_14064 455  St_call (x_14068, x_14067, x_14066) > h_St_call x_14068 x_14067 x_14066 456  St_seq (x_14070, x_14069) > 457 h_St_seq x_14070 x_14069 454 458 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 455 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0754)459 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14070) 456 460 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 457 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0753)458  St_ifthenelse (sz, sg, x_1 0757, x_10756, x_10755) >459 h_St_ifthenelse sz sg x_1 0757 x_10756 x_10755461 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14069) 462  St_ifthenelse (sz, sg, x_14073, x_14072, x_14071) > 463 h_St_ifthenelse sz sg x_14073 x_14072 x_14071 460 464 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 461 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0756)465 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14072) 462 466 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 463 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0755)464  St_return x_1 0758 > h_St_return x_10758465  St_label (x_1 0760, x_10759) >466 h_St_label x_1 0760 x_10759467 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14071) 468  St_return x_14074 > h_St_return x_14074 469  St_label (x_14076, x_14075) > 470 h_St_label x_14076 x_14075 467 471 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 468 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0759)469  St_goto x_1 0761 > h_St_goto x_10761470  St_cost (x_1 0763, x_10762) >471 h_St_cost x_1 0763 x_10762472 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14075) 473  St_goto x_14077 > h_St_goto x_14077 474  St_cost (x_14079, x_14078) > 475 h_St_cost x_14079 x_14078 472 476 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 473 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0762)477 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14078) 474 478 475 479 (** val stmt_rect_Type1 : … … 484 488 let rec stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function 485 489  St_skip > h_St_skip 486  St_assign (t, x_1 0776, x_10775) > h_St_assign t x_10776 x_10775487  St_store (t, x_1 0778, x_10777) > h_St_store t x_10778 x_10777488  St_call (x_1 0781, x_10780, x_10779) > h_St_call x_10781 x_10780 x_10779489  St_seq (x_1 0783, x_10782) >490 h_St_seq x_1 0783 x_10782490  St_assign (t, x_14092, x_14091) > h_St_assign t x_14092 x_14091 491  St_store (t, x_14094, x_14093) > h_St_store t x_14094 x_14093 492  St_call (x_14097, x_14096, x_14095) > h_St_call x_14097 x_14096 x_14095 493  St_seq (x_14099, x_14098) > 494 h_St_seq x_14099 x_14098 491 495 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 492 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0783)496 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14099) 493 497 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 494 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0782)495  St_ifthenelse (sz, sg, x_1 0786, x_10785, x_10784) >496 h_St_ifthenelse sz sg x_1 0786 x_10785 x_10784498 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14098) 499  St_ifthenelse (sz, sg, x_14102, x_14101, x_14100) > 500 h_St_ifthenelse sz sg x_14102 x_14101 x_14100 497 501 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 498 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0785)502 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101) 499 503 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 500 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0784)501  St_return x_1 0787 > h_St_return x_10787502  St_label (x_1 0789, x_10788) >503 h_St_label x_1 0789 x_10788504 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14100) 505  St_return x_14103 > h_St_return x_14103 506  St_label (x_14105, x_14104) > 507 h_St_label x_14105 x_14104 504 508 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 505 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0788)506  St_goto x_1 0790 > h_St_goto x_10790507  St_cost (x_1 0792, x_10791) >508 h_St_cost x_1 0792 x_10791509 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14104) 510  St_goto x_14106 > h_St_goto x_14106 511  St_cost (x_14108, x_14107) > 512 h_St_cost x_14108 x_14107 509 513 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 510 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0791)514 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14107) 511 515 512 516 (** val stmt_rect_Type0 : … … 521 525 let rec stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function 522 526  St_skip > h_St_skip 523  St_assign (t, x_1 0805, x_10804) > h_St_assign t x_10805 x_10804524  St_store (t, x_1 0807, x_10806) > h_St_store t x_10807 x_10806525  St_call (x_1 0810, x_10809, x_10808) > h_St_call x_10810 x_10809 x_10808526  St_seq (x_1 0812, x_10811) >527 h_St_seq x_1 0812 x_10811527  St_assign (t, x_14121, x_14120) > h_St_assign t x_14121 x_14120 528  St_store (t, x_14123, x_14122) > h_St_store t x_14123 x_14122 529  St_call (x_14126, x_14125, x_14124) > h_St_call x_14126 x_14125 x_14124 530  St_seq (x_14128, x_14127) > 531 h_St_seq x_14128 x_14127 528 532 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 529 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0812)533 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14128) 530 534 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 531 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0811)532  St_ifthenelse (sz, sg, x_1 0815, x_10814, x_10813) >533 h_St_ifthenelse sz sg x_1 0815 x_10814 x_10813535 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14127) 536  St_ifthenelse (sz, sg, x_14131, x_14130, x_14129) > 537 h_St_ifthenelse sz sg x_14131 x_14130 x_14129 534 538 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 535 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0814)539 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130) 536 540 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 537 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0813)538  St_return x_1 0816 > h_St_return x_10816539  St_label (x_1 0818, x_10817) >540 h_St_label x_1 0818 x_10817541 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14129) 542  St_return x_14132 > h_St_return x_14132 543  St_label (x_14134, x_14133) > 544 h_St_label x_14134 x_14133 541 545 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 542 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0817)543  St_goto x_1 0819 > h_St_goto x_10819544  St_cost (x_1 0821, x_10820) >545 h_St_cost x_1 0821 x_10820546 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14133) 547  St_goto x_14135 > h_St_goto x_14135 548  St_cost (x_14137, x_14136) > 549 h_St_cost x_14137 x_14136 546 550 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 547 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 0820)551 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14136) 548 552 549 553 (** val stmt_inv_rect_Type4 : … … 759 763 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 760 764 > 'a1) > internal_function > 'a1 **) 761 let rec internal_function_rect_Type4 h_mk_internal_function x_1 1116=765 let rec internal_function_rect_Type4 h_mk_internal_function x_14432 = 762 766 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 763 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 1116767 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14432 764 768 in 765 769 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 770 774 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 771 775 > 'a1) > internal_function > 'a1 **) 772 let rec internal_function_rect_Type5 h_mk_internal_function x_1 1118=776 let rec internal_function_rect_Type5 h_mk_internal_function x_14434 = 773 777 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 774 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 1118778 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14434 775 779 in 776 780 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 781 785 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 782 786 > 'a1) > internal_function > 'a1 **) 783 let rec internal_function_rect_Type3 h_mk_internal_function x_1 1120=787 let rec internal_function_rect_Type3 h_mk_internal_function x_14436 = 784 788 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 785 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 1120789 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14436 786 790 in 787 791 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 792 796 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 793 797 > 'a1) > internal_function > 'a1 **) 794 let rec internal_function_rect_Type2 h_mk_internal_function x_1 1122=798 let rec internal_function_rect_Type2 h_mk_internal_function x_14438 = 795 799 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 796 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 1122800 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14438 797 801 in 798 802 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 803 807 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 804 808 > 'a1) > internal_function > 'a1 **) 805 let rec internal_function_rect_Type1 h_mk_internal_function x_1 1124=809 let rec internal_function_rect_Type1 h_mk_internal_function x_14440 = 806 810 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 807 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 1124811 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14440 808 812 in 809 813 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 814 818 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 815 819 > 'a1) > internal_function > 'a1 **) 816 let rec internal_function_rect_Type0 h_mk_internal_function x_1 1126=820 let rec internal_function_rect_Type0 h_mk_internal_function x_14442 = 817 821 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 818 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 1126822 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14442 819 823 in 820 824 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
Note: See TracChangeset
for help on using the changeset viewer.