Mercurial > urweb

comparison src/elaborate.sml @ 139:adfa2c7a75da

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Form binding parameters threaded through
author Adam Chlipala <adamc@hcoop.net>
date Sun, 20 Jul 2008 10:11:16 -0400
parents e3041657d653
children f214c535d253
comparison
equal deleted inserted replaced
138:d6d78055f001 139:adfa2c7a75da
968 val (xml1', t1, gs1) = elabExp (env, denv) xml1 968 val (xml1', t1, gs1) = elabExp (env, denv) xml1
969 val (xml2', t2, gs2) = elabExp (env, denv) xml2 969 val (xml2', t2, gs2) = elabExp (env, denv) xml2
970 970
971 val kunit = (L'.KUnit, loc) 971 val kunit = (L'.KUnit, loc)
972 val k = (L'.KRecord kunit, loc) 972 val k = (L'.KRecord kunit, loc)
973 val kt = (L'.KRecord (L'.KType, loc), loc)
973 974
974 val basis = 975 val basis =
975 case E.lookupStr env "Basis" of 976 case E.lookupStr env "Basis" of
976 NONE => raise Fail "elabExp: Unbound Basis" 977 NONE => raise Fail "elabExp: Unbound Basis"
977 | SOME (n, _) => n 978 | SOME (n, _) => n
978 979
979 fun xml () = 980 fun xml () =
980 let 981 let
981 val ns = cunif (loc, k) 982 val ns = cunif (loc, k)
983 val use = cunif (loc, kt)
984 val bind = cunif (loc, kt)
985
986 val t = (L'.CModProj (basis, [], "xml"), loc)
987 val t = (L'.CApp (t, ns), loc)
988 val t = (L'.CApp (t, use), loc)
989 val t = (L'.CApp (t, bind), loc)
982 in 990 in
983 (ns, (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), ns), loc)) 991 (ns, use, bind, t)
984 end 992 end
985 993
986 val (ns1, c1) = xml () 994 val (ns1, use1, bind1, c1) = xml ()
987 val (ns2, c2) = xml () 995 val (ns2, use2, bind2, c2) = xml ()
988 996
989 val gs3 = checkCon (env, denv) xml1' t1 c1 997 val gs3 = checkCon (env, denv) xml1' t1 c1
990 val gs4 = checkCon (env, denv) xml2' t2 c2 998 val gs4 = checkCon (env, denv) xml2' t2 c2
991 999
992 val (ns1, gs5) = hnormCon (env, denv) ns1 1000 val (ns1, gs5) = hnormCon (env, denv) ns1
1015 1023
1016 val e = (L'.EModProj (basis, [], "join"), loc) 1024 val e = (L'.EModProj (basis, [], "join"), loc)
1017 val e = (L'.ECApp (e, shared), loc) 1025 val e = (L'.ECApp (e, shared), loc)
1018 val e = (L'.ECApp (e, ctx1), loc) 1026 val e = (L'.ECApp (e, ctx1), loc)
1019 val e = (L'.ECApp (e, ctx2), loc) 1027 val e = (L'.ECApp (e, ctx2), loc)
1028 val e = (L'.ECApp (e, use1), loc)
1029 val e = (L'.ECApp (e, use2), loc)
1030 val e = (L'.ECApp (e, bind1), loc)
1031 val e = (L'.ECApp (e, bind2), loc)
1020 val e = (L'.EApp (e, xml1'), loc) 1032 val e = (L'.EApp (e, xml1'), loc)
1021 val e = (L'.EApp (e, xml2'), loc) 1033 val e = (L'.EApp (e, xml2'), loc)
1022 1034
1023 val t = (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), shared), loc) 1035 val t = (L'.CModProj (basis, [], "xml"), loc)
1036 val t = (L'.CApp (t, shared), loc)
1037 val t = (L'.CApp (t, (L'.CConcat (use1, use2), loc)), loc)
1038 val t = (L'.CApp (t, (L'.CConcat (bind1, bind2), loc)), loc)
1024 1039
1025 fun doUnify (ns, ns') = 1040 fun doUnify (ns, ns') =
1026 let 1041 let
1027 fun setEmpty c = 1042 fun setEmpty c =
1028 let 1043 let
1047 val gs7 = doUnify (ns1, ns1') 1062 val gs7 = doUnify (ns1, ns1')
1048 val gs8 = doUnify (ns2, ns2') 1063 val gs8 = doUnify (ns2, ns2')
1049 in 1064 in
1050 (e, t, (loc, env, denv, shared, ctx1) 1065 (e, t, (loc, env, denv, shared, ctx1)
1051 :: (loc, env, denv, shared, ctx2) 1066 :: (loc, env, denv, shared, ctx2)
1067 :: (loc, env, denv, use1, use2)
1068 :: (loc, env, denv, bind1, bind2)
1052 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8) 1069 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8)
1053 end 1070 end
1054 1071
1055 | L.EApp (e1, e2) => 1072 | L.EApp (e1, e2) =>
1056 let 1073 let
1973 L'.SgiVal (x, n, t) => 1990 L'.SgiVal (x, n, t) =>
1974 (case hnormCon (env, denv) t of 1991 (case hnormCon (env, denv) t of
1975 ((L'.TFun (dom, ran), _), []) => 1992 ((L'.TFun (dom, ran), _), []) =>
1976 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of 1993 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
1977 (((L'.TRecord domR, _), []), 1994 (((L'.TRecord domR, _), []),
1978 ((L'.CApp (tf, ranR), _), [])) => 1995 ((L'.CApp (tf, arg3), _), [])) =>
1979 (case (hnormCon (env, denv) tf, hnormCon (env, denv) ranR) of 1996 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
1980 ((tf, []), (ranR, [])) => 1997 (((L'.CApp (tf, arg2), _), []),
1981 (case (hnormCon (env, denv) domR, hnormCon (env, denv) ranR) of 1998 (((L'.CRecord (_, []), _), []))) =>
1982 ((domR, []), (ranR, [])) => 1999 (case (hnormCon (env, denv) tf) of
1983 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), 2000 ((L'.CApp (tf, arg1), _), []) =>
1984 (L'.CApp (tf, ranR), loc)), 2001 (case (hnormCon (env, denv) tf,
1985 loc)), loc) 2002 hnormCon (env, denv) domR,
2003 hnormCon (env, denv) arg2) of
2004 ((tf, []), (domR, []),
2005 ((L'.CRecord (_, []), _), [])) =>
2006 let
2007 val t = (L'.CApp (tf, arg1), loc)
2008 val t = (L'.CApp (t, arg2), loc)
2009 val t = (L'.CApp (t, arg3), loc)
2010 in
2011 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
2012 t),
2013 loc)), loc)
2014 end
2015 | _ => all)
1986 | _ => all) 2016 | _ => all)
1987 | _ => all) 2017 | _ => all)
1988 | _ => all) 2018 | _ => all)
1989 | _ => all) 2019 | _ => all)
1990 | _ => all 2020 | _ => all