term.mli 8.04 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
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) Francois Bobot, Jean-Christophe Filliatre,              *)
(*  Johannes Kanig and 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.                  *)
(*                                                                        *)
(**************************************************************************)
16 17 18

type label

19
(** Types *)
20 21 22

module Ty : sig

23 24 25 26
  type tvsymbol = Name.t

  (* type symbols and types *)

27
  type tysymbol = private {
28 29 30 31
    ts_name : Name.t;
    ts_args : tvsymbol list;
    ts_def  : ty option;
    ts_tag  : int;
32 33
  }

34 35 36 37
  and ty = private {
    ty_node : ty_node;
    ty_tag  : int;
  }
38 39

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

43
  val create_tysymbol : Name.t -> tvsymbol list -> ty option -> tysymbol
44

45
  val ty_var : tvsymbol -> ty
46 47
  val ty_app : tysymbol -> ty list -> ty

48 49
  val ty_match : ty -> ty -> ty Name.M.t -> ty Name.M.t option

50 51
end

52
type tvsymbol = Ty.tvsymbol
53 54 55
type tysymbol = Ty.tysymbol
type ty = Ty.ty

56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
(** Variable symbols *)

type vsymbol = private {
  vs_name : Name.t;
  vs_ty : ty;
  vs_tag : int;
}

module Mvs : Map.S with type key = vsymbol
module Svs : Set.S with type elt = vsymbol

val create_vsymbol : Name.t -> ty -> vsymbol

(** Function symbols *)

71
type fsymbol = private {
72 73 74 75
  fs_name   : Name.t;
  fs_scheme : ty list * ty;
  fs_constr : bool;
  fs_tag    : int;
76 77
}

78 79 80
val create_fsymbol : Name.t -> ty list * ty -> bool -> fsymbol

(** Predicate symbols *)
81

82
type psymbol = private {
83 84 85
  ps_name   : Name.t;
  ps_scheme : ty list;
  ps_tag    : int;
86 87
}

88 89
val create_psymbol : Name.t -> ty list -> psymbol

90 91 92 93 94 95 96 97 98 99 100 101
(** Patterns *)

type pattern = private {
  pat_node : pattern_node;
  pat_ty : ty;
  pat_tag : int;
}

and pattern_node = private
  | Pwild
  | Pvar of vsymbol
  | Papp of fsymbol * pattern list
102
  | Pas  of pattern * vsymbol
103 104 105 106 107 108

(* smart constructors for patterns *)

val pat_wild : ty -> pattern
val pat_var : vsymbol -> pattern
val pat_app : fsymbol -> pattern list -> ty -> pattern
109 110 111
val pat_as  : pattern -> vsymbol -> pattern

val pat_alpha_equal : pattern -> pattern -> bool
112 113 114 115

(** Terms and formulas *)

type quant =
116 117 118
  | Fforall
  | Fexists

119
type binop =
120 121 122 123 124
  | Fand
  | For
  | Fimplies
  | Fiff

125 126
type term = private {
  t_node : term_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127
  t_label : label list;
128 129 130 131 132 133
  t_ty : ty;
  t_tag : int;
}

and fmla = private {
  f_node : fmla_node;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134
  f_label : label list;
135 136 137 138
  f_tag : int;
}

and term_node = private
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
  | Tbvar of int
140 141 142
  | Tvar of vsymbol
  | Tapp of fsymbol * term list
  | Tlet of term * bind_term
143
  | Tcase of term * tbranch list
144 145 146 147 148 149
  | Teps of bind_fmla

and fmla_node = private
  | Fapp of psymbol * term list
  | Fquant of quant * bind_fmla
  | Fbinop of binop * fmla * fmla
150
  | Fnot of fmla
151 152 153 154 155 156 157 158 159 160
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
  | Flet of term * bind_fmla
  | Fcase of term * fbranch list

and bind_term

and bind_fmla

161
and tbranch
162

163
and fbranch
164

165 166 167 168 169
module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
module Mfmla : Map.S with type key = fmla
module Sfmla : Set.S with type elt = fmla

170 171
(* smart constructors for term *)

172
val t_var : vsymbol -> term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173
val t_app : fsymbol -> term list -> ty -> term
174
val t_let : vsymbol -> term -> term -> term
175
val t_case : term -> (pattern * term) list -> ty -> term
176
val t_eps : vsymbol -> fmla -> term
177

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178 179
val t_label : label list -> term -> term
val t_label_add : label -> term -> term
180

181 182 183
(* smart constructors for fmla *)

val f_app : psymbol -> term list -> fmla
184 185
val f_forall : vsymbol -> fmla -> fmla
val f_exists : vsymbol -> fmla -> fmla
186
val f_and : fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
187
val f_or : fmla -> fmla -> fmla
188 189
val f_implies : fmla -> fmla -> fmla
val f_iff : fmla -> fmla -> fmla
190
val f_binary : binop -> fmla -> fmla -> fmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
191
val f_not : fmla -> fmla
192 193
val f_true : fmla
val f_false : fmla
194 195 196 197
val f_if : fmla -> fmla -> fmla -> fmla
val f_let : vsymbol -> term -> fmla -> fmla
val f_case :  term -> (pattern * fmla) list -> fmla

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
198 199
val f_label : label list -> fmla -> fmla
val f_label_add : label -> fmla -> fmla
200

201 202
(* bindings *)

203
val open_bind_term : bind_term -> vsymbol * term
204
val open_tbranch : tbranch -> pattern * Svs.t * term
205

206
val open_bind_fmla : bind_fmla -> vsymbol * fmla
207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
val open_fbranch : fbranch -> pattern * Svs.t * fmla

(* safe opening map/fold *)

val map_open_term : (term -> term) -> (fmla -> fmla) -> term -> term
val map_open_fmla : (term -> term) -> (fmla -> fmla) -> fmla -> fmla

val fold_open_term : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
                                         -> 'a -> term -> 'a

val fold_open_fmla : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
                                         -> 'a -> fmla -> 'a

val forall_open_term : (term -> bool) -> (fmla -> bool) -> term -> bool
val forall_open_fmla : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val exists_open_term : (term -> bool) -> (fmla -> bool) -> term -> bool
val exists_open_fmla : (term -> bool) -> (fmla -> bool) -> fmla -> bool

(* safe transparent map/fold *)

val map_trans_term : (term -> term) -> (fmla -> fmla) -> term -> term
val map_trans_fmla : (term -> term) -> (fmla -> fmla) -> fmla -> fmla

val fold_trans_term : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
                                          -> 'a -> term -> 'a

val fold_trans_fmla : ('a -> term -> 'a) -> ('a -> fmla -> 'a)
                                          -> 'a -> fmla -> 'a

val forall_trans_term : (term -> bool) -> (fmla -> bool) -> term -> bool
val forall_trans_fmla : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val exists_trans_term : (term -> bool) -> (fmla -> bool) -> term -> bool
val exists_trans_fmla : (term -> bool) -> (fmla -> bool) -> fmla -> bool
240

241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
(* variable occurrence check *)

val occurs_term : Svs.t -> term -> bool
val occurs_fmla : Svs.t -> fmla -> bool

val occurs_term_single : vsymbol -> term -> bool
val occurs_fmla_single : vsymbol -> fmla -> bool

(* substitution for variables *)

val subst_term : term Mvs.t -> term -> term
val subst_fmla : term Mvs.t -> fmla -> fmla

val subst_term_single : term -> vsymbol -> term -> term
val subst_fmla_single : term -> vsymbol -> fmla -> fmla

(* set of free variables *)

val freevars_term : term -> Svs.t
val freevars_fmla : fmla -> Svs.t

262 263
(* USE PHYSICAL EQUALITY *)
(*
264 265
(* equality *)

266 267
val t_equal : term -> term -> bool
val f_equal : fmla -> fmla -> bool
268
*)
269 270

(* alpha-equivalence *)
271

272
val t_alpha_equal : term -> term -> bool
273
val f_alpha_equal : fmla -> fmla -> bool
274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298

(* occurrence check *)

val t_occurs_term : term -> term -> bool
val t_occurs_fmla : term -> fmla -> bool
val f_occurs_term : fmla -> term -> bool
val f_occurs_fmla : fmla -> fmla -> bool

val t_alpha_occurs_term : term -> term -> bool
val t_alpha_occurs_fmla : term -> fmla -> bool
val f_alpha_occurs_term : fmla -> term -> bool
val f_alpha_occurs_fmla : fmla -> fmla -> bool

(* term/fmla replacement *)

val t_subst_term : term -> term -> term -> term
val t_subst_fmla : term -> term -> fmla -> fmla
val f_subst_term : fmla -> fmla -> term -> term
val f_subst_fmla : fmla -> fmla -> fmla -> fmla

val t_alpha_subst_term : term -> term -> term -> term
val t_alpha_subst_fmla : term -> term -> fmla -> fmla
val f_alpha_subst_term : fmla -> fmla -> term -> term
val f_alpha_subst_fmla : fmla -> fmla -> fmla -> fmla

299 300 301 302 303
(* term/fmla matching modulo alpha in the pattern *)

val t_match : term -> term -> term Mvs.t -> term Mvs.t option
val f_match : fmla -> fmla -> term Mvs.t -> term Mvs.t option