(* $Header: /users/lal/black/hol/Disser/RCS/state.sml,v 1.7 1997/06/20 14:51:54 black Exp $ *)
(* *created  "Thu Apr  4 14:50:04 1996" *by "Paul E. Black" *)
(* *modified "Tue Jun 17 15:53:59 1997" *by "Paul E. Black" *)

(*---------------------------------------------------------------------------
	Types which describe the state of a (Unix) file system and 
	(Unix) processes.
 ----------------------------------------------------------------------------*)

(* this uses Phil Windley's "records" package - preloaded in LAL extensions *)

create_record "unixFile"
   [("permissions", ==`:'permission`==),
    ("contents",    ==`:'fscontents`==)];

(*-----------
  This creates theorems unixFile_Update_commute_thms,
  unixFile_selectors_work, unixFile_cases, unixFile_one_one,
  Update_unixFile_thm, unixFile_updates, and unixFile_selectors.
  These can be retrieved with
    val theThm = theorem "-" "unixFile_selectors";
 ------------*)

(* a file is the permissions and the contents.  New files are declared
   as (--`theFile:^unixFile`--); *)
val unixFile = ty_antiq (==`:('permission,'fscontents)unixFile`==);

(* for recursive definitions, we need an inductive definition of unix
   files.  This one begins with an empty file and appends strings to it. *)
new_constant {
   Name="empty_unixFile", Ty=(==`:^unixFile`==)
};

new_constant {
   Name="appendFile", Ty=(==`:string -> ^unixFile -> ^unixFile`==)
};

(* state the recurrence relation as an axiom for now *)
val unixFile_Axiom = mk_thm([],
  (--`!e f. ?!fn.
	(fn (empty_unixFile:^unixFile) = (e:'a)) /\
	(!n o. fn (appendFile n o) = f (fn o) n o)`--));


(*
  SKIMP - In Unix terms, a "file system" is just one volume, partition, or
  disk.  We really want to verify over everything in the read/write space
  since the program may have access to several file systems and devices.
  In particular, STDOUT doesn't even have an inode!
*)

(* a file system is (a list of) files designated by inode numbers *)
(* SKIMP - names, directories, and paths *)
val unixFileSystem = ty_antiq (==`:(^unixFile # num) CArray`==);

(* define the function which maps names to inode numbers *)
(* SKIMP - this must refer to the current working directory *)
new_constant{Name = "inodeNamed", Ty = ==`:string -> num`==};

(* define the function which maps inode numbers to files in a file system *)
new_constant {
  Name="getFile", Ty=(==`:^unixFileSystem -> num -> ^unixFile`==)
};

(* define the distinguished "file" STDOUT *)
new_constant {Name="SYS_stdout", Ty = ==`:num`==};

(* define predicates on the State of the File System.  We can
   use this to define a state before code execution. *)
val SoFS = new_definition (
   "SoFS",
   (--`! P (fs:^unixFileSystem) .
	SoFS P fs = (!inode. P inode (getFile fs inode))`--)
);

(* define THE file system *)
val SYS_FileSystem = (--`SYS_FileSystem:^unixFileSystem`--);

(* end of $Source: /users/lal/black/hol/Disser/RCS/state.sml,v $ *)