types.mli 3.19 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
19
20
21
22
23
24
25
26
27
28
29
30

(** 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


(** 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 **)

31
val interval : Big_int.big_int -> Big_int.big_int -> descr
32
33
34
35
val atom     : atom -> descr
val times    : node -> node -> descr
val arrow    : node -> node -> descr
val record   : label -> bool -> node -> descr
36
37
val char     : Chars.Unichar.t -> descr
val char_class : Chars.Unichar.t -> Chars.Unichar.t -> descr
38
39
40
41
42
43
44
45
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
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

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
  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
  val normal: descr -> t
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

104
105
module Arrow : sig
  val any : descr
106

107
108
109
  type t
  val get: descr -> t
    (* Always succeed; no check <= Arrow.any *)
110

111
112
113
114
115
116
117
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
end


val normalize : node -> node
118
119
120
121
122
123
124
125
126
127

(** Subtyping and sample values **)

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

module Sample :
sig
  type t =
128
    | Int of Big_int.big_int
129
    | Atom of atom
130
    | Char of Chars.Unichar.t
131
132
133
134
135
136
137
138
139
140
141
142
143
    | 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
144
145
  val register_global : string -> descr -> unit

146
147
  val print : Format.formatter -> node -> unit
  val print_descr: Format.formatter -> descr -> unit
148
  val print_sample : Format.formatter -> Sample.t -> unit
149
150
151
end

val check: descr -> unit