Ignore:
Timestamp:
Apr 2, 2013, 1:25:09 AM (7 years ago)
Author:
sacerdot
Message:

New extraction

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_semantics.ml

    r3043 r3059  
    123123let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
    124124| Kend -> h_Kend
    125 | Kseq (x_218, x_217) ->
    126   h_Kseq x_218 x_217 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_217)
    127 | Kblock x_219 ->
    128   h_Kblock x_219 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_219)
     125| Kseq (x_23729, x_23728) ->
     126  h_Kseq x_23729 x_23728 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23728)
     127| Kblock x_23730 ->
     128  h_Kblock x_23730 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23730)
    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_232, x_231) ->
    136   h_Kseq x_232 x_231 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_231)
    137 | Kblock x_233 ->
    138   h_Kblock x_233 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_233)
     135| Kseq (x_23743, x_23742) ->
     136  h_Kseq x_23743 x_23742 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23742)
     137| Kblock x_23744 ->
     138  h_Kblock x_23744 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23744)
    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_239, x_238) ->
    146   h_Kseq x_239 x_238 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_238)
    147 | Kblock x_240 ->
    148   h_Kblock x_240 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_240)
     145| Kseq (x_23750, x_23749) ->
     146  h_Kseq x_23750 x_23749 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23749)
     147| Kblock x_23751 ->
     148  h_Kblock x_23751 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23751)
    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_246, x_245) ->
    156   h_Kseq x_246 x_245 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_245)
    157 | Kblock x_247 ->
    158   h_Kblock x_247 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_247)
     155| Kseq (x_23757, x_23756) ->
     156  h_Kseq x_23757 x_23756 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23756)
     157| Kblock x_23758 ->
     158  h_Kblock x_23758 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23758)
    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_253, x_252) ->
    166   h_Kseq x_253 x_252 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_252)
    167 | Kblock x_254 ->
    168   h_Kblock x_254 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_254)
     165| Kseq (x_23764, x_23763) ->
     166  h_Kseq x_23764 x_23763 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23763)
     167| Kblock x_23765 ->
     168  h_Kblock x_23765 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23765)
    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_313, en, k, x_309) ->
    229   h_Scall dest f x_313 en __ __ k __ x_309
    230     (stack_rect_Type4 h_SStop h_Scall x_309)
     228| Scall (dest, f, x_23824, en, k, x_23820) ->
     229  h_Scall dest f x_23824 en __ __ k __ x_23820
     230    (stack_rect_Type4 h_SStop h_Scall x_23820)
    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_329, en, k, x_325) ->
    239   h_Scall dest f x_329 en __ __ k __ x_325
    240     (stack_rect_Type3 h_SStop h_Scall x_325)
     238| Scall (dest, f, x_23840, en, k, x_23836) ->
     239  h_Scall dest f x_23840 en __ __ k __ x_23836
     240    (stack_rect_Type3 h_SStop h_Scall x_23836)
    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_337, en, k, x_333) ->
    249   h_Scall dest f x_337 en __ __ k __ x_333
    250     (stack_rect_Type2 h_SStop h_Scall x_333)
     248| Scall (dest, f, x_23848, en, k, x_23844) ->
     249  h_Scall dest f x_23848 en __ __ k __ x_23844
     250    (stack_rect_Type2 h_SStop h_Scall x_23844)
    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_345, en, k, x_341) ->
    259   h_Scall dest f x_345 en __ __ k __ x_341
    260     (stack_rect_Type1 h_SStop h_Scall x_341)
     258| Scall (dest, f, x_23856, en, k, x_23852) ->
     259  h_Scall dest f x_23856 en __ __ k __ x_23852
     260    (stack_rect_Type1 h_SStop h_Scall x_23852)
    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_353, en, k, x_349) ->
    269   h_Scall dest f x_353 en __ __ k __ x_349
    270     (stack_rect_Type0 h_SStop h_Scall x_349)
     268| Scall (dest, f, x_23864, en, k, x_23860) ->
     269  h_Scall dest f x_23864 en __ __ k __ x_23860
     270    (stack_rect_Type0 h_SStop h_Scall x_23860)
    271271
    272272(** val stack_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.