Changeset 2155


Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (5 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

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1882 r2155  
    1616  on _n : nat to rtl_argument.
    1717
    18 inductive rtl_step_extension: Type[0] ≝
    19   | rtl_st_ext_stack_address: register → register → rtl_step_extension
    20   | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension.
     18inductive rtl_seq : Type[0] ≝
     19  | rtl_stack_address: register → register → rtl_seq.
     20 
     21inductive rtl_call : Type[0] ≝
     22  | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
    2123
    22 inductive rtl_statement_extension : Type[0] ≝
    23   | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
    24   | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
     24inductive rtl_tailcall : Type[0] ≝
     25  | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
     26  | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
    2527
    2628definition rtl_uns_params ≝ mk_unserialized_params
     
    3840    (* call_args ≝ *) (list rtl_argument)
    3941    (* call_dest ≝ *) (list register)
    40     (* ext_step ≝ *) rtl_step_extension
    41     (* ext_step_labels ≝ *) (λes.[ ])
    42     (* ext_fin_stmt ≝ *) rtl_statement_extension
    43     (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
     42    (* ext_seq ≝ *) rtl_seq
     43    (* ext_call ≝ *) rtl_call
     44    (* ext_tailcall ≝ *) rtl_tailcall
     45  )
    4446  (mk_local_params
    4547    (mk_funct_params
    4648      (* resultT ≝ *) (list register)
    4749      (* paramsT ≝ *) (list register))
    48       (* localsT ≝ *) (list register)).
     50      (* localsT ≝ *) register).
    4951
    5052definition rtl_params ≝ mk_graph_params rtl_uns_params.
     
    5456definition rtl_program ≝ joint_program rtl_params.
    5557definition rtl_step ≝ joint_step rtl_params.
     58definition rtl_seq ≝ joint_seq rtl_params.
    5659definition rtl_statement ≝ joint_statement rtl_params.
    57 
    5860
    5961interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
     
    6365unification hint 0 ≔
    6466(*---------------*) ⊢
    65 acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     67acc_a_reg rtl_params ≡ register.
    6668unification hint 0 ≔
    6769(*---------------*) ⊢
    68 acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     70acc_b_reg rtl_params ≡ register.
    6971unification hint 0 ≔
    7072(*---------------*) ⊢
    71 acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     73acc_a_arg rtl_params ≡ rtl_argument.
    7274unification hint 0 ≔
    7375(*---------------*) ⊢
    74 acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     76acc_b_arg rtl_params ≡ rtl_argument.
    7577unification hint 0 ≔
    7678(*---------------*) ⊢
    77 dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     79dpl_reg rtl_params ≡ register.
    7880unification hint 0 ≔
    7981(*---------------*) ⊢
    80 dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
     82dph_reg rtl_params ≡ register.
    8183unification hint 0 ≔
    8284(*---------------*) ⊢
    83 dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     85dpl_arg rtl_params ≡ rtl_argument.
    8486unification hint 0 ≔
    8587(*---------------*) ⊢
    86 dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     88dph_arg rtl_params ≡ rtl_argument.
    8789unification hint 0 ≔
    8890(*---------------*) ⊢
    89 snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
     91snd_arg rtl_params ≡ rtl_argument.
    9092unification hint 0 ≔
    9193(*---------------*) ⊢
    92 pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
     94pair_move rtl_params ≡ register × rtl_argument.
    9395unification hint 0 ≔
    9496(*---------------*) ⊢
    95 call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
     97call_args rtl_params ≡ list rtl_argument.
    9698unification hint 0 ≔
    9799(*---------------*) ⊢
    98 call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
     100call_dest rtl_params ≡ list register.
    99101
    100102unification hint 0 ≔
    101103(*---------------*) ⊢
    102 ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
     104ext_seq rtl_params ≡ rtl_seq.
     105unification hint 0 ≔
     106(*---------------*) ⊢
     107ext_call rtl_params ≡ rtl_call.
     108unification hint 0 ≔
     109(*---------------*) ⊢
     110ext_tailcall rtl_params ≡ rtl_tailcall.
    103111unification hint 0 ≔ globals
    104112(*---------------*) ⊢
    105 joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.
     113joint_step rtl_params globals ≡ rtl_step globals.
    106114
    107 unification hint 0 ≔
     115unification hint 0 ≔ globals
    108116(*---------------*) ⊢
    109 ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
     117joint_seq rtl_params globals ≡ rtl_seq globals.
    110118unification hint 0 ≔ globals
    111119(*---------------*) ⊢
    112120joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    113121
     122coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
     123  on _r : register to snd_arg rtl_params.
     124coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
     125  on _b : Byte to snd_arg rtl_params.
     126
     127
    114128(************ Same without tail calls ****************)
    115 
    116 inductive rtlntc_statement_extension: Type[0] ≝
    117   | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
    118   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    119129
    120130definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
     
    132142    (* call_args ≝ *) (list rtl_argument)
    133143    (* call_dest ≝ *) (list register)
    134     (* extend_statements ≝ *) rtlntc_statement_extension
    135     (* ext_forall_labels ≝ *) (λes.[ ])
    136     void (λes.[ ]))
     144    (* ext_seq ≝ *) rtl_seq
     145    (* ext_call ≝ *) rtl_call
     146    (* ext_tailcall ≝ *) void
     147  )
    137148  (mk_local_params
    138149    (mk_funct_params
    139150      (* resultT ≝ *) (list register)
    140151      (* paramsT ≝ *) (list register))
    141       (* localsT ≝ *) (list register))).
     152      (* localsT ≝ *) register)).
    142153
    143154definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
  • 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
  • src/common/Identifiers.ma

    r2111 r2155  
    834834qed. 
    835835
    836 
    837 
     836lemma map_mem_prop :
     837  ∀tag,A.∀m : identifier_map tag A.∀i.
     838  lookup ?? m i ≠ None ? → i ∈ m.
     839#p #globals #m #i
     840lapply (in_map_domain … m i)
     841cases (i∈m)
     842[ * #x #_ #_ %
     843| #EQ >EQ * #ABS @ABS %
     844] qed.
     845
     846
     847
  • src/joint/Joint_paolo.ma

    r1976 r2155  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
    9 include "basics/deqsets.ma".
    10 include "basics/finset.ma". (* for DeqNat *)
     9include "common/StructuredTraces.ma".
    1110
    1211(* Here is the structure of parameter records (downward edges are coercions,
     
    3736params : adds type of code and related properties *)
    3837
     38inductive possible_flows : Type[0] ≝
     39| Labels : list label → possible_flows
     40| Call : possible_flows.
     41
    3942record step_params : Type[1] ≝
    4043 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
     
    5053 ; call_args: Type[0] (* arguments of function calls *)
    5154 ; call_dest: Type[0] (* possible destination of function computation *)
    52  ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
    53  ; ext_step_labels : ext_step → list label
    54  ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
    55  ; ext_fin_stmt_labels : ext_fin_stmt → list label
     55 (* other instructions not fitting in the general framework *)
     56 ; ext_seq : Type[0]
     57(* ; ext_branch : Type[0]
     58 ; ext_branch_labels : ext_branch → list label*)
     59 ; ext_call : Type[0]
     60 ; ext_tailcall : Type[0]
     61 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    5662 }.
    57  
    58 inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
    59   | COMMENT: String → joint_step p globals
    60   | COST_LABEL: costlabel → joint_step p globals
    61   | MOVE: pair_move p → joint_step p globals
    62   | POP: acc_a_reg p → joint_step p globals
    63   | PUSH: acc_a_arg p → joint_step p globals
    64   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
    65   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
    66   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
    67   | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
     63
     64inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
     65  | COMMENT: String → joint_seq p globals
     66  | COST_LABEL: costlabel → joint_seq p globals
     67  | MOVE: pair_move p → joint_seq p globals
     68  | POP: acc_a_reg p → joint_seq p globals
     69  | PUSH: acc_a_arg p → joint_seq p globals
     70  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     71  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
     72  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     73  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
    6874  (* int done with generic move *)
    69 (*| INT: generic_reg p → Byte → joint_step p globals *)
    70   | CLEAR_CARRY: joint_step p globals
    71   | SET_CARRY: joint_step p globals
    72   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
    73   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
    74   | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
    75   | COND: acc_a_reg p → label → joint_step p globals
    76   | extension: ext_step p → joint_step p globals.
     75(*| INT: generic_reg p → Byte → joint_seq p globals *)
     76  | CLEAR_CARRY: joint_seq p globals
     77  | SET_CARRY: joint_seq p globals
     78  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
     79  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
     80  | extension_seq : ext_seq p → joint_seq p globals.
    7781
    7882axiom EmptyString : String.
     
    9296interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9397
    94 coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
    95   extension on _s : ext_step ? to joint_step ??.
     98coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     99  extension_seq on _s : ext_seq ? to joint_seq ??.
     100
     101inductive joint_call (p : step_params) : Type[0] ≝
     102  | CALL_ID: ident → call_args p → call_dest p → joint_call p
     103  | extension_call : ext_call p → joint_call p.
     104
     105coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
     106  extension_call on _s : ext_call ? to joint_call ?.
     107 
     108inductive joint_branch (p : step_params) : Type[0] ≝
     109  | COND: acc_a_reg p → label → joint_branch p
     110  (*| extension_branch : ext_branch p → joint_branch p*).
     111
     112(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     113  extension_branch on _s : ext_branch ? to joint_branch ?.*)
     114
     115inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
     116  | step_seq : joint_seq p globals → joint_step p globals
     117  | step_call : joint_call p → joint_step p globals
     118  | step_branch : joint_branch p → joint_step p globals.
     119
     120coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
     121  step_seq on _s : joint_seq ?? to joint_step ??.
     122coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
     123  step_call on _s : joint_call ? to joint_step ??.
     124coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
     125  step_branch on _s : joint_branch ? to joint_step ??.
     126
     127definition step_flows ≝ λp,globals.λs : joint_step p globals.
     128  match s with
     129  [ step_seq _ ⇒ Labels … [ ]
     130  | step_call _ ⇒ Call
     131  | step_branch s ⇒
     132    match s with
     133    [ COND _ l ⇒ Labels … [l]
     134    (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
     135    ]
     136  ].
    96137
    97138definition step_labels ≝
    98139  λp, globals.λs : joint_step p globals.
    99     match s with
    100     [ COND _ l ⇒ [l]
    101     | extension ext_s ⇒ ext_step_labels ? ext_s
    102     | _ ⇒ [ ]
     140    match step_flows … s with
     141    [ Labels lbls ⇒ lbls
     142    | Call ⇒ [ ]
    103143    ].
    104144
     
    106146    (label → Prop) → joint_step p globals → Prop ≝
    107147λp,g,P,inst. All … P (step_labels … inst).
    108  
     148
     149definition step_classifier :
     150  ∀p : step_params.∀globals.
     151    joint_step p globals → status_class ≝ λp,g,s.
     152  match s with
     153  [ step_seq _ ⇒ cl_other
     154  | step_call _ ⇒ cl_call
     155  | step_branch _ ⇒ cl_jump
     156  ].
     157
    109158record funct_params : Type[1] ≝
    110159  { resultT : Type[0]
     
    117166 }.
    118167
    119 
    120168record unserialized_params : Type[1] ≝
    121169 { u_inst_pars :> step_params
     
    129177  }.
    130178
    131 inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝
    132   | GOTO: label → joint_fin_step p globals
    133   | RETURN: joint_fin_step p globals
    134   | extension_fin : ext_fin_stmt p → joint_fin_step p globals.
     179inductive joint_fin_step (p: step_params): Type[0] ≝
     180  | GOTO: label → joint_fin_step p
     181  | RETURN: joint_fin_step p
     182  | tailcall : ext_tailcall p → joint_fin_step p.
     183
     184definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     185  match s with
     186  [ GOTO l ⇒ Labels … [l]
     187  | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *)
     188  ].
     189
     190definition fin_step_labels ≝
     191  λp.λs : joint_fin_step p.
     192    match fin_step_flows … s with
     193    [ Labels lbls ⇒ lbls
     194    | Call ⇒ [ ]
     195    ].
     196
     197definition fin_step_classifier :
     198  ∀p : stmt_params.
     199    joint_fin_step p → status_class
     200  ≝ λp,s.
     201  match s with
     202  [ GOTO _ ⇒ cl_other
     203  | _ ⇒ cl_return
     204  ].
    135205
    136206inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    137207  | sequential: joint_step p globals → succ p → joint_statement p globals
    138   | final: joint_fin_step p globals → joint_statement p globals.
    139 
    140 coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals.
    141   ∀s : ext_fin_stmt p.joint_fin_step p globals ≝
    142   extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??.
     208  | final: joint_fin_step p → joint_statement p globals.
     209
     210definition stmt_classifier :
     211  ∀p : stmt_params.∀globals.
     212    joint_statement p globals → status_class
     213  ≝ λp,g,s.
     214  match s with
     215  [ sequential stp _ ⇒ step_classifier p g stp
     216  | final stp ⇒ fin_step_classifier p stp
     217  ].
     218
     219coercion extension_fin_to_fin_step : ∀p : stmt_params.
     220  ∀s : ext_tailcall p.joint_fin_step p ≝
     221  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
    143222
    144223coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
    145   ∀s : joint_fin_step p globals.joint_statement p globals ≝
    146   final on _s : joint_fin_step ?? to joint_statement ??.
     224  ∀s : joint_fin_step p.joint_statement p globals ≝
     225  final on _s : joint_fin_step ? to joint_statement ??.
    147226
    148227record params : Type[1] ≝
    149228 { stmt_pars :> stmt_params
    150229 ; codeT: list ident → Type[0]
    151  ; code_point : DeqSet
     230 ; code_point : Type[0]
    152231 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
    153232 ; point_of_label : ∀globals.codeT globals → label → option code_point
     
    192271  [ Some pt ⇒ code_has_point … c pt
    193272  | None ⇒ false
    194   ].
    195 
    196 definition fin_step_labels ≝
    197   λp,globals.λs : joint_fin_step p globals.
    198   match s with
    199   [ GOTO l ⇒ [ l ]
    200   | RETURN ⇒ [ ]
    201   | extension_fin c ⇒ ext_fin_stmt_labels … c
    202273  ].
    203274
     
    254325
    255326record lin_params : Type[1] ≝
    256   { l_u_pars :> unserialized_params }.
     327  { l_u_pars : unserialized_params }.
    257328 
    258329lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     
    290361  λlp : lin_params.
    291362     mk_params
    292       (mk_stmt_params lp unit (λ_.None ?))
     363      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
    293364    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    294     (* code_point ≝ *)DeqNat
     365    (* code_point ≝ *)
    295366    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
    296367    (* point_of_label ≝ *)(λglobals,c,lbl.
     
    325396
    326397record graph_params : Type[1] ≝
    327   { g_u_pars :> unserialized_params }.
     398  { g_u_pars : unserialized_params }.
    328399
    329400(* One common instantiation of params via Graphs of joint_statements
     
    332403  λgp : graph_params.
    333404     mk_params
    334       (mk_stmt_params gp label (Some ?))
     405      (mk_stmt_params (g_u_pars gp) label (Some ?))
    335406    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    336     (* code_point ≝ *)(Deq_identifier LabelTag)
     407    (* code_point ≝ *)label
    337408    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
    338409    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
  • src/joint/TranslateUtils_paolo.ma

    r1882 r2155  
    11include "joint/Joint_paolo.ma".
    2 include "utilities/bindLists.ma".
     2include "joint/blocks.ma".
    33
    44(* general type of functions generating fresh things *)
     
    3535
    3636(* insert into a graph a block of instructions *)
    37 let rec adds_graph
     37let rec adds_graph_list
    3838  (g_pars: graph_params)
    3939  (globals: list ident)
    40   (insts: list (joint_step g_pars globals))
     40  (insts: list (joint_seq g_pars globals))
    4141  (src : label)
    42   (dest : label)
    43   (def: joint_internal_function … g_pars) on insts
     42  (def: joint_internal_function … g_pars) on insts
     43  : (joint_internal_function … g_pars) × label
    4444  match insts with
    45   [ nil ⇒ add_graph … src (GOTO … dest) def
     45  [ nil ⇒ 〈def, src〉
    4646  | cons instr others ⇒
    47     match others with
    48     [ nil ⇒ (* only one instruction *)
    49       add_graph … src (sequential … instr dest) def
    50     | _ ⇒ (* need to generate label *)
    51       let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    52       adds_graph g_pars globals others tmp_lbl dest
    53         (add_graph … src (sequential … instr tmp_lbl) def)
    54     ]
     47    let 〈def, mid〉 ≝ fresh_label … def in
     48    let def ≝ add_graph … src (sequential … instr mid) def in
     49    adds_graph_list g_pars globals others mid def
     50  ].
     51
     52definition adds_graph :
     53  ∀g_pars : graph_params.
     54  ∀globals: list ident.
     55  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
     56       seq_block g_pars globals (joint_fin_step g_pars).
     57  label → if is_inl … b then label else unit →
     58  joint_internal_function … g_pars → joint_internal_function … g_pars ≝
     59  λg_pars,globals,insts,src.
     60  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     61  [ inl b ⇒ λdst,def.
     62    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     63    add_graph … mid (sequential … (\snd b) dst) def
     64  | inr b ⇒ λdst,def.
     65    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     66    add_graph … mid (final … (\snd b)) def
    5567  ].
    5668
     
    6072  (* fresh register creation *)
    6173  freshT globals g_pars (localsT … g_pars) →
    62   ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
    63   ∀src : label.
    64   ∀dest : label.
     74  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
     75       bind_seq_block g_pars globals (joint_fin_step g_pars).
     76  label → if is_inl … b then label else unit →
    6577  joint_internal_function globals g_pars →
    6678  joint_internal_function globals g_pars ≝
    67   λg_pars,globals,fresh_r,insts,src,dest,def.
    68   let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
    69   adds_graph … stmts src dest def'.
     79  λg_pars,globals,fresh_r,insts,src.
     80  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     81  [ inl b ⇒ λdst,def.
     82    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     83    adds_graph … (inl … stmts) src dst def
     84  | inr b ⇒ λdst,def.
     85    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     86    adds_graph … (inr … stmts) src dst def
     87  ].
    7088
    7189(* translation with inline fresh register allocation *)
     
    7593  (* fresh register creation *)
    7694  freshT globals dst_g_pars (localsT dst_g_pars) →
    77   (* function dictating the translation *)
    78   (label → joint_step src_g_pars globals →
    79     bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
    80     (* this can be added to allow redirections: × label *)) →
    81   (label → ext_fin_stmt src_g_pars →
    82      bind_new (localsT dst_g_pars)
    83       ((list (joint_step dst_g_pars globals))
    84       ×
    85       (joint_statement dst_g_pars globals))) →
    8695  (* initialized function definition with empty graph *)
    8796  joint_internal_function globals dst_g_pars →
     97  (* functions dictating the translation *)
     98  (label → joint_step src_g_pars globals →
     99    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     100  (label → joint_fin_step src_g_pars →
     101    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    88102  (* source function *)
    89103  joint_internal_function globals src_g_pars →
    90104  (* destination function *)
    91   joint_internal_function globals dst_g_pars ≝ 
    92   λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
     105  joint_internal_function globals dst_g_pars ≝
     106  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
    93107  let f : label → joint_statement (src_g_pars : params) globals →
    94108    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    95109    λlbl,stmt,def.
    96110    match stmt with
    97     [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def
    98     | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    99     | RETURN ⇒ add_graph … lbl (RETURN …) def
    100     | extension_fin c ⇒
    101       let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in
    102       let 〈insts, fin〉 ≝ p in
    103       let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in
    104       adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def)
     111    [ sequential inst next ⇒
     112      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
     113    | final inst ⇒
     114      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
    105115    ] in
    106116  foldi … f (joint_if_code … def) empty.
    107  
     117(* 
    108118(* translation without register allocation *)
    109119definition graph_translate :
     
    137147    ] in
    138148  foldi ??? f (joint_if_code ?? def) empty.
    139 
     149*)
     150(*
    140151definition graph_to_lin_statement :
    141152  ∀p : unserialized_params.∀globals.
    142153  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
    143   λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with
     154  λp,globals,stmt.match stmt with
    144155  [ sequential c _ ⇒ sequential … c it
    145   | GOTO l ⇒ GOTO … l
    146   | RETURN ⇒ RETURN …
    147   | extension_fin c ⇒ extension_fin … c
     156  | final c ⇒
     157    final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with
     158    [ GOTO l ⇒ GOTO … l
     159    | RETURN ⇒ RETURN …
     160    | extension_fin c ⇒ extension_fin ?? c
     161    ]
    148162  ].
    149163
     
    152166  stmt_labels … (graph_to_lin_statement p globals s) =
    153167  stmt_explicit_labels … s.
    154 #p#globals * //
     168#p#globals * [//] * //
    155169qed.
    156170
     
    216230(*----------------------------*)⊢
    217231list lo ≡ codeT lp globals.
     232
    218233
    219234definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
     
    791806#f_out * #f_out_closed #H assumption
    792807qed.
    793 
    794  
     808*) 
    795809
    796810     
  • src/joint/blocks.ma

    r2042 r2155  
    11include "joint/Joint_paolo.ma".
    2 include "utilities/bind_new.ma".
    3 
    4 definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝
    5   λA,B,C,f,p.f (\fst p) (\snd p).
    6 
    7 inductive stmt_type : Type[0] ≝
    8   | SEQ : stmt_type
    9   | FIN : stmt_type.
    10 
    11 definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝
    12   λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ].
    13 
    14 definition block_cont ≝ λp : params.λglobals,ty.
    15   (list (joint_step p globals)) ×
    16     (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals).
    17 
    18 definition Skip : ∀p,globals.block_cont p globals SEQ ≝
    19   λp,globals.〈[ ], NOOP …〉.
    20 
    21 definition instr_block ≝ λp : params.λglobals,ty.
    22   bind_new (localsT p) (block_cont p globals ty).
    23 unification hint 0 ≔ p, globals, ty;
    24 B ≟ block_cont p globals ty, R ≟ localsT p
     2include "utilities/bindLists.ma".
     3
     4inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
     5  | block_seq : joint_seq p globals → block_step p globals
     6  | block_skip : label → block_step p globals.
     7
     8definition if_seq : ∀p,globals.∀A:Type[2].block_step p globals → A → A → A ≝
     9λp,g,A,s.match s with
     10[ block_seq _ ⇒ λx,y.x
     11| _ ⇒ λx,y.y
     12].
     13
     14definition stmt_of_block_step : ∀p : stmt_params.∀globals.
     15  ∀s : block_step p globals.if_seq … s (succ p) unit → joint_statement p globals ≝
     16  λp,g,s.match s return λx.if_seq ??? x ?? → joint_statement ?? with
     17  [ block_seq s' ⇒ λnxt.sequential … s' nxt
     18  | block_skip l ⇒ λ_.GOTO … l
     19  ].
     20
     21definition seq_to_block_step_list : ∀p : stmt_params.∀globals.
     22  list (joint_seq p globals) →
     23  list (block_step p globals) ≝ λp,globals.map ?? (block_seq ??).
     24
     25coercion block_step_from_seq_list : ∀p : stmt_params.∀globals.
     26  ∀l:list (joint_seq p globals).
     27  list (block_step p globals) ≝
     28  seq_to_block_step_list
     29  on _l:list (joint_seq ??)
     30  to list (block_step ??).
     31
     32definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     33  [ inl _ ⇒ true
     34  | inr _ ⇒ false
     35  ].
     36definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     37  [ inl _ ⇒ true
     38  | inr _ ⇒ false
     39  ].
     40
     41definition skip_block ≝ λp,globals,A.
     42  (list (block_step p globals)) × A.
     43
     44definition seq_block ≝ λp : stmt_params.λglobals,A.
     45  (list (joint_seq p globals)) × A.
     46
     47definition seq_to_skip_block :
     48  ∀p,g,A.seq_block p g A → skip_block p g A
     49 ≝ λp,g,A,b.〈\fst b, \snd b〉.
     50
     51coercion skip_from_seq_block :
     52  ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
     53  seq_to_skip_block on _b : seq_block ??? to skip_block ???.
     54
     55definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
     56  bind_new (localsT p) (seq_block p globals A).
     57unification hint 0 ≔ p : stmt_params, g, X;
     58R ≟ localsT p,
     59P ≟ seq_block p g X
    2560(*---------------------------------------*)⊢
    26 instr_block p globals ty ≡ bind_new R B.
    27 
    28 definition block_cont_append :
    29   ∀p,g,ty.
    30   ∀b1 : block_cont p g SEQ.
    31   ∀b2 : block_cont p g ty.
    32   block_cont p g ty ≝
    33   λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉.
    34 
    35 definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉.
    36 
    37 interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b).
    38 interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2).
    39 
    40 definition step_to_block : ∀p : params.∀g.
    41   joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉.
    42 
    43 definition fin_step_to_block : ∀p : params.∀g.
    44   joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉.
    45 
    46 coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g.
    47   block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ.
    48 
    49 coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g.
    50   block_cont p g FIN ≝ fin_step_to_block
    51   on _s : joint_fin_step ?? to block_cont ?? FIN.
    52 
    53 definition block_cons :
    54   ∀p : params.∀globals,ty.
    55   joint_step p globals → instr_block p globals ty → instr_block p globals ty
    56   ≝ λp,globals,ty,x.m_map … (block_cont_cons … x).
    57 
    58 definition block_append :
    59   ∀p : params.∀globals,ty.
    60   instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝
    61   λp,globals,ty.m_bin_op … (block_cont_append …).
    62 
    63 interpretation "instruction block cons" 'cons x b = (block_cons ??? x b).
    64 interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2).
    65 
    66 let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝
     61bind_seq_block p g X ≡ bind_new R P.
     62
     63definition bind_seq_list ≝ λp : stmt_params.λglobals.
     64  bind_new (localsT p) (list (joint_seq p globals)).
     65unification hint 0 ≔ p : stmt_params, g;
     66R ≟ localsT p,
     67S ≟ joint_seq p g,
     68L ≟ list S
     69(*---------------------------------------*)⊢
     70bind_seq_list p g ≡ bind_new R L.
     71
     72definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     73  bind_new (localsT p) (skip_block p globals A).
     74unification hint 0 ≔ p : stmt_params, g, A;
     75B ≟ skip_block p g A, R ≟ localsT p
     76(*---------------------------------------*)⊢
     77bind_skip_block p g A ≡ bind_new R B.
     78
     79definition bind_seq_to_skip_block :
     80  ∀p,g,A.bind_seq_block p g A → bind_skip_block p g A ≝
     81  λp,g,A.m_map ? (seq_block p g A) (skip_block p g A)
     82    (λx.x).
     83
     84coercion bind_skip_from_seq_block :
     85  ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
     86  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.
     87(*
     88definition block_classifier ≝
     89  λp,g.λb : other_block p g.
     90  seq_or_fin_step_classifier ?? (\snd b).
     91*)
     92
     93let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝
     94match l with
     95[ nil ⇒ 〈[ ], dflt〉
     96| cons hd tl ⇒
     97  match tl with
     98  [ nil ⇒ 〈[ ], hd〉
     99  | _ ⇒
     100    let 〈pref, post〉 ≝ split_on_last A dflt tl in
     101    〈hd :: pref, post〉
     102  ]
     103].
     104
     105lemma split_on_last_ok :
     106  ∀A,dflt,l.
     107  match l with
     108  [ nil ⇒ True
     109  | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post])
     110  ].
     111#A #dflt #l elim l normalize nodelta
     112[ %
     113| #hd * [ #_ %]
     114  #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?);
     115  elim (split_on_last ???) #a #b %
     116]
     117qed.
     118
     119definition seq_block_from_seq_list :
     120∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
     121λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
     122
     123definition bind_seq_block_from_bind_seq_list :
     124  ∀p : stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) →
     125    bind_seq_block p g (joint_step p g) ≝ λp.λg.m_map … (seq_block_from_seq_list …).
     126
     127definition bind_seq_block_step :
     128  ∀p,g.bind_seq_block p g (joint_step p g) →
     129    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     130  λp,g.inl ….
     131coercion bind_seq_block_from_step :
     132  ∀p,g.∀b:bind_seq_block p g (joint_step p g).
     133    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     134  bind_seq_block_step on _b : bind_seq_block ?? (joint_step ??) to
     135    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
     136
     137definition bind_seq_block_fin_step :
     138  ∀p,g.bind_seq_block p g (joint_fin_step p) →
     139    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     140  λp,g.inr ….
     141coercion bind_seq_block_from_fin_step :
     142  ∀p,g.∀b:bind_seq_block p g (joint_fin_step p).
     143    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     144  bind_seq_block_fin_step on _b : bind_seq_block ?? (joint_fin_step ?) to
     145    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
     146
     147definition seq_block_bind_seq_block :
     148  ∀p : stmt_params.∀g,A.seq_block p g A → bind_seq_block p g A ≝ λp,g,A.bret ….
     149coercion seq_block_to_bind_seq_block :
     150  ∀p : stmt_params.∀g,A.∀b:seq_block p g A.bind_seq_block p g A ≝
     151  seq_block_bind_seq_block
     152  on _b : seq_block ??? to bind_seq_block ???.
     153
     154definition joint_step_seq_block : ∀p : stmt_params.∀g.joint_step p g → seq_block p g (joint_step p g) ≝
     155  λp,g,x.〈[ ], x〉.
     156coercion joint_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_step p g.seq_block p g (joint_step p g) ≝
     157  joint_step_seq_block on _b : joint_step ?? to seq_block ?? (joint_step ??).
     158
     159definition joint_fin_step_seq_block : ∀p : stmt_params.∀g.joint_fin_step p → seq_block p g (joint_fin_step p) ≝
     160  λp,g,x.〈[ ], x〉.
     161coercion joint_fin_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_fin_step p.seq_block p g (joint_fin_step p) ≝
     162  joint_fin_step_seq_block on _b : joint_fin_step ? to seq_block ?? (joint_fin_step ?).
     163
     164definition seq_list_seq_block :
     165  ∀p:stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
     166  λp,g,l.let pr ≝ split_on_last … (NOOP ??) l in 〈\fst pr, \snd pr〉.
     167coercion seq_list_to_seq_block :
     168  ∀p:stmt_params.∀g.∀l:list (joint_seq p g).seq_block p g (joint_step p g) ≝
     169  seq_list_seq_block on _l : list (joint_seq ??) to seq_block ?? (joint_step ??).
     170
     171definition bind_seq_list_bind_seq_block :
     172  ∀p:stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → bind_seq_block p g (joint_step p g) ≝
     173  λp,g.m_map ??? (λx : list (joint_seq ??).(x : seq_block ???)).
     174
     175coercion bind_seq_list_to_bind_seq_block :
     176  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
     177  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
     178
     179(*
     180
     181definition seq_block_append :
     182  ∀p,g.
     183  ∀b1 : Σb.is_safe_block p g b.
     184  ∀b2 : seq_block p g.
     185  seq_block p g ≝ λp,g,b1,b2.
     186  〈match b1 with
     187  [ mk_Sig instr prf ⇒
     188    match \snd instr return λx.bool_to_Prop (is_inl … x) ∧ seq_or_fin_step_classifier … x = ? → ? with
     189    [ inl i ⇒ λprf.\fst b1 @ i :: \fst b2
     190    | inr _ ⇒ λprf.⊥
     191    ] prf
     192  ],\snd b2〉.
     193  cases prf #H1 #H2 assumption
     194  qed.
     195
     196definition other_block_append :
     197  ∀p,g.
     198  (Σb.block_classifier ?? b = cl_other) →
     199  other_block p g →
     200  other_block p g ≝ λp,g,b1,b2.
     201  〈\fst b1 @ «\snd b1, pi2 … b1» :: \fst b2, \snd b2〉.
     202
     203definition seq_block_cons : ∀p : stmt_params.∀g.(Σs.step_classifier p g s = cl_other) →
     204  seq_block p g → seq_block p g ≝
     205  λp,g,x,b.〈x :: \fst b,\snd b〉.
     206definition other_block_cons : ∀p,g.
     207  (Σs.seq_or_fin_step_classifier p g s = cl_other) → other_block p g →
     208  other_block p g ≝
     209  λp,g,x,b.〈x :: \fst b,\snd b〉.
     210
     211interpretation "seq block cons" 'cons x b = (seq_block_cons ?? x b).
     212interpretation "other block cons" 'vcons x b = (other_block_cons ?? x b).
     213interpretation "seq block append" 'append b1 b2 = (seq_block_append ?? b1 b2).
     214interpretation "other block append" 'vappend b1 b2 = (other_block_append ?? b1 b2).
     215
     216definition step_to_block : ∀p,g.
     217  seq_or_fin_step p g → seq_block p g ≝ λp,g,s.〈[ ], s〉.
     218
     219coercion block_from_step : ∀p,g.∀s : seq_or_fin_step p g.
     220  seq_block p g ≝ step_to_block on _s : seq_or_fin_step ?? to seq_block ??.
     221
     222definition bind_seq_block_cons :
     223  ∀p : stmt_params.∀g,is_seq.
     224  (Σs.step_classifier p g s = cl_other) → bind_seq_block p g is_seq →
     225  bind_seq_block p g is_seq ≝
     226  λp,g,is_seq,x.m_map ??? (λb.〈x::\fst b,\snd b〉).
     227
     228definition bind_other_block_cons :
     229  ∀p,g.(Σs.seq_or_fin_step_classifier p g s = cl_other) → bind_other_block p g → bind_other_block p g ≝
     230  λp,g,x.m_map … (other_block_cons … x).
     231
     232let rec bind_pred_aux B X (P : X → Prop) (c : bind_new B X) on c : Prop ≝
     233  match c with
     234  [ bret x ⇒ P x
     235  | bnew f ⇒ ∀b.bind_pred_aux B X P (f b)
     236  ].
     237
     238let rec bind_pred_inj_aux B X (P : X → Prop) (c : bind_new B X) on c :
     239  bind_pred_aux B X P c → bind_new B (Σx.P x) ≝
     240  match c return λx.bind_pred_aux B X P x → bind_new B (Σx.P x) with
     241  [ bret x ⇒ λprf.return «x, prf»
     242  | bnew f ⇒ λprf.bnew … (λx.bind_pred_inj_aux B X P (f x) (prf x))
     243  ].
     244
     245definition bind_pred ≝ λB.
     246  mk_InjMonadPred (BindNew B)
     247    (mk_MonadPred ?
     248      (bind_pred_aux B)
     249      ???)
     250    (λX,P,c_sig.bind_pred_inj_aux B X P c_sig (pi2 … c_sig))
     251    ?.
     252[ #X #P #Q #H #y elim y [ #x @H | #f #IH #G #b @IH @G]
     253| #X #Y #Pin #Pout #m elim m [#x | #f #IH] #H #g #G [ @G @H | #b @(IH … G) @H]
     254| #X #P #x #Px @Px
     255| #X #P * #m elim m [#x | #f #IH] #H [ % | @bnew_proper #b @IH]
     256]
     257qed.
     258
     259definition bind_seq_block_append :
     260  ∀p,g,is_seq.(Σb : bind_seq_block p g true.bind_pred ? (λb.step_classifier p g (\snd b) = cl_other) b) →
     261  bind_seq_block p g is_seq → bind_seq_block p g is_seq ≝
     262  λp,g,is_seq,b1,b2.
     263    !«p, prf» ← mp_inject … b1;
     264    !〈post, last〉 ← b2;
     265    return 〈\fst p @ «\snd p, prf» :: post, last〉.
     266
     267definition bind_other_block_append :
     268  ∀p,g.(Σb : bind_other_block p g.bind_pred ?
     269    (λx.block_classifier ?? x = cl_other) b) →
     270  bind_other_block p g → bind_other_block p g ≝
     271  λp,g,b1.m_bin_op … (other_block_append ??) (mp_inject … b1).
     272
     273interpretation "bind seq block cons" 'cons x b = (bind_seq_block_cons ??? x b).
     274interpretation "bind other block cons" 'vcons x b = (bind_other_block_cons ?? x b).
     275interpretation "bind seq block append" 'append b1 b2 = (bind_seq_block_append ??? b1 b2).
     276interpretation "bind other block append" 'vappend b1 b2 = (bind_other_block_append ?? b1 b2).
     277
     278let rec instantiates_to B X
     279  (b : bind_new B X) (l : list B) (x : X) on b : Prop ≝
    67280  match b with
    68281  [ bret B ⇒
    69282    match l with
    70     [ nil ⇒ B = b'
    71     | cons _ _ ⇒ False
     283    [ nil ⇒ x = B
     284    | _ ⇒ False
    72285    ]
    73286  | bnew f ⇒
     
    75288    [ nil ⇒ False
    76289    | cons r l' ⇒
    77       is_block_instance p g ty (f r) l' b'
     290      instantiates_to B X (f r) l' x
    78291    ]
    79292  ].
    80293
    81 lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'.
    82   is_block_instance p globals SEQ b1 l1 b1' →
    83   is_block_instance p globals ty b2 l2 b2' →
    84   is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2').
    85 #p#globals#ty #b1 elim b1
    86 [ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *]
    87 normalize in ⊢ (%→?);
     294lemma instantiates_to_bind_pred :
     295  ∀B,X,P,b,l,x.instantiates_to B X b l x → bind_pred B P b → P x.
     296#B #X #P #b elim b
     297[ #x * [ #y #EQ >EQ normalize // | #hd #tl #y *]
     298| #f #IH * [ #y * | #hd #tl normalize #b #H #G @(IH … H) @G ]
     299]
     300qed.
     301
     302lemma seq_block_append_proof_irr :
     303  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
     304    seq_block_append p g b1 b2 = seq_block_append p g b1' b2.
     305#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
     306qed.
     307
     308lemma other_block_append_proof_irr :
     309  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
     310  other_block_append p g b1 b2 = other_block_append p g b1' b2.
     311#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
     312qed.
     313
     314(*
     315lemma is_seq_block_instance_append : ∀p,g,is_seq.
     316  ∀B1.
     317  ∀B2 : bind_seq_block p g is_seq.
     318  ∀l1,l2.
     319  ∀b1 : Σb.is_safe_block p g b.
     320  ∀b2 : seq_block p g.
     321  instantiates_to ? (seq_block p g) B1 l1 (pi1 … b1) →
     322  instantiates_to ? (seq_block p g) B2 l2 b2 →
     323  instantiates_to ? (seq_block p g) (B1 @ B2) (l1 @ l2) (b1 @ b2).
     324#p #g * #B1 elim B1 -B1
     325[ #B1 | #f1 #IH1 ]
     326#B1prf whd in B1prf;
     327#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
     328whd in ⊢ (%→?);
    88329[ @IH1
    89 | #EQ destruct(EQ) lapply b2' -b2' lapply l2 -l2 elim b2
    90   [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *]
    91   normalize in ⊢ (%→?); [2: //] #H2
    92   change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd
    93   @(IH2 … H2)
     330| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
     331  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
     332  whd in ⊢ (%→?);
     333  [ @IH2
     334  | #EQ' whd destruct @seq_block_append_proof_irr %
     335  ]
    94336]
    95337qed.
    96338
    97 definition tunnel_step : ∀p,g.codeT p g → relation (code_point p) ≝
    98   λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y.
    99 
    100 notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}.
    101 notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}.
    102 interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y).
    103 
    104 let rec tunnel_through p g (c : codeT p g) x through y on through : Prop ≝
    105   match through with
    106   [ nil ⇒ x = y
    107   | cons hd tl ⇒ x ~~> hd in c ∧ tunnel_through … hd tl y
    108   ].
    109 
    110 definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y.
    111 
    112 notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}.
    113 notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}.
    114 interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y).
    115 
    116 lemma tunnel_refl : ∀p,g.∀c : codeT p g.reflexive ? (tunnel p g c).
    117 #p #g #c #x %{[]} % qed.
    118 
    119 lemma tunnel_trans : ∀p,g.∀c : codeT p g.
    120   transitive ? (tunnel p g c).
    121 #p#g#c #x#y#z * #l1 #H1 * #l2 #H2 %{(l1@l2)}
    122 lapply H1 -H1 lapply x -x elim l1 -l1
    123 [ #x #H1 >H1 @H2
    124 | #hd #tl #IH #x * #H11 #H12
    125   %{H11} @IH @H12
    126 ] qed.
    127  
    128 definition tunnel_plus ≝ λp,g.λc : codeT p g.λx,y.
    129   ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c.
    130 
    131 notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}.
    132 notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}.
    133 interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y).
    134 
    135 lemma tunnel_plus_to_star : ∀p,g.∀c : codeT p g.∀x,y.x ~~>^+ y in c → x ~~>^* y in c.
    136 #p #g #c #x #y * #mid * #H1 * #through #H2 %{(mid :: through)}
    137 %{H1 H2} qed.
    138 
    139 lemma tunnel_plus_trans : ∀p,g.∀c : codeT p g.transitive ? (tunnel_plus p g c).
    140 #p #g #c #x #y #z * #mid * #H1 #H2
    141 #H3 %{mid} %{H1} @(tunnel_trans … H2) /2 by tunnel_plus_to_star/
    142 qed.
    143 
    144 lemma tunnel_tunnel_plus : ∀p,g.∀c : codeT p g.∀x,y,z.
    145   x ~~>^* y in c → y ~~>^+ z in c → x ~~>^+ z in c.
    146 #p #g #c #x #y #z * #through
    147 lapply x -x elim through
    148 [ #x #H1 >H1 //
    149 | #hd #tl #IH #x * #H1 #H2 #H3
    150   %{hd} %{H1} @(tunnel_trans ???? y)
    151   [ %{tl} assumption | /2 by tunnel_plus_to_star/]
     339lemma is_other_block_instance_append : ∀p,g.
     340  ∀B1 : Σb.bind_pred ? (λx.block_classifier p g x = cl_other) b.
     341  ∀B2 : bind_other_block p g.
     342  ∀l1,l2.
     343  ∀b1 : Σb.block_classifier p g b = cl_other.
     344  ∀b2 : other_block p g.
     345  instantiates_to ? (other_block p g) B1 l1 (pi1 … b1) →
     346  instantiates_to ? (other_block p g) B2 l2 b2 →
     347  instantiates_to ? (other_block p g) (B1 @@ B2) (l1 @ l2) (b1 @@ b2).
     348#p #g * #B1 elim B1 -B1
     349[ #B1 | #f1 #IH1 ]
     350#B1prf whd in B1prf;
     351#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
     352whd in ⊢ (%→?);
     353[ @IH1
     354| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
     355  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
     356  whd in ⊢ (%→?);
     357  [ @IH2
     358  | #EQ' whd destruct @other_block_append_proof_irr %
     359  ]
    152360]
    153361qed.
    154362
    155 lemma tunnel_plus_tunnel : ∀p,g.∀c : codeT p g.∀x,y,z.
    156   x ~~>^+ y in c → y ~~>^* z in c → x ~~>^+ z in c.
    157 #p #g #c #x #y #z * #mid * #H1 #H2 #H3 %{mid} %{H1}
    158 @(tunnel_trans … H2 H3)
    159 qed.
    160 
    161 let rec seq_list_in_code (p : params) g (c : codeT p g)
    162   src l dst on l : Prop ≝
    163   match l with
     363lemma other_fin_step_has_one_label :
     364  ∀p,g.∀s:(Σs.fin_step_classifier p g s = cl_other).
     365  match fin_step_labels ?? s with
     366  [ nil ⇒ False
     367  | cons _ tl ⇒
     368    match tl with
     369    [ nil ⇒ True
     370    | _ ⇒ False
     371    ]
     372  ].
     373#p #g ** [#lbl || #ext]
     374normalize
     375[3: cases (ext_fin_step_flows p ext)
     376  [* [2: #lbl' * [2: #lbl'' #tl']]] normalize nodelta ]
     377#EQ destruct %
     378qed.
     379
     380definition label_of_other_fin_step : ∀p,g.
     381  (Σs.fin_step_classifier p g s = cl_other) → label ≝
     382λp,g,s.
     383match fin_step_labels p ? s return λx.match x with [ nil ⇒ ? | cons _ tl ⇒ ?] → ? with
     384[ nil ⇒ Ⓧ
     385| cons lbl tl ⇒ λ_.lbl
     386] (other_fin_step_has_one_label p g s).
     387
     388(*
     389definition point_seq_transition : ∀p,g.codeT p g →
     390  code_point p → code_point p → Prop ≝
     391  λp,g,c,src,dst.
     392  match stmt_at … c src with
     393  [ Some stmt ⇒ match stmt with
     394    [ sequential sq nxt ⇒
     395      point_of_succ … src nxt = dst
     396    | final fn ⇒
     397      match fin_step_labels … fn with
     398      [ nil ⇒ False
     399      | cons lbl tl ⇒
     400        match tl with
     401        [ nil ⇒ point_of_label … c lbl = Some ? dst
     402        | _ ⇒ False
     403        ]
     404      ]
     405    ]
     406  | None ⇒ False
     407  ].
     408
     409lemma point_seq_transition_label_of_other_fin_step :
     410  ∀p,c,src.∀s : (Σs.fin_step_classifier p s = cl_other).∀dst.
     411  stmt_at ?? c src = Some ? s →
     412  point_seq_transition p c src dst →
     413  point_of_label … c (label_of_other_fin_step p s) = Some ? dst.
     414#p #c #src ** [#lbl || #ext] #EQ1
     415#dst #EQ2
     416whd in match point_seq_transition; normalize nodelta
     417>EQ2 normalize nodelta whd in ⊢ (?→??(????%)?);
     418[#H @H | * ]
     419lapply (other_fin_step_has_one_label ? «ext,?»)
     420cases (fin_step_labels p ? ext) normalize nodelta [*]
     421#hd * normalize nodelta [2: #_ #_ *] *
     422#H @H
     423qed.
     424
     425lemma point_seq_transition_succ :
     426  ∀p,c,src.∀s,nxt.∀dst.
     427  stmt_at ?? c src = Some ? (sequential ?? s nxt) →
     428  point_seq_transition p c src dst →
     429  point_of_succ … src nxt = dst.
     430#p #c #src #s #nxt #dst #EQ
     431whd in match point_seq_transition; normalize nodelta
     432>EQ normalize nodelta #H @H
     433qed.
     434*)
     435
     436definition if_other : ∀p,g.∀A : Type[2].seq_or_fin_step p g → A → A → A ≝
     437  λp,g,A,c.match seq_or_fin_step_classifier p g c with
     438  [ cl_other ⇒ λx,y.x
     439  | _ ⇒ λx,y.y
     440  ].
     441
     442definition other_step_in_code ≝
     443  λp,g.
     444  λc : codeT p g.
     445  λsrc : code_point p.
     446  λs : seq_or_fin_step p g.
     447  match s return λx.if_other p g ? x (code_point p) unit → Prop with
     448  [ inl s'' ⇒ λdst.∃n.stmt_at … c src = Some ? (sequential … s'' n) ∧ ?
     449  | inr s'' ⇒ λdst.stmt_at … c src = Some ? (final … s'') ∧ ?
     450  ].
     451  [ whd in dst; cases (seq_or_fin_step_classifier ???) in dst;
     452    normalize nodelta [1,2,3: #_ @True |*: #dst
     453      @(point_of_succ … src n = dst)]
     454  | whd in dst;
     455    lapply dst -dst
     456    lapply (refl … (seq_or_fin_step_classifier ?? (inr … s'')))
     457    cases (seq_or_fin_step_classifier ?? (inr … s'')) in ⊢ (???%→%);
     458    normalize nodelta
     459    [1,2,3: #_ #_ @True
     460    |*: #EQ #dst
     461      @(point_of_label … c (label_of_other_fin_step p g «s'', EQ») = Some ? dst)
     462    ]
     463  ]
     464qed.
     465
     466definition if_other_sig :
     467  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
     468  if_other p g ? s B C → B ≝
     469  λp,g,B,C.?.
     470  ** #s whd in match (if_other ??????);
     471  cases (seq_or_fin_step_classifier ???) normalize nodelta #EQ destruct(EQ)
     472  #x @x
     473qed.
     474
     475definition if_other_block_sig :
     476  ∀p,g.∀B,C : Type[0].∀b : Σb.block_classifier p g b = cl_other.
     477  if_other p g ? (\snd b) B C → B ≝
     478  λp,g,B,C.?.
     479  ** #l #s
     480  #prf #x @(if_other_sig ???? «s, prf» x)
     481qed.
     482
     483coercion other_sig_to_if nocomposites:
     484  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
     485  ∀x : if_other p g ? s B C.B ≝ if_other_sig
     486  on _x : if_other ?? Type[0] ??? to ?.
     487
     488coercion other_block_sig_to_if nocomposites:
     489  ∀p,g.∀B,C : Type[0].∀s : Σs.block_classifier p g s = cl_other.
     490  ∀x : if_other p g ? (\snd s) B C.B ≝ if_other_block_sig
     491  on _x : if_other ?? Type[0] (\snd ?) ?? to ?.
     492
     493let rec other_list_in_code p g (c : codeT p g)
     494  src
     495  (b : list (Σs.seq_or_fin_step_classifier p g s = cl_other))
     496  dst on b : Prop ≝
     497  match b with
    164498  [ nil ⇒ src = dst
    165   | cons hd tl ⇒
    166     ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧
    167        seq_list_in_code p g c (point_of_succ … src n) tl dst
    168   ].
    169 
    170 (*
    171 definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝
    172   λp,g,b.\fst b @ [\snd b].
    173 
    174 coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝
    175   seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??).
    176 *)
    177 
    178 definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?.
    179  * * /2/
    180 qed.
    181 
    182 definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
    183   code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝
    184   λp,g.λc : codeT p g.λty,src,b,dst.
    185   ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
    186   match ty
    187   return λx.stmt_type_if ? x ??? →
    188     stmt_type_if ? x ? unit_deqset → Prop
    189   with
    190   [ SEQ ⇒ λs,dst.
    191       ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
    192          point_of_succ … mid n = dst
    193   | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s)
    194   ] (\snd b) dst.
    195  
     499  | cons hd tl ⇒ ∃mid.
     500    other_step_in_code p g c src hd mid ∧ other_list_in_code p g c mid tl dst
     501  ].
    196502
    197503notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
     
    201507  @{'block_in_code $c $x $B $y}.
    202508
    203 interpretation "block cont in code" 'block_in_code c x B y =
    204   (block_cont_in_code ?? c ? x B y).
    205 
    206 lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z.
    207   seq_list_in_code p g c x l1 y →
    208   seq_list_in_code p g c y l2 z →
    209   seq_list_in_code p g c x (l1@l2) z.
    210 #p#g#c#x#l1 lapply x -x
    211 elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?);
    212 [ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G)
    213 | #EQ destruct(EQ) //
    214 ]
    215 qed.
    216 
    217 lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x.
    218   ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z.
    219   x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c.
    220 #p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta
    221 #l1 #s1 #y * #l2 #s2 #z * normalize nodelta
    222 #mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3
    223 %{mid2} %
    224 [ whd in match (〈?,?〉@?);
    225   @(seq_list_in_code_append … H1)
    226   %{n} %{EQ1} >EQ2 assumption
    227 | assumption
    228 ]
    229 qed.
    230 
     509interpretation "list in code" 'block_in_code c x B y =
     510  (other_list_in_code ?? c x B y).
     511
     512definition other_block_in_code : ∀p,g.codeT p g →
     513  code_point p → ∀b : other_block p g.
     514    if_other … (\snd b) (code_point p) unit → Prop ≝
     515  λp,g,c,src,b,dst.
     516  ∃mid.src ~❨\fst b❩~> mid in c ∧
     517  other_step_in_code p g c mid (\snd b) dst.
     518
     519interpretation "block in code" 'block_in_code c x B y =
     520  (other_block_in_code ?? c x B y).
     521
     522lemma other_list_in_code_append : ∀p,g.∀c : codeT p g.
     523  ∀x.∀b1 : list ?.
     524  ∀y.∀b2 : list ?.∀z.
     525  x ~❨b1❩~> y in c→ y ~❨b2❩~> z in c → x ~❨b1@b2❩~> z in c.
     526#p#g#c#x#b1 lapply x -x
     527elim b1 [2: ** #hd #hd_prf #tl #IH] #x #y #b2 #z
     528[3: #EQ normalize in EQ; destruct #H @H]
     529* #mid * normalize nodelta [ *#n ] #H1 #H2 #H3
     530whd normalize nodelta %{mid}
     531%{(IH … H2 H3)}
     532[ %{n} ] @H1
     533qed.
     534
     535lemma other_block_in_code_append : ∀p,g.∀c : codeT p g.∀x.
     536  ∀B1 : Σb.block_classifier p g b = cl_other.
     537  ∀y.
     538  ∀B2 : other_block p g.
     539  ∀z.
     540  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c →
     541  x ~❨B1@@B2❩~> z in c.
     542#p#g#c #x ** #hd1 *#tl1 #tl1prf
     543#y * #hd2 #tl2 #z
     544* #mid1 * #H1 #H2
     545* #mid2 * #G1 #G2
     546%{mid2} %{G2}
     547whd in match (\fst ?);
     548@(other_list_in_code_append … H1)
     549%{y} %{H2 G1}
     550qed.
     551
     552(*
    231553definition instr_block_in_function :
    232   ∀p,g.∀fn : joint_internal_function g p.∀ty.
    233     instr_block p g ty →
     554  ∀p : evaluation_params.∀fn : joint_internal_function (globals p) p.
    234555    code_point p →
     556    ∀b : bind_other_block p.
    235557    ? → Prop ≝
    236  λp,g,fn,ty,B,src,dst.
     558 λp,fn,src,B,dst.
    237559 ∃vars,B'.
    238560  All ? (In ? (joint_if_locals … fn)) vars ∧
    239   is_block_instance … B vars B' ∧
     561  instantiates_to … B vars B' ∧
    240562  src ~❨B'❩~> dst in joint_if_code … fn.
    241563
    242 interpretation "instr block in function" 'block_in_code fn x B y =
    243   (instr_block_in_function ?? fn ? B x y).
     564interpretation "bind block in function" 'block_in_code fn x B y =
     565  (instr_block_in_function ? fn x B y).
    244566
    245567lemma instr_block_in_function_trans :
    246   ∀p,g.∀fn : joint_internal_function g p.∀ty,src.
    247   ∀B1 : instr_block p g SEQ.
    248   ∀mid.∀B2 : instr_block p g ty.∀dst.
    249   src ~❨B1❩~> mid in fn →
     568  ∀p,fn,src.
     569  ∀B1 : ΣB.bind_pred ? (λb.block_classifier p b = cl_other) B.
     570  ∀mid.
     571  ∀B2 : bind_other_block p.
     572  ∀dst.
     573  src ~❨B1❩~> Some ? mid in fn →
    250574  mid ~❨B2❩~> dst in fn →
    251   src ~❨B1@B2❩~> dst in fn.
    252 #p#g#fn#ty#src#B1#mid#B2#dst
     575  src ~❨B1@@B2❩~> dst in fn.
     576#p#fn#src*#B1#B1prf#mid#B2#dst
    253577* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
    254578* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
    255 %{(vars1@vars2)} %{(b1 @ b2)}
    256 /4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/
    257 qed.
     579%{(vars1@vars2)} %{(«b1,instantiates_to_bind_pred … b1B1 B1prf» @@ b2)}
     580/4 by All_append, conj, is_other_block_instance_append, other_block_in_code_append/
     581qed.
     582*)
     583*)
     584*)
  • src/utilities/bindLists.ma

    r1882 r2155  
    1818
    1919definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
    20   λB,E,e,l.[e] @@ l.
    21 
     20  λB,E,e.m_map … (cons … e).
    2221interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
    2322
     
    4342  (bcompile U R (list E) fresh (e ::: bl2)) ≅
    4443    ! l ← bcompile … fresh bl2 ; return (e :: l).
    45       #U#R#E#fresh#e#bl2 #u
    46       >bcompile_append normalize //
     44      #U#R#E#fresh#e#bl2 #u @bcompile_bbind
    4745qed.
Note: See TracChangeset for help on using the changeset viewer.