Changeset 1640 for src/RTL


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (8 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1636 r1640  
    2525  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
    2626
    27  
    28 inductive rtl_move : Type[0] ≝
    29   | CARRY : bool → rtl_move
    30   | REG : register → rtl_argument → rtl_move.
    31  
    32 (* avoid expansion *)
    33 definition rtl_params : graph_params ≝ mk_graph_params
     27definition rtl_params ≝ mk_graph_params (mk_unserialized_params
    3428  (mk_inst_params
    3529    (* acc_a_reg ≝ *) register
     
    4236    (* dph_arg   ≝ *) rtl_argument
    4337    (* snd_arg   ≝ *) rtl_argument
    44     (* operator1 ≝ *) Op1
    45     (* operator2 ≝ *) Op2
    46     (* pair_move ≝ *) rtl_move
     38    (* pair_move ≝ *) (register × rtl_argument)
    4739    (* call_args ≝ *) (list rtl_argument)
    4840    (* call_dest ≝ *) (list register)
     
    5345      (* resultT ≝ *) (list register)
    5446      (* paramsT ≝ *) (list register))
    55       (* localsT ≝ *) (list register)).
     47      (* localsT ≝ *) (list register))).
     48
     49interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
    5650
    5751(* aid unification *)
     
    5953unification hint 0 ≔
    6054(*---------------*) ⊢
    61 acc_a_reg (g_inst_pars rtl_params) ≡ register.
     55acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    6256unification hint 0 ≔
    6357(*---------------*) ⊢
    64 acc_b_reg (g_inst_pars rtl_params) ≡ register.
     58acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    6559unification hint 0 ≔
    6660(*---------------*) ⊢
    67 acc_a_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     61acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    6862unification hint 0 ≔
    6963(*---------------*) ⊢
    70 acc_b_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     64acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    7165unification hint 0 ≔
    7266(*---------------*) ⊢
    73 dpl_reg (g_inst_pars rtl_params) ≡ register.
     67dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    7468unification hint 0 ≔
    7569(*---------------*) ⊢
    76 dph_reg (g_inst_pars rtl_params) ≡ register.
     70dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    7771unification hint 0 ≔
    7872(*---------------*) ⊢
    79 dpl_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     73dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    8074unification hint 0 ≔
    8175(*---------------*) ⊢
    82 dph_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     76dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    8377unification hint 0 ≔
    8478(*---------------*) ⊢
    85 snd_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     79snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    8680unification hint 0 ≔
    8781(*---------------*) ⊢
    88 operator1 (g_inst_pars rtl_params) ≡ Op1.
     82pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
    8983unification hint 0 ≔
    9084(*---------------*) ⊢
    91 operator2 (g_inst_pars rtl_params) ≡ Op2.
     85call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
    9286unification hint 0 ≔
    9387(*---------------*) ⊢
    94 pair_move (g_inst_pars rtl_params) ≡ rtl_move.
    95 unification hint 0 ≔
    96 (*---------------*) ⊢
    97 call_args (g_inst_pars rtl_params) ≡ list rtl_argument.
    98 unification hint 0 ≔
    99 (*---------------*) ⊢
    100 call_dest (g_inst_pars rtl_params) ≡ list register.
     88call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
    10189
    102 check (λglobals,r.OP2 rtl_params globals Or r r r)
    10390
    10491definition rtl_instruction ≝ joint_instruction rtl_params.
    105 definition rtl_statement ≝ joint_statement rtl_params.
    106 
    107 
    108 definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝
    109   λglobals,r,k.
    110   MOVE rtl_params globals (REG r (imm_nat k)).
    111 
    112 definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝
    113   λglobals,r,k.
    114   MOVE rtl_params globals (REG r (Imm k)).
    115 
    116 definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝
    117   λglobals,r,k.
    118   MOVE … (REG r (Reg k)).
    119 
    120 definition set_carry : ∀globals.rtl_instruction globals ≝
    121   λglobals.MOVE … (CARRY true).
    122 
    123 definition clear_carry : ∀globals.rtl_instruction globals ≝
    124   λglobals.MOVE … (CARRY false).
    125  
     92(* Paolo: can't understand why coercions do not compose implicitly here *)
     93definition rtl_statement ≝ joint_statement (rtl_params : params).
    12694
    12795definition rtl_internal_function ≝
     
    136104  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    137105
    138 definition rtlntc_params : graph_params ≝ mk_graph_params
     106definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
    139107  (mk_inst_params
    140108    (* acc_a_reg ≝ *) register
     
    147115    (* dph_arg   ≝ *) rtl_argument
    148116    (* snd_arg   ≝ *) rtl_argument
    149     (* operator1 ≝ *) Op1
    150     (* operator2 ≝ *) Op2
    151     (* pair_move ≝ *) rtl_move
     117    (* pair_move ≝ *) (register × rtl_argument)
    152118    (* call_args ≝ *) (list rtl_argument)
    153119    (* call_dest ≝ *) (list register)
     
    158124      (* resultT ≝ *) (list register)
    159125      (* paramsT ≝ *) (list register))
    160       (* localsT ≝ *) (list register)).
     126      (* localsT ≝ *) (list register))).
    161127
    162 definition rtlntc_statement ≝ joint_statement rtlntc_params.
     128definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
    163129
    164130definition rtlntc_internal_function ≝
Note: See TracChangeset for help on using the changeset viewer.