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

Tidy up branch

Location:
Deliverables/D3.3/id-lookup-branch/Cminor
Files:
3 edited

Legend:

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

    r1101 r1102  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
     6include "utilities/pair.ma".
     7include "utilities/deppair.ma".
    68
    79(* XXX having to specify the return type in the match is annoying. *)
     
    3941qed.
    4042
    41 lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
    42   let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
    43 #A #B #C #D * // qed.
    44 
    45 lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
    46   R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
    47 #A #B #C #D *; normalize /2/
    48 qed.
    49 
    50 lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
    51   stmt_inv s.
    52 * #s #p @p
    53 qed.
    54 
    5543definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
    5644λid,r,init.
     
    6351| elim init
    6452  [ % //
    65   | #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % // | @sig_stmt_inv ] | @IH ]
     53  | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
    6654] qed.
    6755
     
    6957λvars. foldr ? (Σs:stmt. stmt_inv s)
    7058  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    71 % [ % [ % // | @sig_stmt_inv ] | @sig_stmt_inv ]
     59% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
    7260qed.
    7361
  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r961 r1102  
    106106].
    107107
    108 let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
     108let rec find_label (l:identifier Label) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
    109109match s with
    110110[ St_seq s1 s2 ⇒
     
    121121| St_block s' ⇒ find_label l s' (Kblock k)
    122122| St_label l' s' ⇒
    123     match ident_eq l l' with
     123    match identifier_eq ? l l' with
    124124    [ inl _ ⇒ Some ? 〈s',k〉
    125125    | inr _ ⇒ find_label l s' k
  • 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.