Changeset 2286 for src/ERTL/ERTL.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/ERTL/ERTL.ma

    r1388 r2286  
    11include "joint/Joint.ma".
    22
    3 inductive move_registers: Type[0] ≝
    4   | pseudo: register → move_registers
    5   | hardware: Register → move_registers.
    6                  
    7 inductive ertl_statement_extension: Type[0] ≝
    8   | ertl_st_ext_new_frame: ertl_statement_extension
    9   | ertl_st_ext_del_frame: ertl_statement_extension
    10   | ertl_st_ext_frame_size: register → ertl_statement_extension.
     3inductive move_dst: Type[0] ≝
     4  | PSD: register → move_dst
     5  | HDW: Register → move_dst.
    116
    12 definition ertl_params__: params__ ≝
    13  mk_params__ register register register register (move_registers × move_registers)
    14   register nat unit ertl_statement_extension.
    15 definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
    16 definition ertl_params0: params0 ≝ mk_params0 ertl_params__ (list register) nat.
    17 definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
    18 definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
     7definition move_src ≝ argument move_dst.
    198
    20 definition ertl_statement ≝ joint_statement ertl_params_.
     9definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
     10coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
    2111
    22 definition ertl_internal_function ≝
    23   λglobals.joint_internal_function … (ertl_params globals).
     12definition psd_argument_move_src : psd_argument → move_src ≝
     13  λarg.match arg with
     14  [ Imm b ⇒ Imm ? b
     15  | Reg r ⇒ Reg ? (PSD r)
     16  ].
     17coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
     18  psd_argument_move_src on _a : psd_argument to move_src.
    2419
    25 definition ertl_program ≝ joint_program ertl_params.
     20inductive ertl_seq : Type[0] ≝
     21  | ertl_new_frame: ertl_seq
     22  | ertl_del_frame: ertl_seq
     23  | ertl_frame_size: register → ertl_seq.
     24
     25definition ERTL_uns ≝ mk_unserialized_params
     26    (* acc_a_reg ≝ *) register
     27    (* acc_b_reg ≝ *) register
     28    (* acc_a_arg ≝ *) psd_argument
     29    (* acc_b_arg ≝ *) psd_argument
     30    (* dpl_reg   ≝ *) register
     31    (* dph_reg   ≝ *) register
     32    (* dpl_arg   ≝ *) psd_argument
     33    (* dph_arg   ≝ *) psd_argument
     34    (* snd_arg   ≝ *) psd_argument
     35    (* pair_move ≝ *) (move_dst × move_src)
     36    (* call_args ≝ *) ℕ
     37    (* call_dest ≝ *) unit
     38    (* ext_seq ≝ *) ertl_seq
     39    (* ext_call ≝ *) void
     40    (* ext_tailcall ≝ *) void
     41    (* paramsT ≝ *) ℕ
     42    (* localsT ≝ *) register.
     43
     44definition ERTL ≝ mk_graph_params ERTL_uns.
     45definition ertl_program ≝ joint_program ERTL.
     46
     47interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
     48
     49(* aid unification *)
     50unification hint 0 ≔
     51(*---------------*) ⊢
     52pair_move ERTL ≡ move_dst × move_src.
     53unification hint 0 ≔
     54(*---------------*) ⊢
     55acc_a_reg ERTL ≡ register.
     56unification hint 0 ≔
     57(*---------------*) ⊢
     58acc_b_reg ERTL ≡ register.
     59unification hint 0 ≔
     60(*---------------*) ⊢
     61acc_a_arg ERTL ≡ psd_argument.
     62unification hint 0 ≔
     63(*---------------*) ⊢
     64acc_b_arg ERTL ≡ psd_argument.
     65unification hint 0 ≔
     66(*---------------*) ⊢
     67dpl_reg ERTL ≡ register.
     68unification hint 0 ≔
     69(*---------------*) ⊢
     70dph_reg ERTL ≡ register.
     71unification hint 0 ≔
     72(*---------------*) ⊢
     73dpl_arg ERTL ≡ psd_argument.
     74unification hint 0 ≔
     75(*---------------*) ⊢
     76dph_arg ERTL ≡ psd_argument.
     77unification hint 0 ≔
     78(*---------------*) ⊢
     79snd_arg ERTL ≡ psd_argument.
     80unification hint 0 ≔
     81(*---------------*) ⊢
     82call_args ERTL ≡ ℕ.
     83unification hint 0 ≔
     84(*---------------*) ⊢
     85call_dest ERTL ≡ unit.
     86
     87unification hint 0 ≔
     88(*---------------*) ⊢
     89ext_seq ERTL ≡ ertl_seq.
     90unification hint 0 ≔
     91(*---------------*) ⊢
     92ext_call ERTL ≡ void.
     93unification hint 0 ≔
     94(*---------------*) ⊢
     95ext_tailcall ERTL ≡ void.
     96
     97coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
     98  psd_argument_from_reg
     99  on _r : register to snd_arg ERTL.
     100coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝
     101  psd_argument_from_byte
     102  on _b : Byte to snd_arg ERTL.
     103 
     104definition ertl_seq_joint ≝ extension_seq ERTL.
     105coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
     106  on _s : ertl_seq to joint_seq ERTL.
Note: See TracChangeset for help on using the changeset viewer.