Ignore:
Timestamp:
Aug 4, 2011, 1:55:53 PM (9 years ago)
Author:
campbell
Message:

Tidy up branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1101 r1102  
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
     5include "utilities/pair.ma".
     6include "utilities/deppair.ma".
    57
    68definition env ≝ identifier_map SymbolTag register.
     
    7779] qed.
    7880
    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 @H
    82 qed.
    83 
    8481definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
    8582λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
     
    9895                       (f_stacksize f) (add ?? (f_graph f) l s)
    9996                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
    100 @lookup_add_oblivious @lookup_sigma
     97@lookup_add_oblivious @use_sig
    10198qed.
    10299
     
    109106                       (dp ?? l ?) (dp ?? (f_exit f) ?).
    110107[ >lookup_add_hit % #E destruct
    111 | @lookup_add_oblivious @lookup_sigma
     108| @lookup_add_oblivious @use_sig
    112109] qed.
    113110
     
    123120                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
    124121[ >lookup_add_hit % #E destruct
    125 | @lookup_add_oblivious @lookup_sigma
     122| @lookup_add_oblivious @use_sig
    126123] qed.
    127124
     
    235232axiom ReturnMismatch : String.
    236233
    237 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
    238  with precedence 10
    239 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
    240         λ${ident E}.$s ] (refl ? $t) }.
    241 
    242234definition stmt_inv : env → label_env → stmt → Prop ≝
    243235λ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 ??) }.
    247236
    248237let 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 ≝
     
    358347] qed.
    359348
    360 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    361  with precedence 10
    362 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 
    366349
    367350definition c2ra_function (*: internal_function → internal_function*) ≝
Note: See TracChangeset for help on using the changeset viewer.