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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id: perror.ml,v 1.9.2.1 2004/07/16 19:30:01 herbelin Exp $ *)
open Pp
open Util
open Names
open Nameops
open Term
open Himsg
open Ptype
open Past
let is_mutable = function Ref _ | Array _ -> true | _ -> false
let is_pure = function TypePure _ -> true | _ -> false
let raise_with_loc = function
| None -> raise
| Some loc -> Stdpp.raise_with_loc loc
let unbound_variable id loc =
raise_with_loc loc
(UserError ("Perror.unbound_variable",
(hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ()))))
let unbound_reference id loc =
raise_with_loc loc
(UserError ("Perror.unbound_reference",
(hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ()))))
let clash id loc =
raise_with_loc loc
(UserError ("Perror.clash",
(hov 0 (str"Clash with previous constant" ++ spc () ++
str(string_of_id id) ++ fnl ()))))
let not_defined id =
raise
(UserError ("Perror.not_defined",
(hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++
str"is not defined" ++ fnl ()))))
let check_for_reference loc id = function
Ref _ -> ()
| _ -> Stdpp.raise_with_loc loc
(UserError ("Perror.check_for_reference",
hov 0 (pr_id id ++ spc () ++
str"is not a reference")))
let check_for_array loc id = function
Array _ -> ()
| _ -> Stdpp.raise_with_loc loc
(UserError ("Perror.check_for_array",
hov 0 (pr_id id ++ spc () ++
str"is not an array")))
let is_constant_type s = function
TypePure c ->
let id = id_of_string s in
let c' = Constrintern.global_reference id in
Reductionops.is_conv (Global.env()) Evd.empty c c'
| _ -> false
let check_for_index_type loc v =
let is_index = is_constant_type "Z" v in
if not is_index then
Stdpp.raise_with_loc loc
(UserError ("Perror.check_for_index",
hov 0 (str"This expression is an index" ++ spc () ++
str"and should have type int (Z)")))
let check_no_effect loc ef =
if not (Peffect.get_writes ef = []) then
Stdpp.raise_with_loc loc
(UserError ("Perror.check_no_effect",
hov 0 (str"A boolean should not have side effects"
)))
let should_be_boolean loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.should_be_boolean",
hov 0 (str"This expression is a test:" ++ spc () ++
str"it should have type bool")))
let test_should_be_annotated loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.test_should_be_annotated",
hov 0 (str"This test should be annotated")))
let if_branches loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.if_branches",
hov 0 (str"The two branches of an `if' expression" ++ spc () ++
str"should have the same type")))
let check_for_not_mutable loc v =
if is_mutable v then
Stdpp.raise_with_loc loc
(UserError ("Perror.check_for_not_mutable",
hov 0 (str"This expression cannot be a mutable")))
let check_for_pure_type loc v =
if not (is_pure v) then
Stdpp.raise_with_loc loc
(UserError ("Perror.check_for_pure_type",
hov 0 (str"This expression must be pure" ++ spc () ++
str"(neither a mutable nor a function)")))
let check_for_let_ref loc v =
if not (is_pure v) then
Stdpp.raise_with_loc loc
(UserError ("Perror.check_for_let_ref",
hov 0 (str"References can only be bound in pure terms")))
let informative loc s =
Stdpp.raise_with_loc loc
(UserError ("Perror.variant_informative",
hov 0 (str s ++ spc () ++ str"must be informative")))
let variant_informative loc = informative loc "Variant"
let should_be_informative loc = informative loc "This term"
let app_of_non_function loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.app_of_non_function",
hov 0 (str"This term cannot be applied" ++ spc () ++
str"(either it is not a function" ++ spc () ++
str"or it is applied to non pure arguments)")))
let partial_app loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.partial_app",
hov 0 (str"This function does not have" ++
spc () ++ str"the right number of arguments")))
let expected_type loc s =
Stdpp.raise_with_loc loc
(UserError ("Perror.expected_type",
hov 0 (str"Argument is expected to have type" ++ spc () ++ s)))
let expects_a_type id loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.expects_a_type",
hov 0 (str"The argument " ++ pr_id id ++ spc () ++
str"in this application is supposed to be a type")))
let expects_a_term id =
raise
(UserError ("Perror.expects_a_type",
hov 0 (str"The argument " ++ pr_id id ++ spc () ++
str"in this application is supposed to be a term")))
let should_be_a_variable loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.should_be_a_variable",
hov 0 (str"Argument should be a variable")))
let should_be_a_reference loc =
Stdpp.raise_with_loc loc
(UserError ("Perror.should_be_a_reference",
hov 0 (str"Argument of function should be a reference")))
|
