Changeset 3574


Ignore:
Timestamp:
Jun 18, 2015, 6:33:00 PM (4 years ago)
Author:
piccolo
Message:

assembly pass in place

Location:
LTS
Files:
2 added
4 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3570 r3574  
    6969              [ LOOP y ltrue' i1' lfalse' i2' ⇒ x == y ∧
    7070                      eq_instructions … i1 i1' ∧ eq_nf_label … ltrue ltrue' ∧
    71                       eq_instructions … i2 i2'
     71                      eq_instructions … i2 i2' ∧ eq_nf_label … lfalse lfalse'
    7272              | _ ⇒ false
    7373              ]
     
    9696  [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9797  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
    98 | #seq * [| #lbl] #i #IH #P * normalize
     98| #seq * [| #lbl] #i #IH #P *
    9999  [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c
    100100  |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3]
    101   #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct)
    102   inversion(?==?) normalize nodelta
     101  #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) whd in match (eq_instructions ????);
     102  normalize nodelta inversion(?==?) normalize nodelta
    103103  [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    104104        >(\b (refl …)) in ABS; #EQ destruct]
    105   #EQseq cases daemon
    106 |*: cases daemon
    107 qed.
     105  #EQseq @IH normalize nodelta [2,4: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     106  #EQ destruct cases opt_l in H1 H2; -opt_l normalize nodelta
     107  [ #H1 #_ @H1 >(\P EQseq) %
     108  | #lab #_ #H1 @H1 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     109  | #_ #H1 @H1 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     110  | #lab #H1 #H2 @eq_fn_label_elim [ #EQ destruct @H1 >(\P EQseq) % ]
     111    * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %
     112  ]
     113| #cond #ltrue #i_true #lfalse #i_false #instr #IH1 #IH2 #IH3 #P *
     114   [| #t_t | #seq1 #opt_l #i2 | #cond' #ltrue' #i_t' #lfalse' #i_f' #i_c'
     115   | #cond' #ltrue' #i_t' #lfalse' #i_f' | #f #act_p #ret #i3 | #lin #io #lout #i3]
     116   #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct)
     117   whd in match (eq_instructions ????); inversion(?==?) normalize nodelta
     118   [2: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     119        >(\b (refl …)) in ABS; #EQ destruct] #EQcond @eq_fn_label_elim
     120   normalize nodelta [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     121   #EQ destruct @IH1 normalize nodelta
     122   [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     123   #EQ destruct  @eq_fn_label_elim
     124   normalize nodelta [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     125   #EQ destruct @IH2 normalize nodelta
     126   [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     127   #EQ destruct @IH3 normalize nodelta
     128   [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     129   #EQ destruct @H1 >(\P EQcond) %
     130| #cond #ltrue #i_true #lfalse #instr #IH1 #IH2 #P *
     131   [| #t_t | #seq1 #opt_l #i2 | #cond' #ltrue' #i_t' #lfalse' #i_f' #i_c'
     132   | #cond' #ltrue' #i_t' #lfalse' #i_f' | #f #act_p #ret #i3 | #lin #io #lout #i3]
     133   #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct)
     134   whd in match (eq_instructions ????); inversion(?==?) normalize nodelta
     135   [2: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     136        >(\b (refl …)) in ABS; #EQ destruct] #EQcond @IH1 normalize nodelta
     137   [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     138   #EQ destruct  @eq_fn_label_elim
     139   normalize nodelta [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     140   #EQ destruct @IH2 normalize nodelta
     141   [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     142   #EQ destruct  @eq_fn_label_elim
     143   normalize nodelta [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     144   #EQ destruct @H1 >(\P EQcond) %
     145| #a #b #c #d #IH #P *
     146   [| #t_t | #seq1 #opt_l #i2 | #cond' #ltrue' #i_t' #lfalse' #i_f' #i_c'
     147   | #cond' #ltrue' #i_t' #lfalse' #i_f' | #f #act_p #ret #i3 | #lin #io #lout #i3]
     148   #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) whd in match (eq_instructions ????);
     149   @eq_function_name_elim [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     150   #EQ destruct inversion (?==?) normalize nodelta
     151   [2: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     152        >(\b (refl …)) in ABS; #EQ destruct] #EQcond @IH
     153        [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     154   #EQ destruct normalize nodelta cases c in H1 H2; normalize nodelta cases ret normalize nodelta
     155   [ #H1 #H2 @H1 >(\P EQcond) %
     156   |2,3: #lab #H1 #H2 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %
     157   | #lab1 #lab2 #H1 #H2 @eq_return_cost_lab_elim
     158     [ #EQ destruct @H1 >(\P EQcond) %
     159     | * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %
     160     ]
     161   ]
     162| #a #b #c #d #IH #P *
     163   [| #t_t | #seq1 #opt_l #i2 | #cond' #ltrue' #i_t' #lfalse' #i_f' #i_c'
     164   | #cond' #ltrue' #i_t' #lfalse' #i_f' | #f #act_p #ret #i3 | #lin #io #lout #i3]
     165   #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) whd in match (eq_instructions ????);
     166    @eq_fn_label_elim
     167   normalize nodelta [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     168   #EQ destruct inversion (?==?) normalize nodelta
     169   [2: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     170        >(\b (refl …)) in ABS; #EQ destruct] #EQcond
     171   @eq_fn_label_elim
     172   normalize nodelta [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     173   #EQ destruct @IH
     174        [2: * #H3 @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases H3 %]
     175   #EQ destruct @H1 >(\P EQcond) %
     176]
     177qed.
    108178
    109179record env_params : Type[1] ≝
  • LTS/stack_monostack_pass.ma

    r3572 r3574  
    2020[ nil ⇒ s2 = nil ?
    2121| cons x xs ⇒ ∃old_fp,s21,s22.s2 = s21 @ [old_fp] @ s22 ∧
    22               match x with [ nil ⇒ False | cons y ys ⇒ ys = s21 ] ∧
     22              x= s21 @ [O] ∧
    2323              mono_env_store_rel xs s22 old_fp ∧ |s22| = fp
    2424].
     
    3535mk_relations … (λs1,s2.mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2)
    3636  (λ_.λ_.True).
    37  
     37
     38lemma minus_right_cancellable : ∀n,m,p : ℕ.n = m → n-p = m -p. //
     39qed.
     40
     41
     42lemma read_frame_ok :
     43∀st1,st2,fp,env,x,n.
     44mono_env_store_rel st1 st2 fp → option_hd … st1 = return env →
     45to_shift + x < |env| →
     46read_frame env (to_shift+x) O = return n →
     47read_frame st2 (to_shift+x) fp = return n.
     48#st1 elim st1 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in H7; destruct]
     49#env #tl #IH #st2 #fp #env' #x #n * #old_fp * #s21 * #s22 *** #EQ1 #EQ2 destruct #H #EQ destruct
     50whd in ⊢ (??%% → ?); #EQ destruct #H1
     51change with (nth_opt ???) in ⊢ (??%? → ?);  <minus_n_O >length_append normalize in ⊢ (??(??%?)? → ?);
     52>nth_first
     53[2: normalize >minus_minus_comm >commutative_plus <(plus_minus … 1) // normalize <(minus_Sn_m … (S (S x)))
     54   [2: >length_append in H1; normalize >(commutative_plus) normalize  /2/]
     55   normalize /2/
     56]
     57#H2 change with (nth_opt ???) in ⊢ (??%?); >nth_first
     58[2: >length_append >length_append normalize <plus_n_Sm normalize <(minus_minus_comm ? (|s22|))
     59    >commutative_plus <(plus_minus … (|s22|)) [2: //] <minus_n_n normalize >minus_plus <(minus_Sn_m … (S x +1))
     60    [2: normalize >commutative_plus normalize normalize in H1; >length_append in H1; normalize >commutative_plus
     61        normalize /2/ ]
     62    <commutative_plus normalize /2/
     63]
     64>length_append >length_append
     65cut((|s21|+(|[old_fp]|+|s22|)-(to_shift+x)-|s22|-1) = (|s21|+1-S (S x)-1))
     66[ normalize @minus_right_cancellable  >minus_minus_comm >commutative_plus <(plus_minus … (|s22|)) [2: //]
     67  <(minus_Sn_n … (|s22|)) >commutative_plus %
     68] #EQ >EQ assumption
     69qed.
     70
    3871definition stack_mono_stack_simulation : ∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
    3972simulation_conditions … (mono_stack_relations prog bound) ≝λprog.λbound.mk_simulation_conditions ….
     73(*[4: #s1 #s2 #s1' #H inversion H
     74   [ #st1 #st2 * #lab #instr #tl #EQcode_st1 #EQcond_st1 #EQ1 #EQ2 destruct #EQstore *)
    4075cases daemon
    4176qed.
  • LTS/utils.ma

    r3563 r3574  
    1717include "../src/ASM/Util.ma".
    1818include "../src/utilities/option.ma".
     19
     20definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝
     21λA,B,f,a,b,x.if x == a then b else f x.
    1922
    2023lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
     
    360363@eq_f2 // @IH //
    361364qed.
     365
     366(* nth_opt*)
     367
     368lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| > n → nth_opt … n (l1 @ l2) = nth_opt … n l1.
     369#A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/
     370qed.
     371
     372lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| ≤ n → nth_opt …  n (l1 @ l2) = nth_opt … (n - |l1|) l2.
     373#A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/
     374qed.
  • LTS/variable_stack_pass.ma

    r3570 r3574  
    134134]
    135135qed.
    136 
    137 lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| > n → nth_opt … n (l1 @ l2) = nth_opt … n l1.
    138 #A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/
    139 qed.
    140 
    141 lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| ≤ n → nth_opt …  n (l1 @ l2) = nth_opt … (n - |l1|) l2.
    142 #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/
    143 qed.
    144136
    145137lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2.
Note: See TracChangeset for help on using the changeset viewer.