Mercurial > urweb

comparison src/elaborate.sml @ 1570:c7d0328ba777

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix wildification for signatures with synonyms
author Adam Chlipala <adam@chlipala.net>
date Sat, 08 Oct 2011 14:16:13 -0400
parents 396e8d881205
children f6c74b4bc4e6
comparison
equal deleted inserted replaced
1569:81d007609b1a 1570:c7d0328ba777
1770 | _ => NONE 1770 | _ => NONE
1771 in 1771 in
1772 findHead e 1772 findHead e
1773 end 1773 end
1774 1774
1775 datatype needed = Needed of {Cons : (L'.kind * L'.con option) SM.map, 1775 datatype needed = Needed of {Cons : L'.kind SM.map,
1776 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, 1776 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list,
1777 Vals : SS.set, 1777 Vals : SS.set,
1778 Mods : (E.env * needed) SM.map} 1778 Mods : (E.env * needed) SM.map}
1779 1779
1780 fun ncons (Needed r) = #Cons r 1780 fun ncons (Needed r) = #Cons r
3433 | _ => NONE 3433 | _ => NONE
3434 3434
3435 fun buildNeeded env sgis = 3435 fun buildNeeded env sgis =
3436 #1 (foldl (fn ((sgi, loc), (nd, env')) => 3436 #1 (foldl (fn ((sgi, loc), (nd, env')) =>
3437 (case sgi of 3437 (case sgi of
3438 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c)) 3438 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k)
3439 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (k, NONE)) 3439 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k)
3440 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc)) 3440 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc))
3441 | L'.SgiVal (x, _, t) => 3441 | L'.SgiVal (x, _, t) =>
3442 let 3442 let
3443 fun should t = 3443 fun should t =
3444 let 3444 let
3511 3511
3512 val ds' = 3512 val ds' =
3513 case SM.listItemsi (ncons nd) of 3513 case SM.listItemsi (ncons nd) of
3514 [] => ds' 3514 [] => ds'
3515 | xs => 3515 | xs =>
3516 map (fn (x, (k, co)) => 3516 map (fn (x, k) =>
3517 let 3517 let
3518 val k = 3518 val k =
3519 case decompileKind k of 3519 case decompileKind k of
3520 NONE => (L.KWild, #2 str) 3520 NONE => (L.KWild, #2 str)
3521 | SOME k => k 3521 | SOME k => k
3522 3522
3523 val cwild = (L.CWild k, #2 str) 3523 val cwild = (L.CWild k, #2 str)
3524 val c =
3525 case co of
3526 NONE => cwild
3527 | SOME c =>
3528 case decompileCon env c of
3529 NONE => cwild
3530 | SOME c' => c'
3531 in 3524 in
3532 (L.DCon (x, NONE, c), #2 str) 3525 (L.DCon (x, NONE, cwild), #2 str)
3533 end) xs @ ds' 3526 end) xs @ ds'
3534 3527
3535 val ds = ds @ ds' 3528 val ds = ds @ ds'
3536 in 3529 in
3537 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => 3530 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) =>