Ignore:
Timestamp:
Feb 7, 2013, 3:13:41 PM (7 years ago)
Author:
tranquil
Message:

updated RTL and RTLabs to RTL translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2601 r2640  
    55include "common/Graphs.ma".
    66include "joint/TranslateUtils.ma".
    7 include "utilities/bindLists.ma".
    87include alias "ASM/BitVector.ma".
    98include alias "arithmetics/nat.ma".
    10 
    11 definition rtl_fresh_reg:
    12  ∀globals.freshT RTL globals register ≝
    13   λglobals,def.
    14     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    15     〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    16 
    17 definition rtl_fresh_reg_no_local :
    18  ∀globals.freshT RTL globals register ≝
    19   λglobals,def.
    20     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    21     〈set_runiverse ?? def runiverse, r〉.
    229
    2310definition size_of_sig_type ≝
     
    5744  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
    5845
    59 definition initialize_local_env_internal :
    60   ∀globals.
    61   ((joint_internal_function RTL globals) × local_env) → (register×typ) →
    62   ((joint_internal_function RTL globals) × local_env) ≝
    63   λglobals,def_env,r_sig.
    64   let 〈def,lenv〉 ≝ def_env in
    65   let 〈r, sig〉 ≝ r_sig in
    66   let size ≝ size_of_sig_type sig in
    67   let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in
    68     〈def,add … lenv r rs〉.
     46(* move *)
     47let rec m_iter (M : Monad) X (f : X → M X) (n : ℕ) (m : M X) on n : M X ≝
     48match n with
     49[ O ⇒ m
     50| S k ⇒
     51  ! v ← m ;
     52  m_iter … f k (f v)
     53].
     54
     55definition fresh_registers : ∀p,g.ℕ → state_monad (joint_internal_function p g) (list register) ≝
     56λp,g,n.
     57  let f ≝ λacc.! m ← fresh_register … ; return (m :: acc) in
     58  m_iter … f n (return [ ]).
    6959
    7060include alias "common/Identifiers.ma".
     
    8070  ∀globals.
    8171  list (register×typ) →
    82   freshT RTL globals local_env ≝
    83   λglobals,registers,def.
    84   foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers.
     72  state_monad (joint_internal_function RTL globals) local_env ≝
     73  λglobals,registers.
     74  let f ≝
     75    λr_sig,lenv.
     76    let 〈r, sig〉 ≝ r_sig in
     77    let size ≝ size_of_sig_type sig in
     78    ! regs ← fresh_registers … size ;
     79    return add … lenv r regs in
     80  m_fold … f registers (empty_map …).
    8581
    8682lemma initialize_local_env_in : ∀globals,l,def,r.
    8783  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def).
    88 #globals #l #U #r @(list_elim_left … l)
    89 [ *
    90 | * #tl #sig #hd #IH #G elim (Exists_append … G) -G
    91   whd in match initialize_local_env; normalize nodelta
    92   >foldl_step change with (initialize_local_env ???) in match (foldl ?????);
    93   [ #H lapply (IH H)
    94   | * [2: *] #EQ destruct(EQ)
    95   ] 
    96   cases (initialize_local_env ???)
    97   #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
    98   elim (repeat_fresh ??????) #U'' #rs
    99   [ >mem_set_add @orb_Prop_r assumption
    100   | @mem_set_add_id
    101   ]
     84whd in match initialize_local_env; normalize nodelta #globals
     85cut (∀l,init,def,r.(Exists  ? (λx.\fst x = r) l ∨ bool_to_Prop (r ∈ init)) →
     86     r ∈ \snd (m_fold (state_monad ?) ??? l init def))
     87[7: #aux #l #def #r #H @aux %1{H} |*:]
     88#l elim l -l
     89[ #init #def #r * [*] #H @H ]
     90* #hd #sig #tl #IH #init #def #r #H
     91whd in ⊢ (?(???(???%)?)); normalize nodelta
     92whd in ⊢ (?(???(???(match % with [ _ ⇒ ?]))?));
     93inversion (fresh_registers ????) #def' #regs #EQfresh normalize nodelta
     94@IH cases H -H [*] #H
     95[ destruct %2 @mem_set_add_id
     96| %1{H}
     97| %2 >mem_set_add @orb_Prop_r @H
     98]
    10299qed.
    103100
     
    112109  (* params *) list (register×typ) →
    113110  (* return *) option (register×typ) →
    114   freshT RTL globals local_env ≝
     111  state_monad (joint_internal_function RTL globals) local_env ≝
    115112  λglobals,locals,params,ret,def.
    116113  let 〈def',lenv〉 as EQ ≝
     
    120117     | None ⇒ [ ]
    121118     ]) @ locals @ params) def in
    122   let locals' ≝ map_list_local_env lenv locals ? in
    123119  let params' ≝ map_list_local_env lenv params ? in
    124120  let ret' ≝ match ret return λx.ret = x → ? with
     
    129125    mk_joint_internal_function RTL globals
    130126      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
    131       params' locals' (joint_if_stacksize … def')
    132       (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in
     127      params' (joint_if_stacksize … def')
     128      (joint_if_code … def') (joint_if_entry … def') in
    133129   〈def'', lenv〉. @hide_prf
    134130[ >(proj2_rewrite ????? EQ)
     
    136132|*: >(proj2_rewrite ????? EQ)
    137133  @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr)))
    138   [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
    139     [ #a #H @Exists_append_r @Exists_append_r @H
    140     | generalize in match params;
    141     ]
    142   | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals))
    143     [ #a #H @Exists_append_r @Exists_append_l @H
    144     | generalize in match locals;
    145     ]
     134  @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
     135  [ #a #H @Exists_append_r @Exists_append_r @H
     136  | elim params [%] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #G %2{G}
    146137  ]
    147   #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
    148138]
    149139qed.
     
    152142  λA.
    153143  λlst: list A.
    154   λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf //
     144  λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf [%2] %1
    155145  qed.
    156146
     
    187177
    188178let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝
    189 match l return λx.All A P x → ? with
     179match l return λx.All A P x → list (Σx.P x) with
    190180[ nil ⇒ λ_.[ ]
    191 | cons hd tl ⇒ λprf.«hd, ?» :: list_inject_All_aux A P tl ?
    192 ]. cases prf #H1 #H2 [@H1 | @H2]
    193 qed.
    194 
    195 include alias "basics/lists/list.ma".
     181| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_inject_All_aux A P tl (proj2 … prf)
     182].
     183
    196184definition translate_op:
    197185  ∀globals. Op2 →
     
    200188  ∀srcrs2 : list psd_argument.
    201189  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    202   list (joint_seq RTL globals)
     190  bind_new register (list (joint_seq RTL globals))
    203191  ≝
    204192  λglobals: list ident.
     
    251239definition translate_op_asym_unsigned :
    252240  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
    253   list (joint_seq RTL globals) ≝
     241  bind_new register (list (joint_seq RTL globals)) ≝
    254242  λglobals,op,destrs,srcrs1,srcrs2.
    255243  let l ≝ |destrs| in
     
    257245  let srcrs2' ≝ cast_list ? (zero_byte : psd_argument) l srcrs2 in
    258246  translate_op globals op destrs srcrs1' srcrs2' ??.
     247  @hide_prf
    259248  normalize nodelta
    260249  >length_cast_list [2: >length_cast_list ] %
     
    266255| S size' ⇒
    267256  (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8)
    268 ]. [ % | cases (nat_to_args ??) #res #EQ  normalize >EQ % ] qed.
     257]. @hide_prf [ % | cases (nat_to_args ??) #res #EQ  normalize >EQ % ] qed.
    269258
    270259definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
     
    273262  ].
    274263
    275 (* JHM/BJC 2012.11.26: TODO fix this use of bool_to_Prop/remove other defn of member *)
    276264definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
    277265  match cst with
    278   [ Oaddrsymbol id _ ⇒ bool_to_Prop (member ? (eq_identifier ?) id globals)
     266  [ Oaddrsymbol id _ ⇒ bool_to_Prop (id ∈ globals)
    279267  | _ ⇒ True
    280268  ].
    281 
     269 
    282270definition translate_cst :
    283271  ∀ty.
     
    286274  ∀destrs: list register.
    287275  |destrs| = size_of_cst ? cst_sig →
    288   list (joint_seq RTL globals)
     276  bind_new register (list (joint_seq RTL globals))
    289277 ≝
    290278  λty,globals,cst_sig,destrs.
     
    302290    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
    303291  ] (pi2 … cst_sig).
     292  @hide_prf
    304293  [ cases (split_into_bytes ??) #lst
    305     #EQ >EQ >prf whd in ⊢ (??%?); cases size %.
    306   | @cst_prf (* previously failed to typecheck here, until change 2012.11.26 above *)
     294    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
     295  | @cst_prf
    307296  |*: >prf %
    308297  ]
     
    344333  ∀globals : list ident.
    345334  list register → psd_argument →
    346   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     335  bind_new register (list (joint_seq RTL globals)) ≝
    347336  λglobals,destrs,srca.
    348337  ν tmp in
     
    369358].
    370359
    371 lemma last_not_empty : ∀A,l.
    372   match l with [ nil ⇒ False | _ ⇒ True ] →
     360lemma last_def : ∀A,hd,tl.last A (hd @ [tl]) = Some ? tl.
     361#A #hd elim hd -hd [ #tl % ] #hd * [ #_ #last % ] #hd' #tl #IH #last
     362@IH qed.
     363
     364lemma last_last_ne : ∀A,l.last A (pi1 … l) = Some ? (last_ne … l).
     365#A * @list_elim_left [*] #hd #tl #_ #prf
     366whd in match last_ne; normalize nodelta
     367>split_on_last_ne_def @last_def qed.
     368
     369lemma last_not_empty : ∀A,l.not_empty A l →
    373370  match last A l with
    374371  [ None ⇒ False
    375372  | _ ⇒ True ].
    376 #A #l elim l [ * ]
    377 #hd * [ #_ * % ]
    378 #hd' #tl #IH * @(IH I)
    379 qed.
     373#A #l #prf >(last_last_ne … «l, prf») % qed.
    380374
    381375definition translate_op_asym_signed :
    382376  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
    383   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     377  bind_new register (list (joint_seq RTL globals)) ≝
    384378  λglobals,op,destrs,srcrs1,srcrs2.
    385379  νtmp1,tmp2 in
    386380  let l ≝ |destrs| in
    387   let f ≝ λsrcrs,tmp.
     381  let cast_srcrs ≝ λsrcrs,tmp.
    388382    let srcrs_l ≝ |srcrs| in
    389383    if leb srcrs_l l then
    390       match last srcrs with
     384      match last ? srcrs with
    391385      [ Some last ⇒
    392386        〈srcrs @ make_list … (Reg ? tmp) (l - srcrs_l),
     
    397391    else
    398392      〈lhd … srcrs l, [ ]〉 in
    399   let prf : ∀srcrs,tmp.|destrs| = |\fst (f srcrs tmp)| ≝ ? in
    400   let srcrs1init ≝ f srcrs1 tmp1 in
    401   let srcrs2init ≝ f srcrs2 tmp2 in
    402   \snd srcrs1init @ \snd srcrs2init @
     393  let prf : ∀srcrs,tmp.|destrs| = |\fst (cast_srcrs srcrs tmp)| ≝ ? in
     394  let srcrs1init ≝ cast_srcrs srcrs1 tmp1 in
     395  let srcrs2init ≝ cast_srcrs srcrs2 tmp2 in
     396  \snd srcrs1init @@ \snd srcrs2init @@
    403397  translate_op globals op destrs (\fst srcrs1init) (\fst srcrs2init) ??.
     398  @hide_prf
    404399  [ @prf | <prf @prf ]
    405400  #srcrs #tmp normalize nodelta
    406401  @leb_elim #H normalize nodelta
    407   [ lapply (last_not_empty … srcrs)
    408     cases (last ??)
    409     [ cases srcrs
    410       [ #_ normalize >length_make_list %
    411       | #hd #tl #abs elim(abs I)
    412       ]
    413     | #last #_ normalize nodelta
    414       >length_append >length_make_list
     402  [ cases (last ??) normalize nodelta
     403    [ >length_make_list %
     404    | #_ >length_append >length_make_list
    415405      @minus_to_plus //
    416406    ]
    417   | >length_lhd normalize @leb_elim
    418     [ #G elim (absurd … G H)
    419     | #_ %
    420     ]
     407  | >length_lhd normalize >(not_le_to_leb_false … H) %
    421408  ]
    422409qed.
     
    426413  ∀globals: list ident.
    427414  signedness → list register → list register →
    428     bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     415    bind_new register (list (joint_seq RTL globals)) ≝
    429416  λglobals,src_sign,destrs,srcrs.
    430417  match reduce_strong ?? destrs srcrs with
     
    459446  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
    460447
    461 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     448definition translate_negint : ∀globals.? → ? → ? → bind_new register (list (joint_seq RTL globals)) ≝
    462449  λglobals: list ident.
    463450  λdestrs: list register.
    464451  λsrcrs: list register.
    465452  λprf: |destrs| = |srcrs|. (* assert in caml code *)
    466   translate_notint … destrs srcrs prf @
    467   match nat_to_args (|destrs|) 1 with
    468   [ mk_Sig res prf' ⇒
    469     translate_op ? Add destrs (map … (Reg ?) destrs) res ??
    470   ].
    471 >length_map // qed.
     453  translate_notint … destrs srcrs prf @@
     454  translate_op ? Add destrs (map … (Reg ?) destrs) (nat_to_args (|destrs|) 1) ??.
     455@hide_prf >length_map [ cases (nat_to_args ??) ] // qed.
    472456
    473457definition translate_notbool:
    474458  ∀globals : list ident.
    475459  list register → list register →
    476     bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     460    bind_new register (list (joint_seq RTL globals)) ≝
    477461  λglobals,destrs,srcrs.
    478462  match destrs with
     
    497481
    498482definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
    499   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     483  bind_new register (list (joint_seq RTL globals)) ≝
    500484  λglobals.
    501485  λty, ty'.
     
    507491  match op1
    508492  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    509     bind_new (localsT RTL) (list (joint_seq RTL globals)) with
     493    bind_new register (list (joint_seq RTL globals)) with
    510494  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    511495    translate_cast globals src_sign destrs srcrs
     
    524508  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
    525509  ] (refl …) (refl …).
     510  @hide_prf
    526511  destruct >prf1 >prf2 [3: >length_map ] //
    527512qed.
     
    548533  (Σi.i<S k) →
    549534  (* the accumulator *)
    550   list (joint_seq RTL globals) →
    551     list (joint_seq RTL globals) ≝
     535  bind_new register (list (joint_seq RTL globals)) →
     536    bind_new register (list (joint_seq RTL globals)) ≝
    552537  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    553538    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    570555      let tmp_destrs_view : list register ≝
    571556        ltl ? tmp_destrs_dummy k in
    572       ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
    573       translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
     557      [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?)] @@
     558      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @@
    574559      acc
    575560    ].
    576 [ @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
     561@hide_prf
     562[ <srcrs1_prf
     563  @(transitive_le … i_prf k_prf)
     564| @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
    577565  whd >(plus_n_O (S k)) @le_plus // ]
    578 | <srcrs1_prf
    579   @(transitive_le … i_prf k_prf)
    580 | >length_map //
     566| >length_map %
    581567| >length_map
    582568  >length_ltl
     
    584570  >length_make_list
    585571  normalize in ⊢ (???(?%?));
    586   >plus_minus_commutative
    587     [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption]
    588   cut (S n = 2 + (n - 1))
    589     [2: #EQ >EQ %]
    590   >plus_minus_commutative
    591     [2: @(transitive_le … k_prf) //]
    592   @sym_eq
    593   @plus_to_minus %
     572  cases n in k_prf; [ #ABS cases (absurd ? ABS ?) /2 by le_to_not_lt/ ]
     573  #n' #k_prf >minus_S_S <minus_n_O
     574  >plus_minus_commutative [%] @le_S_S_to_le assumption
    594575] qed.
    595576
    596 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     577definition translate_mul : ∀globals.?→?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝
    597578λglobals : list ident.
    598579λdestrs : list register.
     
    610591(* the step calculating all products with least significant byte going in the
    611592   k-th position of the result *)
    612 let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
    613   list (joint_seq RTL globals) ≝
     593let translate_mul_k : (Σk.k<|destrs|) → bind_new register (list (joint_seq RTL globals)) →
     594  bind_new register (list (joint_seq RTL globals)) ≝
    614595  λk_sig,acc.match k_sig with
    615596  [ mk_Sig k k_prf ⇒
     
    620601(* initializing tmp_destrs to zero
    621602   dummy is intentionally uninitialized *)
    622 translate_fill_with_zero … tmp_destrs @
     603translate_fill_with_zero … tmp_destrs @@
    623604(* the main body, roughly:
    624605   for k in 0 ... n-1 do
    625606     for i in 0 ... k do
    626607       translate_mul_i … k … i *)
    627 foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ 
     608foldr … translate_mul_k [ ] (range_strong (|destrs|)) @@
    628609(* epilogue: saving the result *)
    629610translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
     611@hide_prf
    630612[ >length_map >tmp_destrs_prf //
    631613| >length_append <plus_n_Sm <plus_n_O //
     
    634616
    635617definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    636     bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     618    bind_new register (list (joint_seq RTL globals)) ≝
    637619  λglobals: list ident.
    638620  λdiv_not_mod: bool.
     
    663645  ] (refl …).
    664646[3: elim not_implemented]
    665 destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed.
     647@hide_prf
     648destruct normalize in srcrs1_prf srcrs2_prf; destruct qed.
    666649
    667650(* Paolo: to be moved elsewhere *)
     
    677660    ] (refl …)
    678661  ] (refl …).
     662@hide_prf
    679663destruct normalize in prf;  [destruct|//]
    680664qed.
    681665
    682666definition translate_ne: ∀globals: list ident.?→?→?→?→
    683   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     667  bind_new register (list (joint_seq RTL globals)) ≝
    684668  λglobals: list ident.
    685669  λdestrs: list register.
     
    711695       ]
    712696     ] EQ
    713    ]. normalize in EQ; destruct(EQ) assumption qed.
     697   ].
     698@hide_prf normalize in EQ; destruct(EQ) assumption qed.
    714699
    715700(* if destrs is 0 or 1, it inverses it. To be used after operations that
    716701   ensure this. *)
    717 definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝
     702definition translate_toggle_bool : ∀globals.?→bind_new register (list (joint_seq RTL globals)) ≝
    718703  λglobals: list ident.
    719704  λdestrs: list register.
     
    729714  ∀srcrs2: list psd_argument.
    730715  |srcrs1| = |srcrs2| →
    731   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     716  bind_new register (list (joint_seq RTL globals)) ≝
    732717  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    733718  match destrs with
     
    735720  | cons destr destrs' ⇒
    736721    ν tmpr in
    737     (translate_fill_with_zero … destrs' @
     722    (translate_fill_with_zero … destrs' @@
    738723    (* I perform a subtraction, but the only interest is in the carry bit *)
    739     translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @
     724    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @@
    740725    [ destr ← zero_byte .Addc. zero_byte ])
    741726  ].
     727@hide_prf
    742728>length_make_list % qed.
    743729
     
    759745    ]
    760746  ].
     747@hide_prf
    761748[1,2: %
    762749|*: cases re * #a #b >p1 normalize #EQ >EQ %
     
    769756  ∀srcrs2: list psd_argument.
    770757  |srcrs1| = |srcrs2| →
    771   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     758  bind_new register (list (joint_seq RTL globals)) ≝
    772759  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    773760  νtmp_last_s1 in
     
    781768  shift_srcrs1 @@ shift_srcrs2 @@
    782769  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?.
     770@hide_prf
    783771whd in match new_srcrs1; whd in match new_srcrs2;
    784772cases p1
     
    787775qed.
    788776
    789 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     777definition translate_lt : bool→∀globals.?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝
    790778  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
    791779  if is_unsigned then
     
    812800    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@
    813801    translate_toggle_bool globals destrs
    814   ].
    815 // qed.
     802  ]. @sym_eq assumption qed.
    816803
    817804definition translate_op2 :
     
    822809  |srcrs1| = size_of_sig_type ty1 →
    823810  |srcrs2| = size_of_sig_type ty2 →
    824   bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     811  bind_new register (list (joint_seq RTL globals)) ≝
    825812  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
    826813  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
     
    829816  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
    830817    translate_op globals Add destrs srcrs1 srcrs2 ??
    831   | Oaddp sz ⇒ λprf1,prf2,prf3.
     818  | Oaddpi sz ⇒ λprf1,prf2,prf3.
    832819    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
     820  | Oaddip sz ⇒ λprf1,prf2,prf3.
     821    translate_op_asym_signed globals Add destrs srcrs2 srcrs1
    833822  | Osub sz sg ⇒ λprf1,prf2,prf2.
    834823    translate_op globals Sub destrs srcrs1 srcrs2 ??
     
    857846    translate_cmp true globals c destrs srcrs1 srcrs2 ?
    858847  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
    859   ]. try @not_implemented //
     848  ]. try @not_implemented @hide_prf //
    860849  qed.
    861850
    862851definition translate_cond: ∀globals: list ident. list register → label →
    863   bind_seq_block RTL globals (joint_step RTL globals)
     852  bind_step_block RTL globals
    864853  λglobals: list ident.
    865854  λsrcrs: list register.
    866855  λlbl_true: label.
    867   match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with
    868   [ nil ⇒ bret … 〈[ ], NOOP ??〉
     856  match srcrs return λ_.bind_step_block RTL ? with
     857  [ nil ⇒ bret … [ ]
    869858  | cons srcr srcrs' ⇒
    870859    ν tmpr in
    871860    let f : register → joint_seq RTL globals ≝
    872861      λr. tmpr ← tmpr .Or. r in
    873     bret … MOVE RTL globals 〈tmpr,srcr〉 ::
    874     map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
     862    bret … ((MOVE RTL globals 〈tmpr,srcr〉 ::
     863    map ?? f srcrs' : list (joint_step ??)) @ [COND … tmpr lbl_true])
    875864  ].
    876865
    877866(* Paolo: to be controlled (original seemed overly complex) *)
    878 definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
     867definition translate_load : ∀globals.?→?→?→bind_new register ? ≝
    879868  λglobals: list ident.
    880869  λaddr : list psd_argument.
     
    883872  ν tmp_addr_l in
    884873  ν tmp_addr_h in
    885   let f ≝ λdestr : register.λacc : list (joint_seq RTL globals).
    886     LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     874  (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
     875  let f ≝ λdestr : register.λacc : bind_new register (list (joint_seq RTL globals)).
     876    [LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h)] @@
    887877    translate_op ? Add
    888878      [tmp_addr_l ; tmp_addr_h]
    889879      [tmp_addr_l ; tmp_addr_h]
    890       [zero_byte ; (int_size : Byte)] ? ? @ acc in
    891   translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    892   foldr … f [ ] destrs.
    893 [1: <addr_prf
    894 ] // qed.
     880      [zero_byte ; (int_size : Byte)] ? ? @@ acc in
     881  foldr … f [ ] destrs).
     882@hide_prf
     883[ <addr_prf ] % qed.
    895884 
    896 definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
     885definition translate_store : ∀globals.?→?→?→bind_new register ? ≝
    897886  λglobals: list ident.
    898887  λaddr : list psd_argument.
     
    901890  ν tmp_addr_l in
    902891  ν tmp_addr_h in
    903   let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals).
    904     STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
     892  (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
     893  let f ≝ λsrcr : psd_argument.λacc : bind_new register (list (joint_seq RTL globals)).
     894    [STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr] @@
    905895    translate_op … Add
    906896      [tmp_addr_l ; tmp_addr_h]
    907897      [tmp_addr_l ; tmp_addr_h]
    908       [zero_byte ; (int_size : Byte)] ? ? @ acc in
    909   translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    910   foldr … f [ ] srcrs.
    911 [1: <addr_prf] // qed.
     898      [zero_byte ; (int_size : Byte)] ? ? @@ acc in
     899  foldr … f [ ] srcrs).
     900@hide_prf [ <addr_prf ] % qed.
    912901
    913902lemma lenv_typed_reg_typed_ok1 :
     
    951940qed.
    952941
     942definition ensure_bind_step_block : ∀p : params.∀g.
     943  bind_new register (list (joint_step p g)) → bind_step_block p g ≝
     944  λp,g,b.! l ← b; bret ? (step_block p g) l.
     945
     946definition ensure_bind_step_block_from_seq : ∀p : params.∀g.
     947  bind_new register (list (joint_seq p g)) → bind_step_block p g ≝
     948  λp,g,b.! l ← b; bret ? (step_block p g) l.
     949
     950coercion bind_step_block_from_bind_list nocomposites :
     951  ∀p : params.∀g.
     952  ∀b : bind_new register (list (joint_step p g)).bind_step_block p g ≝
     953  ensure_bind_step_block on _b : bind_new register (list (joint_step ??)) to
     954  bind_step_block ??.
     955
     956coercion bind_step_block_from_bind_seq_list nocomposites :
     957  ∀p : params.∀g.
     958  ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝
     959  ensure_bind_step_block_from_seq on _b : bind_new register (list (joint_seq ??)) to
     960  bind_step_block ??.
     961
    953962definition translate_statement : ∀globals, locals.∀env.
    954963  local_env_typed locals env →
    955964  ∀stmt : statement.statement_typed locals stmt →
    956965  𝚺b :
    957   bind_seq_block RTL globals (joint_step RTL globals) +
    958   bind_seq_block RTL globals (joint_fin_step RTL).
    959   if is_inl … b then label else unit
     966  bind_step_block RTL globals +
     967  bind_fin_block RTL globals.
     968  match b with [ inl _ ⇒ label | _ ⇒ unit]
    960969  λglobals,locals,lenv,lenv_typed,stmt.
    961   match stmt return λstmt.statement_typed locals stmt → 𝚺b:bind_seq_block ???+bind_seq_block ???.if is_inl … b then label else unit with
     970  match stmt return λstmt.statement_typed locals stmt → 𝚺b: bind_step_block RTL globals ⊎ bind_fin_block RTL globals.match b with [ inl _ ⇒ label | _ ⇒ unit ] with
    962971  [ St_skip lbl' ⇒ λstmt_typed.
    963     ❬NOOP ??, lbl'❭
     972    ❬inl … (bret … [ ]), lbl'❭
    964973  | St_cost cost_lbl lbl' ⇒ λstmt_typed.
    965     ❬COST_LABEL … cost_lbl, lbl'❭
     974    ❬inl … (bret … [COST_LABEL … cost_lbl]), lbl'❭
    966975  | St_const ty destr cst lbl' ⇒ λstmt_typed.
    967     ❬translate_cst ty globals cst (find_local_env destr lenv ?) ?, lbl'❭
     976    ❬inl … (translate_cst ty globals cst (find_local_env destr lenv ?) ?), lbl'❭
    968977  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λstmt_typed.
    969     ❬translate_op1 globals ty' ty op1
     978    ❬inl … (translate_op1 globals ty' ty op1
    970979      (find_local_env destr lenv ?)
    971       (find_local_env srcr lenv ?) ??, lbl'❭
     980      (find_local_env srcr lenv ?) ??), lbl'❭
    972981  | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ λstmt_typed.
    973     ❬translate_op2 globals … op2
     982    ❬inl … (translate_op2 globals … op2
    974983      (find_local_env destr lenv ?)
    975984      (find_local_env_arg srcr1 lenv ?)
    976       (find_local_env_arg srcr2 lenv ?) ???, lbl'❭
     985      (find_local_env_arg srcr2 lenv ?) ???), lbl'❭
    977986    (* XXX: should we be ignoring this? *)
    978987  | St_load ignore addr destr lbl' ⇒ λstmt_typed.
    979     ❬translate_load globals
    980       (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?), lbl'❭
     988    ❬inl … (translate_load globals
     989      (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?)), lbl'❭
    981990    (* XXX: should we be ignoring this? *)
    982991  | St_store ignore addr srcr lbl' ⇒ λstmt_typed.
    983     ❬translate_store globals (find_local_env_arg addr lenv ?) ?
    984       (find_local_env_arg srcr lenv ?), lbl'❭
     992    ❬inl … (translate_store globals (find_local_env_arg addr lenv ?) ?
     993      (find_local_env_arg srcr lenv ?)), lbl'❭
    985994  | St_call_id f args retr lbl' ⇒ λstmt_typed.
    986     ❬(CALL RTL ? (inl … f) (rtl_args args lenv ?)
     995    ❬inl ?? (bret ?? [CALL RTL ? (inl … f) (rtl_args args lenv ?)
    987996      (match retr with
    988997      [ Some retr ⇒ find_local_env retr lenv ?
    989998      | None ⇒ [ ]
    990       ]) : bind_seq_block ???), lbl'❭
     999      ])]), lbl'❭
    9911000  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
    9921001    let fs ≝ find_and_addr_arg f lenv ?? in
    993     ❬(CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
     1002    ❬inl … (bret … [CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
    9941003      (match retr with
    9951004       [ Some retr ⇒
    9961005         find_local_env retr lenv ?
    9971006       | None ⇒ [ ]
    998        ]) : joint_step ??), lbl'❭
     1007       ])]), lbl'❭
    9991008  | St_cond r lbl_true lbl_false ⇒ λstmt_typed.
    1000     ❬translate_cond globals (find_local_env r lenv ?) lbl_true, lbl_false❭
    1001   | St_return ⇒ λ_. ❬inr … (RETURN ?),it❭
    1002   ].
    1003   [ >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed)
     1009    ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭
     1010  | St_return ⇒ λ_. ❬inr … (bret … 〈[ ], RETURN ?〉),it❭
     1011  ].
     1012  @hide_prf
     1013  [ cases daemon (* needs more hypotheses *)
     1014  | @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed)
     1015  | >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed)
    10041016    @cst_size_ok
    1005   | @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed)
    1006   | cases daemon (* needs more hypotheses *)
    10071017  |4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed
    1008     [1,2: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
    1009     | @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed)
    1010     | @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed)
     1018    [3,4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
     1019    |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed)
     1020    |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed)
    10111021    ]
    10121022  |8,9,10,11,12,13:
    10131023    cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf
    1014     [1,2: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption
    1015     | @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
    1016     | @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf)
    1017     | @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf)
    1018     | @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
     1024    [5,6: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption
     1025    |4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
     1026    |3: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf)
     1027    |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf)
     1028    |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
    10191029    ]
    10201030  |*: cases daemon (* TODO  *)
     
    10221032qed.
    10231033
    1024 (* XXX: we use a "hack" here to circumvent the proof obligations required to
    1025    create res, an empty internal_function record.  we insert into our graph
    1026    the start and end nodes to ensure that they are in, and place dummy
    1027    skip instructions at these nodes. *)
    10281034definition translate_internal :
    10291035  ∀globals.internal_function → (* insert here more properties *)
     
    10351041  let stack_size' ≝ f_stacksize def in
    10361042  let entry' ≝ f_entry def in
    1037   let exit' ≝ f_exit def in
    1038   let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ] [ ]
    1039      [ ] stack_size' (pi1 … entry') (pi1 … exit') in
     1043  let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ]
     1044     [ ] stack_size' (pi1 … entry') in
    10401045  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
    10411046    (f_locals def) (f_params def) (f_result def) init in
     
    10441049  let f_trans ≝ λlbl,stmt,def.
    10451050    let pr ≝ translate_statement … vars lenv ? stmt ? in
    1046     b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
     1051    match dpi1 … pr return λx.match x with [ inl _ ⇒ label | _ ⇒ unit ] → ? with
     1052    [ inl instrs ⇒ λlbl'.b_adds_graph … instrs lbl lbl' def
     1053    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
     1054    ] (dpi2 … pr) in
    10471055  foldi … f_trans (f_graph def) init'. (* TODO *) cases daemon
    10481056qed.
Note: See TracChangeset for help on using the changeset viewer.