package zelus

  1. Overview
  2. Docs
module S : sig ... end

a set of initialization names

module M : sig ... end
val fprint_t : Stdlib.Format.formatter -> S.t -> unit
val fprint_tt : Stdlib.Format.formatter -> S.t M.t -> unit
type error =
  1. | Iless_than
exception Clash of error
val new_var : unit -> Definit.t
val ivalue : Definit.value -> Definit.t
val ione : Definit.t
val ihalf : Definit.t
val izero : Definit.t
val funtype : Definit.ti -> Definit.ti -> Definit.ti
val funtype_list : Definit.ti list -> Definit.ti -> Definit.ti
val product : Definit.ti list -> Definit.ti
val atom : Definit.t -> Definit.ti
val irepr : Definit.t -> Definit.t
val equal : Definit.t -> Definit.t -> bool
val add : Definit.t -> Definit.t list -> Definit.t list
val remove : Definit.t -> Definit.t list -> Definit.t list
val union : Definit.t list -> Definit.t list -> Definit.t list
val set : Definit.t list -> Definit.t list
val polarity_c : Definit.t -> bool -> unit

Sets the polarity of a type.

val increase_polarity : Definit.polarity -> Definit.t -> unit
val saturate_i : bool -> Definit.t -> unit
val less_v : Definit.value -> Definit.value -> bool
val less : Definit.ti -> Definit.ti -> unit

Sub-typing

val less_i : Definit.t -> Definit.t -> unit
val skeleton : Deftypes.typ -> Definit.ti

Computing an initialization type from a type

val skeleton_on_i : Definit.t -> Deftypes.typ -> Definit.ti
val fresh_on_i : Definit.t -> Definit.ti -> Definit.ti
val suptype : bool -> Definit.ti -> Definit.ti -> Definit.ti
val sup_i : bool -> Definit.t -> Definit.t -> Definit.t
val visit : int -> Definit.ti -> unit
val visit_i : int -> Definit.t -> unit
val mark : bool -> Definit.ti -> unit

Mark useful/useless types and sets the polarity

val imark : bool -> Definit.t -> unit
val shorten : Definit.ti -> unit
val shorten_i : Definit.t -> unit
val short_list : bool -> Definit.t list -> Definit.t list -> Definit.t list
val remove_polarity : Definit.polarity -> Definit.t list -> Definit.t list
val short : bool -> Definit.t list -> Definit.t -> Definit.t list
val simplify : bool -> Definit.ti -> Definit.ti
val isimplify : bool -> Definit.t -> Definit.t
val list_of_vars : S.elt list Stdlib.ref

Generalisation of a type

val gen : Definit.ti -> unit
val igen : S.elt -> int
val gen_set : S.elt list -> int
val relation : S.elt list -> (S.elt * Definit.t list) list

Computes the dependence relation from a list of initialisation variables

val generalise : Definit.ti -> Definit.ti_scheme

Main generalisation function

Instantiation of a type

val save : Definit.t -> unit
val cleanup : unit -> unit
val copy : Definit.ti -> Definit.ti
val icopy : Definit.t -> Definit.t
val subtype : bool -> Definit.ti -> Definit.ti
val halftype : bool -> Definit.ti -> Definit.ti
val half_i : bool -> Definit.t -> Definit.t
val filter_arrow : Definit.ti -> Definit.ti * Definit.ti
val filter_product : Definit.ti -> Definit.ti list
type tentry = {
  1. t_typ : Definit.ti;
  2. t_last : Definit.t;
}

An entry in the type environment

val penv : Stdlib.Format.formatter -> tentry Zident.Env.t -> unit