Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (9 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1139 r1224  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
     54  globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. res (genv_t (F (prog_var_names … p)));
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
     57  init_mem: ∀F,V. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    502502    (OK ? init_env) vars.
    503503
    504 definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     504definition globalenv_initmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. res (genv (F (prog_var_names … p)) × mem) ≝
    505505λF,V,init_info,p.
    506   add_globals F V init_info
     506  add_globals init_info
    507507   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508508   (prog_vars ?? p).
    509509
    510 definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     510definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. res (genv (F (prog_var_names … p))) ≝
    511511λF,V,i,p.
    512512  do 〈g,m〉 ← globalenv_initmem F V i p;
    513513    OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     514definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝
    515515λF,V,i,p.
    516516  do 〈g,m〉 ← globalenv_initmem F V i p;
Note: See TracChangeset for help on using the changeset viewer.