jon.recoil.org

Module Types.Rigid_name

Types shared by ikind algorithms.

type unknown_id
type t =
  1. | Atom of {
    1. constr : Path.t;
    2. arg_index : int;
      (*

      arg_index = 0 refers to the base contribution, and subsequent indices refer to the coefficients of the i-th argument. This is a positional index, not a type-variable id.

      *)
    }
  2. | KAtom of Path.t
    (*

    A jkind-atom path. Unlike Atom, this refers to a jkind alias path and should be interpreted through jkind lookup in an environment when possible.

    *)
  3. | Param of int
    (*

    Param id only occurs in formulas for type constructors. Refers to a type-parameter of the constructor, where id is the Types.get_id of the type variable representing the parameter.

    *)
  4. | Unknown of unknown_id
    (*

    An unknown quantity with a given id. Used to model not-best in ikinds. This is used when we couldn't compute a precise ikind, e.g. for a polymorphic variant with conjunctive type -- `Constr of (a & b & ...)

    *)
val compare : t -> t -> int

Ordering on rigid names used in the LDD to order the nodes.

val to_string : t -> string
val atomic : Path.t -> int -> t
val katom : Path.t -> t
val param : int -> t
val unknown : Shape.Uid.t -> t