Ignore:
Timestamp:
Mar 13, 2013, 11:12:29 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after indianess bug fixes by Paolo.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_semantics.ml

    r2827 r2867  
    123123let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
    124124| Kend -> h_Kend
    125 | Kseq (x_70, x_69) ->
    126   h_Kseq x_70 x_69 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_69)
    127 | Kblock x_71 -> h_Kblock x_71 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_71)
     125| Kseq (x_25288, x_25287) ->
     126  h_Kseq x_25288 x_25287 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25287)
     127| Kblock x_25289 ->
     128  h_Kblock x_25289 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25289)
    128129
    129130(** val cont_rect_Type3 :
     
    132133let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
    133134| Kend -> h_Kend
    134 | Kseq (x_84, x_83) ->
    135   h_Kseq x_84 x_83 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_83)
    136 | Kblock x_85 -> h_Kblock x_85 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_85)
     135| Kseq (x_25302, x_25301) ->
     136  h_Kseq x_25302 x_25301 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25301)
     137| Kblock x_25303 ->
     138  h_Kblock x_25303 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25303)
    137139
    138140(** val cont_rect_Type2 :
     
    141143let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
    142144| Kend -> h_Kend
    143 | Kseq (x_91, x_90) ->
    144   h_Kseq x_91 x_90 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_90)
    145 | Kblock x_92 -> h_Kblock x_92 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_92)
     145| Kseq (x_25309, x_25308) ->
     146  h_Kseq x_25309 x_25308 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25308)
     147| Kblock x_25310 ->
     148  h_Kblock x_25310 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25310)
    146149
    147150(** val cont_rect_Type1 :
     
    150153let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
    151154| Kend -> h_Kend
    152 | Kseq (x_98, x_97) ->
    153   h_Kseq x_98 x_97 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_97)
    154 | Kblock x_99 -> h_Kblock x_99 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_99)
     155| Kseq (x_25316, x_25315) ->
     156  h_Kseq x_25316 x_25315 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25315)
     157| Kblock x_25317 ->
     158  h_Kblock x_25317 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25317)
    155159
    156160(** val cont_rect_Type0 :
     
    159163let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
    160164| Kend -> h_Kend
    161 | Kseq (x_105, x_104) ->
    162   h_Kseq x_105 x_104 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_104)
    163 | Kblock x_106 ->
    164   h_Kblock x_106 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_106)
     165| Kseq (x_25323, x_25322) ->
     166  h_Kseq x_25323 x_25322 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25322)
     167| Kblock x_25324 ->
     168  h_Kblock x_25324 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25324)
    165169
    166170(** val cont_inv_rect_Type4 :
     
    222226let rec stack_rect_Type4 h_SStop h_Scall = function
    223227| SStop -> h_SStop
    224 | Scall (dest, f, x_165, en, k, x_161) ->
    225   h_Scall dest f x_165 en __ __ k __ x_161
    226     (stack_rect_Type4 h_SStop h_Scall x_161)
     228| Scall (dest, f, x_25383, en, k, x_25379) ->
     229  h_Scall dest f x_25383 en __ __ k __ x_25379
     230    (stack_rect_Type4 h_SStop h_Scall x_25379)
    227231
    228232(** val stack_rect_Type3 :
     
    232236let rec stack_rect_Type3 h_SStop h_Scall = function
    233237| SStop -> h_SStop
    234 | Scall (dest, f, x_181, en, k, x_177) ->
    235   h_Scall dest f x_181 en __ __ k __ x_177
    236     (stack_rect_Type3 h_SStop h_Scall x_177)
     238| Scall (dest, f, x_25399, en, k, x_25395) ->
     239  h_Scall dest f x_25399 en __ __ k __ x_25395
     240    (stack_rect_Type3 h_SStop h_Scall x_25395)
    237241
    238242(** val stack_rect_Type2 :
     
    242246let rec stack_rect_Type2 h_SStop h_Scall = function
    243247| SStop -> h_SStop
    244 | Scall (dest, f, x_189, en, k, x_185) ->
    245   h_Scall dest f x_189 en __ __ k __ x_185
    246     (stack_rect_Type2 h_SStop h_Scall x_185)
     248| Scall (dest, f, x_25407, en, k, x_25403) ->
     249  h_Scall dest f x_25407 en __ __ k __ x_25403
     250    (stack_rect_Type2 h_SStop h_Scall x_25403)
    247251
    248252(** val stack_rect_Type1 :
     
    252256let rec stack_rect_Type1 h_SStop h_Scall = function
    253257| SStop -> h_SStop
    254 | Scall (dest, f, x_197, en, k, x_193) ->
    255   h_Scall dest f x_197 en __ __ k __ x_193
    256     (stack_rect_Type1 h_SStop h_Scall x_193)
     258| Scall (dest, f, x_25415, en, k, x_25411) ->
     259  h_Scall dest f x_25415 en __ __ k __ x_25411
     260    (stack_rect_Type1 h_SStop h_Scall x_25411)
    257261
    258262(** val stack_rect_Type0 :
     
    262266let rec stack_rect_Type0 h_SStop h_Scall = function
    263267| SStop -> h_SStop
    264 | Scall (dest, f, x_205, en, k, x_201) ->
    265   h_Scall dest f x_205 en __ __ k __ x_201
    266     (stack_rect_Type0 h_SStop h_Scall x_201)
     268| Scall (dest, f, x_25423, en, k, x_25419) ->
     269  h_Scall dest f x_25423 en __ __ k __ x_25419
     270    (stack_rect_Type0 h_SStop h_Scall x_25419)
    267271
    268272(** val stack_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.