Changeset 3570


Ignore:
Timestamp:
Jun 17, 2015, 5:49:19 PM (4 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3561 r3570  
    8989lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,l_p,i1,i2.(i1 = i2 → P true) →
    9090(i1 ≠ i2 → P false) → P (eq_instructions p l_p i1 i2).
    91 #P #p #l_p #i1 elim i1
    92 [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
     91#P #p #l_p #i1 lapply P -P elim i1
     92[ #P * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9393  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
    94 | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/
     94| #rt #P * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/
    9595  #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //]
    9696  [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9797  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
    98 | #seq * [| #lbl] #i #IH * normalize
     98| #seq * [| #lbl] #i #IH #P * normalize
    9999  [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c
    100100  |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3]
  • LTS/mono_stack.ma

    r3566 r3570  
    1919@hide_prf ** % // qed.
    2020
    21 definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqNat).
     21definition mono_stack_store_t ≝ DeqProd (DeqSet_List DeqNat) (DeqProd DeqNat DeqNat).
    2222
    2323definition mono_stack_state_params:state_params≝
     
    3636λc,s.match c with
    3737[ push_var x ⇒ 
    38                 ! n ← read_frame (\fst s) (to_shift+x) (\snd s);
     38                ! n ← read_frame (\fst s) (to_shift+x) (\fst (\snd s));
    3939                return mono_push s n
    4040| push_const n ⇒ return mono_push s n
     
    4545].
    4646
     47check assign_frame
    4748
    4849definition mono_stack_eval_seq: (seq_instr mono_stack_state_params)→
    49 (store_type mono_stack_state_params)→ option (store_type mono_stack_state_params)
     50mono_stack_store_t→ option mono_stack_store_t
    5051λi,s.match i with
    51 [ pop_Ass v ⇒ ! 〈val1,st1〉 ← mono_pop s; return 〈(assign_frame (\fst s) (to_shift +v) (\snd s) val1),(\snd s)〉
     52[ pop_Ass v ⇒ ! 〈val1,st1〉 ← mono_pop s; ! new_env ← (assign_frame (\fst s) (to_shift +v) (\fst (\snd s)) val1); return 〈new_env,(\snd s)〉
    5253| push c ⇒ mono_eval_combinators c s
     54| popreg v ⇒ ! x ← assign_frame (\fst s) (to_shift +v) (\fst (\snd s)) (\snd (\snd s)); return 〈x,(\snd s)〉
    5355].
    5456
     
    6668    !〈exp_val,st1〉 ← mono_pop st;
    6769    let new_fp ≝ (|(\fst st1)|) in
    68     let st2 ≝ mono_push st1 (\snd st1) in
     70    let st2 ≝ mono_push st1 (\fst (\snd st)) in
    6971    let st3 ≝ mono_push st2 O in
    7072    let st4 ≝ mono_push st3 exp_val in
    7173    let new_frame ≝ list_n … O (pred (to_shift + (f_pars … sgn))) in
    72     return 〈new_frame @ (\fst st4),new_fp〉.
     74    return 〈new_frame @ (\fst st4),〈new_fp,(\snd(\snd st))〉〉.
    7375
    7476let rec reduce_list (A : Type[0]) (l : list A) (n : ℕ) on l : option (list A) ≝
     
    99101definition mono_stack_return_call:mono_stack_store_t → (option mono_stack_store_t)≝
    100102λs.!〈n,st1〉 ← mono_pop s;
    101    ! new_fp ← read_frame (\fst st1) (\snd st1) O; (* 0 leggi il frame pointer precedente *)
    102    ! st2 ← mono_pop_frame st1 (\snd st1) ;(* 1: accorciare la lista fino a diventare lunga come \snd st1 ovvero il frame pointer corrente *)
     103   ! new_fp ← read_frame (\fst st1) (\fst (\snd s)) O; (* 0 leggi il frame pointer precedente *)
     104   ! st2 ← mono_pop_frame st1 (\fst (\snd s)) ;(* 1: accorciare la lista fino a diventare lunga come \snd st1 ovvero il frame pointer corrente *)
    103105   let st3 ≝  mono_push st2 n in (* 2: pushare il valore n *)
    104    return 〈(\fst st3),new_fp〉. (* 3: ritornare lo stato con il nuovo fp *)
     106   return 〈(\fst st3),〈new_fp,(\snd(\snd s))〉〉. (* 3: ritornare lo stato con il nuovo fp *)
    105107
    106 definition mono_stack_init_store ≝ λn : ℕ.〈list_n … O  (to_shift + n),O〉.
     108definition mono_stack_init_store ≝ λn : ℕ.〈list_n … O  (to_shift + n),〈O,O〉〉.
    107109
    108110definition mono_stack_sem_state_params : ℕ → sem_state_params mono_stack_state_params ≝
  • LTS/stack.ma

    r3566 r3570  
    4949inductive stack_seq:Type[0]≝
    5050| pop_Ass: variable → stack_seq
    51 | push : guard_combinators → stack_seq.
     51| push : guard_combinators → stack_seq
     52| popreg : variable → stack_seq.
    5253
    5354definition eq_stack_seq : stack_seq → stack_seq → bool ≝
     
    5556[ pop_Ass v1 ⇒ λy.match y with [pop_Ass v2 ⇒ eqb v1 v2 | _ ⇒ false ]
    5657| push c1 ⇒ λy.match y with [push c2 ⇒ eq_guard_combinator c1 c2 | _ ⇒ false]
     58| popreg v⇒ λy.match y with [popreg v' ⇒ eqb v v' | _ ⇒ false]
    5759].
    5860
     
    6062∀x1,x2.(x1 = x2 → P true) → (x1 ≠ x2 → P false) →
    6163P(eq_stack_seq x1 x2).
    62 #P * [#v1 | #c1] * [1,3: #v2 |*: #c2] #H1 #H2 try(@H2 % #EQ destruct)
     64#P * [#v1 | #c1 | #v1 ] * [1,4,7: #v2 |2,5,8: #c2 |*: #v2] #H1 #H2 try(@H2 % #EQ destruct)
    6365[ normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
    6466| whd in match eq_stack_seq; normalize nodelta @eq_guard_combinator_elim /2/
    6567 * #H @H2 % #EQ destruct @H %
     68| normalize @(eqb_elim … v1 v2) [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
    6669]
    6770qed.
     
    7881 
    7982definition stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality)
    80  (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) variable (mk_DeqSet unit (λ_.λ_.true) ?).
     83 (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
    8184@hide_prf ** % // qed.
    8285
     
    8992λs,n.match \fst s with
    9093[nil ⇒ None ?
    91 |cons x xs ⇒ return 〈〈(n::(\fst x)),\snd x〉 :: xs,\snd s〉
     94|cons x xs ⇒ return 〈(n::x) :: xs,\snd s〉
    9295].
    9396
     
    9598λs.match \fst s with
    9699[nil ⇒ None ?
    97 |cons x xs ⇒ match \fst x with
     100|cons x xs ⇒ match x with
    98101             [ nil ⇒ None ?
    99              | cons y ys ⇒ return 〈y,〈〈ys,\snd x〉::xs,\snd s〉〉
     102             | cons y ys ⇒ return 〈y,〈ys::xs,\snd s〉〉
    100103             ]
    101104             ].
     
    118121[ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1
    119122| push c ⇒ eval_combinators c s
     123| popreg v ⇒ frame_assign_var s (to_shift +v) (\snd (\snd s))
    120124].
    121125
     
    137141λsgn.λvar,st.
    138142    !〈n,st1〉 ← pop st; 
    139     frame_assign_var 〈(〈list_n … O (pred (to_shift + (f_pars … sgn))),var〉::(\fst st1)),(\snd st1)〉 to_shift n.
     143    frame_assign_var 〈(list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st1),(\snd st1)〉 to_shift n.
    140144
    141145definition stack_return_call:frame_store_t→ (option frame_store_t)≝
    142146λs.match (\fst s) with
    143147[nil⇒ None ?
    144 |cons hd tl⇒ let 〈env,v〉≝ hd in
    145              !〈n,st1〉 ← pop s;
    146              frame_assign_var 〈tl,\snd s〉 v n
     148|cons hd tl⇒ !〈n,st1〉 ← pop s;
     149             return 〈tl,〈(\fst (\snd s)),n〉〉
    147150].
    148151 
    149 definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉.
     152definition stack_init_store ≝ λn : ℕ.〈[list_n … O (to_shift + n)],〈O,O〉〉.
    150153
    151154
  • LTS/variable.ma

    r3569 r3570  
    4444definition read_frame ≝ λenv:activation_frame.λv:variable.λfp : ℕ.nth_opt … (|env| -v -fp -1) env.
    4545
     46(*
    4647lemma read_frame_assign_frame_hit:
    4748 ∀env,v,fp,n.
    4849  read_frame (assign_frame env v fp n) v fp = return n.
    4950 normalize
     51*)
    5052
    5153let rec frame_sem_expr (env:activation_frame) (e: expr) on e : (option nat) ≝
     
    107109match \fst env with
    108110[ nil ⇒ None ?
    109 | cons hd tl ⇒ return 〈(assign_frame hd v (\fst (\snd env)) n :: tl),\snd env〉
     111| cons hd tl ⇒ ! x ← (assign_frame hd v (\fst (\snd env)) n); return ((〈x::tl,\snd env〉))
    110112].
    111113
  • LTS/variable_stack_pass.ma

    r3566 r3570  
    5353  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
    5454  match seq with
    55   [ sNop ⇒ 〈t_instr,c_bound〉
    56   | sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
     55  [ Seq_i seq' ⇒
     56     match seq' with
     57     [ sNop ⇒ 〈t_instr,c_bound〉
     58     | sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
    5759                max (get_expr_bound e) c_bound〉
     60     ]
     61  | PopReg v ⇒ 〈SEQ stack_instr_params ? (popreg v) opt_l t_instr,max (S v) c_bound〉
    5862  ]
    5963| COND cond ltrue i_true lfalse i_false instr ⇒
     
    7074| CALL f act_p opt_l instr ⇒
    7175  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
    72   〈list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l t_instr),
    73    max (get_expr_bound (\snd act_p)) c_bound〉
     76  〈list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr),
     77   max (get_expr_bound act_p) c_bound〉
    7478| IO lin io lout instr ⇒ ?
    7579].
     
    7781qed.
    7882
    79 definition trans_var_prog : Program frame_env_params imp_instr_params flat_labels →
     83definition trans_var_prog : Program frame_env_params frame_instr_params flat_labels →
    8084(Program stack_env_params stack_instr_params flat_labels × ℕ) ≝
    8185λprog.
     
    170174∃st'.m_fold Option … eval_combinators (trans_expr e) st = return st' ∧
    171175pop st' = return 〈n,st〉.
    172 ** [| * #curr_env #var #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
     176** [| #curr_env #rem] #sp_fp #env #e #n #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
    173177lapply n -n lapply H1 -H1 lapply H2 -H2 lapply env -env elim e
    174 [ #v #env #_ #_ #n whd in ⊢ (??%% → ?); #H %{(〈〈n::env,var〉::rem,sp_fp〉)} % try %
     178[ #v #env #_ #_ #n whd in ⊢ (??%% → ?); #H %{(〈(n::env)::rem,sp_fp〉)} % try %
    175179  whd in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
    176180  whd in match frame_current_env; normalize nodelta whd in match option_hd; normalize nodelta
    177181  >m_return_bind whd in match read_frame; normalize nodelta >H %
    178 | #n #env #_ #_ #m whd in ⊢ (??%% → ?); #EQ destruct %{(〈〈m::env,var〉::rem,sp_fp〉)} %%
     182| #n #env #_ #_ #m whd in ⊢ (??%% → ?); #EQ destruct %{(〈(m::env)::rem,sp_fp〉)} %%
    179183|*: #e1 #e2 #IH1 #IH2 #env #H1 #H2 #n change with (m_bind ?????) in ⊢ (??%? → ?);
    180184  #H cases(bind_inversion ????? H) -H #n1 * #EQn1
    181185  #H cases(bind_inversion ????? H) -H #n2 * #EQn2
    182186  whd in ⊢ (??%% → ?); #EQ destruct
    183   [ %{(〈〈(n1 + n2)::env,var〉::rem,sp_fp〉)} | %{(〈〈(n1 - n2)::env,var〉::rem,sp_fp〉)} ]
     187  [ %{(〈((n1 + n2)::env)::rem,sp_fp〉)} | %{(〈((n1 - n2)::env)::rem,sp_fp〉)} ]
    184188  >m_fold_append cases(IH1 … EQn1) // [2,4: cases(All_inv_append … H1) //] #st1 * #EQst1 #EQpop1 >EQst1
    185189  >m_return_bind >m_fold_append cases(IH2 … (n1 :: env))
     
    189193  |4,9:
    190194  ]
    191   #st2 * #EQst2 #EQpop2 cases st1 in EQst1 EQpop1; * [2,4: * #env' #var' #rem'] #fp_sp' #EQst1
     195  #st2 * #EQst2 #EQpop2 cases st1 in EQst1 EQpop1; * [2,4: #env' #rem'] #fp_sp' #EQst1
    192196  [3,4: whd in ⊢ (??%% → ?); #EQ destruct ] cases env' in EQst1; [2,4: #val1 #env''] #EQst1
    193197  whd in ⊢ (??%% → ?); #EQ destruct >EQst2 >m_return_bind % [2,4: %] whd in ⊢ (??%?);
     
    202206∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧
    203207pop st' = Some ? 〈if b then 1 else O,st〉.
    204 ** [| * #curr_env #var #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
     208** [| #curr_env #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
    205209lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c
    206210[ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
    207211  #n * #EQn #H cases(bind_inversion ????? H) -H #m * #EQm whd in ⊢ (??%% → ?); #EQ destruct
    208   %{(〈〈(if (eqb n m )then 1 else O) :: env,var〉::rem,sp_fp〉)} >m_fold_append
     212  %{(〈((if (eqb n m )then 1 else O) :: env)::rem,sp_fp〉)} >m_fold_append
    209213  cases(eval_exp_ok … EQn) //
    210   [2: @(〈〈env,var〉::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
     214  [2: @(〈env::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
    211215  #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind % // >m_fold_append
    212   cases st1 in EQst1 EQpop1; * [| * * [| #m' #env'] #var #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?);
     216  cases st1 in EQst1 EQpop1; * [| * [| #m' #env'] #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?);
    213217  #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm))
    214   [2: @(〈〈n::env,var〉::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) //
     218  [2: @(〈(n::env)::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) //
    215219  |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //]
    216220  |6: cases(All_inv_append … H) // |7: // |8:]
     
    219223| #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?);
    220224  #H cases(bind_inversion ????? H) -H #b1 * #EQb1 whd in ⊢ (??%% → ?); #EQ destruct
    221   %{(〈〈(if (if b1 then false else true) then 1 else O) :: env,var〉::rem,sp_fp〉)} % //
     225  %{(〈((if (if b1 then false else true) then 1 else O) :: env)::rem,sp_fp〉)} % //
    222226  >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind
    223227  change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.