%
% types for a byte-writeable ram
% consisting of B (2^k x 8)-banks
%

bw_ram_types[k:nat, B:posnat]: THEORY
BEGIN
  IMPORTING 
    ram

% types for address and dataword vectors
  bw_ram_bankt    : TYPE+ = below(B);
  bw_ram_bank_wet : TYPE+ = bvec[B];
  bw_ram_wordt    : TYPE+ = bvec[8*B];
  bw_ram_addresst : TYPE+ = bvec[k];

% bw_ramt implements the bw_ram
  bw_ramt : TYPE+ = [below(B) -> ramt[k,8]];
END bw_ram_types