1e81550cda742a87e20198e3a85092b6c1076afa
[hcoop/domtool2.git] / src / describe.sml
1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
2 * Copyright (c) 2006-2007, Adam Chlipala
3 *
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.
8 *
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.
13 *
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.
17 *)
18
19 (* Error message generation *)
20
21 structure Describe :> DESCRIBE = struct
22
23 open Ast Print
24
25 structure SM = StringMap
26
27 exception UnequalDomains
28
29 fun eqRecord f (r1, r2) =
30 (SM.appi (fn (k, v1) =>
31 case SM.find (r2, k) of
32 NONE => raise UnequalDomains
33 | SOME v2 =>
34 if f (v1, v2) then
35 ()
36 else
37 raise UnequalDomains) r1;
38 SM.appi (fn (k, v2) =>
39 case SM.find (r1, k) of
40 NONE => raise UnequalDomains
41 | SOME v1 =>
42 if f (v1, v2) then
43 ()
44 else
45 raise UnequalDomains) r2;
46 true)
47 handle UnequalDomains => false
48
49 fun eqPred ((p1, _), (p2, _)) =
50 case (p1, p2) of
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)
57
58 | _ => false
59
60 fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
61 case (t1, t2) of
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)
66
67 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
68 eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
69 andalso eqRecord eqTy (r1, r2)
70
71 | (TNested (p1, q1), TNested (p2, q2)) =>
72 eqPred (p1, p2) andalso eqTy (q1, q2)
73
74 | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
75 | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
76
77 | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
78
79 | (TError, TError) => true
80
81 | _ => false
82
83 fun describe_unification_error t ue =
84 case ue of
85 UnifyPred (p1, p2) =>
86 (print "Reason: Incompatible contexts.\n";
87 preface ("Have:", p_pred p1);
88 preface ("Need:", p_pred p2))
89 | UnifyTyp (t1, t2) =>
90 if eqTy (t, t1) then
91 ()
92 else
93 (print "Reason: Incompatible types.\n";
94 preface ("Have:", p_typ t1);
95 preface ("Need:", p_typ t2))
96 | UnifyOccurs (name, t') =>
97 if eqTy (t, t') then
98 ()
99 else
100 (print "Reason: Occurs check failed for ";
101 print name;
102 print " in:\n";
103 output (p_typ t))
104
105 fun will_be_action (t, _) =
106 case t of
107 TArrow (_, t') => will_be_action t'
108 | TAction _ => true
109 | TNested _ => true
110 | TUnif (_, ref (SOME t')) => will_be_action t'
111 | _ => false
112
113 fun get_first_arg (t, _) =
114 case t of
115 TArrow (t', _) => t'
116 | TUnif (_, ref (SOME t')) => get_first_arg t'
117 | _ => raise Fail "get_first_arg failed!"
118
119 fun hint te =
120 case te of
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."
126 else
127 NONE
128 | _ => NONE
129
130 fun describe_type_error' loc te =
131 case te of
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 (ErrorMsg.error (SOME loc) "Not enough arguments passed to configuration function.";
141 preface (" Expression so far:", p_exp e);
142 preface ("Next argument type:", p_typ (get_first_arg t)))
143 else
144 (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
145 preface ("Expression:", p_exp e);
146 preface (" Type:", p_typ t);
147 Option.app (describe_unification_error t) ueo)
148 | UnboundVariable name =>
149 ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
150 | WrongPred (place, p1, p2) =>
151 (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
152 preface ("Have:", p_pred p1);
153 preface ("Need:", p_pred p2))
154
155 fun ununify (tAll as (t, _)) =
156 case t of
157 TUnif (_, ref (SOME t)) => ununify t
158 | _ => tAll
159
160 fun normalize_error err =
161 case err of
162 WrongType (s, e, t1, t2, ueo) =>
163 WrongType (s, e, ununify t1, ununify t2, ueo)
164 | WrongForm (s1, s2, e, t, ueo) =>
165 WrongForm (s1, s2, e, ununify t, ueo)
166 | UnboundVariable _ => err
167 | WrongPred _ => err
168
169 fun describe_type_error loc te =
170 let
171 val te = normalize_error te
172 in
173 describe_type_error' loc te;
174 Option.app (fn s => (print "Hint Monster says:\n";
175 print s;
176 print "\n"))
177 (hint te)
178 end
179
180 end