Changeset 2214 for src/RTL/RTL_paolo.ma


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/RTL_paolo.ma

    r2208 r2214  
    1111  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    1212
    13 definition rtl_uns_params ≝ mk_unserialized_params
     13definition RTL_uns ≝ mk_unserialized_params
    1414  (mk_step_params
    1515    (* acc_a_reg ≝ *) register
     
    3535      (* localsT ≝ *) register).
    3636
    37 definition rtl_params ≝ mk_graph_params rtl_uns_params.
    38 definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
    39 definition rtl_internal_function ≝
    40   λglobals. joint_internal_function globals rtl_params.
    41 definition rtl_program ≝ joint_program rtl_params.
    42 definition rtl_step ≝ joint_step rtl_params.
    43 definition rtl_seq ≝ joint_seq rtl_params.
    44 definition rtl_statement ≝ joint_statement rtl_params.
     37definition RTL ≝ mk_graph_params RTL_uns.
     38definition rtl_program ≝ joint_program RTL.
    4539
    46 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
     40interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
    4741
    4842(* aid unification *)
     
    5044unification hint 0 ≔
    5145(*---------------*) ⊢
    52 acc_a_reg rtl_params ≡ register.
     46acc_a_reg RTL ≡ register.
    5347unification hint 0 ≔
    5448(*---------------*) ⊢
    55 acc_b_reg rtl_params ≡ register.
     49acc_b_reg RTL ≡ register.
    5650unification hint 0 ≔
    5751(*---------------*) ⊢
    58 acc_a_arg rtl_params ≡ psd_argument.
     52acc_a_arg RTL ≡ psd_argument.
    5953unification hint 0 ≔
    6054(*---------------*) ⊢
    61 acc_b_arg rtl_params ≡ psd_argument.
     55acc_b_arg RTL ≡ psd_argument.
    6256unification hint 0 ≔
    6357(*---------------*) ⊢
    64 dpl_reg rtl_params ≡ register.
     58dpl_reg RTL ≡ register.
    6559unification hint 0 ≔
    6660(*---------------*) ⊢
    67 dph_reg rtl_params ≡ register.
     61dph_reg RTL ≡ register.
    6862unification hint 0 ≔
    6963(*---------------*) ⊢
    70 dpl_arg rtl_params ≡ psd_argument.
     64dpl_arg RTL ≡ psd_argument.
    7165unification hint 0 ≔
    7266(*---------------*) ⊢
    73 dph_arg rtl_params ≡ psd_argument.
     67dph_arg RTL ≡ psd_argument.
    7468unification hint 0 ≔
    7569(*---------------*) ⊢
    76 snd_arg rtl_params ≡ psd_argument.
     70snd_arg RTL ≡ psd_argument.
    7771unification hint 0 ≔
    7872(*---------------*) ⊢
    79 pair_move rtl_params ≡ register × psd_argument.
     73pair_move RTL ≡ register × psd_argument.
    8074unification hint 0 ≔
    8175(*---------------*) ⊢
    82 call_args rtl_params ≡ list psd_argument.
     76call_args RTL ≡ list psd_argument.
    8377unification hint 0 ≔
    8478(*---------------*) ⊢
    85 call_dest rtl_params ≡ list register.
     79call_dest RTL ≡ list register.
    8680
    8781unification hint 0 ≔
    8882(*---------------*) ⊢
    89 ext_seq rtl_params ≡ rtl_seq.
     83ext_seq RTL ≡ rtl_seq.
    9084unification hint 0 ≔
    9185(*---------------*) ⊢
    92 ext_call rtl_params ≡ rtl_call.
     86ext_call RTL ≡ rtl_call.
    9387unification hint 0 ≔
    9488(*---------------*) ⊢
    95 ext_tailcall rtl_params ≡ rtl_tailcall.
    96 unification hint 0 ≔ globals
    97 (*---------------*) ⊢
    98 joint_step rtl_params globals ≡ rtl_step globals.
     89ext_tailcall RTL ≡ rtl_tailcall.
    9990
    100 unification hint 0 ≔ globals
    101 (*---------------*) ⊢
    102 joint_seq rtl_params globals ≡ rtl_seq globals.
    103 unification hint 0 ≔ globals
    104 (*---------------*) ⊢
    105 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    106 
    107 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
    108   on _r : register to snd_arg rtl_params.
    109 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
    110   on _b : Byte to snd_arg rtl_params.
     91coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     92  on _r : register to snd_arg RTL.
     93coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
     94  on _b : Byte to snd_arg RTL.
    11195
    11296
    11397(************ Same without tail calls ****************)
    11498
    115 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
     99definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    116100  (mk_step_params
    117101    (* acc_a_reg ≝ *) register
     
    137121      (* localsT ≝ *) register)).
    138122
    139 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
    140 
    141 definition rtlntc_internal_function ≝
    142   λglobals. joint_internal_function … globals rtlntc_params.
    143 
    144 definition rtlntc_program ≝ joint_program rtlntc_params.
     123definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracChangeset for help on using the changeset viewer.