Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_syntax.ml

    r2601 r2649  
    2323open Identifiers
    2424
    25 open Floats
    26 
    2725open Integers
    2826
     
    4745open Pointers
    4846
     47open ErrorMessages
     48
    4949open Option
    5050
     
    5454
    5555open Positive
    56 
    57 open Char
    58 
    59 open String
    6056
    6157open PreIdentifiers
     
    115111    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    116112    -> '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_12680 = function
    118 | Id (t, x_12682) -> h_Id t x_12682
    119 | Cst (t, x_12683) -> h_Cst t x_12683
    120 | Op1 (t, t', x_12685, x_12684) ->
    121   h_Op1 t t' x_12685 x_12684
    122     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12684)
    123 | Op2 (t1, t2, t', x_12688, x_12687, x_12686) ->
    124   h_Op2 t1 t2 t' x_12688 x_12687 x_12686
    125     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_12687)
    126     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_12686)
    127 | Mem (t, x_12689) ->
    128   h_Mem t x_12689
     113let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10365 = function
     114| Id (t, x_10367) -> h_Id t x_10367
     115| Cst (t, x_10368) -> h_Cst t x_10368
     116| Op1 (t, t', x_10370, x_10369) ->
     117  h_Op1 t t' x_10370 x_10369
     118    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10369)
     119| Op2 (t1, t2, t', x_10373, x_10372, x_10371) ->
     120  h_Op2 t1 t2 t' x_10373 x_10372 x_10371
     121    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10372)
     122    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10371)
     123| Mem (t, x_10374) ->
     124  h_Mem t x_10374
    129125    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    130       x_12689)
    131 | Cond (sz, sg, t, x_12692, x_12691, x_12690) ->
    132   h_Cond sz sg t x_12692 x_12691 x_12690
     126      x_10374)
     127| Cond (sz, sg, t, x_10377, x_10376, x_10375) ->
     128  h_Cond sz sg t x_10377 x_10376 x_10375
    133129    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    134       (sz, sg)) x_12692)
    135     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12691)
    136     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12690)
    137 | Ecost (t, x_12694, x_12693) ->
    138   h_Ecost t x_12694 x_12693
    139     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12693)
     130      (sz, sg)) x_10377)
     131    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10376)
     132    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10375)
     133| Ecost (t, x_10379, x_10378) ->
     134  h_Ecost t x_10379 x_10378
     135    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10378)
    140136
    141137(** val expr_rect_Type3 :
     
    147143    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    148144    -> '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_12724 = function
    150 | Id (t, x_12726) -> h_Id t x_12726
    151 | Cst (t, x_12727) -> h_Cst t x_12727
    152 | Op1 (t, t', x_12729, x_12728) ->
    153   h_Op1 t t' x_12729 x_12728
    154     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12728)
    155 | Op2 (t1, t2, t', x_12732, x_12731, x_12730) ->
    156   h_Op2 t1 t2 t' x_12732 x_12731 x_12730
    157     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_12731)
    158     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_12730)
    159 | Mem (t, x_12733) ->
    160   h_Mem t x_12733
     145let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10409 = function
     146| Id (t, x_10411) -> h_Id t x_10411
     147| Cst (t, x_10412) -> h_Cst t x_10412
     148| Op1 (t, t', x_10414, x_10413) ->
     149  h_Op1 t t' x_10414 x_10413
     150    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10413)
     151| Op2 (t1, t2, t', x_10417, x_10416, x_10415) ->
     152  h_Op2 t1 t2 t' x_10417 x_10416 x_10415
     153    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10416)
     154    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10415)
     155| Mem (t, x_10418) ->
     156  h_Mem t x_10418
    161157    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    162       x_12733)
    163 | Cond (sz, sg, t, x_12736, x_12735, x_12734) ->
    164   h_Cond sz sg t x_12736 x_12735 x_12734
     158      x_10418)
     159| Cond (sz, sg, t, x_10421, x_10420, x_10419) ->
     160  h_Cond sz sg t x_10421 x_10420 x_10419
    165161    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    166       (sz, sg)) x_12736)
    167     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12735)
    168     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12734)
    169 | Ecost (t, x_12738, x_12737) ->
    170   h_Ecost t x_12738 x_12737
    171     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12737)
     162      (sz, sg)) x_10421)
     163    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10420)
     164    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10419)
     165| Ecost (t, x_10423, x_10422) ->
     166  h_Ecost t x_10423 x_10422
     167    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10422)
    172168
    173169(** val expr_rect_Type2 :
     
    179175    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    180176    -> '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_12746 = function
    182 | Id (t, x_12748) -> h_Id t x_12748
    183 | Cst (t, x_12749) -> h_Cst t x_12749
    184 | Op1 (t, t', x_12751, x_12750) ->
    185   h_Op1 t t' x_12751 x_12750
    186     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12750)
    187 | Op2 (t1, t2, t', x_12754, x_12753, x_12752) ->
    188   h_Op2 t1 t2 t' x_12754 x_12753 x_12752
    189     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_12753)
    190     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_12752)
    191 | Mem (t, x_12755) ->
    192   h_Mem t x_12755
     177let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10431 = function
     178| Id (t, x_10433) -> h_Id t x_10433
     179| Cst (t, x_10434) -> h_Cst t x_10434
     180| Op1 (t, t', x_10436, x_10435) ->
     181  h_Op1 t t' x_10436 x_10435
     182    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10435)
     183| Op2 (t1, t2, t', x_10439, x_10438, x_10437) ->
     184  h_Op2 t1 t2 t' x_10439 x_10438 x_10437
     185    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10438)
     186    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10437)
     187| Mem (t, x_10440) ->
     188  h_Mem t x_10440
    193189    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    194       x_12755)
    195 | Cond (sz, sg, t, x_12758, x_12757, x_12756) ->
    196   h_Cond sz sg t x_12758 x_12757 x_12756
     190      x_10440)
     191| Cond (sz, sg, t, x_10443, x_10442, x_10441) ->
     192  h_Cond sz sg t x_10443 x_10442 x_10441
    197193    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    198       (sz, sg)) x_12758)
    199     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12757)
    200     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12756)
    201 | Ecost (t, x_12760, x_12759) ->
    202   h_Ecost t x_12760 x_12759
    203     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12759)
     194      (sz, sg)) x_10443)
     195    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10442)
     196    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10441)
     197| Ecost (t, x_10445, x_10444) ->
     198  h_Ecost t x_10445 x_10444
     199    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10444)
    204200
    205201(** val expr_rect_Type1 :
     
    211207    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    212208    -> '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_12768 = function
    214 | Id (t, x_12770) -> h_Id t x_12770
    215 | Cst (t, x_12771) -> h_Cst t x_12771
    216 | Op1 (t, t', x_12773, x_12772) ->
    217   h_Op1 t t' x_12773 x_12772
    218     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12772)
    219 | Op2 (t1, t2, t', x_12776, x_12775, x_12774) ->
    220   h_Op2 t1 t2 t' x_12776 x_12775 x_12774
    221     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_12775)
    222     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_12774)
    223 | Mem (t, x_12777) ->
    224   h_Mem t x_12777
     209let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10453 = function
     210| Id (t, x_10455) -> h_Id t x_10455
     211| Cst (t, x_10456) -> h_Cst t x_10456
     212| Op1 (t, t', x_10458, x_10457) ->
     213  h_Op1 t t' x_10458 x_10457
     214    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10457)
     215| Op2 (t1, t2, t', x_10461, x_10460, x_10459) ->
     216  h_Op2 t1 t2 t' x_10461 x_10460 x_10459
     217    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10460)
     218    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10459)
     219| Mem (t, x_10462) ->
     220  h_Mem t x_10462
    225221    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    226       x_12777)
    227 | Cond (sz, sg, t, x_12780, x_12779, x_12778) ->
    228   h_Cond sz sg t x_12780 x_12779 x_12778
     222      x_10462)
     223| Cond (sz, sg, t, x_10465, x_10464, x_10463) ->
     224  h_Cond sz sg t x_10465 x_10464 x_10463
    229225    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    230       (sz, sg)) x_12780)
    231     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12779)
    232     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12778)
    233 | Ecost (t, x_12782, x_12781) ->
    234   h_Ecost t x_12782 x_12781
    235     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12781)
     226      (sz, sg)) x_10465)
     227    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10464)
     228    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10463)
     229| Ecost (t, x_10467, x_10466) ->
     230  h_Ecost t x_10467 x_10466
     231    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10466)
    236232
    237233(** val expr_rect_Type0 :
     
    243239    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    244240    -> '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_12790 = function
    246 | Id (t, x_12792) -> h_Id t x_12792
    247 | Cst (t, x_12793) -> h_Cst t x_12793
    248 | Op1 (t, t', x_12795, x_12794) ->
    249   h_Op1 t t' x_12795 x_12794
    250     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12794)
    251 | Op2 (t1, t2, t', x_12798, x_12797, x_12796) ->
    252   h_Op2 t1 t2 t' x_12798 x_12797 x_12796
    253     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_12797)
    254     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_12796)
    255 | Mem (t, x_12799) ->
    256   h_Mem t x_12799
     241let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10475 = function
     242| Id (t, x_10477) -> h_Id t x_10477
     243| Cst (t, x_10478) -> h_Cst t x_10478
     244| Op1 (t, t', x_10480, x_10479) ->
     245  h_Op1 t t' x_10480 x_10479
     246    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10479)
     247| Op2 (t1, t2, t', x_10483, x_10482, x_10481) ->
     248  h_Op2 t1 t2 t' x_10483 x_10482 x_10481
     249    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10482)
     250    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10481)
     251| Mem (t, x_10484) ->
     252  h_Mem t x_10484
    257253    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    258       x_12799)
    259 | Cond (sz, sg, t, x_12802, x_12801, x_12800) ->
    260   h_Cond sz sg t x_12802 x_12801 x_12800
     254      x_10484)
     255| Cond (sz, sg, t, x_10487, x_10486, x_10485) ->
     256  h_Cond sz sg t x_10487 x_10486 x_10485
    261257    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    262       (sz, sg)) x_12802)
    263     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12801)
    264     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12800)
    265 | Ecost (t, x_12804, x_12803) ->
    266   h_Ecost t x_12804 x_12803
    267     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_12803)
     258      (sz, sg)) x_10487)
     259    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10486)
     260    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10485)
     261| Ecost (t, x_10489, x_10488) ->
     262  h_Ecost t x_10489 x_10488
     263    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10488)
    268264
    269265(** val expr_inv_rect_Type4 :
     
    353349type expr_vars = __
    354350
    355 (** val label : String.string **)
    356 let label = "Label"
    357   (*failwith "AXIOM TO BE REALIZED"*)
    358 
    359351type stmt =
    360352| St_skip
     
    381373let 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
    382374| St_skip -> h_St_skip
    383 | St_assign (t, x_12975, x_12974) -> h_St_assign t x_12975 x_12974
    384 | St_store (t, x_12977, x_12976) -> h_St_store t x_12977 x_12976
    385 | St_call (x_12980, x_12979, x_12978) -> h_St_call x_12980 x_12979 x_12978
    386 | St_seq (x_12982, x_12981) ->
    387   h_St_seq x_12982 x_12981
     375| St_assign (t, x_10660, x_10659) -> h_St_assign t x_10660 x_10659
     376| St_store (t, x_10662, x_10661) -> h_St_store t x_10662 x_10661
     377| St_call (x_10665, x_10664, x_10663) -> h_St_call x_10665 x_10664 x_10663
     378| St_seq (x_10667, x_10666) ->
     379  h_St_seq x_10667 x_10666
    388380    (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_12982)
     381      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10667)
    390382    (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_12981)
    392 | St_ifthenelse (sz, sg, x_12985, x_12984, x_12983) ->
    393   h_St_ifthenelse sz sg x_12985 x_12984 x_12983
     383      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10666)
     384| St_ifthenelse (sz, sg, x_10670, x_10669, x_10668) ->
     385  h_St_ifthenelse sz sg x_10670 x_10669 x_10668
    394386    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    395       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_12984)
     387      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10669)
    396388    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    397       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_12983)
    398 | St_return x_12986 -> h_St_return x_12986
    399 | St_label (x_12988, x_12987) ->
    400   h_St_label x_12988 x_12987
     389      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10668)
     390| St_return x_10671 -> h_St_return x_10671
     391| St_label (x_10673, x_10672) ->
     392  h_St_label x_10673 x_10672
    401393    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    402       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_12987)
    403 | St_goto x_12989 -> h_St_goto x_12989
    404 | St_cost (x_12991, x_12990) ->
    405   h_St_cost x_12991 x_12990
     394      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10672)
     395| St_goto x_10674 -> h_St_goto x_10674
     396| St_cost (x_10676, x_10675) ->
     397  h_St_cost x_10676 x_10675
    406398    (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    407       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_12990)
     399      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10675)
    408400
    409401(** val stmt_rect_Type3 :
     
    418410let 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
    419411| St_skip -> h_St_skip
    420 | St_assign (t, x_13033, x_13032) -> h_St_assign t x_13033 x_13032
    421 | St_store (t, x_13035, x_13034) -> h_St_store t x_13035 x_13034
    422 | St_call (x_13038, x_13037, x_13036) -> h_St_call x_13038 x_13037 x_13036
    423 | St_seq (x_13040, x_13039) ->
    424   h_St_seq x_13040 x_13039
     412| St_assign (t, x_10718, x_10717) -> h_St_assign t x_10718 x_10717
     413| St_store (t, x_10720, x_10719) -> h_St_store t x_10720 x_10719
     414| St_call (x_10723, x_10722, x_10721) -> h_St_call x_10723 x_10722 x_10721
     415| St_seq (x_10725, x_10724) ->
     416  h_St_seq x_10725 x_10724
    425417    (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_13040)
     418      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10725)
    427419    (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_13039)
    429 | St_ifthenelse (sz, sg, x_13043, x_13042, x_13041) ->
    430   h_St_ifthenelse sz sg x_13043 x_13042 x_13041
     420      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10724)
     421| St_ifthenelse (sz, sg, x_10728, x_10727, x_10726) ->
     422  h_St_ifthenelse sz sg x_10728 x_10727 x_10726
    431423    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    432       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13042)
     424      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10727)
    433425    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    434       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13041)
    435 | St_return x_13044 -> h_St_return x_13044
    436 | St_label (x_13046, x_13045) ->
    437   h_St_label x_13046 x_13045
     426      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10726)
     427| St_return x_10729 -> h_St_return x_10729
     428| St_label (x_10731, x_10730) ->
     429  h_St_label x_10731 x_10730
    438430    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    439       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13045)
    440 | St_goto x_13047 -> h_St_goto x_13047
    441 | St_cost (x_13049, x_13048) ->
    442   h_St_cost x_13049 x_13048
     431      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10730)
     432| St_goto x_10732 -> h_St_goto x_10732
     433| St_cost (x_10734, x_10733) ->
     434  h_St_cost x_10734 x_10733
    443435    (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    444       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13048)
     436      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10733)
    445437
    446438(** val stmt_rect_Type2 :
     
    455447let 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
    456448| St_skip -> h_St_skip
    457 | St_assign (t, x_13062, x_13061) -> h_St_assign t x_13062 x_13061
    458 | St_store (t, x_13064, x_13063) -> h_St_store t x_13064 x_13063
    459 | St_call (x_13067, x_13066, x_13065) -> h_St_call x_13067 x_13066 x_13065
    460 | St_seq (x_13069, x_13068) ->
    461   h_St_seq x_13069 x_13068
     449| St_assign (t, x_10747, x_10746) -> h_St_assign t x_10747 x_10746
     450| St_store (t, x_10749, x_10748) -> h_St_store t x_10749 x_10748
     451| St_call (x_10752, x_10751, x_10750) -> h_St_call x_10752 x_10751 x_10750
     452| St_seq (x_10754, x_10753) ->
     453  h_St_seq x_10754 x_10753
    462454    (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_13069)
     455      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10754)
    464456    (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_13068)
    466 | St_ifthenelse (sz, sg, x_13072, x_13071, x_13070) ->
    467   h_St_ifthenelse sz sg x_13072 x_13071 x_13070
     457      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10753)
     458| St_ifthenelse (sz, sg, x_10757, x_10756, x_10755) ->
     459  h_St_ifthenelse sz sg x_10757 x_10756 x_10755
    468460    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    469       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13071)
     461      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10756)
    470462    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    471       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13070)
    472 | St_return x_13073 -> h_St_return x_13073
    473 | St_label (x_13075, x_13074) ->
    474   h_St_label x_13075 x_13074
     463      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10755)
     464| St_return x_10758 -> h_St_return x_10758
     465| St_label (x_10760, x_10759) ->
     466  h_St_label x_10760 x_10759
    475467    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    476       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13074)
    477 | St_goto x_13076 -> h_St_goto x_13076
    478 | St_cost (x_13078, x_13077) ->
    479   h_St_cost x_13078 x_13077
     468      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10759)
     469| St_goto x_10761 -> h_St_goto x_10761
     470| St_cost (x_10763, x_10762) ->
     471  h_St_cost x_10763 x_10762
    480472    (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    481       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13077)
     473      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10762)
    482474
    483475(** val stmt_rect_Type1 :
     
    492484let 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
    493485| St_skip -> h_St_skip
    494 | St_assign (t, x_13091, x_13090) -> h_St_assign t x_13091 x_13090
    495 | St_store (t, x_13093, x_13092) -> h_St_store t x_13093 x_13092
    496 | St_call (x_13096, x_13095, x_13094) -> h_St_call x_13096 x_13095 x_13094
    497 | St_seq (x_13098, x_13097) ->
    498   h_St_seq x_13098 x_13097
     486| St_assign (t, x_10776, x_10775) -> h_St_assign t x_10776 x_10775
     487| St_store (t, x_10778, x_10777) -> h_St_store t x_10778 x_10777
     488| St_call (x_10781, x_10780, x_10779) -> h_St_call x_10781 x_10780 x_10779
     489| St_seq (x_10783, x_10782) ->
     490  h_St_seq x_10783 x_10782
    499491    (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_13098)
     492      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10783)
    501493    (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_13097)
    503 | St_ifthenelse (sz, sg, x_13101, x_13100, x_13099) ->
    504   h_St_ifthenelse sz sg x_13101 x_13100 x_13099
     494      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10782)
     495| St_ifthenelse (sz, sg, x_10786, x_10785, x_10784) ->
     496  h_St_ifthenelse sz sg x_10786 x_10785 x_10784
    505497    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    506       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13100)
     498      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10785)
    507499    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    508       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13099)
    509 | St_return x_13102 -> h_St_return x_13102
    510 | St_label (x_13104, x_13103) ->
    511   h_St_label x_13104 x_13103
     500      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10784)
     501| St_return x_10787 -> h_St_return x_10787
     502| St_label (x_10789, x_10788) ->
     503  h_St_label x_10789 x_10788
    512504    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    513       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13103)
    514 | St_goto x_13105 -> h_St_goto x_13105
    515 | St_cost (x_13107, x_13106) ->
    516   h_St_cost x_13107 x_13106
     505      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10788)
     506| St_goto x_10790 -> h_St_goto x_10790
     507| St_cost (x_10792, x_10791) ->
     508  h_St_cost x_10792 x_10791
    517509    (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    518       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13106)
     510      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10791)
    519511
    520512(** val stmt_rect_Type0 :
     
    529521let 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
    530522| St_skip -> h_St_skip
    531 | St_assign (t, x_13120, x_13119) -> h_St_assign t x_13120 x_13119
    532 | St_store (t, x_13122, x_13121) -> h_St_store t x_13122 x_13121
    533 | St_call (x_13125, x_13124, x_13123) -> h_St_call x_13125 x_13124 x_13123
    534 | St_seq (x_13127, x_13126) ->
    535   h_St_seq x_13127 x_13126
     523| St_assign (t, x_10805, x_10804) -> h_St_assign t x_10805 x_10804
     524| St_store (t, x_10807, x_10806) -> h_St_store t x_10807 x_10806
     525| St_call (x_10810, x_10809, x_10808) -> h_St_call x_10810 x_10809 x_10808
     526| St_seq (x_10812, x_10811) ->
     527  h_St_seq x_10812 x_10811
    536528    (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_13127)
     529      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10812)
    538530    (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_13126)
    540 | St_ifthenelse (sz, sg, x_13130, x_13129, x_13128) ->
    541   h_St_ifthenelse sz sg x_13130 x_13129 x_13128
     531      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10811)
     532| St_ifthenelse (sz, sg, x_10815, x_10814, x_10813) ->
     533  h_St_ifthenelse sz sg x_10815 x_10814 x_10813
    542534    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    543       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13129)
     535      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10814)
    544536    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    545       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13128)
    546 | St_return x_13131 -> h_St_return x_13131
    547 | St_label (x_13133, x_13132) ->
    548   h_St_label x_13133 x_13132
     537      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10813)
     538| St_return x_10816 -> h_St_return x_10816
     539| St_label (x_10818, x_10817) ->
     540  h_St_label x_10818 x_10817
    549541    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    550       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13132)
    551 | St_goto x_13134 -> h_St_goto x_13134
    552 | St_cost (x_13136, x_13135) ->
    553   h_St_cost x_13136 x_13135
     542      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10817)
     543| St_goto x_10819 -> h_St_goto x_10819
     544| St_cost (x_10821, x_10820) ->
     545  h_St_cost x_10821 x_10820
    554546    (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
    555       h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13135)
     547      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_10820)
    556548
    557549(** val stmt_inv_rect_Type4 :
     
    767759    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    768760    -> 'a1) -> internal_function -> 'a1 **)
    769 let rec internal_function_rect_Type4 h_mk_internal_function x_13431 =
     761let rec internal_function_rect_Type4 h_mk_internal_function x_11116 =
    770762  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    771     f_stacksize = f_stacksize0; f_body = f_body0 } = x_13431
     763    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11116
    772764  in
    773765  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    778770    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    779771    -> 'a1) -> internal_function -> 'a1 **)
    780 let rec internal_function_rect_Type5 h_mk_internal_function x_13433 =
     772let rec internal_function_rect_Type5 h_mk_internal_function x_11118 =
    781773  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    782     f_stacksize = f_stacksize0; f_body = f_body0 } = x_13433
     774    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11118
    783775  in
    784776  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    789781    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    790782    -> 'a1) -> internal_function -> 'a1 **)
    791 let rec internal_function_rect_Type3 h_mk_internal_function x_13435 =
     783let rec internal_function_rect_Type3 h_mk_internal_function x_11120 =
    792784  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    793     f_stacksize = f_stacksize0; f_body = f_body0 } = x_13435
     785    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11120
    794786  in
    795787  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    800792    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    801793    -> 'a1) -> internal_function -> 'a1 **)
    802 let rec internal_function_rect_Type2 h_mk_internal_function x_13437 =
     794let rec internal_function_rect_Type2 h_mk_internal_function x_11122 =
    803795  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    804     f_stacksize = f_stacksize0; f_body = f_body0 } = x_13437
     796    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11122
    805797  in
    806798  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    811803    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    812804    -> 'a1) -> internal_function -> 'a1 **)
    813 let rec internal_function_rect_Type1 h_mk_internal_function x_13439 =
     805let rec internal_function_rect_Type1 h_mk_internal_function x_11124 =
    814806  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    815     f_stacksize = f_stacksize0; f_body = f_body0 } = x_13439
     807    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11124
    816808  in
    817809  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    822814    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    823815    -> 'a1) -> internal_function -> 'a1 **)
    824 let rec internal_function_rect_Type0 h_mk_internal_function x_13441 =
     816let rec internal_function_rect_Type0 h_mk_internal_function x_11126 =
    825817  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    826     f_stacksize = f_stacksize0; f_body = f_body0 } = x_13441
     818    f_stacksize = f_stacksize0; f_body = f_body0 } = x_11126
    827819  in
    828820  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
Note: See TracChangeset for help on using the changeset viewer.