Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 years ago)
Author:
piccolo
Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraIdentifiers.ma

    r3217 r3259  
    2121[//] #i #IH #f #b @IH
    2222qed.
    23    
     23
     24let rec pm_clean (A : Type[0]) (p : positive_map A) on p : positive_map A ≝
     25match p with
     26[ pm_leaf ⇒ pm_leaf A
     27| pm_node a l r ⇒ let l' ≝ pm_clean A l in
     28                  let r' ≝ pm_clean A r in
     29                  if andb (is_none ? a)
     30                      (andb (is_pm_leaf ? l') (is_pm_leaf ? r')) then
     31                     pm_leaf A
     32                  else
     33                     pm_node ? a l' r'
     34].
     35 
     36lemma lookup_pm_clean : ∀A : Type[0].∀p,p' : positive_map A.
     37(∀i.lookup_opt A i p = lookup_opt A i p') →
     38pm_clean A p = pm_clean A p'.
     39#A #p elim p
     40[ #p' elim p' [ #_ normalize %] * [2: #a] #l #r #IHl #IHr #H normalize
     41  [ lapply(H one) normalize #EQ destruct]
     42  <IHl [2,4: #i lapply(H (p0 i)) normalize //] normalize
     43  <IHr [2,4: #i lapply(H (p1 i)) normalize //] %
     44| #opt_a #l #r #IHl #IHr *
     45  [ #H normalize lapply(H one) normalize #EQ destruct(EQ) normalize
     46    >(IHl (pm_leaf ?)) [2: #i lapply(H (p0 i)) normalize //] normalize
     47    >(IHr (pm_leaf ?)) [2: #i lapply(H (p1 i)) normalize //] %
     48  | #opt_a' #l' #r' #H normalize lapply(H one) normalize #EQ destruct(EQ)
     49    >(IHl l') [2: #i lapply(H (p0 i)) normalize //]
     50    >(IHr r') [2: #i lapply(H (p1 i)) normalize //] %
     51  ]
     52]
     53qed. 
     54
     55definition pm_find_all : ∀A : Type[0].positive_map A →
     56(Pos → A → bool) → positive_map A ≝
     57λA,p,P.fold ??
     58 (λi,a,p'.if P i a then pm_set ? i (Some ? a) p' else p') p (pm_leaf A).
     59 
     60
     61lemma pm_clean_idempotent : ∀A : Type[0].∀p : positive_map A.
     62pm_clean ? p = pm_clean ? (pm_clean ? p).
     63cases daemon
     64qed.
     65
     66 
     67lemma pm_find_all_canonic : ∀A : Type[0].∀p : positive_map A.∀P.
     68pm_find_all A p P = pm_clean A (pm_find_all A p P).
     69#A #p #P whd in match pm_find_all; normalize nodelta
     70@pm_fold_ind
     71[ %] #i #ps #a #b #H #H1 #H2 cases(P i a) normalize
     72[2: assumption] lapply H2 lapply b elim i
     73[ normalize * [ #_ %] #opt_a #l #r
     74  normalize nodelta normalize cases opt_a
     75  [2: #a1 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
     76      >e1 in ⊢ (??%?); % ] normalize
     77  cases(pm_clean ? l) normalize [2: #opt_a1 #l1 #r1
     78  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?); %]
     79  cases(pm_clean ? r) normalize [#EQ destruct] #opt_a1 #l1 #r1
     80  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct %
     81|*: #x #IH * normalize
     82   [1,3: #_ <IH [2,4: % ]
     83    inversion(pm_set A x ??) [2,4: #opt_a1 #l1 #r1 #_#_#_ %]
     84    #ABS @⊥ cases x in ABS; [1,4: normalize #EQ destruct] #x1 normalize
     85    #EQ destruct
     86   |*: * [2,4: #a1] #l #r normalize
     87       [1,2: #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
     88             >e1 in ⊢ (??%?); <IH
     89             [ @eq_f3 try % >e1 in ⊢ (???%); %
     90             | assumption
     91             | @eq_f3 try % @pm_clean_idempotent
     92             | @pm_clean_idempotent
     93             ]
     94       |*: inversion(pm_clean A l) normalize
     95           [ #H3 inversion(pm_clean A r) normalize [#_ #EQ destruct] #opt_a1 #l1 #r1
     96             #_ #_ #H4 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ  <(IH r)
     97             [2: cut(r = pm_node A opt_a1 l1 r1) [ destruct %] #H5
     98             >H5 in ⊢ (??%?); <H4 % ] inversion(pm_set A x ??)
     99             [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
     100             #ABS @⊥ cases x in ABS; normalize cases r normalize
     101             [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     102             #EQ1 destruct
     103           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     104             <(IH r) [destruct %] destruct assumption
     105           | #H3 cases(pm_clean A r) normalize [#EQ destruct] #opt_a1 #l1 #r1
     106              #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ <(IH l) [2: >H3 destruct %]
     107              inversion(pm_set A x ??)
     108              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
     109              #ABS @⊥ cases x in ABS; normalize cases l normalize
     110              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     111              #EQ1 destruct
     112           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     113             <(IH l) [2: >H3 destruct %] inversion(pm_set A x ??)
     114              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct >e0 in ⊢ (??%?); %]
     115              #ABS @⊥ cases x in ABS; normalize cases l normalize
     116              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     117              #EQ1 destruct
     118           ] 
     119       ]   
     120   ]
     121]
     122qed. 
     123
    24124
    25125definition find_all : ∀tag,A. identifier_map tag A →
    26126(identifier tag → A → bool) → identifier_map tag A ≝
    27 λtag,A,m,P.foldi A (identifier_map tag A) tag
    28 (λi,a,l.if (P i a) then (add tag A l i a) else l) m (empty_map tag A).
    29 
     127λtag,A,m,P.match m with
     128  [an_id_map p ⇒ an_id_map ?? (pm_find_all A p (λx,a.P (an_identifier tag x) a))].
     129(*
    30130
    31131lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A.
     
    33133lookup tag A (find_all tag A m P) i = Some ? a →
    34134lookup tag A m i = Some ? a  ∧ (bool_to_Prop (P i a)).
    35 #tag #A #m #P #i #a whd in match find_all; normalize nodelta @foldi_ind
     135#tag #A * #m #P * #i #a whd in match find_all; normalize @pm_fold_ind
    36136[ normalize #EQ destruct
    37 | #k #ks #a1 #b * #H #H1 #H2 inversion(P k a1)
    38   [ #H3 normalize nodelta >H3
    39     cut(bool_to_Prop (eq_identifier tag i k) ∨
     137| #k #ks #a1 #b * #H #H1 #H2 inversion(P (an_identifier tag i) a1)
     138  [ cases(decidable_eq_pos i k)
     139    [#EQ destruct #H3 >H3 in H2; normalize >looku
     140
     141
     142  [#EQ destruct inversion(
     143
     144  [ #H3 normalize nodelta >H3 cases(decidable_eq_pos i k)
     145    [ #EQ destruct >H3 in H2;
     146 
     147 
     148    cut(bool_to_Prop (eq_identifier tag (an_identifier tag i) (an_identifierk) ∨
    40149     (bool_to_Prop (notb (eq_identifier tag i k))))
    41150    [@eq_identifier_elim #_ [ %%|%2 %]]
     
    68177]
    69178qed.
    70 
     179*)
    71180(*
    72181 whd in match (add ?????); whd in match (add ?????); normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.