Ignore:
Timestamp:
May 24, 2012, 9:35:08 AM (8 years ago)
Author:
campbell
Message:

Get rid of unused abstraction of Globalenvs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1920 r1986  
    1212include "RTLabs/syntax.ma".
    1313
    14 definition genv ≝ (genv_t Genv) (fundef internal_function).
     14definition genv ≝ genv_t (fundef internal_function).
    1515
    1616record frame : Type[0] ≝
     
    122122      return 〈E0, build_state f fs m' l ?〉
    123123  | St_call_id id args dst l ⇒ λH.
    124       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    125       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     124      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ge id);
     125      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ge b);
    126126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    127127      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    128128  | St_call_ptr frs args dst l ⇒ λH.
    129129      ! fv ← reg_retrieve (locals f) frs;
    130       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
     130      ! fd ← opt_to_res … (msg BadFunction) (find_funct ge fv);
    131131      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    132132      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     
    221221
    222222definition make_global : RTLabs_program → genv ≝
    223 λp. globalenv Genv ?? (λx.[Init_space x]) p.
     223λp. globalenv (λx.[Init_space x]) p.
    224224
    225225definition make_initial_state : RTLabs_program → res state ≝
    226226λp.
    227227  let ge ≝ make_global p in
    228   do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     228  do m ← init_mem (λx.[Init_space x]) p;
    229229  let main ≝ prog_main ?? p in
    230   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    231   do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
     230  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ge main);
     231  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ge b);
    232232  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
    233233
     
    249249inductive state_rel : genv → state → state → Prop ≝
    250250| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
    251 | to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
     251| to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
    252252(*
    253253| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
     
    283283  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    284284  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
    285   | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    286   | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     285  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ???) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
     286  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ???) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    287287(*
    288288  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
Note: See TracChangeset for help on using the changeset viewer.