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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.