1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2025 -- Inria - CNRS - Paris-Saclay University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(********************************************************************)
open Why3
open Ident
open Ty
open Term
type hsymbol = private {
hs_name : ident;
}
module Mhs : Extmap.S with type key = hsymbol
module Shs : Extset.S with module M = Mhs
module Hhs : Exthtbl.S with type key = hsymbol
module Whs : Weakhtbl.S with type key = hsymbol
val hs_compare : hsymbol -> hsymbol -> int
val hs_equal : hsymbol -> hsymbol -> bool
val hs_hash : hsymbol -> int
val create_hsymbol : preid -> hsymbol
type param =
| Pt of tvsymbol
| Pv of vsymbol
| Pr of vsymbol
| Pc of hsymbol * vsymbol list * param list
type expr =
| Esym of hsymbol
| Eapp of expr * argument
| Elam of param list * expr
| Edef of expr * bool * defn list
| Eset of expr * (vsymbol * term) list
| Elet of expr * (vsymbol * term * bool) list
| Ecut of term * bool * expr
| Ebox of expr
| Ewox of expr
| Eany
and argument =
| At of ty
| Av of term
| Ar of vsymbol
| Ac of expr
and defn = hsymbol * vsymbol list * param list * expr
val debug_slow : Debug.flag
type context
val c_empty : context
val c_known : context -> Decl.known_map -> context
val c_merge : context -> context -> context (* c_merge old new *)
val vc_expr : context -> expr -> term
val vc_defn : context -> bool -> defn list -> context * (hsymbol * term) list
val vc_spec : context -> hsymbol ->
(Why3.Ident.preid * vsymbol list * term) list
|
