Changeset 1999 for src/common


Ignore:
Timestamp:
May 25, 2012, 10:45:15 AM (8 years ago)
Author:
campbell
Message:

Make back-end use the main global envs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1994 r1999  
    196196  \fst (globalenv_allocmem F V i p).
    197197
     198(* Return the global environment for the given program with no data initialisation. *)
     199definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
     200λF,p.
     201  \fst (globalenv_allocmem F nat (λn.[Init_space n]) p).
     202
    198203(* Return the initial memory state for the given program. *)
    199204definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝
     
    201206  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
    202207  init_globals ? V i g m (prog_vars ?? p).
     208
     209(* Setup memory when data initialisation is not required (has the benefit
     210   of being total. *)
     211definition alloc_mem: ∀F. program F nat → mem ≝
     212λF,p.
     213  \snd (globalenv_allocmem F nat (λn. [Init_space n]) p).
    203214
    204215(* Return the function description associated with the given address, if any. *)
Note: See TracChangeset for help on using the changeset viewer.