Changeset 3059 for extracted/cminor_semantics.ml
 Timestamp:
 Apr 2, 2013, 1:25:09 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/cminor_semantics.ml
r3043 r3059 123 123 let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function 124 124  Kend > h_Kend 125  Kseq (x_2 18, x_217) >126 h_Kseq x_2 18 x_217 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_217)127  Kblock x_2 19>128 h_Kblock x_2 19 (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) 129 129 130 130 (** val cont_rect_Type3 : … … 133 133 let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function 134 134  Kend > h_Kend 135  Kseq (x_23 2, x_231) >136 h_Kseq x_23 2 x_231 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_231)137  Kblock x_23 3>138 h_Kblock x_23 3 (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) 139 139 140 140 (** val cont_rect_Type2 : … … 143 143 let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function 144 144  Kend > h_Kend 145  Kseq (x_23 9, x_238) >146 h_Kseq x_23 9 x_238 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_238)147  Kblock x_2 40>148 h_Kblock x_2 40 (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) 149 149 150 150 (** val cont_rect_Type1 : … … 153 153 let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function 154 154  Kend > h_Kend 155  Kseq (x_2 46, x_245) >156 h_Kseq x_2 46 x_245 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_245)157  Kblock x_2 47>158 h_Kblock x_2 47 (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) 159 159 160 160 (** val cont_rect_Type0 : … … 163 163 let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function 164 164  Kend > h_Kend 165  Kseq (x_2 53, x_252) >166 h_Kseq x_2 53 x_252 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_252)167  Kblock x_2 54>168 h_Kblock x_2 54 (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) 169 169 170 170 (** val cont_inv_rect_Type4 : … … 226 226 let rec stack_rect_Type4 h_SStop h_Scall = function 227 227  SStop > h_SStop 228  Scall (dest, f, x_ 313, en, k, x_309) >229 h_Scall dest f x_ 313 en __ __ k __ x_309230 (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) 231 231 232 232 (** val stack_rect_Type3 : … … 236 236 let rec stack_rect_Type3 h_SStop h_Scall = function 237 237  SStop > h_SStop 238  Scall (dest, f, x_ 329, en, k, x_325) >239 h_Scall dest f x_ 329 en __ __ k __ x_325240 (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) 241 241 242 242 (** val stack_rect_Type2 : … … 246 246 let rec stack_rect_Type2 h_SStop h_Scall = function 247 247  SStop > h_SStop 248  Scall (dest, f, x_ 337, en, k, x_333) >249 h_Scall dest f x_ 337 en __ __ k __ x_333250 (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) 251 251 252 252 (** val stack_rect_Type1 : … … 256 256 let rec stack_rect_Type1 h_SStop h_Scall = function 257 257  SStop > h_SStop 258  Scall (dest, f, x_ 345, en, k, x_341) >259 h_Scall dest f x_ 345 en __ __ k __ x_341260 (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) 261 261 262 262 (** val stack_rect_Type0 : … … 266 266 let rec stack_rect_Type0 h_SStop h_Scall = function 267 267  SStop > h_SStop 268  Scall (dest, f, x_ 353, en, k, x_349) >269 h_Scall dest f x_ 353 en __ __ k __ x_349270 (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) 271 271 272 272 (** val stack_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.