Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptrToLTL.ml

    r2773 r2775  
    167167    arg_decision -> 'a1 **)
    168168let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    169 | Arg_decision_colour x_16991 -> h_arg_decision_colour x_16991
    170 | Arg_decision_spill x_16992 -> h_arg_decision_spill x_16992
    171 | Arg_decision_imm x_16993 -> h_arg_decision_imm x_16993
     169| Arg_decision_colour x_21731 -> h_arg_decision_colour x_21731
     170| Arg_decision_spill x_21732 -> h_arg_decision_spill x_21732
     171| Arg_decision_imm x_21733 -> h_arg_decision_imm x_21733
    172172
    173173(** val arg_decision_rect_Type5 :
     
    175175    arg_decision -> 'a1 **)
    176176let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    177 | Arg_decision_colour x_16998 -> h_arg_decision_colour x_16998
    178 | Arg_decision_spill x_16999 -> h_arg_decision_spill x_16999
    179 | Arg_decision_imm x_17000 -> h_arg_decision_imm x_17000
     177| Arg_decision_colour x_21738 -> h_arg_decision_colour x_21738
     178| Arg_decision_spill x_21739 -> h_arg_decision_spill x_21739
     179| Arg_decision_imm x_21740 -> h_arg_decision_imm x_21740
    180180
    181181(** val arg_decision_rect_Type3 :
     
    183183    arg_decision -> 'a1 **)
    184184let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    185 | Arg_decision_colour x_17005 -> h_arg_decision_colour x_17005
    186 | Arg_decision_spill x_17006 -> h_arg_decision_spill x_17006
    187 | Arg_decision_imm x_17007 -> h_arg_decision_imm x_17007
     185| Arg_decision_colour x_21745 -> h_arg_decision_colour x_21745
     186| Arg_decision_spill x_21746 -> h_arg_decision_spill x_21746
     187| Arg_decision_imm x_21747 -> h_arg_decision_imm x_21747
    188188
    189189(** val arg_decision_rect_Type2 :
     
    191191    arg_decision -> 'a1 **)
    192192let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    193 | Arg_decision_colour x_17012 -> h_arg_decision_colour x_17012
    194 | Arg_decision_spill x_17013 -> h_arg_decision_spill x_17013
    195 | Arg_decision_imm x_17014 -> h_arg_decision_imm x_17014
     193| Arg_decision_colour x_21752 -> h_arg_decision_colour x_21752
     194| Arg_decision_spill x_21753 -> h_arg_decision_spill x_21753
     195| Arg_decision_imm x_21754 -> h_arg_decision_imm x_21754
    196196
    197197(** val arg_decision_rect_Type1 :
     
    199199    arg_decision -> 'a1 **)
    200200let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    201 | Arg_decision_colour x_17019 -> h_arg_decision_colour x_17019
    202 | Arg_decision_spill x_17020 -> h_arg_decision_spill x_17020
    203 | Arg_decision_imm x_17021 -> h_arg_decision_imm x_17021
     201| Arg_decision_colour x_21759 -> h_arg_decision_colour x_21759
     202| Arg_decision_spill x_21760 -> h_arg_decision_spill x_21760
     203| Arg_decision_imm x_21761 -> h_arg_decision_imm x_21761
    204204
    205205(** val arg_decision_rect_Type0 :
     
    207207    arg_decision -> 'a1 **)
    208208let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    209 | Arg_decision_colour x_17026 -> h_arg_decision_colour x_17026
    210 | Arg_decision_spill x_17027 -> h_arg_decision_spill x_17027
    211 | Arg_decision_imm x_17028 -> h_arg_decision_imm x_17028
     209| Arg_decision_colour x_21766 -> h_arg_decision_colour x_21766
     210| Arg_decision_spill x_21767 -> h_arg_decision_spill x_21767
     211| Arg_decision_imm x_21768 -> h_arg_decision_imm x_21768
    212212
    213213(** val arg_decision_inv_rect_Type4 :
     
    943943  TranslateUtils.f_fin = (translate_fin_step globals) }
    944944
     945(** val first_free_stack_addr : LTL.ltl_program -> Nat.nat **)
     946let first_free_stack_addr p =
     947  let globals_addr_internal = fun offset x_size ->
     948    let { Types.fst = eta4401; Types.snd = size } = x_size in
     949    let { Types.fst = x; Types.snd = region } = eta4401 in
     950    Nat.plus offset size
     951  in
     952  Util.foldl globals_addr_internal Nat.O p.AST.prog_vars
     953
    945954(** val ertlptr_to_ltl :
    946955    Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
    947     ERTLptr.ertlptr_program -> LTL.ltl_program **)
    948 let ertlptr_to_ltl the_fixpoint build =
    949   TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL
    950     (translate_data the_fixpoint build)
    951 
     956    ERTLptr.ertlptr_program -> ((LTL.ltl_program, Joint.stack_cost_model)
     957    Types.prod, Nat.nat) Types.prod **)
     958let ertlptr_to_ltl the_fixpoint build pr =
     959  let ltlprog =
     960    TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL
     961      (translate_data the_fixpoint build) pr
     962  in
     963  { Types.fst = { Types.fst = ltlprog; Types.snd =
     964  (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
     965  Types.snd =
     966  (Nat.minus
     967    (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     968      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     969      Nat.O))))))))))))))))) (first_free_stack_addr ltlprog)) }
     970
Note: See TracChangeset for help on using the changeset viewer.