Implementation of Array data type in OCaml

Question

I have very little knowledge about OCaml as a whole and just received an assignment to take one of the source files in the project and allow it to take a new data type (Array). I am not asking for someone to solve this problem for me, but instead I would appreciate someone walking me through this code. I would also appreciate any input on how difficult it is going to be to implement this new data type.

The file itself lacks a lot of documentation which doesn't make it any easier either.

(* * Types (hashconsed) *)

(* ** Imports *)
open Abbrevs
open Util

(* ** Identifiers *)

module Lenvar : (module type of Id) = Id

module Tysym : (module type of Id) = Id

module Groupvar : (module type of Id) = Id

module Permvar : (module type of Id) = Id


(* ** Types and type nodes *)

type ty = {
  ty_node : ty_node;
  ty_tag : int
}
and ty_node =
  | BS of Lenvar.id
  | Bool
  | G of Groupvar.id
  | TySym of Tysym.id
  | Fq
  | Prod of ty list
  | Int

(* ** Equality, hashing, and hash consing *)

let equal_ty : ty -> ty -> bool = (==)
let hash_ty t = t.ty_tag
let compare_ty t1 t2 = t1.ty_tag - t2.ty_tag

module Hsty = Hashcons.Make (struct
  type t = ty

  let equal t1 t2 =
    match t1.ty_node, t2.ty_node with
    | BS lv1, BS lv2                 -> Lenvar.equal lv1 lv2
    | Bool, Bool                     -> true
    | G gv1, G gv2                   -> Groupvar.equal gv1 gv2
    | TySym ts1, TySym ts2           -> Tysym.equal ts1 ts2
    | Fq, Fq                         -> true
    | Prod ts1, Prod ts2             -> list_eq_for_all2 equal_ty ts1 ts2
    | _                              -> false

  let hash t =
    match t.ty_node with
    | BS lv         -> hcomb 1 (Lenvar.hash lv)
    | Bool          -> 2
    | G gv          -> hcomb 3 (Groupvar.hash gv)
    | TySym gv      -> hcomb 4 (Tysym.hash gv)
    | Fq            -> 5
    | Prod ts       -> hcomb_l hash_ty 6 ts
    | Int           -> 7

  let tag n t = { t with ty_tag = n }
end)

(** Create [Map], [Set], and [Hashtbl] modules for types. *)
module Ty = StructMake (struct
  type t = ty
  let tag = hash_ty
end)
module Mty = Ty.M
module Sty = Ty.S
module Hty = Ty.H

(* ** Constructor functions *)

let mk_ty n = Hsty.hashcons {
  ty_node = n;
  ty_tag  = (-1)
}

let mk_BS lv = mk_ty (BS lv)

let mk_G gv = mk_ty (G gv)

let mk_TySym ts = mk_ty (TySym ts)

let mk_Fq = mk_ty Fq

let mk_Bool = mk_ty Bool

let mk_Int = mk_ty Int

let mk_Prod tys =
  match tys with
  | [t] -> t
  | _   -> mk_ty (Prod tys)

(* ** Indicator and destructor functions *)

let is_G ty = match ty.ty_node with
  | G _ -> true
  | _   -> false

let is_Fq ty = match ty.ty_node with
  | Fq -> true
  | _  -> false

let is_Prod ty = match ty.ty_node with
  | Prod _ -> true
  | _      -> false

let destr_G_exn ty =
  match ty.ty_node with
  | G gv -> gv
  | _    -> raise Not_found

let destr_BS_exn ty =
  match ty.ty_node with
  | BS lv -> lv
  | _     -> raise Not_found

let destr_Prod_exn ty =
  match ty.ty_node with
  | Prod ts -> ts
  | _       -> raise Not_found

let destr_Prod ty =
  match ty.ty_node with
  | Prod ts -> Some ts
  | _       -> None

(* ** Pretty printing *)

let pp_group fmt gv =
  if Groupvar.name gv = ""
  then F.fprintf fmt "G"
  else F.fprintf fmt "G_%s" (Groupvar.name gv)

let rec pp_ty fmt ty =
  match ty.ty_node with
  | BS lv             -> F.fprintf fmt "BS_%s" (Lenvar.name lv)
  | Bool              -> F.fprintf fmt "Bool"
  | Fq                -> F.fprintf fmt "Fq"
  | TySym ts          -> F.fprintf fmt "%s" (Tysym.name ts)
  | Prod ts           -> F.fprintf fmt "(%a)" (pp_list " * " pp_ty) ts
  | Int               -> F.fprintf fmt "Int"
  | G gv ->
    if Groupvar.name gv = ""
    then F.fprintf fmt "G"
    else F.fprintf fmt "G_%s" (Groupvar.name gv)

Answer 1

It's hard to walk through this code because quite a bit is missing (definitions of Id, Hashcons, StructMake). But in general this code manipulates data structures that represent types.

You can read about hash consing here: https://en.wikipedia.org/wiki/Hash_consing (which is what I just did myself). In essence it is a way of maintaining a canonical representation for a set of structures (in this case, structures representing types) so that two structures that are equal (having constituents that are equal) are represented by the identical value. This allows constant-time comparison for equality. When you do this with strings, it's called "interning" (a technique from Lisp I've used many times).

To add arrays, you need to know whether the array type will include the length of the array or just the type of its elements. The semi-mysterious type BS seems to include a length, which suggests you may want to include the length in your reprsentation.

If I were doing this project I would look for every occurence of Prod (which represents tuples) and I'd add a type representing Array in an analogous way. Instead of a list of constituent types (as for a tuple) you have one constituent type and (I would guess) a variable representing the length of the array.

Before starting out I'd look for some documentation, on what BS represents for one thing. I also have no idea what "groups" are, but maybe you could worry about it later.

Update

Here's what I mean by copying Prod. Keep in mind that I am basing this almost entirely on guesswork. So, many details (or even the entire idea) could be wrong.

The current definition of a type looks like this:

and ty_node =
  | BS of Lenvar.id
  | Bool
  | G of Groupvar.id
  | TySym of Tysym.id
  | Fq
  | Prod of ty list
  | Int

If you add a representation for Array after Prod you get something like this:

and ty_node =
  | BS of Lenvar.id
  | Bool
  | G of Groupvar.id
  | TySym of Tysym.id
  | Fq
  | Prod of ty list
  | Array of Lenvar.id * ty
  | Int

You would then go through the rest of the code adding support for the new Array variant. The compiler will help you find many of the places that need fixing.