Mercurial > urweb

comparison src/elaborate.sml @ 147:eb16f2aadbe9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Meta-programming forms
author Adam Chlipala <adamc@hcoop.net>
date Tue, 22 Jul 2008 18:46:04 -0400
parents 80ac94b54e41
children 7420fa18d657
comparison
equal deleted inserted replaced
146:80ac94b54e41 147:eb16f2aadbe9
467 | CExplicitness (c1, c2) => 467 | CExplicitness (c1, c2) =>
468 eprefaces "Differing constructor function explicitness" 468 eprefaces "Differing constructor function explicitness"
469 [("Con 1", p_con env c1), 469 [("Con 1", p_con env c1),
470 ("Con 2", p_con env c2)] 470 ("Con 2", p_con env c2)]
471 | CKindof (k, c) => 471 | CKindof (k, c) =>
472 eprefaces "Kind unification variable blocks kindof calculation" 472 eprefaces "Unexpected kind for kindof calculation"
473 [("Kind", p_kind k), 473 [("Kind", p_kind k),
474 ("Con", p_con env c)] 474 ("Con", p_con env c)]
475 | CRecordFailure => 475 | CRecordFailure =>
476 eprefaces "Can't unify record constructors" [] 476 eprefaces "Can't unify record constructors" []
477 477
548 val hnormCon = D.hnormCon 548 val hnormCon = D.hnormCon
549 549
550 fun unifyRecordCons (env, denv) (c1, c2) = 550 fun unifyRecordCons (env, denv) (c1, c2) =
551 let 551 let
552 fun rkindof c = 552 fun rkindof c =
553 case kindof env c of 553 case hnormKind (kindof env c) of
554 (L'.KRecord k, _) => k 554 (L'.KRecord k, _) => k
555 | (L'.KError, _) => kerror 555 | (L'.KError, _) => kerror
556 | k => raise CUnify' (CKindof (k, c)) 556 | k => raise CUnify' (CKindof (k, c))
557 557
558 val k1 = rkindof c1 558 val k1 = rkindof c1
871 | L'.EModProj (n, ms, x) => 871 | L'.EModProj (n, ms, x) =>
872 let 872 let
873 val (_, sgn) = E.lookupStrNamed env n 873 val (_, sgn) = E.lookupStrNamed env n
874 val (str, sgn) = foldl (fn (m, (str, sgn)) => 874 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
875 case E.projectStr env {sgn = sgn, str = str, field = m} of 875 case E.projectStr env {sgn = sgn, str = str, field = m} of
876 NONE => raise Fail "kindof: Unknown substructure" 876 NONE => raise Fail "typeof: Unknown substructure"
877 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 877 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
878 ((L'.StrVar n, loc), sgn) ms 878 ((L'.StrVar n, loc), sgn) ms
879 in 879 in
880 case E.projectVal env {sgn = sgn, str = str, field = x} of 880 case E.projectVal env {sgn = sgn, str = str, field = x} of
881 NONE => raise Fail "typeof: Unknown val in structure" 881 NONE => raise Fail "typeof: Unknown val in structure"
963 cerror) 963 cerror)
964 | SOME t => t 964 | SOME t => t
965 in 965 in
966 ((L'.EModProj (n, ms, s), loc), t, []) 966 ((L'.EModProj (n, ms, s), loc), t, [])
967 end) 967 end)
968
969 (*| L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) =>
970 let
971 val (xml1', t1, gs1) = elabExp (env, denv) xml1
972 val (xml2', t2, gs2) = elabExp (env, denv) xml2
973
974 val kunit = (L'.KUnit, loc)
975 val k = (L'.KRecord kunit, loc)
976 val kt = (L'.KRecord (L'.KType, loc), loc)
977
978 val basis =
979 case E.lookupStr env "Basis" of
980 NONE => raise Fail "elabExp: Unbound Basis"
981 | SOME (n, _) => n
982
983 fun xml () =
984 let
985 val ns = cunif (loc, k)
986 val use = cunif (loc, kt)
987 val bind = cunif (loc, kt)
988
989 val t = (L'.CModProj (basis, [], "xml"), loc)
990 val t = (L'.CApp (t, ns), loc)
991 val t = (L'.CApp (t, use), loc)
992 val t = (L'.CApp (t, bind), loc)
993 in
994 (ns, use, bind, t)
995 end
996
997 val (ns1, use1, bind1, c1) = xml ()
998 val (ns2, use2, bind2, c2) = xml ()
999
1000 val gs3 = checkCon (env, denv) xml1' t1 c1
1001 val gs4 = checkCon (env, denv) xml2' t2 c2
1002
1003 val (ns1, gs5) = hnormCon (env, denv) ns1
1004 val (ns2, gs6) = hnormCon (env, denv) ns2
1005
1006 val cemp = (L'.CRecord (kunit, []), loc)
1007
1008 val (shared, ctx1, ctx2) =
1009 case (#1 ns1, #1 ns2) of
1010 (L'.CRecord (_, ns1), L'.CRecord (_, ns2)) =>
1011 let
1012 val ns = List.filter (fn ((nm, _), _) =>
1013 case nm of
1014 L'.CName s =>
1015 List.exists (fn ((L'.CName s', _), _) => s' = s
1016 | _ => false) ns2
1017 | _ => false) ns1
1018 in
1019 ((L'.CRecord (kunit, ns), loc), cunif (loc, k), cunif (loc, k))
1020 end
1021 | (_, L'.CRecord _) => (ns2, cemp, cemp)
1022 | _ => (ns1, cemp, cemp)
1023
1024 val ns1' = (L'.CConcat (shared, ctx1), loc)
1025 val ns2' = (L'.CConcat (shared, ctx2), loc)
1026
1027 val e = (L'.EModProj (basis, [], "join"), loc)
1028 val e = (L'.ECApp (e, shared), loc)
1029 val e = (L'.ECApp (e, ctx1), loc)
1030 val e = (L'.ECApp (e, ctx2), loc)
1031 val e = (L'.ECApp (e, use1), loc)
1032 val e = (L'.ECApp (e, use2), loc)
1033 val e = (L'.ECApp (e, bind1), loc)
1034 val e = (L'.ECApp (e, bind2), loc)
1035 val e = (L'.EApp (e, xml1'), loc)
1036 val e = (L'.EApp (e, xml2'), loc)
1037
1038 val t = (L'.CModProj (basis, [], "xml"), loc)
1039 val t = (L'.CApp (t, shared), loc)
1040 val t = (L'.CApp (t, (L'.CConcat (use1, use2), loc)), loc)
1041 val t = (L'.CApp (t, (L'.CConcat (bind1, bind2), loc)), loc)
1042
1043 fun doUnify (ns, ns') =
1044 let
1045 fun setEmpty c =
1046 let
1047 val ((c, _), gs) = hnormCon (env, denv) c
1048 in
1049 case c of
1050 L'.CUnif (_, _, _, r) =>
1051 (r := SOME cemp;
1052 gs)
1053 | L'.CConcat (_, c') => setEmpty c' @ gs
1054 | _ => gs
1055 end
1056
1057 val gs1 = unifyCons (env, denv) ns ns'
1058 val gs2 = setEmpty ns'
1059 val gs3 = unifyCons (env, denv) ns ns'
1060 in
1061 gs1 @ gs2 @ gs3
1062 end handle CUnify _ => (expError env (IncompatibleCons (ns, ns'));
1063 [])
1064
1065 val gs7 = doUnify (ns1, ns1')
1066 val gs8 = doUnify (ns2, ns2')
1067 in
1068 (e, t, (loc, env, denv, shared, ctx1)
1069 :: (loc, env, denv, shared, ctx2)
1070 :: (loc, env, denv, use1, use2)
1071 :: (loc, env, denv, bind1, bind2)
1072 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8)
1073 end*)
1074 968
1075 | L.EApp (e1, e2) => 969 | L.EApp (e1, e2) =>
1076 let 970 let
1077 val (e1', t1, gs1) = elabExp (env, denv) e1 971 val (e1', t1, gs1) = elabExp (env, denv) e1
1078 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 972 val (e1', t1, gs2) = elabHead (env, denv) e1' t1