open Ident type const = | Integer of Intervals.V.t | Atom of Atoms.V.t | Char of Chars.V.t | Pair of const * const | Xml of const * const | Record of const label_map | String of U.uindex * U.uindex * U.t * const type service_params = | TProd of service_params * service_params | TOption of service_params | TList of string * service_params | TSet of service_params | TSum of service_params * service_params | TString of string | TInt of string | TInt32 of string | TInt64 of string | TFloat of string | TBool of string | TFile of string (* | TUserType of string * (string -> 'a) * ('a -> string) *) | TCoord of string | TCoordv of service_params * string | TESuffix of string | TESuffixs of string (* | TESuffixu of (string * (string -> 'a) * ('a -> string)) *) | TSuffix of (bool * service_params) | TUnit | TAny | TConst of string;; module Const: Custom.T with type t = const (* module CompUnit : sig include Custom.T val get_current: unit -> t val mk: U.t -> t val value: t -> U.t val print_qual: Format.formatter -> t -> unit val enter: t -> unit val leave: unit -> unit val close_serialize: unit -> t list val pervasives: t module Tbl : Inttbl.S with type key = t end *) module Abstracts : sig module T : Custom.T with type t = string type abs = T.t type t val any: t val atom: abs -> t val compare: t -> t -> int module V : sig type t = abs * Obj.t end val contains: abs -> t -> bool end (** Algebra **) module BoolAtoms : BoolVar.S with type s = Atoms.t and type elem = Atoms.t Var.var_or_atom module BoolIntervals : BoolVar.S with type s = Intervals.t and type elem = Intervals.t Var.var_or_atom module BoolChars : BoolVar.S with type s = Chars.t and type elem = Chars.t Var.var_or_atom module BoolAbstracts: BoolVar.S with type s = Abstracts.t and type elem = Abstracts.t Var.var_or_atom include Custom.T module Node : Custom.T type descr = t val make: unit -> Node.t val define: Node.t -> t -> unit val cons: t -> Node.t val internalize: Node.t -> Node.t val id: Node.t -> int val descr: Node.t -> t (** Boolean connectives **) val cup : t -> t -> t val cap : t -> t -> t val diff : t -> t -> t val neg : t -> t val empty : t val any : t val no_var : t -> bool val is_var : t -> bool val has_tlv : t -> bool val is_closed : Var.Set.t -> t -> bool val any_node : Node.t val empty_node : Node.t val non_constructed : t val non_constructed_or_absent : t (** Constructors **) type pair_kind = [ `Normal | `XML ] val var : Var.var -> t val interval : Intervals.t -> t val atom : Atoms.t -> t val times : Node.t -> Node.t -> t val xml : Node.t -> Node.t -> t val arrow : Node.t -> Node.t -> t val record : label -> Node.t -> t (** bool = true -> open record; bool = false -> closed record *) val record_fields : bool * Node.t label_map -> t val char : Chars.t -> t val constant : const -> t val abstract : Abstracts.t -> t (** Helpers *) val all_vars : t -> Var.Set.t val tuple : Node.t list -> t val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t val empty_closed_record: t val empty_open_record: t (** Positive systems and least solutions **) module Positive : sig type v val forward: unit -> v val define: v -> v -> unit val ty: t -> v val cup: v list -> v val times: v -> v -> v val xml: v -> v -> v val solve: v -> Node.t end module Substitution : sig val full : t -> (Var.var * t) list -> t val single : t -> (Var.var * t) -> t val freshen : Var.Set.t -> t -> t val hide_vars : t -> t end (** Normalization **) module Product : sig val any : t val any_xml : t val any_of: pair_kind -> t val other : ?kind:pair_kind -> t -> t val is_product : ?kind:pair_kind -> t -> bool (* List of non-empty rectangles *) type t = (descr * descr) list val is_empty: t -> bool val get: ?kind:pair_kind -> descr -> t val pi1: t -> descr val pi2: t -> descr val pi2_restricted: descr -> t -> descr (* Intersection with (pi1,Any) *) val restrict_1: t -> descr -> t (* List of non-empty rectangles whose first projection are pair-wise disjunct *) type normal = t val normal: ?kind:pair_kind -> descr -> normal val constraint_on_2: normal -> descr -> descr (* constraint_on_2 n t1: maximal t2 such that (t1,t2) <= n *) (* Assumption: t1 <= pi1(n) *) val need_second: t -> bool (* Is there more than a single rectangle ? *) val clean_normal: t -> t (* Merge rectangles with same second component *) end module Record : sig val any : t val absent : t val absent_node : Node.t val or_absent: t -> t val any_or_absent: t val any_or_absent_node : Node.t val has_absent: t -> bool val has_record: t -> bool val split : t -> label -> Product.t val split_normal : t -> label -> Product.normal val pi : label -> t -> t (* May contain absent *) val project : t -> label -> t (* Raise Not_found if label is not necessarily present *) val condition : t -> label -> t -> t (* condition t1 l t2 : What must follow if field l hash type t2 *) val project_opt : t -> label -> t val has_empty_record: t -> bool val first_label: t -> label val all_labels: t -> LabelSet.t val empty_cases: t -> bool * bool val merge: t -> t -> t val remove_field: t -> label -> t val get: t -> ((bool * t) label_map * bool * bool) list type t val focus: descr -> label -> t val get_this: t -> descr val need_others: t -> bool val constraint_on_others: t -> descr -> descr end module Arrow : sig val any : t val sample: t -> t (** [check_strenghten t s] Assume that [t] is an intersection of arrow types representing the interface of an abstraction; check that this abstraction has type [s] (otherwise raise Not_found) and returns a refined type for this abstraction. *) val check_strenghten: t -> t -> t val check_iface: (t * t) list -> t -> bool type t = descr * (descr * descr) list list val is_empty: t -> bool val get: descr -> t (* Always succeed; no check <= Arrow.any *) val domain: t -> descr (* Always succeed; no check on the domain *) val apply: t -> descr -> descr (** True if the type of the argument is needed to obtain the type of the result (must use [apply]; otherwise, [apply_noarg] is enough *) val need_arg : t -> bool val apply_noarg : t -> descr end module Int : sig val has_int : t -> Intervals.V.t -> bool val get: t -> BoolIntervals.t val any : t end module Atom : sig val has_atom : t -> Atoms.V.t -> bool val get: t -> BoolAtoms.t val any : t end module Char : sig val has_char : t -> Chars.V.t -> bool val is_empty : t -> bool val get: t -> BoolChars.t val any : t end module Abstract : sig val has_abstract : t -> Abstracts.T.t -> bool val get: t -> BoolAbstracts.t val any : t end (* val get_abstract: t -> Abstracts.t *) val normalize : t -> t (** Subtyping **) val is_empty : t -> bool val non_empty: t -> bool val subtype : t -> t -> bool val disjoint : t -> t -> bool val equiv : t -> t -> bool (** Tools for compilation of PM **) val cond_partition: t -> (t * t) list -> t list (* The second argument is a list of pair of types (ti,si) interpreted as the question "member of ti under the assumption si". The result is a partition of the first argument which is precise enough to answer all the questions. *) module Print : sig type gname = string * Ns.QName.t * (Var.var * t) list val register_global : gname -> t -> unit val pp_const : Format.formatter -> const -> unit val pp_type: Format.formatter -> t -> unit val pp_node: Format.formatter -> Node.t -> unit (* Don't try to find a global name at toplevel *) val pp_noname: Format.formatter -> t -> unit val string_of_type: t -> string val string_of_node: Node.t -> string val printf : t -> unit val dump: Format.formatter -> t -> unit val dump_by_id: Format.formatter -> int -> unit end module Service : sig val to_service_params: t -> service_params val to_string: service_params -> string end module Witness : sig type witness val pp: Format.formatter -> witness -> unit val printf : witness -> unit end val witness: t -> Witness.witness module Cache : sig type 'a cache val emp: 'a cache val find: (t -> 'a) -> t -> 'a cache -> 'a cache * 'a val memo: (t -> 'a) -> (t -> 'a) end module Tallying : sig type constr = |Pos of (Var.var * t) (** alpha <= t | alpha \in P *) |Neg of (t * Var.var) (** t <= alpha | alpha \in N *) exception UnSatConstr of string exception Step1Fail exception Step2Fail module CS : sig module M : sig type key = Var.var type t val compare : t -> t -> int val empty : t val add : Var.Set.t -> key -> descr*descr -> t -> t val singleton : key -> descr*descr -> t val pp : Format.formatter -> t -> unit val inter : Var.Set.t -> t -> t -> t end module E : sig include Map.S with type key = Var.var val pp : Format.formatter -> descr t -> unit end module ES : sig include Set.S with type elt = descr E.t val pp : Format.formatter -> t -> unit end module S : sig type t = M.t list val empty : t val add : M.t -> t -> t val singleton : M.t -> t val union : t -> t -> t val elements : t -> M.t list val fold : (M.t -> 'b -> 'b) -> M.t list -> 'b -> 'b val pp : Format.formatter -> t -> unit end type s = S.t type m = M.t type es = ES.t type sigma = t E.t type sl = sigma list val pp_s : Format.formatter -> s -> unit val pp_m : Format.formatter -> m -> unit val pp_e : Format.formatter -> sigma -> unit val pp_sl : Format.formatter -> sl -> unit (* val merge : m -> m -> m *) val singleton : constr -> s val sat : s val unsat : s val union : s -> s -> s val prod : Var.Set.t -> s -> s -> s end val norm : Var.Set.t -> t -> CS.s val merge : Var.Set.t -> CS.m -> CS.s val solve : Var.Set.t -> CS.s -> CS.es val unify : CS.sigma -> CS.sigma (* [s1 ... sn] . si is a solution for tallying problem if si # delta and for all (s,t) in C si @ s < si @ t *) val tallying : Var.Set.t -> (t * t) list -> CS.sl val (>>) : t -> CS.sigma -> t (** Symbolic Substitution Set *) type symsubst = |I (** Identity *) |S of CS.sigma (** Substitution *) |A of (symsubst * symsubst) (** Composition si (sj t) *) (** Cartesian Product of two symbolic substitution sets *) val ( ++ ) : symsubst list -> symsubst list -> symsubst list (** Evaluation of a substitution *) val (@@) : t -> symsubst -> t val domain : CS.sl -> Var.Set.t val codomain : CS.sl -> Var.Set.t val is_identity : CS.sl -> bool val identity : CS.sl val filter : (Var.t -> bool) -> CS.sl -> CS.sl end (** Square Subtype relation. [squaresubtype delta s t] . True if there exists a substitution such that s < t only considering variables that are not in delta *) val squaresubtype : Var.Set.t -> t -> t -> Tallying.CS.sl val is_squaresubtype : Var.Set.t -> t -> t -> bool (** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where subst is the set of substitution that make the application succeed, ss and tt are the expansions of s and t corresponding to that substitution and res is the type of the result of the application *) val apply_full : Var.Set.t -> t -> t -> t val apply_raw : Var.Set.t -> t -> t -> Tallying.CS.sl * t * t * t val squareapply : Var.Set.t -> t -> t -> (Tallying.CS.sl * t)