Ignore:
Timestamp:
Jan 25, 2011, 5:30:37 PM (9 years ago)
Author:
campbell
Message:

"memory_space" to "region" replacement to match ocaml code

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/AST.ma

    r478 r480  
    107107(* Memory spaces *)
    108108
    109 ninductive memory_space : Type ≝
    110   | Any : memory_space
    111   | Data : memory_space
    112   | IData : memory_space
    113   | PData : memory_space
    114   | XData : memory_space
    115   | Code : memory_space.
     109ninductive region : Type ≝
     110  | Any : region
     111  | Data : region
     112  | IData : region
     113  | PData : region
     114  | XData : region
     115  | Code : region.
    116116
    117117(* * Initialization data for global variables. *)
     
    142142  prog_funct: list (ident × F);
    143143  prog_main: ident;
    144   prog_vars: list (ident × (list init_data) × memory_space × V)
     144  prog_vars: list (ident × (list init_data) × region × V)
    145145}.
    146146
     
    149149
    150150ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
    151   map ?? (λx: ident × (list init_data) × memory_space × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     151  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
    152152(*
    153153(** * Generic transformations over programs *)
Note: See TracChangeset for help on using the changeset viewer.