Improve ocamldoc comments

Check in a slightly nicer stylesheet for OCamldoc generated
documentation in etc. Most just add a maximum width and increase the
font size because the default looks absolutely terrible on high-DPI
monitors.

Move val_spec_ids out of initial_check and into ast_util where it
probably belongs. Rename some functions in util.ml to better match the
OCaml stdlib.

20 files changed, 393 insertions, 325 deletions

diff --git a/etc/style.css b/etc/style.css
new file mode 100644
index 00000000..845a9998
--- /dev/null
+++ b/etc/style.css
@@ -0,0 +1,43 @@
+.keyword { font-weight : bold ; color : Red }
+.keywordsign { color : #C04600 }
+.comment { color : Green }
+.constructor { color : Blue }
+.type { color : #5C6585 }
+.string { color : Maroon }
+.warning { color : Red ; font-weight : bold }
+.info { margin-left : 3em; margin-right: 3em }
+.param_info { margin-top: 4px; margin-left : 3em; margin-right : 3em }
+.code { color : #465F91 ; }
+.typetable { border-style : hidden }
+.paramstable { border-style : hidden ; padding: 5pt 5pt}
+tr { background-color : White }
+td.typefieldcomment { background-color : #FFFFFF ; font-size: smaller ;}
+div.sig_block {margin-left: 2em}
+*:target { background: yellow; }
+body {font: 13px sans-serif; color: black; text-align: left; padding: 5px; margin: 0; width: 70pc; margin-left: 5pc; font-size: large}
+h1 { font-size : 20pt ; text-align: center; }
+h2 { font-size : 20pt ; text-align: center; }
+h3 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ;padding: 2px; border-radius: 20px }
+h4 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ;padding: 2px; border-radius: 20px }
+h5 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90EDFF ;padding: 2px; border-radius: 20px }
+h6 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90FDFF ;padding: 2px; border-radius: 20px }
+div.h7 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ; padding: 2px; border-radius: 20px }
+div.h8 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #E0FFFF ; padding: 2px; border-radius: 20px }
+div.h9 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #F0FFFF ; padding: 2px; border-radius: 20px }
+div.h10 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #FFFFFF ; padding: 2px; border-radius: 20px }
+a {color: #416DFF; text-decoration: none}
+a:hover {background-color: #ddd; text-decoration: underline}
+pre { margin-bottom: 4px; font-family: monospace; }
+pre.verbatim, pre.codepre { }
+.indextable {border: 1px #ddd solid; border-collapse: collapse}
+.indextable td, .indextable th {border: 1px #ddd solid; min-width: 80px}
+.indextable td.module {background-color: #eee ;  padding-left: 2px; padding-right: 2px}
+.indextable td.module a {color: #4E6272; text-decoration: none; display: block; width: 100%}
+.indextable td.module a:hover {text-decoration: underline; background-color: transparent}
+.deprecated {color: #888; font-style: italic}
+.indextable tr td div.info { margin-left: 2px; margin-right: 2px }
+ul.indexlist { margin-left: 0; padding-left: 0;}
+ul.indexlist li { list-style-type: none ; margin-left: 0; padding-left: 0; }
+ul.info-attributes {list-style: none; margin: 0; padding: 0; }
+div.info > p:first-child { margin-top:0; }
+div.info-desc > p:first-child { margin-top:0; margin-bottom:0; }
\ No newline at end of file
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 79b5b0eb..96849f88 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -986,6 +986,18 @@ let ids_of_def = function
 let ids_of_defs (Defs defs) =
   List.fold_left IdSet.union IdSet.empty (List.map ids_of_def defs)
 
+let val_spec_ids (Defs defs) =
+  let val_spec_id (VS_aux (vs_aux, _)) =
+    match vs_aux with
+    | VS_val_spec (_, id, _, _) -> id
+  in
+  let rec vs_ids = function
+    | DEF_spec vs :: defs -> val_spec_id vs :: vs_ids defs
+    | def :: defs -> vs_ids defs
+    | [] -> []
+  in
+  IdSet.of_list (vs_ids defs)
+
 module BE = struct
   type t = base_effect
   let compare be1 be2 = String.compare (string_of_base_effect be1) (string_of_base_effect be2)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 750d3730..815ef421 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -48,7 +48,7 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
-(** Utilities for operating on Sail ASTs *)
+(** Utilities and helper functions for operating on Sail ASTs *)
 
 open Ast
 module Big_int = Nat_big_num
@@ -56,16 +56,26 @@ module Big_int = Nat_big_num
 type mut = Immutable | Mutable
 
 (** [lvar] is the type of variables - they can either be registers,
-   local mutable or immutable variables, nullary union constructors
-   (i.e. None in option), or unbound identifiers *)
+   local mutable or immutable variables constructors or unbound
+   identifiers. *)
 type 'a lvar = Register of effect * effect * 'a | Enum of 'a | Local of mut * 'a | Unbound
 
 (** Note: Partial function -- fails for Unknown lvars *)
 val lvar_typ : 'a lvar -> 'a
 
+(** The empty annotation. Should be used carefully because it can
+   result in unhelpful error messgaes. However a common pattern is
+   generating code with [no_annot], then adding location information
+   with the various [locate_] functions in this module. *)
 val no_annot : unit annot
+
+(** [gen_loc l] takes a location l and generates a location which
+   means 'generated from location l'. This is useful for debugging
+   errors that occur in generated code. *)
 val gen_loc : Parse_ast.l -> Parse_ast.l
 
+(** {2 Functions for building (untyped) AST elements} *)
+
 val mk_id : string -> id
 val mk_kid : string -> kid
 val mk_ord : order_aux -> order
@@ -92,6 +102,11 @@ val mk_fexp : id -> unit exp -> unit fexp
 val mk_letbind : unit pat -> unit exp -> unit letbind
 val mk_kopt : kind_aux -> kid -> kinded_id
 
+val inc_ord : order
+val dec_ord : order
+
+(** {2 Unwrap aux constructors} *)
+
 val unaux_exp : 'a exp -> 'a exp_aux
 val unaux_pat : 'a pat -> 'a pat_aux
 val unaux_nexp : nexp -> nexp_aux
@@ -100,26 +115,33 @@ val unaux_typ : typ -> typ_aux
 val unaux_kind : kind -> kind_aux
 val unaux_constraint : n_constraint -> n_constraint_aux
 
+(** {2 Destruct type annotated patterns and expressions} *)
+
+(** [untyp_pat (P_aux (P_typ (typ, pat)), _)] returns [Some (pat,
+   typ)] or [None] if the pattern does not match. *)
 val untyp_pat : 'a pat -> 'a pat * typ option
+
+(** Same as [untyp_pat], but for [E_cast] nodes *)
 val uncast_exp : 'a exp -> 'a exp * typ option
 
-val inc_ord : order
-val dec_ord : order
+(** {2 Utilites for working with kinded_ids} *)
 
-(* Utilites for working with kinded_ids *)
 val kopt_kid : kinded_id -> kid
 val kopt_kind : kinded_id -> kind
+
 val is_int_kopt : kinded_id -> bool
 val is_order_kopt : kinded_id -> bool
 val is_typ_kopt : kinded_id -> bool
 val is_bool_kopt : kinded_id -> bool
 
-(* Some handy utility functions for constructing types. *)
+(** {2 Utility functions for constructing types} *)
+
 val mk_typ : typ_aux -> typ
 val mk_typ_arg : typ_arg_aux -> typ_arg
 val mk_id_typ : id -> typ
 
-(* Sail builtin types. *)
+(** {2 Sail builtin types} *)
+
 val unknown_typ : typ
 val int_typ : typ
 val nat_typ : typ
@@ -140,18 +162,128 @@ val exc_typ : typ
 val tuple_typ : typ list -> typ
 val function_typ : typ list -> typ -> effect -> typ
 
-val no_effect : effect
-val mk_effect : base_effect_aux list -> effect
+val is_unit_typ : typ -> bool
+val is_number : typ -> bool
+val is_ref_typ : typ -> bool
+val is_vector_typ : typ -> bool
+val is_bit_typ : typ -> bool
+val is_bitvector_typ : typ -> bool
+
+(** {2 Simplifcation of numeric expressions and constraints}
+
+   These functions simplify nexps and n_constraints using various
+   basic rules. In general they will guarantee to reduce constant
+   numeric expressions like 2 + 5 into 7, although they will not
+   simplify 2^constant, as that often leads to unreadable error
+   messages containing huge numbers. *)
 
 val nexp_simp : nexp -> nexp
 val constraint_simp : n_constraint -> n_constraint
 
-(* If a constraint is a conjunction, return a list of all the top-level conjuncts *)
+(** If a constraint is a conjunction, return a list of all the top-level conjuncts *)
 val constraint_conj : n_constraint -> n_constraint list
-(* Same as constraint_conj but for disjunctions *)
+
+(** Same as constraint_conj but for disjunctions *)
 val constraint_disj : n_constraint -> n_constraint list
 
-(* Utilities for building n-expressions *)
+(** {2 Set and Map modules for various AST elements} *)
+
+module Id : sig
+  type t = id
+  val compare : id -> id -> int
+end
+
+module Kid : sig
+  type t = kid
+  val compare : kid -> kid -> int
+end
+
+module Kind : sig
+  type t = kind
+  val compare : kind -> kind -> int
+end
+
+module KOpt : sig
+  type t = kinded_id
+  val compare : kinded_id -> kinded_id -> int
+end
+
+module Nexp : sig
+  type t = nexp
+  val compare : nexp -> nexp -> int
+end
+
+module BE : sig
+  type t = base_effect
+  val compare : base_effect -> base_effect -> int
+end
+
+module NC : sig
+  type t = n_constraint
+  val compare : n_constraint -> n_constraint -> int
+end
+
+(* NB: the comparison function does not expand synonyms *)
+module Typ : sig
+  type t = typ
+  val compare : typ -> typ -> int
+end
+
+module IdSet : sig
+  include Set.S with type elt = id
+end
+
+module NexpSet : sig
+  include Set.S with type elt = nexp
+end
+
+module NexpMap : sig
+  include Map.S with type key = nexp
+end
+
+module KOptSet : sig
+  include Set.S with type elt = kinded_id
+end
+
+module KOptMap : sig
+  include Map.S with type key = kinded_id
+end
+
+module BESet : sig
+  include Set.S with type elt = base_effect
+end
+
+module KidSet : sig
+  include Set.S with type elt = kid
+end
+
+module KBindings : sig
+  include Map.S with type key = kid
+end
+
+module Bindings : sig
+  include Map.S with type key = id
+end
+
+module TypMap : sig
+  include Map.S with type key = typ
+end
+
+
+(** {2 Functions for building and manipulating effects} *)
+
+val no_effect : effect
+val mk_effect : base_effect_aux list -> effect
+
+val has_effect : effect -> base_effect_aux -> bool
+val effect_set : effect -> BESet.t
+
+val equal_effects : effect -> effect -> bool
+val subseteq_effects : effect -> effect -> bool
+val union_effects : effect -> effect -> effect
+
+(** {2 Functions for building numeric expressions} *)
+
 val nconstant : Big_int.num -> nexp
 val nint : int -> nexp
 val nminus : nexp -> nexp -> nexp
@@ -162,7 +294,8 @@ val nvar : kid -> nexp
 val napp : id -> nexp list -> nexp
 val nid : id -> nexp
 
-(* Numeric constraint builders *)
+(** {2 Functions for building numeric constraints} *)
+
 val nc_eq : nexp -> nexp -> n_constraint
 val nc_neq : nexp -> nexp -> n_constraint
 val nc_lteq : nexp -> nexp -> n_constraint
@@ -178,13 +311,16 @@ val nc_set : kid -> Big_int.num list -> n_constraint
 val nc_int_set : kid -> int list -> n_constraint
 val nc_var : kid -> n_constraint
 
+(** {2 Functions for building type arguments}*)
+
 val arg_nexp : ?loc:l -> nexp -> typ_arg
 val arg_order : ?loc:l -> order -> typ_arg
 val arg_typ : ?loc:l -> typ -> typ_arg
 val arg_bool : ?loc:l -> n_constraint -> typ_arg
 val arg_kopt : kinded_id -> typ_arg
 
-(* Functions for working with type quantifiers *)
+(** {2 Functions for working with type quantifiers} *)
+
 val quant_add : quant_item -> typquant -> typquant
 val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
@@ -194,7 +330,8 @@ val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
 val is_quant_kopt : quant_item -> bool
 val is_quant_constraint : quant_item -> bool
 
-(* Functions to map over the annotations in sub-expressions *)
+(** {2 Functions to map over annotations in sub-expressions} *)
+
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
 val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
 val map_pexp_annot : ('a annot -> 'b annot) -> 'a pexp -> 'b pexp
@@ -205,7 +342,8 @@ val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat
 val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp
 val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl
 
-(* Extract locations from identifiers *)
+(** {2 Extract locations from terms} *)
+
 val id_loc : id -> Parse_ast.l
 val kid_loc : kid -> Parse_ast.l
 val typ_loc : typ -> Parse_ast.l
@@ -213,8 +351,11 @@ val pat_loc : 'a pat -> Parse_ast.l
 val exp_loc : 'a exp -> Parse_ast.l
 val def_loc : 'a def -> Parse_ast.l
 
-(* For debugging and error messages only: Not guaranteed to produce
-   parseable SAIL, or even print all language constructs! *)
+(** {2 Printing utilities}
+
+   Note: For debugging and error messages only - not guaranteed to
+   produce parseable Sail, or even print all language constructs! *)
+
 val string_of_id : id -> string
 val string_of_kid : kid -> string
 val string_of_base_effect_aux : base_effect_aux -> string
@@ -241,11 +382,15 @@ val string_of_mpat : 'a mpat -> string
 val string_of_letbind : 'a letbind -> string
 val string_of_index_range : index_range -> string
 
+(** {2 Functions for getting identifiers from toplevel definitions} *)
+
 val id_of_fundef : 'a fundef -> id
 val id_of_type_def : 'a type_def -> id
 val id_of_val_spec : 'a val_spec -> id
 val id_of_dec_spec : 'a dec_spec -> id
 
+(** {2 Functions for manipulating identifiers} *)
+
 val id_of_kid : kid -> id
 val kid_of_id : id -> kid
 
@@ -253,86 +398,7 @@ val prepend_id : string -> id -> id
 val append_id : id -> string -> id
 val prepend_kid : string -> kid -> kid
 
-module Id : sig
-  type t = id
-  val compare : id -> id -> int
-end
-
-module Kid : sig
-  type t = kid
-  val compare : kid -> kid -> int
-end
-
-module Kind : sig
-  type t = kind
-  val compare : kind -> kind -> int
-end
-
-module KOpt : sig
-  type t = kinded_id
-  val compare : kinded_id -> kinded_id -> int
-end
-
-module Nexp : sig
-  type t = nexp
-  val compare : nexp -> nexp -> int
-end
-
-module BE : sig
-  type t = base_effect
-  val compare : base_effect -> base_effect -> int
-end
-
-module NC : sig
-  type t = n_constraint
-  val compare : n_constraint -> n_constraint -> int
-end
-
-(* NB: the comparison function does not expand synonyms *)
-module Typ : sig
-  type t = typ
-  val compare : typ -> typ -> int
-end
-
-module IdSet : sig
-  include Set.S with type elt = id
-end
-
-module NexpSet : sig
-  include Set.S with type elt = nexp
-end
-
-module NexpMap : sig
-  include Map.S with type key = nexp
-end
-
-module KOptSet : sig
-  include Set.S with type elt = kinded_id
-end
-
-module KOptMap : sig
-  include Map.S with type key = kinded_id
-end
-
-module BESet : sig
-  include Set.S with type elt = base_effect
-end
-
-module KidSet : sig
-  include Set.S with type elt = kid
-end
-
-module KBindings : sig
-  include Map.S with type key = kid
-end
-
-module Bindings : sig
-  include Map.S with type key = id
-end
-
-module TypMap : sig
-  include Map.S with type key = typ
-end
+(** {2 Misc functions} *)
 
 val nexp_frees : nexp -> KidSet.t
 val nexp_identical : nexp -> nexp -> bool
@@ -341,27 +407,12 @@ val int_of_nexp_opt : nexp -> Big_int.num option
 
 val lexp_to_exp : 'a lexp -> 'a exp
 
-val is_unit_typ : typ -> bool
-val is_number : typ -> bool
-val is_ref_typ : typ -> bool
-val is_vector_typ : typ -> bool
-val is_bit_typ : typ -> bool
-val is_bitvector_typ : typ -> bool
-
 val typ_app_args_of : typ -> string * typ_arg_aux list * Ast.l
 val vector_typ_args_of : typ -> nexp * order * typ
 val vector_start_index : typ -> nexp
 
 val is_order_inc : order -> bool
 
-val has_effect : effect -> base_effect_aux -> bool
-
-val effect_set : effect -> BESet.t
-
-val equal_effects : effect -> effect -> bool
-val subseteq_effects : effect -> effect -> bool
-val union_effects : effect -> effect -> effect
-
 val kopts_of_order : order -> KOptSet.t
 val kopts_of_nexp : nexp -> KOptSet.t
 val kopts_of_typ : typ -> KOptSet.t
@@ -383,9 +434,7 @@ val construct_pexp : 'a pat * ('a exp) option * 'a exp * (Ast.l * 'a) ->  'a pex
 val destruct_mpexp : 'a mpexp -> 'a mpat * ('a exp) option * (Ast.l * 'a)
 val construct_mpexp : 'a mpat * ('a exp) option * (Ast.l * 'a) ->  'a mpexp
 
-
 val is_valspec : id -> 'a def -> bool
-
 val is_fundef : id -> 'a def -> bool
 
 val rename_valspec : id -> 'a val_spec -> 'a val_spec
@@ -402,12 +451,16 @@ val type_union_id : type_union -> id
 val ids_of_def : 'a def -> IdSet.t
 val ids_of_defs : 'a defs -> IdSet.t
 
+val val_spec_ids : 'a defs -> IdSet.t
+
 val pat_ids : 'a pat -> IdSet.t
 
 val subst : id -> 'a exp -> 'a exp -> 'a exp
 
 val hex_to_bin : string -> string
 
+(** {2 Manipulating locations} *)
+
 (** locate takes an expression and recursively sets the location in
    every subexpression using a function that takes the orginal
    location as an argument. Expressions build using mk_exp and similar
@@ -422,15 +475,26 @@ val locate_lexp : (l -> l) -> 'a lexp -> 'a lexp
 
 val locate_typ : (l -> l) -> typ -> typ
 
-(* Make a unique location by giving it a Parse_ast.Unique wrapper with
+(** Make a unique location by giving it a Parse_ast.Unique wrapper with
    a generated number. *)
 val unique : l -> l
 
-(** Substitutions *)
+(** Reduce a location to a pair of positions if possible *)
+val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
+
+(** Try to find the annotation closest to the provided (simplified)
+   location. Note that this function makes no guarantees about finding
+   the closest annotation or even finding an annotation at all. This
+   is used by the Emacs mode to provide type-at-cursor functionality
+   and we don't mind if it's a bit fuzzy in that context. *)
+val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a defs -> (Ast.l * 'a) option
+
+(** {2 Substitutions}
 
-(* The function X_subst substitutes a type argument into something of
+   The function X_subst substitutes a type argument into something of
    type X. The type of the type argument determines which kind of type
-   variables willb e replaced *)
+   variables will be replaced *)
+
 val nexp_subst : kid -> typ_arg -> nexp -> nexp
 val constraint_subst : kid -> typ_arg -> n_constraint -> n_constraint
 val order_subst : kid -> typ_arg -> order -> order
@@ -439,7 +503,7 @@ val typ_arg_subst : kid -> typ_arg -> typ_arg -> typ_arg
 
 val subst_kid : (kid -> typ_arg -> 'a -> 'a) -> kid -> kid -> 'a -> 'a
 
-(* Multiple type-level substitution *)
+(* Multiple type-level substitutions *)
 val subst_kids_nexp : nexp KBindings.t -> nexp -> nexp
 val subst_kids_nc : nexp KBindings.t -> n_constraint -> n_constraint
 val subst_kids_typ : nexp KBindings.t -> typ -> typ
@@ -447,7 +511,3 @@ val subst_kids_typ_arg : nexp KBindings.t -> typ_arg -> typ_arg
 
 val quant_item_subst_kid : kid -> kid -> quant_item -> quant_item
 val typquant_subst_kid : kid -> kid -> typquant -> typquant
-
-val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
-
-val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a defs -> (Ast.l * 'a) option
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 5893563b..b3d24820 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -811,18 +811,6 @@ let constraint_of_string str =
 let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false))
 let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false))
 
-let val_spec_ids (Defs defs) =
-  let val_spec_id (VS_aux (vs_aux, _)) =
-    match vs_aux with
-    | VS_val_spec (_, id, _, _) -> id
-  in
-  let rec vs_ids = function
-    | DEF_spec vs :: defs -> val_spec_id vs :: vs_ids defs
-    | def :: defs -> vs_ids defs
-    | [] -> []
-  in
-  IdSet.of_list (vs_ids defs)
-
 let quant_item_param = function
   | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))]
@@ -1047,7 +1035,7 @@ let process_ast ?generate:(generate=true) defs =
     |> generate_initialize_registers vs_ids
   else
     ast
-  
+
 let ast_of_def_string str =
   let def = Parser.def_eof Lexer.token (Lexing.from_string str) in
   process_ast (P.Defs [def])
diff --git a/src/initial_check.mli b/src/initial_check.mli
index a0bde482..b96a9efb 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -48,14 +48,18 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(** Initial desugaring pass over AST after parsing *)
+
 open Ast
 open Ast_util
 
-(* Generate undefined_T functions for every type T. False by
+(** {2 Options} *)
+
+(** Generate undefined_T functions for every type T. False by
    default. *)
 val opt_undefined_gen : bool ref
 
-(* Generate faster undefined_T functions. Rather than generating
+(** Generate faster undefined_T functions. Rather than generating
    functions that allow for the undefined values of enums and variants
    to be picked at runtime using a RNG or similar, this creates
    undefined_T functions for those types that simply return a specific
@@ -65,16 +69,17 @@ val opt_undefined_gen : bool ref
    default. *)
 val opt_fast_undefined : bool ref
 
-(* Allow # in identifiers when set, like the GHC option of the same name *)
+(** Allow # in identifiers when set, much like the GHC option of the same
+   name *)
 val opt_magic_hash : bool ref
 
-(* When true enums can be automatically casted to range types and
+(** When true enums can be automatically casted to range types and
    back.  Otherwise generated T_of_num and num_of_T functions must be
    manually used for each enum T *)
 val opt_enum_casts : bool ref
 
-(* This is a bit of a hack right now - it ensures that the undefiend
-   builtins (undefined_vector etc), only get added to the ast
+(** This is a bit of a hack right now - it ensures that the undefiend
+   builtins (undefined_vector etc), only get added to the AST
    once. The original assumption in sail is that the whole AST gets
    processed at once (therefore they could only get added once), and
    this isn't true any more with the interpreter. This needs to be
@@ -82,17 +87,17 @@ val opt_enum_casts : bool ref
    all the loaded files. *)
 val have_undefined_builtins : bool ref
 
-val ast_of_def_string : string -> unit defs
+(** {2 Desugar and process AST } *)
 
 (** If the generate flag is false, then we won't generate any
    auxilliary definitions, like the initialize_registers function *)
 val process_ast : ?generate:bool -> Parse_ast.defs -> unit defs
 
-val val_spec_ids : 'a defs -> IdSet.t
+(** {2 Parsing expressions and definitions from strings} *)
 
 val extern_of_string : id -> string -> unit def
 val val_spec_of_string : id -> string -> unit def
-
+val ast_of_def_string : string -> unit defs
 val exp_of_string : string -> unit exp
 val typ_of_string : string -> typ
 val constraint_of_string : string -> n_constraint
diff --git a/src/isail.ml b/src/isail.ml
index e47973b4..8f71a809 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -106,7 +106,7 @@ let sail_logo =
   in
   List.map banner logo @ [""] @ help @ [""]
 
-let vs_ids = ref (Initial_check.val_spec_ids !Interactive.ast)
+let vs_ids = ref (val_spec_ids !Interactive.ast)
 
 let interactive_state = ref (initial_state !Interactive.ast Value.primops)
 
@@ -399,12 +399,12 @@ let handle_input' input =
            Interactive.ast := append_ast !Interactive.ast ast;
            interactive_state := initial_state !Interactive.ast Value.primops;
            Interactive.env := env;
-           vs_ids := Initial_check.val_spec_ids !Interactive.ast
+           vs_ids := val_spec_ids !Interactive.ast
         | ":u" | ":unload" ->
            Interactive.ast := Ast.Defs [];
            Interactive.env := Type_check.initial_env;
            interactive_state := initial_state !Interactive.ast Value.primops;
-           vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+           vs_ids := val_spec_ids !Interactive.ast;
            (* See initial_check.mli for an explanation of why we need this. *)
            Initial_check.have_undefined_builtins := false;
            Process_file.clear_symbols ()
@@ -431,7 +431,7 @@ let handle_input' input =
                Interactive.ast := append_ast !Interactive.ast ast;
                interactive_state := initial_state !Interactive.ast Value.primops;
                Interactive.env := env;
-               vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+               vs_ids := val_spec_ids !Interactive.ast;
                print_endline ("(message \"Checked " ^ arg ^ " done\")\n");
              with
              | Reporting.Fatal_error (Err_type (l, msg)) ->
@@ -441,7 +441,7 @@ let handle_input' input =
            Interactive.ast := Ast.Defs [];
            Interactive.env := Type_check.initial_env;
            interactive_state := initial_state !Interactive.ast Value.primops;
-           vs_ids := Initial_check.val_spec_ids !Interactive.ast;
+           vs_ids := val_spec_ids !Interactive.ast;
            Initial_check.have_undefined_builtins := false;
            Process_file.clear_symbols ()
         | ":typeat" ->
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 16fb6756..025138d0 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -61,31 +61,6 @@ module Big_int = Nat_big_num
 (* 1. Conversion to A-normal form (ANF)                                   *)
 (**************************************************************************)
 
-(* The first step in compiling sail is converting the Sail expression
-   grammar into A-normal form. Essentially this converts expressions
-   such as f(g(x), h(y)) into something like:
-
-   let v0 = g(x) in let v1 = h(x) in f(v0, v1)
-
-   Essentially the arguments to every function must be trivial, and
-   complex expressions must be let bound to new variables, or used in
-   a block, assignment, or control flow statement (if, for, and
-   while/until loops). The aexp datatype represents these expressions,
-   while aval represents the trivial values.
-
-   The convention is that the type of an aexp is given by last
-   argument to a constructor. It is omitted where it is obvious - for
-   example all for loops have unit as their type. If some constituent
-   part of the aexp has an annotation, the it refers to the previous
-   argument, so in
-
-   AE_let (id, typ1, _, body, typ2)
-
-   typ1 is the type of the bound identifer, whereas typ2 is the type
-   of the whole let expression (and therefore also the body).
-
-   See Flanagan et al's 'The Essence of Compiling with Continuations'
-   *)
 type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l
 
 and 'a aexp_aux =
diff --git a/src/jib/anf.mli b/src/jib/anf.mli
index e8d58fe4..79fb35ca 100644
--- a/src/jib/anf.mli
+++ b/src/jib/anf.mli
@@ -48,12 +48,38 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(** The A-normal form (ANF) grammar *)
+
 open Ast
 open Ast_util
 open Jib
 open Type_check
 
-(* The A-normal form (ANF) grammar *)
+(** The first step in compiling Sail is converting the Sail expression
+   grammar into A-normal form (ANF). Essentially this converts
+   expressions such as [f(g(x), h(y))] into something like:
+
+   [let v0 = g(x) in let v1 = h(x) in f(v0, v1)]
+
+   Essentially the arguments to every function must be trivial, and
+   complex expressions must be let bound to new variables, or used in
+   a block, assignment, or control flow statement (if, for, and
+   while/until loops). The aexp datatype represents these expressions,
+   while aval represents the trivial values.
+
+   The convention is that the type of an aexp is given by last
+   argument to a constructor. It is omitted where it is obvious - for
+   example all for loops have unit as their type. If some constituent
+   part of the aexp has an annotation, the it refers to the previous
+   argument, so in
+
+   [AE_let (id, typ1, _, body, typ2)]
+
+   [typ1] is the type of the bound identifer, whereas [typ2] is the type
+   of the whole let expression (and therefore also the body).
+
+   See Flanagan et al's {e The Essence of Compiling with Continuations}.
+   *)
 
 type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l
 
@@ -88,6 +114,9 @@ and 'a apat_aux =
   | AP_nil of 'a
   | AP_wild of 'a
 
+(** We allow ANF->ANF optimization to insert fragments of C code
+   directly in the ANF grammar via [AV_C_fragment]. Such fragments
+   must be side-effect free expressions. *)
 and 'a aval =
   | AV_lit of lit * 'a
   | AV_id of id * 'a lvar
@@ -98,28 +127,35 @@ and 'a aval =
   | AV_record of ('a aval) Bindings.t * 'a
   | AV_C_fragment of fragment * 'a * ctyp
 
+(** Function for generating unique identifiers during ANF
+   translation. *)
 val gensym : unit -> id
 
-(* Functions for transforming ANF expressions *)
+(** {2 Functions for transforming ANF expressions} *)
 
+(** Map over all values in an ANF expression *)
 val map_aval : (Env.t -> Ast.l -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp
 
+(** Map over all function calls in an ANF expression *)
 val map_functions : (Env.t -> Ast.l -> id -> ('a aval) list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp
 
+(** Remove all variable shadowing in an ANF expression *)
 val no_shadow : IdSet.t -> 'a aexp -> 'a aexp
 
 val apat_globals : 'a apat -> (id * 'a) list
-
 val apat_types : 'a apat -> 'a Bindings.t
 
+(** Returns true if an ANF expression is dead due to flow typing
+   implying it is unreachable. Note: This function calls SMT. *)
 val is_dead_aexp : 'a aexp -> bool
 
-(* Compiling to ANF expressions *)
+(** {2 Compiling to ANF expressions} *)
 
 val anf_pat : ?global:bool -> tannot pat -> typ apat
 
 val anf : tannot exp -> typ aexp
 
-(* Pretty printing ANF expressions *)
+(** {2 Pretty printing ANF expressions} *)
+
 val pp_aval : typ aval -> PPrint.document
 val pp_aexp : typ aexp -> PPrint.document
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 92a0d06a..173e5c5f 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -48,6 +48,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(** Compile Sail ASTs to Jib intermediate representation *)
+
 open Anf
 open Ast
 open Ast_util
@@ -57,6 +59,9 @@ open Type_check
 (** Print the IR representation of a specific function. *)
 val opt_debug_function : string ref
   
+
+(** {2 Jib context} *)
+
 (** Context for compiling Sail to Jib. We need to pass a (global)
    typechecking environment given by checking the full AST. We have to
    provide a conversion function from Sail types into Jib types, as
@@ -81,6 +86,8 @@ val initial_ctx :
   Env.t ->
   ctx
 
+(** {2 Compilation functions} *)
+
 (** Compile a Sail definition into a Jib definition. The first two
    arguments are is the current definition number and the total number
    of definitions, and can be used to drive a progress bar (see
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index a5f0653b..ff4a9818 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -997,7 +997,7 @@ let ocaml_compile spec defs generator_types =
     ignore(Unix.system ("cp -r " ^ sail_dir ^ "/lib/myocamlbuild_coverage.ml myocamlbuild.ml"));
   ocaml_pp_defs out_chan defs generator_types;
   close_out out_chan;
-  if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
+  if IdSet.mem (mk_id "main") (val_spec_ids defs)
   then
     begin
       print_endline "Generating main";
diff --git a/src/pp.mli b/src/pp.mli
deleted file mode 100644
index 5cfb3d88..00000000
--- a/src/pp.mli
+++ /dev/null
@@ -1,58 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*    Alasdair Armstrong                                                  *)
-(*    Brian Campbell                                                      *)
-(*    Thomas Bauereiss                                                    *)
-(*    Anthony Fox                                                         *)
-(*    Jon French                                                          *)
-(*    Dominic Mulligan                                                    *)
-(*    Stephen Kell                                                        *)
-(*    Mark Wassell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(**************************************************************************)
-
-open Format
-val pp_str : formatter -> string -> unit
-
-val lst : ('a, formatter, unit) format -> (formatter -> 'b -> unit) -> formatter -> 'b list -> unit
-
-val opt : (formatter -> 'a -> unit) -> formatter -> 'a option -> unit
-
-val pp_to_string : (formatter -> 'a) -> string
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index fe94dbb5..4afa5153 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2792,7 +2792,7 @@ try
   (* let regtypes = find_regtypes d in *)
   let state_ids =
     State.generate_regstate_defs true defs
-    |> Initial_check.val_spec_ids
+    |> val_spec_ids
   in
   let is_state_def = function
     | DEF_spec vs -> IdSet.mem (id_of_val_spec vs) state_ids
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1c30e06e..50ce1e5a 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1466,7 +1466,7 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) type_env (De
   (* let regtypes = find_regtypes d in *)
   let state_ids =
     State.generate_regstate_defs !opt_mwords defs
-    |> Initial_check.val_spec_ids
+    |> val_spec_ids
   in
   let is_state_def = function
     | DEF_spec vs -> IdSet.mem (id_of_val_spec vs) state_ids
diff --git a/src/rewriter.mli b/src/rewriter.mli
index ec4e381c..ab29d1d9 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -48,6 +48,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(** General rewriting framework for Sail->Sail rewrites *)
+
 module Big_int = Nat_big_num
 open Ast
 open Type_check
@@ -65,14 +67,14 @@ val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
 
 val rewriters_base : tannot rewriters
 
-(* The identity re-writer *)
+(** The identity re-writer *)
 val rewrite_defs : tannot defs -> tannot defs
 
 val rewrite_defs_base : tannot rewriters -> tannot defs -> tannot defs
 
 val rewrite_defs_base_parallel : int -> tannot rewriters -> tannot defs -> tannot defs
-  
-(* Same as rewrite_defs base but display a progress bar when verbosity >= 1 *)
+
+(** Same as rewrite_defs_base but display a progress bar when verbosity >= 1 *)
 val rewrite_defs_base_progress : string -> tannot rewriters -> tannot defs -> tannot defs
 
 val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp
diff --git a/src/rewrites.ml b/src/rewrites.ml
index ec074607..34b9388d 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -319,7 +319,7 @@ let rewrite_bitvector_exps env defs =
     | (e_aux, a) -> E_aux (e_aux, a)
   in
   let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in
-  if IdSet.mem (mk_id "bitvector_of_bitlist") (Initial_check.val_spec_ids defs) then
+  if IdSet.mem (mk_id "bitvector_of_bitlist") (val_spec_ids defs) then
     rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } defs
   else defs
 
diff --git a/src/sail.odocl b/src/sail.odocl
index 87209053..4e91e22e 100644
--- a/src/sail.odocl
+++ b/src/sail.odocl
@@ -1,16 +1,16 @@
 ast
-ast_util
-finite_map
-initial_check
-lexer
-sail
 parse_ast
+lexer
 parser
-pp
-pretty_print
-process_file
-reporting_basic
+ast_util
+initial_check
+type_check
 rewriter
+rewrites
 specialize
-type_check
+anf
+jib
+jib_compile
+jib_util
 util
+graph
\ No newline at end of file
diff --git a/src/specialize.ml b/src/specialize.ml
index e2ab3c68..afce4b0f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -256,7 +256,7 @@ let rec instantiations_of spec id ast =
   !instantiations
 
 let rec rewrite_polymorphic_calls spec id ast =
-  let vs_ids = Initial_check.val_spec_ids ast in
+  let vs_ids = val_spec_ids ast in
 
   let rewrite_e_aux = function
     | E_aux (E_app (id', args), annot) as exp when Id.compare id id' = 0 ->
@@ -495,7 +495,7 @@ let initial_calls = IdSet.of_list
 
 let remove_unused_valspecs ?(initial_calls=initial_calls) env ast =
   let calls = ref initial_calls in
-  let vs_ids = Initial_check.val_spec_ids ast in
+  let vs_ids = val_spec_ids ast in
 
   let inspect_exp = function
     | E_aux (E_app (call, _), _) as exp ->
diff --git a/src/type_check.mli b/src/type_check.mli
index 15110b37..5333d02d 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -56,19 +56,21 @@ module Big_int = Nat_big_num
 
 (** [opt_tc_debug] controls the verbosity of the type checker. 0 is
    silent, 1 prints a tree of the type derivation and 2 is like 1 but
-   with much more debugging information. *)
+   with much more debugging information. 3 is the highest level, and
+   is even more verbose still. *)
 val opt_tc_debug : int ref
 
-(** [opt_no_effects] turns of the effect checking. This can break
-   re-writer passes, so it should only be used for debugging. *)
+(** [opt_no_effects] turns of the effect checking. Effects will still
+   be propagated as normal however. *)
 val opt_no_effects : bool ref
 
 (** [opt_no_lexp_bounds_check] turns of the bounds checking in vector
    assignments in l-expressions. *)
 val opt_no_lexp_bounds_check : bool ref
 
-(** opt_expand_valspec expands typedefs in valspecs during type check.
-   We prefer not to do it for latex output but it is otherwise a good idea. *)
+(** [opt_expand_valspec] expands typedefs in valspecs during type
+   checking. We prefer not to do it for latex output but it is
+   otherwise a good idea. *)
 val opt_expand_valspec : bool ref
 
 (** Linearize cases involving power where we would otherwise require
@@ -204,9 +206,11 @@ module Env : sig
      node. *)
   val no_casts : t -> t
 
-  (* Is casting allowed by the environment? *)
+  (** Is casting allowed by the environment? *)
   val allow_casts : t -> bool
 
+  (** Note: Likely want use Type_check.initial_env instead. The empty
+     environment is lacking even basic builtins. *)
   val empty : t
 
   val pattern_completeness_ctx : t -> Pattern_completeness.ctx
@@ -216,17 +220,12 @@ module Env : sig
   val get_union_id : id -> t -> typquant * typ
 end
 
+(** {4 Environment helper functions} *)
+
 (** Push all the type variables and constraints from a typquant into
    an environment *)
 val add_typquant : Ast.l -> typquant -> Env.t -> Env.t
 
-(** Safely destructure an existential type. Returns None if the type
-   is not existential. This function will pick a fresh name for the
-   existential to ensure that no name-clashes occur. The "plain"
-   version does not treat numeric types as existentials. *)
-val destruct_exist_plain : ?name:string option -> typ -> (kinded_id list * n_constraint * typ) option
-val destruct_exist : ?name:string option -> typ -> (kinded_id list * n_constraint * typ) option
-
 val add_existential : Ast.l -> kinded_id list -> n_constraint -> Env.t -> Env.t
 
 (** When the typechecker creates new type variables it gives them
@@ -238,10 +237,10 @@ val add_existential : Ast.l -> kinded_id list -> n_constraint -> Env.t -> Env.t
    not of this form. *)
 val orig_kid : kid -> kid
 
-(* Vector with default order. *)
+(** Vector with default order as set in environment by [default Order ord] *)
 val dvector_typ : Env.t -> nexp -> typ -> typ
 
-val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
+(** {2 Type annotations} *)
 
 (** The type of type annotations *)
 type tannot
@@ -280,7 +279,7 @@ val strip_lexp : 'a lexp -> unit lexp
 val strip_mpexp : 'a mpexp -> unit mpexp
 val strip_mapcl : 'a mapcl -> unit mapcl
 
-(* Strip location information from types for comparison purposes *)
+(** Strip location information from types for comparison purposes *)
 val strip_typ : typ -> typ
 val strip_typq : typquant -> typquant
 val strip_id : id -> id
@@ -372,6 +371,15 @@ val expected_typ_of : Ast.l * tannot -> typ option
 
 (** {2 Utilities } *)
 
+(** Safely destructure an existential type. Returns None if the type
+   is not existential. This function will pick a fresh name for the
+   existential to ensure that no name-collisions occur, although we
+   can optionally suggest a name for the case where it would not cause
+   a collision. The "plain" version does not treat numeric types
+   (i.e. range, int, nat) as existentials. *)
+val destruct_exist_plain : ?name:string option -> typ -> (kinded_id list * n_constraint * typ) option
+val destruct_exist : ?name:string option -> typ -> (kinded_id list * n_constraint * typ) option
+
 val destruct_atom_nexp : Env.t -> typ -> nexp option
 
 val destruct_atom_bool : Env.t -> typ -> n_constraint option
@@ -382,6 +390,10 @@ val destruct_numeric : ?name:string option -> typ -> (kid list * n_constraint *
 
 val destruct_vector : Env.t -> typ -> (nexp * order * typ) option
 
+(** Construct an existential type with a guaranteed fresh
+   identifier. *)
+val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
+
 val subst_unifiers : typ_arg KBindings.t -> typ -> typ
 
 (** [unify l env goals typ1 typ2] returns set of typ_arg bindings such
@@ -392,6 +404,7 @@ val subst_unifiers : typ_arg KBindings.t -> typ -> typ
    typ2 (occurs check). *)
 val unify : l -> Env.t -> KidSet.t -> typ -> typ -> typ_arg KBindings.t
 
+(** Check if two types are alpha equivalent *)
 val alpha_equivalent : Env.t -> typ -> typ -> bool
 
 (** Throws Invalid_argument if the argument is not a E_app expression *)
@@ -408,7 +421,7 @@ val propagate_exp_effect : tannot exp -> tannot exp
 
 val propagate_pexp_effect : tannot pexp -> tannot pexp * effect
 
-(** {2 Checking full AST} *)
+(** {2 Checking full ASTs} *)
 
 (** Fully type-check an AST
 
diff --git a/src/util.ml b/src/util.ml
index 251fb3eb..703bbc1f 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -329,18 +329,7 @@ module IntIntSet = Set.Make(
     type t = int * int
   end )
 
-
-module ExtraSet = functor (S : Set.S) ->
-  struct 
-    let add_list s l = List.fold_left (fun s x -> S.add x s) s l
-    let from_list l = add_list S.empty l
-    let list_union l = List.fold_left S.union S.empty l
-    let list_inter = function s :: l -> List.fold_left S.inter s l
-       | [] -> raise (Failure "ExtraSet.list_inter")
-  end;;
-
-
-let copy_file src dst = 
+let copy_file src dst =
   let len = 5096 in
   let b = Bytes.make len ' ' in
   let read_len = ref 0 in
@@ -357,7 +346,7 @@ let move_file src dst =
    try
      (* try efficient version *)
      Sys.rename src dst
-   with Sys_error _ -> 
+   with Sys_error _ ->
    begin
      (* OK, do it the the hard way *)
      copy_file src dst;
@@ -370,7 +359,7 @@ let same_content_files file1 file2 : bool =
     let s1 = Stream.of_channel (open_in_bin file1) in
     let s2 = Stream.of_channel (open_in_bin file2) in
     let stream_is_empty s = (try Stream.empty s; true with Stream.Failure -> false) in
-    try 
+    try
       while ((Stream.next s1) = (Stream.next s2)) do () done;
       false
     with Stream.Failure -> stream_is_empty s1 && stream_is_empty s2
@@ -454,9 +443,6 @@ let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.ma
 
 let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str))
 
-(** Encode string for use as a filename. We can't use zencode directly
-   because some operating systems make the mistake of being
-   case-insensitive. *)
 let file_encode_string str =
   let zstr = zencode_string str in
   let md5 = Digest.to_hex (Digest.string zstr) in
diff --git a/src/util.mli b/src/util.mli
index 013bdcda..06fd5eff 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -48,6 +48,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+(** Various non Sail specific utility functions *)
+
 (* Last element of a list *)
 val last : 'a list -> 'a
 
@@ -78,7 +80,7 @@ val remove_dups : ('a -> 'a -> int) -> ('a -> 'a -> bool) -> 'a list -> 'a list
 val assoc_equal_opt : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b option
 
 val assoc_compare_opt : ('a -> 'a -> int) -> 'a -> ('a * 'b) list -> 'b option
-  
+
 val power : int -> int -> int
 
 (** {2 Option Functions} *)
@@ -123,6 +125,9 @@ val option_all : 'a option list -> 'a list option
     similarly [y] in case [h y] returns [None]. *)
 val changed2 : ('a -> 'b -> 'c) -> ('a -> 'a option) -> 'a -> ('b -> 'b option) -> 'b -> 'c option
 
+val is_some : 'a option -> bool
+val is_none : 'a option -> bool
+
 (** {2 List Functions} *)
 
 (** [list_index p l] returns the first index [i] such that
@@ -139,14 +144,14 @@ val option_first: ('a -> 'b option) -> 'a list -> 'b option
     If for all elements of [l] the
     function [f] returns [None], then [map_changed f l] returns [None].
     Otherwise, it uses [x] for all elements, where [f x] returns [None],
-    and returns the resulting list. *)   
+    and returns the resulting list. *)
 val map_changed : ('a -> 'a option) -> 'a list -> 'a list option
 
 (** [map_changed_default d f l] maps [f] over [l].
     If for all elements of [l] the
     function [f] returns [None], then [map_changed f l] returns [None].
     Otherwise, it uses [d x] for all elements [x], where [f x] returns [None],
-    and returns the resulting list. *)   
+    and returns the resulting list. *)
 val map_changed_default : ('a -> 'b) -> ('a -> 'b option) -> 'a list -> 'b list option
 
 (** [list_mapi f l] maps [f] over [l]. In contrast to the standard
@@ -156,7 +161,7 @@ val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
 
 (** [list_iter sf f [a1; ...; an]] applies function [f] in turn to [a1; ...; an] and
     calls [sf ()] in between. It is equivalent to [begin f a1; sf(); f a2; sf(); ...; f an; () end]. *)
-val list_iter_sep : (unit -> unit) -> ('a -> unit) -> 'a list -> unit 
+val list_iter_sep : (unit -> unit) -> ('a -> unit) -> 'a list -> unit
 
 (** [map_filter f l] maps [f] over [l] and removes all entries [x] of [l]
     with [f x = None]. *)
@@ -184,6 +189,12 @@ val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
 
 val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int
 
+val take : int -> 'a list -> 'a list
+val drop : int -> 'a list -> 'a list
+
+val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
+
+val list_init : int -> (int -> 'a) -> 'a list
 
 (** {2 Files} *)
 
@@ -213,41 +224,16 @@ val string_to_list : string -> char list
 module IntSet : Set.S with type elt = int
 module IntIntSet : Set.S with type elt = int * int
 
-(** Some useful extra functions for sets *)
-module ExtraSet : functor (S : Set.S) ->
-   sig
-     (** Add a list of values to an existing set. *)
-     val add_list : S.t -> S.elt list -> S.t
-
-     (** Construct a set from a list. *)
-     val from_list : S.elt list -> S.t
+(** {2 Formatting functions} *)
 
-     (** Builds the union of a list of sets  *)
-     val list_union : S.t list -> S.t
-
-     (** Builds the intersection of a list of sets.
-         If the list is empty, a match exception is thrown. *)
-     val list_inter : S.t list -> S.t
-   end
-
-val list_init : int -> (int -> 'a) -> 'a list
-
-(*Formatting functions*)
 val string_of_list : string -> ('a -> string) -> 'a list -> string
 
 val string_of_option : ('a -> string) -> 'a option -> string
 
 val split_on_char : char -> string -> string list
 
-val is_some : 'a option -> bool
-val is_none : 'a option -> bool
-
-val take : int -> 'a list -> 'a list
-val drop : int -> 'a list -> 'a list
-
-val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
+(** {2 Terminal color codes} *)
 
-(* Terminal color codes *)
 val termcode : int -> string
 val bold : string -> string
 val darkgray : string -> string
@@ -260,14 +246,27 @@ val blue : string -> string
 val magenta : string -> string
 val clear : string -> string
 
-val warn : string -> unit
+(** {2 Encoding schemes for strings} *)
+
+(** z-encoding will take any string with ASCII characters in the range
+   32-126 inclusive, and map it to a string that just contains ASCII
+   upper and lower case letters and numbers, prefixed with the letter
+   z. This mapping is one-to-one. *)
 
 val zencode_string : string -> string
 val zencode_upper_string : string -> string
 
+(** Encode string for use as a filename. We can't use zencode directly
+   because some operating systems make the mistake of being
+   case-insensitive. *)
 val file_encode_string : string -> string
 
+(** {2 Misc output functions} *)
+
 val log_line : string -> int -> string -> string
+
 val header : string -> int -> string
 
 val progress : string -> string -> int -> int -> unit
+
+val warn : string -> unit