Changeset 2286 for src/RTL/RTL.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1348 r2286  
    11include "joint/Joint.ma".
    22
    3 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
    4   are not sequential. Thus there is a dummy label at the moment in the code.
    5   To be fixed once we understand exactly what to do with tail calls. *)
    6 inductive rtl_statement_extension: Type[0] ≝
    7   | rtl_st_ext_stack_address: register → register → rtl_statement_extension
    8   | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
    9   | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
    10   | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
     3inductive rtl_seq : Type[0] ≝
     4  | rtl_stack_address: register → register → rtl_seq.
     5 
     6inductive rtl_call : Type[0] ≝
     7  | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    118
    12 definition rtl_params__: params__ ≝
    13  mk_params__ register register register register (register × register) register
    14   (list register) (list register) rtl_statement_extension.
    15 definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
    16 definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
    17 definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
    18 definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.
     9inductive 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.
    1912
    20 definition rtl_statement ≝ joint_statement rtl_params_.
     13definition RTL_uns ≝ mk_unserialized_params
     14    (* acc_a_reg ≝ *) register
     15    (* acc_b_reg ≝ *) register
     16    (* acc_a_arg ≝ *) psd_argument
     17    (* acc_b_arg ≝ *) psd_argument
     18    (* dpl_reg   ≝ *) register
     19    (* dph_reg   ≝ *) register
     20    (* dpl_arg   ≝ *) psd_argument
     21    (* dph_arg   ≝ *) psd_argument
     22    (* snd_arg   ≝ *) psd_argument
     23    (* pair_move ≝ *) (register × psd_argument)
     24    (* call_args ≝ *) (list psd_argument)
     25    (* call_dest ≝ *) (list register)
     26    (* ext_seq ≝ *) rtl_seq
     27    (* ext_call ≝ *) rtl_call
     28    (* ext_tailcall ≝ *) rtl_tailcall
     29    (* paramsT ≝ *) (list register)
     30    (* localsT ≝ *) register.
    2131
    22 definition rtl_internal_function ≝
    23   λglobals. joint_internal_function … (rtl_params globals).
     32definition RTL ≝ mk_graph_params RTL_uns.
     33definition rtl_program ≝ joint_program RTL.
    2434
    25 definition rtl_program ≝ joint_program rtl_params.
     35interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
     36
     37(* aid unification *)
     38include "hints_declaration.ma".
     39unification hint 0 ≔
     40(*---------------*) ⊢
     41acc_a_reg RTL ≡ register.
     42unification hint 0 ≔
     43(*---------------*) ⊢
     44acc_b_reg RTL ≡ register.
     45unification hint 0 ≔
     46(*---------------*) ⊢
     47acc_a_arg RTL ≡ psd_argument.
     48unification hint 0 ≔
     49(*---------------*) ⊢
     50acc_b_arg RTL ≡ psd_argument.
     51unification hint 0 ≔
     52(*---------------*) ⊢
     53dpl_reg RTL ≡ register.
     54unification hint 0 ≔
     55(*---------------*) ⊢
     56dph_reg RTL ≡ register.
     57unification hint 0 ≔
     58(*---------------*) ⊢
     59dpl_arg RTL ≡ psd_argument.
     60unification hint 0 ≔
     61(*---------------*) ⊢
     62dph_arg RTL ≡ psd_argument.
     63unification hint 0 ≔
     64(*---------------*) ⊢
     65snd_arg RTL ≡ psd_argument.
     66unification hint 0 ≔
     67(*---------------*) ⊢
     68pair_move RTL ≡ register × psd_argument.
     69unification hint 0 ≔
     70(*---------------*) ⊢
     71call_args RTL ≡ list psd_argument.
     72unification hint 0 ≔
     73(*---------------*) ⊢
     74call_dest RTL ≡ list register.
     75
     76unification hint 0 ≔
     77(*---------------*) ⊢
     78ext_seq RTL ≡ rtl_seq.
     79unification hint 0 ≔
     80(*---------------*) ⊢
     81ext_call RTL ≡ rtl_call.
     82unification hint 0 ≔
     83(*---------------*) ⊢
     84ext_tailcall RTL ≡ rtl_tailcall.
     85
     86coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     87  on _r : register to snd_arg RTL.
     88coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
     89  on _b : Byte to snd_arg RTL.
     90
    2691
    2792(************ Same without tail calls ****************)
    2893
    29 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
    30   are not sequential. Thus there is a dummy label at the moment in the code.
    31   To be fixed once we understand exactly what to do with tail calls. *)
    32 inductive rtlntc_statement_extension: Type[0] ≝
    33   | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
    34   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
     94definition 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).
    35112
    36 definition rtlntc_params__: params__ ≝
    37  mk_params__ register register register register (register × register) register
    38   (list register) (list register) rtlntc_statement_extension.
    39 definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
    40 definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
    41 definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
    42 definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.
    43 
    44 definition rtlntc_statement ≝ joint_statement rtlntc_params_.
    45 
    46 definition rtlntc_internal_function ≝
    47   λglobals. joint_internal_function … (rtlntc_params globals).
    48 
    49 definition rtlntc_program ≝ joint_program rtlntc_params.
     113definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracChangeset for help on using the changeset viewer.