Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2682 r2722  
    8787 ]
    8888| #v #ty #b #o #tr #EX #u %{tr} % [
    89     whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
     89    whd in EX:(??%?) ⊢ (??%?); cases (lookup SymbolTag ?? v) in EX ⊢ %;
    9090    [ whd in ⊢ (??%? → ??%?); >(rgg_find_symbol … RG) //
    9191    | #b // ]
     
    407407qed.
    408408
    409 lemma opt_find_funct : ∀ge,ge',m,vf,fd.
     409lemma opt_find_funct : ∀ge,ge',m,vf,fd,id.
    410410  related_globals_gen … label_fundef ge ge' →
    411   opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd
    412   ∃u. opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (\fst (label_fundef u fd)).
    413 #ge #ge' #m #vf #fd #RG
    414 lapply (rgg_find_funct … RG … vf fd)
    415 cases (find_funct … vf)
     411  opt_to_io io_out io_in … m (find_funct_id … ge vf) = Value … 〈fd,id〉
     412  ∃u. opt_to_io io_out io_in … m (find_funct_id … ge' vf) = Value … 〈\fst (label_fundef u fd), id〉.
     413#ge #ge' #m #vf #fd #id #RG
     414lapply (rgg_find_funct_id … RG … vf fd)
     415cases (find_funct_id … vf)
    416416[ #_ #E normalize in E; destruct
    417 | #fd' #H #E normalize in E; destruct cases (H (refl ??)) #u #FF %{u} >FF //
     417| * #fd' #id' #H #E normalize in E; destruct cases (H ? (refl ??)) #u #FF %{u} >FF //
    418418] qed.
    419419
     
    768768    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    769769    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
    770     cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
     770    cases (bindIO_inversion ??????? EX) -EX * #fd #fid * #EX3 #EX
    771771    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
    772772    whd in EX:(??%%);
     
    910910    cases v1 in EX1 EX;
    911911    [ 2: #sz #i #EX1 #EX
    912     | *: normalize #A #B try #C destruct
     912    | *: [ 3: #x ] #A whd in ⊢ (??%% → ?); #B destruct
    913913    ]
    914914    whd in EX:(??%%); cases ty in EX1 EX ⊢ %; normalize nodelta #sz' try #sg try #EX1 try #EX destruct
Note: See TracChangeset for help on using the changeset viewer.