Changeset 1627


Ignore:
Timestamp:
Dec 19, 2011, 2:48:34 PM (8 years ago)
Author:
campbell
Message:

Add some notions of freshness, and start using them for temporary
generation (not yet complete).

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1626 r1627  
    720720qed.
    721721
    722 record tmpgen : Type[0] ≝ {
     722definition add_tmps : var_types → list (ident × type) → var_types ≝
     723λvs,tmpenv.
     724  foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv.
     725
     726record tmpgen (vars:var_types) : Type[0] ≝ {
    723727  tmp_universe : universe SymbolTag;
    724   tmp_env : list (ident × type)
     728  tmp_env : list (ident × type);
     729  tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe;
     730  tmp_preserved :
     731    ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty
    725732}.
    726733
    727 definition alloc_tmp : type → tmpgen → ident × tmpgen ≝
    728 λty,g.
    729   let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
    730   〈tmp, mk_tmpgen u (〈tmp, ty〉::(tmp_env g))〉.
     734definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝
     735λvars,ty,g.
     736  let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in
     737  〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉.
     738[ #id #ty'
     739  whd in ⊢ (? → ?%??);
     740  whd in ⊢ (% → %);
     741  whd in ⊢ (? → match % with [_ ⇒ ? | _ ⇒ ?]); #H
     742  >lookup_add_miss
     743  [ @(tmp_preserved … g) @H
     744  | @(fresh_distinct … E) @(tmp_ok … g)
     745    lapply (tmp_preserved … g id ty' H)
     746    whd in ⊢ (% → %);
     747    whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
     748    cases (lookup ??? id)
     749    [ * | #x #_ % #E destruct ]
     750  ]
     751| @fresh_map_add
     752  [ @(fresh_map_preserved … E) @(tmp_ok … g)
     753  | @(fresh_is_fresh … E)
     754  ]
     755] qed.
    731756
    732757lemma lookup_label_hit : ∀lbls,l,l'.
     
    736761qed.
    737762
    738 definition add_tmps : var_types → tmpgen → var_types ≝
    739 λvs,g.
    740   foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs (tmp_env g).
    741 
    742 definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝
     763(* TODO: is this really needed now? *)
     764definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝
    743765λvars,u1,u2.
    744   ∀id,ty. local_id (add_tmps vars u1) id ty → local_id (add_tmps vars u2) id ty.
    745 
    746 lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q.
    747   〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
    748 cases daemon (* XXX freshness
    749 #tmp #g #g' #vars #q
    750 whd in ⊢ (???% → ?); #E
    751 #id #H
    752 cases (identifier_eq ? id tmp)
    753 destruct #E
    754 whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
    755 [ >E >lookup_add_hit @I
    756 | cases E #NE >lookup_add_miss [ @H | /2/
    757 ] *) qed.
    758 
    759 definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
     766  ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty.
     767
     768lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q.
     769  〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'.
     770#vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q
     771whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
     772cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?);
     773#tmp' #u' #E1 #E2 whd in E2:(???%); destruct
     774#id #ty #H whd in ⊢ (?%??); whd in H ⊢ %;
     775whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
     776>lookup_add_miss // @(fresh_distinct … E1) @F1
     777whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %;
     778cases (lookup ??? id) in H ⊢ %;
     779[ * | #x #_ % #E destruct ]
     780qed.
     781
     782definition trans_inv : ∀vars:var_types. lenv → statement → tmpgen vars → (stmt×(tmpgen vars)) → Prop ≝
    760783λvars,lbls,s,u,su'.
    761784  let 〈s',u'〉 ≝ su' in
    762   stmt_inv (add_tmps vars u') lbls s' ∧
     785  stmt_inv (add_tmps vars (tmp_env … u')) lbls s' ∧
    763786  labels_translated lbls s s' ∧
    764787  tmps_preserved vars u u'.
    765788
    766789lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su.
    767   trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su).
     790  trans_inv vars lbls s u su → stmt_inv (add_tmps vars (tmp_env … (\snd su))) lbls (\fst su).
    768791#var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1
    769792qed.
     
    774797qed.
    775798
    776 (* XXX Not true without fresh id' XXX
     799(* TODO: still needed? *)
    777800lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'.
     801  fresh_for_map ?? id' vars →
    778802  local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty.
    779 #vars #id #ty #id' #ty' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     803#vars #id #ty #id' #ty' #F #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    780804cases (identifier_eq ? id id')
    781 [ #E >E >lookup_add_hit @I
    782 | #NE >lookup_add_miss [ @H | /2/
     805[ #E @False_ind >E in H; whd in ⊢ (% → ?);
     806  whd in ⊢ (match % with [_⇒ ?|_⇒ ?] → ?); cases id' in F ⊢ %; #id'
     807  #F whd in F; >F *
     808| #NE >lookup_add_miss [ @H | // ]
     809] qed.
     810
     811(*
     812lemma local_id_add_tmps_oblivious : ∀vars,id,ty,u.
     813  local_id vars id ty → local_id (add_tmps vars (tmp_env vars u)) id ty.
     814#vars #id #ty * #u #l #F #H elim l
     815[ //
     816| * #id' #ty' #tl @local_id_add_local_oblivious @F
    783817] qed.
    784818*)
    785819
    786 (* XXX freshness XXX *)
    787 axiom local_id_add_tmps_oblivious : ∀vars,id,ty,u.
    788   local_id vars id ty → local_id (add_tmps vars u) id ty.
    789 (*
    790 #vars #id * #u #l #H elim l
    791 [ //
    792 | * #id' #ty #tl @local_id_add_local_oblivious
    793 ] qed.
    794 *)
    795 
    796820lemma add_tmps_oblivious : ∀vars,lbls,s,u.
    797   stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s.
     821  stmt_inv vars lbls s → stmt_inv (add_tmps vars (tmp_env vars u)) lbls s.
    798822#vars #lbls #s #u #H
    799823@(stmt_P_mp … H)
    800824#s' * #H1 #H2 %
    801825[ @(stmt_vars_mp … H1)
    802   #id #t @local_id_add_tmps_oblivious
     826  #id #t @(tmp_preserved ? u)
    803827| @H2
    804828] qed.
    805829
    806 lemma local_id_fresh_tmp : ∀tmp,u,ty,u0,vars.
    807   〈tmp,u〉 = alloc_tmp ty u0 → local_id (add_tmps vars u) tmp (typ_of_type ty).
    808 #tmp #u #ty #u0 #vars
    809 whd in ⊢ (???% → ?); #E
     830lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0.
     831  〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty).
     832#vars #tmp #u #ty #u0
     833whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?);
     834cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?);
     835* #tmp' #u' #e #E whd in E:(???%);
    810836destruct
    811837whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
     
    813839qed.
    814840
    815 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝
    816 match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with
     841let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen vars) (s:statement) on s : res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) ≝
     842match s return λs.res (Σsu:stmt×(tmpgen vars).trans_inv vars lbls s u su) with
    817843[ Sskip ⇒ OK ? «〈St_skip, u〉, ?»
    818844| Sassign e1 e2 ⇒
     
    830856        [ IdDest id ty p ⇒ OK ? «〈St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?»
    831857        | MemDest r q e1' ⇒
    832             let 〈tmp, u〉 as Etmp ≝ alloc_tmp (typeof e1) u in
     858            let 〈tmp, u〉 as Etmp ≝ alloc_tmp ? (typeof e1) u in
    833859            OK ? «〈St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?»
    834860        ]
     
    909935try (#id #ty #H @H)
    910936[ @add_tmps_oblivious @(pi2 ?? s')
    911 | @local_id_add_tmps_oblivious @p
     937| @(tmp_preserved … u) @p
    912938]
    913 try (@sub_pi2 #x @expr_vars_mp #i #ty @local_id_add_tmps_oblivious)
    914 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @local_id_add_tmps_oblivious
     939try (@sub_pi2 #x @expr_vars_mp #i #ty @(tmp_preserved … u))
     940[ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @(tmp_preserved … u)
    915941| 2,4: @(local_id_fresh_tmp … Etmp)
    916942| @(alloc_tmp_preserves … Etmp)
     
    960986
    961987(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
    962 definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝
     988definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×(tmpgen vars). trans_inv vars ls s0 u su) → res (Σsu:stmt×(tmpgen vars).trans_inv vars ls s0 u su) ≝
    963989λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
    964990  let 〈id,ty〉 ≝ it in
     
    966992  do 〈t,ty'〉 as E ← lookup' vars id;
    967993  match t return λx.? → ? with
    968   [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
     994  [ Local ⇒ λE. OK (Σs:stmt×(tmpgen vars).?) «〈s,u〉,Is»
    969995  | Stack n ⇒ λE.
    970996      do q ← match access_mode ty with
     
    9781004try @conj try @conj try @conj try @conj try @conj try @conj
    9791005try @I
    980 [ @(expr_vars_mp … (λid,ty. local_id_add_tmps_oblivious vars id ty u)) whd >E @refl
     1006[ @(expr_vars_mp … (tmp_preserved … u)) whd >E @refl
    9811007| @(π1 (π1 Is))
    9821008| @(π2 (π1 Is))
     
    10471073
    10481074lemma local_id_split : ∀vars,tmpgen,i,t.
    1049   local_id (add_tmps vars tmpgen) i t →
    1050   local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env tmpgen).
     1075  local_id (add_tmps vars (tmp_env vars tmpgen)) i t →
     1076  local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env tmpgen).
    10511077#vars #tmpgen #i #t
    10521078whd in ⊢ (?%?? → ?);
    1053 elim (tmp_env tmpgen)
     1079elim (tmp_env vars tmpgen)
    10541080[ #H %1 @H
    10551081| * #id #ty #tl #IH
     
    10771103  do «lbls, Ilbls» ← build_label_env (fn_body f);
    10781104  let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
    1079   let tmp ≝ mk_tmpgen tmpuniverse [ ] in
     1105  let tmp ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
    10801106  do s ← translate_statement vartypes lbls tmp (fn_body f);
    10811107   do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
     
    10831109    (opttyp_of_type (fn_return f))
    10841110    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    1085     ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env tmp @ fn_vars f)))
     1111    ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f)))
    10861112    stacksize
    10871113    s ?).
    1088 cases Is * #S #L #TP
    1089 @(stmt_P_mp ???? S)
    1090 #s1 * #H1 #H2 %
    1091 [ @(stmt_vars_mp … H1)
    1092   #i #t #H
    1093   cases (local_id_split … H)
    1094   [ #H' >map_append
    1095     @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H'
    1096                 | skip
    1097                 | * #id #ty * #E1 #E2 <E1 <E2 @refl
    1098                 ]
    1099   | #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
    1100   ]
    1101 | @(stmt_labels_mp … H2)
    1102   #l * #l' #LOOKUP
    1103   lapply (Ilbls l' l LOOKUP) #DEFINED
    1104   cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
    1105   #H @H
     1114[ //
     1115| (* FIXME *) cases daemon
     1116| cases Is * #S #L #TP
     1117  @(stmt_P_mp ???? S)
     1118  #s1 * #H1 #H2 %
     1119  [ @(stmt_vars_mp … H1)
     1120    #i #t #H
     1121    cases (local_id_split … H)
     1122    [ #H' >map_append
     1123      @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H'
     1124                  | skip
     1125                  | * #id #ty * #E1 #E2 <E1 <E2 @refl
     1126                  ]
     1127    | #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
     1128    ]
     1129  | @(stmt_labels_mp … H2)
     1130    #l * #l' #LOOKUP
     1131    lapply (Ilbls l' l LOOKUP) #DEFINED
     1132    cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
     1133    #H @H
     1134  ]
    11061135] qed.
    11071136
  • src/common/Identifiers.ma

    r1601 r1627  
    2020  λtag. mk_universe tag one.
    2121
    22 (* Fresh identifier generation uses delayed overflow checking.  To make sure
    23    that the identifiers really were fresh, use the check_universe_ok function
    24    below afterwards. *)
    25 definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
    26   λtag.
    27   λuniv: universe tag.
    28   let id ≝ next_identifier ? univ in
     22let rec fresh (tag:String) (u:universe tag) on u : identifier tag × (universe tag) ≝
     23  let id ≝ next_identifier ? u in
    2924  〈an_identifier tag id, mk_universe tag (succ id)〉.
     25
     26
     27let rec fresh_for_univ tag (id:identifier tag) (u:universe tag) on id : Prop ≝
     28  match id with [ an_identifier p ⇒ p < next_identifier … u ].
     29
     30
     31lemma fresh_is_fresh : ∀tag,id,u,u'.
     32  〈id,u〉 = fresh tag u' →
     33  fresh_for_univ tag id u.
     34#tag * #id * #u * #u' #E whd in E:(???%); destruct //
     35qed.
     36
     37lemma fresh_remains_fresh : ∀tag,id,id',u,u'.
     38  fresh_for_univ tag id u →
     39  〈id',u'〉 = fresh tag u →
     40  fresh_for_univ tag id u'.
     41#tag * #id * #id' * #u * #u' normalize #H #E destruct /2/
     42qed.
     43
     44lemma fresh_distinct : ∀tag,id,id',u,u'.
     45  fresh_for_univ tag id u →
     46  〈id',u'〉 = fresh tag u →
     47  id ≠ id'.
     48#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2/
     49qed.
     50
     51
     52let rec env_fresh_for_univ tag A (env:list (identifier tag × A)) (u:universe tag) on u : Prop ≝
     53  All ? (λida. fresh_for_univ tag (\fst ida) u) env.
     54
     55lemma fresh_env_extend : ∀tag,A,env,u,u',id,a.
     56  env_fresh_for_univ tag A env u →
     57  〈id,u'〉 = fresh tag u →
     58  env_fresh_for_univ tag A (〈id,a〉::env) u'.
     59#tag #A #env * #u * #u' #id #a
     60#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
     61qed.
     62
    3063
    3164definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     
    226259] qed.
    227260
     261
     262let rec fresh_for_map tag A (id:identifier tag) (m:identifier_map tag A) on id : Prop ≝
     263  lookup … m id = None A.
     264
     265definition fresh_map_for_univ ≝
     266λtag,A. λm:identifier_map tag A. λu:universe tag.
     267  ∀id. present tag A m id → fresh_for_univ tag id u.
     268
     269lemma fresh_fresh_for_map : ∀tag,A,m,id,u,u'.
     270  fresh_map_for_univ tag A m u →
     271  〈id,u'〉 = fresh tag u →
     272  fresh_for_map tag A id m.
     273#tag #A * #m * #id * #u * #u' whd in ⊢ (% → ???% → %);
     274#FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
     275generalize in ⊢ ((?(??%?) → ?) → ??%?); *
     276[ // | #a #H @False_ind lapply (H ?) /2/ % #E destruct
     277qed.
     278
     279lemma fresh_map_preserved : ∀tag,A,m,u,u',id.
     280  fresh_map_for_univ tag A m u →
     281  〈id,u'〉 = fresh tag u →
     282  fresh_map_for_univ tag A m u'.
     283#tag #A #m #u * #u' #id whd in ⊢ (% → ? → %); #H #E
     284#id' #PR @(fresh_remains_fresh … E) @H //
     285qed.
     286
     287lemma fresh_map_add : ∀tag,A,m,u,id,a.
     288  fresh_map_for_univ tag A m u →
     289  fresh_for_univ tag id u →
     290  fresh_map_for_univ tag A (add tag A m id a) u.
     291#tag #A * #m #u #id #a #Hm #Hi
     292#id' #PR cases (identifier_eq tag id' id)
     293[ #E >E @Hi
     294| #NE @Hm whd in PR;
     295  change with (add tag A (an_id_map tag A m) id a) in PR:(?(??(???%?)?));
     296  >lookup_add_miss in PR; //
     297] qed.
     298
     299lemma present_not_fresh : ∀tag,A,m,id,id'.
     300  present tag A m id →
     301  fresh_for_map tag A id' m →
     302  id ≠ id'.
     303#tag #A #m #id * #id' whd in ⊢ (% → % → ?);
     304* #NE #E % #E' destruct @(NE E)
     305qed.
     306
    228307(* Sets *)
    229308
Note: See TracChangeset for help on using the changeset viewer.