Ignore:
Timestamp:
Jul 10, 2015, 4:08:09 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/frame_variable_pass.ma

    r3577 r3579  
    1414
    1515include "Simulation.ma".
    16 include "variable.ma".
    17 include alias "arithmetics/nat.ma".
     16include "common_variable_stack.ma".
    1817
    1918definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝
    2019λA,B,f,a,b,x.if x == a then b else f x.
    2120
    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
    6322
    6423let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝
     
    10059cases io qed.
    10160
    102 
    103 let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
    104 match l1 with
    105 [ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False]
    106 | cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
    107 ].
    10861
    10962definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.