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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
(********************************************************************)
(* *)
(* 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
type pvar =
Ptree.ident * Ptree.term * Ptree.pty * bool
type pparam =
| PPt of Ptree.ident
| PPv of Ptree.ident * Ptree.pty
| PPr of Ptree.ident * Ptree.pty
| PPc of
Ptree.ident * Ptree.ident list * pparam list
| PPa of Ptree.term * bool
| PPo
| PPb
| PPl of pvar list
type pexpr = {
pexpr_desc : pexpr_desc;
pexpr_loc : Loc.position;
}
and pexpr_desc =
| PEsym of Ptree.qualid
| PEapp of pexpr * pargument
| PElam of pparam list * pexpr
| PEdef of pexpr * bool * pdefn list
| PEset of pexpr * (Ptree.ident * Ptree.term) list
| PElet of pexpr * pvar list
| PEcut of (Ptree.term * bool) list * pexpr
| PEbox of pexpr
| PEwox of pexpr
| PEany
and pargument =
| PAt of Ptree.pty
| PAv of Ptree.term
| PAr of Ptree.ident
| PAc of pexpr
and pdefn = {
pdefn_desc : pdefn_desc;
pdefn_loc : Loc.position;
}
and pdefn_desc = {
pdefn_name : Ptree.ident;
pdefn_writes : Ptree.ident list;
pdefn_params : pparam list;
pdefn_body : pexpr;
}
type use =
| Puseexport of Ptree.qualid
| Puseimport of
bool * Ptree.qualid * Ptree.ident option
type pdecl =
| Blo of pdefn list
| Mlw of Ptree.decl
| Use of use
type pfile = (Ptree.ident * pdecl list) list
module PP : sig
open Format
val pr : Ident.ident_printer
val pp_osp : formatter -> bool -> unit
val pp_sp_nl2 : formatter -> unit -> unit
val pp_tv : formatter -> Ty.tvsymbol -> unit
val pp_ty : formatter -> Ty.ty -> unit
val pp_hs : formatter -> Coma_logic.hsymbol -> unit
val pp_term : formatter -> Term.term -> unit
val pp_ofty : formatter -> Ty.ty -> unit
val pp_pval : formatter -> Term.vsymbol -> unit
val pp_var :
bool -> formatter -> Term.vsymbol -> unit
val pp_hdl :
formatter ->
Coma_logic.hsymbol
* Term.vsymbol list
* Coma_logic.param list ->
unit
val pp_prew : formatter -> Term.vsymbol list -> unit
val pp_prms : formatter -> Coma_logic.param list -> unit
val pp_param : formatter -> Coma_logic.param -> unit
val pp_set :
formatter ->
(Term.vsymbol * Term.term) list ->
unit
val pp_let :
formatter ->
(Term.vsymbol * Term.term * bool) list ->
unit
val pp_annot : bool -> formatter -> Term.term -> unit
val pp_expr : formatter -> Coma_logic.expr -> unit
val pp_arg : formatter -> Coma_logic.argument -> unit
val pp_def : bool -> formatter -> Coma_logic.defn -> unit
val pp_local_defs_block : bool -> formatter -> Coma_logic.defn list -> unit
val pp_def_block : formatter -> Coma_logic.defn list -> unit
end
module PPp : sig
open Format
val pr : Ident.ident_printer
val pp_osp : formatter -> bool -> unit
val pp_sp_nl2 : formatter -> unit -> unit
val pp_var : bool -> formatter -> Ptree.ident -> unit
val pp_prew : formatter -> Ptree.ident list -> unit
val pp_param : formatter -> pparam -> unit
val pp_set : formatter -> (Ptree.ident * 'a) list -> unit
val pp_let : formatter -> (Ptree.ident * 'a * 'b * bool) list -> unit
val pp_annot : bool -> formatter -> 'a -> unit
val pp_expr : formatter -> pexpr -> unit
val pp_arg : formatter -> pargument -> unit
val pp_def : bool -> formatter -> pdefn -> unit
val pp_local_defs_block : bool -> formatter -> pdefn list -> unit
val pp_def_block : formatter -> pdefn list -> unit
end
|
