Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (8 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL_paolo.ma

    r2208 r2214  
    88
    99definition save_hdws :
    10   ∀globals.list (register×Register) → list (joint_seq ertl_params globals) ≝
     10  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
    1111 λglobals.
    1212  let save_hdws_internal ≝
     
    1515
    1616definition restore_hdws :
    17   ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝
     17  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
    1818  λglobals.
    1919   let restore_hdws_internal ≝
     
    2222
    2323definition get_params_hdw :
    24   ∀globals.list register → list (joint_seq ertl_params globals) ≝
     24  ∀globals.list register → list (joint_seq ERTL globals) ≝
    2525  λglobals,params.
    2626  save_hdws … (zip_pottier … params RegisterParams).
     
    2828definition get_param_stack :
    2929  ∀globals.register → register → register →
    30   list (joint_seq ertl_params globals) ≝
     30  list (joint_seq ERTL globals) ≝
    3131  λglobals,addr1,addr2,destr.
    3232  (* liveness analysis will erase the last useless ops *)
     
    3838definition get_params_stack :
    3939  ∀globals.list register →
    40   bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
     40  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    4141  λglobals,params.
    4242  νtmpr,addr1,addr2 in
     
    5959definition prologue :
    6060  ∀globals.list register → register → register → list (register×Register) →
    61   bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
     61  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    6262  λglobals,params,sral,srah,sregs.
    6363  [ (ertl_new_frame : joint_seq ??) ;
     
    6767
    6868definition save_return :
    69   ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
     69  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    7070  λglobals,ret_regs.
    7171  match reduce_strong ? ? RegisterSTS ret_regs with
     
    7979  ].
    8080
    81 definition assign_result : ∀globals.list (joint_seq ertl_params globals) ≝
     81definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
    8282  λglobals.
    8383  match reduce_strong ?? RegisterRets RegisterSTS with
     
    9090definition epilogue :
    9191  ∀globals.list register → register → register → list (register × Register) →
    92   list (joint_seq ertl_params globals) ≝
     92  list (joint_seq ERTL globals) ≝
    9393  λglobals,ret_regs,sral,srah,sregs.
    9494  save_return … (map … (Reg ?) ret_regs) @
    9595  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
    96   [ PUSH ertl_params ? srah ;
     96  [ PUSH ERTL ? srah ;
    9797    PUSH … sral ;
    9898    ertl_del_frame ] @
     
    101101definition allocate_regs :
    102102  ∀globals,rs.rs_set rs →
    103   state_monad (joint_internal_function globals ertl_params) (list (register×Register)) ≝
     103  state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
    104104  λglobals,rs,saved,def.
    105105   let allocate_regs_internal ≝
     
    112112definition add_pro_and_epilogue :
    113113  ∀globals.list register → list register →
    114   joint_internal_function globals ertl_params →
    115   joint_internal_function globals ertl_params ≝
     114  joint_internal_function ERTL globals →
     115  joint_internal_function ERTL globals ≝
    116116  λglobals,params,ret_regs,def.
    117117  let start_lbl ≝ joint_if_entry … def in
     
    129129
    130130definition set_params_hdw :
    131   ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
     131  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    132132  λglobals,params.
    133133  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     
    137137definition set_param_stack :
    138138  ∀globals.register → register → psd_argument →
    139   list (joint_seq ertl_params globals) ≝
     139  list (joint_seq ERTL globals) ≝
    140140  λglobals,addr1,addr2,arg.
    141141  [ STORE … addr1 addr2 arg ;
     
    145145
    146146definition set_params_stack :
    147   ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝
     147  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
    148148  λglobals,params.
    149149  νaddr1,addr2 in
     
    166166
    167167definition fetch_result :
    168   ∀globals.list register → list (joint_seq ertl_params globals) ≝
     168  ∀globals.list register → list (joint_seq ERTL globals) ≝
    169169  λglobals,ret_regs.
    170170  match reduce_strong ?? RegisterSTS RegisterRets with
     
    182182
    183183definition translate_step :
    184   ∀globals.label → joint_step rtlntc_params globals →
    185     bind_seq_block ertl_params globals (joint_step ertl_params globals) ≝
     184  ∀globals.label → joint_step RTL_ntc globals →
     185    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
    186186  λglobals.λ_.λs.
    187187  match s return λ_.bind_seq_block ?? (joint_step ??) with
     
    194194      COST_LABEL … lbl
    195195    | ADDRESS x prf r1 r2 ⇒
    196       ADDRESS ertl_params ? x prf r1 r2
     196      ADDRESS ERTL ? x prf r1 r2
    197197    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    198       OPACCS ertl_params ? op destr1 destr2 srcr1 srcr2 
     198      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
    199199    | OP1 op1 destr srcr ⇒
    200       OP1 ertl_params ? op1 destr srcr
     200      OP1 ERTL ? op1 destr srcr
    201201    | OP2 op2 destr srcr1 srcr2 ⇒
    202       OP2 ertl_params ? op2 destr srcr1 srcr2
     202      OP2 ERTL ? op2 destr srcr1 srcr2
    203203    | CLEAR_CARRY ⇒
    204204      CLEAR_CARRY …
     
    206206      SET_CARRY …
    207207    | LOAD destr addr1 addr2 ⇒
    208       LOAD ertl_params ? destr addr1 addr2
     208      LOAD ERTL ? destr addr1 addr2
    209209    | STORE addr1 addr2 srcr ⇒
    210       STORE ertl_params ? addr1 addr2 srcr
     210      STORE ERTL ? addr1 addr2 srcr
    211211    | COMMENT msg ⇒
    212212      COMMENT … msg
     
    218218    | CALL_ID f args ret_regs ⇒
    219219      set_params ? args @@
    220       CALL_ID ertl_params ? f (|args|) it :::
     220      CALL_ID ERTL ? f (|args|) it :::
    221221      fetch_result ? ret_regs
    222222    | extension_call c ⇒
     
    227227    ]
    228228  | COND r ltrue ⇒
    229     COND ertl_params ? r ltrue
     229    COND ERTL ? r ltrue
    230230  ]. cases daemon (* pointer call to be ported yet *) qed.
    231231
    232232definition translate_fin_step :
    233   ∀globals.label → joint_fin_step rtlntc_params
    234     bind_seq_block ertl_params globals (joint_fin_step ertl_params) ≝
     233  ∀globals.label → joint_fin_step RTL_ntc
     234    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
    235235  λglobals.λ_.λs.
    236236  match s with
     
    242242(* hack with empty graphs used here *)
    243243definition translate_funct :
    244   ∀globals.joint_internal_function globals rtlntc_params →
    245     joint_internal_function globals ertl_params ≝
     244  ∀globals.joint_internal_function RTL_ntc globals →
     245    joint_internal_function ERTL globals ≝
    246246  λglobals,def.
    247247  let nb_params ≝ |joint_if_params ?? def| in
     
    253253  let graph' ≝ add ? ? graph' exit' (RETURN …) in
    254254  let def' ≝
    255     mk_joint_internal_function globals ertl_params
     255    mk_joint_internal_function ERTL globals
    256256      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    257257      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
     
    272272  λglobals.
    273273  λstmt.
    274   λdef: joint_internal_function globals ertl_params.
     274  λdef: joint_internal_function globals ERTL.
    275275  let 〈entry, def〉 ≝ fresh_label … def in
    276276  let graph ≝ add … (joint_if_code … def) entry stmt in
    277    set_joint_if_graph … (ertl_params globals) graph def ??.
     277   set_joint_if_graph … (ERTL globals) graph def ??.
    278278  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
    279279  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     
    295295         match inst with
    296296          [ COST_LABEL cost_lbl ⇒
    297              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
     297             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
    298298          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    299299      | RETURN ⇒ 〈None …, def〉
     
    310310  match cost_label with
    311311  [ None ⇒ def
    312   | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
     312  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    313313  ].
    314314
Note: See TracChangeset for help on using the changeset viewer.