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
, _
) =
115 TArrow (t
', _
) => SOME t
'
116 |
TUnif (_
, ref (SOME t
')) => get_first_arg t
'
121 WrongType (_
, _
, (TBase
"string", _
), (TBase
"your_domain", _
), _
) =>
122 SOME
"Did you forget to request permission to configure this domain? See:\n\thttps://members.hcoop.net/portal/domain"
123 |
WrongType (_
, (EString dom
, _
), (TBase
"string", _
), (TBase
"domain", _
), _
) =>
124 if CharVector
.exists
Char.isUpper dom
then
125 SOME
"Uppercase letters aren't allowed in domain strings."
130 fun describe_type_error
' loc te
=
132 WrongType (place
, e
, t1
, t2
, ueo
) =>
133 (ErrorMsg
.error (SOME loc
) (place ^
" has wrong type.");
134 preface (" Expression:", p_exp e
);
135 preface ("Actual type:", p_typ t1
);
136 preface ("Needed type:", p_typ t2
);
137 Option
.app (describe_unification_error t1
) ueo
)
138 |
WrongForm (place
, form
, e
, t
, ueo
) =>
139 if form
= "action" andalso will_be_action t
then
140 (case get_first_arg t
of
141 NONE
=> ErrorMsg
.error (SOME loc
) "You probably forgot a 'with' clause here."
143 (ErrorMsg
.error (SOME loc
) ("Not enough arguments passed to configuration function. (" ^ place ^
")");
144 preface (" Expression so far:", p_exp e
);
145 preface ("Next argument type:", p_typ t
')))
147 (ErrorMsg
.error (SOME loc
) (place ^
" has a non-" ^ form ^
" type.");
148 preface ("Expression:", p_exp e
);
149 preface (" Type:", p_typ t
);
150 Option
.app (describe_unification_error t
) ueo
)
151 | UnboundVariable name
=>
152 ErrorMsg
.error (SOME loc
) ("Unbound variable " ^ name ^
".\n")
153 |
WrongPred (place
, p1
, p2
) =>
154 (ErrorMsg
.error (SOME loc
) ("Context incompatibility for " ^ place ^
".");
155 preface ("Have:", p_pred p1
);
156 preface ("Need:", p_pred p2
))
158 fun ununify (tAll
as (t
, _
)) =
160 TUnif (_
, ref (SOME t
)) => ununify t
163 fun normalize_error err
=
165 WrongType (s
, e
, t1
, t2
, ueo
) =>
166 WrongType (s
, e
, ununify t1
, ununify t2
, ueo
)
167 |
WrongForm (s1
, s2
, e
, t
, ueo
) =>
168 WrongForm (s1
, s2
, e
, ununify t
, ueo
)
169 | UnboundVariable _
=> err
172 fun describe_type_error loc te
=
174 val te
= normalize_error te
176 describe_type_error
' loc te
;
177 Option
.app (fn s
=> (print
"Hint Monster says:\n";