Changeset 2599


Ignore:
Timestamp:
Jan 31, 2013, 5:15:49 PM (6 years ago)
Author:
tranquil
Message:
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2541 r2599  
    341341#tag #A * #m * #id * #id' #NE
    342342@lookup_opt_pm_set_miss
    343 /2/
     343/2 by not_to_not/
    344344qed.
    345345
     
    511511  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
    512512  [1:
    513     * #k_eq_hyp @⊥ /2/
     513    * #k_eq_hyp @⊥ /2 by absurd/
    514514  |2:
    515     #Some_eq_hyp' /2/
     515    #Some_eq_hyp' /2 by /
    516516  ]
    517517qed.
     
    537537#tag #A #map #k #v #k' normalize
    538538cases (identifier_eq ? k k')
    539 [ #E /2/
    540 | #NE >lookup_add_miss /3/
     539[ #E /2 by or_introl/
     540| #NE >lookup_add_miss /3 by or_intror, conj, absurd, nmk/
    541541] qed.
    542542
     
    675675[ % | #x %{x} % ]
    676676qed.
    677 
     677(*
    678678lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
    679679#tag * normalize #m >map_opt_id_eq_ext // * %
     
    694694>map_opt_id >map_opt_id //
    695695qed.
    696 
     696*)
    697697lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag.
    698698  i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s').
     
    10151015[ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct | * * #x #y #z #E destruct % ] ]
    10161016* * * #L1 #L2 #L3 #_
    1017 % [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ]
     1017% [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2 by or_introl/ | #L4 %2 @L4 ] ]
    10181018qed.
    10191019
     
    10631063[ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct | * #x #y #E destruct % ] ]
    10641064* * * #L1 #L2 #L3 #_
    1065 % [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ]
     1065% [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2 by or_introl/ | #L4 %2 @L4 ] ]
    10661066qed.
    10671067
     
    11401140  Exists ? (λid'. id = id') l.
    11411141#tag #l #id whd in match (set_of_list ??);
    1142 cut (¬present ?? ∅ id) [ /3/ ]
     1142cut (¬present ?? ∅ id) [ /3 by refl, absurd, nmk/ ]
    11431143generalize in match ∅;
    11441144elim l
     
    11461146| #id' #tl #IH #s #F #PR whd in PR:(???%?);
    11471147  cases (identifier_eq … id id')
    1148   [ #E destruct /2/
     1148  [ #E destruct /2 by or_introl/
    11491149  | #NE %2 @(IH … PR)
    1150     @(not_to_not … F) /2/
     1150    @(not_to_not … F) /2 by present_add_present/
    11511151  ]
    11521152] qed.
     
    11731173[ @P0
    11741174| #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
    1175   [ normalize >FR /3/
     1175  [ normalize >FR /3 by absurd, nmk/
    11761176  | @L
    11771177  | @pre
     
    11841184  foldi A B tag f m b = b' →
    11851185  P b' (domain_of_map … m).
    1186 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
    1187 qed.
    1188 
     1186#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2 by /
     1187qed.
     1188
  • src/common/PositiveMap.ma

    r2590 r2599  
    422422include "utilities/option.ma".
    423423
     424definition is_none : ∀A.option A → bool ≝ λA,o.match o with [ None ⇒ true | _ ⇒ false ].
     425definition is_pm_leaf : ∀A.positive_map A → bool ≝ λA,m.match m with [ pm_leaf ⇒ true | _ ⇒ false ].
     426
    424427let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
    425428match b with
    426429[ pm_leaf ⇒ pm_leaf ?
    427 | pm_node a l r ⇒ pm_node ? (!x ← a ; f x)
    428     (map_opt ?? f l)
    429     (map_opt ?? f r)
     430| pm_node a l r ⇒
     431  let a' ≝ !x ← a ; f x in
     432  let l' ≝ map_opt ?? f l in
     433  let r' ≝ map_opt ?? f r in
     434  if is_none … a' ∧ is_pm_leaf … l' ∧ is_pm_leaf … r' then
     435    pm_leaf ?
     436  else
     437    pm_node ? a' l' r'
    430438].
    431439
    432440definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
     441
     442lemma andb_false_r : ∀b.(b∧false)=false. *% qed.
    433443
    434444lemma lookup_opt_map : ∀A,B,f,b,p.
    435445  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
    436446#A#B#f#b elim b [//]
    437 #a #l #r #Hil #Hir * [//]
    438 #p
    439 whd in ⊢ (??(???%)(????%?));
    440 whd in ⊢ (??%?); //
    441 qed.
    442 
     447#a #l #r #IHl #IHr * [2,3: #p ]
     448whd in match (map_opt ????); whd in match (lookup_opt ???) in ⊢ (???%);
     449[3: cases (! x ← a ; f x) [2: #x] try % cases (?∧?) % ]
     450inversion (map_opt ??? l)
     451[2,4: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
     452  whd in ⊢ (??%?); // ]
     453#EQl
     454inversion (map_opt ??? r)
     455[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
     456  whd in ⊢ (??%?); // ]
     457#EQr
     458[ <IHr >EQr | <IHl >EQl ] cases (?∧?) %
     459qed.
     460
     461(*
    443462lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
    444463#A #m #f #Hf elim m [//]
     
    449468#A #m @map_opt_id_eq_ext //
    450469qed.
     470*)
    451471
    452472let rec merge A B C (choice : option A → option B → option C)
     
    458478  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
    459479  | pm_node o' l' r' ⇒
    460     match (choice o o') with 
    461     [None ⇒
    462       match (merge … choice l l') with
    463       [pm_leaf ⇒ match (merge … choice r r') with
    464           [pm_leaf ⇒ pm_leaf ?
    465           |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
    466           ]
    467       |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
    468       ]
    469    |Some x ⇒
    470     pm_node ? (Some ? x)
    471       (merge … choice l l')
    472       (merge … choice r r')
    473   ]
    474 ]].
     480    let o'' ≝ choice o o' in
     481    let l'' ≝ merge … choice l l' in
     482    let r'' ≝ merge … choice r r' in
     483    if is_none … o'' ∧ is_pm_leaf … l'' ∧ is_pm_leaf … r'' then
     484      pm_leaf ?
     485    else
     486      pm_node ? o'' l'' r''
     487  ]
     488].
    475489
    476490lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     
    478492  lookup_opt … p (merge A B C choice a b) =
    479493    choice (lookup_opt … p a) (lookup_opt … p b).
    480  #A#B#C#choice#a elim a
    481 [ normalize #b
     494 #A#B#C#choice#a elim a -a
     495[ #b
    482496| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
    483497  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
     
    490504elim (lookup_opt ???)
    491505normalize //
    492 qed. 
     506qed.
    493507
    494508let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
     
    504518interpretation "positive map size" 'card p = (domain_size ? p).
    505519
     520(*
    506521lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
    507522#A#B#f#b elim b [//]
     
    510525@le_plus assumption
    511526qed.
     527*)
    512528
    513529lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
    514530#A#B#f#b elim b [//]
    515 *[2:#x]#l#r#Hil#Hir normalize
    516 >Hil >Hir @refl
     531*[2:#x]#l#r#Hil#Hir
     532[ normalize >Hil >Hir @refl ]
     533whd in match (map ????);
     534inversion (map_opt ??? l)
     535[2: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
     536  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
     537#EQl
     538inversion (map_opt ??? r)
     539[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
     540  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
     541#EQr normalize nodelta normalize
     542<Hil <Hir whd in match map; normalize nodelta >EQl >EQr %
    517543qed.
    518544
  • src/joint/blocks.ma

    r2595 r2599  
    296296
    297297interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
     298
     299lemma step_list_in_code_ne : ∀p,globals.∀c : codeT p globals.∀src,B,l,dst.
     300  not_empty ? B →
     301  src ~❨B,l❩~> dst in c →
     302  ∃prf : not_empty … l.
     303  \snd (split_on_last_ne … «l, prf») = dst.
     304#p #globals #c #src #b lapply src -src elim b -b [ #src #l #dst * ]
     305#hd * [2: #hd' #tl ] #IH #src * [1,3: #dst #_ * ]
     306#mid * [ #dst #_ * #_ * |4: #mid' #tl #dst #_ * #_ * ]
     307[2: #dst * * #_ whd in ⊢ (%→?); #EQ destruct %{I} % ]
     308#mid' #rest #dst * * #H1 #H2 %{I}
     309cases (IH … I H2) * #EQ <EQ
     310whd in match (split_on_last_ne ??);
     311whd in match split_on_last_ne; normalize nodelta
     312@pair_elim #a #b #_ %
     313qed.
    298314
    299315lemma step_list_in_code_append :
  • src/joint/semantics_blocks.ma

    r2595 r2599  
    5151    return 〈curr_id, curr_fn〉 →
    5252  let src ≝ point_of_pc p (pc … st) in
    53   (* disambiguation: select 3rd (step list in code) *)
    54   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     53  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
    5554  All ? (no_cost_label …) b →
    5655  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    138137    return 〈curr_id, curr_fn〉 →
    139138  let src ≝ point_of_pc p (pc … st) in
    140   (* disambiguation: select 3rd (step list in code) *)
    141   src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     139  step_list_in_code … (joint_if_code … curr_fn) src b l dst →
    142140  All ? (no_cost_label …) b →
    143141  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
Note: See TracChangeset for help on using the changeset viewer.