Mercurial > urweb

comparison src/elaborate.sml @ 704:70cbdcf5989b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
UNIQUE constraints
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 12:24:31 -0400
parents fab5998b840e
children e6706a1df013
comparison
equal deleted inserted replaced
703:a5d8b470d7ca 704:70cbdcf5989b
1124 (e, t, enD gs @ gs') 1124 (e, t, enD gs @ gs')
1125 end 1125 end
1126 else 1126 else
1127 (e, t, []) 1127 (e, t, [])
1128 | t => (e, t, []) 1128 | t => (e, t, [])
1129 in 1129 in
1130 case infer of 1130 case infer of
1131 L.DontInfer => (e, t, []) 1131 L.DontInfer => (e, t, [])
1132 | _ => unravel (t, e) 1132 | _ => unravel (t, e)
1133 end 1133 end
1134 1134
1135 fun elabPat (pAll as (p, loc), (env, bound)) = 1135 fun elabPat (pAll as (p, loc), (env, bound)) =
1136 let 1136 let
1137 val perror = (L'.PWild, loc) 1137 val perror = (L'.PWild, loc)
1138 val terror = (L'.CError, loc) 1138 val terror = (L'.CError, loc)
2317 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 2317 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
2318 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2318 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
2319 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2319 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2320 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2320 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2321 | L'.DExport _ => [] 2321 | L'.DExport _ => []
2322 | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] 2322 | L'.DTable (tn, x, n, c, _) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
2323 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2323 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2324 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2324 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2325 | L'.DDatabase _ => [] 2325 | L'.DDatabase _ => []
2326 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2326 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2327 2327
3263 | _ => sgn 3263 | _ => sgn
3264 in 3264 in
3265 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) 3265 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
3266 end 3266 end
3267 3267
3268 | L.DTable (x, c) => 3268 | L.DTable (x, c, e) =>
3269 let 3269 let
3270 val (c', k, gs') = elabCon (env, denv) c 3270 val (c', k, gs') = elabCon (env, denv) c
3271 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 3271 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
3272 val (e', et, gs'') = elabExp (env, denv) e
3273
3274 val names = cunif (loc, (L'.KRecord (L'.KUnit, loc), loc))
3275 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
3276 val cst = (L'.CApp (cst, names), loc)
3277 val cst = (L'.CApp (cst, c'), loc)
3272 in 3278 in
3273 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 3279 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
3274 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) 3280 checkCon env e' et cst;
3281 ([(L'.DTable (!basis_r, x, n, c', e'), loc)], (env, denv, gs'' @ enD gs' @ gs))
3275 end 3282 end
3276 | L.DSequence x => 3283 | L.DSequence x =>
3277 let 3284 let
3278 val (env, n) = E.pushENamed env x (sequenceOf ()) 3285 val (env, n) = E.pushENamed env x (sequenceOf ())
3279 in 3286 in