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).

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.