Mercurial > urweb

comparison src/elaborate.sml @ 707:d8217b4cb617

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PRIMARY KEY
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 16:14:31 -0400
parents 1fb318c17546
children 0406e9cccb72
comparison
equal deleted inserted replaced
706:1fb318c17546 707:d8217b4cb617
2025 handle KUnify ue => strError env (NotType (loc, ck, ue))); 2025 handle KUnify ue => strError env (NotType (loc, ck, ue)));
2026 2026
2027 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) 2027 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
2028 end 2028 end
2029 2029
2030 | L.SgiTable (x, c, e) => 2030 | L.SgiTable (x, c, pe, ce) =>
2031 let 2031 let
2032 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) 2032 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
2033 val x' = x ^ "_hidden_constraints" 2033 val x' = x ^ "_hidden_constraints"
2034 val (env', hidden_n) = E.pushCNamed env x' cstK NONE 2034 val (env', hidden_n) = E.pushCNamed env x' cstK NONE
2035 val hidden = (L'.CNamed hidden_n, loc) 2035 val hidden = (L'.CNamed hidden_n, loc)
2036 2036
2037 val (c', ck, gs') = elabCon (env, denv) c 2037 val (c', ck, gs') = elabCon (env, denv) c
2038 val pkey = cunif (loc, cstK)
2038 val visible = cunif (loc, cstK) 2039 val visible = cunif (loc, cstK)
2039 val uniques = (L'.CConcat (visible, hidden), loc) 2040 val uniques = (L'.CConcat (visible, hidden), loc)
2040 2041
2041 val ct = tableOf () 2042 val ct = tableOf ()
2042 val ct = (L'.CApp (ct, c'), loc) 2043 val ct = (L'.CApp (ct, c'), loc)
2043 val ct = (L'.CApp (ct, uniques), loc) 2044 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
2045
2046 val (pe', pet, gs'') = elabExp (env', denv) pe
2047 val gs'' = List.mapPartial (fn Disjoint x => SOME x
2048 | _ => NONE) gs''
2049
2050 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
2051 val pst = (L'.CApp (pst, c'), loc)
2052 val pst = (L'.CApp (pst, pkey), loc)
2044 2053
2045 val (env', n) = E.pushENamed env' x ct 2054 val (env', n) = E.pushENamed env' x ct
2046 2055
2047 val (e', et, gs'') = elabExp (env, denv) e 2056 val (ce', cet, gs''') = elabExp (env', denv) ce
2048 val gs'' = List.mapPartial (fn Disjoint x => SOME x 2057 val gs''' = List.mapPartial (fn Disjoint x => SOME x
2049 | _ => NONE) gs'' 2058 | _ => NONE) gs'''
2050 2059
2051 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) 2060 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
2052 val cst = (L'.CApp (cst, c'), loc) 2061 val cst = (L'.CApp (cst, c'), loc)
2053 val cst = (L'.CApp (cst, visible), loc) 2062 val cst = (L'.CApp (cst, visible), loc)
2054 in 2063 in
2055 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); 2064 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
2056 checkCon env' e' et cst; 2065 checkCon env' pe' pet pst;
2066 checkCon env' ce' cet cst;
2057 2067
2058 ([(L'.SgiConAbs (x', hidden_n, cstK), loc), 2068 ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
2059 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs'' @ gs' @ gs)) 2069 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
2060 end 2070 end
2061 2071
2062 | L.SgiStr (x, sgn) => 2072 | L.SgiStr (x, sgn) =>
2063 let 2073 let
2064 val (sgn', gs') = elabSgn (env, denv) sgn 2074 val (sgn', gs') = elabSgn (env, denv) sgn
2358 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] 2368 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
2359 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] 2369 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
2360 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2370 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2361 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2371 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2362 | L'.DExport _ => [] 2372 | L'.DExport _ => []
2363 | L'.DTable (tn, x, n, c, _, cc) => 2373 | L'.DTable (tn, x, n, c, _, pc, _, cc) =>
2364 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), cc), loc)), loc)] 2374 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc),
2375 (L'.CConcat (pc, cc), loc)), loc)), loc)]
2365 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2376 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2366 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2377 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2367 | L'.DDatabase _ => [] 2378 | L'.DDatabase _ => []
2368 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2379 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2369 2380
3305 | _ => sgn 3316 | _ => sgn
3306 in 3317 in
3307 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) 3318 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
3308 end 3319 end
3309 3320
3310 | L.DTable (x, c, e) => 3321 | L.DTable (x, c, pe, ce) =>
3311 let 3322 let
3323 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
3324
3312 val (c', k, gs') = elabCon (env, denv) c 3325 val (c', k, gs') = elabCon (env, denv) c
3313 val uniques = cunif (loc, (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)) 3326 val pkey = cunif (loc, cstK)
3327 val uniques = cunif (loc, cstK)
3314 3328
3315 val ct = tableOf () 3329 val ct = tableOf ()
3316 val ct = (L'.CApp (ct, c'), loc) 3330 val ct = (L'.CApp (ct, c'), loc)
3317 val ct = (L'.CApp (ct, uniques), loc) 3331 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
3318 3332
3319 val (env, n) = E.pushENamed env x ct 3333 val (env, n) = E.pushENamed env x ct
3320 val (e', et, gs'') = elabExp (env, denv) e 3334 val (pe', pet, gs'') = elabExp (env, denv) pe
3335 val (ce', cet, gs''') = elabExp (env, denv) ce
3336
3337 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
3338 val pst = (L'.CApp (pst, c'), loc)
3339 val pst = (L'.CApp (pst, pkey), loc)
3321 3340
3322 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) 3341 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
3323 val cst = (L'.CApp (cst, c'), loc) 3342 val cst = (L'.CApp (cst, c'), loc)
3324 val cst = (L'.CApp (cst, uniques), loc) 3343 val cst = (L'.CApp (cst, uniques), loc)
3325 in 3344 in
3326 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 3345 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
3327 checkCon env e' et cst; 3346 checkCon env pe' pet pst;
3328 ([(L'.DTable (!basis_r, x, n, c', e', uniques), loc)], (env, denv, gs'' @ enD gs' @ gs)) 3347 checkCon env ce' cet cst;
3348 ([(L'.DTable (!basis_r, x, n, c', pe', pkey, ce', uniques), loc)],
3349 (env, denv, gs''' @ gs'' @ enD gs' @ gs))
3329 end 3350 end
3330 | L.DSequence x => 3351 | L.DSequence x =>
3331 let 3352 let
3332 val (env, n) = E.pushENamed env x (sequenceOf ()) 3353 val (env, n) = E.pushENamed env x (sequenceOf ())
3333 in 3354 in