Changeset 2335 for src/common


Ignore:
Timestamp:
Sep 20, 2012, 6:57:34 PM (7 years ago)
Author:
campbell
Message:

Deal with goto labels in RTLabs to Cminor by fixing up goto statements
after the main translation to avoid generating extra skips in awkward
locations.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2314 r2335  
    334334  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
    335335
     336(* An informative, dependently-typed, fold. *)
     337
     338definition fold_inf:
     339  ∀A, B: Type[0].
     340  ∀tag: String.
     341  ∀m:identifier_map tag A.
     342  (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B ≝
     343λA,B,tag,m.
     344  match m return λm. (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B with
     345  [ an_id_map m' ⇒ λf,b. pm_fold_inf A B m' (λbv,a,H. f (an_identifier ? bv) a H) b ].
     346
    336347(* A predicate that an identifier is in a map, and a failure-avoiding lookup
    337348   and update using it. *)
     
    518529whd >lookup_add_miss //
    519530qed.
     531
     532(* Extending the domain of a map (without necessarily preserving contents). *)
     533
     534definition extends_domain : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝
     535λtag,A,m1,m2. ∀l. present ?? m1 l → present ?? m2 l.
     536
     537lemma extends_dom_trans : ∀tag,A,m1,m2,m3.
     538  extends_domain tag A m1 m2 → extends_domain tag A m2 m3 → extends_domain tag A m1 m3.
     539#tag #A #m1 #m2 #m3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
    520540
    521541
     
    10181038
    10191039
    1020 
     1040(* Transforming a list into a set. *)
     1041
     1042definition set_of_list : ∀tag. list (identifier tag) → identifier_set tag ≝
     1043λtag,l. foldl ?? (λs,id. add_set tag s id) ∅ l.
     1044
     1045lemma fold_add_set_monotone : ∀tag,l,s,id.
     1046  present tag unit s id →
     1047  present tag unit (foldl ?? (λs,id. add_set tag s id) s l) id.
     1048#tag #l elim l
     1049[ //
     1050| #h #t #IH #s #id #PR
     1051  whd in ⊢ (???%?); @IH
     1052  @lookup_add_oblivious
     1053  @PR
     1054] qed.
     1055
     1056lemma in_set_of_list : ∀tag,l,id.
     1057  Exists ? (λid'. id' = id) l →
     1058  present ?? (set_of_list tag l) id.
     1059#tag #l #id whd in match (set_of_list ??); generalize in match ∅; elim l
     1060[ #s *
     1061| #id' #tl #IH #s *
     1062  [ #E whd in ⊢ (???%?); destruct
     1063    @fold_add_set_monotone //
     1064  | @IH
     1065  ]
     1066] qed.
     1067
     1068lemma in_set_of_list' : ∀tag,l,id.
     1069  present ?? (set_of_list tag l) id →
     1070  Exists ? (λid'. id = id') l.
     1071#tag #l #id whd in match (set_of_list ??);
     1072cut (¬present ?? ∅ id) [ /3/ ]
     1073generalize in match ∅;
     1074elim l
     1075[ #s #F #T @⊥ @(absurd … T F)
     1076| #id' #tl #IH #s #F #PR whd in PR:(???%?);
     1077  cases (identifier_eq … id id')
     1078  [ #E destruct /2/
     1079  | #NE %2 @(IH … PR)
     1080    @(not_to_not … F) /2/
     1081  ]
     1082] qed.
     1083
     1084
     1085
  • src/common/PositiveMap.ma

    r2307 r2335  
    567567] qed.
    568568
    569 
     569(* An "informative" dependently typed fold *)
     570
     571let rec pm_fold_inf_aux
     572 (A, B: Type[0])
     573 (t: positive_map A)
     574 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B)
     575 (t': positive_map A)
     576 (pre: Pos → Pos)
     577 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝
     578match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with
     579[ pm_leaf ⇒ λ_. b
     580| pm_node a l r ⇒ λH.
     581    let b ≝ match a return λa. lookup_opt A one (pm_node A a ??) = ? → B with [ None ⇒ λ_.b | Some a ⇒ λH. f (pre one) a ? b ] (H one) in
     582    let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in
     583            pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ?
     584].
     585[ #p @(H (p1 p)) | #p @(H (p0 p)) | <H % ]
     586qed.
     587
     588definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A.
     589 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝
     590  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
     591
Note: See TracChangeset for help on using the changeset viewer.