ty.mli 2.64 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
type tvsymbol = ident
25 26 27 28

(* type symbols and types *)

type tysymbol = private {
29
  ts_name : ident;
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
  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

exception NonLinear
exception UnboundTypeVariable

46 47
val create_tvsymbol : preid -> tvsymbol
val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
48 49 50

module Sts : Set.S with type elt = tysymbol
module Mts : Map.S with type key = tysymbol
51
module Hts : Hashtbl.S with type key = tysymbol
52 53 54 55 56 57 58 59 60 61 62

exception BadTypeArity

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
val ty_forall : (ty -> bool) -> ty -> bool
val ty_exists : (ty -> bool) -> ty -> bool

63 64 65 66 67
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
val ty_s_forall : (tysymbol -> bool) -> ty -> bool
val ty_s_exists : (tysymbol -> bool) -> ty -> bool

68 69
exception TypeMismatch

70 71
val matching : ty Mid.t -> ty -> ty -> ty Mid.t
val ty_match : ty -> ty -> ty Mid.t -> ty Mid.t option
72

73 74 75 76 77 78 79 80
(* built-in symbols *)

val ts_int  : tysymbol
val ts_real : tysymbol

val ty_int  : ty
val ty_real : ty