Mercurial > urweb

comparison src/elaborate.sml @ 18:9a578171de9e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unification wildcards
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 14:25:27 -0400
parents 9bd8669d53c2
children 4ab19c19665f
comparison
equal deleted inserted replaced
17:9bd8669d53c2 18:9a578171de9e
34 structure U = ElabUtil 34 structure U = ElabUtil
35 35
36 open Print 36 open Print
37 open ElabPrint 37 open ElabPrint
38 38
39 fun elabKind (k, loc) =
40 case k of
41 L.KType => (L'.KType, loc)
42 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
43 | L.KName => (L'.KName, loc)
44 | L.KRecord k => (L'.KRecord (elabKind k), loc)
45
46 fun elabExplicitness e = 39 fun elabExplicitness e =
47 case e of 40 case e of
48 L.Explicit => L'.Explicit 41 L.Explicit => L'.Explicit
49 | L.Implicit => L'.Implicit 42 | L.Implicit => L'.Implicit
50 43
181 (L'.CUnif (k, s, ref NONE), dummy) 174 (L'.CUnif (k, s, ref NONE), dummy)
182 end 175 end
183 176
184 end 177 end
185 178
179 fun elabKind (k, loc) =
180 case k of
181 L.KType => (L'.KType, loc)
182 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
183 | L.KName => (L'.KName, loc)
184 | L.KRecord k => (L'.KRecord (elabKind k), loc)
185 | L.KWild => kunif ()
186
186 fun elabCon env (c, loc) = 187 fun elabCon env (c, loc) =
187 case c of 188 case c of
188 L.CAnnot (c, k) => 189 L.CAnnot (c, k) =>
189 let 190 let
190 val k' = elabKind k 191 val k' = elabKind k
279 val k = (L'.KRecord ku, loc) 280 val k = (L'.KRecord ku, loc)
280 in 281 in
281 checkKind env c1' k1 k; 282 checkKind env c1' k1 k;
282 checkKind env c2' k2 k; 283 checkKind env c2' k2 k;
283 ((L'.CConcat (c1', c2'), loc), k) 284 ((L'.CConcat (c1', c2'), loc), k)
285 end
286
287 | L.CWild k =>
288 let
289 val k' = elabKind k
290 in
291 (cunif k', k')
284 end 292 end
285 293
286 fun kunifsRemain k = 294 fun kunifsRemain k =
287 case k of 295 case k of
288 L'.KUnif (_, ref NONE) => true 296 L'.KUnif (_, ref NONE) => true