Source file Signatures.ml

(******************************************************************************)
(*                                                                            *)
(*                                  Inferno                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the MIT License, as described in the file LICENSE.               *)
(*                                                                            *)
(******************************************************************************)

(* This file defines the input and output signatures of several functors.     *)

(* We use [include] directives to avoid redundancy, but annotate them with
   @inline so as to hide them in the generated documentation. This also
   allows us to hide the names of these signatures, which are difficult
   to remember, due to the many variants that are needed. *)

(* -------------------------------------------------------------------------- *)

(**Every equivalence class (of unification variables) carries a unique
   identifier. This is used for several purposes, including constructing
   dictionaries (hash tables) whose keys are equivalence classes and mapping
   equivalence classes to decoded type variables. One must be aware that these
   identifiers are stable only while the unifier is inactive. So, a hash table
   whose keys are equivalence should not persist across a call to [unify]. *)
type id = int

(* -------------------------------------------------------------------------- *)

(* [SSTRUCTURE] describes just the type ['a structure]. *)

module type SSTRUCTURE = sig

  (**A structure is a piece of information that the unifier attaches to a
     variable (or, more accurately, to an equivalence class of variables).

     In some contexts, a structure represents a logical constraint that bears
     on a variable. A structure of type ['a structure] may itself contain
     variables, which are represented as values of type ['a]. We refer to
     these values as the children of this structure.

     In some contexts, a structure may record not only a logical constraint,
     but also other kinds of meta-information, such as the unique identifier
     of this equivalence class, where and how it is bound (its rank; whether
     it is rigid or flexible; etc.).

     For example, in the case of first-order unification, a structure might
     be an optional shallow term: that is,
     - either [None], which indicates the absence of a constraint;
     - or [Some term], where [term] is a shallow term
       (a term of depth 1 whose leaves are variables of type ['a]),
       which indicates the presence of an equality constraint. *)
  type 'a structure

end

(* [USTRUCTURE] describes an input of [Unifier.Make]. *)

module type USTRUCTURE = sig

  (** @inline *)
  include SSTRUCTURE

  (**[InconsistentConjunction] is raised by {!conjunction}. *)
  exception InconsistentConjunction

  (**[conjunction equate s1 s2] computes the logical conjunction [s] of the
     structures [s1] and [s2]. If these structures are logically inconsistent
     with one another (that is, if their conjunction implies a logical
     contradiction), then the exception {!InconsistentConjunction} is raised.

     [conjunction] invokes [equate] to emit auxiliary equality constraints
     that are necessary and sufficient for [s] to actually represent the
     conjunction of [s1] and [s2].

     For example, in the case of first-order unification, assuming that a
     structure is an optional shallow term:
     - the conjunction of [None] and [s] would be [s];
     - the conjunction of [s] and [None] would be [s];
     - the conjunction of [Some term1] and [Some term2], where the shallow
       terms [term1] and [term2] have the same head constructor,
       would be [Some term1] or [Some term2] (it does not matter which!),
       and [equate] would be invoked to equate the leaves of [term1] and
       [term2];
     - the conjunction of [Some term1] and [Some term2], where the shallow
       terms [term1] and [term2] have distinct head constructors,
       would raise {!InconsistentConjunction}. *)
  val conjunction:
    ('a -> 'a -> unit) -> 'a structure -> 'a structure -> 'a structure

end

(* [OCSTRUCTURE] describes an input of [OccursCheck.Make]. *)

module type OCSTRUCTURE = sig

  (** @inline *)
  include SSTRUCTURE

  (**[iter] applies an action to every child of a structure. *)
  val iter: ('a -> unit) -> 'a structure -> unit

  (**[id] extracts the unique identifier of a structure. *)
  val id: 'a structure -> id

end

(* [OSTRUCTURE] describes an input of [Decoder.Make]. *)

module type OSTRUCTURE = sig

  (** @inline *)
  include OCSTRUCTURE

  (**[map] applies a transformation to the children of a structure,
     while preserving the shape of the structure. *)
  val map: ('a -> 'b) -> 'a structure -> 'b structure

  (**[is_leaf s] determines whether the structure [s] is a leaf, that is,
     whether it represents the absence of a logical constraint. This function
     is typically used by a decoder to determine which equivalence classes
     should be translated to "type variables" in a decoded type. *)
  val is_leaf: 'a structure -> bool

end

(* [GSTRUCTURE] describes an input of [Structure.Option],
   and also describes part of its output. *)

module type GSTRUCTURE = sig

  (** @inline *)
  include USTRUCTURE

  (**[iter] applies an action to every child of a structure. *)
  val iter: ('a -> unit) -> 'a structure -> unit

  (**[fold] applies an action to every child of a structure,
     and carries an accumulator. *)
  val fold: ('a -> 'b -> 'b) -> 'a structure -> 'b -> 'b

  (**[map] applies a transformation to the children of a structure,
     while preserving the shape of the structure. *)
  val map: ('a -> 'b) -> 'a structure -> 'b structure

end

(* [STRUCTURE_LEAF] describes the output of [Structure.Option] and
   an input of [Generalization.Make]. *)

module type STRUCTURE_LEAF = sig

  (** @inline *)
  include GSTRUCTURE

  (**The constant [leaf] is a structure that represents the absence of a
     logical constraint. It is typically used when a variable is created
     fresh. *)
  val leaf: 'a structure

  (**[is_leaf s] determines whether the structure [s] is a leaf, that is,
     whether it represents the absence of a logical constraint. This function
     is typically used by a decoder to determine which equivalence classes
     should be translated to "type variables" in a decoded type. *)
  val is_leaf: 'a structure -> bool

end

(* [HSTRUCTURE] describes an input of [Solver.Make]. *)

module type HSTRUCTURE = sig

  (** @inline *)
  include GSTRUCTURE

  (**[pprint] is a structure printer, parameterized over a child printer.
     It is used for debugging purposes only. *)
  val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document

end

(* -------------------------------------------------------------------------- *)

(* [MUNIFIER] describes a fragment of the functionality offered by the
   unifier. This fragment provides read access to the unifier's data
   structures. This signature serves as an input of [OccursCheck.Make] and
   [Decoder.Make]. *)

module type MUNIFIER = sig

  (**A unifier maintains a graph whose vertices are equivalence classes of
     variables. With each equivalence class, a piece of information of type
     {!data} is attached. *)
  type variable

  (**The type ['a structure] describes the information that is attached with
     each class. It is parameterized over a type ['a] of children. In the
     definition of the type {!data}, ['a] is instantiated with [variable]. *)
  type 'a structure

  (**By definition, [data] is a synonym for [variable structure]. So, the data
     attached with an equivalence class of variables is a structure whose
     children are variables. *)
  type data = variable structure

  (**[get v] is the structure currently attached with the (equivalence class
     of the) variable [v]. The structure that is attached with a class can
     change when the unifier is invoked. *)
  val get: variable -> data

end

(* [GUNIFIER] describes the unifier that is embedded in the output of
   [Generalization.Make]. Some functions, especially [fresh], are removed.
   Exposing [fresh] would be undesirable: we want to hide the unifier's
   [fresh] function, because [Generalization.Make] overrides it with its own
   [fresh] function. *)

module type GUNIFIER = sig

  (** @inline *)
  include MUNIFIER

  (**This exception is raised by {!unify}. *)
  exception Unify of variable * variable

  (**[unify v1 v2] equates the two variables [v1] and [v2]. These variables
     become part of the same equivalence class. The structures carried by [v1]
     and [v2] are combined by invoking the [conjunction] function supplied by
     the user as an argument to [Unifier.Make]. [conjunction] itself is given
     access to an [equate] function which submits an equality constraint to
     the unifier.

     If a logical inconsistency is detected, [Unify (v1, v2)] is raised, and
     the state of the unifier is unaffected. (The unifier undoes any updates
     that it may have performed.) For this undo machinery to work correctly,
     the [conjunction] function provided by the user {i must not perform any
     side effect}.

     Unification can create cycles in the graph maintained by the unifier. By
     default, the unifier tolerates these cycles. An occurs check, which
     detects these cycles, is provided separately: see {!OccursCheck.Make}.
     Because cycles are permitted, the variables [v1] and [v2] carried by the
     exception {!Unify} can participate in cycles. When reporting a unification
     error, a cyclic decoder should be used: see {!Decoder.Make}. *)
  val unify: variable -> variable -> unit

end

(* [UNIFIER] describes the output of [Unifier.Make]. *)

module type UNIFIER = sig

  (** @inline *)
  include GUNIFIER

  (**[is_representative v] determines whether the variable [v] is currently
     the representative element of its equivalence class. *)
  val is_representative: variable -> bool

  (**[fresh s] creates a new variable whose structure is [s]. This variable
     forms an equivalence class of its own. *)
  val fresh: data -> variable

end

(* -------------------------------------------------------------------------- *)

(* [OCCURS_CHECK] describes the output of [OccursCheck.Make]. *)

module type OCCURS_CHECK = sig

  type variable

  type data

  (**[Cycle v] is raised by the occurs check. *)
  exception Cycle of variable

  (**[new_occurs_check is_young] initiates a cycle detection phase. It
     produces a function [check] that can be applied to a number of
     roots. The function [check] visits the vertices that are reachable from
     some root and that satisfy the user-supplied predicate [is_young]. If a
     cycle is detected, then [Cycle v] is raised, where [v] is a vertex that
     participates in the cycle.

     The function [check] has internal state and records the vertices that it
     has visited, so no vertex is visited twice: the complexity of the occurs
     check is linear in the size of the graph fragment that is visited. *)
  val new_occurs_check: (data -> bool) -> (variable -> unit)

end

(* -------------------------------------------------------------------------- *)

(* [OUTPUT] describes an input of [Decoder.Make] and [Solver.Make]. *)

module type OUTPUT = sig

  (** @inline *)
  include SSTRUCTURE

  (**A representation of decoded type variables. *)
  type tyvar

  (**A representation of decoded types. *)
  type ty

  (**[inject] provides an injection of unique integer identifiers into
     decoded type variables. *)
  val inject: id -> tyvar

  (**[variable v] is a representation of the type variable [v] as a decoded
     type. *)
  val variable: tyvar -> ty

  (**[structure s] turns [s], a structure whose children are decoded types,
     into a decoded type. *)
  val structure: ty structure -> ty

  (**If [v] is a type variable and [t] is a decoded type, then [mu v t] is a
     representation of the recursive type [mu v.t]. The function [mu] is used
     only by the cyclic decoder. *)
  val mu: tyvar -> ty -> ty

end

(* -------------------------------------------------------------------------- *)

(* [DECODER] describes the output of [Decoder.Make]. *)

module type DECODER = sig

  type variable
  type tyvar
  type ty

  (**[decode_variable v] decodes the variable [v]. *)
  val decode_variable: variable -> tyvar

  (**[new_acyclic_decoder()] initiates a new decoding phase. It returns a
     decoding function [decode], which can be used as many as times as one
     wishes. Decoding requires the graph to be acyclic: it is a bottom-up
     computation. [decode] internally performs memoization, so even if the
     decoder is called many times, the total cost of decoding is linear in the
     size of the graph fragment that is decoded.

     As a caveat that one must bear in mind, when the type [ty] of decoded
     types is a type of abstract syntax {i trees}, then the decoder actually
     produces a {i DAG} of type [ty]. Traversing this DAG in a naive way,
     without paying attention to the fact that some subtrees may be shared,
     can result in a traversal whose complexity is exponential. *)
  val new_acyclic_decoder: unit -> (variable -> ty)

  (**[new_cyclic_decoder] is analogous to {!new_acyclic_decoder}, but
     tolerates cyclic graphs. The decoder detects cycles and uses the function
     [mu] to decode them into equirecursive types. The decoder performs
     memoization only at the vertices that do {i not} participate in a cycle.
     This makes the complexity of decoding higher than the acyclic case, but
     we expect it to remain linear in practice. *)
  val new_cyclic_decoder: unit -> (variable -> ty)

end

(* -------------------------------------------------------------------------- *)

(* [TEVAR] describes an input of [Solver.Make]. *)

module type TEVAR = sig

  (**A type of variables. *)
  type t

  (** @inline *)
  include Hashtbl.HashedType with type t := t

  (**A conversion of variables to strings. This function is used for
     debugging purposes only. *)
  val to_string: t -> string

end