Changeset 2960 for extracted/joint_semantics.ml
 Timestamp:
 Mar 26, 2013, 4:51:40 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/joint_semantics.ml
r2951 r2960 133 133 type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t; 134 134 stack_sizes : (AST.ident > Nat.nat Types.option); 135 get_pc_from_label : (AST.ident > Graphs.label > 136 ByteValues.program_counter 137 Errors.res) } 135 premain : 'f; 136 pc_from_label : (Pointers.block Types.sig0 > 'f > 137 Graphs.label > 138 ByteValues.program_counter Types.option) } 138 139 139 140 (** val genv_gen_rect_Type4 : 140 141 AST.ident List.list > ('a1 AST.fundef Globalenvs.genv_t > __ > 141 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 142 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_5376 = 144 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 145 get_pc_from_label0 } = x_5376 146 in 147 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 142 (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block Types.sig0 143 > 'a1 > Graphs.label > ByteValues.program_counter Types.option) > 144 'a2) > 'a1 genv_gen > 'a2 **) 145 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_55 = 146 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; 147 pc_from_label = pc_from_label0 } = x_55 148 in 149 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 148 150 149 151 (** val genv_gen_rect_Type5 : 150 152 AST.ident List.list > ('a1 AST.fundef Globalenvs.genv_t > __ > 151 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 152 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5378 = 154 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 155 get_pc_from_label0 } = x_5378 156 in 157 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 153 (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block Types.sig0 154 > 'a1 > Graphs.label > ByteValues.program_counter Types.option) > 155 'a2) > 'a1 genv_gen > 'a2 **) 156 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_57 = 157 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; 158 pc_from_label = pc_from_label0 } = x_57 159 in 160 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 158 161 159 162 (** val genv_gen_rect_Type3 : 160 163 AST.ident List.list > ('a1 AST.fundef Globalenvs.genv_t > __ > 161 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 162 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_5380 = 164 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 165 get_pc_from_label0 } = x_5380 166 in 167 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 164 (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block Types.sig0 165 > 'a1 > Graphs.label > ByteValues.program_counter Types.option) > 166 'a2) > 'a1 genv_gen > 'a2 **) 167 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_59 = 168 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; 169 pc_from_label = pc_from_label0 } = x_59 170 in 171 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 168 172 169 173 (** val genv_gen_rect_Type2 : 170 174 AST.ident List.list > ('a1 AST.fundef Globalenvs.genv_t > __ > 171 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 172 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_5382 = 174 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 175 get_pc_from_label0 } = x_5382 176 in 177 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 175 (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block Types.sig0 176 > 'a1 > Graphs.label > ByteValues.program_counter Types.option) > 177 'a2) > 'a1 genv_gen > 'a2 **) 178 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_61 = 179 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; 180 pc_from_label = pc_from_label0 } = x_61 181 in 182 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 178 183 179 184 (** val genv_gen_rect_Type1 : 180 185 AST.ident List.list > ('a1 AST.fundef Globalenvs.genv_t > __ > 181 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 182 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_5384 = 184 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 185 get_pc_from_label0 } = x_5384 186 in 187 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 186 (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block Types.sig0 187 > 'a1 > Graphs.label > ByteValues.program_counter Types.option) > 188 'a2) > 'a1 genv_gen > 'a2 **) 189 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_63 = 190 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; 191 pc_from_label = pc_from_label0 } = x_63 192 in 193 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 188 194 189 195 (** val genv_gen_rect_Type0 : 190 196 AST.ident List.list > ('a1 AST.fundef Globalenvs.genv_t > __ > 191 (AST.ident > Nat.nat Types.option) > (AST.ident > Graphs.label > 192 ByteValues.program_counter Errors.res) > 'a2) > 'a1 genv_gen > 'a2 **) 193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_5386 = 194 let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label = 195 get_pc_from_label0 } = x_5386 196 in 197 h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0 197 (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block Types.sig0 198 > 'a1 > Graphs.label > ByteValues.program_counter Types.option) > 199 'a2) > 'a1 genv_gen > 'a2 **) 200 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_65 = 201 let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; 202 pc_from_label = pc_from_label0 } = x_65 203 in 204 h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 198 205 199 206 (** val ge : … … 207 214 xxx.stack_sizes 208 215 209 (** val get_pc_from_label : 210 AST.ident List.list > 'a1 genv_gen > AST.ident > Graphs.label > 211 ByteValues.program_counter Errors.res **) 212 let rec get_pc_from_label globals xxx = 213 xxx.get_pc_from_label 216 (** val premain : AST.ident List.list > 'a1 genv_gen > 'a1 **) 217 let rec premain globals xxx = 218 xxx.premain 219 220 (** val pc_from_label : 221 AST.ident List.list > 'a1 genv_gen > Pointers.block Types.sig0 > 'a1 222 > Graphs.label > ByteValues.program_counter Types.option **) 223 let rec pc_from_label globals xxx = 224 xxx.pc_from_label 214 225 215 226 (** val genv_gen_inv_rect_Type4 : 216 227 AST.ident List.list > 'a1 genv_gen > ('a1 AST.fundef Globalenvs.genv_t 217 > __ > (AST.ident > Nat.nat Types.option) > (AST.ident >218 Graphs.label > ByteValues.program_counter Errors.res) > __ > 'a2) >219 'a2 **)228 > __ > (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block 229 Types.sig0 > 'a1 > Graphs.label > ByteValues.program_counter 230 Types.option) > __ > 'a2) > 'a2 **) 220 231 let genv_gen_inv_rect_Type4 x2 hterm h1 = 221 232 let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __ … … 223 234 (** val genv_gen_inv_rect_Type3 : 224 235 AST.ident List.list > 'a1 genv_gen > ('a1 AST.fundef Globalenvs.genv_t 225 > __ > (AST.ident > Nat.nat Types.option) > (AST.ident >226 Graphs.label > ByteValues.program_counter Errors.res) > __ > 'a2) >227 'a2 **)236 > __ > (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block 237 Types.sig0 > 'a1 > Graphs.label > ByteValues.program_counter 238 Types.option) > __ > 'a2) > 'a2 **) 228 239 let genv_gen_inv_rect_Type3 x2 hterm h1 = 229 240 let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __ … … 231 242 (** val genv_gen_inv_rect_Type2 : 232 243 AST.ident List.list > 'a1 genv_gen > ('a1 AST.fundef Globalenvs.genv_t 233 > __ > (AST.ident > Nat.nat Types.option) > (AST.ident >234 Graphs.label > ByteValues.program_counter Errors.res) > __ > 'a2) >235 'a2 **)244 > __ > (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block 245 Types.sig0 > 'a1 > Graphs.label > ByteValues.program_counter 246 Types.option) > __ > 'a2) > 'a2 **) 236 247 let genv_gen_inv_rect_Type2 x2 hterm h1 = 237 248 let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __ … … 239 250 (** val genv_gen_inv_rect_Type1 : 240 251 AST.ident List.list > 'a1 genv_gen > ('a1 AST.fundef Globalenvs.genv_t 241 > __ > (AST.ident > Nat.nat Types.option) > (AST.ident >242 Graphs.label > ByteValues.program_counter Errors.res) > __ > 'a2) >243 'a2 **)252 > __ > (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block 253 Types.sig0 > 'a1 > Graphs.label > ByteValues.program_counter 254 Types.option) > __ > 'a2) > 'a2 **) 244 255 let genv_gen_inv_rect_Type1 x2 hterm h1 = 245 256 let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __ … … 247 258 (** val genv_gen_inv_rect_Type0 : 248 259 AST.ident List.list > 'a1 genv_gen > ('a1 AST.fundef Globalenvs.genv_t 249 > __ > (AST.ident > Nat.nat Types.option) > (AST.ident >250 Graphs.label > ByteValues.program_counter Errors.res) > __ > 'a2) >251 'a2 **)260 > __ > (AST.ident > Nat.nat Types.option) > 'a1 > (Pointers.block 261 Types.sig0 > 'a1 > Graphs.label > ByteValues.program_counter 262 Types.option) > __ > 'a2) > 'a2 **) 252 263 let genv_gen_inv_rect_Type0 x2 hterm h1 = 253 264 let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __ … … 257 268 let genv_gen_discr a2 x y = 258 269 Logic.eq_rect_Type2 x 259 (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in 260 Obj.magic (fun _ dH > dH __ __ __ __)) y 270 (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x 271 in 272 Obj.magic (fun _ dH > dH __ __ __ __ __)) y 261 273 262 274 (** val genv_gen_jmdiscr : … … 264 276 let genv_gen_jmdiscr a2 x y = 265 277 Logic.eq_rect_Type2 x 266 (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in 267 Obj.magic (fun _ dH > dH __ __ __ __)) y 278 (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x 279 in 280 Obj.magic (fun _ dH > dH __ __ __ __ __)) y 268 281 269 282 (** val dpi1__o__ge__o__inject : … … 296 309 let eject__o__ge x1 x3 = 297 310 (Types.pi1 x3).ge 311 312 (** val pre_main_id : AST.ident **) 313 let pre_main_id = 314 Positive.One 315 316 (** val fetch_function : 317 AST.ident List.list > 'a1 genv_gen > Pointers.block Types.sig0 > 318 (AST.ident, 'a1 AST.fundef) Types.prod Errors.res **) 319 let fetch_function g ge0 bl = 320 match Z.eqZb (Pointers.block_id (Types.pi1 bl)) 321 (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) with 322  Bool.True > 323 Obj.magic 324 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = pre_main_id; 325 Types.snd = (AST.Internal ge0.premain) }) 326  Bool.False > 327 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), 328 List.Nil)) 329 (Obj.magic 330 (Monad.m_bind0 (Monad.max_def Option.option) 331 (Obj.magic (Globalenvs.symbol_for_block ge0.ge (Types.pi1 bl))) 332 (fun id > 333 Monad.m_bind0 (Monad.max_def Option.option) 334 (Obj.magic (Globalenvs.find_funct_ptr ge0.ge (Types.pi1 bl))) 335 (fun fd > 336 Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id; 337 Types.snd = fd })))) 338 339 (** val fetch_internal_function : 340 AST.ident List.list > 'a1 genv_gen > Pointers.block Types.sig0 > 341 (AST.ident, 'a1) Types.prod Errors.res **) 342 let fetch_internal_function g ge0 bl = 343 Obj.magic 344 (Monad.m_bind2 (Monad.max_def Errors.res0) 345 (Obj.magic (fetch_function g ge0 bl)) (fun id fd > 346 match fd with 347  AST.Internal ifd > 348 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id; 349 Types.snd = ifd } 350  AST.External x > 351 Obj.magic (Errors.Error (List.Cons ((Errors.MSG 352 ErrorMessages.BadFunction), List.Nil))))) 353 354 (** val code_block_of_block : 355 Pointers.block > Pointers.block Types.sig0 Types.option **) 356 let code_block_of_block bl = 357 (match Pointers.block_region bl with 358  AST.XData > (fun _ > Types.None) 359  AST.Code > (fun _ > Types.Some bl)) __ 360 361 (** val block_of_funct_id : 362 'a1 Globalenvs.genv_t > PreIdentifiers.identifier > Pointers.block 363 Types.sig0 Errors.res **) 364 let block_of_funct_id ge0 id = 365 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), 366 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil)))) 367 (Obj.magic 368 (Monad.m_bind0 (Monad.max_def Option.option) 369 (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl > 370 Obj.magic (code_block_of_block bl)))) 371 372 (** val gen_pc_from_label : 373 AST.ident List.list > 'a1 genv_gen > AST.ident > Graphs.label > 374 ByteValues.program_counter Errors.res **) 375 let gen_pc_from_label g ge0 id lbl = 376 Obj.magic 377 (Monad.m_bind0 (Monad.max_def Errors.res0) 378 (Obj.magic (block_of_funct_id ge0.ge id)) (fun bl > 379 Monad.m_bind2 (Monad.max_def Errors.res0) 380 (Obj.magic (fetch_internal_function g ge0 bl)) (fun ignore f_def > 381 Obj.magic 382 (Errors.opt_to_res (List.Cons ((Errors.MSG 383 ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX 384 (PreIdentifiers.LabelTag, lbl)), List.Nil)))) 385 (ge0.pc_from_label bl f_def lbl))))) 298 386 299 387 type genv = Joint.joint_closed_internal_function genv_gen … … 341 429 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 342 430 'a1) > sem_state_params > 'a1 **) 343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_ 5406 =431 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_86 = 344 432 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 345 load_sp0; save_sp = save_sp0 } = x_ 5406433 load_sp0; save_sp = save_sp0 } = x_86 346 434 in 347 435 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 351 439 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 352 440 'a1) > sem_state_params > 'a1 **) 353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_ 5408 =441 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_88 = 354 442 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 355 load_sp0; save_sp = save_sp0 } = x_ 5408443 load_sp0; save_sp = save_sp0 } = x_88 356 444 in 357 445 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 361 449 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 362 450 'a1) > sem_state_params > 'a1 **) 363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_ 5410 =451 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_90 = 364 452 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 365 load_sp0; save_sp = save_sp0 } = x_ 5410453 load_sp0; save_sp = save_sp0 } = x_90 366 454 in 367 455 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 371 459 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 372 460 'a1) > sem_state_params > 'a1 **) 373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_ 5412 =461 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_92 = 374 462 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 375 load_sp0; save_sp = save_sp0 } = x_ 5412463 load_sp0; save_sp = save_sp0 } = x_92 376 464 in 377 465 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 381 469 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 382 470 'a1) > sem_state_params > 'a1 **) 383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_ 5414 =471 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_94 = 384 472 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 385 load_sp0; save_sp = save_sp0 } = x_ 5414473 load_sp0; save_sp = save_sp0 } = x_94 386 474 in 387 475 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 391 479 ByteValues.xpointer Errors.res) > (__ > ByteValues.xpointer > __) > 392 480 'a1) > sem_state_params > 'a1 **) 393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_ 5416 =481 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_96 = 394 482 let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = 395 load_sp0; save_sp = save_sp0 } = x_ 5416483 load_sp0; save_sp = save_sp0 } = x_96 396 484 in 397 485 h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 … … 472 560 let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function 473 561  Empty_is > h_empty_is 474  One_is x_ 5442 > h_one_is x_5442475  Both_is (x_ 5444, x_5443) > h_both_is x_5444 x_5443562  One_is x_122 > h_one_is x_122 563  Both_is (x_124, x_123) > h_both_is x_124 x_123 476 564 477 565 (** val internal_stack_rect_Type5 : … … 480 568 let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function 481 569  Empty_is > h_empty_is 482  One_is x_ 5449 > h_one_is x_5449483  Both_is (x_ 5451, x_5450) > h_both_is x_5451 x_5450570  One_is x_129 > h_one_is x_129 571  Both_is (x_131, x_130) > h_both_is x_131 x_130 484 572 485 573 (** val internal_stack_rect_Type3 : … … 488 576 let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function 489 577  Empty_is > h_empty_is 490  One_is x_ 5456 > h_one_is x_5456491  Both_is (x_ 5458, x_5457) > h_both_is x_5458 x_5457578  One_is x_136 > h_one_is x_136 579  Both_is (x_138, x_137) > h_both_is x_138 x_137 492 580 493 581 (** val internal_stack_rect_Type2 : … … 496 584 let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function 497 585  Empty_is > h_empty_is 498  One_is x_ 5463 > h_one_is x_5463499  Both_is (x_ 5465, x_5464) > h_both_is x_5465 x_5464586  One_is x_143 > h_one_is x_143 587  Both_is (x_145, x_144) > h_both_is x_145 x_144 500 588 501 589 (** val internal_stack_rect_Type1 : … … 504 592 let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function 505 593  Empty_is > h_empty_is 506  One_is x_ 5470 > h_one_is x_5470507  Both_is (x_ 5472, x_5471) > h_both_is x_5472 x_5471594  One_is x_150 > h_one_is x_150 595  Both_is (x_152, x_151) > h_both_is x_152 x_151 508 596 509 597 (** val internal_stack_rect_Type0 : … … 512 600 let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function 513 601  Empty_is > h_empty_is 514  One_is x_ 5477 > h_one_is x_5477515  Both_is (x_ 5479, x_5478) > h_both_is x_5479 x_5478602  One_is x_157 > h_one_is x_157 603  Both_is (x_159, x_158) > h_both_is x_159 x_158 516 604 517 605 (** val internal_stack_inv_rect_Type4 : … … 597 685 sem_state_params > (__ Types.option > internal_stack > 598 686 ByteValues.bebit > __ > BEMem.bemem > Nat.nat > 'a1) > state > 'a1 **) 599 let rec state_rect_Type4 semp h_mk_state x_ 5527 =687 let rec state_rect_Type4 semp h_mk_state x_207 = 600 688 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 601 m = m0; stack_usage = stack_usage0 } = x_ 5527689 m = m0; stack_usage = stack_usage0 } = x_207 602 690 in 603 691 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 … … 606 694 sem_state_params > (__ Types.option > internal_stack > 607 695 ByteValues.bebit > __ > BEMem.bemem > Nat.nat > 'a1) > state > 'a1 **) 608 let rec state_rect_Type5 semp h_mk_state x_ 5529 =696 let rec state_rect_Type5 semp h_mk_state x_209 = 609 697 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 610 m = m0; stack_usage = stack_usage0 } = x_ 5529698 m = m0; stack_usage = stack_usage0 } = x_209 611 699 in 612 700 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 … … 615 703 sem_state_params > (__ Types.option > internal_stack > 616 704 ByteValues.bebit > __ > BEMem.bemem > Nat.nat > 'a1) > state > 'a1 **) 617 let rec state_rect_Type3 semp h_mk_state x_ 5531 =705 let rec state_rect_Type3 semp h_mk_state x_211 = 618 706 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 619 m = m0; stack_usage = stack_usage0 } = x_ 5531707 m = m0; stack_usage = stack_usage0 } = x_211 620 708 in 621 709 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 … … 624 712 sem_state_params > (__ Types.option > internal_stack > 625 713 ByteValues.bebit > __ > BEMem.bemem > Nat.nat > 'a1) > state > 'a1 **) 626 let rec state_rect_Type2 semp h_mk_state x_ 5533 =714 let rec state_rect_Type2 semp h_mk_state x_213 = 627 715 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 628 m = m0; stack_usage = stack_usage0 } = x_ 5533716 m = m0; stack_usage = stack_usage0 } = x_213 629 717 in 630 718 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 … … 633 721 sem_state_params > (__ Types.option > internal_stack > 634 722 ByteValues.bebit > __ > BEMem.bemem > Nat.nat > 'a1) > state > 'a1 **) 635 let rec state_rect_Type1 semp h_mk_state x_ 5535 =723 let rec state_rect_Type1 semp h_mk_state x_215 = 636 724 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 637 m = m0; stack_usage = stack_usage0 } = x_ 5535725 m = m0; stack_usage = stack_usage0 } = x_215 638 726 in 639 727 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 … … 642 730 sem_state_params > (__ Types.option > internal_stack > 643 731 ByteValues.bebit > __ > BEMem.bemem > Nat.nat > 'a1) > state > 'a1 **) 644 let rec state_rect_Type0 semp h_mk_state x_ 5537 =732 let rec state_rect_Type0 semp h_mk_state x_217 = 645 733 let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; 646 m = m0; stack_usage = stack_usage0 } = x_ 5537734 m = m0; stack_usage = stack_usage0 } = x_217 647 735 in 648 736 h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 … … 720 808 sem_state_params > (state > ByteValues.program_counter > 721 809 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 722 let rec state_pc_rect_Type4 semp h_mk_state_pc x_ 5553 =723 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 5553 in810 let rec state_pc_rect_Type4 semp h_mk_state_pc x_233 = 811 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_233 in 724 812 h_mk_state_pc st_no_pc0 pc0 last_pop0 725 813 … … 727 815 sem_state_params > (state > ByteValues.program_counter > 728 816 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 729 let rec state_pc_rect_Type5 semp h_mk_state_pc x_ 5555 =730 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 5555 in817 let rec state_pc_rect_Type5 semp h_mk_state_pc x_235 = 818 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_235 in 731 819 h_mk_state_pc st_no_pc0 pc0 last_pop0 732 820 … … 734 822 sem_state_params > (state > ByteValues.program_counter > 735 823 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 736 let rec state_pc_rect_Type3 semp h_mk_state_pc x_ 5557 =737 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 5557 in824 let rec state_pc_rect_Type3 semp h_mk_state_pc x_237 = 825 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_237 in 738 826 h_mk_state_pc st_no_pc0 pc0 last_pop0 739 827 … … 741 829 sem_state_params > (state > ByteValues.program_counter > 742 830 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 743 let rec state_pc_rect_Type2 semp h_mk_state_pc x_ 5559 =744 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 5559 in831 let rec state_pc_rect_Type2 semp h_mk_state_pc x_239 = 832 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_239 in 745 833 h_mk_state_pc st_no_pc0 pc0 last_pop0 746 834 … … 748 836 sem_state_params > (state > ByteValues.program_counter > 749 837 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 750 let rec state_pc_rect_Type1 semp h_mk_state_pc x_ 5561 =751 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 5561 in838 let rec state_pc_rect_Type1 semp h_mk_state_pc x_241 = 839 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_241 in 752 840 h_mk_state_pc st_no_pc0 pc0 last_pop0 753 841 … … 755 843 sem_state_params > (state > ByteValues.program_counter > 756 844 ByteValues.program_counter > 'a1) > state_pc > 'a1 **) 757 let rec state_pc_rect_Type0 semp h_mk_state_pc x_ 5563 =758 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_ 5563 in845 let rec state_pc_rect_Type0 semp h_mk_state_pc x_243 = 846 let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_243 in 759 847 h_mk_state_pc st_no_pc0 pc0 last_pop0 760 848 … … 895 983 { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs = 896 984 st.regs; m = st.m; stack_usage = st.stack_usage } 897 898 (** val fetch_function :899 'a1 Globalenvs.genv_t > Pointers.block Types.sig0 > (AST.ident, 'a1)900 Types.prod Errors.res **)901 let fetch_function ge0 bl =902 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),903 List.Nil))904 (Obj.magic905 (Monad.m_bind0 (Monad.max_def Option.option)906 (Obj.magic (Globalenvs.symbol_for_block ge0 (Types.pi1 bl)))907 (fun id >908 Monad.m_bind0 (Monad.max_def Option.option)909 (Obj.magic (Globalenvs.find_funct_ptr ge0 (Types.pi1 bl)))910 (fun fd >911 Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;912 Types.snd = fd }))))913 914 (** val fetch_internal_function :915 'a1 AST.fundef Globalenvs.genv_t > Pointers.block Types.sig0 >916 (AST.ident, 'a1) Types.prod Errors.res **)917 let fetch_internal_function ge0 bl =918 Obj.magic919 (Monad.m_bind2 (Monad.max_def Errors.res0)920 (Obj.magic (fetch_function ge0 bl)) (fun id fd >921 match fd with922  AST.Internal ifd >923 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;924 Types.snd = ifd }925  AST.External x >926 Obj.magic (Errors.Error (List.Cons ((Errors.MSG927 ErrorMessages.BadFunction), List.Nil)))))928 985 929 986 type call_kind = … … 1094 1151 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1095 1152 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_ 5618 =1153 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_298 = 1097 1154 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1098 1155 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1106 1163 set_result0; call_args_for_main = call_args_for_main0; 1107 1164 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1108 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_ 56181165 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_298 1109 1166 in 1110 1167 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1135 1192 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1136 1193 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_ 5620 =1194 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_300 = 1138 1195 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1139 1196 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1147 1204 set_result0; call_args_for_main = call_args_for_main0; 1148 1205 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1149 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_ 56201206 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_300 1150 1207 in 1151 1208 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1176 1233 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1177 1234 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_ 5622 =1235 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_302 = 1179 1236 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1180 1237 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1188 1245 set_result0; call_args_for_main = call_args_for_main0; 1189 1246 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1190 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_ 56221247 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_302 1191 1248 in 1192 1249 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1217 1274 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1218 1275 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_ 5624 =1276 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_304 = 1220 1277 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1221 1278 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1229 1286 set_result0; call_args_for_main = call_args_for_main0; 1230 1287 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1231 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_ 56241288 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_304 1232 1289 in 1233 1290 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1258 1315 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1259 1316 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_ 5626 =1317 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_306 = 1261 1318 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1262 1319 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1270 1327 set_result0; call_args_for_main = call_args_for_main0; 1271 1328 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1272 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_ 56261329 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_306 1273 1330 in 1274 1331 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1299 1356 state > (state, ByteValues.program_counter) Types.prod Errors.res) > 1300 1357 'a2) > 'a1 sem_unserialized_params > 'a2 **) 1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_ 5628 =1358 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_308 = 1302 1359 let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = 1303 1360 acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = … … 1311 1368 set_result0; call_args_for_main = call_args_for_main0; 1312 1369 call_dest_for_main = call_dest_for_main0; read_result = read_result0; 1313 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_ 56281370 eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_308 1314 1371 in 1315 1372 h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 … … 1761 1818 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1762 1819 > __ > __ > 'a1) > serialized_params > 'a1 **) 1763 let rec serialized_params_rect_Type4 h_mk_serialized_params x_ 5698 =1820 let rec serialized_params_rect_Type4 h_mk_serialized_params x_378 = 1764 1821 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1765 point_of_offset = point_of_offset0 } = x_ 56981822 point_of_offset = point_of_offset0 } = x_378 1766 1823 in 1767 1824 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ … … 1772 1829 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1773 1830 > __ > __ > 'a1) > serialized_params > 'a1 **) 1774 let rec serialized_params_rect_Type5 h_mk_serialized_params x_ 5700 =1831 let rec serialized_params_rect_Type5 h_mk_serialized_params x_380 = 1775 1832 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1776 point_of_offset = point_of_offset0 } = x_ 57001833 point_of_offset = point_of_offset0 } = x_380 1777 1834 in 1778 1835 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ … … 1783 1840 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1784 1841 > __ > __ > 'a1) > serialized_params > 'a1 **) 1785 let rec serialized_params_rect_Type3 h_mk_serialized_params x_ 5702 =1842 let rec serialized_params_rect_Type3 h_mk_serialized_params x_382 = 1786 1843 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1787 point_of_offset = point_of_offset0 } = x_ 57021844 point_of_offset = point_of_offset0 } = x_382 1788 1845 in 1789 1846 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ … … 1794 1851 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1795 1852 > __ > __ > 'a1) > serialized_params > 'a1 **) 1796 let rec serialized_params_rect_Type2 h_mk_serialized_params x_ 5704 =1853 let rec serialized_params_rect_Type2 h_mk_serialized_params x_384 = 1797 1854 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1798 point_of_offset = point_of_offset0 } = x_ 57041855 point_of_offset = point_of_offset0 } = x_384 1799 1856 in 1800 1857 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ … … 1805 1862 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1806 1863 > __ > __ > 'a1) > serialized_params > 'a1 **) 1807 let rec serialized_params_rect_Type1 h_mk_serialized_params x_ 5706 =1864 let rec serialized_params_rect_Type1 h_mk_serialized_params x_386 = 1808 1865 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1809 point_of_offset = point_of_offset0 } = x_ 57061866 point_of_offset = point_of_offset0 } = x_386 1810 1867 in 1811 1868 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ … … 1816 1873 sem_unserialized_params > (__ > Positive.pos) > (Positive.pos > __) 1817 1874 > __ > __ > 'a1) > serialized_params > 'a1 **) 1818 let rec serialized_params_rect_Type0 h_mk_serialized_params x_ 5708 =1875 let rec serialized_params_rect_Type0 h_mk_serialized_params x_388 = 1819 1876 let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; 1820 point_of_offset = point_of_offset0 } = x_ 57081877 point_of_offset = point_of_offset0 } = x_388 1821 1878 in 1822 1879 h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ … … 1910 1967 (serialized_params > (Joint.joint_program > 1911 1968 Joint.joint_closed_internal_function) > 'a1) > sem_params > 'a1 **) 1912 let rec sem_params_rect_Type4 h_mk_sem_params x_ 5726 =1913 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_ 5726 in1969 let rec sem_params_rect_Type4 h_mk_sem_params x_406 = 1970 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_406 in 1914 1971 h_mk_sem_params spp'0 pre_main_generator0 1915 1972 … … 1917 1974 (serialized_params > (Joint.joint_program > 1918 1975 Joint.joint_closed_internal_function) > 'a1) > sem_params > 'a1 **) 1919 let rec sem_params_rect_Type5 h_mk_sem_params x_ 5728 =1920 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_ 5728 in1976 let rec sem_params_rect_Type5 h_mk_sem_params x_408 = 1977 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_408 in 1921 1978 h_mk_sem_params spp'0 pre_main_generator0 1922 1979 … … 1924 1981 (serialized_params > (Joint.joint_program > 1925 1982 Joint.joint_closed_internal_function) > 'a1) > sem_params > 'a1 **) 1926 let rec sem_params_rect_Type3 h_mk_sem_params x_ 5730 =1927 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_ 5730 in1983 let rec sem_params_rect_Type3 h_mk_sem_params x_410 = 1984 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_410 in 1928 1985 h_mk_sem_params spp'0 pre_main_generator0 1929 1986 … … 1931 1988 (serialized_params > (Joint.joint_program > 1932 1989 Joint.joint_closed_internal_function) > 'a1) > sem_params > 'a1 **) 1933 let rec sem_params_rect_Type2 h_mk_sem_params x_ 5732 =1934 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_ 5732 in1990 let rec sem_params_rect_Type2 h_mk_sem_params x_412 = 1991 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_412 in 1935 1992 h_mk_sem_params spp'0 pre_main_generator0 1936 1993 … … 1938 1995 (serialized_params > (Joint.joint_program > 1939 1996 Joint.joint_closed_internal_function) > 'a1) > sem_params > 'a1 **) 1940 let rec sem_params_rect_Type1 h_mk_sem_params x_ 5734 =1941 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_ 5734 in1997 let rec sem_params_rect_Type1 h_mk_sem_params x_414 = 1998 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_414 in 1942 1999 h_mk_sem_params spp'0 pre_main_generator0 1943 2000 … … 1945 2002 (serialized_params > (Joint.joint_program > 1946 2003 Joint.joint_closed_internal_function) > 'a1) > sem_params > 'a1 **) 1947 let rec sem_params_rect_Type0 h_mk_sem_params x_ 5736 =1948 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_ 5736 in2004 let rec sem_params_rect_Type0 h_mk_sem_params x_416 = 2005 let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_416 in 1949 2006 h_mk_sem_params spp'0 pre_main_generator0 1950 2007 … … 2034 2091 2035 2092 (** val fetch_statement : 2036 sem_params > AST.ident List.list > Joint.joint_function 2037 Globalenvs.genv_t > ByteValues.program_counter > ((AST.ident, 2038 Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement) 2039 Types.prod Errors.res **) 2093 sem_params > AST.ident List.list > genv > ByteValues.program_counter 2094 > ((AST.ident, Joint.joint_closed_internal_function) Types.prod, 2095 Joint.joint_statement) Types.prod Errors.res **) 2040 2096 let fetch_statement p globals ge0 ptr = 2041 2097 Obj.magic 2042 2098 (Monad.m_bind2 (Monad.max_def Errors.res0) 2043 (Obj.magic (fetch_internal_function ge0 ptr.ByteValues.pc_block)) 2099 (Obj.magic 2100 (fetch_internal_function globals ge0 ptr.ByteValues.pc_block)) 2044 2101 (fun id fn > 2045 2102 let pt = point_of_pc p ptr in … … 2054 2111 2055 2112 (** val pc_of_label : 2056 sem_params > AST.ident List.list > Joint.joint_function 2057 Globalenvs.genv_t > Pointers.block Types.sig0 > Graphs.label > 2058 ByteValues.program_counter Errors.res **) 2113 sem_params > AST.ident List.list > genv > Pointers.block Types.sig0 > 2114 Graphs.label > ByteValues.program_counter Errors.res **) 2059 2115 let pc_of_label p globals ge0 bl lbl = 2060 2116 Obj.magic 2061 2117 (Monad.m_bind2 (Monad.max_def Errors.res0) 2062 (Obj.magic (fetch_internal_function g e0 bl)) (fun i fn >2118 (Obj.magic (fetch_internal_function globals ge0 bl)) (fun i fn > 2063 2119 Monad.m_bind0 (Monad.max_def Errors.res0) 2064 2120 (Obj.magic … … 2080 2136 2081 2137 (** val goto : 2082 sem_params > AST.ident List.list > Joint.joint_function2083 Globalenvs.genv_t > Graphs.label > state_pc >state_pc Errors.res **)2138 sem_params > AST.ident List.list > genv > Graphs.label > state_pc > 2139 state_pc Errors.res **) 2084 2140 let goto p globals ge0 l st = 2085 2141 Obj.magic … … 2096 2152 2097 2153 (** val next_of_call_pc : 2098 sem_params > AST.ident List.list > Joint.joint_function2099 Globalenvs.genv_t > ByteValues.program_counter> __ Errors.res **)2154 sem_params > AST.ident List.list > genv > ByteValues.program_counter 2155 > __ Errors.res **) 2100 2156 let next_of_call_pc p globals ge0 pc0 = 2101 2157 Obj.magic … … 2289 2345 p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st 2290 2346 2291 (** val code_block_of_block :2292 Pointers.block > Pointers.block Types.sig0 Types.option **)2293 let code_block_of_block bl =2294 (match Pointers.block_region bl with2295  AST.XData > (fun _ > Types.None)2296  AST.Code > (fun _ > Types.Some bl)) __2297 2298 (** val block_of_funct_id :2299 sem_state_params > 'a1 Globalenvs.genv_t > PreIdentifiers.identifier >2300 Pointers.block Types.sig0 Errors.res **)2301 let block_of_funct_id sp0 ge0 id =2302 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),2303 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))2304 (Obj.magic2305 (Monad.m_bind0 (Monad.max_def Option.option)2306 (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl >2307 Obj.magic (code_block_of_block bl))))2308 2309 2347 (** val block_of_call : 2310 2348 sem_params > AST.ident List.list > Joint.joint_function … … 2423 2461 Obj.magic x) (fun bl > 2424 2462 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad) 2425 (let x = 2426 IOMonad.err_to_io 2427 (fetch_function 2428 (let p0 = spp'__o__spp p in 2429 let globals0 = globals in let g = ge0 in g.ge) bl) 2430 in 2463 (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in 2431 2464 Obj.magic x) (fun i fd > 2432 2465 match fd with … … 2488 2521 (fun st' call_pc > 2489 2522 Monad.m_bind0 (Monad.max_def Errors.res0) 2490 (Obj.magic 2491 (next_of_call_pc p globals 2492 (let p0 = spp'__o__spp p in 2493 let globals0 = globals in let g = ge0 in g.ge) call_pc)) 2494 (fun nxt > 2523 (Obj.magic (next_of_call_pc p globals ge0 call_pc)) (fun nxt > 2495 2524 let st'' = 2496 2525 set_last_pop p.spp'.msu_pars.st_pars … … 2515 2544 Obj.magic x) (fun bl > 2516 2545 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad) 2517 (let x = 2518 IOMonad.err_to_io 2519 (fetch_function 2520 (let p0 = spp'__o__spp p in 2521 let globals0 = globals in let g = ge0 in g.ge) bl) 2522 in 2546 (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in 2523 2547 Obj.magic x) (fun i fd > 2524 2548 match fd with … … 2577 2601 (Obj.magic (ByteValues.bool_of_beval v)) (fun b > 2578 2602 match b with 2579  Bool.True > 2580 Obj.magic 2581 (goto p g 2582 (let p0 = spp'__o__spp p in 2583 let globals = g in let g0 = ge0 in g0.ge) l st) 2603  Bool.True > Obj.magic (goto p g ge0 l st) 2584 2604  Bool.False > 2585 2605 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st))))) … … 2590 2610 let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in 2591 2611 (match s0 with 2592  Joint.GOTO l > 2593 IOMonad.err_to_io 2594 (goto p g 2595 (let p0 = spp'__o__spp p in 2596 let globals = g in let g0 = ge0 in g0.ge) l st) 2612  Joint.GOTO l > IOMonad.err_to_io (goto p g ge0 l st) 2597 2613  Joint.RETURN > 2598 2614 IOMonad.err_to_io … … 2611 2627 (Obj.magic (ByteValues.bool_of_beval v)) (fun b > 2612 2628 match b with 2613  Bool.True > 2614 Obj.magic 2615 (goto p g 2616 (let p0 = spp'__o__spp p in 2617 let globals = g in let g0 = ge0 in g0.ge) lbltrue st) 2618  Bool.False > 2619 Obj.magic 2620 (goto p g 2621 (let p0 = spp'__o__spp p in 2622 let globals = g in let g0 = ge0 in g0.ge) lblfalse st))))) 2629  Bool.True > Obj.magic (goto p g ge0 lbltrue st) 2630  Bool.False > Obj.magic (goto p g ge0 lblfalse st))))) 2623 2631 2624 2632 (** val eval_state : … … 2628 2636 Obj.magic 2629 2637 (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad) 2630 (let x = 2631 IOMonad.err_to_io 2632 (fetch_statement p globals 2633 (let p0 = spp'__o__spp p in 2634 let globals0 = globals in let g = ge0 in g.ge) st.pc) 2635 in 2638 (let x = IOMonad.err_to_io (fetch_statement p globals ge0 st.pc) in 2636 2639 Obj.magic x) (fun id fn s > 2637 2640 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
Note: See TracChangeset
for help on using the changeset viewer.