Changeset 3577


Ignore:
Timestamp:
Jun 19, 2015, 6:31:59 PM (4 years ago)
Author:
sacerdot
Message:

Number of local variables computed during the first pass and then propagated.

Location:
LTS
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • LTS/frame_variable_pass.ma

    r3575 r3577  
    1919definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝
    2020λA,B,f,a,b,x.if x == a then b else f x.
     21
     22let rec get_expr_bound (e : expr) on e : ℕ ≝
     23match e with
     24[ Var v ⇒ S v
     25| Const n ⇒ O
     26| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
     27| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
     28].
     29
     30let rec get_cond_bound (c : condition) on c : ℕ ≝
     31match c with
     32[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
     33| Not c ⇒ get_cond_bound c
     34].
     35
     36let rec get_instr_bound (i : frame_Instructions) ≝
     37match i with
     38[ EMPTY ⇒ O
     39| RETURN exp ⇒ get_expr_bound exp
     40| SEQ seq opt_l instr ⇒
     41  let c_bound ≝ get_instr_bound instr in
     42  match seq with
     43  [ Seq_i seq' ⇒
     44     match seq' with [ sAss v e ⇒ max (get_expr_bound e) c_bound ]
     45  | PopReg v ⇒ max (S v) c_bound
     46  ]
     47| COND cond ltrue i_true lfalse i_false instr ⇒
     48  let i_true_bound ≝ get_instr_bound i_true in
     49  let i_false_bound ≝ get_instr_bound i_false in
     50  let c_bound ≝ get_instr_bound instr in 
     51   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))
     52| LOOP cond ltrue i_true lfalse instr ⇒
     53  let i_true_bound ≝ get_instr_bound i_true in
     54  let c_bound ≝ get_instr_bound instr in
     55   max (get_cond_bound cond) (max i_true_bound c_bound)
     56| CALL f act_p opt_l instr ⇒
     57  let c_bound ≝ get_instr_bound instr in
     58   max (get_expr_bound act_p) c_bound
     59| IO lin io lout instr ⇒ ?
     60].
     61cases io
     62qed.
    2163
    2264let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝
     
    92134(foldr …
    93135   (λx,tail.(mk_env_item …
    94                (mk_signature frame_env_params … (f_name … (f_sig … x)) it ?(*(f_ret …(f_sig … x))*))
     136               (mk_signature frame_env_params … (f_name … (f_sig … x)) 14 ?(*(f_ret …(f_sig … x))*))
    95137               (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog))
    96138(trans_imp_instr (main … prog) map).
  • LTS/stack.ma

    r3575 r3577  
    130130
    131131
    132 let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
    133 match n with
    134 [ O ⇒ nil ?
    135 | S m ⇒ a :: list_n … a m
    136 ].
    137 
    138132definition stack_signature≝signature stack_state_params stack_state_params.
    139133
  • LTS/variable.ma

    r3575 r3577  
    119119definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
    120120
    121 definition frame_env_params ≝ mk_env_params unit.
     121definition frame_env_params ≝ mk_env_params .
    122122
    123123inductive frame_seq_i : Type[0] ≝
     
    185185definition frame_signature≝signature frame_state_params frame_state_params.
    186186
     187let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
     188match n with
     189[ O ⇒ nil ?
     190| S m ⇒ a :: list_n … a m
     191].
     192
    187193definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝
    188194λsgn,e,st.
    189195    !env ← frame_current_env … st;
    190196    !n ← frame_sem_expr env e;
    191     frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
     197    frame_assign_var 〈((list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st)),(\snd st)〉 to_shift n.
    192198
    193199definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝
  • LTS/variable_stack_pass.ma

    r3575 r3577  
    3232λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
    3333
    34 let rec get_expr_bound (e : expr) on e : ℕ ≝
    35 match 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 
    42 let rec get_cond_bound (c : condition) on c : ℕ ≝
    43 match c with
    44 [Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
    45 | Not c ⇒ get_cond_bound c
    46 ].
    47 
    48 let rec trans_var_instr (i : frame_Instructions) on i : (stack_Instructions × ℕ) ≝
     34let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝
    4935match i with
    50 [ EMPTY ⇒ 〈EMPTY …,O〉
    51 | RETURN exp ⇒ 〈list_combinators_to_instructions (trans_expr exp) (RETURN … it),get_expr_bound exp〉
     36[ EMPTY ⇒ EMPTY …
     37| RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
    5238| SEQ seq opt_l instr ⇒
    53   let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
     39  let t_instr ≝ trans_var_instr … instr in
    5440  match seq with
    5541  [ Seq_i seq' ⇒
    5642     match seq' with
    57      [ sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
    58                 max (get_expr_bound e) c_bound〉
     43     [ sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr)
    5944     ]
    60   | PopReg v ⇒ 〈SEQ stack_instr_params ? (popreg v) opt_l t_instr,max (S v) c_bound〉
     45  | PopReg v ⇒ SEQ stack_instr_params ? (popreg v) opt_l t_instr
    6146  ]
    6247| COND cond ltrue i_true lfalse i_false instr ⇒
    63   let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in
    64   let 〈t_i_false,i_false_bound〉 ≝ trans_var_instr … i_false in
    65   let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
    66   〈list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr),
    67    max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))〉
     48  let t_i_true ≝ trans_var_instr … i_true in
     49  let t_i_false ≝ trans_var_instr … i_false in
     50  let t_instr ≝ trans_var_instr … instr in
     51  list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr)
    6852| LOOP cond ltrue i_true lfalse instr ⇒
    69   let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in
    70   let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
    71   〈LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr,
    72    max (get_cond_bound cond) (max i_true_bound c_bound)〉
     53  let t_i_true ≝ trans_var_instr … i_true in
     54  let t_instr ≝ trans_var_instr … instr in
     55   LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr
    7356| CALL f act_p opt_l instr ⇒
    74   let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
    75   〈list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr),
    76    max (get_expr_bound act_p) c_bound〉
     57  let t_instr ≝ trans_var_instr … instr in
     58  list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr)
    7759| IO lin io lout instr ⇒ ?
    7860].
     
    8062qed.
    8163
    82 definition trans_var_prog : Program frame_env_params frame_instr_params flat_labels →
    83 (Program stack_env_params stack_instr_params flat_labels × ℕ) ≝
     64definition trans_var_prog :
     65 Program frame_env_params frame_instr_params flat_labels →
     66 Program stack_env_params stack_instr_params flat_labels ≝
    8467λprog.
    85 let 〈t_main,m_bound〉 ≝ trans_var_instr … (main … prog) in
    86 (mk_Program …
     68let t_main ≝ trans_var_instr … (main … prog) in
     69 (mk_Program …
    8770  (foldr …
    88    (λx,tail.(let 〈t_body,bound〉 ≝ trans_var_instr … (f_body … x) in
     71   (λx,tail.(let t_body ≝ trans_var_instr … (f_body … x) in
    8972     mk_env_item …       
    90      (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) bound it) (f_lab … x) t_body) :: tail)
     73     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) (f_pars … x) it) (f_lab … x) t_body) :: tail)
    9174   (nil ?) (env … prog))
    92   t_main),m_bound〉.
     75  t_main (initial_act … prog)).
    9376
    9477include "Simulation.ma".
     
    10386(mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
    10487 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
    105  (λs1,s2.store … s1 = store … s2 ∧ code … s2 = (\fst (trans_var_instr (code … s1))) ∧
    106          cont … s2 = foldr … (λx,tail. 〈(\fst x),(\fst (trans_var_instr (\snd x)))〉 :: tail) (nil ?) (cont … s1))
     88 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
     89         cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
    10790 (λ_.λ_.True)).
    108 
    10991
    11092let rec expr_fv (e : expr) on e : list variable ≝
     
    228210definition simulation_imp_frame :
    229211∀prog : Program frame_state_params frame_state_params frame_state_params.
    230 t_prog,bound.〈t_prog,bound〉 = trans_var_prog prog →
    231 simulation_conditions … (frame_variable_pass_rel prog t_prog bound) ≝
    232 λprog,t_prog,bound,good_trans.
     212bound: ℕ.
     213simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝
     214λprog,bound.
    233215mk_simulation_conditions ….
    234216cases daemon
    235217qed.
    236  
Note: See TracChangeset for help on using the changeset viewer.