Mercurial > urweb
changeset 1275:74150edf1134
Undo fancy wildification; instead, client code should include extra wildcard con declarations
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 03 Jun 2010 14:44:08 -0400 |
parents | 38eb0d0f39b9 |
children | 5b5c0b552f59 |
files | src/elaborate.sml |
diffstat | 1 files changed, 20 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jun 03 13:35:26 2010 -0400 +++ b/src/elaborate.sml Thu Jun 03 14:44:08 2010 -0400 @@ -1655,7 +1655,7 @@ findHead e end -datatype needed = Needed of {Cons : (string option * L'.kind * L'.con option) SM.map, +datatype needed = Needed of {Cons : (L'.kind * L'.con option) SM.map, Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, Vals : SS.set, Mods : (E.env * needed) SM.map} @@ -3274,10 +3274,10 @@ | _ => NONE fun buildNeeded env sgis = - #1 (foldl (fn ((sgi, loc), (nd, env', lastCon)) => + #1 (foldl (fn ((sgi, loc), (nd, env')) => (case sgi of - L'.SgiCon (x, _, k, c) => naddCon (nd, x, (lastCon, k, SOME c)) - | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (lastCon, k, NONE)) + L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c)) + | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (k, NONE)) | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc)) | L'.SgiVal (x, _, t) => let @@ -3296,11 +3296,8 @@ L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) | _ => nd) | _ => nd, - E.sgiBinds env' (sgi, loc), - case cname sgi of - NONE => lastCon - | v => v)) - (nempty, env, NONE) sgis) + E.sgiBinds env' (sgi, loc))) + (nempty, env) sgis) val nd = buildNeeded env sgis @@ -3339,20 +3336,17 @@ ds'' @ ds' end - val ds = ds @ ds' - - val ds = + val ds' = case SM.listItemsi (ncons nd) of - [] => ds + [] => ds' | xs => - let - fun findPlace ((x, (lastCon, k, co)), ds') = + map (fn (x, (k, co)) => let val k = case decompileKind k of NONE => (L.KWild, #2 str) | SOME k => k - + val cwild = (L.CWild k, #2 str) val c = case co of @@ -3361,28 +3355,11 @@ case decompileCon env c of NONE => cwild | SOME c' => c' - - val d = (L.DCon (x, NONE, c), #2 str) in - case lastCon of - NONE => d :: ds' - | _ => - let - fun seek (ds'', passed) = - case ds'' of - [] => d :: ds' - | d1 :: ds'' => - if dname d1 = lastCon then - List.revAppend (passed, d1 :: d :: ds'') - else - seek (ds'', d1 :: passed) - in - seek (ds', []) - end - end - in - foldl findPlace ds xs - end + (L.DCon (x, NONE, c), #2 str) + end) xs @ ds' + + val ds = ds @ ds' in map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => (case SM.find (nmods nd, x) of @@ -4039,7 +4016,12 @@ val str2 = case sgn1 of (L'.SgnFun (_, _, dom, _), _) => - wildifyStr env (str2, dom) + let + val s = wildifyStr env (str2, dom) + in + (*Print.preface ("Wild", SourcePrint.p_str s);*) + s + end | _ => str2 val (str2', sgn2, gs2) = elabStr (env, denv) str2 in