Changeset 3577 for LTS/frame_variable_pass.ma
 Timestamp:
 Jun 19, 2015, 6:31:59 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/frame_variable_pass.ma
r3575 r3577 19 19 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 20 20 λA,B,f,a,b,x.if x == a then b else f x. 21 22 let rec get_expr_bound (e : expr) on e : ℕ ≝ 23 match 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 30 let rec get_cond_bound (c : condition) on c : ℕ ≝ 31 match c with 32 [Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 33  Not c ⇒ get_cond_bound c 34 ]. 35 36 let rec get_instr_bound (i : frame_Instructions) ≝ 37 match 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 ]. 61 cases io 62 qed. 21 63 22 64 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ … … 92 134 (foldr … 93 135 (λ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))*)) 95 137 (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog)) 96 138 (trans_imp_instr (main … prog) map).
Note: See TracChangeset
for help on using the changeset viewer.