types.mli 4.53 KB
Newer Older
1
2
type label = int
type atom  = int
3
type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

(** Algebra **)

type node
type descr

val make: unit -> node
val define: node -> descr -> unit

val cons: descr -> node
val internalize: node -> node

val id: node -> int
val descr: node -> descr

19
20
21
val equal_descr: descr -> descr -> bool
val hash_descr: descr -> int

22

23
module DescrHash: Hashtbl.S with type key = descr
24
25
26
27
module DescrMap: Map.S with type key = descr

(* Note: it seems that even for non-functional data, DescrMap
is more efficient than DescrHash ... *)
28

29
30
31
32
33
34
35
36
37
38
39
(** Boolean connectives **)

val cup    : descr -> descr -> descr
val cap    : descr -> descr -> descr
val diff   : descr -> descr -> descr
val neg    : descr -> descr
val empty  : descr
val any    : descr

(** Constructors **)

40
val interval : Intervals.t -> descr
41
val atom     : atom Atoms.t -> descr
42
43
44
val times    : node -> node -> descr
val arrow    : node -> node -> descr
val record   : label -> bool -> node -> descr
45
val char     : Chars.t -> descr
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
val constant : const -> descr

(** Positive systems and least solutions **)

module Positive :
sig
  type v
  val forward: unit -> v
  val define: v -> v -> unit
  val ty: descr -> v
  val cup: v list -> v
  val times: v -> v -> v

  val solve: v -> node
end

(** Labels and atom names **)

val mk_atom  : string -> atom
val atom_name : atom -> string

val label : string -> label
val label_name : label -> string

(** Normalization **)

module Product : sig
  val any : descr
74
75
  val other : descr -> descr
  val is_product : descr -> bool
76
77
78

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
79
  val is_empty: t -> bool
80
81
82
83
84
85
86
87
88
89
  val get: descr -> t
  val pi1: t -> descr
  val pi2: 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
90
91
92
93
  val normal: descr -> normal

  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
end

module Record : sig
  val any : descr

  (* List of maps label -> (optional, content) *)
  type t = (label, (bool * descr)) SortedMap.t list
  val get: descr -> t
  val is_empty: t -> bool
  val restrict_label_present: t -> label -> t
  val restrict_field: t -> label -> descr -> t
  val restrict_label_absent: t -> label -> t
  val project_field: t -> label -> descr

  type normal = 
      [ `Success
      | `Fail
      | `Label of label * (descr * normal) list * normal ]
  val normal: descr -> normal

  val project : descr -> label -> descr
    (* Raise Not_found if label is not necessarily present *)
end

118
119
module Arrow : sig
  val any : descr
120

121
122
123
124
125
126
127
128
  val check_strenghten: descr -> descr -> descr
    (* [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.
    *)

129
130
  val check_iface: (descr * descr) list -> descr -> bool

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

136
137
138
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
139
140
141
142
143
144

  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
145
146
147
end


148
module Int : sig
149
150
  val has_int : descr -> Big_int.big_int -> bool

151
152
153
154
155
156
157
  val any : descr

  val is_int : descr -> bool
  val get: descr -> Intervals.t
  val put: Intervals.t -> descr
end

158
159
160
161
module Atom : sig
  val has_atom : descr -> atom -> bool
end

162
163
module Char : sig
  val has_char : descr -> Chars.Unichar.t -> bool
164
  val any : descr
165
166
end

167
val normalize : descr -> descr
168
169
170
171
172
173
174
175
176
177

(** Subtyping and sample values **)

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

module Sample :
sig
  type t =
178
    | Int of Big_int.big_int
179
    | Atom of atom
180
    | Char of Chars.Unichar.t
181
182
183
184
185
186
187
188
189
190
191
192
193
    | Pair of t * t
    | Record of (label * t) list
    | Fun of (node * node) list

  val get : descr -> t
	(** 
	  Extract a sample value from a non empty type;
	  raise Not_found for an empty type
	**)
end

module Print :
sig
194
  val register_global : string -> descr -> unit
195
  val print_const : Format.formatter -> const -> unit
196
197
  val print : Format.formatter -> node -> unit
  val print_descr: Format.formatter -> descr -> unit
198
  val print_sample : Format.formatter -> Sample.t -> unit
199
200
201
end

val check: descr -> unit