Changeset 2730 for extracted/cminor_syntax.ml
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_syntax.ml
r2717 r2730 115 115 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 116 116 > '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_ 13681= function118  Id (t, x_ 13683) > h_Id t x_13683119  Cst (t, x_ 13684) > h_Cst t x_13684120  Op1 (t, t', x_ 13686, x_13685) >121 h_Op1 t t' x_ 13686 x_13685122 (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_13687125 (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_ 13690117 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2569 = function 118  Id (t, x_2571) > h_Id t x_2571 119  Cst (t, x_2572) > h_Cst t x_2572 120  Op1 (t, t', x_2574, x_2573) > 121 h_Op1 t t' x_2574 x_2573 122 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2573) 123  Op2 (t1, t2, t', x_2577, x_2576, x_2575) > 124 h_Op2 t1 t2 t' x_2577 x_2576 x_2575 125 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2576) 126 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2575) 127  Mem (t, x_2578) > 128 h_Mem t x_2578 129 129 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 130 x_ 13690)131  Cond (sz, sg, t, x_ 13693, x_13692, x_13691) >132 h_Cond sz sg t x_ 13693 x_13692 x_13691130 x_2578) 131  Cond (sz, sg, t, x_2581, x_2580, x_2579) > 132 h_Cond sz sg t x_2581 x_2580 x_2579 133 133 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 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_13694139 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_ 13694)134 (sz, sg)) x_2581) 135 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2580) 136 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2579) 137  Ecost (t, x_2583, x_2582) > 138 h_Ecost t x_2583 x_2582 139 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2582) 140 140 141 141 (** val expr_rect_Type3 : … … 147 147 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 148 148 > '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_ 13725= function150  Id (t, x_ 13727) > h_Id t x_13727151  Cst (t, x_ 13728) > h_Cst t x_13728152  Op1 (t, t', x_ 13730, x_13729) >153 h_Op1 t t' x_ 13730 x_13729154 (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_13731157 (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_ 13734149 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2613 = function 150  Id (t, x_2615) > h_Id t x_2615 151  Cst (t, x_2616) > h_Cst t x_2616 152  Op1 (t, t', x_2618, x_2617) > 153 h_Op1 t t' x_2618 x_2617 154 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2617) 155  Op2 (t1, t2, t', x_2621, x_2620, x_2619) > 156 h_Op2 t1 t2 t' x_2621 x_2620 x_2619 157 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2620) 158 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2619) 159  Mem (t, x_2622) > 160 h_Mem t x_2622 161 161 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 162 x_ 13734)163  Cond (sz, sg, t, x_ 13737, x_13736, x_13735) >164 h_Cond sz sg t x_ 13737 x_13736 x_13735162 x_2622) 163  Cond (sz, sg, t, x_2625, x_2624, x_2623) > 164 h_Cond sz sg t x_2625 x_2624 x_2623 165 165 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 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_13738171 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_ 13738)166 (sz, sg)) x_2625) 167 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2624) 168 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2623) 169  Ecost (t, x_2627, x_2626) > 170 h_Ecost t x_2627 x_2626 171 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2626) 172 172 173 173 (** val expr_rect_Type2 : … … 179 179 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 180 180 > '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_ 13747= function182  Id (t, x_ 13749) > h_Id t x_13749183  Cst (t, x_ 13750) > h_Cst t x_13750184  Op1 (t, t', x_ 13752, x_13751) >185 h_Op1 t t' x_ 13752 x_13751186 (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_13753189 (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_ 13756181 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2635 = function 182  Id (t, x_2637) > h_Id t x_2637 183  Cst (t, x_2638) > h_Cst t x_2638 184  Op1 (t, t', x_2640, x_2639) > 185 h_Op1 t t' x_2640 x_2639 186 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2639) 187  Op2 (t1, t2, t', x_2643, x_2642, x_2641) > 188 h_Op2 t1 t2 t' x_2643 x_2642 x_2641 189 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2642) 190 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2641) 191  Mem (t, x_2644) > 192 h_Mem t x_2644 193 193 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 194 x_ 13756)195  Cond (sz, sg, t, x_ 13759, x_13758, x_13757) >196 h_Cond sz sg t x_ 13759 x_13758 x_13757194 x_2644) 195  Cond (sz, sg, t, x_2647, x_2646, x_2645) > 196 h_Cond sz sg t x_2647 x_2646 x_2645 197 197 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 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_13760203 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_ 13760)198 (sz, sg)) x_2647) 199 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2646) 200 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2645) 201  Ecost (t, x_2649, x_2648) > 202 h_Ecost t x_2649 x_2648 203 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2648) 204 204 205 205 (** val expr_rect_Type1 : … … 211 211 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 212 212 > '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_ 13769= function214  Id (t, x_ 13771) > h_Id t x_13771215  Cst (t, x_ 13772) > h_Cst t x_13772216  Op1 (t, t', x_ 13774, x_13773) >217 h_Op1 t t' x_ 13774 x_13773218 (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_13775221 (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_ 13778213 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2657 = function 214  Id (t, x_2659) > h_Id t x_2659 215  Cst (t, x_2660) > h_Cst t x_2660 216  Op1 (t, t', x_2662, x_2661) > 217 h_Op1 t t' x_2662 x_2661 218 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2661) 219  Op2 (t1, t2, t', x_2665, x_2664, x_2663) > 220 h_Op2 t1 t2 t' x_2665 x_2664 x_2663 221 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2664) 222 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2663) 223  Mem (t, x_2666) > 224 h_Mem t x_2666 225 225 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 226 x_ 13778)227  Cond (sz, sg, t, x_ 13781, x_13780, x_13779) >228 h_Cond sz sg t x_ 13781 x_13780 x_13779226 x_2666) 227  Cond (sz, sg, t, x_2669, x_2668, x_2667) > 228 h_Cond sz sg t x_2669 x_2668 x_2667 229 229 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 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_13782235 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_ 13782)230 (sz, sg)) x_2669) 231 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2668) 232 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2667) 233  Ecost (t, x_2671, x_2670) > 234 h_Ecost t x_2671 x_2670 235 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2670) 236 236 237 237 (** val expr_rect_Type0 : … … 243 243 > 'a1 > 'a1 > 'a1) > (AST.typ > CostLabel.costlabel > expr > 'a1 244 244 > '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_ 13791= function246  Id (t, x_ 13793) > h_Id t x_13793247  Cst (t, x_ 13794) > h_Cst t x_13794248  Op1 (t, t', x_ 13796, x_13795) >249 h_Op1 t t' x_ 13796 x_13795250 (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_13797253 (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_ 13800245 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_2679 = function 246  Id (t, x_2681) > h_Id t x_2681 247  Cst (t, x_2682) > h_Cst t x_2682 248  Op1 (t, t', x_2684, x_2683) > 249 h_Op1 t t' x_2684 x_2683 250 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2683) 251  Op2 (t1, t2, t', x_2687, x_2686, x_2685) > 252 h_Op2 t1 t2 t' x_2687 x_2686 x_2685 253 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_2686) 254 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_2685) 255  Mem (t, x_2688) > 256 h_Mem t x_2688 257 257 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr 258 x_ 13800)259  Cond (sz, sg, t, x_ 13803, x_13802, x_13801) >260 h_Cond sz sg t x_ 13803 x_13802 x_13801258 x_2688) 259  Cond (sz, sg, t, x_2691, x_2690, x_2689) > 260 h_Cond sz sg t x_2691 x_2690 x_2689 261 261 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint 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_13804267 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_ 13804)262 (sz, sg)) x_2691) 263 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2690) 264 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2689) 265  Ecost (t, x_2693, x_2692) > 266 h_Ecost t x_2693 x_2692 267 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_2692) 268 268 269 269 (** val expr_inv_rect_Type4 : … … 377 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 378 378  St_skip > h_St_skip 379  St_assign (t, x_ 13976, x_13975) > h_St_assign t x_13976 x_13975380  St_store (t, x_ 13978, x_13977) > h_St_store t x_13978 x_13977381  St_call (x_ 13981, x_13980, x_13979) > h_St_call x_13981 x_13980 x_13979382  St_seq (x_ 13983, x_13982) >383 h_St_seq x_ 13983 x_13982379  St_assign (t, x_2864, x_2863) > h_St_assign t x_2864 x_2863 380  St_store (t, x_2866, x_2865) > h_St_store t x_2866 x_2865 381  St_call (x_2869, x_2868, x_2867) > h_St_call x_2869 x_2868 x_2867 382  St_seq (x_2871, x_2870) > 383 h_St_seq x_2871 x_2870 384 384 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 385 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 13983)385 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2871) 386 386 (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_ 13982)388  St_ifthenelse (sz, sg, x_ 13986, x_13985, x_13984) >389 h_St_ifthenelse sz sg x_ 13986 x_13985 x_13984387 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2870) 388  St_ifthenelse (sz, sg, x_2874, x_2873, x_2872) > 389 h_St_ifthenelse sz sg x_2874 x_2873 x_2872 390 390 (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_ 13985)391 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2873) 392 392 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 393 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_13987395  St_label (x_ 13989, x_13988) >396 h_St_label x_ 13989 x_13988393 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2872) 394  St_return x_2875 > h_St_return x_2875 395  St_label (x_2877, x_2876) > 396 h_St_label x_2877 x_2876 397 397 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 398 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_13990400  St_cost (x_ 13992, x_13991) >401 h_St_cost x_ 13992 x_13991398 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2876) 399  St_goto x_2878 > h_St_goto x_2878 400  St_cost (x_2880, x_2879) > 401 h_St_cost x_2880 x_2879 402 402 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 403 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 13991)403 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2879) 404 404 405 405 (** val stmt_rect_Type3 : … … 414 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 415 415  St_skip > h_St_skip 416  St_assign (t, x_ 14034, x_14033) > h_St_assign t x_14034 x_14033417  St_store (t, x_ 14036, x_14035) > h_St_store t x_14036 x_14035418  St_call (x_ 14039, x_14038, x_14037) > h_St_call x_14039 x_14038 x_14037419  St_seq (x_ 14041, x_14040) >420 h_St_seq x_ 14041 x_14040416  St_assign (t, x_2922, x_2921) > h_St_assign t x_2922 x_2921 417  St_store (t, x_2924, x_2923) > h_St_store t x_2924 x_2923 418  St_call (x_2927, x_2926, x_2925) > h_St_call x_2927 x_2926 x_2925 419  St_seq (x_2929, x_2928) > 420 h_St_seq x_2929 x_2928 421 421 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 422 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14041)422 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2929) 423 423 (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_ 14040)425  St_ifthenelse (sz, sg, x_ 14044, x_14043, x_14042) >426 h_St_ifthenelse sz sg x_ 14044 x_14043 x_14042424 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2928) 425  St_ifthenelse (sz, sg, x_2932, x_2931, x_2930) > 426 h_St_ifthenelse sz sg x_2932 x_2931 x_2930 427 427 (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_ 14043)428 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2931) 429 429 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 430 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_14045432  St_label (x_ 14047, x_14046) >433 h_St_label x_ 14047 x_14046430 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2930) 431  St_return x_2933 > h_St_return x_2933 432  St_label (x_2935, x_2934) > 433 h_St_label x_2935 x_2934 434 434 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 435 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_14048437  St_cost (x_ 14050, x_14049) >438 h_St_cost x_ 14050 x_14049435 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2934) 436  St_goto x_2936 > h_St_goto x_2936 437  St_cost (x_2938, x_2937) > 438 h_St_cost x_2938 x_2937 439 439 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 440 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14049)440 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2937) 441 441 442 442 (** val stmt_rect_Type2 : … … 451 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 452 452  St_skip > h_St_skip 453  St_assign (t, x_ 14063, x_14062) > h_St_assign t x_14063 x_14062454  St_store (t, x_ 14065, x_14064) > h_St_store t x_14065 x_14064455  St_call (x_ 14068, x_14067, x_14066) > h_St_call x_14068 x_14067 x_14066456  St_seq (x_ 14070, x_14069) >457 h_St_seq x_ 14070 x_14069453  St_assign (t, x_2951, x_2950) > h_St_assign t x_2951 x_2950 454  St_store (t, x_2953, x_2952) > h_St_store t x_2953 x_2952 455  St_call (x_2956, x_2955, x_2954) > h_St_call x_2956 x_2955 x_2954 456  St_seq (x_2958, x_2957) > 457 h_St_seq x_2958 x_2957 458 458 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 459 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14070)459 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2958) 460 460 (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_ 14069)462  St_ifthenelse (sz, sg, x_ 14073, x_14072, x_14071) >463 h_St_ifthenelse sz sg x_ 14073 x_14072 x_14071461 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2957) 462  St_ifthenelse (sz, sg, x_2961, x_2960, x_2959) > 463 h_St_ifthenelse sz sg x_2961 x_2960 x_2959 464 464 (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_ 14072)465 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2960) 466 466 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 467 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_14074469  St_label (x_ 14076, x_14075) >470 h_St_label x_ 14076 x_14075467 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2959) 468  St_return x_2962 > h_St_return x_2962 469  St_label (x_2964, x_2963) > 470 h_St_label x_2964 x_2963 471 471 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 472 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_14077474  St_cost (x_ 14079, x_14078) >475 h_St_cost x_ 14079 x_14078472 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2963) 473  St_goto x_2965 > h_St_goto x_2965 474  St_cost (x_2967, x_2966) > 475 h_St_cost x_2967 x_2966 476 476 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 477 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14078)477 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2966) 478 478 479 479 (** val stmt_rect_Type1 : … … 488 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 489 489  St_skip > h_St_skip 490  St_assign (t, x_ 14092, x_14091) > h_St_assign t x_14092 x_14091491  St_store (t, x_ 14094, x_14093) > h_St_store t x_14094 x_14093492  St_call (x_ 14097, x_14096, x_14095) > h_St_call x_14097 x_14096 x_14095493  St_seq (x_ 14099, x_14098) >494 h_St_seq x_ 14099 x_14098490  St_assign (t, x_2980, x_2979) > h_St_assign t x_2980 x_2979 491  St_store (t, x_2982, x_2981) > h_St_store t x_2982 x_2981 492  St_call (x_2985, x_2984, x_2983) > h_St_call x_2985 x_2984 x_2983 493  St_seq (x_2987, x_2986) > 494 h_St_seq x_2987 x_2986 495 495 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 496 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14099)496 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2987) 497 497 (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_ 14098)499  St_ifthenelse (sz, sg, x_ 14102, x_14101, x_14100) >500 h_St_ifthenelse sz sg x_ 14102 x_14101 x_14100498 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2986) 499  St_ifthenelse (sz, sg, x_2990, x_2989, x_2988) > 500 h_St_ifthenelse sz sg x_2990 x_2989 x_2988 501 501 (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_ 14101)502 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2989) 503 503 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 504 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_14103506  St_label (x_ 14105, x_14104) >507 h_St_label x_ 14105 x_14104504 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2988) 505  St_return x_2991 > h_St_return x_2991 506  St_label (x_2993, x_2992) > 507 h_St_label x_2993 x_2992 508 508 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 509 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_14106511  St_cost (x_ 14108, x_14107) >512 h_St_cost x_ 14108 x_14107509 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2992) 510  St_goto x_2994 > h_St_goto x_2994 511  St_cost (x_2996, x_2995) > 512 h_St_cost x_2996 x_2995 513 513 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 514 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14107)514 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_2995) 515 515 516 516 (** val stmt_rect_Type0 : … … 525 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 526 526  St_skip > h_St_skip 527  St_assign (t, x_ 14121, x_14120) > h_St_assign t x_14121 x_14120528  St_store (t, x_ 14123, x_14122) > h_St_store t x_14123 x_14122529  St_call (x_ 14126, x_14125, x_14124) > h_St_call x_14126 x_14125 x_14124530  St_seq (x_ 14128, x_14127) >531 h_St_seq x_ 14128 x_14127527  St_assign (t, x_3009, x_3008) > h_St_assign t x_3009 x_3008 528  St_store (t, x_3011, x_3010) > h_St_store t x_3011 x_3010 529  St_call (x_3014, x_3013, x_3012) > h_St_call x_3014 x_3013 x_3012 530  St_seq (x_3016, x_3015) > 531 h_St_seq x_3016 x_3015 532 532 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 533 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14128)533 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3016) 534 534 (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_ 14127)536  St_ifthenelse (sz, sg, x_ 14131, x_14130, x_14129) >537 h_St_ifthenelse sz sg x_ 14131 x_14130 x_14129535 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3015) 536  St_ifthenelse (sz, sg, x_3019, x_3018, x_3017) > 537 h_St_ifthenelse sz sg x_3019 x_3018 x_3017 538 538 (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_ 14130)539 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3018) 540 540 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 541 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_14132543  St_label (x_ 14134, x_14133) >544 h_St_label x_ 14134 x_14133541 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3017) 542  St_return x_3020 > h_St_return x_3020 543  St_label (x_3022, x_3021) > 544 h_St_label x_3022 x_3021 545 545 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 546 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_14135548  St_cost (x_ 14137, x_14136) >549 h_St_cost x_ 14137 x_14136546 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3021) 547  St_goto x_3023 > h_St_goto x_3023 548  St_cost (x_3025, x_3024) > 549 h_St_cost x_3025 x_3024 550 550 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq 551 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_ 14136)551 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_3024) 552 552 553 553 (** val stmt_inv_rect_Type4 : … … 763 763 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 764 764 > 'a1) > internal_function > 'a1 **) 765 let rec internal_function_rect_Type4 h_mk_internal_function x_ 14432=765 let rec internal_function_rect_Type4 h_mk_internal_function x_3320 = 766 766 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 767 f_stacksize = f_stacksize0; f_body = f_body0 } = x_ 14432767 f_stacksize = f_stacksize0; f_body = f_body0 } = x_3320 768 768 in 769 769 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 774 774 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 775 775 > 'a1) > internal_function > 'a1 **) 776 let rec internal_function_rect_Type5 h_mk_internal_function x_ 14434=776 let rec internal_function_rect_Type5 h_mk_internal_function x_3322 = 777 777 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 778 f_stacksize = f_stacksize0; f_body = f_body0 } = x_ 14434778 f_stacksize = f_stacksize0; f_body = f_body0 } = x_3322 779 779 in 780 780 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 785 785 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 786 786 > 'a1) > internal_function > 'a1 **) 787 let rec internal_function_rect_Type3 h_mk_internal_function x_ 14436=787 let rec internal_function_rect_Type3 h_mk_internal_function x_3324 = 788 788 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 789 f_stacksize = f_stacksize0; f_body = f_body0 } = x_ 14436789 f_stacksize = f_stacksize0; f_body = f_body0 } = x_3324 790 790 in 791 791 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 796 796 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 797 797 > 'a1) > internal_function > 'a1 **) 798 let rec internal_function_rect_Type2 h_mk_internal_function x_ 14438=798 let rec internal_function_rect_Type2 h_mk_internal_function x_3326 = 799 799 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 800 f_stacksize = f_stacksize0; f_body = f_body0 } = x_ 14438800 f_stacksize = f_stacksize0; f_body = f_body0 } = x_3326 801 801 in 802 802 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 807 807 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 808 808 > 'a1) > internal_function > 'a1 **) 809 let rec internal_function_rect_Type1 h_mk_internal_function x_ 14440=809 let rec internal_function_rect_Type1 h_mk_internal_function x_3328 = 810 810 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 811 f_stacksize = f_stacksize0; f_body = f_body0 } = x_ 14440811 f_stacksize = f_stacksize0; f_body = f_body0 } = x_3328 812 812 in 813 813 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0 … … 818 818 (AST.ident, AST.typ) Types.prod List.list > __ > Nat.nat > stmt > __ 819 819 > 'a1) > internal_function > 'a1 **) 820 let rec internal_function_rect_Type0 h_mk_internal_function x_ 14442=820 let rec internal_function_rect_Type0 h_mk_internal_function x_3330 = 821 821 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0; 822 f_stacksize = f_stacksize0; f_body = f_body0 } = x_ 14442822 f_stacksize = f_stacksize0; f_body = f_body0 } = x_3330 823 823 in 824 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.