Changeset 1986 for src/Cminor


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/Cminor/semantics.ma

    r1878 r1986  
    99
    1010definition env ≝ identifier_map SymbolTag val.
    11 definition genv ≝ (genv_t Genv) (fundef internal_function).
     11definition genv ≝ genv_t (fundef internal_function).
    1212
    1313definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
     
    314314    | St_call dst ef args ⇒ λInv.
    315315        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    316         ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
     316        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ge vf);
    317317        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    318318        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     
    447447
    448448definition make_global : Cminor_program → genv ≝
    449 λp. globalenv Genv ?? (λx.x) p.
     449λp. globalenv (λx.x) p.
    450450
    451451definition make_initial_state : Cminor_program → res state ≝
    452452λp.
    453453  let ge ≝ make_global p in
    454   do m ← init_mem Genv ?? (λx.x) p;
    455   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    456   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     454  do m ← init_mem (λx.x) p;
     455  do b ← opt_to_res ? (msg MainMissing) (find_symbol ge (prog_main ?? p));
     456  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ge b);
    457457  OK ? (Callstate f (nil ?) m SStop).
    458458
     
    461461
    462462definition make_noinit_global : Cminor_noinit_program → genv ≝
    463 λp. globalenv Genv ?? (λx.[Init_space x]) p.
     463λp. globalenv (λx.[Init_space x]) p.
    464464
    465465definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
    466466λp.
    467467  let ge ≝ make_noinit_global p in
    468   do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    469   do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    470   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     468  do m ← init_mem (λx.[Init_space x]) p;
     469  do b ← opt_to_res ? (msg MainMissing) (find_symbol ge (prog_main ?? p));
     470  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ge b);
    471471  OK ? (Callstate f (nil ?) m SStop).
    472472
Note: See TracChangeset for help on using the changeset viewer.