types.mli 4.21 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

  (* List of non-empty rectangles *)
  type t = (descr * descr) list
75
  val is_empty: t -> bool
76 77 78 79 80 81 82 83 84 85
  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
86 87 88 89
  val normal: descr -> normal

  val need_second: t -> bool
    (* Is there more than a single rectangle ? *)
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
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

114 115
module Arrow : sig
  val any : descr
116

117 118 119 120 121 122 123 124
  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.
    *)

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

130 131 132
  val domain: t -> descr
  val apply: t -> descr -> descr
    (* Always succeed; no check on the domain *)
133 134 135 136 137 138

  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
139 140 141
end


142 143 144 145 146 147 148 149
module Int : sig
  val any : descr

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

150 151 152 153
module Atom : sig
  val has_atom : descr -> atom -> bool
end

154
val normalize : descr -> descr
155 156 157 158 159 160 161 162 163 164

(** Subtyping and sample values **)

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

module Sample :
sig
  type t =
165
    | Int of Big_int.big_int
166
    | Atom of atom
167
    | Char of Chars.Unichar.t
168 169 170 171 172 173 174 175 176 177 178 179 180
    | 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
181
  val register_global : string -> descr -> unit
182
  val print_const : Format.formatter -> const -> unit
183 184
  val print : Format.formatter -> node -> unit
  val print_descr: Format.formatter -> descr -> unit
185
  val print_sample : Format.formatter -> Sample.t -> unit
186 187 188
end

val check: descr -> unit