Changeset 2208 for src/RTL/RTL_paolo.ma


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r2186 r2208  
    11include "joint/Joint_paolo.ma".
    2 
    3 inductive rtl_argument : Type[0] ≝
    4   | Reg : register → rtl_argument
    5   | Imm : Byte → rtl_argument.
    6  
    7 coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
    8   on _r : register to rtl_argument.
    9 
    10 coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
    11   on _b : Byte to rtl_argument.
    12 
    13 definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
    14  
    15 coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
    16   on _n : nat to rtl_argument.
    172
    183inductive rtl_seq : Type[0] ≝
     
    205 
    216inductive rtl_call : Type[0] ≝
    22   | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
     7  | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    238
    249inductive 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.
     10  | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
     11  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    2712
    2813definition rtl_uns_params ≝ mk_unserialized_params
     
    3015    (* acc_a_reg ≝ *) register
    3116    (* acc_b_reg ≝ *) register
    32     (* acc_a_arg ≝ *) rtl_argument
    33     (* acc_b_arg ≝ *) rtl_argument
     17    (* acc_a_arg ≝ *) psd_argument
     18    (* acc_b_arg ≝ *) psd_argument
    3419    (* dpl_reg   ≝ *) register
    3520    (* dph_reg   ≝ *) register
    36     (* dpl_arg   ≝ *) rtl_argument
    37     (* dph_arg   ≝ *) rtl_argument
    38     (* snd_arg   ≝ *) rtl_argument
    39     (* pair_move ≝ *) (register × rtl_argument)
    40     (* call_args ≝ *) (list rtl_argument)
     21    (* dpl_arg   ≝ *) psd_argument
     22    (* dph_arg   ≝ *) psd_argument
     23    (* snd_arg   ≝ *) psd_argument
     24    (* pair_move ≝ *) (register × psd_argument)
     25    (* call_args ≝ *) (list psd_argument)
    4126    (* call_dest ≝ *) (list register)
    4227    (* ext_seq ≝ *) rtl_seq
     
    5944definition rtl_statement ≝ joint_statement rtl_params.
    6045
    61 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)).
     46interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
    6247
    6348(* aid unification *)
     
    7156unification hint 0 ≔
    7257(*---------------*) ⊢
    73 acc_a_arg rtl_params ≡ rtl_argument.
     58acc_a_arg rtl_params ≡ psd_argument.
    7459unification hint 0 ≔
    7560(*---------------*) ⊢
    76 acc_b_arg rtl_params ≡ rtl_argument.
     61acc_b_arg rtl_params ≡ psd_argument.
    7762unification hint 0 ≔
    7863(*---------------*) ⊢
     
    8368unification hint 0 ≔
    8469(*---------------*) ⊢
    85 dpl_arg rtl_params ≡ rtl_argument.
     70dpl_arg rtl_params ≡ psd_argument.
    8671unification hint 0 ≔
    8772(*---------------*) ⊢
    88 dph_arg rtl_params ≡ rtl_argument.
     73dph_arg rtl_params ≡ psd_argument.
    8974unification hint 0 ≔
    9075(*---------------*) ⊢
    91 snd_arg rtl_params ≡ rtl_argument.
     76snd_arg rtl_params ≡ psd_argument.
    9277unification hint 0 ≔
    9378(*---------------*) ⊢
    94 pair_move rtl_params ≡ register × rtl_argument.
     79pair_move rtl_params ≡ register × psd_argument.
    9580unification hint 0 ≔
    9681(*---------------*) ⊢
    97 call_args rtl_params ≡ list rtl_argument.
     82call_args rtl_params ≡ list psd_argument.
    9883unification hint 0 ≔
    9984(*---------------*) ⊢
     
    120105joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    121106
    122 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
     107coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
    123108  on _r : register to snd_arg rtl_params.
    124 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
     109coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
    125110  on _b : Byte to snd_arg rtl_params.
    126111
     
    132117    (* acc_a_reg ≝ *) register
    133118    (* acc_b_reg ≝ *) register
    134     (* acc_a_arg ≝ *) rtl_argument
    135     (* acc_b_arg ≝ *) rtl_argument
     119    (* acc_a_arg ≝ *) psd_argument
     120    (* acc_b_arg ≝ *) psd_argument
    136121    (* dpl_reg   ≝ *) register
    137122    (* dph_reg   ≝ *) register
    138     (* dpl_arg   ≝ *) rtl_argument
    139     (* dph_arg   ≝ *) rtl_argument
    140     (* snd_arg   ≝ *) rtl_argument
    141     (* pair_move ≝ *) (register × rtl_argument)
    142     (* call_args ≝ *) (list rtl_argument)
     123    (* dpl_arg   ≝ *) psd_argument
     124    (* dph_arg   ≝ *) psd_argument
     125    (* snd_arg   ≝ *) psd_argument
     126    (* pair_move ≝ *) (register × psd_argument)
     127    (* call_args ≝ *) (list psd_argument)
    143128    (* call_dest ≝ *) (list register)
    144129    (* ext_seq ≝ *) rtl_seq
Note: See TracChangeset for help on using the changeset viewer.