ty.mli 4.24 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    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

François Bobot's avatar
François Bobot committed
20
open Stdlib
21 22
open Ident

23 24
(** Types *)

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

module Mtv : Map.S with type key = tvsymbol
30
module Stv : Mtv.Set
31 32
module Htv : Hashtbl.S with type key = tvsymbol

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

Andrei Paskevich's avatar
Andrei Paskevich committed
35 36
val tv_hash : tvsymbol -> int

37
val create_tvsymbol : preid -> tvsymbol
38 39 40 41

(* type symbols and types *)

type tysymbol = private {
42
  ts_name : ident;
43 44 45 46 47 48
  ts_args : tvsymbol list;
  ts_def  : ty option;
}

and ty = private {
  ty_node : ty_node;
Andrei Paskevich's avatar
Andrei Paskevich committed
49
  ty_tag  : Hashweak.tag;
50 51 52 53 54 55 56
}

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

module Mts : Map.S with type key = tysymbol
57
module Sts : Mts.Set
58
module Hts : Hashtbl.S with type key = tysymbol
59
module Wts : Hashweak.S with type key = tysymbol
60

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
69 70 71
val ts_hash : tysymbol -> int
val ty_hash : ty -> int

72
exception BadTypeArity of tysymbol * int * int
73
exception DuplicateTypeVar of tvsymbol
74
exception UnboundTypeVar of tvsymbol
75 76

val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
77 78 79 80

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

François Bobot's avatar
Api doc  
François Bobot committed
81 82 83
(** {3 generic traversal functions} *)
(** traverse only one level of constructor, if you want full traversal
    you need to call those function inside your function *)
84 85
val ty_map : (ty -> ty) -> ty -> ty
val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
86 87
val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool
88

François Bobot's avatar
Api doc  
François Bobot committed
89
(** {3 symbol-wise map/fold} *)
90
(** visits every symbol of the type *)
91 92
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
93 94
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
95

96
exception TypeMismatch of ty * ty
97

98 99
val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ty_inst  : ty Mtv.t -> ty -> ty
100

101 102
val ty_freevars : Stv.t -> ty -> Stv.t

103 104
val check_ty_equal : ty -> ty -> unit

105 106 107 108 109 110 111 112
(* built-in symbols *)

val ts_int  : tysymbol
val ts_real : tysymbol

val ty_int  : ty
val ty_real : ty

113 114 115 116 117 118
val ts_func : tysymbol
val ts_pred : tysymbol

val ty_func : ty -> ty -> ty
val ty_pred : ty -> ty

119 120
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
121 122

val is_ts_tuple : tysymbol -> bool
123

124 125 126 127 128 129 130 131 132
(** {2 Operations on [ty option]} *)

type oty = ty option

exception UnexpectedProp

val oty_equal : oty -> oty -> bool
val oty_hash  : oty -> int

Andrei Paskevich's avatar
Andrei Paskevich committed
133
val oty_ty : oty -> ty
134 135 136 137 138 139 140 141 142 143
val oty_map : (ty -> ty) -> oty -> oty
val oty_iter : (ty -> unit) -> oty -> unit
val oty_apply : 'a -> (ty -> 'a) -> oty -> 'a
val oty_fold : ('a -> ty -> 'a) -> 'a -> oty -> 'a
val oty_map_fold : ('a -> ty -> 'a * ty) -> 'a -> oty -> 'a * oty

val oty_match : ty Mtv.t -> oty -> oty -> ty Mtv.t
val oty_inst  : ty Mtv.t -> oty -> oty
val oty_freevars : Stv.t -> oty -> Stv.t