From ea5a24773259c147e806960843d3305a3c72067b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 6 Nov 2008 10:43:48 -0500 Subject: Cookies through explify --- src/elaborate.sml | 160 ++---------------------------------------------------- 1 file changed, 4 insertions(+), 156 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index 3a966eaf..3b70c623 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1932,22 +1932,6 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = ([(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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = ([(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 @@ and elabSgn (env, denv) (sgn, loc) = (); (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 @@ and elabSgn (env, denv) (sgn, loc) = 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 @@ fun dopen (env, denv) {str, strs, sgn} = (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 @@ fun dopen (env, denv) {str, strs, sgn} = 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 @@ fun sgiOfDecl (d, loc) = | 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 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 @@ and elabStr (env, denv) (str, loc) = ((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 @@ and elabStr (env, denv) (str, loc) = (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 -- cgit v1.2.3