viewcvs.cgi/types/types.mli

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


module Const: Custom.T with type t = const


module CompUnit : sig
  include Custom.T

  val mk: U.t -> t
  val value: t -> U.t

  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 Abstract : sig
  type abs = CompUnit.t * Ident.id
  type t
  val any: t
  val atom: abs -> t

  module V : sig
    type t = abs * Obj.t
  end

  val contains: abs -> t -> bool
end

(** Algebra **)

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 any_node : Node.t

val non_constructed : t

(** Constructors **)

type pair_kind = [ `Normal | `XML ]

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'  : bool * Node.t label_map -> t
val char     : Chars.t -> t
val constant : const -> t
val abstract : Abstract.t -> t

(** Helpers *)

val tuple : Node.t list -> t

  (** given a list of descrs create an OR type including all descrs *)
val choice_of_list: t list -> t

  (** do it yourself: create an Xml type from three types (tag type, attribute
  type, content type) *)
val xml': t -> t -> t -> t

  (** Build a record from a list of <name,t> pairs. Open defaults to true.
  All specified fields are required. *)
val rec_of_list: ?opened:bool -> (Ns.qname * t) list -> t

  (** Similiar to rec_of_list, the additional boolean value specify whether the
  specified field is optional (true) or not (false. *)
val rec_of_list': ?opened:bool -> (bool * Ns.qname * t) list -> t

val empty_closed_record: t
val empty_opened_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

(** Normalization **)

module Product : sig
  val any : t
  val any_xml : 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 ? *)
end

module Record : sig
  val any : t
  val or_absent: t -> t
  val any_or_absent: 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 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 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
end

module Arrow : sig
  val any : t

  val sample: t -> t

  val check_strenghten: t -> 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_iface: (t * t) list -> t -> bool

  type t
  val is_empty: t -> bool
  val get: descr -> t
    (* Always succeed; no check <= Arrow.any *)

  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)

  val need_arg : t -> bool
    (* 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 apply_noarg : t -> descr
end


module Int : sig
  val has_int : t -> Intervals.V.t -> bool
  val get: t -> Intervals.t
  val any : t
end

module Atom : sig
  val has_atom : t -> Atoms.V.t -> bool
  val get: t -> Atoms.t
  val any : t
end

module Char : sig
  val has_char : t -> Chars.V.t -> bool
  val is_empty : t -> bool
  val get: t -> Chars.t
  val any : t
end

val get_abstract: t -> Abstract.t

val normalize : t -> t

(** Subtyping  **)

val is_empty : t -> bool
val non_empty: t -> bool
val subtype  : t -> t -> bool

module Print :
sig
  val register_global : U.t -> t -> unit
  val print_const : Format.formatter -> const -> unit
  val print: Format.formatter -> t -> unit
end

1	abate	233	open Ident
2
3	abate	672	type const =
4			\| Integer of Intervals.V.t
5			\| Atom of Atoms.V.t
6			\| Char of Chars.V.t
7			\| Pair of const * const
8			\| Xml of const * const
9			\| Record of const label_map
10			\| String of U.uindex * U.uindex * U.t * const
11	abate	1
12	abate	672
13	abate	691	module Const: Custom.T with type t = const
14	abate	271
15	abate	713
16			module CompUnit : sig
17			include Custom.T
18
19			val mk: U.t -> t
20			val value: t -> U.t
21
22			val enter: t -> unit
23			val leave: unit -> unit
24			val close_serialize: unit -> t list
25
26			val pervasives: t
27
28			module Tbl : Inttbl.S with type key = t
29			end
30
31	abate	956	module Abstract : sig
32			type abs = CompUnit.t * Ident.id
33			type t
34			val any: t
35			val atom: abs -> t
36
37			module V : sig
38			type t = abs * Obj.t
39			end
40
41			val contains: abs -> t -> bool
42			end
43
44	abate	1	( Algebra )
45
46	abate	653	include Custom.T
47			module Node : Custom.T
48	abate	698
49	abate	653	type descr = t
50	abate	1
51	abate	653	val make: unit -> Node.t
52			val define: Node.t -> t -> unit
53	abate	1
54	abate	653	val cons: t -> Node.t
55			val internalize: Node.t -> Node.t
56	abate	1
57	abate	653	val id: Node.t -> int
58			val descr: Node.t -> t
59	abate	1
60			( Boolean connectives )
61
62	abate	653	val cup : t -> t -> t
63			val cap : t -> t -> t
64			val diff : t -> t -> t
65			val neg : t -> t
66			val empty : t
67			val any : t
68	abate	1
69	abate	653	val any_node : Node.t
70	abate	167
71	abate	653	val non_constructed : t
72	abate	407
73	abate	1	( Constructors )
74
75	abate	110	type pair_kind = [ `Normal \| `XML ]
76
77	abate	653	val interval : Intervals.t -> t
78			val atom : Atoms.t -> t
79			val times : Node.t -> Node.t -> t
80			val xml : Node.t -> Node.t -> t
81			val arrow : Node.t -> Node.t -> t
82			val record : label -> Node.t -> t
83	abate	501	(* bool = true -> open record; bool = false -> closed record *)
84	abate	653	val record' : bool * Node.t label_map -> t
85			val char : Chars.t -> t
86			val constant : const -> t
87	abate	956	val abstract : Abstract.t -> t
88	abate	1
89	abate	501	(** Helpers *)
90
91	abate	1146	val tuple : Node.t list -> t
92
93	abate	501	(** given a list of descrs create an OR type including all descrs *)
94	abate	653	val choice_of_list: t list -> t
95	abate	501
96			(** do it yourself: create an Xml type from three types (tag type, attribute
97			type, content type) *)
98	abate	653	val xml': t -> t -> t -> t
99	abate	501
100	abate	653	(** Build a record from a list of <name,t> pairs. Open defaults to true.
101	abate	501	All specified fields are required. *)
102	abate	802	val rec_of_list: ?opened:bool -> (Ns.qname * t) list -> t
103	abate	501
104			(** Similiar to rec_of_list, the additional boolean value specify whether the
105			specified field is optional (true) or not (false. *)
106	abate	802	val rec_of_list': ?opened:bool -> (bool * Ns.qname * t) list -> t
107	abate	501
108	abate	653	val empty_closed_record: t
109			val empty_opened_record: t
110	abate	501
111	abate	1	( Positive systems and least solutions )
112
113			module Positive :
114			sig
115			type v
116			val forward: unit -> v
117			val define: v -> v -> unit
118	abate	653	val ty: t -> v
119	abate	1	val cup: v list -> v
120			val times: v -> v -> v
121	abate	263	val xml: v -> v -> v
122	abate	1
123	abate	653	val solve: v -> Node.t
124	abate	1	end
125
126			( Normalization )
127
128			module Product : sig
129	abate	653	val any : t
130			val any_xml : t
131			val other : ?kind:pair_kind -> t -> t
132			val is_product : ?kind:pair_kind -> t -> bool
133	abate	1
134			(* List of non-empty rectangles *)
135			type t = (descr * descr) list
136	abate	19	val is_empty: t -> bool
137	abate	110	val get: ?kind:pair_kind -> descr -> t
138	abate	1	val pi1: t -> descr
139			val pi2: t -> descr
140	abate	229	val pi2_restricted: descr -> t -> descr
141	abate	1
142			(* Intersection with (pi1,Any) *)
143			val restrict_1: t -> descr -> t
144
145			(* List of non-empty rectangles whose first projection
146			are pair-wise disjunct *)
147			type normal = t
148	abate	110	val normal: ?kind:pair_kind -> descr -> normal
149	abate	19
150	abate	355	val constraint_on_2: normal -> descr -> descr
151			(* constraint_on_2 n t1: maximal t2 such that (t1,t2) <= n *)
152			(* Assumption: t1 <= pi1(n) *)
153
154	abate	19	val need_second: t -> bool
155			(* Is there more than a single rectangle ? *)
156	abate	1	end
157
158			module Record : sig
159	abate	653	val any : t
160			val or_absent: t -> t
161			val any_or_absent: t
162	abate	229
163	abate	653	val has_absent: t -> bool
164			val has_record: t -> bool
165	abate	229
166	abate	653	val split : t -> label -> Product.t
167			val split_normal : t -> label -> Product.normal
168	abate	229
169	abate	653	val project : t -> label -> t
170	abate	229	(* Raise Not_found if label is not necessarily present *)
171
172	abate	653	val condition : t -> label -> t -> t
173	abate	242	(* condition t1 l t2 : What must follow if field l hash type t2 *)
174	abate	653	val project_opt : t -> label -> t
175			val has_empty_record: t -> bool
176	abate	242
177
178	abate	653	val first_label: t -> label
179	abate	229
180	abate	653	val empty_cases: t -> bool * bool
181	abate	229
182	abate	653	val merge: t -> t -> t
183			val remove_field: t -> label -> t
184	abate	364
185	abate	653	val get: t -> ((bool * t) label_map * bool * bool) list
186	abate	1	end
187
188	abate	11	module Arrow : sig
189	abate	653	val any : t
190	abate	1
191	abate	653	val sample: t -> t
192	abate	407
193	abate	653	val check_strenghten: t -> t -> t
194	abate	19	(* [check_strenghten t s]
195			Assume that [t] is an intersection of arrow types
196			representing the interface of an abstraction;
197			check that this abstraction has type [s] (otherwise raise Not_found)
198			and returns a refined type for this abstraction.
199			*)
200
201	abate	653	val check_iface: (t * t) list -> t -> bool
202	abate	45
203	abate	11	type t
204	abate	19	val is_empty: t -> bool
205	abate	11	val get: descr -> t
206			(* Always succeed; no check <= Arrow.any *)
207
208			val domain: t -> descr
209			val apply: t -> descr -> descr
210			(* Always succeed; no check on the domain *)
211	abate	19
212			val need_arg : t -> bool
213			(* True if the type of the argument is needed to obtain
214			the type of the result (must use [apply]; otherwise,
215			[apply_noarg] is enough *)
216			val apply_noarg : t -> descr
217	abate	11	end
218
219
220	abate	16	module Int : sig
221	abate	656	val has_int : t -> Intervals.V.t -> bool
222	abate	653	val get: t -> Intervals.t
223			val any : t
224	abate	16	end
225
226	abate	17	module Atom : sig
227	abate	656	val has_atom : t -> Atoms.V.t -> bool
228	abate	653	val get: t -> Atoms.t
229			val any : t
230	abate	17	end
231
232	abate	45	module Char : sig
233	abate	656	val has_char : t -> Chars.V.t -> bool
234	abate	653	val is_empty : t -> bool
235			val get: t -> Chars.t
236			val any : t
237	abate	45	end
238
239	abate	956	val get_abstract: t -> Abstract.t
240
241	abate	653	val normalize : t -> t
242	abate	1
243	abate	407	( Subtyping )
244	abate	1
245	abate	653	val is_empty : t -> bool
246			val non_empty: t -> bool
247			val subtype : t -> t -> bool
248	abate	1
249			module Print :
250			sig
251	abate	653	val register_global : U.t -> t -> unit
252	abate	42	val print_const : Format.formatter -> const -> unit
253	abate	653	val print: Format.formatter -> t -> unit
254	abate	1	end
255