Mercurial > urweb

comparison src/elaborate.sml @ 706:1fb318c17546

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Enhance table sig item support and get demo compiling again
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 15:04:07 -0400
parents e6706a1df013
children d8217b4cb617
comparison
equal deleted inserted replaced
705:e6706a1df013 706:1fb318c17546
869 869
870 and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) = 870 and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) =
871 let 871 let
872 fun err f = raise CUnify' (f (c1All, c2All)) 872 fun err f = raise CUnify' (f (c1All, c2All))
873 873
874 fun isRecord () = unifyRecordCons env (c1All, c2All) 874 fun projSpecial1 (c1, n1, onFail) =
875 in
876 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
877 ("c2All", p_con env c2All)];*)
878
879 case (c1, c2) of
880 (L'.CError, _) => ()
881 | (_, L'.CError) => ()
882
883 | (L'.CProj (c1, n1), _) =>
884 let 875 let
885 fun trySnd () = 876 fun trySnd () =
886 case #1 (hnormCon env c2All) of 877 case #1 (hnormCon env c2All) of
887 L'.CProj (c2, n2) => 878 L'.CProj (c2, n2) =>
888 let 879 let
889 fun tryNormal () = 880 fun tryNormal () =
890 if n1 = n2 then 881 if n1 = n2 then
891 unifyCons' env c1 c2 882 unifyCons' env c1 c2
892 else 883 else
893 err CIncompatible 884 onFail ()
894 in 885 in
895 case #1 (hnormCon env c2) of 886 case #1 (hnormCon env c2) of
896 L'.CUnif (_, k, _, r) => 887 L'.CUnif (_, k, _, r) =>
897 (case #1 (hnormKind k) of 888 (case #1 (hnormKind k) of
898 L'.KTuple ks => 889 L'.KTuple ks =>
904 unifyCons' env c1All (List.nth (us, n2 - 1)) 895 unifyCons' env c1All (List.nth (us, n2 - 1))
905 end 896 end
906 | _ => tryNormal ()) 897 | _ => tryNormal ())
907 | _ => tryNormal () 898 | _ => tryNormal ()
908 end 899 end
909 | _ => err CIncompatible 900 | _ => onFail ()
910 in 901 in
911 case #1 (hnormCon env c1) of 902 case #1 (hnormCon env c1) of
912 L'.CUnif (_, k, _, r) => 903 L'.CUnif (_, k, _, r) =>
913 (case #1 (hnormKind k) of 904 (case #1 (hnormKind k) of
914 L'.KTuple ks => 905 L'.KTuple ks =>
921 end 912 end
922 | _ => trySnd ()) 913 | _ => trySnd ())
923 | _ => trySnd () 914 | _ => trySnd ()
924 end 915 end
925 916
926 | (_, L'.CProj (c2, n2)) => 917 fun projSpecial2 (c2, n2, onFail) =
927 (case #1 (hnormCon env c2) of 918 case #1 (hnormCon env c2) of
928 L'.CUnif (_, k, _, r) => 919 L'.CUnif (_, k, _, r) =>
929 (case #1 (hnormKind k) of 920 (case #1 (hnormKind k) of
930 L'.KTuple ks => 921 L'.KTuple ks =>
931 let 922 let
932 val loc = #2 c2 923 val loc = #2 c2
933 val us = map (fn k => cunif (loc, k)) ks 924 val us = map (fn k => cunif (loc, k)) ks
934 in 925 in
935 r := SOME (L'.CTuple us, loc); 926 r := SOME (L'.CTuple us, loc);
936 unifyCons' env c1All (List.nth (us, n2 - 1)) 927 unifyCons' env c1All (List.nth (us, n2 - 1))
937 end 928 end
938 | _ => err CIncompatible) 929 | _ => onFail ())
939 | _ => err CIncompatible) 930 | _ => onFail ()
931
932 fun isRecord' () = unifyRecordCons env (c1All, c2All)
933
934 fun isRecord () =
935 case (c1, c2) of
936 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
937 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
938 | _ => isRecord' ()
939 in
940 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
941 ("c2All", p_con env c2All)];*)
942
943 case (c1, c2) of
944 (L'.CError, _) => ()
945 | (_, L'.CError) => ()
940 946
941 | (L'.CRecord _, _) => isRecord () 947 | (L'.CRecord _, _) => isRecord ()
942 | (_, L'.CRecord _) => isRecord () 948 | (_, L'.CRecord _) => isRecord ()
943 | (L'.CConcat _, _) => isRecord () 949 | (L'.CConcat _, _) => isRecord ()
944 | (_, L'.CConcat _) => isRecord () 950 | (_, L'.CConcat _) => isRecord ()
1017 err CIncompatible 1023 err CIncompatible
1018 1024
1019 | (L'.CTuple cs1, L'.CTuple cs2) => 1025 | (L'.CTuple cs1, L'.CTuple cs2) =>
1020 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) 1026 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
1021 handle ListPair.UnequalLengths => err CIncompatible) 1027 handle ListPair.UnequalLengths => err CIncompatible)
1028
1029 | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
1030 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
1022 1031
1023 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => 1032 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
1024 (unifyKinds env dom1 dom2; 1033 (unifyKinds env dom1 dom2;
1025 unifyKinds env ran1 ran2) 1034 unifyKinds env ran1 ran2)
1026 1035
2011 2020
2012 val (env', n) = E.pushENamed env x c' 2021 val (env', n) = E.pushENamed env x c'
2013 val c' = normClassConstraint env c' 2022 val c' = normClassConstraint env c'
2014 in 2023 in
2015 (unifyKinds env ck ktype 2024 (unifyKinds env ck ktype
2016 handle KUnify ue => strError env (NotType (ck, ue))); 2025 handle KUnify ue => strError env (NotType (loc, ck, ue)));
2017 2026
2018 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) 2027 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
2028 end
2029
2030 | L.SgiTable (x, c, e) =>
2031 let
2032 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
2033 val x' = x ^ "_hidden_constraints"
2034 val (env', hidden_n) = E.pushCNamed env x' cstK NONE
2035 val hidden = (L'.CNamed hidden_n, loc)
2036
2037 val (c', ck, gs') = elabCon (env, denv) c
2038 val visible = cunif (loc, cstK)
2039 val uniques = (L'.CConcat (visible, hidden), loc)
2040
2041 val ct = tableOf ()
2042 val ct = (L'.CApp (ct, c'), loc)
2043 val ct = (L'.CApp (ct, uniques), loc)
2044
2045 val (env', n) = E.pushENamed env' x ct
2046
2047 val (e', et, gs'') = elabExp (env, denv) e
2048 val gs'' = List.mapPartial (fn Disjoint x => SOME x
2049 | _ => NONE) gs''
2050
2051 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
2052 val cst = (L'.CApp (cst, c'), loc)
2053 val cst = (L'.CApp (cst, visible), loc)
2054 in
2055 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
2056 checkCon env' e' et cst;
2057
2058 ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
2059 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs'' @ gs' @ gs))
2019 end 2060 end
2020 2061
2021 | L.SgiStr (x, sgn) => 2062 | L.SgiStr (x, sgn) =>
2022 let 2063 let
2023 val (sgn', gs') = elabSgn (env, denv) sgn 2064 val (sgn', gs') = elabSgn (env, denv) sgn
2211 (sgnerror, [])) 2252 (sgnerror, []))
2212 | SOME _ => ((L'.SgnProj (n, ms, x), loc), []) 2253 | SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
2213 end) 2254 end)
2214 2255
2215 2256
2216 fun selfify env {str, strs, sgn} = 2257 and selfify env {str, strs, sgn} =
2217 case #1 (hnormSgn env sgn) of 2258 case #1 (hnormSgn env sgn) of
2218 L'.SgnError => sgn 2259 L'.SgnError => sgn
2219 | L'.SgnVar _ => sgn 2260 | L'.SgnVar _ => sgn
2220 2261
2221 | L'.SgnConst sgis => 2262 | L'.SgnConst sgis =>
2236 sgn = #2 (E.lookupStrNamed env m), 2277 sgn = #2 (E.lookupStrNamed env m),
2237 field = x} of 2278 field = x} of
2238 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE" 2279 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
2239 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn} 2280 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
2240 2281
2241 fun selfifyAt env {str, sgn} = 2282 and selfifyAt env {str, sgn} =
2242 let 2283 let
2243 fun self (str, _) = 2284 fun self (str, _) =
2244 case str of 2285 case str of
2245 L'.StrVar x => SOME (x, []) 2286 L'.StrVar x => SOME (x, [])
2246 | L'.StrProj (str, x) => 2287 | L'.StrProj (str, x) =>
2252 case self str of 2293 case self str of
2253 NONE => sgn 2294 NONE => sgn
2254 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} 2295 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
2255 end 2296 end
2256 2297
2257 fun dopen env {str, strs, sgn} = 2298 and dopen env {str, strs, sgn} =
2258 let 2299 let
2259 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) 2300 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
2260 (L'.StrVar str, #2 sgn) strs 2301 (L'.StrVar str, #2 sgn) strs
2261 in 2302 in
2262 case #1 (hnormSgn env sgn) of 2303 case #1 (hnormSgn env sgn) of
2305 env sgis 2346 env sgis
2306 | _ => (strError env (UnOpenable sgn); 2347 | _ => (strError env (UnOpenable sgn);
2307 ([], env)) 2348 ([], env))
2308 end 2349 end
2309 2350
2310 fun sgiOfDecl (d, loc) = 2351 and sgiOfDecl (d, loc) =
2311 case d of 2352 case d of
2312 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] 2353 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
2313 | L'.DDatatype x => [(L'.SgiDatatype x, loc)] 2354 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
2314 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] 2355 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
2315 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] 2356 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
2324 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2365 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2325 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] 2366 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2326 | L'.DDatabase _ => [] 2367 | L'.DDatabase _ => []
2327 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2368 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2328 2369
2329 fun subSgn env sgn1 (sgn2 as (_, loc2)) = 2370 and subSgn env sgn1 (sgn2 as (_, loc2)) =
2330 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), 2371 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
2331 ("sgn2", p_sgn env sgn2)];*) 2372 ("sgn2", p_sgn env sgn2)];*)
2332 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of 2373 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
2333 (L'.SgnError, _) => () 2374 (L'.SgnError, _) => ()
2334 | (_, L'.SgnError) => () 2375 | (_, L'.SgnError) => ()
2692 end 2733 end
2693 2734
2694 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) 2735 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
2695 2736
2696 2737
2697 fun positive self = 2738 and positive self =
2698 let 2739 let
2699 open L 2740 open L
2700 2741
2701 fun none (c, _) = 2742 fun none (c, _) =
2702 case c of 2743 case c of
2758 | CWild _ => false 2799 | CWild _ => false
2759 in 2800 in
2760 pos 2801 pos
2761 end 2802 end
2762 2803
2763 fun wildifyStr env (str, sgn) = 2804 and wildifyStr env (str, sgn) =
2764 case #1 (hnormSgn env sgn) of 2805 case #1 (hnormSgn env sgn) of
2765 L'.SgnConst sgis => 2806 L'.SgnConst sgis =>
2766 (case #1 str of 2807 (case #1 str of
2767 L.StrConst ds => 2808 L.StrConst ds =>
2768 let 2809 let
2920 (L.StrConst (ds @ ds'), #2 str) 2961 (L.StrConst (ds @ ds'), #2 str)
2921 end 2962 end
2922 | _ => str) 2963 | _ => str)
2923 | _ => str 2964 | _ => str
2924 2965
2925 fun elabDecl (dAll as (d, loc), (env, denv, gs)) = 2966 and elabDecl (dAll as (d, loc), (env, denv, gs)) =
2926 let 2967 let
2927 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2968 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2928 (*val befor = Time.now ()*) 2969 (*val befor = Time.now ()*)
2929 2970
2930 val r = 2971 val r =