1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006-2007, Adam Chlipala
4 * This program is free software
; you can redistribute it
and/or
5 * modify it under the terms
of the GNU General Public License
6 * as published by the Free Software Foundation
; either version
2
7 * of the License
, or (at your option
) any later version
.
9 * This program is distributed
in the hope that it will be useful
,
10 * but WITHOUT ANY WARRANTY
; without even the implied warranty
of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE
. See the
12 * GNU General Public License for more details
.
14 * You should have received a copy
of the GNU General Public License
15 * along
with this program
; if not
, write to the Free Software
16 * Foundation
, Inc
., 51 Franklin Street
, Fifth Floor
, Boston
, MA
02110-1301, USA
.
19 (* Error message generation
*)
21 structure Describe
:> DESCRIBE
= struct
25 structure SM
= StringMap
27 exception UnequalDomains
29 fun eqRecord
f (r1
, r2
) =
30 (SM
.appi (fn (k
, v1
) =>
31 case SM
.find (r2
, k
) of
32 NONE
=> raise UnequalDomains
37 raise UnequalDomains
) r1
;
38 SM
.appi (fn (k
, v2
) =>
39 case SM
.find (r1
, k
) of
40 NONE
=> raise UnequalDomains
45 raise UnequalDomains
) r2
;
47 handle UnequalDomains
=> false
49 fun eqPred ((p1
, _
), (p2
, _
)) =
51 (CRoot
, CRoot
) => true
52 |
(CConst s1
, CConst s2
) => s1
= s2
53 |
(CPrefix p1
, CPrefix p2
) => eqPred (p1
, p2
)
54 |
(CNot p1
, CNot p2
) => eqPred (p1
, p2
)
55 |
(CAnd (p1
, q1
), CAnd (p2
, q2
)) =>
56 eqPred (p1
, p2
) andalso eqPred (q1
, q2
)
60 fun eqTy (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
62 (TBase s1
, TBase s2
) => s1
= s2
63 |
(TList t1
, TList t2
) => eqTy (t1
, t2
)
64 |
(TArrow (d1
, r1
), TArrow (d2
, r2
)) =>
65 eqTy (d1
, d2
) andalso eqTy (r1
, r2
)
67 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
68 eqPred (p1
, p2
) andalso eqRecord
eqTy (d1
, d2
)
69 andalso eqRecord
eqTy (r1
, r2
)
71 |
(TNested (p1
, q1
), TNested (p2
, q2
)) =>
72 eqPred (p1
, p2
) andalso eqTy (q1
, q2
)
74 |
(TUnif (_
, ref (SOME t1
)), _
) => eqTy (t1
, t2All
)
75 |
(_
, TUnif (_
, ref (SOME t2
))) => eqTy (t1All
, t2
)
77 |
(TUnif (_
, r1
), TUnif (_
, r2
)) => r1
= r2
79 |
(TError
, TError
) => true
83 fun describe_unification_error t ue
=
86 (print
"Reason: Incompatible contexts.\n";
87 preface ("Have:", p_pred p1
);
88 preface ("Need:", p_pred p2
))
89 |
UnifyTyp (t1
, t2
) =>
93 (print
"Reason: Incompatible types.\n";
94 preface ("Have:", p_typ t1
);
95 preface ("Need:", p_typ t2
))
96 |
UnifyOccurs (name
, t
') =>
100 (print
"Reason: Occurs check failed for ";
105 fun will_be_action (t
, _
) =
107 TArrow (_
, t
') => will_be_action t
'
110 |
TUnif (_
, ref (SOME t
')) => will_be_action t
'
113 fun get_first_arg (t
, _
) =
116 |
TUnif (_
, ref (SOME t
')) => get_first_arg t
'
117 | _
=> raise Fail
"get_first_arg failed!"
119 fun describe_type_error loc te
=
121 WrongType (place
, e
, t1
, t2
, ueo
) =>
122 (ErrorMsg
.error (SOME loc
) (place ^
" has wrong type.");
123 preface (" Expression:", p_exp e
);
124 preface ("Actual type:", p_typ t1
);
125 preface ("Needed type:", p_typ t2
);
126 Option
.app (describe_unification_error t1
) ueo
)
127 |
WrongForm (place
, form
, e
, t
, ueo
) =>
128 if form
= "action" andalso will_be_action t
then
129 (ErrorMsg
.error (SOME loc
) "Not enough arguments passed to configuration function.";
130 preface (" Expression so far:", p_exp e
);
131 preface ("Next argument type:", p_typ (get_first_arg t
)))
133 (ErrorMsg
.error (SOME loc
) (place ^
" has a non-" ^ form ^
" type.");
134 preface ("Expression:", p_exp e
);
135 preface (" Type:", p_typ t
);
136 Option
.app (describe_unification_error t
) ueo
)
137 | UnboundVariable name
=>
138 ErrorMsg
.error (SOME loc
) ("Unbound variable " ^ name ^
".\n")
139 |
WrongPred (place
, p1
, p2
) =>
140 (ErrorMsg
.error (SOME loc
) ("Context incompatibility for " ^ place ^
".");
141 preface ("Have:", p_pred p1
);
142 preface ("Need:", p_pred p2
))