Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_syntax.ml

    r2717 r2730  
    115115    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    116116    -> '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 = 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
     117let 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
    129129    (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_13691
     130      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
    133133    (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_13694
    139     (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)
    140140
    141141(** val expr_rect_Type3 :
     
    147147    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    148148    -> '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 = 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
     149let 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
    161161    (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_13735
     162      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
    165165    (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_13738
    171     (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)
    172172
    173173(** val expr_rect_Type2 :
     
    179179    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    180180    -> '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 = 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
     181let 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
    193193    (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_13757
     194      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
    197197    (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_13760
    203     (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)
    204204
    205205(** val expr_rect_Type1 :
     
    211211    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    212212    -> '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 = 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
     213let 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
    225225    (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_13779
     226      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
    229229    (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_13782
    235     (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)
    236236
    237237(** val expr_rect_Type0 :
     
    243243    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    244244    -> '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 = 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
     245let 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
    257257    (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_13801
     258      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
    261261    (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_13804
    267     (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)
    268268
    269269(** val expr_inv_rect_Type4 :
     
    377377let 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
    378378| St_skip -> h_St_skip
    379 | 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
     379| 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
    384384    (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)
    386386    (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_13984
     387      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
    390390    (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)
    392392    (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_13987
    395 | St_label (x_13989, x_13988) ->
    396   h_St_label x_13989 x_13988
     393      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
    397397    (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_13990
    400 | St_cost (x_13992, x_13991) ->
    401   h_St_cost x_13992 x_13991
     398      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
    402402    (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)
    404404
    405405(** val stmt_rect_Type3 :
     
    414414let 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
    415415| St_skip -> h_St_skip
    416 | 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
     416| 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
    421421    (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)
    423423    (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_14042
     424      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
    427427    (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)
    429429    (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_14045
    432 | St_label (x_14047, x_14046) ->
    433   h_St_label x_14047 x_14046
     430      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
    434434    (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_14048
    437 | St_cost (x_14050, x_14049) ->
    438   h_St_cost x_14050 x_14049
     435      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
    439439    (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)
    441441
    442442(** val stmt_rect_Type2 :
     
    451451let 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
    452452| St_skip -> h_St_skip
    453 | 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
     453| 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
    458458    (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)
    460460    (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_14071
     461      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
    464464    (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)
    466466    (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_14074
    469 | St_label (x_14076, x_14075) ->
    470   h_St_label x_14076 x_14075
     467      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
    471471    (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_14077
    474 | St_cost (x_14079, x_14078) ->
    475   h_St_cost x_14079 x_14078
     472      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
    476476    (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)
    478478
    479479(** val stmt_rect_Type1 :
     
    488488let 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
    489489| St_skip -> h_St_skip
    490 | 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
     490| 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
    495495    (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)
    497497    (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_14100
     498      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
    501501    (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)
    503503    (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_14103
    506 | St_label (x_14105, x_14104) ->
    507   h_St_label x_14105 x_14104
     504      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
    508508    (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_14106
    511 | St_cost (x_14108, x_14107) ->
    512   h_St_cost x_14108 x_14107
     509      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
    513513    (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)
    515515
    516516(** val stmt_rect_Type0 :
     
    525525let 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
    526526| St_skip -> h_St_skip
    527 | 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
     527| 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
    532532    (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)
    534534    (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_14129
     535      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
    538538    (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)
    540540    (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_14132
    543 | St_label (x_14134, x_14133) ->
    544   h_St_label x_14134 x_14133
     541      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
    545545    (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_14135
    548 | St_cost (x_14137, x_14136) ->
    549   h_St_cost x_14137 x_14136
     546      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
    550550    (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)
    552552
    553553(** val stmt_inv_rect_Type4 :
     
    763763    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    764764    -> 'a1) -> internal_function -> 'a1 **)
    765 let rec internal_function_rect_Type4 h_mk_internal_function x_14432 =
     765let rec internal_function_rect_Type4 h_mk_internal_function x_3320 =
    766766  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    767     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14432
     767    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3320
    768768  in
    769769  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    774774    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    775775    -> 'a1) -> internal_function -> 'a1 **)
    776 let rec internal_function_rect_Type5 h_mk_internal_function x_14434 =
     776let rec internal_function_rect_Type5 h_mk_internal_function x_3322 =
    777777  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    778     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14434
     778    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3322
    779779  in
    780780  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    785785    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    786786    -> 'a1) -> internal_function -> 'a1 **)
    787 let rec internal_function_rect_Type3 h_mk_internal_function x_14436 =
     787let rec internal_function_rect_Type3 h_mk_internal_function x_3324 =
    788788  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    789     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14436
     789    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3324
    790790  in
    791791  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    796796    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    797797    -> 'a1) -> internal_function -> 'a1 **)
    798 let rec internal_function_rect_Type2 h_mk_internal_function x_14438 =
     798let rec internal_function_rect_Type2 h_mk_internal_function x_3326 =
    799799  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    800     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14438
     800    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3326
    801801  in
    802802  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    807807    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    808808    -> 'a1) -> internal_function -> 'a1 **)
    809 let rec internal_function_rect_Type1 h_mk_internal_function x_14440 =
     809let rec internal_function_rect_Type1 h_mk_internal_function x_3328 =
    810810  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    811     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14440
     811    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3328
    812812  in
    813813  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    818818    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    819819    -> 'a1) -> internal_function -> 'a1 **)
    820 let rec internal_function_rect_Type0 h_mk_internal_function x_14442 =
     820let rec internal_function_rect_Type0 h_mk_internal_function x_3330 =
    821821  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    822     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14442
     822    f_stacksize = f_stacksize0; f_body = f_body0 } = x_3330
    823823  in
    824824  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
Note: See TracChangeset for help on using the changeset viewer.