Ignore:
Timestamp:
Mar 15, 2013, 11:11:45 PM (7 years ago)
Author:
sacerdot
Message:

Exported again, now the execution is correct up to LIN for a simple program.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_semantics.ml

    r2873 r2890  
    123123let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
    124124| Kend -> h_Kend
    125 | Kseq (x_25457, x_25456) ->
    126   h_Kseq x_25457 x_25456 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25456)
    127 | Kblock x_25458 ->
    128   h_Kblock x_25458 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25458)
     125| Kseq (x_25483, x_25482) ->
     126  h_Kseq x_25483 x_25482 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25482)
     127| Kblock x_25484 ->
     128  h_Kblock x_25484 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25484)
    129129
    130130(** val cont_rect_Type3 :
     
    133133let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
    134134| Kend -> h_Kend
    135 | Kseq (x_25471, x_25470) ->
    136   h_Kseq x_25471 x_25470 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25470)
    137 | Kblock x_25472 ->
    138   h_Kblock x_25472 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25472)
     135| Kseq (x_25497, x_25496) ->
     136  h_Kseq x_25497 x_25496 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25496)
     137| Kblock x_25498 ->
     138  h_Kblock x_25498 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25498)
    139139
    140140(** val cont_rect_Type2 :
     
    143143let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
    144144| Kend -> h_Kend
    145 | Kseq (x_25478, x_25477) ->
    146   h_Kseq x_25478 x_25477 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25477)
    147 | Kblock x_25479 ->
    148   h_Kblock x_25479 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25479)
     145| Kseq (x_25504, x_25503) ->
     146  h_Kseq x_25504 x_25503 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25503)
     147| Kblock x_25505 ->
     148  h_Kblock x_25505 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25505)
    149149
    150150(** val cont_rect_Type1 :
     
    153153let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
    154154| Kend -> h_Kend
    155 | Kseq (x_25485, x_25484) ->
    156   h_Kseq x_25485 x_25484 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25484)
    157 | Kblock x_25486 ->
    158   h_Kblock x_25486 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25486)
     155| Kseq (x_25511, x_25510) ->
     156  h_Kseq x_25511 x_25510 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25510)
     157| Kblock x_25512 ->
     158  h_Kblock x_25512 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25512)
    159159
    160160(** val cont_rect_Type0 :
     
    163163let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
    164164| Kend -> h_Kend
    165 | Kseq (x_25492, x_25491) ->
    166   h_Kseq x_25492 x_25491 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25491)
    167 | Kblock x_25493 ->
    168   h_Kblock x_25493 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25493)
     165| Kseq (x_25518, x_25517) ->
     166  h_Kseq x_25518 x_25517 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25517)
     167| Kblock x_25519 ->
     168  h_Kblock x_25519 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25519)
    169169
    170170(** val cont_inv_rect_Type4 :
     
    226226let rec stack_rect_Type4 h_SStop h_Scall = function
    227227| SStop -> h_SStop
    228 | Scall (dest, f, x_25552, en, k, x_25548) ->
    229   h_Scall dest f x_25552 en __ __ k __ x_25548
    230     (stack_rect_Type4 h_SStop h_Scall x_25548)
     228| Scall (dest, f, x_25578, en, k, x_25574) ->
     229  h_Scall dest f x_25578 en __ __ k __ x_25574
     230    (stack_rect_Type4 h_SStop h_Scall x_25574)
    231231
    232232(** val stack_rect_Type3 :
     
    236236let rec stack_rect_Type3 h_SStop h_Scall = function
    237237| SStop -> h_SStop
    238 | Scall (dest, f, x_25568, en, k, x_25564) ->
    239   h_Scall dest f x_25568 en __ __ k __ x_25564
    240     (stack_rect_Type3 h_SStop h_Scall x_25564)
     238| Scall (dest, f, x_25594, en, k, x_25590) ->
     239  h_Scall dest f x_25594 en __ __ k __ x_25590
     240    (stack_rect_Type3 h_SStop h_Scall x_25590)
    241241
    242242(** val stack_rect_Type2 :
     
    246246let rec stack_rect_Type2 h_SStop h_Scall = function
    247247| SStop -> h_SStop
    248 | Scall (dest, f, x_25576, en, k, x_25572) ->
    249   h_Scall dest f x_25576 en __ __ k __ x_25572
    250     (stack_rect_Type2 h_SStop h_Scall x_25572)
     248| Scall (dest, f, x_25602, en, k, x_25598) ->
     249  h_Scall dest f x_25602 en __ __ k __ x_25598
     250    (stack_rect_Type2 h_SStop h_Scall x_25598)
    251251
    252252(** val stack_rect_Type1 :
     
    256256let rec stack_rect_Type1 h_SStop h_Scall = function
    257257| SStop -> h_SStop
    258 | Scall (dest, f, x_25584, en, k, x_25580) ->
    259   h_Scall dest f x_25584 en __ __ k __ x_25580
    260     (stack_rect_Type1 h_SStop h_Scall x_25580)
     258| Scall (dest, f, x_25610, en, k, x_25606) ->
     259  h_Scall dest f x_25610 en __ __ k __ x_25606
     260    (stack_rect_Type1 h_SStop h_Scall x_25606)
    261261
    262262(** val stack_rect_Type0 :
     
    266266let rec stack_rect_Type0 h_SStop h_Scall = function
    267267| SStop -> h_SStop
    268 | Scall (dest, f, x_25592, en, k, x_25588) ->
    269   h_Scall dest f x_25592 en __ __ k __ x_25588
    270     (stack_rect_Type0 h_SStop h_Scall x_25588)
     268| Scall (dest, f, x_25618, en, k, x_25614) ->
     269  h_Scall dest f x_25618 en __ __ k __ x_25614
     270    (stack_rect_Type0 h_SStop h_Scall x_25614)
    271271
    272272(** val stack_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.