Changeset 1636


Ignore:
Timestamp:
Jan 9, 2012, 12:38:32 PM (8 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
Location:
src
Files:
3 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.
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1635 r1636  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
     10
     11
     12(* Paolo: to be moved elsewhere *)
     13
     14notation "r ← a1 .op. a2" with precedence 50 for
     15  @{'op2 $op $r $a1 $a2}.
     16notation "r ← . op . a" with precedence 50 for
     17  @{'op1 $op $r $a}.
     18notation "r ← a" with precedence 50 for
     19  @{'mov $r $a}.
     20notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     21  @{'opaccs $op $r $s $a1 $a2}.
     22
     23interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
     24interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
     25interpretation "move" 'mov r a = (MOVE ? ? (REG r a)).
     26interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
     27
    1028
    1129definition size_of_sig_type ≝
     
    138156  λsrcrs2.
    139157  λprf1,prf2.
    140   let f_add ≝ λop,destr,srcr1,srcr2.
    141     OP2 rtl_params globals op destr srcr1 srcr2 in
     158  let f_add ≝ OP2 rtl_params globals in
    142159  let res : list (rtl_instruction globals) ≝
    143160    map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
     
    166183    ] (refl …)
    167184  | _ ⇒ res
    168   ]. 
     185  ].
    169186  [5,6: assumption
    170187  |1: >prf1 in eq_destrs; >eq_srcrs1 normalize //
     
    238255  |destrs| = |srcrs| → list (rtl_instruction globals) ≝
    239256  λglobals,destrs,srcrs,length_eq.
    240   map2 … (λdst,src.MOVE rtl_params … (REG dst src)) destrs srcrs length_eq.
     257  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
    241258
    242259let rec make
     
    269286     *)
    270287  λglobals,destr,srcr.
    271   [OP2 … Or destr (Reg srcr) (imm_nat 127) ;
    272    OP1 … Rl destr destr ;
    273    OP1 … Inc destr destr ;
    274    OP1 … Cmpl destr destr ].
     288  [destr ← srcr .Or. 127 ;
     289   destr ← .Rl. destr ;
     290   destr ← .Inc. destr ;
     291   destr ← .Cmpl. destr ].
    275292   
    276293definition translate_cast_signed :
     
    354371    translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *)
    355372    match srcrs with
    356     [ nil ⇒ [reg_from_nat … destr 0]
     373    [ nil ⇒ [destr ← 0]
    357374    | cons srcr srcrs' ⇒
    358375      let f : register → rtl_instruction globals ≝
     
    364381      (* many uses of 0, better not use immediates *)
    365382      ν tmp in
    366       [reg_from_nat … tmp 0 ;
    367        OP2 … Sub destr (Reg tmp) (Reg tmp) ;
     383      [tmp ← 0 ;
     384       destr ← tmp .Sub. tmp ;
    368385       (* now carry bit is set iff destr was non-null *)
    369        OP2 … Addc destr (Reg tmp) (Reg tmp)]
     386       destr ← tmp .Addc. tmp]
    370387     ]
    371388   ].
     
    461478      let tmp_destrs_view : list register ≝
    462479        ltl ? tmp_destrs_dummy k in
    463       OPACCS rtl_params globals Mul a b
    464         (nth_safe ? i srcrs1 ?)
    465         (nth_safe ? (k - i) srcrs2 ?) ::
     480      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
    466481      translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @
    467482      acc
     
    501516(* temporary registers for the result are created, so to avoid overwriting
    502517   sources *)
    503 ννtmp_destrs: |destrs| with tmp_destrs_prf in
     518νν tmp_destrs × |destrs| with tmp_destrs_prf in
    504519νdummy in
    505520(* the step calculating all products with least significant byte going in the
     
    520535     for i in 0 ... k do
    521536       translate_mul_i … k … i *)
    522 foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
     537foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ 
    523538(* epilogue: saving the result *)
    524539translate_move … destrs (map … Reg tmp_destrs) ?.
     
    552567          let 〈destr1, destr2〉 ≝
    553568            if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
    554           [OPACCS rtl_params globals DivuModu destr1 destr2 srcr1 srcr2]
     569          [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2]
    555570        ] (refl …)
    556571      ] (refl …)
     
    561576destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed.
    562577
     578(* Paolo: to be moved elsewhere *)
    563579let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
    564580  (prf : |l1| = |l2|) on l1 : C ≝
     
    572588    ] (refl …)
    573589  ] (refl …).
    574 [destruct normalize in prf; destruct
    575 |destruct normalize in prf; //
    576 ] qed.
    577 
    578 let rec foldr3 (A : Type[0]) (B : Type[0]) (C : Type[0]) (D : Type[0])
    579   (f : A→B→C→D→D) (init : D) (l1 : list A) (l2 : list B) (l3 : list C)
    580   (prf1 : |l1| = |l2|) (prf2 : |l2| = |l3|) on l1 : D ≝
    581   match l1 return λx.x = l1 → D with 
    582   [ nil ⇒ λ_.init
    583   | cons a l1' ⇒ λeq_l1.
    584     match l2 return λy.y = l2 → D with
    585     [ nil ⇒ λeq_l2.⊥
    586     | cons b l2' ⇒ λeq_l2.
    587       match l3 return λz.z = l3 → D with
    588       [ nil ⇒ λeq_l3.⊥
    589       | cons c l3' ⇒ λeq_l3.
    590         f a b c (foldr3 A B C D f init l1' l2' l3' ? ?)
    591       ] (refl …)
    592     ] (refl …)
    593   ] (refl …).
    594 destruct normalize in prf1; normalize in prf2; destruct // qed.
     590destruct normalize in prf;  [destruct|//]
     591qed.
    595592
    596593definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     
    614611        let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝
    615612          λs1,s2,acc.
    616           OP2 … Xor tmpr s1 s2 ::
    617           OP2 … Or destr (Reg destr) (Reg tmpr) ::
     613          tmpr  ← s1 .Xor. s2 ::
     614          destr ← destr .Or. tmpr ::
    618615          acc in
    619616        let epilogue : list (rtl_instruction globals) ≝
    620617          [ clear_carry … ;
    621             OP2 … Sub tmpr (Imm (zero …)) (Reg destr) ;
     618            tmpr ← 0 .Sub. destr ;
    622619            (* now carry bit is 1 iff destrs != 0 *)
    623             OP2 … Addc destr (Imm (zero …)) (Imm (zero …)) ] in
     620            destr ← 0 .Addc. 0 ] in
    624621         translate_cast_unsigned … destrs' @
    625          OP2 rtl_params globals Xor destr srcr1 srcr2 ::
     622         destr ← srcr1 .Xor. srcr2 ::
    626623         foldr2 ??? f epilogue srcrs1' srcrs2' ?
    627624       ] (refl …)
     
    637634  match destrs with
    638635  [ nil ⇒ [ ]
    639   | cons destr _ ⇒ [OP1 rtl_params globals Cmpl destr destr]
     636  | cons destr _ ⇒ [destr ← .Cmpl. destr]
    640637  ].
    641638 
     
    655652    (* I perform a subtraction, but the only interest is in the carry bit *)
    656653    translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @
    657     [ OP2 … Addc destr (imm_nat 0) (imm_nat 0) ]
     654    [ destr ← 0 .Addc. 0 ]
    658655  ].
    659656[ <make_length ] assumption qed.
     
    669666  | cons srcr srcrs' ⇒
    670667    match srcrs' with
    671     [ nil ⇒ 〈[ Reg tmp ], [ OP2 … Add tmp srcr (imm_nat 128) ]〉
     668    [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
    672669    | _ ⇒
    673670      let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in
  • src/utilities/bindLists.ma

    r1635 r1636  
    6767 }.
    6868 
    69 notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     69notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
     70 ${default
     71   @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) }
     72   @{ 'tnews $ts (λ${ident l}:$ty.$f)}
     73 }.
     74 
     75notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    7076   @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    71 notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
     77notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
    7278   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
    7379
    74 notation > "νν ident l : n opt('with' ident EQ) 'in' f" with precedence 47 for
     80notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for
    7581 ${default
    7682   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
     
    7884 }.
    7985 
    80 notation < "hvbox(νν ident l : n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     86notation > "νν ident l : ty × n opt('with' ident EQ) 'in' f" with precedence 47 for
     87 ${default
     88   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
     89   @{ 'unews $n (λ${ident l}:$ty.$f)}
     90 }.
     91 
     92notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    8193   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    82 notation < "hvbox(νν ident l : n \nbsp 'in' \nbsp break f)" with precedence 47 for
     94notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for
    8395   @{ 'unews $n (λ${ident l} : $ty.$f) }.
    8496
Note: See TracChangeset for help on using the changeset viewer.