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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* Brian Campbell *)
(* Thomas Bauereiss *)
(* Anthony Fox *)
(* Jon French *)
(* Dominic Mulligan *)
(* Stephen Kell *)
(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
open Util
open Ast
open Ast_defs
open Ast_util
open Type_check
type suggestion =
| Suggest_add_constraint of n_constraint
| Suggest_none
let rec analyze_unresolved_quant locals ncs = function
| QI_aux (QI_constraint nc, _) ->
let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in
if gen_kids = [] then
Suggest_add_constraint nc
else
(* If there are generated kind-identifiers in the constraint,
we don't want to make a suggestion based on them, so try to
look for generated kid free nexps in the set of constraints
that are equal to the generated identifier. This often
occurs due to how the type-checker introduces new type
variables. *)
let is_subst v = function
| NC_aux (NC_equal (Nexp_aux (Nexp_var v', _), nexp), _)
when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) ->
[(v, nexp)]
| NC_aux (NC_equal (nexp, Nexp_aux (Nexp_var v', _)), _)
when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) ->
[(v, nexp)]
| _ -> []
in
let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_subst v nc) ncs)) gen_kids) in
let nc = List.fold_left (fun nc (v, nexp) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
Suggest_add_constraint nc
else
(* If we have a really anonymous type-variable, try to find a
regular variable that corresponds to it. *)
let is_linked v = function
| (id, (Immutable, (Typ_aux (Typ_app (ty_id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 ->
[(v, nid id, typ)]
| (id, (mut, typ)) ->
[]
in
let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_linked v nc) (Bindings.bindings locals))) gen_kids) in
let nc = List.fold_left (fun nc (v, nexp, _) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
Suggest_none
else
Suggest_none
| QI_aux (QI_id _, _) | QI_aux (QI_constant _, _) ->
Suggest_none
let message_of_type_error =
let open Error_format in
let rec msg = function
| Err_because (err, l', err') ->
Seq [msg err;
Line "This error was caused by:";
Location (l', msg err')]
| Err_other str -> Line str
| Err_no_overloading (id, errs) ->
Seq [Line ("No overloading for " ^ string_of_id id ^ ", tried:");
List (List.map (fun (id, err) -> string_of_id id, msg err) errs)]
| Err_unresolved_quants (id, quants, locals, ncs) ->
Seq [Line ("Could not resolve quantifiers for " ^ string_of_id id);
Line (bullet ^ " " ^ Util.string_of_list ("\n" ^ bullet ^ " ") string_of_quant_item quants)]
| Err_lexp_bounds (check, locals, ncs) ->
Line ("Bounds check failed for l-expression: " ^ string_of_n_constraint check)
| Err_subtype (typ1, typ2, _, vars) ->
let vars = KBindings.bindings vars in
let vars = List.filter (fun (v, _) -> KidSet.mem v (KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2))) vars in
With ((fun ppf -> { ppf with loc_color = Util.yellow }),
Seq (Line (string_of_typ typ1 ^ " is not a subtype of " ^ string_of_typ typ2)
:: List.map (fun (kid, l) -> Location (l, Line (string_of_kid kid ^ " bound here"))) vars))
| Err_no_num_ident id ->
Line ("No num identifier " ^ string_of_id id)
| Err_no_casts (exp, typ_from, typ_to, trigger, reasons) ->
let coercion =
Line ("Tried performing type coercion from " ^ string_of_typ typ_from
^ " to " ^ string_of_typ typ_to
^ " on " ^ string_of_exp exp)
in
Seq ([coercion; Line "Coercion failed because:"; msg trigger]
@ if not (reasons = []) then
Line "Possible reasons:" :: List.map msg reasons
else
[])
in
msg
let rec string_of_type_error err =
let open Error_format in
let b = Buffer.create 20 in
format_message (message_of_type_error err) (buffer_formatter b);
Buffer.contents b
let rec collapse_errors = function
| (Err_no_overloading (_, errs) as no_collapse) ->
let errs = List.map (fun (_, err) -> collapse_errors err) errs in
let interesting = function
| Err_other _ -> false
| Err_no_casts _ -> false
| _ -> true
in
begin match List.filter interesting errs with
| err :: errs ->
let fold_equal msg err =
match msg, err with
| Some msg, Err_no_overloading _ -> Some msg
| Some msg, Err_no_casts _ -> Some msg
| Some msg, err when msg = string_of_type_error err -> Some msg
| _, _ -> None
in
begin match List.fold_left fold_equal (Some (string_of_type_error err)) errs with
| Some _ -> err
| None -> no_collapse
end
| [] -> no_collapse
end
| Err_because (err1, l, err2) as no_collapse ->
let err1 = collapse_errors err1 in
let err2 = collapse_errors err2 in
if string_of_type_error err1 = string_of_type_error err2 then
err1
else
Err_because (err1, l, err2)
| err -> err
let check_defs : 'a. Env.t -> 'a def list -> tannot def list * Env.t =
fun env defs ->
try Type_check.check_defs env defs with
| Type_error (env, l, err) ->
raise (Reporting.err_typ l (string_of_type_error err))
let check : 'a. Env.t -> 'a ast -> tannot ast * Env.t =
fun env defs ->
try Type_check.check env defs with
| Type_error (env, l, err) ->
Interactive.env := env;
raise (Reporting.err_typ l (string_of_type_error err))
|
