Mercurial > urweb
diff src/elaborate.sml @ 460:d34834af4512
Cookies through explify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 06 Nov 2008 10:43:48 -0500 |
| parents | f542bc3133dc |
| children | 3f1b9231a37b |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Nov 06 10:29:55 2008 -0500 +++ b/src/elaborate.sml Thu Nov 06 10:43:48 2008 -0500 @@ -1932,22 +1932,6 @@ ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) end - | L.SgiTable (x, c) => - let - val (c', k, gs) = elabCon (env, denv) c - val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) - in - checkKind env c' k (L'.KRecord (L'.KType, loc), loc); - ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs)) - end - - | L.SgiSequence x => - let - val (env, n) = E.pushENamed env x (sequenceOf ()) - in - ([(L'.SgiSequence (!basis_r, x, n), loc)], (env, denv, gs)) - end - | L.SgiClassAbs x => let val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) @@ -1968,15 +1952,6 @@ ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) end - | L.SgiCookie (x, c) => - let - val (c', k, gs) = elabCon (env, denv) c - val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc) - in - checkKind env c' k (L'.KType, loc); - ([(L'.SgiCookie (!basis_r, x, n, c'), loc)], (env, denv, gs)) - end - and elabSgn (env, denv) (sgn, loc) = case sgn of L.SgnConst sgis => @@ -2038,18 +2013,6 @@ (); (cons, vals, sgns, SS.add (strs, x))) | L'.SgiConstraint _ => (cons, vals, sgns, strs) - | L'.SgiTable (_, x, _, _) => - (if SS.member (vals, x) then - sgnError env (DuplicateVal (loc, x)) - else - (); - (cons, SS.add (vals, x), sgns, strs)) - | L'.SgiSequence (_, x, _) => - (if SS.member (vals, x) then - sgnError env (DuplicateVal (loc, x)) - else - (); - (cons, SS.add (vals, x), sgns, strs)) | L'.SgiClassAbs (x, _) => (if SS.member (cons, x) then sgnError env (DuplicateCon (loc, x)) @@ -2061,13 +2024,7 @@ sgnError env (DuplicateCon (loc, x)) else (); - (SS.add (cons, x), vals, sgns, strs)) - | L'.SgiCookie (_, x, _, _) => - (if SS.member (vals, x) then - sgnError env (DuplicateVal (loc, x)) - else - (); - (cons, SS.add (vals, x), sgns, strs))) + (SS.add (cons, x), vals, sgns, strs))) (SS.empty, SS.empty, SS.empty, SS.empty) sgis' in ((L'.SgnConst sgis', loc), gs) @@ -2199,12 +2156,6 @@ (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) | L'.SgiConstraint (c1, c2) => (L'.DConstraint (c1, c2), loc) - | L'.SgiTable (_, x, n, c) => - (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc), - (L'.EModProj (str, strs, x), loc)), loc) - | L'.SgiSequence (_, x, n) => - (L'.DVal (x, n, sequenceOf (), - (L'.EModProj (str, strs, x), loc)), loc) | L'.SgiClassAbs (x, n) => let val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) @@ -2219,9 +2170,6 @@ in (L'.DCon (x, n, k, c), loc) end - | L'.SgiCookie (_, x, n, c) => - (L'.DVal (x, n, (L'.CApp (cookieOf (), c), loc), - (L'.EModProj (str, strs, x), loc)), loc) in (d, (E.declBinds env' d, denv')) end) @@ -2274,11 +2222,11 @@ | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | L'.DExport _ => [] - | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)] - | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)] + | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] + | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] | L'.DDatabase _ => [] - | L'.DCookie (tn, x, n, c) => [(L'.SgiCookie (tn, x, n, c), loc)] + | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] fun sgiBindsD (env, denv) (sgi, _) = case sgi of @@ -2508,36 +2456,6 @@ SOME (env, denv)) else NONE - | L'.SgiTable (_, x', n1, c1) => - if x = x' then - (case unifyCons (env, denv) (L'.CApp (tableOf (), c1), loc) c2 of - [] => SOME (env, denv) - | _ => NONE) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME (env, denv)) - else - NONE - | L'.SgiSequence (_, x', n1) => - if x = x' then - (case unifyCons (env, denv) (sequenceOf ()) c2 of - [] => SOME (env, denv) - | _ => NONE) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME (env, denv)) - else - NONE - | L'.SgiCookie (_, x', n1, c1) => - if x = x' then - (case unifyCons (env, denv) (L'.CApp (cookieOf (), c1), loc) c2 of - [] => SOME (env, denv) - | _ => NONE) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME (env, denv)) - else - NONE | _ => NONE) | L'.SgiStr (x, n2, sgn2) => @@ -2600,31 +2518,6 @@ NONE | _ => NONE) - | L'.SgiTable (_, x, n2, c2) => - seek (fn sgi1All as (sgi1, _) => - case sgi1 of - L'.SgiTable (_, x', n1, c1) => - if x = x' then - (case unifyCons (env, denv) c1 c2 of - [] => SOME (env, denv) - | _ => NONE) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME (env, denv)) - else - NONE - | _ => NONE) - - | L'.SgiSequence (_, x, n2) => - seek (fn sgi1All as (sgi1, _) => - case sgi1 of - L'.SgiSequence (_, x', n1) => - if x = x' then - SOME (env, denv) - else - NONE - | _ => NONE) - | L'.SgiClassAbs (x, n2) => seek (fn sgi1All as (sgi1, _) => let @@ -2681,21 +2574,6 @@ L'.SgiClass (x', n1, c1) => found (x', n1, c1) | _ => NONE end) - - | L'.SgiCookie (_, x, n2, c2) => - seek (fn sgi1All as (sgi1, _) => - case sgi1 of - L'.SgiCookie (_, x', n1, c1) => - if x = x' then - (case unifyCons (env, denv) c1 c2 of - [] => SOME (env, denv) - | _ => NONE) - handle CUnify (c1, c2, err) => - (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME (env, denv)) - else - NONE - | _ => NONE) end in ignore (foldl folder (env, denv) sgis2) @@ -3347,26 +3225,6 @@ ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) end | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) - | L'.SgiTable (tn, x, n, c) => - let - val (vals, x) = - if SS.member (vals, x) then - (vals, "?" ^ x) - else - (SS.add (vals, x), x) - in - ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) - end - | L'.SgiSequence (tn, x, n) => - let - val (vals, x) = - if SS.member (vals, x) then - (vals, "?" ^ x) - else - (SS.add (vals, x), x) - in - ((L'.SgiSequence (tn, x, n), loc) :: sgis, cons, vals, sgns, strs) - end | L'.SgiClassAbs (x, n) => let val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) @@ -3390,16 +3248,6 @@ (SS.add (cons, x), x) in ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) - end - | L'.SgiCookie (tn, x, n, c) => - let - val (vals, x) = - if SS.member (vals, x) then - (vals, "?" ^ x) - else - (SS.add (vals, x), x) - in - ((L'.SgiCookie (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) end) ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis