Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_syntax.ml

    r2649 r2717  
    2929open Division
    3030
     31open Exp
     32
    3133open Arithmetic
    3234
     
    9092
    9193open FrontEndOps
     94
     95open BitVectorTrie
    9296
    9397open CostLabel
     
    111115    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    112116    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    113 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10365 = function
    114 | Id (t, x_10367) -> h_Id t x_10367
    115 | Cst (t, x_10368) -> h_Cst t x_10368
    116 | Op1 (t, t', x_10370, x_10369) ->
    117   h_Op1 t t' x_10370 x_10369
    118     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10369)
    119 | Op2 (t1, t2, t', x_10373, x_10372, x_10371) ->
    120   h_Op2 t1 t2 t' x_10373 x_10372 x_10371
    121     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10372)
    122     (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10371)
    123 | Mem (t, x_10374) ->
    124   h_Mem t x_10374
     117let 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
    125129    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    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
     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
    129133    (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    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)
     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)
    136140
    137141(** val expr_rect_Type3 :
     
    143147    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    144148    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    145 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10409 = function
    146 | Id (t, x_10411) -> h_Id t x_10411
    147 | Cst (t, x_10412) -> h_Cst t x_10412
    148 | Op1 (t, t', x_10414, x_10413) ->
    149   h_Op1 t t' x_10414 x_10413
    150     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10413)
    151 | Op2 (t1, t2, t', x_10417, x_10416, x_10415) ->
    152   h_Op2 t1 t2 t' x_10417 x_10416 x_10415
    153     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10416)
    154     (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10415)
    155 | Mem (t, x_10418) ->
    156   h_Mem t x_10418
     149let 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
    157161    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    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
     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
    161165    (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    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)
     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)
    168172
    169173(** val expr_rect_Type2 :
     
    175179    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    176180    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    177 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10431 = function
    178 | Id (t, x_10433) -> h_Id t x_10433
    179 | Cst (t, x_10434) -> h_Cst t x_10434
    180 | Op1 (t, t', x_10436, x_10435) ->
    181   h_Op1 t t' x_10436 x_10435
    182     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10435)
    183 | Op2 (t1, t2, t', x_10439, x_10438, x_10437) ->
    184   h_Op2 t1 t2 t' x_10439 x_10438 x_10437
    185     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10438)
    186     (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10437)
    187 | Mem (t, x_10440) ->
    188   h_Mem t x_10440
     181let 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
    189193    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    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
     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
    193197    (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    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)
     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)
    200204
    201205(** val expr_rect_Type1 :
     
    207211    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    208212    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    209 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10453 = function
    210 | Id (t, x_10455) -> h_Id t x_10455
    211 | Cst (t, x_10456) -> h_Cst t x_10456
    212 | Op1 (t, t', x_10458, x_10457) ->
    213   h_Op1 t t' x_10458 x_10457
    214     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10457)
    215 | Op2 (t1, t2, t', x_10461, x_10460, x_10459) ->
    216   h_Op2 t1 t2 t' x_10461 x_10460 x_10459
    217     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10460)
    218     (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10459)
    219 | Mem (t, x_10462) ->
    220   h_Mem t x_10462
     213let 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
    221225    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    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
     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
    225229    (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    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)
     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)
    232236
    233237(** val expr_rect_Type0 :
     
    239243    -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
    240244    -> 'a1) -> AST.typ -> expr -> 'a1 **)
    241 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_10475 = function
    242 | Id (t, x_10477) -> h_Id t x_10477
    243 | Cst (t, x_10478) -> h_Cst t x_10478
    244 | Op1 (t, t', x_10480, x_10479) ->
    245   h_Op1 t t' x_10480 x_10479
    246     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_10479)
    247 | Op2 (t1, t2, t', x_10483, x_10482, x_10481) ->
    248   h_Op2 t1 t2 t' x_10483 x_10482 x_10481
    249     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_10482)
    250     (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_10481)
    251 | Mem (t, x_10484) ->
    252   h_Mem t x_10484
     245let 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
    253257    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
    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
     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
    257261    (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
    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)
     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)
    264268
    265269(** val expr_inv_rect_Type4 :
     
    373377let 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
    374378| St_skip -> h_St_skip
    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
     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
    380384    (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_10667)
     385      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13983)
    382386    (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_10666)
    384 | St_ifthenelse (sz, sg, x_10670, x_10669, x_10668) ->
    385   h_St_ifthenelse sz sg x_10670 x_10669 x_10668
     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
    386390    (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_10669)
     391      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13985)
    388392    (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_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
     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
    393397    (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_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
     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
    398402    (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_10675)
     403      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_13991)
    400404
    401405(** val stmt_rect_Type3 :
     
    410414let 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
    411415| St_skip -> h_St_skip
    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
     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
    417421    (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_10725)
     422      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14041)
    419423    (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_10724)
    421 | St_ifthenelse (sz, sg, x_10728, x_10727, x_10726) ->
    422   h_St_ifthenelse sz sg x_10728 x_10727 x_10726
     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
    423427    (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_10727)
     428      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14043)
    425429    (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_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
     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
    430434    (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_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
     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
    435439    (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_10733)
     440      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049)
    437441
    438442(** val stmt_rect_Type2 :
     
    447451let 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
    448452| St_skip -> h_St_skip
    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
     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
    454458    (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_10754)
     459      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14070)
    456460    (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_10753)
    458 | St_ifthenelse (sz, sg, x_10757, x_10756, x_10755) ->
    459   h_St_ifthenelse sz sg x_10757 x_10756 x_10755
     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
    460464    (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_10756)
     465      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14072)
    462466    (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_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
     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
    467471    (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_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
     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
    472476    (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_10762)
     477      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14078)
    474478
    475479(** val stmt_rect_Type1 :
     
    484488let 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
    485489| St_skip -> h_St_skip
    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
     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
    491495    (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_10783)
     496      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14099)
    493497    (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_10782)
    495 | St_ifthenelse (sz, sg, x_10786, x_10785, x_10784) ->
    496   h_St_ifthenelse sz sg x_10786 x_10785 x_10784
     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
    497501    (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_10785)
     502      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101)
    499503    (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_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
     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
    504508    (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_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
     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
    509513    (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_10791)
     514      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14107)
    511515
    512516(** val stmt_rect_Type0 :
     
    521525let 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
    522526| St_skip -> h_St_skip
    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
     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
    528532    (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_10812)
     533      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14128)
    530534    (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_10811)
    532 | St_ifthenelse (sz, sg, x_10815, x_10814, x_10813) ->
    533   h_St_ifthenelse sz sg x_10815 x_10814 x_10813
     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
    534538    (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_10814)
     539      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130)
    536540    (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_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
     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
    541545    (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_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
     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
    546550    (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_10820)
     551      h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14136)
    548552
    549553(** val stmt_inv_rect_Type4 :
     
    759763    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    760764    -> 'a1) -> internal_function -> 'a1 **)
    761 let rec internal_function_rect_Type4 h_mk_internal_function x_11116 =
     765let rec internal_function_rect_Type4 h_mk_internal_function x_14432 =
    762766  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    763     f_stacksize = f_stacksize0; f_body = f_body0 } = x_11116
     767    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14432
    764768  in
    765769  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    770774    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    771775    -> 'a1) -> internal_function -> 'a1 **)
    772 let rec internal_function_rect_Type5 h_mk_internal_function x_11118 =
     776let rec internal_function_rect_Type5 h_mk_internal_function x_14434 =
    773777  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    774     f_stacksize = f_stacksize0; f_body = f_body0 } = x_11118
     778    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14434
    775779  in
    776780  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    781785    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    782786    -> 'a1) -> internal_function -> 'a1 **)
    783 let rec internal_function_rect_Type3 h_mk_internal_function x_11120 =
     787let rec internal_function_rect_Type3 h_mk_internal_function x_14436 =
    784788  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    785     f_stacksize = f_stacksize0; f_body = f_body0 } = x_11120
     789    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14436
    786790  in
    787791  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    792796    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    793797    -> 'a1) -> internal_function -> 'a1 **)
    794 let rec internal_function_rect_Type2 h_mk_internal_function x_11122 =
     798let rec internal_function_rect_Type2 h_mk_internal_function x_14438 =
    795799  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    796     f_stacksize = f_stacksize0; f_body = f_body0 } = x_11122
     800    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14438
    797801  in
    798802  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    803807    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    804808    -> 'a1) -> internal_function -> 'a1 **)
    805 let rec internal_function_rect_Type1 h_mk_internal_function x_11124 =
     809let rec internal_function_rect_Type1 h_mk_internal_function x_14440 =
    806810  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    807     f_stacksize = f_stacksize0; f_body = f_body0 } = x_11124
     811    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14440
    808812  in
    809813  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
     
    814818    (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
    815819    -> 'a1) -> internal_function -> 'a1 **)
    816 let rec internal_function_rect_Type0 h_mk_internal_function x_11126 =
     820let rec internal_function_rect_Type0 h_mk_internal_function x_14442 =
    817821  let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
    818     f_stacksize = f_stacksize0; f_body = f_body0 } = x_11126
     822    f_stacksize = f_stacksize0; f_body = f_body0 } = x_14442
    819823  in
    820824  h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
Note: See TracChangeset for help on using the changeset viewer.