ty.mli 3.34 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

20 21
open Ident

22 23
(** Types *)

24 25 26
type tvsymbol = private {
  tv_name : ident;
}
27 28 29 30 31

module Stv : Set.S with type elt = tvsymbol
module Mtv : Map.S with type key = tvsymbol
module Htv : Hashtbl.S with type key = tvsymbol

32 33
val tv_equal : tvsymbol -> tvsymbol -> bool

34
val create_tvsymbol : preid -> tvsymbol
35 36 37 38

(* type symbols and types *)

type tysymbol = private {
39
  ts_name : ident;
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
  ts_args : tvsymbol list;
  ts_def  : ty option;
}

and ty = private {
  ty_node : ty_node;
  ty_tag  : int;
}

and ty_node = private
  | Tyvar of tvsymbol
  | Tyapp of tysymbol * ty list

module Sts : Set.S with type elt = tysymbol
module Mts : Map.S with type key = tysymbol
55
module Hts : Hashtbl.S with type key = tysymbol
56
module Wts : Hashweak.S with type key = tysymbol
57

58 59
module Tty : Hashweak.Tagged with type t = ty

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
60 61 62
module Sty : Set.S with type elt = ty
module Mty : Map.S with type key = ty
module Hty : Hashtbl.S with type key = ty
63
module Wty : Hashweak.S with type key = ty
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
64

65 66 67
val ts_equal : tysymbol -> tysymbol -> bool
val ty_equal : ty -> ty -> bool

68
exception BadTypeArity of tysymbol * int * int
69
exception DuplicateTypeVar of tvsymbol
70
exception UnboundTypeVar of tvsymbol
71 72

val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
73 74 75 76 77 78

val ty_var : tvsymbol -> ty
val ty_app : tysymbol -> ty list -> ty

val ty_map : (ty -> ty) -> ty -> ty
val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
79 80
val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool
81

82 83
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
84 85
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
86

87
exception TypeMismatch of ty * ty
88

89 90
val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ty_inst  : ty Mtv.t -> ty -> ty
91

92 93
val ty_freevars : Stv.t -> ty -> Stv.t

94 95 96 97 98 99 100 101
(* built-in symbols *)

val ts_int  : tysymbol
val ts_real : tysymbol

val ty_int  : ty
val ty_real : ty

102 103
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
104 105

val is_ts_tuple : tysymbol -> bool
106