library CaseStudies/PuCache/PuCacheData version 0.1

from Basic/StructuredDatatypes version 0.7 get Map
from Basic/StructuredDatatypes version 0.7 get List
from CaseStudies/Misc/Haskell version 0.1 get Maybe
from CaseStudies/PuCache/PFS_Protocol get PFS_Protocol

spec PuCacheData = 
  PFS_Protocol 
and
  Map[sort Uid fit sort S |-> Uid]
	   [sort PuUserEntry fit sort T |-> PuUserEntry] 
and
  Map[sort Filehandle fit sort S |-> Filehandle]
           [sort PuFileEntry fit sort T |-> PuFileEntry] 
and
  Map [sort Filehandle fit sort S |-> Filehandle]
            [sort PuDirEntry fit sort T |-> PuDirEntry]
and
  Map [sort Filename fit sort S |-> Filename]
            [sort Filehandle fit sort T |-> Filehandle]
and 
  List [sort PFS_Command fit sort Elem |-> PFS_Command]
and
  Maybe [sort Path fit sort Elem |-> Path]
then

%%-----------------------------------------------------------------------------
%%-- ****h* PU/PuCacheData
%%-- NAME
%%--    PuCacheDate -- datatypes for the cache
%%-- DESCRIPTION
%%--    This module contains the datatypes used by PU's cache
%%--    Haskells Word64 replaced by CASLs Int
%%--    ! No idea what to do with 'deriving' statements
%%-- ***
%%-----------------------------------------------------------------------------
%%-- $Id
%%-----------------------------------------------------------------------------

free type PuCache ::= PuCache ( puc_getOffline   : Boolean;
			 puc_globalQuota  : Int;
			 puc_globalSafety : Int;
			 puc_maxUsers     : Int;
			 puc_cacheDir     : Path;
			 puc_conflictDir  : Path;
                         puc_getUserData  : Map[Uid,PuUserEntry] )
%% deriving Eq 

free type PuUserEntry ::= PuUserEntry ( puc_userOffline     : Boolean;
                          puc_userRefresh     : Time;
                          puc_userOfflineList : OfflineList;
			  puc_userQuota       : Int;
			  puc_userSafety      : Int;
                          puc_userSpace       : Int;
			  puc_userLastFh      : Int;
		          puc_userQueue       : List[PFS_Command];
                          puc_getDirData      : Map[Filehandle, PuDirEntry];
                          puc_getFileData     : Map[Filehandle, PuFileEntry])
%%                   deriving Eq

free type  PuDirEntry ::= PuDirEntry ( puc_dirName    : Path;
                               puc_dirAttr    : Attributes;
                               puc_dirExtAttr : ExtAttributes;
                               puc_dirSubDirs : Map[Filename, Filehandle];
                               puc_dirFiles   : Map[Filename, Filehandle];
			       puc_dirGen     : Int;
                               puc_dirChanged : Boolean )
%%                  deriving Eq

free type  PuFileEntry ::= PuFileEntry ( puc_fileServerTime : Time;
                                 puc_fileCachedName : Path;
                                 puc_fileAttr       : Attributes;
                                 puc_fileExtAttr    : ExtAttributes;
				 puc_fileSymlink    : Maybe[Path];
                                 puc_fileChanged    : Boolean )
%%                   deriving (Eq,Ord,Show,Read)

ops
  pu_EOK: Errno;
  pu_ESTALE : Errno;
  pu_EACCES : Errno;
  pu_EINVAL : Errno;

op puc_emptyCache : PuCache;
axiom
puc_emptyCache = PuCache(True, 0, 0, 0, "", "", empty)