Changeset 2155 for src/RTLabs


Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (7 years ago)
Author:
tranquil
Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2103 r2155  
    55include "common/Graphs.ma".
    66include "joint/TranslateUtils_paolo.ma".
    7 include "utilities/lists.ma".
     7include "utilities/bindLists.ma".
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
    10 
    1110
    1211definition size_of_sig_type ≝
     
    5049  λr,lenv,prf. map … Reg (find_local_env r lenv prf).
    5150
    52 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
    53   match n with
    54   [ O ⇒ 〈[],runiverse〉
     51definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝
     52λtag,univ.let pr ≝ fresh … univ in 〈\snd pr, \fst pr〉.
     53
     54let rec register_freshes (n: nat) on n :
     55  state_monad (universe RegisterTag) (Σl.|l| = n) ≝
     56  match n return λx.state_monad ? (Σl.|l| = x) with
     57  [ O ⇒ return «[ ],?»
    5558  | S n' ⇒
    56      let 〈r,runiverse〉 ≝ fresh … runiverse in
    57      let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
    58       〈r::res,runiverse〉 ].
    59 
    60 definition initialize_local_env_internal ≝
    61   λlenv_runiverse : local_env × ?.
    62   λr_sig.
    63   let 〈lenv,runiverse〉 ≝ lenv_runiverse in
     59    ! r ← m_fresh ?;
     60    ! res ← register_freshes n';
     61    return «r::res,?»
     62  ].[2: cases res -res #res #EQ <EQ] % qed.
     63
     64definition initialize_local_env_internal :
     65  (universe RegisterTag × local_env) → (register×typ) → (universe RegisterTag × local_env) ≝
     66  λlenv_runiverse,r_sig.
     67  let 〈runiverse,lenv〉 ≝ lenv_runiverse in
    6468  let 〈r, sig〉 ≝ r_sig in
    6569  let size ≝ size_of_sig_type sig in
    66   let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
    67     〈add … lenv r rs,runiverse〉.
    68 
    69 definition initialize_local_env ≝
    70   λruniverse.
    71   λregisters.
    72   λresult.
    73   let registers ≝
    74     match result with
    75     [ None ⇒ registers
    76     | Some rt ⇒ rt :: registers
    77     ]
    78   in
    79     foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.
    80 
    81 definition map_list_local_env_internal ≝
    82   λlenv,res,r_sig. res @ (find_local_env (pi1 … r_sig) lenv (pi2 … r_sig)).
    83    
    84 definition map_list_local_env ≝
    85   λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
     70  let 〈runiverse,rs〉 ≝ register_freshes size runiverse in
     71    〈runiverse,add … lenv r rs〉.
     72
     73definition initialize_local_env :
     74  list (register×typ) →
     75  state_monad (universe RegisterTag) local_env ≝
     76  λregisters,runiverse.
     77  foldl … initialize_local_env_internal 〈runiverse,empty_map …〉 registers.
     78
     79include alias "common/Identifiers.ma".
     80let rec map_list_local_env
     81  lenv (regs : list (register×typ)) on regs :
     82  All ? (λpr.bool_to_Prop (\fst pr ∈ lenv)) regs → list register ≝
     83  match regs return λx.All ?? x → ? with
     84  [ nil ⇒ λ_.[ ]
     85  | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ?
     86  ].cases prf #A #B assumption qed.
    8687
    8788definition make_addr ≝
    8889  λA.
    8990  λlst: list A.
    90   λprf: 2 = length A lst.
    91   match lst return λx. 2 = |x| → A × A with
    92   [ nil ⇒ λlst_nil_prf. ⊥
    93   | cons hd tl ⇒ λprf.
    94     match tl return λx. 1 = |x| → A × A with
    95     [ nil ⇒ λtl_nil_prf. ⊥
    96     | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    97     ] ?
    98   ] prf.
    99   [1: normalize in lst_nil_prf;
    100       destruct(lst_nil_prf)
    101   |2: normalize in prf;
    102       @injective_S
    103       assumption
    104   |3: normalize in tl_nil_prf;
    105       destruct(tl_nil_prf)
    106   ]
    107 qed.
     91  λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf //
     92  qed.
    10893
    10994definition find_and_addr ≝
    11095  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
    11196
    112 definition rtl_args ≝
    113   λlenv,regs_list. flatten … (map … (λr.find_local_env_arg (pi1 … r) lenv (pi2 … r)) regs_list).
     97include alias "common/Identifiers.ma".
     98let rec rtl_args (args : list register) (env : local_env) on args :
     99  All ? (λr.bool_to_Prop (r∈env)) args → list rtl_argument ≝
     100  match args return λx.All ?? x → ? with
     101  [ nil ⇒ λ_.[ ]
     102  | cons hd tl ⇒ λprf.find_local_env_arg hd env ? @ rtl_args tl env ?
     103  ].
     104  cases prf #H #G assumption
     105  qed.
     106
     107include alias "basics/lists/list.ma".
     108let rec vrsplit A (m,n : nat)
     109  on m : Vector A (m*n) → Σs : list (Vector A n).|s| = m ≝
     110  match m return λx.Vector A (x*n) → Sig (list ?) ? with
     111  [ O ⇒ λv.[ ]
     112  | S k ⇒ λv.let spl ≝ vsplit ? n … v in \fst spl :: vrsplit ? k n (\snd spl)
     113  ].
     114  [ %
     115  | cases (vrsplit ????) #lst #EQ normalize >EQ %
     116  ] qed.
    114117
    115118definition split_into_bytes:
    116119  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝
    117 λsize.
    118  match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with
    119   [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
    120 [ %[@[int]] //
    121 | %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) normalize //
    122 | %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
    123       let 〈h2,l〉 ≝ vsplit ? 8 … l in
    124       let 〈h3,l〉 ≝ vsplit ? 8 … l in
    125        [l;h3;h2;h1])]
    126   cases (vsplit ????) #h1 #l normalize
    127   cases (vsplit ????) #h2 #l normalize
    128   cases (vsplit ????) // ]
    129 qed.
    130 
     120λsize.vrsplit ? (size_intsize size) 8.
     121
     122let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝
     123match l return λx.All A P x → ? with
     124[ nil ⇒ λ_.[ ]
     125| cons hd tl ⇒ λprf.«hd, ?» :: list_inject_All_aux A P tl ?
     126]. cases prf #H1 #H2 [@H1 | @H2]
     127qed.
     128
     129include alias "basics/lists/list.ma".
    131130definition translate_op:
    132131  ∀globals. Op2 →
     
    135134  ∀srcrs2 : list rtl_argument.
    136135  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    137   list (rtl_step globals)
    138    
     136  list (joint_seq rtl_params globals)
     137 
    139138  λglobals: list ident.
    140139  λop.
     
    143142  λsrcrs2.
    144143  λprf1,prf2.
    145   let f_add ≝ OP2 rtl_params globals in
    146   let res : list (rtl_step globals) ≝
    147     map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
    148144  (* first, clear carry if op relies on it *)
    149145  match op with
     
    151147  | Sub ⇒ [CLEAR_CARRY ??]
    152148  | _ ⇒ [ ]
    153   ] @
    154   match op with
    155   (* if adding, we use a first Add op, that clear the carry, and then Addc's *)
    156   [ Add ⇒
    157     match destrs return λx.|destrs| = |x| → list (rtl_step globals) with
    158     [ nil ⇒ λeq_destrs.[ ]
    159     | cons destr destrs' ⇒ λeq_destrs.
    160       match srcrs1 return λy.|srcrs1| = |y| → list (rtl_step globals) with
    161       [ nil ⇒ λeq_srcrs1.⊥
    162       | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
    163         match srcrs2 return λz.|srcrs2| = |z| → list (rtl_step globals) with
    164         [ nil ⇒ λeq_srcrs2.⊥
    165         | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
    166           f_add Add destr srcr1 srcr2 ::
    167           map3 ???? (f_add Addc) destrs' srcrs1' srcrs2' ??
    168         ] (refl …)
    169       ] (refl …)
    170     ] (refl …)
    171   | _ ⇒ res
    172   ].
    173   [5,6: assumption
    174   |1: >prf1 in eq_destrs; >eq_srcrs1 normalize //
    175   |2: >prf2 in eq_srcrs1; >eq_srcrs2 normalize //
    176   |3: >prf2 in eq_srcrs1; >eq_srcrs2 normalize #H destruct(H)
    177   |4: >prf1 in eq_destrs; >eq_srcrs1 normalize #H destruct(H)
    178 qed.
     149  ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2.
    179150
    180151let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.|l| = size ≝
     
    188159]. normalize // qed.
    189160
    190 definition size_of_cst ≝ λcst.match cst with
    191   [ Ointconst size _ ⇒ size_intsize size
    192   | Ofloatconst float ⇒ ? (* not implemented *)
     161definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
     162  [ Ointconst size _ _ ⇒ size_intsize size
     163  | Ofloatconst _ _ ⇒ ? (* not implemented *)
    193164  | _ ⇒ 2
    194165  ].
    195166  cases not_implemented qed.
    196167
    197 definition cst_well_defd : list ident → constant → Prop ≝ λglobals,cst.
     168definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
    198169  match cst with
    199   [ Oaddrsymbol id offset ⇒ member id (eq_identifier ?) globals
     170  [ Oaddrsymbol r id offset ⇒ member id (eq_identifier ?) globals
    200171  | _ ⇒ True
    201172  ].
    202173
    203174definition translate_cst :
     175  ∀ty.
    204176  ∀globals: list ident.
    205   ∀cst_sig: Σcst : constant.cst_well_defd globals cst.
     177  ∀cst_sig: Σcst : constant ty.cst_well_defd ty globals cst.
    206178  ∀destrs: list register.
    207   |destrs| = size_of_cst cst_sig → list (rtl_step globals)
     179  |destrs| = size_of_cst ? cst_sig →
     180  list (joint_seq rtl_params globals)
    208181 ≝
    209   λglobals,cst_sig,destrs,prf.
    210   match cst_sig return λy.cst_sig = y → list (rtl_step globals) with
    211   [ mk_Sig cst cst_good ⇒ λeqcst_sig.
    212     match cst return λx.cst = x → list (rtl_step globals)
    213     with
    214     [ Ointconst size const ⇒ λeqcst.
    215       match split_into_bytes size const with
    216       [ mk_Sig bytes bytes_length_proof ⇒
    217         map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs bytes ?
    218       ]
    219     | Ofloatconst float ⇒ λ_.⊥
    220     | Oaddrsymbol id offset ⇒ λeqcst.
    221       let 〈r1, r2〉 ≝ make_addr … destrs ? in
    222       [ADDRESS rtl_params globals id ? r1 r2]
    223     | Oaddrstack offset ⇒ λeqcst.
    224       let 〈r1, r2〉 ≝ make_addr … destrs ? in
    225       [(rtl_st_ext_stack_address r1 r2 : rtl_step globals)]
    226     ] (refl …)
    227   ] (refl …).
     182  λty,globals,cst_sig,destrs.
     183  match pi1 … cst_sig in constant return λty'.λx : constant ty'.
     184      cst_well_defd ty' ? x → |destrs| = size_of_cst ty' x → ?
     185  with
     186  [ Ointconst size sign const ⇒ λcst_prf,prf.
     187      map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs
     188        (split_into_bytes size const) ?
     189  | Ofloatconst _ _ ⇒ ?
     190  | Oaddrsymbol r id offset ⇒ λcst_prf,prf.
     191    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     192    [ADDRESS rtl_params globals id ? r1 r2]
     193  | Oaddrstack offset ⇒ λcst_prf,prf.
     194    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     195    [(rtl_stack_address r1 r2 : joint_seq rtl_params globals)]
     196  ] (pi2 … cst_sig).
    228197  [2: cases not_implemented
    229   |3: >eqcst in cst_good; //]
    230   >eqcst_sig in prf;
    231   >eqcst whd in ⊢ (???% → ?); #prf
    232   [1: >bytes_length_proof
    233       >prf //]
    234   //
    235   qed.
    236 
     198  |1: cases (split_into_bytes ??) #lst
     199    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
     200  |3: @cst_prf
     201  |*: >prf %
     202  ]
     203qed.
    237204 
    238205definition translate_move :
     
    240207  ∀destrs: list register.
    241208  ∀srcrs: list rtl_argument.
    242   |destrs| = |srcrs| → list (rtl_step globals) ≝
     209  |destrs| = |srcrs| → list (joint_seq rtl_params globals) ≝
    243210  λglobals,destrs,srcrs,length_eq.
    244211  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
    245212
    246 let rec make
    247   (A: Type[0]) (elt: A) (n: nat) on n ≝
    248   match n with
    249   [ O ⇒ [ ]
    250   | S n' ⇒ elt :: make A elt n'
    251   ].
    252  
    253 lemma make_length:
     213lemma make_list_length:
    254214  ∀A: Type[0].
    255215  ∀elt: A.
    256216  ∀n: nat.
    257     n = length ? (make A elt n).
     217    n = length ? (make_list A elt n).
    258218  #A #ELT #N
    259   elim N
    260   [ normalize %
    261   | #N #IH
    262     normalize <IH %
    263   ]
    264 qed.
    265 
    266 definition sign_mask : ∀globals.register → register → list (rtl_step globals) ≝
     219  elim N normalize // qed.
     220
     221definition sign_mask : ∀globals.register → register →
     222  list (joint_seq rtl_params globals) ≝
    267223    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
    268224       byte in destr if srcr is: neg   |  pos
     
    277233   destr ← .Inc. destr ;
    278234   destr ← .Cmpl. destr ].
    279    
     235
    280236definition translate_cast_signed :
    281237  ∀globals : list ident.
    282   list register → register → bind_list register (rtl_step globals) ≝
     238  list register → register →
     239  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    283240  λglobals,destrs,srcr.
    284241  ν tmp in
    285242  (sign_mask ? tmp srcr @
    286   translate_move ? destrs (make ? (Reg tmp) (|destrs|)) (make_length …)).
     243  translate_move ? destrs (make_list ? (Reg tmp) (|destrs|)) (make_list_length …)).
    287244 
    288 definition translate_cast_unsigned :
     245definition translate_fill_with_zero :
    289246  ∀globals : list ident.
    290   list register → list (rtl_step globals) ≝
     247  list register → list (joint_seq rtl_params globals) ≝
    291248  λglobals,destrs.
    292249  match nat_to_args (|destrs|) 0 with
     
    294251  // qed.
    295252
    296 theorem length_map : ∀A,B.∀f:A→B.∀l : list A.|map … f l| = |l|.
    297 #A#B#f #l elim l normalize // qed.
     253let rec last A (l : list A) on l : option A ≝
     254match l with
     255[ nil ⇒ None ?
     256| cons hd tl ⇒
     257  match tl with
     258  [ nil ⇒ Some ? hd
     259  | _ ⇒ last A tl
     260  ]
     261].
     262
     263lemma last_nth : ∀A,l.last A l = nth_opt A (pred (|l|)) l.
     264#A #l elim l [%]
     265#hd * [#_ %]
     266#hd2 #tl #IH
     267change with (last A (hd2 :: tl) = ?)
     268>IH //
     269qed.
    298270
    299271(* using size of lists as size of ints *)
     
    301273  ∀globals: list ident.
    302274  signedness → list register → list register →
    303     bind_list register (rtl_step globals) ≝
     275    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    304276  λglobals,src_sign,destrs,srcrs.
    305   match srcrs
    306   return λy. y = srcrs → bind_list register (rtl_step globals)
    307   with
    308   [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *)
    309   | _ ⇒ λeq_srcrs.
    310     match reduce_strong ? ? destrs srcrs with
    311     [ mk_Sig crl len_proof ⇒
    312       (* move prefix of srcrs in destrs *)
    313       translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @@
    314       match \snd (\snd crl) return λ_.bind_list ?? with
    315       [ nil ⇒
    316         match src_sign return λ_.bind_list register (rtl_step globals) with
    317         [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl))
    318         | Signed ⇒
    319           translate_cast_signed ? (\snd (\fst crl)) (last_safe ? srcrs ?)
     277  match reduce_strong ?? destrs srcrs with
     278  [ mk_Sig t prf ⇒
     279    let src_common ≝ \fst (\fst t) in
     280    let src_rest   ≝ \snd (\fst t) in
     281    let dst_common ≝ \fst (\snd t) in
     282    let dst_rest   ≝ \snd (\snd t) in
     283    (* first, move the common part *)
     284    translate_move ? src_common (map … Reg dst_common) ? @@
     285    match src_rest return λ_.bind_new ?? with
     286    [ nil ⇒ (* upcast *)
     287      match src_sign return λ_.bind_new ?? with
     288      [ Unsigned ⇒ translate_fill_with_zero ? dst_rest
     289      | Signed ⇒
     290        match last … srcrs (* = src_common *) with
     291        [ Some src_last ⇒ translate_cast_signed ? dst_rest src_last
     292        | None ⇒ (* srcrs is empty *) translate_fill_with_zero ? dst_rest
    320293        ]
    321       | _ ⇒ [ ] (* nothing to do if |srcrs| > |destrs| *)
    322294      ]
     295    | _ ⇒ (* downcast, nothing else to do *) [ ]
    323296    ]
    324   ] (refl …).
    325   [ >len_proof >length_map @refl
    326   | <eq_srcrs normalize //
    327   ] qed.
     297  ].
     298  >length_map @prf qed.
    328299 
    329300definition translate_notint :
     
    331302  ∀destrs : list register.
    332303  ∀srcrs_arg : list register.
    333   |destrs| = |srcrs_arg| → list (rtl_step globals) ≝
     304  |destrs| = |srcrs_arg| → list (joint_seq rtl_params globals) ≝
    334305  λglobals, destrs, srcrs, prf.
    335306  map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
    336307
    337 definition translate_negint : ∀globals.? → ? → ? → bind_list register (rtl_step globals) ≝
     308definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    338309  λglobals: list ident.
    339310  λdestrs: list register.
     
    350321  ∀globals : list ident.
    351322  list register → list register →
    352     bind_list register (rtl_step globals) ≝
     323    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    353324  λglobals,destrs,srcrs.
    354325  match destrs with
    355326  [ nil ⇒ [ ]
    356327  | cons destr destrs' ⇒
    357     translate_cast_unsigned ? destrs' @@ (* fill destrs' with 0 *)
    358     match srcrs with
     328    translate_fill_with_zero ? destrs' @@
     329    match srcrs return λ_.bind_new ?? with
    359330    [ nil ⇒ [destr ← 0]
    360331    | cons srcr srcrs' ⇒
    361       let f : register → rtl_step globals ≝
    362         λr. destr ← destr .Or. r in
    363       (destr ← srcr) ::: ? ]].
    364       map ?? f srcrs' @@
     332      (destr ← srcr) :::
     333      map register (joint_seq rtl_params globals) (λr. destr ← destr .Or. r) srcrs' @@
    365334      (* now destr is non-null iff srcrs was non-null *)
    366       CLEAR_CARRY ? ? ::
     335      CLEAR_CARRY ?? :::
    367336      (* many uses of 0, better not use immediates *)
    368337      ν tmp in
     
    375344
    376345definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
    377   bind_list register unit (rtl_step globals) ≝
     346  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    378347  λglobals.
    379348  λty, ty'.
     
    385354  match op1
    386355  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    387     bind_list register unit (rtl_step globals) with
     356    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) with
    388357  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    389358    translate_cast globals src_sign destrs srcrs
     
    444413  (Σi.i<S k) →
    445414  (* the accumulator *)
    446   list (rtl_step globals) →
    447     list (rtl_step globals) ≝
     415  list (joint_seq rtl_params globals) →
     416    list (joint_seq rtl_params globals) ≝
    448417  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    449418    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    463432         by constant propagation. *)
    464433      let args : list rtl_argument ≝
    465         [Reg a;Reg b] @ make ? (Imm (zero …)) (n - 1 - k) in
     434        [Reg a;Reg b] @ make_list ? (Imm (zero …)) (n - 1 - k) in
    466435      let tmp_destrs_view : list register ≝
    467436        ltl ? tmp_destrs_dummy k in
     
    478447  >length_ltl
    479448  >tmp_destrs_dummy_prf >length_append
    480   <make_length
     449  <make_list_length
    481450  normalize in ⊢ (???(?%?));
    482451  >plus_minus_commutative
     
    492461] qed.
    493462
    494 definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
     463definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    495464λglobals : list ident.
    496465λdestrs : list register.
     
    504473(* temporary registers for the result are created, so to avoid overwriting
    505474   sources *)
    506 νν tmp_destrs × |destrs| with tmp_destrs_prf in
     475νν |destrs| as tmp_destrs with tmp_destrs_prf in
    507476νdummy in
    508477(* the step calculating all products with least significant byte going in the
    509478   k-th position of the result *)
    510 let translate_mul_k : (Σk.k<|destrs|) → list (rtl_step globals) →
    511   list (rtl_step globals) ≝
     479let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq rtl_params globals) →
     480  list (joint_seq rtl_params globals) ≝
    512481  λk_sig,acc.match k_sig with
    513482  [ mk_Sig k k_prf ⇒
     
    518487(* initializing tmp_destrs to zero
    519488   dummy is intentionally uninitialized *)
    520 translate_cast_unsigned … tmp_destrs @
     489translate_fill_with_zero … tmp_destrs @
    521490(* the main body, roughly:
    522491   for k in 0 ... n-1 do
     
    532501
    533502definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    534     bind_list register unit (rtl_step globals) ≝
     503    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    535504  λglobals: list ident.
    536505  λdiv_not_mod: bool.
     
    540509  λsrcrs1_prf : |destrs| = |srcrs1|.
    541510  λsrcrs2_prf : |srcrs1| = |srcrs2|.
    542   let return_type ≝ bind_list register unit (rtl_step globals) in
    543   match destrs return λx.x = destrs → return_type with
     511  match destrs return λx.x = destrs → bind_new ?? with
    544512  [ nil ⇒ λ_.[ ]
    545513  | cons destr destrs' ⇒ λeq_destrs.
    546514    match destrs' with
    547515    [ nil ⇒
    548       match srcrs1 return λx.x = srcrs1 → return_type  with
     516      match srcrs1 return λx.x = srcrs1 → bind_new ??  with
    549517      [ nil ⇒ λeq_srcrs1.⊥
    550518      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
    551         match srcrs2 return λx.x = srcrs2 → return_type  with
     519        match srcrs2 return λx.x = srcrs2 → bind_new ??  with
    552520        [ nil ⇒ λeq_srcrs2.⊥
    553521        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
     
    579547qed.
    580548
    581 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
     549definition translate_ne: ∀globals: list ident.?→?→?→?→
     550  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
    582551  λglobals: list ident.
    583552  λdestrs: list register.
    584553  λsrcrs1: list rtl_argument.
    585554  λsrcrs2: list rtl_argument.
    586   λsrcrs1_prf : |destrs| = |srcrs1|.
    587   λsrcrs2_prf : |srcrs1| = |srcrs2|.
    588   let return_type ≝ bind_list register unit (rtl_step globals) in
    589   match destrs return λx.x = destrs → return_type with
     555  match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with
    590556  [ nil ⇒ λ_.[ ]
    591   | cons destr destrs' ⇒ λeq_destrs.
    592     match srcrs1 return λy.y = srcrs1 → return_type with
    593     [ nil ⇒ λeq_srcrs1.⊥
    594     | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
    595       match srcrs2 return λz.z = srcrs2 → return_type with
    596       [ nil ⇒ λeq_srcrs2.⊥
    597       | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
     557  | cons destr destrs' ⇒ λEQ.
     558    translate_fill_with_zero … destrs' @@
     559    match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with
     560    [ nil ⇒ λ_.[destr ← 0]
     561    | cons srcr1 srcrs1' ⇒
     562      match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with
     563      [ nil ⇒ λEQ.⊥
     564      | cons srcr2 srcrs2' ⇒ λEQ.
    598565        νtmpr in
    599         let f : rtl_argument → rtl_argument → list (rtl_step globals) → list (rtl_step globals) ≝
     566        let f : rtl_argument → rtl_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
    600567          λs1,s2,acc.
    601568          tmpr  ← s1 .Xor. s2 ::
    602569          destr ← destr .Or. tmpr ::
    603570          acc in
    604         let epilogue : list (rtl_step globals) ≝
    605           [ CLEAR_CARRY ;
     571        let epilogue : list (joint_seq rtl_params globals) ≝
     572          [ CLEAR_CARRY ?? ;
    606573            tmpr ← 0 .Sub. destr ;
    607574            (* now carry bit is 1 iff destrs != 0 *)
    608575            destr ← 0 .Addc. 0 ] in
    609          translate_cast_unsigned … destrs' @
    610576         destr ← srcr1 .Xor. srcr2 ::
    611577         foldr2 ??? f epilogue srcrs1' srcrs2' ?
    612        ] (refl …)
    613      ] (refl …)
    614    ] (refl …).
    615    destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct // qed.
     578       ]
     579     ] EQ
     580   ]. normalize in EQ; destruct(EQ) assumption qed.
    616581
    617582(* if destrs is 0 or 1, it inverses it. To be used after operations that
    618583   ensure this. *)
    619 definition translate_toggle_bool : ∀globals.?→list (rtl_step globals) ≝
     584definition translate_toggle_bool : ∀globals.?→list (joint_seq rtl_params globals) ≝
    620585  λglobals: list ident.
    621586  λdestrs: list register.
     
    630595  ∀srcrs1: list rtl_argument.
    631596  ∀srcrs2: list rtl_argument.
    632   |destrs| = |srcrs1| →
    633597  |srcrs1| = |srcrs2| →
    634   list (rtl_step globals) ≝
    635   λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
     598  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     599  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    636600  match destrs with
    637601  [ nil ⇒ [ ]
    638602  | cons destr destrs' ⇒
    639     translate_cast_unsigned … destrs' @
     603    ν tmpr in
     604    (translate_fill_with_zero … destrs' @
    640605    (* I perform a subtraction, but the only interest is in the carry bit *)
    641     translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @
    642     [ destr ← 0 .Addc. 0 ]
    643   ].
    644 [ <make_length ] assumption qed.
     606    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @
     607    [ destr ← 0 .Addc. 0 ])
     608  ].
     609<make_list_length % qed.
    645610
    646611(* shifts signed integers by adding 128 to the most significant byte
     
    649614  (tmp : register)
    650615  (srcrs : list rtl_argument) on srcrs :
    651   (list rtl_argument) × (list (rtl_step globals))
     616  Σt : (list rtl_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs|
    652617  match srcrs with
    653618  [ nil ⇒ 〈[ ],[ ]〉
     
    656621    [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
    657622    | _ ⇒
    658       let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in
    659       〈srcr :: new_srcrs', op
     623      let re ≝ shift_signed globals tmp srcrs' in
     624      〈srcr :: \fst re, \snd re
    660625    ]
    661626  ].
    662 
    663 lemma shift_signed_length : ∀globals,tmp,srcrs.
    664   |\fst (shift_signed globals tmp srcrs)| = |srcrs|.
    665 #globals #tmp #srcrs elim srcrs [//]
    666 #srcr * [//]
    667 #srcr' #srcrs'' #Hi
    668 whd in ⊢ (??(??(???%))?);
    669 @pair_elim #new_srcrs' #op #EQ >EQ in Hi;
    670 normalize #Hi >Hi //
    671 qed.
     627[1,2: %
     628|*: cases re * #a #b >p1 normalize #EQ >EQ %
     629] qed.
    672630
    673631definition translate_lt_signed :
     
    676634  ∀srcrs1: list rtl_argument.
    677635  ∀srcrs2: list rtl_argument.
    678   |destrs| = |srcrs1| →
    679636  |srcrs1| = |srcrs2| →
    680   bind_list register unit (rtl_step globals) ≝
    681   λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
     637  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     638  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    682639  νtmp_last_s1 in
    683640  νtmp_last_s2 in
     
    688645  let new_srcrs2 ≝ \fst p2 in
    689646  let shift_srcrs2 ≝ \snd p2 in
    690   shift_srcrs1 @ shift_srcrs2 @
    691   translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ??.
    692 >shift_signed_length [2: >shift_signed_length] assumption qed.
    693 
    694 definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    695   λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
     647  shift_srcrs1 @@ shift_srcrs2 @@
     648  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?.
     649whd in match new_srcrs1; whd in match new_srcrs2;
     650cases p1
     651cases p2
     652//
     653qed.
     654
     655definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     656  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
    696657  if is_unsigned then
    697     translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
     658    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
    698659  else
    699     translate_lt_signed globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf.
     660    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs_prf.
    700661
    701662definition translate_cmp ≝
    702   λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
     663  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs_prf.
    703664  match cmp with
    704665  [ Ceq ⇒
    705     translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
     666    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf @@
    706667    translate_toggle_bool globals destrs
    707668  | Cne ⇒
    708     translate_ne globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
     669    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf
    709670  | Clt ⇒
    710     translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
     671    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
    711672  | Cgt ⇒
    712     translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ?
     673    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ?
    713674  | Cle ⇒
    714     translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? ? @
     675    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? @@
    715676    translate_toggle_bool globals destrs
    716677  | Cge ⇒
    717     translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf @
     678    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@
    718679    translate_toggle_bool globals destrs
    719680  ].
    720681// qed.
    721  
     682
    722683definition translate_op2 :
    723   ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    724   λglobals: list ident.
    725   λop2.
    726   λdestrs: list register.
    727   λsrcrs1: list rtl_argument.
    728   λsrcrs2: list rtl_argument.
    729   λsrcrs1_prf: |destrs| = |srcrs1|.
    730   λsrcrs2_prf: |srcrs1| = |srcrs2|.
    731   match op2 with
    732   [ Oadd ⇒
    733     translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    734   | Oaddp ⇒
    735     translate_op globals Add destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    736   | Osub ⇒
    737     translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    738   | Osubpi ⇒
    739     translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    740   | Osubpp _ ⇒
    741     translate_op globals Sub destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    742   | Omul ⇒
    743     translate_mul globals destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    744   | Odivu ⇒
    745     translate_divumodu8 globals true destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    746   | Omodu ⇒
    747     translate_divumodu8 globals false destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    748   | Oand ⇒
    749     translate_op globals And destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    750   | Oor ⇒
    751     translate_op globals Or destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    752   | Oxor ⇒
    753     translate_op globals Xor destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    754   | Ocmp c ⇒
    755     translate_cmp false globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    756   | Ocmpu c ⇒
    757     translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    758   | Ocmpp c ⇒
    759     translate_cmp true globals c destrs srcrs1 srcrs2 srcrs1_prf srcrs2_prf
    760   | _ ⇒ ? (* assert false, implemented in run time or float op *)
    761   ].
    762   cases not_implemented (* XXX: yes, really *) qed.
    763 
    764 definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_step globals) ≝
     684  ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3.
     685  ∀destrs : list register.
     686  ∀srcrs1,srcrs2 : list rtl_argument.
     687  |destrs| = size_of_sig_type ty3 →
     688  |srcrs1| = size_of_sig_type ty1 →
     689  |srcrs2| = size_of_sig_type ty2 →
     690  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     691  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
     692  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
     693    ? = size_of_sig_type ty3 → ? = size_of_sig_type ty1 → ? = size_of_sig_type ty2 →
     694    bind_new ?? with
     695  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
     696    translate_op globals Add destrs srcrs1 srcrs2 ??
     697  | Oaddp sz r ⇒ λprf1,prf2,prf3.
     698    let is_Oaddp ≝ 0 in
     699    translate_op globals Add destrs srcrs1 srcrs2 ??
     700  | Osub sz sg ⇒ λprf1,prf2,prf2.
     701    translate_op globals Sub destrs srcrs1 srcrs2 ??
     702  | Osubpi sz r ⇒ λprf1,prf2,prf3.
     703    let is_Osubpi ≝ 0 in
     704    translate_op globals Sub destrs srcrs1 srcrs2 ??
     705  | Osubpp sz r1 r2 ⇒ λprf1,prf2,prf3.
     706    let is_Osubpp ≝ 0 in
     707    translate_op globals Sub destrs srcrs1 srcrs2 ??
     708  | Omul sz sg ⇒ λprf1,prf2,prf3.
     709    translate_mul globals destrs srcrs1 srcrs2 ??
     710  | Odivu sz ⇒ λprf1,prf2,prf3.
     711    translate_divumodu8 globals true destrs srcrs1 srcrs2 ??
     712  | Omodu sz ⇒ λprf1,prf2,prf3.
     713    translate_divumodu8 globals false destrs srcrs1 srcrs2 ??
     714  | Oand sz sg ⇒ λprf1,prf2,prf3.
     715    translate_op globals And destrs srcrs1 srcrs2 ??
     716  | Oor sz sg ⇒ λprf1,prf2,prf3.
     717    translate_op globals Or destrs srcrs1 srcrs2 ??
     718  | Oxor sz sg ⇒ λprf1,prf2,prf3.
     719    translate_op globals Xor destrs srcrs1 srcrs2 ??
     720  | Ocmp sz sg1 sg2 c ⇒ λprf1,prf2,prf3.
     721    translate_cmp false globals c destrs srcrs1 srcrs2 ?
     722  | Ocmpu sz sg c ⇒ λprf1,prf2,prf3.
     723    translate_cmp true globals c destrs srcrs1 srcrs2 ?
     724  | Ocmpp r sg c ⇒ λprf1,prf2,prf3.
     725    let is_Ocmpp ≝ 0 in
     726    translate_cmp true globals c destrs srcrs1 srcrs2 ?
     727  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
     728  ]. // try @not_implemented
     729  (* pointer arithmetics is broken at the moment *)
     730  cases daemon
     731  qed.
     732
     733definition translate_cond: ∀globals: list ident. list register → label →
     734  bind_seq_block rtl_params globals (joint_step rtl_params globals) ≝
    765735  λglobals: list ident.
    766736  λsrcrs: list register.
    767737  λlbl_true: label.
    768   match srcrs with
    769   [ nil ⇒ [ ]
     738  match srcrs return λ_.bind_seq_block rtl_params ? (joint_step ??) with
     739  [ nil ⇒ bret … 〈[ ], NOOP ??〉
    770740  | cons srcr srcrs' ⇒
    771741    ν tmpr in
    772     let f : register → rtl_step globals ≝
     742    let f : register → joint_seq rtl_params globals ≝
    773743      λr. tmpr ← tmpr .Or. r in
    774     MOVE rtl_params globals 〈tmpr,srcr〉 ::
    775     map … f srcrs' @
    776     [ COND ?? tmpr lbl_true ]
     744    bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
     745    map ?? f srcrs', (COND ? tmpr lbl_true : joint_step ??) 〉
    777746  ].
    778747
    779748(* Paolo: to be controlled (original seemed overly complex) *)
    780 definition translate_load
     749definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ?
    781750  λglobals: list ident.
    782751  λaddr : list rtl_argument.
     
    785754  ν tmp_addr_l in
    786755  ν tmp_addr_h in
    787   let f ≝ λdestr : register.λacc : list (rtl_step globals).
     756  let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals).
    788757    LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
    789758    translate_op … Add
     
    791760      [Reg tmp_addr_l ; Reg tmp_addr_h]
    792761      [imm_nat 0 ; Imm int_size] ? ? @ acc in
    793   translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
     762  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    794763  foldr … f [ ] destrs.
    795764[1: <addr_prf] // qed.
    796765 
    797 definition translate_store
     766definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ?
    798767  λglobals: list ident.
    799768  λaddr : list rtl_argument.
     
    802771  ν tmp_addr_l in
    803772  ν tmp_addr_h in
    804   let f ≝ λsrcr : rtl_argument.λacc : list (rtl_step globals).
     773  let f ≝ λsrcr : rtl_argument.λacc : list (joint_seq rtl_params globals).
    805774    STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
    806775    translate_op … Add
     
    808777      [Reg tmp_addr_l ; Reg tmp_addr_h]
    809778      [imm_nat 0 ; Imm int_size] ? ? @ acc in
    810   translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @
     779  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    811780  foldr … f [ ] srcrs.
    812781[1: <addr_prf] // qed.
    813782
    814 (* alias for b_adds_graph *)
    815 definition rtl_adds_graph ≝
    816   λglobals.b_adds_graph rtl_params globals register unit
    817     (rtl_ertl_fresh_reg rtl_params rtl_params globals).
    818 
    819 axiom fake_label: label.
    820 
    821 definition stmt_not_final ≝ λstmt.match stmt with
    822   [ St_return ⇒ False
    823   | St_tailcall_id _ _ ⇒ False
    824   | St_tailcall_ptr _ _ ⇒ False
    825   | _ ⇒ True ].
    826 
    827 definition translate_inst : ∀globals.?→?→?→
    828   (bind_list register unit (rtl_step globals)) × label ≝
    829   λglobals: list ident.
    830   λlenv: local_env.
    831   λstmt.
    832   λstmt_typed :
    833   λstmt_prf : stmt_not_final stmt.
    834   match stmt return λx.stmt = x →
    835     (bind_list register unit (rtl_step globals)) × label with
    836   [ St_skip lbl' ⇒ λ_.
    837     〈[ ], lbl'〉
    838   | St_cost cost_lbl lbl' ⇒ λ_.
    839     〈[COST_LABEL … cost_lbl], lbl'〉
    840   | St_const destr cst lbl' ⇒ λ_.
    841     〈translate_cst globals cst (find_local_env destr lenv) ?, lbl'〉
    842   | St_op1 ty ty' op1 destr srcr lbl' ⇒ λ_.
    843     〈translate_op1 globals ty' ty op1
    844       (find_local_env destr lenv)
    845       (find_local_env srcr lenv) ??, lbl'〉
    846   | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ λ_.
    847     〈translate_op2 globals op2
    848       (find_local_env destr lenv)
    849       (find_local_env_arg srcr1 lenv)
    850       (find_local_env_arg srcr2 lenv) ??, lbl'〉
     783definition translate_statement : ∀globals.local_env → statement →
     784  𝚺b :
     785  bind_seq_block rtl_params globals (joint_step rtl_params globals) +
     786  bind_seq_block rtl_params globals (joint_fin_step rtl_params).
     787  if is_inl … b then label else unit ≝
     788  λglobals,lenv,stmt.
     789  (*λstmt_typed : TODO*)
     790  match stmt return λ_.𝚺b:bind_seq_block ???+bind_seq_block ???.if is_inl … b then label else unit with
     791  [ St_skip lbl' ⇒
     792    ❬NOOP ??, lbl'❭
     793  | St_cost cost_lbl lbl' ⇒
     794    ❬COST_LABEL … cost_lbl, lbl'❭
     795  | St_const ty destr cst lbl' ⇒
     796    ❬translate_cst ty globals cst (find_local_env destr lenv ?) ?, lbl'❭
     797  | St_op1 ty ty' op1 destr srcr lbl' ⇒
     798    ❬translate_op1 globals ty' ty op1
     799      (find_local_env destr lenv ?)
     800      (find_local_env srcr lenv ?) ??, lbl'❭
     801  | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒
     802    ❬translate_op2 globals … op2
     803      (find_local_env destr lenv ?)
     804      (find_local_env_arg srcr1 lenv ?)
     805      (find_local_env_arg srcr2 lenv ?) ???, lbl'❭
    851806    (* XXX: should we be ignoring this? *)
    852   | St_load ignore addr destr lbl' ⇒ λ_.
    853     translate_load globals
    854       (find_local_env_arg addr lenv) ? (find_local_env destr lenv), lbl'〉
     807  | St_load ignore addr destr lbl' ⇒
     808    translate_load globals
     809      (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?), lbl'❭
    855810    (* XXX: should we be ignoring this? *)
    856   | St_store ignore addr srcr lbl' ⇒ λ_.
    857     〈translate_store globals (find_local_env_arg addr lenv) ?
    858       (find_local_env_arg srcr lenv), lbl'〉
    859   | St_call_id f args retr lbl' ⇒ λ_.
    860     (* Paolo: no notation to avoid ambiguity *)
    861     〈bcons … (
    862       match retr with
     811  | St_store ignore addr srcr lbl' ⇒
     812    ❬translate_store globals (find_local_env_arg addr lenv ?) ?
     813      (find_local_env_arg srcr lenv ?), lbl'❭
     814  | St_call_id f args retr lbl' ⇒
     815    ❬(match retr with
    863816      [ Some retr ⇒
    864         CALL_ID rtl_params globals f (rtl_args args lenv) (find_local_env retr lenv)
     817        CALL_ID rtl_params f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    865818      | None ⇒
    866         CALL_ID … f (rtl_args args lenv) [ ]
    867       ]) [ ], lbl'〉
    868   | St_call_ptr f args retr lbl' ⇒ λ_.
    869     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    870     (* Paolo: no notation to avoid ambiguity *)
    871     〈bcons … (
    872       match retr return λ_.rtl_step globals with
    873       [ Some retr ⇒
    874         rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
    875       | None ⇒
    876         rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ]
    877       ]) [ ], lbl'〉
    878   | St_cond r lbl_true lbl_false ⇒ λ_.
    879     〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
    880   | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
    881   | _ ⇒ λeq_stmt.⊥
    882   ] (refl …).
    883   [12: cases not_implemented (* jtable case *)
    884   |10,11,13: >eq_stmt in stmt_prf; normalize //
    885   |*: cases daemon
     819        CALL_ID rtl_params f (rtl_args args lenv ?) [ ]
     820      ] : bind_seq_block ???), lbl'❭
     821  | St_call_ptr f args retr lbl' ⇒
     822    let fs ≝ find_and_addr f lenv ?? in
     823    ❬(rtl_call_ptr (\fst fs) (\snd fs) (rtl_args args lenv ?)
     824      (match retr with
     825       [ Some retr ⇒
     826         find_local_env retr lenv ?
     827       | None ⇒ [ ]
     828       ]) : joint_step ??), lbl'❭
     829  | St_cond r lbl_true lbl_false ⇒
     830    ❬translate_cond globals (find_local_env r lenv ?) lbl_true, lbl_false❭
     831  | St_jumptable r l ⇒  ? (* assert false: not implemented yet *)
     832  | St_return ⇒ ❬RETURN ?, it❭
     833  ].
     834  [*: cases daemon
    886835  (* TODO: proofs regarding lengths of lists, examine! *)
    887   (* Paolo: probably hypotheses need to be added *)
    888836  ]
    889837qed.
    890838
    891 definition translate_stmt ≝
    892   λglobals,lenv,lbl,stmt,def.
    893   match stmt return λx.stmt = x → rtl_internal_function globals with
    894   [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def
    895   | St_tailcall_id f args ⇒ λ_.
    896     add_graph rtl_params globals lbl
    897       (extension_fin … (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
    898   | St_tailcall_ptr f args ⇒ λ_.
    899     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    900     add_graph rtl_params globals lbl
    901       (extension_fin … (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
    902   | _ ⇒ λstmt_eq.
    903     let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
    904     rtl_adds_graph globals translation lbl lbl' def
    905   ] (refl …).
    906 [10: cases daemon (* length of address lookup *)
    907 |*: >stmt_eq normalize %] qed.
    908  
    909  
     839lemma initialize_local_env_in : ∀l,runiverse,r.
     840  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env l runiverse).
     841#l #U #r @(list_elim_left … l)
     842[ *
     843| * #tl #sig #hd #IH #G elim (Exists_append … G) -G
     844  whd in match initialize_local_env; normalize nodelta
     845  >foldl_step change with (initialize_local_env ??) in match (foldl ?????);
     846  [ #H lapply (IH H)
     847  | * [2: *] #EQ destruct(EQ)
     848  ] 
     849  cases (initialize_local_env ??)
     850  #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
     851  elim (register_freshes ??) #U'' #rs
     852  [ >mem_set_add @orb_Prop_r assumption
     853  | @mem_set_add_id
     854  ]
     855qed.
     856
     857definition proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
     858// qed.
     859definition proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
     860// qed.
     861
     862
    910863(* XXX: we use a "hack" here to circumvent the proof obligations required to
    911864   create res, an empty internal_function record.  we insert into our graph
     
    916869  λdef.
    917870  let runiverse ≝ f_reggen def in
    918   let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    919     (f_params def @ f_locals def) (f_result def) in
    920   let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in
    921   let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
    922   let result ≝
    923     match (f_result def) with
    924     [ None ⇒ [ ]
    925     | Some r_typ ⇒
    926       let 〈r, typ〉 ≝ r_typ in
    927         find_local_env r lenv
    928     ]
     871  let 〈runiverse',lenv〉 as pr_eq ≝ initialize_local_env
     872    (match f_result def with [ None ⇒ [ ] | Some r_sig ⇒ [r_sig]] @
     873     f_params def @ f_locals def) runiverse in
     874  let params' ≝ map_list_local_env lenv (f_params def) ? in
     875  let locals' ≝ map_list_local_env lenv (f_locals def) ? in
     876  let result' ≝
     877    match (f_result def) return λx.f_result def = x → ? with
     878    [ None ⇒ λ_.[ ]
     879    | Some r_typ ⇒ λEQ.
     880       find_local_env (\fst r_typ) lenv ?
     881    ] (refl …)
    929882  in
    930883  let luniverse' ≝ f_labgen def in
    931   let runiverse' ≝ runiverse in
    932   let result' ≝ result in
    933   let params' ≝ parameters in
    934   let locals' ≝ locals in
    935884  let stack_size' ≝ f_stacksize def in
    936885  let entry' ≝ f_entry def in
    937886  let exit' ≝ f_exit def in
    938   let graph' ≝ empty_map LabelTag ? in
     887  let graph' ≝ empty_map LabelTag (joint_statement rtl_params globals) in
    939888  let graph' ≝ add LabelTag ? graph' entry'
    940889    (GOTO … exit') in
    941890  let graph' ≝ add LabelTag ? graph' exit'
    942891    (RETURN …) in
     892  let f_trans ≝ λlbl,stmt,def.
     893    let pr ≝ translate_statement … lenv stmt in
     894    b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
    943895  let res ≝
    944896    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
    945897     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    946     foldi … (translate_stmt globals … lenv) (f_graph def) res.
    947 [ @graph_add_lookup ] @graph_add
     898    foldi … f_trans (f_graph def) res. 
     899   
     900[1,2: >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
     901| >(proj2_rewrite ????? pr_eq)
     902  @initialize_local_env_in >EQ normalize nodelta %1 %
     903|*: >(proj2_rewrite ????? pr_eq)
     904  @(All_mp ??? (λpr.initialize_local_env_in ?? (\fst pr)))
     905  [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_locals def)))
     906    [ #a #H @Exists_append_r @Exists_append_r @H
     907    | generalize in match (f_locals def);
     908    ]
     909  | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_params def)))
     910    [ #a #H @Exists_append_r @Exists_append_l @H
     911    | generalize in match (f_params def);
     912    ]
     913  ]
     914  #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
     915]
    948916qed.
    949917
Note: See TracChangeset for help on using the changeset viewer.