Changeset 2649 for extracted/cminor_syntax.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_syntax.ml
r2601 r2649 23 23 open Identifiers 24 24 25 open Floats26 27 25 open Integers 28 26 … … 47 45 open Pointers 48 46 47 open ErrorMessages 48 49 49 open Option 50 50 … … 54 54 55 55 open Positive 56 57 open Char58 59 open String60 56 61 57 open PreIdentifiers … … 115 111 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 116 112 > 'a1) > AST.typ > expr > 'a1 **) 117 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 2680= function118  Id (t, x_1 2682) > h_Id t x_12682119  Cst (t, x_1 2683) > h_Cst t x_12683120  Op1 (t, t', x_1 2685, x_12684) >121 h_Op1 t t' x_1 2685 x_12684122 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2684)123  Op2 (t1, t2, t', x_1 2688, x_12687, x_12686) >124 h_Op2 t1 t2 t' x_1 2688 x_12687 x_12686125 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 2687)126 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 2686)127  Mem (t, x_1 2689) >128 h_Mem t x_1 2689113 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10365 = function 114  Id (t, x_10367) > h_Id t x_10367 115  Cst (t, x_10368) > h_Cst t x_10368 116  Op1 (t, t', x_10370, x_10369) > 117 h_Op1 t t' x_10370 x_10369 118 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10369) 119  Op2 (t1, t2, t', x_10373, x_10372, x_10371) > 120 h_Op2 t1 t2 t' x_10373 x_10372 x_10371 121 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10372) 122 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10371) 123  Mem (t, x_10374) > 124 h_Mem t x_10374 129 125 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 130 x_1 2689)131  Cond (sz, sg, t, x_1 2692, x_12691, x_12690) >132 h_Cond sz sg t x_1 2692 x_12691 x_12690126 x_10374) 127  Cond (sz, sg, t, x_10377, x_10376, x_10375) > 128 h_Cond sz sg t x_10377 x_10376 x_10375 133 129 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 134 (sz, sg)) x_1 2692)135 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2691)136 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2690)137  Ecost (t, x_1 2694, x_12693) >138 h_Ecost t x_1 2694 x_12693139 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2693)130 (sz, sg)) x_10377) 131 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10376) 132 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10375) 133  Ecost (t, x_10379, x_10378) > 134 h_Ecost t x_10379 x_10378 135 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10378) 140 136 141 137 (** val expr_rect_Type3 : … … 147 143 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 148 144 > 'a1) > AST.typ > expr > 'a1 **) 149 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 2724= function150  Id (t, x_1 2726) > h_Id t x_12726151  Cst (t, x_1 2727) > h_Cst t x_12727152  Op1 (t, t', x_1 2729, x_12728) >153 h_Op1 t t' x_1 2729 x_12728154 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2728)155  Op2 (t1, t2, t', x_1 2732, x_12731, x_12730) >156 h_Op2 t1 t2 t' x_1 2732 x_12731 x_12730157 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 2731)158 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 2730)159  Mem (t, x_1 2733) >160 h_Mem t x_1 2733145 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10409 = function 146  Id (t, x_10411) > h_Id t x_10411 147  Cst (t, x_10412) > h_Cst t x_10412 148  Op1 (t, t', x_10414, x_10413) > 149 h_Op1 t t' x_10414 x_10413 150 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10413) 151  Op2 (t1, t2, t', x_10417, x_10416, x_10415) > 152 h_Op2 t1 t2 t' x_10417 x_10416 x_10415 153 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10416) 154 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10415) 155  Mem (t, x_10418) > 156 h_Mem t x_10418 161 157 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 162 x_1 2733)163  Cond (sz, sg, t, x_1 2736, x_12735, x_12734) >164 h_Cond sz sg t x_1 2736 x_12735 x_12734158 x_10418) 159  Cond (sz, sg, t, x_10421, x_10420, x_10419) > 160 h_Cond sz sg t x_10421 x_10420 x_10419 165 161 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 166 (sz, sg)) x_1 2736)167 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2735)168 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2734)169  Ecost (t, x_1 2738, x_12737) >170 h_Ecost t x_1 2738 x_12737171 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2737)162 (sz, sg)) x_10421) 163 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10420) 164 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10419) 165  Ecost (t, x_10423, x_10422) > 166 h_Ecost t x_10423 x_10422 167 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10422) 172 168 173 169 (** val expr_rect_Type2 : … … 179 175 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 180 176 > 'a1) > AST.typ > expr > 'a1 **) 181 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 2746= function182  Id (t, x_1 2748) > h_Id t x_12748183  Cst (t, x_1 2749) > h_Cst t x_12749184  Op1 (t, t', x_1 2751, x_12750) >185 h_Op1 t t' x_1 2751 x_12750186 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2750)187  Op2 (t1, t2, t', x_1 2754, x_12753, x_12752) >188 h_Op2 t1 t2 t' x_1 2754 x_12753 x_12752189 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 2753)190 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 2752)191  Mem (t, x_1 2755) >192 h_Mem t x_1 2755177 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10431 = function 178  Id (t, x_10433) > h_Id t x_10433 179  Cst (t, x_10434) > h_Cst t x_10434 180  Op1 (t, t', x_10436, x_10435) > 181 h_Op1 t t' x_10436 x_10435 182 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10435) 183  Op2 (t1, t2, t', x_10439, x_10438, x_10437) > 184 h_Op2 t1 t2 t' x_10439 x_10438 x_10437 185 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10438) 186 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10437) 187  Mem (t, x_10440) > 188 h_Mem t x_10440 193 189 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 194 x_1 2755)195  Cond (sz, sg, t, x_1 2758, x_12757, x_12756) >196 h_Cond sz sg t x_1 2758 x_12757 x_12756190 x_10440) 191  Cond (sz, sg, t, x_10443, x_10442, x_10441) > 192 h_Cond sz sg t x_10443 x_10442 x_10441 197 193 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 198 (sz, sg)) x_1 2758)199 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2757)200 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2756)201  Ecost (t, x_1 2760, x_12759) >202 h_Ecost t x_1 2760 x_12759203 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2759)194 (sz, sg)) x_10443) 195 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10442) 196 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10441) 197  Ecost (t, x_10445, x_10444) > 198 h_Ecost t x_10445 x_10444 199 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10444) 204 200 205 201 (** val expr_rect_Type1 : … … 211 207 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 212 208 > 'a1) > AST.typ > expr > 'a1 **) 213 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 2768= function214  Id (t, x_1 2770) > h_Id t x_12770215  Cst (t, x_1 2771) > h_Cst t x_12771216  Op1 (t, t', x_1 2773, x_12772) >217 h_Op1 t t' x_1 2773 x_12772218 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2772)219  Op2 (t1, t2, t', x_1 2776, x_12775, x_12774) >220 h_Op2 t1 t2 t' x_1 2776 x_12775 x_12774221 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 2775)222 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 2774)223  Mem (t, x_1 2777) >224 h_Mem t x_1 2777209 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10453 = function 210  Id (t, x_10455) > h_Id t x_10455 211  Cst (t, x_10456) > h_Cst t x_10456 212  Op1 (t, t', x_10458, x_10457) > 213 h_Op1 t t' x_10458 x_10457 214 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10457) 215  Op2 (t1, t2, t', x_10461, x_10460, x_10459) > 216 h_Op2 t1 t2 t' x_10461 x_10460 x_10459 217 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10460) 218 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10459) 219  Mem (t, x_10462) > 220 h_Mem t x_10462 225 221 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 226 x_1 2777)227  Cond (sz, sg, t, x_1 2780, x_12779, x_12778) >228 h_Cond sz sg t x_1 2780 x_12779 x_12778222 x_10462) 223  Cond (sz, sg, t, x_10465, x_10464, x_10463) > 224 h_Cond sz sg t x_10465 x_10464 x_10463 229 225 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 230 (sz, sg)) x_1 2780)231 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2779)232 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2778)233  Ecost (t, x_1 2782, x_12781) >234 h_Ecost t x_1 2782 x_12781235 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2781)226 (sz, sg)) x_10465) 227 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10464) 228 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10463) 229  Ecost (t, x_10467, x_10466) > 230 h_Ecost t x_10467 x_10466 231 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10466) 236 232 237 233 (** val expr_rect_Type0 : … … 243 239 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 244 240 > 'a1) > AST.typ > expr > 'a1 **) 245 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_1 2790= function246  Id (t, x_1 2792) > h_Id t x_12792247  Cst (t, x_1 2793) > h_Cst t x_12793248  Op1 (t, t', x_1 2795, x_12794) >249 h_Op1 t t' x_1 2795 x_12794250 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2794)251  Op2 (t1, t2, t', x_1 2798, x_12797, x_12796) >252 h_Op2 t1 t2 t' x_1 2798 x_12797 x_12796253 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_1 2797)254 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_1 2796)255  Mem (t, x_1 2799) >256 h_Mem t x_1 2799241 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10475 = function 242  Id (t, x_10477) > h_Id t x_10477 243  Cst (t, x_10478) > h_Cst t x_10478 244  Op1 (t, t', x_10480, x_10479) > 245 h_Op1 t t' x_10480 x_10479 246 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10479) 247  Op2 (t1, t2, t', x_10483, x_10482, x_10481) > 248 h_Op2 t1 t2 t' x_10483 x_10482 x_10481 249 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10482) 250 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10481) 251  Mem (t, x_10484) > 252 h_Mem t x_10484 257 253 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 258 x_1 2799)259  Cond (sz, sg, t, x_1 2802, x_12801, x_12800) >260 h_Cond sz sg t x_1 2802 x_12801 x_12800254 x_10484) 255  Cond (sz, sg, t, x_10487, x_10486, x_10485) > 256 h_Cond sz sg t x_10487 x_10486 x_10485 261 257 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 262 (sz, sg)) x_1 2802)263 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2801)264 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2800)265  Ecost (t, x_1 2804, x_12803) >266 h_Ecost t x_1 2804 x_12803267 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_1 2803)258 (sz, sg)) x_10487) 259 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10486) 260 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10485) 261  Ecost (t, x_10489, x_10488) > 262 h_Ecost t x_10489 x_10488 263 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10488) 268 264 269 265 (** val expr_inv_rect_Type4 : … … 353 349 type expr_vars = __ 354 350 355 (** val label : String.string **)356 let label = "Label"357 (*failwith "AXIOM TO BE REALIZED"*)358 359 351 type stmt = 360 352  St_skip … … 381 373 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 382 374  St_skip > h_St_skip 383  St_assign (t, x_1 2975, x_12974) > h_St_assign t x_12975 x_12974384  St_store (t, x_1 2977, x_12976) > h_St_store t x_12977 x_12976385  St_call (x_1 2980, x_12979, x_12978) > h_St_call x_12980 x_12979 x_12978386  St_seq (x_1 2982, x_12981) >387 h_St_seq x_1 2982 x_12981375  St_assign (t, x_10660, x_10659) > h_St_assign t x_10660 x_10659 376  St_store (t, x_10662, x_10661) > h_St_store t x_10662 x_10661 377  St_call (x_10665, x_10664, x_10663) > h_St_call x_10665 x_10664 x_10663 378  St_seq (x_10667, x_10666) > 379 h_St_seq x_10667 x_10666 388 380 (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 2982)381 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10667) 390 382 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 391 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 2981)392  St_ifthenelse (sz, sg, x_1 2985, x_12984, x_12983) >393 h_St_ifthenelse sz sg x_1 2985 x_12984 x_12983383 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10666) 384  St_ifthenelse (sz, sg, x_10670, x_10669, x_10668) > 385 h_St_ifthenelse sz sg x_10670 x_10669 x_10668 394 386 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 395 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 2984)387 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10669) 396 388 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 397 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 2983)398  St_return x_1 2986 > h_St_return x_12986399  St_label (x_1 2988, x_12987) >400 h_St_label x_1 2988 x_12987389 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10668) 390  St_return x_10671 > h_St_return x_10671 391  St_label (x_10673, x_10672) > 392 h_St_label x_10673 x_10672 401 393 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 402 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 2987)403  St_goto x_1 2989 > h_St_goto x_12989404  St_cost (x_1 2991, x_12990) >405 h_St_cost x_1 2991 x_12990394 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10672) 395  St_goto x_10674 > h_St_goto x_10674 396  St_cost (x_10676, x_10675) > 397 h_St_cost x_10676 x_10675 406 398 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 407 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 2990)399 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10675) 408 400 409 401 (** val stmt_rect_Type3 : … … 418 410 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 419 411  St_skip > h_St_skip 420  St_assign (t, x_1 3033, x_13032) > h_St_assign t x_13033 x_13032421  St_store (t, x_1 3035, x_13034) > h_St_store t x_13035 x_13034422  St_call (x_1 3038, x_13037, x_13036) > h_St_call x_13038 x_13037 x_13036423  St_seq (x_1 3040, x_13039) >424 h_St_seq x_1 3040 x_13039412  St_assign (t, x_10718, x_10717) > h_St_assign t x_10718 x_10717 413  St_store (t, x_10720, x_10719) > h_St_store t x_10720 x_10719 414  St_call (x_10723, x_10722, x_10721) > h_St_call x_10723 x_10722 x_10721 415  St_seq (x_10725, x_10724) > 416 h_St_seq x_10725 x_10724 425 417 (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 3040)418 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10725) 427 419 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 428 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3039)429  St_ifthenelse (sz, sg, x_1 3043, x_13042, x_13041) >430 h_St_ifthenelse sz sg x_1 3043 x_13042 x_13041420 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10724) 421  St_ifthenelse (sz, sg, x_10728, x_10727, x_10726) > 422 h_St_ifthenelse sz sg x_10728 x_10727 x_10726 431 423 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 432 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3042)424 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10727) 433 425 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 434 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3041)435  St_return x_1 3044 > h_St_return x_13044436  St_label (x_1 3046, x_13045) >437 h_St_label x_1 3046 x_13045426 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10726) 427  St_return x_10729 > h_St_return x_10729 428  St_label (x_10731, x_10730) > 429 h_St_label x_10731 x_10730 438 430 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 439 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3045)440  St_goto x_1 3047 > h_St_goto x_13047441  St_cost (x_1 3049, x_13048) >442 h_St_cost x_1 3049 x_13048431 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10730) 432  St_goto x_10732 > h_St_goto x_10732 433  St_cost (x_10734, x_10733) > 434 h_St_cost x_10734 x_10733 443 435 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 444 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3048)436 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10733) 445 437 446 438 (** val stmt_rect_Type2 : … … 455 447 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 456 448  St_skip > h_St_skip 457  St_assign (t, x_1 3062, x_13061) > h_St_assign t x_13062 x_13061458  St_store (t, x_1 3064, x_13063) > h_St_store t x_13064 x_13063459  St_call (x_1 3067, x_13066, x_13065) > h_St_call x_13067 x_13066 x_13065460  St_seq (x_1 3069, x_13068) >461 h_St_seq x_1 3069 x_13068449  St_assign (t, x_10747, x_10746) > h_St_assign t x_10747 x_10746 450  St_store (t, x_10749, x_10748) > h_St_store t x_10749 x_10748 451  St_call (x_10752, x_10751, x_10750) > h_St_call x_10752 x_10751 x_10750 452  St_seq (x_10754, x_10753) > 453 h_St_seq x_10754 x_10753 462 454 (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 3069)455 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10754) 464 456 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 465 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3068)466  St_ifthenelse (sz, sg, x_1 3072, x_13071, x_13070) >467 h_St_ifthenelse sz sg x_1 3072 x_13071 x_13070457 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10753) 458  St_ifthenelse (sz, sg, x_10757, x_10756, x_10755) > 459 h_St_ifthenelse sz sg x_10757 x_10756 x_10755 468 460 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 469 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3071)461 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10756) 470 462 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 471 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3070)472  St_return x_1 3073 > h_St_return x_13073473  St_label (x_1 3075, x_13074) >474 h_St_label x_1 3075 x_13074463 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10755) 464  St_return x_10758 > h_St_return x_10758 465  St_label (x_10760, x_10759) > 466 h_St_label x_10760 x_10759 475 467 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 476 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3074)477  St_goto x_1 3076 > h_St_goto x_13076478  St_cost (x_1 3078, x_13077) >479 h_St_cost x_1 3078 x_13077468 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10759) 469  St_goto x_10761 > h_St_goto x_10761 470  St_cost (x_10763, x_10762) > 471 h_St_cost x_10763 x_10762 480 472 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 481 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3077)473 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10762) 482 474 483 475 (** val stmt_rect_Type1 : … … 492 484 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 493 485  St_skip > h_St_skip 494  St_assign (t, x_1 3091, x_13090) > h_St_assign t x_13091 x_13090495  St_store (t, x_1 3093, x_13092) > h_St_store t x_13093 x_13092496  St_call (x_1 3096, x_13095, x_13094) > h_St_call x_13096 x_13095 x_13094497  St_seq (x_1 3098, x_13097) >498 h_St_seq x_1 3098 x_13097486  St_assign (t, x_10776, x_10775) > h_St_assign t x_10776 x_10775 487  St_store (t, x_10778, x_10777) > h_St_store t x_10778 x_10777 488  St_call (x_10781, x_10780, x_10779) > h_St_call x_10781 x_10780 x_10779 489  St_seq (x_10783, x_10782) > 490 h_St_seq x_10783 x_10782 499 491 (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 3098)492 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10783) 501 493 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 502 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3097)503  St_ifthenelse (sz, sg, x_1 3101, x_13100, x_13099) >504 h_St_ifthenelse sz sg x_1 3101 x_13100 x_13099494 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10782) 495  St_ifthenelse (sz, sg, x_10786, x_10785, x_10784) > 496 h_St_ifthenelse sz sg x_10786 x_10785 x_10784 505 497 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 506 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3100)498 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10785) 507 499 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 508 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3099)509  St_return x_1 3102 > h_St_return x_13102510  St_label (x_1 3104, x_13103) >511 h_St_label x_1 3104 x_13103500 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10784) 501  St_return x_10787 > h_St_return x_10787 502  St_label (x_10789, x_10788) > 503 h_St_label x_10789 x_10788 512 504 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 513 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3103)514  St_goto x_1 3105 > h_St_goto x_13105515  St_cost (x_1 3107, x_13106) >516 h_St_cost x_1 3107 x_13106505 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10788) 506  St_goto x_10790 > h_St_goto x_10790 507  St_cost (x_10792, x_10791) > 508 h_St_cost x_10792 x_10791 517 509 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 518 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3106)510 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10791) 519 511 520 512 (** val stmt_rect_Type0 : … … 529 521 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 530 522  St_skip > h_St_skip 531  St_assign (t, x_1 3120, x_13119) > h_St_assign t x_13120 x_13119532  St_store (t, x_1 3122, x_13121) > h_St_store t x_13122 x_13121533  St_call (x_1 3125, x_13124, x_13123) > h_St_call x_13125 x_13124 x_13123534  St_seq (x_1 3127, x_13126) >535 h_St_seq x_1 3127 x_13126523  St_assign (t, x_10805, x_10804) > h_St_assign t x_10805 x_10804 524  St_store (t, x_10807, x_10806) > h_St_store t x_10807 x_10806 525  St_call (x_10810, x_10809, x_10808) > h_St_call x_10810 x_10809 x_10808 526  St_seq (x_10812, x_10811) > 527 h_St_seq x_10812 x_10811 536 528 (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 3127)529 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10812) 538 530 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 539 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3126)540  St_ifthenelse (sz, sg, x_1 3130, x_13129, x_13128) >541 h_St_ifthenelse sz sg x_1 3130 x_13129 x_13128531 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10811) 532  St_ifthenelse (sz, sg, x_10815, x_10814, x_10813) > 533 h_St_ifthenelse sz sg x_10815 x_10814 x_10813 542 534 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 543 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3129)535 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10814) 544 536 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 545 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3128)546  St_return x_1 3131 > h_St_return x_13131547  St_label (x_1 3133, x_13132) >548 h_St_label x_1 3133 x_13132537 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10813) 538  St_return x_10816 > h_St_return x_10816 539  St_label (x_10818, x_10817) > 540 h_St_label x_10818 x_10817 549 541 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 550 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3132)551  St_goto x_1 3134 > h_St_goto x_13134552  St_cost (x_1 3136, x_13135) >553 h_St_cost x_1 3136 x_13135542 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10817) 543  St_goto x_10819 > h_St_goto x_10819 544  St_cost (x_10821, x_10820) > 545 h_St_cost x_10821 x_10820 554 546 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 555 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_1 3135)547 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10820) 556 548 557 549 (** val stmt_inv_rect_Type4 : … … 767 759 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 768 760 > 'a1) > internal_function > 'a1 **) 769 let rec internal_function_rect_Type4 h_mk_internal_function x_1 3431=761 let rec internal_function_rect_Type4 h_mk_internal_function x_11116 = 770 762 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 771 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 3431763 f_stacksize = f_stacksize0; f_body = f_body0 } = x_11116 772 764 in 773 765 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 778 770 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 779 771 > 'a1) > internal_function > 'a1 **) 780 let rec internal_function_rect_Type5 h_mk_internal_function x_1 3433=772 let rec internal_function_rect_Type5 h_mk_internal_function x_11118 = 781 773 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 782 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 3433774 f_stacksize = f_stacksize0; f_body = f_body0 } = x_11118 783 775 in 784 776 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 789 781 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 790 782 > 'a1) > internal_function > 'a1 **) 791 let rec internal_function_rect_Type3 h_mk_internal_function x_1 3435=783 let rec internal_function_rect_Type3 h_mk_internal_function x_11120 = 792 784 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 793 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 3435785 f_stacksize = f_stacksize0; f_body = f_body0 } = x_11120 794 786 in 795 787 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 800 792 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 801 793 > 'a1) > internal_function > 'a1 **) 802 let rec internal_function_rect_Type2 h_mk_internal_function x_1 3437=794 let rec internal_function_rect_Type2 h_mk_internal_function x_11122 = 803 795 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 804 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 3437796 f_stacksize = f_stacksize0; f_body = f_body0 } = x_11122 805 797 in 806 798 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 811 803 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 812 804 > 'a1) > internal_function > 'a1 **) 813 let rec internal_function_rect_Type1 h_mk_internal_function x_1 3439=805 let rec internal_function_rect_Type1 h_mk_internal_function x_11124 = 814 806 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 815 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 3439807 f_stacksize = f_stacksize0; f_body = f_body0 } = x_11124 816 808 in 817 809 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 822 814 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 823 815 > 'a1) > internal_function > 'a1 **) 824 let rec internal_function_rect_Type0 h_mk_internal_function x_1 3441=816 let rec internal_function_rect_Type0 h_mk_internal_function x_11126 = 825 817 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 826 f_stacksize = f_stacksize0; f_body = f_body0 } = x_1 3441818 f_stacksize = f_stacksize0; f_body = f_body0 } = x_11126 827 819 in 828 820 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
Note: See TracChangeset
for help on using the changeset viewer.