Changeset 3566 for LTS


Ignore:
Timestamp:
Jun 17, 2015, 4:23:08 PM (4 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3565 r3566  
    8181@hide_prf ** % // qed.
    8282
     83definition stack_env_params ≝ mk_env_params ℕ.
     84
    8385definition stack_state_params:state_params≝
    84 mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
     86mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
    8587
    8688definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝
     
    125127
    126128
     129let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
     130match n with
     131[ O ⇒ nil ?
     132| S m ⇒ a :: list_n … a m
     133].
     134
    127135definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params →
    128136frame_store_t → (option frame_store_t)≝
    129 λsgn,var,st.
    130   match sgn with
    131   [ mk_signature fun fpt rt ⇒
    132     !〈n,st1〉 ← pop st;
    133     frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n
    134   ].
     137λsgn.λvar,st.
     138    !〈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.
    135140
    136141definition stack_return_call:frame_store_t→ (option frame_store_t)≝
     
    142147].
    143148 
     149definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉.
    144150
    145151
    146 definition stack_sem_state_params : sem_state_params stack_state_params ≝ mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
    147 (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) frame_init_store.
     152definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝
     153λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
     154(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
    148155
    149156  (* Abitare tipo Instructions *)
     
    154161
    155162
    156 definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).
     163definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).
  • LTS/variable.ma

    r3562 r3566  
    5252
    5353
    54 definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)
     54definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
    5555
    5656definition frame_env_params ≝ mk_env_params unit.
    5757
     58inductive frame_seq_i : Type[0] ≝
     59| Seq_i : seq_i → frame_seq_i
     60| PopReg : variable → frame_seq_i.
     61
     62definition eq_frame_seq_i : frame_seq_i → frame_seq_i → bool ≝
     63λx,y.
     64match x with
     65[ Seq_i s ⇒ match y with [Seq_i s' ⇒ seq_i_eq s s' | _ ⇒ false ]
     66| PopReg v ⇒ match y with [PopReg v' ⇒ eqb v v' | _ ⇒ false]
     67].
     68
     69definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?.
     70@hide_prf cases daemon qed.
     71
     72definition frame_instr_params : instr_params ≝
     73mk_instr_params ? ? ? ? ? ?.
     74[ @DeqFrameSeqI
     75|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
     76|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
     77|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
     78|@(DeqProd variable DeqExpr)
     79|@DeqExpr].qed.
     80
    5881definition frame_state_params:state_params≝
    59 mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
     82mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
    6083
    61 definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd.
     84definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return hd.
    6285
    6386definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
    6487match \fst env with
    6588[ nil ⇒ None ?
    66 | cons hd tl ⇒ let 〈e,var〉 ≝ hd in return 〈(〈assign_frame e v (\fst (\snd env)) n,var〉 :: tl),\snd env〉
     89| cons hd tl ⇒ return 〈(assign_frame hd v (\fst (\snd env)) n :: tl),\snd env〉
    6790].
    6891
    6992definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝
    7093λi,s.match i with
    71 [sNop ⇒ Some ? s
    72 |sAss v e ⇒ !env ← frame_current_env … s;
    73             ! n ← frame_sem_expr env e;
    74             frame_assign_var s v n
     94[ Seq_i instr ⇒
     95   match instr with
     96   [sNop ⇒ Some ? s
     97   |sAss v e ⇒ !env ← frame_current_env … s;
     98               ! n ← frame_sem_expr env e;
     99               frame_assign_var s v n
     100   ]
     101| PopReg v ⇒ frame_assign_var s v (\snd (\snd s))
    75102].
    76103
     
    88115frame_eval_cond_cond.
    89116
    90 definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
     117definition frame_eval_call:(signature frame_state_params frame_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
    91118λsgn,e,st.
    92119    let 〈var,act_exp〉 ≝ e in
    93120    !env ← frame_current_env … st;
    94121    !n ← frame_sem_expr env act_exp;
    95     frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n.
     122    frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
    96123
    97124definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝
    98125λr,s.match (\fst s) with
    99126[nil⇒ None ?
    100 |cons hd tl⇒ let 〈env,v〉≝ hd in
    101              !n ← frame_sem_expr env r;
    102              frame_assign_var 〈tl,\snd s〉 v n
     127|cons hd tl⇒ !n ← frame_sem_expr hd r;
     128             return 〈tl,〈(\fst (\snd s)),n〉〉
    103129].
    104130 
    105 
    106 definition frame_init_store: (store_type frame_state_params)≝ 〈[〈(nil ?),O〉],〈O,O〉〉.
     131definition frame_init_store: (store_type frame_state_params)≝ 〈[(nil ?)],〈O,O〉〉.
    107132
    108133
     
    117142
    118143
    119 definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).
     144definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels).
  • LTS/variable_stack_pass.ma

    r3565 r3566  
    3232λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
    3333
    34 let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝
     34let rec get_expr_bound (e : expr) on e : ℕ ≝
     35match e with
     36[ Var v ⇒ S v
     37| Const n ⇒ O
     38| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
     39| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
     40].
     41
     42let rec get_cond_bound (c : condition) on c : ℕ ≝
     43match c with
     44[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
     45| Not c ⇒ get_cond_bound c
     46].
     47
     48let rec trans_var_instr (i : frame_Instructions) on i : (stack_Instructions × ℕ) ≝
    3549match i with
    36 [ EMPTY ⇒ EMPTY …
    37 | RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
     50[ EMPTY ⇒ 〈EMPTY …,O〉
     51| RETURN exp ⇒ 〈list_combinators_to_instructions (trans_expr exp) (RETURN … it),get_expr_bound exp〉
    3852| SEQ seq opt_l instr ⇒
     53  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
    3954  match seq with
    40   [ sNop ⇒ trans_var_instr … instr
    41   | sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l (trans_var_instr … instr))
     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),
     57                max (get_expr_bound e) c_bound〉
    4258  ]
    43 | COND cond ltrue i_true lfalse i_false instr ⇒
    44      list_combinators_to_instructions (trans_cond cond)
    45       (COND … it ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … i_false) (trans_var_instr … instr))
     59| COND cond ltrue i_true lfalse i_false instr ⇒
     60  let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in
     61  let 〈t_i_false,i_false_bound〉 ≝ trans_var_instr … i_false in
     62  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
     63  〈list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr),
     64   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))〉
    4665| LOOP cond ltrue i_true lfalse instr ⇒
    47      LOOP stack_state_params flat_labels (trans_cond … cond) ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … instr)
     66  let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in
     67  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
     68  〈LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr,
     69   max (get_cond_bound cond) (max i_true_bound c_bound)〉
    4870| CALL f act_p opt_l instr ⇒
    49      list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l (trans_var_instr … instr))
     71  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〉
    5074| IO lin io lout instr ⇒ ?
    5175].
     
    5478
    5579definition trans_var_prog : Program frame_env_params imp_instr_params flat_labels →
    56 Program frame_env_params stack_instr_params flat_labels ≝ λprog.
    57 mk_Program …
    58 (foldr … (λx,tail.(mk_env_item …
    59    (mk_signature ? stack_instr_params (f_name … (f_sig … x)) (f_pars … (f_sig … x)) it) (f_lab … x)
    60         (trans_var_instr … (f_body … x)) ) :: tail) (nil ?) (env … prog))
    61 (trans_var_instr … (main … prog)).
     80(Program stack_env_params stack_instr_params flat_labels × ℕ) ≝
     81λprog.
     82let 〈t_main,m_bound〉 ≝ trans_var_instr … (main … prog) in
     83〈(mk_Program …
     84  (foldr …
     85   (λx,tail.(let 〈t_body,bound〉 ≝ trans_var_instr … (f_body … x) in
     86     mk_env_item …       
     87     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) bound it) (f_lab … x) t_body) :: tail)
     88   (nil ?) (env … prog))
     89  t_main),m_bound〉.
    6290
    6391include "Simulation.ma".
    6492
    65 definition frame_variable_pass_rel ≝ 
    66 λprog : Program frame_state_params frame_state_params frame_state_params.
    67 let t_prog ≝ trans_var_prog prog in
    68 mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
    69  (operational_semantics stack_state_params stack_sem_state_params t_prog)
    70  (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
    71          cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
    72  (λ_.λ_.True).
     93definition frame_variable_pass_rel :
     94∀prog : Program frame_state_params frame_state_params frame_state_params.
     95∀t_prog : Program stack_env_params stack_instr_params flat_labels.
     96∀bound : ℕ.
     97relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
     98(operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝
     99λprog,t_prog,bound.
     100(mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
     101 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
     102 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = (\fst (trans_var_instr (code … s1))) ∧
     103         cont … s2 = foldr … (λx,tail. 〈(\fst x),(\fst (trans_var_instr (\snd x)))〉 :: tail) (nil ?) (cont … s1))
     104 (λ_.λ_.True)).
     105
    73106
    74107let rec expr_fv (e : expr) on e : list variable ≝
     
    81114
    82115definition good_expr ≝  λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e).
     116
     117let rec cond_fv (c : condition) on c : list variable ≝
     118match c with
     119[ Eq e1 e2 ⇒ expr_fv e1 @ expr_fv e2
     120| Not c1 ⇒ cond_fv c1
     121].
     122
     123definition good_cond ≝ λbound : ℕ.λc : condition.All … (λv.v < bound) (cond_fv c).
    83124
    84125lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e →
     
    155196qed.
    156197
    157 
     198lemma eval_cond_ok :  ∀st.∀env:activation_frame.∀c: condition.∀b.
     199to_shift ≤ |env| → good_cond (|env| - to_shift) c →
     200frame_current_env … st = return env →
     201frame_sem_condition env c = return b →
     202∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧
     203pop 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
     205lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c
     206[ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
     207  #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
     209  cases(eval_exp_ok … EQn) //
     210  [2: @(〈〈env,var〉::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
     211  #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 ⊢ (??%% → ?);
     213  #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm))
     214  [2: @(〈〈n::env,var〉::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) //
     215  |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //]
     216  |6: cases(All_inv_append … H) // |7: // |8:]
     217  #st2 * #EQst2 #EQpop2 >EQst2 >m_return_bind change with (m_bind ?????) in ⊢ (??%?);
     218  whd in match eval_combinators; normalize nodelta >EQpop2 %
     219| #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?);
     220  #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〉)} % //
     222  >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind
     223  change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
     224  >EQpop1 >m_return_bind whd in ⊢ (??%?); @eq_f @eq_f2 // cases b1 //
     225]
     226qed.
     227
     228(*
     229let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators)
     230(prf: m_fold Option … eval_combinators l st = return st')
     231*)
     232
     233definition simulation_imp_frame :
     234∀prog : Program frame_state_params frame_state_params frame_state_params.
     235∀t_prog,bound.〈t_prog,bound〉 = trans_var_prog prog →
     236simulation_conditions … (frame_variable_pass_rel prog t_prog bound) ≝
     237λprog,t_prog,bound,good_trans.
     238mk_simulation_conditions ….
     239cases daemon
     240qed.
    158241 
    159 definition simulation_imp_frame ≝
    160 λprog : Program frame_state_params frame_state_params frame_state_params.
    161 mk_simulation_conditions … (frame_variable_pass_rel prog) ???????????.
    162 cases daemon
    163 qed.
    164  
Note: See TracChangeset for help on using the changeset viewer.