Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_syntax.ml

    r2775 r2797  
    113113    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    114114    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    115 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13616 = function
    116 | Id (t, x_13618) -> h_Id t x_13618
    117 | Cst (t, x_13619) -> h_Cst t x_13619
    118 | Op1 (t, t', x_13621, x_13620) ->
    119   h_Op1 t t' x_13621 x_13620
    120     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13620)
    121 | Op2 (t1, t2, t', x_13624, x_13623, x_13622) ->
    122   h_Op2 t1 t2 t' x_13624 x_13623 x_13622
    123     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13623)
    124     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13622)
    125 | Mem (t, x_13625) ->
    126   h_Mem t x_13625
     115let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13629 = function
     116| Id (t, x_13631) -> h_Id t x_13631
     117| Cst (t, x_13632) -> h_Cst t x_13632
     118| Op1 (t, t', x_13634, x_13633) ->
     119  h_Op1 t t' x_13634 x_13633
     120    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13633)
     121| Op2 (t1, t2, t', x_13637, x_13636, x_13635) ->
     122  h_Op2 t1 t2 t' x_13637 x_13636 x_13635
     123    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13636)
     124    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13635)
     125| Mem (t, x_13638) ->
     126  h_Mem t x_13638
    127127    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    128       x_13625)
    129 | Cond (sz, sg, t, x_13628, x_13627, x_13626) ->
    130   h_Cond sz sg t x_13628 x_13627 x_13626
     128      x_13638)
     129| Cond (sz, sg, t, x_13641, x_13640, x_13639) ->
     130  h_Cond sz sg t x_13641 x_13640 x_13639
    131131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    132       (sz, sg)) x_13628)
    133     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13627)
    134     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13626)
    135 | Ecost (t, x_13630, x_13629) ->
    136   h_Ecost t x_13630 x_13629
    137     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13629)
     132      (sz, sg)) x_13641)
     133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13640)
     134    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13639)
     135| Ecost (t, x_13643, x_13642) ->
     136  h_Ecost t x_13643 x_13642
     137    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13642)
    138138
    139139(** val expr_rect_Type3 :
     
    145145    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    146146    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    147 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13660 = function
    148 | Id (t, x_13662) -> h_Id t x_13662
    149 | Cst (t, x_13663) -> h_Cst t x_13663
    150 | Op1 (t, t', x_13665, x_13664) ->
    151   h_Op1 t t' x_13665 x_13664
    152     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13664)
    153 | Op2 (t1, t2, t', x_13668, x_13667, x_13666) ->
    154   h_Op2 t1 t2 t' x_13668 x_13667 x_13666
    155     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13667)
    156     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13666)
    157 | Mem (t, x_13669) ->
    158   h_Mem t x_13669
     147let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13673 = function
     148| Id (t, x_13675) -> h_Id t x_13675
     149| Cst (t, x_13676) -> h_Cst t x_13676
     150| Op1 (t, t', x_13678, x_13677) ->
     151  h_Op1 t t' x_13678 x_13677
     152    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13677)
     153| Op2 (t1, t2, t', x_13681, x_13680, x_13679) ->
     154  h_Op2 t1 t2 t' x_13681 x_13680 x_13679
     155    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13680)
     156    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13679)
     157| Mem (t, x_13682) ->
     158  h_Mem t x_13682
    159159    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    160       x_13669)
    161 | Cond (sz, sg, t, x_13672, x_13671, x_13670) ->
    162   h_Cond sz sg t x_13672 x_13671 x_13670
     160      x_13682)
     161| Cond (sz, sg, t, x_13685, x_13684, x_13683) ->
     162  h_Cond sz sg t x_13685 x_13684 x_13683
    163163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    164       (sz, sg)) x_13672)
    165     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13671)
    166     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13670)
    167 | Ecost (t, x_13674, x_13673) ->
    168   h_Ecost t x_13674 x_13673
    169     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13673)
     164      (sz, sg)) x_13685)
     165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13684)
     166    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13683)
     167| Ecost (t, x_13687, x_13686) ->
     168  h_Ecost t x_13687 x_13686
     169    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13686)
    170170
    171171(** val expr_rect_Type2 :
     
    177177    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    178178    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    179 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13682 = function
    180 | Id (t, x_13684) -> h_Id t x_13684
    181 | Cst (t, x_13685) -> h_Cst t x_13685
    182 | Op1 (t, t', x_13687, x_13686) ->
    183   h_Op1 t t' x_13687 x_13686
    184     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13686)
    185 | Op2 (t1, t2, t', x_13690, x_13689, x_13688) ->
    186   h_Op2 t1 t2 t' x_13690 x_13689 x_13688
    187     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13689)
    188     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13688)
    189 | Mem (t, x_13691) ->
    190   h_Mem t x_13691
     179let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13695 = function
     180| Id (t, x_13697) -> h_Id t x_13697
     181| Cst (t, x_13698) -> h_Cst t x_13698
     182| Op1 (t, t', x_13700, x_13699) ->
     183  h_Op1 t t' x_13700 x_13699
     184    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13699)
     185| Op2 (t1, t2, t', x_13703, x_13702, x_13701) ->
     186  h_Op2 t1 t2 t' x_13703 x_13702 x_13701
     187    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13702)
     188    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13701)
     189| Mem (t, x_13704) ->
     190  h_Mem t x_13704
    191191    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    192       x_13691)
    193 | Cond (sz, sg, t, x_13694, x_13693, x_13692) ->
    194   h_Cond sz sg t x_13694 x_13693 x_13692
     192      x_13704)
     193| Cond (sz, sg, t, x_13707, x_13706, x_13705) ->
     194  h_Cond sz sg t x_13707 x_13706 x_13705
    195195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    196       (sz, sg)) x_13694)
    197     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13693)
    198     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13692)
    199 | Ecost (t, x_13696, x_13695) ->
    200   h_Ecost t x_13696 x_13695
    201     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13695)
     196      (sz, sg)) x_13707)
     197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13706)
     198    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13705)
     199| Ecost (t, x_13709, x_13708) ->
     200  h_Ecost t x_13709 x_13708
     201    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13708)
    202202
    203203(** val expr_rect_Type1 :
     
    209209    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    210210    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    211 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13704 = function
    212 | Id (t, x_13706) -> h_Id t x_13706
    213 | Cst (t, x_13707) -> h_Cst t x_13707
    214 | Op1 (t, t', x_13709, x_13708) ->
    215   h_Op1 t t' x_13709 x_13708
    216     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13708)
    217 | Op2 (t1, t2, t', x_13712, x_13711, x_13710) ->
    218   h_Op2 t1 t2 t' x_13712 x_13711 x_13710
    219     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13711)
    220     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13710)
    221 | Mem (t, x_13713) ->
    222   h_Mem t x_13713
     211let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13717 = function
     212| Id (t, x_13719) -> h_Id t x_13719
     213| Cst (t, x_13720) -> h_Cst t x_13720
     214| Op1 (t, t', x_13722, x_13721) ->
     215  h_Op1 t t' x_13722 x_13721
     216    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13721)
     217| Op2 (t1, t2, t', x_13725, x_13724, x_13723) ->
     218  h_Op2 t1 t2 t' x_13725 x_13724 x_13723
     219    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13724)
     220    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13723)
     221| Mem (t, x_13726) ->
     222  h_Mem t x_13726
    223223    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    224       x_13713)
    225 | Cond (sz, sg, t, x_13716, x_13715, x_13714) ->
    226   h_Cond sz sg t x_13716 x_13715 x_13714
     224      x_13726)
     225| Cond (sz, sg, t, x_13729, x_13728, x_13727) ->
     226  h_Cond sz sg t x_13729 x_13728 x_13727
    227227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    228       (sz, sg)) x_13716)
    229     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13715)
    230     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13714)
    231 | Ecost (t, x_13718, x_13717) ->
    232   h_Ecost t x_13718 x_13717
    233     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13717)
     228      (sz, sg)) x_13729)
     229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13728)
     230    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13727)
     231| Ecost (t, x_13731, x_13730) ->
     232  h_Ecost t x_13731 x_13730
     233    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13730)
    234234
    235235(** val expr_rect_Type0 :
     
    241241    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    242242    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    243 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13726 = function
    244 | Id (t, x_13728) -> h_Id t x_13728
    245 | Cst (t, x_13729) -> h_Cst t x_13729
    246 | Op1 (t, t', x_13731, x_13730) ->
    247   h_Op1 t t' x_13731 x_13730
    248     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13730)
    249 | Op2 (t1, t2, t', x_13734, x_13733, x_13732) ->
    250   h_Op2 t1 t2 t' x_13734 x_13733 x_13732
    251     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13733)
    252     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13732)
    253 | Mem (t, x_13735) ->
    254   h_Mem t x_13735
     243let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13739 = function
     244| Id (t, x_13741) -> h_Id t x_13741
     245| Cst (t, x_13742) -> h_Cst t x_13742
     246| Op1 (t, t', x_13744, x_13743) ->
     247  h_Op1 t t' x_13744 x_13743
     248    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13743)
     249| Op2 (t1, t2, t', x_13747, x_13746, x_13745) ->
     250  h_Op2 t1 t2 t' x_13747 x_13746 x_13745
     251    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13746)
     252    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13745)
     253| Mem (t, x_13748) ->
     254  h_Mem t x_13748
    255255    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    256       x_13735)
    257 | Cond (sz, sg, t, x_13738, x_13737, x_13736) ->
    258   h_Cond sz sg t x_13738 x_13737 x_13736
     256      x_13748)
     257| Cond (sz, sg, t, x_13751, x_13750, x_13749) ->
     258  h_Cond sz sg t x_13751 x_13750 x_13749
    259259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    260       (sz, sg)) x_13738)
    261     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13737)
    262     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13736)
    263 | Ecost (t, x_13740, x_13739) ->
    264   h_Ecost t x_13740 x_13739
    265     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13739)
     260      (sz, sg)) x_13751)
     261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13750)
     262    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13749)
     263| Ecost (t, x_13753, x_13752) ->
     264  h_Ecost t x_13753 x_13752
     265    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13752)
    266266
    267267(** val expr_inv_rect_Type4 :
     
    373373let 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
    374374| St_skip -> h_St_skip
    375 | St_assign (t, x_13911, x_13910) -> h_St_assign t x_13911 x_13910
    376 | St_store (t, x_13913, x_13912) -> h_St_store t x_13913 x_13912
    377 | St_call (x_13916, x_13915, x_13914) -> h_St_call x_13916 x_13915 x_13914
    378 | St_seq (x_13918, x_13917) ->
    379   h_St_seq x_13918 x_13917
     375| St_assign (t, x_13924, x_13923) -> h_St_assign t x_13924 x_13923
     376| St_store (t, x_13926, x_13925) -> h_St_store t x_13926 x_13925
     377| St_call (x_13929, x_13928, x_13927) -> h_St_call x_13929 x_13928 x_13927
     378| St_seq (x_13931, x_13930) ->
     379  h_St_seq x_13931 x_13930
    380380    (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_13918)
     381      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13931)
    382382    (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_13917)
    384 | St_ifthenelse (sz, sg, x_13921, x_13920, x_13919) ->
    385   h_St_ifthenelse sz sg x_13921 x_13920 x_13919
     383      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13930)
     384| St_ifthenelse (sz, sg, x_13934, x_13933, x_13932) ->
     385  h_St_ifthenelse sz sg x_13934 x_13933 x_13932
    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_13920)
     387      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13933)
    388388    (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_13919)
    390 | St_return x_13922 -> h_St_return x_13922
    391 | St_label (x_13924, x_13923) ->
    392   h_St_label x_13924 x_13923
     389      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13932)
     390| St_return x_13935 -> h_St_return x_13935
     391| St_label (x_13937, x_13936) ->
     392  h_St_label x_13937 x_13936
    393393    (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_13923)
    395 | St_goto x_13925 -> h_St_goto x_13925
    396 | St_cost (x_13927, x_13926) ->
    397   h_St_cost x_13927 x_13926
     394      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13936)
     395| St_goto x_13938 -> h_St_goto x_13938
     396| St_cost (x_13940, x_13939) ->
     397  h_St_cost x_13940 x_13939
    398398    (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_13926)
     399      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13939)
    400400
    401401(** val stmt_rect_Type3 :
     
    410410let 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
    411411| St_skip -> h_St_skip
    412 | St_assign (t, x_13969, x_13968) -> h_St_assign t x_13969 x_13968
    413 | St_store (t, x_13971, x_13970) -> h_St_store t x_13971 x_13970
    414 | St_call (x_13974, x_13973, x_13972) -> h_St_call x_13974 x_13973 x_13972
    415 | St_seq (x_13976, x_13975) ->
    416   h_St_seq x_13976 x_13975
     412| St_assign (t, x_13982, x_13981) -> h_St_assign t x_13982 x_13981
     413| St_store (t, x_13984, x_13983) -> h_St_store t x_13984 x_13983
     414| St_call (x_13987, x_13986, x_13985) -> h_St_call x_13987 x_13986 x_13985
     415| St_seq (x_13989, x_13988) ->
     416  h_St_seq x_13989 x_13988
    417417    (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_13976)
     418      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13989)
    419419    (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_13975)
    421 | St_ifthenelse (sz, sg, x_13979, x_13978, x_13977) ->
    422   h_St_ifthenelse sz sg x_13979 x_13978 x_13977
     420      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13988)
     421| St_ifthenelse (sz, sg, x_13992, x_13991, x_13990) ->
     422  h_St_ifthenelse sz sg x_13992 x_13991 x_13990
    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_13978)
     424      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13991)
    425425    (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_13977)
    427 | St_return x_13980 -> h_St_return x_13980
    428 | St_label (x_13982, x_13981) ->
    429   h_St_label x_13982 x_13981
     426      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13990)
     427| St_return x_13993 -> h_St_return x_13993
     428| St_label (x_13995, x_13994) ->
     429  h_St_label x_13995 x_13994
    430430    (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_13981)
    432 | St_goto x_13983 -> h_St_goto x_13983
    433 | St_cost (x_13985, x_13984) ->
    434   h_St_cost x_13985 x_13984
     431      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13994)
     432| St_goto x_13996 -> h_St_goto x_13996
     433| St_cost (x_13998, x_13997) ->
     434  h_St_cost x_13998 x_13997
    435435    (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_13984)
     436      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13997)
    437437
    438438(** val stmt_rect_Type2 :
     
    447447let 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
    448448| St_skip -> h_St_skip
    449 | St_assign (t, x_13998, x_13997) -> h_St_assign t x_13998 x_13997
    450 | St_store (t, x_14000, x_13999) -> h_St_store t x_14000 x_13999
    451 | St_call (x_14003, x_14002, x_14001) -> h_St_call x_14003 x_14002 x_14001
    452 | St_seq (x_14005, x_14004) ->
    453   h_St_seq x_14005 x_14004
     449| St_assign (t, x_14011, x_14010) -> h_St_assign t x_14011 x_14010
     450| St_store (t, x_14013, x_14012) -> h_St_store t x_14013 x_14012
     451| St_call (x_14016, x_14015, x_14014) -> h_St_call x_14016 x_14015 x_14014
     452| St_seq (x_14018, x_14017) ->
     453  h_St_seq x_14018 x_14017
    454454    (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_14005)
     455      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14018)
    456456    (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_14004)
    458 | St_ifthenelse (sz, sg, x_14008, x_14007, x_14006) ->
    459   h_St_ifthenelse sz sg x_14008 x_14007 x_14006
     457      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14017)
     458| St_ifthenelse (sz, sg, x_14021, x_14020, x_14019) ->
     459  h_St_ifthenelse sz sg x_14021 x_14020 x_14019
    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_14007)
     461      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14020)
    462462    (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_14006)
    464 | St_return x_14009 -> h_St_return x_14009
    465 | St_label (x_14011, x_14010) ->
    466   h_St_label x_14011 x_14010
     463      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14019)
     464| St_return x_14022 -> h_St_return x_14022
     465| St_label (x_14024, x_14023) ->
     466  h_St_label x_14024 x_14023
    467467    (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_14010)
    469 | St_goto x_14012 -> h_St_goto x_14012
    470 | St_cost (x_14014, x_14013) ->
    471   h_St_cost x_14014 x_14013
     468      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14023)
     469| St_goto x_14025 -> h_St_goto x_14025
     470| St_cost (x_14027, x_14026) ->
     471  h_St_cost x_14027 x_14026
    472472    (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_14013)
     473      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14026)
    474474
    475475(** val stmt_rect_Type1 :
     
    484484let 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
    485485| St_skip -> h_St_skip
    486 | St_assign (t, x_14027, x_14026) -> h_St_assign t x_14027 x_14026
    487 | St_store (t, x_14029, x_14028) -> h_St_store t x_14029 x_14028
    488 | St_call (x_14032, x_14031, x_14030) -> h_St_call x_14032 x_14031 x_14030
    489 | St_seq (x_14034, x_14033) ->
    490   h_St_seq x_14034 x_14033
     486| St_assign (t, x_14040, x_14039) -> h_St_assign t x_14040 x_14039
     487| St_store (t, x_14042, x_14041) -> h_St_store t x_14042 x_14041
     488| St_call (x_14045, x_14044, x_14043) -> h_St_call x_14045 x_14044 x_14043
     489| St_seq (x_14047, x_14046) ->
     490  h_St_seq x_14047 x_14046
    491491    (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_14034)
     492      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14047)
    493493    (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_14033)
    495 | St_ifthenelse (sz, sg, x_14037, x_14036, x_14035) ->
    496   h_St_ifthenelse sz sg x_14037 x_14036 x_14035
     494      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14046)
     495| St_ifthenelse (sz, sg, x_14050, x_14049, x_14048) ->
     496  h_St_ifthenelse sz sg x_14050 x_14049 x_14048
    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_14036)
     498      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049)
    499499    (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_14035)
    501 | St_return x_14038 -> h_St_return x_14038
    502 | St_label (x_14040, x_14039) ->
    503   h_St_label x_14040 x_14039
     500      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14048)
     501| St_return x_14051 -> h_St_return x_14051
     502| St_label (x_14053, x_14052) ->
     503  h_St_label x_14053 x_14052
    504504    (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_14039)
    506 | St_goto x_14041 -> h_St_goto x_14041
    507 | St_cost (x_14043, x_14042) ->
    508   h_St_cost x_14043 x_14042
     505      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14052)
     506| St_goto x_14054 -> h_St_goto x_14054
     507| St_cost (x_14056, x_14055) ->
     508  h_St_cost x_14056 x_14055
    509509    (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_14042)
     510      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14055)
    511511
    512512(** val stmt_rect_Type0 :
     
    521521let 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
    522522| St_skip -> h_St_skip
    523 | St_assign (t, x_14056, x_14055) -> h_St_assign t x_14056 x_14055
    524 | St_store (t, x_14058, x_14057) -> h_St_store t x_14058 x_14057
    525 | St_call (x_14061, x_14060, x_14059) -> h_St_call x_14061 x_14060 x_14059
    526 | St_seq (x_14063, x_14062) ->
    527   h_St_seq x_14063 x_14062
     523| St_assign (t, x_14069, x_14068) -> h_St_assign t x_14069 x_14068
     524| St_store (t, x_14071, x_14070) -> h_St_store t x_14071 x_14070
     525| St_call (x_14074, x_14073, x_14072) -> h_St_call x_14074 x_14073 x_14072
     526| St_seq (x_14076, x_14075) ->
     527  h_St_seq x_14076 x_14075
    528528    (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_14063)
     529      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14076)
    530530    (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_14062)
    532 | St_ifthenelse (sz, sg, x_14066, x_14065, x_14064) ->
    533   h_St_ifthenelse sz sg x_14066 x_14065 x_14064
     531      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14075)
     532| St_ifthenelse (sz, sg, x_14079, x_14078, x_14077) ->
     533  h_St_ifthenelse sz sg x_14079 x_14078 x_14077
    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_14065)
     535      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14078)
    536536    (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_14064)
    538 | St_return x_14067 -> h_St_return x_14067
    539 | St_label (x_14069, x_14068) ->
    540   h_St_label x_14069 x_14068
     537      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14077)
     538| St_return x_14080 -> h_St_return x_14080
     539| St_label (x_14082, x_14081) ->
     540  h_St_label x_14082 x_14081
    541541    (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_14068)
    543 | St_goto x_14070 -> h_St_goto x_14070
    544 | St_cost (x_14072, x_14071) ->
    545   h_St_cost x_14072 x_14071
     542      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14081)
     543| St_goto x_14083 -> h_St_goto x_14083
     544| St_cost (x_14085, x_14084) ->
     545  h_St_cost x_14085 x_14084
    546546    (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_14071)
     547      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14084)
    548548
    549549(** val stmt_inv_rect_Type4 :
     
    757757    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    758758    -> 'a1) -> internal_function -> 'a1 **)
    759 let rec internal_function_rect_Type4 h_mk_internal_function x_14367 =
     759let rec internal_function_rect_Type4 h_mk_internal_function x_14380 =
    760760  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    761     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14367
     761    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14380
    762762  in
    763763  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    768768    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    769769    -> 'a1) -> internal_function -> 'a1 **)
    770 let rec internal_function_rect_Type5 h_mk_internal_function x_14369 =
     770let rec internal_function_rect_Type5 h_mk_internal_function x_14382 =
    771771  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    772     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14369
     772    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14382
    773773  in
    774774  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    779779    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    780780    -> 'a1) -> internal_function -> 'a1 **)
    781 let rec internal_function_rect_Type3 h_mk_internal_function x_14371 =
     781let rec internal_function_rect_Type3 h_mk_internal_function x_14384 =
    782782  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    783     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14371
     783    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14384
    784784  in
    785785  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    790790    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    791791    -> 'a1) -> internal_function -> 'a1 **)
    792 let rec internal_function_rect_Type2 h_mk_internal_function x_14373 =
     792let rec internal_function_rect_Type2 h_mk_internal_function x_14386 =
    793793  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    794     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14373
     794    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14386
    795795  in
    796796  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    801801    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    802802    -> 'a1) -> internal_function -> 'a1 **)
    803 let rec internal_function_rect_Type1 h_mk_internal_function x_14375 =
     803let rec internal_function_rect_Type1 h_mk_internal_function x_14388 =
    804804  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    805     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14375
     805    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14388
    806806  in
    807807  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    812812    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    813813    -> 'a1) -> internal_function -> 'a1 **)
    814 let rec internal_function_rect_Type0 h_mk_internal_function x_14377 =
     814let rec internal_function_rect_Type0 h_mk_internal_function x_14390 =
    815815  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    816     f_stacksize = f_stacksize0; f_body = f_body0 } = x_14377
     816    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14390
    817817  in
    818818  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
Note: See TracChangeset for help on using the changeset viewer.