Changeset 2867 for extracted/cminor_semantics.ml
 Timestamp:
 Mar 13, 2013, 11:12:29 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_semantics.ml
r2827 r2867 123 123 let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function 124 124  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) 128 129 129 130 (** val cont_rect_Type3 : … … 132 133 let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function 133 134  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) 137 139 138 140 (** val cont_rect_Type2 : … … 141 143 let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function 142 144  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) 146 149 147 150 (** val cont_rect_Type1 : … … 150 153 let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function 151 154  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) 155 159 156 160 (** val cont_rect_Type0 : … … 159 163 let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function 160 164  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) 165 169 166 170 (** val cont_inv_rect_Type4 : … … 222 226 let rec stack_rect_Type4 h_SStop h_Scall = function 223 227  SStop > h_SStop 224  Scall (dest, f, x_ 165, en, k, x_161) >225 h_Scall dest f x_ 165 en __ __ k __ x_161226 (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) 227 231 228 232 (** val stack_rect_Type3 : … … 232 236 let rec stack_rect_Type3 h_SStop h_Scall = function 233 237  SStop > h_SStop 234  Scall (dest, f, x_ 181, en, k, x_177) >235 h_Scall dest f x_ 181 en __ __ k __ x_177236 (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) 237 241 238 242 (** val stack_rect_Type2 : … … 242 246 let rec stack_rect_Type2 h_SStop h_Scall = function 243 247  SStop > h_SStop 244  Scall (dest, f, x_ 189, en, k, x_185) >245 h_Scall dest f x_ 189 en __ __ k __ x_185246 (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) 247 251 248 252 (** val stack_rect_Type1 : … … 252 256 let rec stack_rect_Type1 h_SStop h_Scall = function 253 257  SStop > h_SStop 254  Scall (dest, f, x_ 197, en, k, x_193) >255 h_Scall dest f x_ 197 en __ __ k __ x_193256 (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) 257 261 258 262 (** val stack_rect_Type0 : … … 262 266 let rec stack_rect_Type0 h_SStop h_Scall = function 263 267  SStop > h_SStop 264  Scall (dest, f, x_2 05, en, k, x_201) >265 h_Scall dest f x_2 05 en __ __ k __ x_201266 (stack_rect_Type0 h_SStop h_Scall x_2 01)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) 267 271 268 272 (** val stack_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.