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 include Bool.S with type elem = T.t module V : sig type t = T.t * Obj.t end val is_empty : t -> bool val sample : t -> elem option val print : t -> (Format.formatter -> unit) list val contains: elem -> t -> bool val contains_sample : elem option -> t -> bool end (** Algebra **) module Descr : Custom.T include Custom.T with type t = Descr.t module Node : Custom.T type descr = t type type_kind = [ `atoms | `intervals | `chars | `times | `xml | `arrow | `record | `abstracts ] val pp_type_kind : Format.formatter -> type_kind -> unit module type VarType = sig include Bool.V type descr = Descr.t val kind : type_kind val inj : t -> descr val proj : descr -> t val update : descr -> t -> descr end type var_type = (module VarType) module VarAtoms : VarType with type Atom.t = Atoms.t module VarIntervals : VarType with type Atom.t = Intervals.t module VarChars : VarType with type Atom.t = Chars.t module VarAbstracts : VarType with type Atom.t = Abstracts.t module Pair : Bool.S with type elem = Node.t * Node.t module Rec : Bool.S with type elem = bool * Node.t Ident.LabelMap.map module VarTimes : VarType with module Atom = Pair module VarXml : VarType with module Atom = Pair module VarArrow : VarType with module Atom = Pair module VarRec : VarType with module Atom = Rec 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.t -> 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 module Iter : sig val simplify : t -> t val map : ?abs:(bool -> bool) -> (var_type -> t -> t) -> t -> t val iter : ?abs:(bool -> unit) ->(var_type -> t -> unit) -> t -> unit val fold : ?abs:(bool -> 'a -> 'a) -> (var_type -> t -> 'a -> 'a) -> t -> 'a -> 'a val compute : default:'a -> ?cup:('a list -> 'a) -> ?cap:('a list -> 'a) -> ?neg:('a -> 'a) -> ?var:(Var.t -> 'a) -> ?atoms:(Atoms.t -> 'a) -> ?ints:(Intervals.t -> 'a) -> ?chars:(Chars.t -> 'a) -> ?times:((Node.t * Node.t) -> 'a) -> ?xml:((Node.t*Node.t) -> 'a) -> ?arrow:((Node.t*Node.t) -> 'a) -> ?record:((bool * Node.t Ident.LabelMap.map) -> 'a) -> ?abstract:(Abstracts.t -> 'a) -> ?absent:(bool -> 'a) -> t -> 'a end (** 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 Variable : sig val extract : t -> Var.t * bool end module Subst : sig type t = descr Var.Map.map val identity : t val print : Format.formatter -> t -> unit val full : descr -> t -> descr val full_list : descr -> (Var.t * descr) list -> descr val single : descr -> (Var.t * descr) -> descr val freshen : Var.Set.t -> descr -> descr val hide_vars : descr -> descr val solve_rectype : descr -> Var.t -> descr val clean_type : Var.Set.t -> descr -> descr 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 -> VarIntervals.t val any : t end module Atom : sig val has_atom : t -> Atoms.V.t -> bool val get: t -> VarAtoms.t val any : t end module Char : sig val has_char : t -> Chars.V.t -> bool val is_empty : t -> bool val get: t -> VarChars.t val any : t end module Abstract : sig val has_abstract : t -> Abstracts.T.t -> bool val get: t -> VarAbstracts.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 (** intermediary representation for records *) (*** TODO : SEAL OFF *) val get_record : Rec.t -> (Label.t list * (bool * t array) * ((bool * t array) list)) list (** 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.t * 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 lookup : t -> 'a cache -> 'a option val memo: (t -> 'a) -> (t -> 'a) end