Changeset 3577

Timestamp:

Jun 19, 2015, 6:31:59 PM (6 years ago)

Author:

sacerdot

Message:

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

Location:

LTS

Files:

• frame_variable_pass.ma (modified) (2 diffs)
• stack.ma (modified) (1 diff)
• variable.ma (modified) (2 diffs)
• variable_stack_pass.ma (modified) (4 diffs)

LTS/frame_variable_pass.ma

@@ -19 +19 @@
 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 
 λA,B,f,a,b,x.if x == a then b else f x.
+
+let rec get_expr_bound (e : expr) on e : ℕ ≝ 
+match e with
+[ Var v ⇒ S v
+| Const n ⇒ O
+| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
+| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
+].
+
+let rec get_cond_bound (c : condition) on c : ℕ ≝ 
+match c with
+[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
+| Not c ⇒ get_cond_bound c
+].
+
+let rec get_instr_bound (i : frame_Instructions) ≝ 
+match i with
+[ EMPTY ⇒ O
+| RETURN exp ⇒ get_expr_bound exp
+| SEQ seq opt_l instr ⇒ 
+  let c_bound ≝ get_instr_bound instr in
+  match seq with
+  [ Seq_i seq' ⇒ 
+     match seq' with [ sAss v e ⇒ max (get_expr_bound e) c_bound ]
+  | PopReg v ⇒ max (S v) c_bound
+  ]
+| COND cond ltrue i_true lfalse i_false instr ⇒
+  let i_true_bound ≝ get_instr_bound i_true in
+  let i_false_bound ≝ get_instr_bound i_false in
+  let c_bound ≝ get_instr_bound instr in  
+   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))
+| LOOP cond ltrue i_true lfalse instr ⇒ 
+  let i_true_bound ≝ get_instr_bound i_true in 
+  let c_bound ≝ get_instr_bound instr in
+   max (get_cond_bound cond) (max i_true_bound c_bound)
+| CALL f act_p opt_l instr ⇒ 
+  let c_bound ≝ get_instr_bound instr in
+   max (get_expr_bound act_p) c_bound
+| IO lin io lout instr ⇒ ?
+].
+cases io
+qed.
 
 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ 
@@ -92 +134 @@
 (foldr … 
    (λx,tail.(mk_env_item …
-               (mk_signature frame_env_params … (f_name … (f_sig … x)) it ?(*(f_ret …(f_sig … x))*))
+               (mk_signature frame_env_params … (f_name … (f_sig … x)) 14 ?(*(f_ret …(f_sig … x))*))
                (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog))
 (trans_imp_instr (main … prog) map).

LTS/stack.ma

@@ -130 +130 @@
 
 
-let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
-match n with
-[ O ⇒ nil ?
-| S m ⇒ a :: list_n … a m
-].
-
 definition stack_signature≝signature stack_state_params stack_state_params.
 

LTS/variable.ma

@@ -119 +119 @@
 definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
 
-definition frame_env_params ≝ mk_env_params unit.
+definition frame_env_params ≝ mk_env_params ℕ.
 
 inductive frame_seq_i : Type[0] ≝ 
@@ -185 +185 @@
 definition frame_signature≝signature frame_state_params frame_state_params.
 
+let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
+match n with
+[ O ⇒ nil ?
+| S m ⇒ a :: list_n … a m
+].
+
 definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝
 λsgn,e,st.
     !env ← frame_current_env … st;
     !n ← frame_sem_expr env e;
-    frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
+    frame_assign_var 〈((list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st)),(\snd st)〉 to_shift n.
 
 definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝

LTS/variable_stack_pass.ma

@@ -32 +32 @@
 λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
 
-let rec get_expr_bound (e : expr) on e : ℕ ≝ 
-match e with
-[ Var v ⇒ S v
-| Const n ⇒ O
-| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
-| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
-].
-
-let rec get_cond_bound (c : condition) on c : ℕ ≝ 
-match c with
-[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
-| Not c ⇒ get_cond_bound c
-].
-
-let rec trans_var_instr (i : frame_Instructions) on i : (stack_Instructions × ℕ) ≝ 
+let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝ 
 match i with
-[ EMPTY ⇒ 〈EMPTY …,O〉
-| RETURN exp ⇒ 〈list_combinators_to_instructions (trans_expr exp) (RETURN … it),get_expr_bound exp〉
+[ EMPTY ⇒ EMPTY …
+| RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
 | SEQ seq opt_l instr ⇒ 
-  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
+  let t_instr ≝ trans_var_instr … instr in
   match seq with
   [ Seq_i seq' ⇒ 
      match seq' with 
-     [ sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
-                max (get_expr_bound e) c_bound〉
+     [ sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr)
      ]
-  | PopReg v ⇒ 〈SEQ stack_instr_params ? (popreg v) opt_l t_instr,max (S v) c_bound〉
+  | PopReg v ⇒ SEQ stack_instr_params ? (popreg v) opt_l t_instr
   ]
 | COND cond ltrue i_true lfalse i_false instr ⇒
-  let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in
-  let 〈t_i_false,i_false_bound〉 ≝ trans_var_instr … i_false in
-  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
-  〈list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr),
-   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))〉
+  let t_i_true ≝ trans_var_instr … i_true in
+  let t_i_false ≝ trans_var_instr … i_false in
+  let t_instr ≝ trans_var_instr … instr in
+  list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr)
 | LOOP cond ltrue i_true lfalse instr ⇒ 
-  let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in 
-  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
-  〈LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr,
-   max (get_cond_bound cond) (max i_true_bound c_bound)〉
+  let t_i_true ≝ trans_var_instr … i_true in 
+  let t_instr ≝ trans_var_instr … instr in
+   LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr
 | CALL f act_p opt_l instr ⇒ 
-  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
-  〈list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr),
-   max (get_expr_bound act_p) c_bound〉
+  let t_instr ≝ trans_var_instr … instr in
+  list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr)
 | IO lin io lout instr ⇒ ?
 ].
@@ -80 +62 @@
 qed.
 
-definition trans_var_prog : Program frame_env_params frame_instr_params flat_labels → 
-(Program stack_env_params stack_instr_params flat_labels × ℕ) ≝ 
+definition trans_var_prog :
+ Program frame_env_params frame_instr_params flat_labels → 
+ Program stack_env_params stack_instr_params flat_labels ≝ 
 λprog.
-let 〈t_main,m_bound〉 ≝ trans_var_instr … (main … prog) in
-〈(mk_Program …
+let t_main ≝ trans_var_instr … (main … prog) in
+ (mk_Program …
   (foldr … 
-   (λx,tail.(let 〈t_body,bound〉 ≝ trans_var_instr … (f_body … x) in
+   (λx,tail.(let t_body ≝ trans_var_instr … (f_body … x) in
      mk_env_item …       
-     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) bound it) (f_lab … x) t_body) :: tail) 
+     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) (f_pars … x) it) (f_lab … x) t_body) :: tail) 
    (nil ?) (env … prog))
-  t_main),m_bound〉.
+  t_main (initial_act … prog)).
 
 include "Simulation.ma".
@@ -103 +86 @@
 (mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
  (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
- (λs1,s2.store … s1 = store … s2 ∧ code … s2 = (\fst (trans_var_instr (code … s1))) ∧
-         cont … s2 = foldr … (λx,tail. 〈(\fst x),(\fst (trans_var_instr (\snd x)))〉 :: tail) (nil ?) (cont … s1))
+ (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
+         cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
  (λ_.λ_.True)).
-
 
 let rec expr_fv (e : expr) on e : list variable ≝ 
@@ -228 +210 @@
 definition simulation_imp_frame : 
 ∀prog : Program frame_state_params frame_state_params frame_state_params.
-∀t_prog,bound.〈t_prog,bound〉 = trans_var_prog prog → 
-simulation_conditions … (frame_variable_pass_rel prog t_prog bound) ≝ 
-λprog,t_prog,bound,good_trans.
+∀bound: ℕ. 
+simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝ 
+λprog,bound.
 mk_simulation_conditions ….
 cases daemon
 qed.
-