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/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).
Note: See TracChangeset for help on using the changeset viewer.