 Timestamp:
 Mar 11, 2013, 12:41:33 PM (8 years ago)
 Location:
 extracted
 Files:

 2 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

extracted/compiler.ml
r2829 r2842 434 434  Ltl_pass > Obj.magic (fun _ dH > dH) 435 435  Lin_pass > Obj.magic (fun _ dH > dH)) y 436 437 type 'x with_stack_model = ('x, AST.ident > Nat.nat Types.option) Types.prod 436 438 437 439 type syntax_of_pass = __ … … 469 471 Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))))) 470 472 473 open Uses 474 471 475 (** val compute_fixpoint : Fixpoints.fixpoint_computer **) 472 476 let compute_fixpoint = Compute_fixpoints.compute_fixpoint … … 474 478 (** val colour_graph : Interference.coloured_graph_computer **) 475 479 let colour_graph = Compute_colouring.colour_graph 480 481 open AssocList 482 483 (** val lookup_stack_cost : 484 Joint.params > Joint.joint_program > PreIdentifiers.identifier > 485 Nat.nat Types.option **) 486 let lookup_stack_cost p p0 id = 487 AssocList.assoc_list_lookup id 488 (Identifiers.eq_identifier PreIdentifiers.SymbolTag) 489 (Joint.stack_cost p p0) 476 490 477 491 (** val back_end : … … 481 495 let back_end observe p = 482 496 let p0 = RTLabsToRTL.rtlabs_to_rtl p in 483 let i = Obj.magic observe Rtl_separate_pass p0 in 484 let i0 = Obj.magic observe Rtl_uniq_pass p0 in 497 let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in 498 let i = 499 Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st } 500 in 501 let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st } 502 in 485 503 let p1 = RTLToERTL.rtl_to_ertl p0 in 486 let i1 = Obj.magic observe Ertl_pass p1 in 504 let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in 505 let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in 487 506 let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in 488 let i2 = Obj.magic observe Ertlptr_pass p2 in 489 let { Types.fst = eta2; Types.snd = max_stack } = 507 let st1 = 508 lookup_stack_cost (Joint.graph_params_to_params ERTLptr.eRTLptr) p2 509 in 510 let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 } 511 in 512 let { Types.fst = eta20; Types.snd = max_stack } = 490 513 ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2 491 514 in 492 let { Types.fst = p3; Types.snd = stack_cost } = eta2 in 493 let i3 = Obj.magic observe Ltl_pass p3 in 515 let { Types.fst = p3; Types.snd = stack_cost0 } = eta20 in 516 let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in 517 let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in 518 let st3 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in 494 519 let p4 = LTLToLIN.ltl_to_lin p3 in 495 let i4 = Obj.magic observe Lin_pass p4 in 520 let st4 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p4 in 521 let i4 = Obj.magic observe Lin_pass { Types.fst = p4; Types.snd = st4 } in 496 522 Obj.magic 497 523 (Monad.m_bind0 (Monad.max_def Errors.res0) … … 500 526 (LINToASM.lin_to_asm p4))) (fun p5 > 501 527 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst = 502 p5; Types.snd = stack_cost }; Types.snd = max_stack }))528 p5; Types.snd = stack_cost0 }; Types.snd = max_stack })) 503 529 504 530 open Assembly … … 708 734 (Obj.magic (front_end observe p)) (fun init_cost p' p0 > 709 735 Monad.m_bind3 (Monad.max_def Errors.res0) 710 (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack >736 (Obj.magic (back_end observe p0)) (fun p1 stack_cost0 max_stack > 711 737 Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1)) 712 738 (fun p2 > … … 717 743 in 718 744 Monad.m_return0 (Monad.max_def Errors.res0) 719 { c_labelled_object_code = p2; c_stack_cost = stack_cost ;745 { c_labelled_object_code = p2; c_stack_cost = stack_cost0; 720 746 c_max_stack = max_stack; c_labelled_clight = p'; 721 747 c_clight_cost_map = k' })))) 
extracted/compiler.mli
r2829 r2842 312 312 val pass_jmdiscr : pass > pass > __ 313 313 314 type 'x with_stack_model = ('x, AST.ident > Nat.nat Types.option) Types.prod 315 314 316 type syntax_of_pass = __ 315 317 … … 321 323 Types.prod Errors.res 322 324 325 open Uses 326 323 327 val compute_fixpoint : Fixpoints.fixpoint_computer 324 328 325 329 val colour_graph : Interference.coloured_graph_computer 330 331 open AssocList 332 333 val lookup_stack_cost : 334 Joint.params > Joint.joint_program > PreIdentifiers.identifier > Nat.nat 335 Types.option 326 336 327 337 val back_end :
Note: See TracChangeset
for help on using the changeset viewer.