Mercurial > urweb

comparison src/elaborate.sml @ 3:daa4f1d7a663

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating cons and decls
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 15:26:12 -0500
parents 64f09f7822c3
children 5c3cc348e9e6
comparison
equal deleted inserted replaced
2:64f09f7822c3 3:daa4f1d7a663
30 structure L = Laconic 30 structure L = Laconic
31 structure L' = Elab 31 structure L' = Elab
32 structure E = ElabEnv 32 structure E = ElabEnv
33 structure U = ElabUtil 33 structure U = ElabUtil
34 34
35 open Print
36 open ElabPrint
37
35 fun elabKind (k, loc) = 38 fun elabKind (k, loc) =
36 case k of 39 case k of
37 L.KType => (L'.KType, loc) 40 L.KType => (L'.KType, loc)
38 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 41 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
39 | L.KName => (L'.KName, loc) 42 | L.KName => (L'.KName, loc)
46 49
47 fun occursKind r = 50 fun occursKind r =
48 U.Kind.exists (fn L'.KUnif (_, r') => r = r' 51 U.Kind.exists (fn L'.KUnif (_, r') => r = r'
49 | _ => false) 52 | _ => false)
50 53
51 datatype unify_error = 54 datatype kunify_error =
52 KOccursCheckFailed of L'.kind * L'.kind 55 KOccursCheckFailed of L'.kind * L'.kind
53 | KIncompatible of L'.kind * L'.kind 56 | KIncompatible of L'.kind * L'.kind
54 57
55 fun unifyError err = 58 exception KUnify' of kunify_error
59
60 fun kunifyError err =
56 case err of 61 case err of
57 KOccursCheckFailed (k1, k2) => 62 KOccursCheckFailed (k1, k2) =>
58 ErrorMsg.errorAt (#2 k1) "Kind occurs check failed" 63 eprefaces "Kind occurs check failed"
64 [("Kind 1", p_kind k1),
65 ("Kind 2", p_kind k2)]
59 | KIncompatible (k1, k2) => 66 | KIncompatible (k1, k2) =>
60 ErrorMsg.errorAt (#2 k1) "Incompatible kinds" 67 eprefaces "Incompatible kinds"
61 68 [("Kind 1", p_kind k1),
62 fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) = 69 ("Kind 2", p_kind k2)]
70
71 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
63 let 72 let
64 fun err f = unifyError (f (k1All, k2All)) 73 fun err f = raise KUnify' (f (k1All, k2All))
65 in 74 in
66 case (k1, k2) of 75 case (k1, k2) of
67 (L'.KType, L'.KType) => () 76 (L'.KType, L'.KType) => ()
68 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => 77 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
69 (unifyKinds d1 d2; 78 (unifyKinds' d1 d2;
70 unifyKinds r1 r2) 79 unifyKinds' r1 r2)
71 | (L'.KName, L'.KName) => () 80 | (L'.KName, L'.KName) => ()
72 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2 81 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
73 82
74 | (L'.KError, _) => () 83 | (L'.KError, _) => ()
75 | (_, L'.KError) => () 84 | (_, L'.KError) => ()
76 85
77 | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All 86 | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All
78 | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All 87 | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All
79 88
80 | (L'.KUnif (_, r1), L'.KUnif (_, r2)) => 89 | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
81 if r1 = r2 then 90 if r1 = r2 then
82 () 91 ()
83 else 92 else
95 r := SOME k1All 104 r := SOME k1All
96 105
97 | _ => err KIncompatible 106 | _ => err KIncompatible
98 end 107 end
99 108
109 exception KUnify of L'.kind * L'.kind * kunify_error
110
111 fun unifyKinds k1 k2 =
112 unifyKinds' k1 k2
113 handle KUnify' err => raise KUnify (k1, k2, err)
114
115 datatype con_error =
116 UnboundCon of ErrorMsg.span * string
117 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
118
119 fun conError err =
120 case err of
121 UnboundCon (loc, s) =>
122 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
123 | WrongKind (c, k1, k2, kerr) =>
124 (ErrorMsg.errorAt (#2 c) "Wrong kind";
125 eprefaces' [("Have", p_kind k1),
126 ("Need", p_kind k2)];
127 kunifyError kerr)
128
129 fun checkKind c k1 k2 =
130 unifyKinds k1 k2
131 handle KUnify (k1, k2, err) =>
132 conError (WrongKind (c, k1, k2, err))
133
134 val dummy = ErrorMsg.dummySpan
135
136 val ktype = (L'.KType, dummy)
137 val kname = (L'.KName, dummy)
138
139 val cerror = (L'.CError, dummy)
140 val kerror = (L'.KError, dummy)
141
142 local
143 val count = ref 0
144 in
145
146 fun resetKunif () = count := 0
147
148 fun kunif () =
149 let
150 val n = !count
151 val s = if n <= 26 then
152 str (chr (ord #"A" + n))
153 else
154 "U" ^ Int.toString (n - 26)
155 in
156 count := n + 1;
157 (L'.KUnif (s, ref NONE), dummy)
158 end
159
160 end
161
162 fun elabCon env (c, loc) =
163 case c of
164 L.CAnnot (c, k) =>
165 let
166 val k' = elabKind k
167 val (c', ck) = elabCon env c
168 in
169 checkKind c' ck k';
170 (c', k')
171 end
172
173 | L.TFun (t1, t2) =>
174 let
175 val (t1', k1) = elabCon env t1
176 val (t2', k2) = elabCon env t2
177 in
178 checkKind t1' k1 ktype;
179 checkKind t2' k2 ktype;
180 ((L'.TFun (t1', t2'), loc), ktype)
181 end
182 | L.TCFun (e, x, k, t) =>
183 let
184 val e' = elabExplicitness e
185 val k' = elabKind k
186 val env' = E.pushCRel env x k'
187 val (t', tk) = elabCon env' t
188 in
189 checkKind t' tk ktype;
190 ((L'.TCFun (e', x, k', t'), loc), ktype)
191 end
192 | L.TRecord c =>
193 let
194 val (c', ck) = elabCon env c
195 val k = (L'.KRecord ktype, loc)
196 in
197 checkKind c' ck k;
198 ((L'.TRecord c', loc), ktype)
199 end
200
201 | L.CVar s =>
202 (case E.lookupC env s of
203 E.CNotBound =>
204 (conError (UnboundCon (loc, s));
205 (cerror, kerror))
206 | E.CRel (n, k) =>
207 ((L'.CRel n, loc), k)
208 | E.CNamed (n, k) =>
209 ((L'.CNamed n, loc), k))
210 | L.CApp (c1, c2) =>
211 let
212 val (c1', k1) = elabCon env c1
213 val (c2', k2) = elabCon env c2
214 val dom = kunif ()
215 val ran = kunif ()
216 in
217 checkKind c1' k1 (L'.KArrow (dom, ran), loc);
218 checkKind c2' k2 dom;
219 ((L'.CApp (c1', c2'), loc), ran)
220 end
221 | L.CAbs (e, x, k, t) =>
222 let
223 val e' = elabExplicitness e
224 val k' = elabKind k
225 val env' = E.pushCRel env x k'
226 val (t', tk) = elabCon env' t
227 in
228 ((L'.CAbs (e', x, k', t'), loc),
229 (L'.KArrow (k', tk), loc))
230 end
231
232 | L.CName s =>
233 ((L'.CName s, loc), kname)
234
235 | L.CRecord xcs =>
236 let
237 val k = kunif ()
238
239 val xcs' = map (fn (x, c) =>
240 let
241 val (x', xk) = elabCon env x
242 val (c', ck) = elabCon env c
243 in
244 checkKind x' xk kname;
245 checkKind c' ck k;
246 (x', c')
247 end) xcs
248 in
249 ((L'.CRecord (k, xcs'), loc), k)
250 end
251 | L.CConcat (c1, c2) =>
252 let
253 val (c1', k1) = elabCon env c1
254 val (c2', k2) = elabCon env c2
255 val ku = kunif ()
256 val k = (L'.KRecord ku, loc)
257 in
258 checkKind c1' k1 k;
259 checkKind c2' k2 k;
260 ((L'.CConcat (c1', c2'), loc), k)
261 end
262
263 fun elabDecl env (d, loc) =
264 case d of
265 L.DCon (x, ko, c) =>
266 let
267 val k' = case ko of
268 NONE => kunif ()
269 | SOME k => elabKind k
270
271 val (c', ck) = elabCon env c
272 in
273 checkKind c' ck k';
274 (E.pushCNamed env x k',
275 L'.DCon (x, k', c'))
276 end
277
100 fun elabFile _ = raise Fail "" 278 fun elabFile _ = raise Fail ""
101 279
102 end 280 end