package zelus

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

a set of causality names

module M : sig ... end
module K : sig ... end
val fprint_t : Stdlib.Format.formatter -> S.t -> unit
val fprint_tt : Stdlib.Format.formatter -> S.t M.t -> unit
type cycle = Defcaus.t list
type error = cycle
exception Clash of error
val new_var : unit -> Defcaus.t
val new_var_with_info : Defcaus.t -> Defcaus.t
val new_gen_var : unit -> Defcaus.t
val product : Defcaus.tc list -> Defcaus.tc
val funtype : Defcaus.tc -> Defcaus.tc -> Defcaus.tc
val funtype_list : Defcaus.tc list -> Defcaus.tc -> Defcaus.tc
val atom : Defcaus.t -> Defcaus.tc
val crepr : Defcaus.t -> Defcaus.t
val equal : Defcaus.t -> Defcaus.t -> bool
val add : Defcaus.t -> Defcaus.t list -> Defcaus.t list
val remove : Defcaus.t -> Defcaus.t list -> Defcaus.t list
val mem : Defcaus.t -> Defcaus.t list -> bool
val union : Defcaus.t list -> Defcaus.t list -> Defcaus.t list
val set : Defcaus.t list -> Defcaus.t list
val sups : Defcaus.t -> Defcaus.t list
val allsups : Defcaus.t list -> Defcaus.t -> Defcaus.t list
val annotate : Defcaus.info -> Defcaus.tc -> Defcaus.tc
val cannotate : Defcaus.info -> Defcaus.t -> Defcaus.t
val vars : S.t -> Defcaus.tc -> S.t
val vars_c : S.t -> S.elt -> S.t
val polarity : bool -> Defcaus.tc -> unit

Sets the polarity of a type.

val polarity_c : bool -> Defcaus.t -> unit
val increase_polarity : Defcaus.polarity -> Defcaus.t -> unit
val occur_check : Defcaus.t -> Defcaus.t -> unit

check for cycles. Does left_c appears in right_c and its

val check_type : Defcaus.tc -> unit
val less : Defcaus.tc -> Defcaus.tc -> unit

order < between types

val less_c : Defcaus.t -> Defcaus.t -> unit
val intro_less_c : Defcaus.t -> Defcaus.t
val strict_path : Defcaus.t -> Defcaus.t -> bool
val path : Defcaus.t -> Defcaus.t -> bool
val fresh : Defcaus.tc -> Defcaus.tc
val fresh_on_c : Defcaus.t -> Defcaus.tc -> Defcaus.tc
val suptype : bool -> Defcaus.tc -> Defcaus.tc -> Defcaus.tc
val sup_c : bool -> Defcaus.t -> Defcaus.t -> Defcaus.t
val suptype_list : bool -> Defcaus.tc list -> Defcaus.tc
val skeleton : Deftypes.typ -> Defcaus.tc

Computing a causality type from a type

val skeleton_on_c : Defcaus.t -> Deftypes.typ -> Defcaus.tc
val skeleton_for_variables : Deftypes.typ -> Defcaus.tc
val on_c : Defcaus.tc -> S.elt -> Defcaus.tc
val mark : Defcaus.tc -> unit

Simplification of types

val mark_c : Defcaus.t -> unit
val mark_and_polarity : bool -> Defcaus.tc -> unit
val is_an_output : Defcaus.t -> bool
val ins_and_outs : S.t -> S.t * S.t
val ins_and_outs_of_a_type : bool -> (S.t * S.t) -> Defcaus.tc -> S.t * S.t
val outrec : S.t -> S.elt -> S.t
val out : S.elt -> S.t
val outset : S.t -> S.t
val io : S.t -> S.t M.t -> M.key -> S.t
val build_o_table : S.t -> S.t M.t -> S.t M.t
val build_io_table : S.t -> S.t M.t -> S.t -> S.t M.t -> S.t M.t
val build_ki_table : K.key M.t -> Defcaus.t K.t * S.t M.t
val filter : S.t M.t -> S.t M.t
val simplify_by_io : Defcaus.tc -> Defcaus.tc
val shorten : Defcaus.tc -> unit
val shorten_c : Defcaus.t -> unit
val short_list : bool -> Defcaus.t list -> Defcaus.t list -> Defcaus.t list
val remove_polarity : Defcaus.polarity -> Defcaus.t list -> Defcaus.t list
val short : bool -> Defcaus.t list -> Defcaus.t -> Defcaus.t list
val csimplify : bool -> Defcaus.t -> Defcaus.t
val simplify : bool -> Defcaus.tc -> Defcaus.tc
val shrink_cycle : S.t -> S.elt list -> S.elt list
val keep_names_in_cycle : S.t -> S.elt list -> S.elt list
val reduce : S.t -> unit
val relation : (S.t * 'a) -> S.t -> S.t * (S.elt * Defcaus.t list) list

Computes the dependence relation from a list of causality variables

val list_of_vars : Defcaus.t list Stdlib.ref

Generalisation of a type

val gen : Defcaus.tc -> unit
val cgen : Defcaus.t -> int
val gen_set : Defcaus.t list -> int
val generalise : Defcaus.tc -> Defcaus.tc_scheme

Main generalisation function

Instantiation of a type

val save : Defcaus.t -> unit
val cleanup : unit -> unit
val copy : Defcaus.tc -> Defcaus.tc
val subtype : bool -> Defcaus.tc -> Defcaus.tc

Type instance

val filter_product : int -> Defcaus.tc -> Defcaus.tc list
val filter_arrow : Defcaus.tc -> Defcaus.tc * Defcaus.tc
type tentry = {
  1. t_typ : Defcaus.tc;
  2. t_last_typ : Defcaus.tc option;
}
val simplify_by_io_env : tentry Zident.Env.t -> Defcaus.tc -> Defcaus.tc -> tentry Zident.Env.t * S.t * (S.elt * Defcaus.t list) list * Defcaus.tc * Defcaus.tc
val prel : Stdlib.Format.formatter -> (Defcaus.t * Defcaus.t list) list -> unit
val penv : Stdlib.Format.formatter -> tentry Zident.Env.t -> unit