Changeset 2460


Ignore:
Timestamp:
Nov 13, 2012, 6:30:56 PM (7 years ago)
Author:
campbell
Message:

Rest of variable characterisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2458 r2460  
    130130  ]
    131131] qed.
     132
     133(* Local variables show up in the variable characterisation as local. *)
     134
     135lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
     136  characterise_vars globals f = 〈vartypes, stacksize〉 →
     137  Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
     138  ∃t. local_id vartypes id t.
     139#globals * #ret #args #vars #body
     140whd in match (characterise_vars ??); elim (args@vars)
     141[ #vartypes #stacksize #id #_ *
     142| * #hd #ty #tl #IH
     143  #vartypes #stacksize #id
     144  whd in match (foldr ?????);
     145  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
     146  #vartypes' #stackspace' #IH
     147  whd in ⊢ (??(match % with [_⇒?])? → ?);
     148  cases (orb ??)
     149  #E whd in E:(??%?); destruct *
     150  [ 1,3: #E destruct %{(typ_of_type ty)}
     151    whd whd in match (lookup' ??); >lookup_add_hit //
     152  | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
     153    cases (identifier_eq ? id hd)
     154    [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
     155    | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
     156    ]
     157  ]
     158] qed.
     159
     160(* Put knowledge that Globals are global into a more useful form than the
     161   one used for the invariant. *)
     162
     163lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
     164  characterise_vars globals f = 〈vartypes, stacksize〉 →
     165  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
     166  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
     167  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
     168#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
     169cases (characterise_vars_src … CHAR id ?)
     170[ * #r' * #ty' >L
     171  * #E1 destruct (E1) #EX
     172  %
     173  [ @EX
     174  | % #EX' cases (characterise_vars_localid … CHAR EX')
     175    #ty' whd in ⊢ (% → ?); >L *
     176  ]
     177| * #ty' whd in ⊢ (% → ?); >L *
     178| whd >(opt_eq_from_res ???? L) % #E destruct
     179] qed.
Note: See TracChangeset for help on using the changeset viewer.