Changeset 1636 for src/RTL


Ignore:
Timestamp:
Jan 9, 2012, 12:38:32 PM (9 years ago)
Author:
tranquil
Message:
  • added coercions to arguments (in RTL) and notation for ops (for the momenti in RTLabsToRTL)
  • changed slightly notations for bindLists
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1635 r1636  
    44  | Reg : register → rtl_argument
    55  | Imm : Byte → rtl_argument.
     6 
     7coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
     8  on _r : register to rtl_argument.
     9
     10coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
     11  on _b : Byte to rtl_argument.
     12
     13definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
     14 
     15coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
     16  on _n : nat to rtl_argument.
    617
    718(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
     
    1425  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
    1526
    16  
    17 definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
    1827 
    1928inductive rtl_move : Type[0] ≝
     
    4554      (* paramsT ≝ *) (list register))
    4655      (* localsT ≝ *) (list register)).
    47    
     56
     57(* aid unification *)
     58include "hints_declaration.ma".
     59unification hint 0 ≔
     60(*---------------*) ⊢
     61acc_a_reg (g_inst_pars rtl_params) ≡ register.
     62unification hint 0 ≔
     63(*---------------*) ⊢
     64acc_b_reg (g_inst_pars rtl_params) ≡ register.
     65unification hint 0 ≔
     66(*---------------*) ⊢
     67acc_a_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     68unification hint 0 ≔
     69(*---------------*) ⊢
     70acc_b_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     71unification hint 0 ≔
     72(*---------------*) ⊢
     73dpl_reg (g_inst_pars rtl_params) ≡ register.
     74unification hint 0 ≔
     75(*---------------*) ⊢
     76dph_reg (g_inst_pars rtl_params) ≡ register.
     77unification hint 0 ≔
     78(*---------------*) ⊢
     79dpl_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     80unification hint 0 ≔
     81(*---------------*) ⊢
     82dph_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     83unification hint 0 ≔
     84(*---------------*) ⊢
     85snd_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     86unification hint 0 ≔
     87(*---------------*) ⊢
     88operator1 (g_inst_pars rtl_params) ≡ Op1.
     89unification hint 0 ≔
     90(*---------------*) ⊢
     91operator2 (g_inst_pars rtl_params) ≡ Op2.
     92unification hint 0 ≔
     93(*---------------*) ⊢
     94pair_move (g_inst_pars rtl_params) ≡ rtl_move.
     95unification hint 0 ≔
     96(*---------------*) ⊢
     97call_args (g_inst_pars rtl_params) ≡ list rtl_argument.
     98unification hint 0 ≔
     99(*---------------*) ⊢
     100call_dest (g_inst_pars rtl_params) ≡ list register.
     101
     102check (λglobals,r.OP2 rtl_params globals Or r r r)
     103
    48104definition rtl_instruction ≝ joint_instruction rtl_params.
    49105definition rtl_statement ≝ joint_statement rtl_params.
Note: See TracChangeset for help on using the changeset viewer.