Changeset 2415


Ignore:
Timestamp:
Oct 23, 2012, 3:57:02 PM (7 years ago)
Author:
campbell
Message:

Add the ability to map blocks to symbols in preparation for stack space.

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2319 r2415  
    228228
    229229
     230(* Turn a memory block into the original symbol. *)
     231definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝
     232λF,genv,b.
     233  option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')).
     234
     235
    230236lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
    231237  find_funct F ge v = Some F f →
     
    312318#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
    313319qed.
     320
     321lemma symbol_of_block_rev : ∀F,genv,b,id.
     322  symbol_for_block F genv b = Some ? id →
     323  find_symbol F genv id = Some ? b.
     324#F #genv #b #id #H whd in H:(??%?);
     325@(find_lookup … (λid,b'. eq_block b b'))
     326lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b'))
     327cases (find ????) in H ⊢ %;
     328[ normalize #E destruct
     329| * #id' #b' normalize in ⊢ (% → ?); #E destruct
     330  #H lapply (H … (refl ??))
     331  @eq_block_elim
     332  [ #E destruct //
     333  | #_ *
     334  ]
     335] qed.
    314336
    315337(*
  • src/common/Identifiers.ma

    r2335 r2415  
    345345  [ an_id_map m' ⇒ λf,b. pm_fold_inf A B m' (λbv,a,H. f (an_identifier ? bv) a H) b ].
    346346
     347(* Find one element of a map that satisfies a predicate *)
     348definition find : ∀tag,A. identifier_map tag A → (identifier tag → A → bool) →
     349  option (identifier tag × A) ≝
     350λtag,A,m,p.
     351  match m with [ an_id_map m' ⇒
     352    option_map … (λx. 〈an_identifier tag (\fst x), \snd x〉)
     353      (pm_find … m' (λid. p (an_identifier tag id))) ].
     354
     355lemma find_lookup : ∀tag,A,m,p,id,a.
     356  find tag A m p = Some ? 〈id,a〉 →
     357  lookup … m id = Some ? a.
     358#tag #A * #m #p * #id #a #FIND
     359@(pm_find_lookup A (λid. p (an_identifier tag id)) id a m)
     360whd in FIND:(??%?); cases (pm_find ???) in FIND ⊢ %;
     361[ normalize #E destruct
     362| * #id' #a' normalize #E destruct %
     363] qed.
     364
     365lemma find_predicate : ∀tag,A,m,p,id,a.
     366  find tag A m p = Some ? 〈id,a〉 →
     367  p id a.
     368#tag #A * #m #p * #id #a #FIND whd in FIND:(??%?);
     369@(pm_find_predicate A m (λid. p (an_identifier tag id)) id a)
     370cases (pm_find ???) in FIND ⊢ %;
     371[ normalize #E destruct
     372| * #id' #a' normalize #E destruct %
     373] qed.
     374
    347375(* A predicate that an identifier is in a map, and a failure-avoiding lookup
    348376   and update using it. *)
  • src/common/PositiveMap.ma

    r2335 r2415  
    590590  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
    591591
     592(* Find an entry in the map matching the given predicate *)
     593
     594let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
     595match t with
     596[ pm_leaf ⇒ None ?
     597| pm_node a l r ⇒
     598  let x ≝ match a with
     599  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
     600  | None ⇒ None ?
     601  ] in
     602  match x with
     603  [ Some x ⇒ Some ? x
     604  | None ⇒
     605    match pm_find_aux (λx. pre (p0 x)) A l p with
     606    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
     607    | Some y ⇒ Some ? y
     608    ]
     609  ]
     610].
     611
     612definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
     613  pm_find_aux (λx.x).
     614
     615lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
     616  pm_find_aux pre A t p = Some ? 〈q,a〉 →
     617  ∃q'. q = pre q'.
     618#A #t elim t
     619[ normalize #pre #p #q #a #E destruct
     620| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
     621  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
     622  lapply (IHl (λx. pre (p0 x)) p)
     623  cases (pm_find_aux ?? l ?)
     624  [ 1,3: #_ normalize
     625    lapply (IHr (λx. pre (p1 x)) p)
     626    cases (pm_find_aux ?? r ?)
     627    [ 1,3: #_ #E destruct
     628    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
     629    ]
     630  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
     631  ]
     632] qed.
     633
     634(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
     635lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
     636  (∀a,a'. f a = f a' → a = a') →
     637  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
     638  a = a' ∧ b = b'.
     639#A #B #a #a' #b #b' #f #EXT #E
     640cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
     641#E' >(EXT … E') in E ⊢ %; #E destruct /2/
     642qed.
     643
     644lemma pm_find_lookup : ∀A,p,q,a,t.
     645  pm_find A t p = Some ? 〈q,a〉 →
     646  lookup_opt A q t = Some ? a.
     647#A #p #q #a normalize #t
     648change with ((λx.x) q) in match q in ⊢ (% → ?);
     649cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
     650generalize in match q; -q generalize in match (λx.x);
     651elim t
     652[ #pre #q #_  normalize #E destruct
     653| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
     654  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
     655  lapply (IHl (λx.pre (p0 x)))
     656  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
     657  cases (pm_find_aux ?? l ?)
     658  [ 1,3: #_ #_ normalize
     659    lapply (IHr (λx.pre (p1 x)))
     660    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
     661    cases (pm_find_aux ?? r ?)
     662    [ 1,3: #_ #_ #E destruct
     663    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
     664         whd in ⊢ (??%?); @H2 //
     665         #y #z #E lapply (PRE … E) #E' destruct //
     666    ]
     667  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
     668         whd in ⊢ (??%?); @H2 //
     669         #y #z #E lapply (PRE … E) #E' destruct //
     670  ]
     671] qed.
     672
     673lemma pm_find_predicate : ∀A,t,p,q,a.
     674  pm_find A t p = Some ? 〈q,a〉 →
     675  p q a.
     676#A #t #p normalize #q
     677change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
     678elim t
     679[ normalize #pre #q #a #E destruct
     680| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
     681  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
     682    [ #E normalize #E'
     683      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
     684      #E'' <E'' in E' ⊢ %; #E' destruct >E %
     685    | #_ normalize
     686    ]
     687  ]
     688  lapply (IHl (λx.pre (p0 x)))
     689  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
     690  cases (pm_find_aux ?? l ?)
     691  [ 1,3: #_ #_ normalize
     692    lapply (IHr (λx.pre (p1 x)))
     693    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
     694    cases (pm_find_aux ?? r ?)
     695    [ 1,3: #_ #_ #E destruct
     696    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
     697    ]
     698  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
     699  ]
     700] qed.
Note: See TracChangeset for help on using the changeset viewer.