Changeset 2155 for src/RTL/RTL_paolo.ma


Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (8 years ago)
Author:
tranquil
Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1882 r2155  
    1616  on _n : nat to rtl_argument.
    1717
    18 inductive rtl_step_extension: Type[0] ≝
    19   | rtl_st_ext_stack_address: register → register → rtl_step_extension
    20   | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension.
     18inductive rtl_seq : Type[0] ≝
     19  | rtl_stack_address: register → register → rtl_seq.
     20 
     21inductive rtl_call : Type[0] ≝
     22  | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
    2123
    22 inductive rtl_statement_extension : Type[0] ≝
    23   | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
    24   | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
     24inductive rtl_tailcall : Type[0] ≝
     25  | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
     26  | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
    2527
    2628definition rtl_uns_params ≝ mk_unserialized_params
     
    3840    (* call_args ≝ *) (list rtl_argument)
    3941    (* call_dest ≝ *) (list register)
    40     (* ext_step ≝ *) rtl_step_extension
    41     (* ext_step_labels ≝ *) (λes.[ ])
    42     (* ext_fin_stmt ≝ *) rtl_statement_extension
    43     (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
     42    (* ext_seq ≝ *) rtl_seq
     43    (* ext_call ≝ *) rtl_call
     44    (* ext_tailcall ≝ *) rtl_tailcall
     45  )
    4446  (mk_local_params
    4547    (mk_funct_params
    4648      (* resultT ≝ *) (list register)
    4749      (* paramsT ≝ *) (list register))
    48       (* localsT ≝ *) (list register)).
     50      (* localsT ≝ *) register).
    4951
    5052definition rtl_params ≝ mk_graph_params rtl_uns_params.
     
    5456definition rtl_program ≝ joint_program rtl_params.
    5557definition rtl_step ≝ joint_step rtl_params.
     58definition rtl_seq ≝ joint_seq rtl_params.
    5659definition rtl_statement ≝ joint_statement rtl_params.
    57 
    5860
    5961interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
     
    6365unification hint 0 ≔
    6466(*---------------*) ⊢
    65 acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     67acc_a_reg rtl_params ≡ register.
    6668unification hint 0 ≔
    6769(*---------------*) ⊢
    68 acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     70acc_b_reg rtl_params ≡ register.
    6971unification hint 0 ≔
    7072(*---------------*) ⊢
    71 acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     73acc_a_arg rtl_params ≡ rtl_argument.
    7274unification hint 0 ≔
    7375(*---------------*) ⊢
    74 acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     76acc_b_arg rtl_params ≡ rtl_argument.
    7577unification hint 0 ≔
    7678(*---------------*) ⊢
    77 dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     79dpl_reg rtl_params ≡ register.
    7880unification hint 0 ≔
    7981(*---------------*) ⊢
    80 dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     82dph_reg rtl_params ≡ register.
    8183unification hint 0 ≔
    8284(*---------------*) ⊢
    83 dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     85dpl_arg rtl_params ≡ rtl_argument.
    8486unification hint 0 ≔
    8587(*---------------*) ⊢
    86 dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     88dph_arg rtl_params ≡ rtl_argument.
    8789unification hint 0 ≔
    8890(*---------------*) ⊢
    89 snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     91snd_arg rtl_params ≡ rtl_argument.
    9092unification hint 0 ≔
    9193(*---------------*) ⊢
    92 pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
     94pair_move rtl_params ≡ register × rtl_argument.
    9395unification hint 0 ≔
    9496(*---------------*) ⊢
    95 call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
     97call_args rtl_params ≡ list rtl_argument.
    9698unification hint 0 ≔
    9799(*---------------*) ⊢
    98 call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
     100call_dest rtl_params ≡ list register.
    99101
    100102unification hint 0 ≔
    101103(*---------------*) ⊢
    102 ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
     104ext_seq rtl_params ≡ rtl_seq.
     105unification hint 0 ≔
     106(*---------------*) ⊢
     107ext_call rtl_params ≡ rtl_call.
     108unification hint 0 ≔
     109(*---------------*) ⊢
     110ext_tailcall rtl_params ≡ rtl_tailcall.
    103111unification hint 0 ≔ globals
    104112(*---------------*) ⊢
    105 joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.
     113joint_step rtl_params globals ≡ rtl_step globals.
    106114
    107 unification hint 0 ≔
     115unification hint 0 ≔ globals
    108116(*---------------*) ⊢
    109 ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
     117joint_seq rtl_params globals ≡ rtl_seq globals.
    110118unification hint 0 ≔ globals
    111119(*---------------*) ⊢
    112120joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    113121
     122coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
     123  on _r : register to snd_arg rtl_params.
     124coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
     125  on _b : Byte to snd_arg rtl_params.
     126
     127
    114128(************ Same without tail calls ****************)
    115 
    116 inductive rtlntc_statement_extension: Type[0] ≝
    117   | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
    118   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    119129
    120130definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
     
    132142    (* call_args ≝ *) (list rtl_argument)
    133143    (* call_dest ≝ *) (list register)
    134     (* extend_statements ≝ *) rtlntc_statement_extension
    135     (* ext_forall_labels ≝ *) (λes.[ ])
    136     void (λes.[ ]))
     144    (* ext_seq ≝ *) rtl_seq
     145    (* ext_call ≝ *) rtl_call
     146    (* ext_tailcall ≝ *) void
     147  )
    137148  (mk_local_params
    138149    (mk_funct_params
    139150      (* resultT ≝ *) (list register)
    140151      (* paramsT ≝ *) (list register))
    141       (* localsT ≝ *) (list register))).
     152      (* localsT ≝ *) register)).
    142153
    143154definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
Note: See TracChangeset for help on using the changeset viewer.