Mercurial > urweb
diff src/elaborate.sml @ 338:e976b187d73a
SQL sequences
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 14 Sep 2008 11:02:18 -0400 |
parents | 9601c717d2f3 |
children | 075b36dbb1a4 |
line wrap: on
line diff
--- a/src/elaborate.sml Sat Sep 13 20:15:30 2008 -0400 +++ b/src/elaborate.sml Sun Sep 14 11:02:18 2008 -0400 @@ -1648,6 +1648,7 @@ val hnormSgn = E.hnormSgn fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) +fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) fun elabSgn_item ((sgi, loc), (env, denv, gs)) = case sgi of @@ -1828,6 +1829,13 @@ ([(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) @@ -1915,6 +1923,12 @@ 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,6 +2075,9 @@ | 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) @@ -2128,6 +2145,7 @@ | 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'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] | L'.DDatabase _ => [] @@ -2355,6 +2373,16 @@ 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 | _ => NONE) | L'.SgiStr (x, n2, sgn2) => @@ -2432,6 +2460,16 @@ 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 @@ -3024,6 +3062,12 @@ checkKind env c' k (L'.KRecord (L'.KType, loc), loc); ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) end + | L.DSequence x => + let + val (env, n) = E.pushENamed env x (sequenceOf ()) + in + ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) + end | L.DClass (x, c) => let @@ -3147,6 +3191,16 @@ 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)