ty.mli 2.79 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 32

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

val create_tvsymbol : preid -> tvsymbol
33 34 35 36

(* type symbols and types *)

type tysymbol = private {
37
  ts_name : ident;
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
  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
53
module Hts : Hashtbl.S with type key = tysymbol
54 55

exception BadTypeArity
56 57 58 59
exception NonLinear
exception UnboundTypeVariable

val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
60 61 62 63 64 65

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
66 67
val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool
68

69 70
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
71 72
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
73

74 75
exception TypeMismatch

76 77
val matching : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ty_match : ty -> ty -> ty Mtv.t -> ty Mtv.t option
78

79 80 81 82 83 84 85 86
(* built-in symbols *)

val ts_int  : tysymbol
val ts_real : tysymbol

val ty_int  : ty
val ty_real : ty