Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Mon, 13 Apr 92 23:17:05 MDT
From: slind@ca.ucalgary.cpsc (Konrad Slind)
Message-Id: <9204140517.AA17943@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted

Tim Leonard poses an excellent problem by raising the issue of how to
do a thorough job of computer words. As he says, this is an application
tailor-made for abstract theories (abstract libraries, really). 

First, though, I would suggest writing a MK_WORDN functor in Standard
ML. The writing down of the signatures for its argument structure and
its returned structure will serve to focus discussion. Also, the functor
provides a quick prototype that should be easily (Ha!) transferable to
an implementation of abstract theories.

As a thumbnail sketch:

datatype endian = big_endian | little_endian;

functor MK_WORDN(val word_size : int
                 val byte_size : int
                 val name : string
                 val fields : int list
                 val endianess : endian) : WORDN_LIB_SIG = 
struct
exception MK_WORDN_ERR of string

structure Wordn_bool = 
struct
  type wordn = array of bool
  type byte = array of bool
  fun mk_word() = array(size,true);
  fun list_to_wordn alist = if (alist = size)
                            then arrayoflist alist
                            else raise MK_WORDN_ERR "list_to_wordn"
    .
    .
    .
end

structure Wordn_mod_num =
struct   ....   end

    .
    .
    .

end; (* MK_WORDN *)

where the result signature, WORDN_LIB_SIG, is something like

signature WORDN_LIB_SIG =
sig
  structure Wordn_bool : WORDN_BOOL_SIG
  structure Wordn_mod_num : WORDN_MOD_NUM_SIG
  structure Wordn_mod_int : WORDN_MOD_INT_SIG
  structure Wordn_radix : WORDN_RADIX_SIG
  structure Wordn_mod_fp : WORDN_MOD_FP_SIG
end;

and WORDN_BOOL_SIG is something like

signature WORDN_BOOL_SIG =
sig
  type wordn
  type byte

  val mk_word : unit -> wordn
  val list_to_wordn : bool list -> wordn
  val wordn_to_list : wordn -> bool list

  (* Word operations *)
  val rotate_left : wordn -> wordn
  val rotate_right : wordn -> wordn
  val shift_right : wordn -> wordn
  val shift_right : wordn -> wordn
  val extract_field : {left_index : int, right_index : int} -> wordn -> wordn
  val insert_field : {left_index : int, right_index : int} -> 
                     wordn -> wordn -> wordn

  (* Words and bytes *)
  val unpack : wordn -> byte list
  val pack : byte list -> wordn

  (* Logical ops *)
  val AND : wordn -> wordn -> wordn
  val OR  : wordn -> wordn -> wordn
  val XOR : wordn -> wordn -> wordn
  val TWOS_COMPL : wordn -> wordn -> wordn

  (* Comparison ops *)

    .
    .
    .
end;

From there, you can define the operations that take words to various types of 
numbers. For example,

signature WORDN_MOD_NUM_SIG =
sig
  type wordn

  (* Mapping functions *)
  val wordn_to_num : wordn -> int
  val num_to_wordn : int -> wordn 

  (* Arithmetic ops *)
  val ADD : wordn -> wordn -> int
  val SUB : wordn -> wordn -> int
  val MUL : wordn -> wordn -> int
  val MUL_HIGH : wordn -> wordn -> int
  val DIV : wordn -> wordn -> int
  val EXP : wordn -> wordn -> int

  (* Arithmetic ops that check overflow. *)
  type psr (* processor status register *)
  val ADD_E : wordn -> wordn -> psr -> (int * psr)
  val SUB_E : wordn -> wordn -> psr -> (int * psr)
  val MUL_E : wordn -> wordn -> psr -> (int * psr)
  val MUL_HIGH_E : wordn -> wordn -> psr -> (int * psr)
  val DIV_E : wordn -> wordn -> psr -> (int * psr)
  val EXP_E : wordn -> wordn -> psr -> (int * psr)

    .
    .
    .
end;


This approach can help organize the package properly, much more so than
talking about library structure. As far as I know, libraries in hol88
have no good structuring facility.

Konrad.