types.mli 3.5 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 24
module DescrHash: Hashtbl.S with type key = descr

25 26 27 28 29 30 31 32 33 34 35
(** 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 **)

36
val interval : Big_int.big_int -> Big_int.big_int -> descr
37
val atom     : atom Atoms.t -> descr
38 39 40
val times    : node -> node -> descr
val arrow    : node -> node -> descr
val record   : label -> bool -> node -> descr
41
val char     : Chars.t -> descr
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
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
70 71
  val other : descr -> descr
  val is_product : descr -> bool
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 104 105 106 107 108 109

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

110 111
module Arrow : sig
  val any : descr
112

113 114 115
  type t
  val get: descr -> t
    (* Always succeed; no check <= Arrow.any *)
116

117 118 119 120 121 122
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
end


123 124 125 126 127 128 129 130
module Int : sig
  val any : descr

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

131 132 133 134
module Atom : sig
  val has_atom : descr -> atom -> bool
end

135
val normalize : node -> node
136 137 138 139 140 141 142 143 144 145

(** Subtyping and sample values **)

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

module Sample :
sig
  type t =
146
    | Int of Big_int.big_int
147
    | Atom of atom
148
    | Char of Chars.Unichar.t
149 150 151 152 153 154 155 156 157 158 159 160 161
    | 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
162 163
  val register_global : string -> descr -> unit

164 165
  val print : Format.formatter -> node -> unit
  val print_descr: Format.formatter -> descr -> unit
166
  val print_sample : Format.formatter -> Sample.t -> unit
167 168 169
end

val check: descr -> unit