Changeset 2490 for src/RTL/RTL.ma


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (8 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r2286 r2490  
    44  | rtl_stack_address: register → register → rtl_seq.
    55 
    6 inductive rtl_call : Type[0] ≝
    7   | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    8 
    9 inductive rtl_tailcall : Type[0] ≝
    10   | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
    11   | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    12 
    13 definition RTL_uns ≝ mk_unserialized_params
     6definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params
    147    (* acc_a_reg ≝ *) register
    158    (* acc_b_reg ≝ *) register
     
    2518    (* call_dest ≝ *) (list register)
    2619    (* ext_seq ≝ *) rtl_seq
    27     (* ext_call ≝ *) rtl_call
    28     (* ext_tailcall ≝ *) rtl_tailcall
     20    (* has_tailcalls ≝ *) has_tailcalls
    2921    (* paramsT ≝ *) (list register)
    3022    (* localsT ≝ *) register.
    3123
    32 definition RTL ≝ mk_graph_params RTL_uns.
     24definition RTL ≝ mk_graph_params (RTL_uns true).
    3325definition rtl_program ≝ joint_program RTL.
    3426
     
    7769(*---------------*) ⊢
    7870ext_seq RTL ≡ rtl_seq.
    79 unification hint 0 ≔
    80 (*---------------*) ⊢
    81 ext_call RTL ≡ rtl_call.
    82 unification hint 0 ≔
    83 (*---------------*) ⊢
    84 ext_tailcall RTL ≡ rtl_tailcall.
    8571
    8672coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     
    9278(************ Same without tail calls ****************)
    9379
    94 definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    95     (* acc_a_reg ≝ *) register
    96     (* acc_b_reg ≝ *) register
    97     (* acc_a_arg ≝ *) psd_argument
    98     (* acc_b_arg ≝ *) psd_argument
    99     (* dpl_reg   ≝ *) register
    100     (* dph_reg   ≝ *) register
    101     (* dpl_arg   ≝ *) psd_argument
    102     (* dph_arg   ≝ *) psd_argument
    103     (* snd_arg   ≝ *) psd_argument
    104     (* pair_move ≝ *) (register × psd_argument)
    105     (* call_args ≝ *) (list psd_argument)
    106     (* call_dest ≝ *) (list register)
    107     (* ext_seq ≝ *) rtl_seq
    108     (* ext_call ≝ *) rtl_call
    109     (* ext_tailcall ≝ *) void
    110     (* paramsT ≝ *) (list register)
    111     (* localsT ≝ *) register).
    112 
     80definition RTL_ntc ≝ mk_graph_params (RTL_uns false).
    11381definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracChangeset for help on using the changeset viewer.