Changeset 1102 for Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
 Timestamp:
 Aug 4, 2011, 1:55:53 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
r1101 r1102 3 3 include "Cminor/syntax.ma". 4 4 include "RTLabs/syntax.ma". 5 include "utilities/pair.ma". 6 include "utilities/deppair.ma". 5 7 6 8 definition env ≝ identifier_map SymbolTag register. … … 77 79 ] qed. 78 80 79 lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?).80 lookup tag A m i ≠ None ?.81 #tag #A #m * #i #H @H82 qed.83 84 81 definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝ 85 82 λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r  None ⇒ λH.⊥ ]. … … 98 95 (f_stacksize f) (add ?? (f_graph f) l s) 99 96 (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). 100 @lookup_add_oblivious @ lookup_sigma97 @lookup_add_oblivious @use_sig 101 98 qed. 102 99 … … 109 106 (dp ?? l ?) (dp ?? (f_exit f) ?). 110 107 [ >lookup_add_hit % #E destruct 111  @lookup_add_oblivious @ lookup_sigma108  @lookup_add_oblivious @use_sig 112 109 ] qed. 113 110 … … 123 120 (dp ?? l ?) (dp ?? (f_exit f) ?)). 124 121 [ >lookup_add_hit % #E destruct 125  @lookup_add_oblivious @ lookup_sigma122  @lookup_add_oblivious @use_sig 126 123 ] qed. 127 124 … … 235 232 axiom ReturnMismatch : String. 236 233 237 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"238 with precedence 10239 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒240 λ${ident E}.$s ] (refl ? $t) }.241 242 234 definition stmt_inv : env → label_env → stmt → Prop ≝ 243 235 λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s). 244 245 notation "π1" with precedence 10 for @{ (proj1 ??) }.246 notation "π2" with precedence 10 for @{ (proj2 ??) }.247 236 248 237 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (exits:list label) (f:internal_function) on s : res internal_function ≝ … … 358 347 ] qed. 359 348 360 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"361 with precedence 10362 for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒363 match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒364 λ${ident E}.$s ] ] (refl ? $t) }.365 366 349 367 350 definition c2ra_function (*: internal_function → internal_function*) ≝
Note: See TracChangeset
for help on using the changeset viewer.