Mercurial > urweb

comparison src/elaborate.sml @ 182:d11754ffe252

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Compiled pattern matching to C
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 12:43:20 -0400
parents 33d4a8eea484
children 8e9f97508f0d
comparison
equal deleted inserted replaced
181:31dfab1d4050 182:d11754ffe252
902 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), 902 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
903 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), 903 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
904 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), 904 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
905 loc)), loc)), loc) 905 loc)), loc)), loc)
906 906
907 fun typeof env (e, loc) =
908 case e of
909 L'.EPrim p => primType env p
910 | L'.ERel n => #2 (E.lookupERel env n)
911 | L'.ENamed n => #2 (E.lookupENamed env n)
912 | L'.EModProj (n, ms, x) =>
913 let
914 val (_, sgn) = E.lookupStrNamed env n
915 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
916 case E.projectStr env {sgn = sgn, str = str, field = m} of
917 NONE => raise Fail "typeof: Unknown substructure"
918 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
919 ((L'.StrVar n, loc), sgn) ms
920 in
921 case E.projectVal env {sgn = sgn, str = str, field = x} of
922 NONE => raise Fail "typeof: Unknown val in structure"
923 | SOME t => t
924 end
925
926 | L'.EApp (e1, _) =>
927 (case #1 (typeof env e1) of
928 L'.TFun (_, c) => c
929 | _ => raise Fail "typeof: Bad EApp")
930 | L'.EAbs (_, _, ran, _) => ran
931 | L'.ECApp (e1, c) =>
932 (case #1 (typeof env e1) of
933 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
934 | _ => raise Fail "typeof: Bad ECApp")
935 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
936
937 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
938 | L'.EField (_, _, {field, ...}) => field
939 | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc)
940 | L'.EFold dom => foldType (dom, loc)
941
942 | L'.ECase (_, _, t) => t
943
944 | L'.EError => cerror
945
946 fun elabHead (env, denv) (e as (_, loc)) t = 907 fun elabHead (env, denv) (e as (_, loc)) t =
947 let 908 let
948 fun unravel (t, e) = 909 fun unravel (t, e) =
949 let 910 let
950 val (t, gs) = hnormCon (env, denv) t 911 val (t, gs) = hnormCon (env, denv) t
998 (expError env (DuplicatePatternVariable (loc, x)); 959 (expError env (DuplicatePatternVariable (loc, x));
999 terror) 960 terror)
1000 else 961 else
1001 cunif (loc, (L'.KType, loc)) 962 cunif (loc, (L'.KType, loc))
1002 in 963 in
1003 (((L'.PVar x, loc), t), 964 (((L'.PVar (x, t), loc), t),
1004 (E.pushERel env x t, SS.add (bound, x))) 965 (E.pushERel env x t, SS.add (bound, x)))
1005 end 966 end
1006 | L.PPrim p => (((L'.PPrim p, loc), primType env p), 967 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
1007 (env, bound)) 968 (env, bound))
1008 | L.PCon ([], x, po) => 969 | L.PCon ([], x, po) =>
1016 rerror) 977 rerror)
1017 | SOME (n, sgn) => 978 | SOME (n, sgn) =>
1018 let 979 let
1019 val (str, sgn) = foldl (fn (m, (str, sgn)) => 980 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
1020 case E.projectStr env {sgn = sgn, str = str, field = m} of 981 case E.projectStr env {sgn = sgn, str = str, field = m} of
1021 NONE => raise Fail "typeof: Unknown substructure" 982 NONE => raise Fail "elabPat: Unknown substructure"
1022 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 983 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1023 ((L'.StrVar n, loc), sgn) ms 984 ((L'.StrVar n, loc), sgn) ms
1024 in 985 in
1025 case E.projectConstructor env {str = str, sgn = sgn, field = x} of 986 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
1026 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); 987 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
1049 if flex then 1010 if flex then
1050 (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc) 1011 (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
1051 else 1012 else
1052 c 1013 c
1053 in 1014 in
1054 (((L'.PRecord (map (fn (x, p', _) => (x, p')) xpts), loc), 1015 (((L'.PRecord xpts, loc),
1055 (L'.TRecord c, loc)), 1016 (L'.TRecord c, loc)),
1056 (env, bound)) 1017 (env, bound))
1057 end 1018 end
1058 1019
1059 end 1020 end
1083 L'.PWild => Wild 1044 L'.PWild => Wild
1084 | L'.PVar _ => Wild 1045 | L'.PVar _ => Wild
1085 | L'.PPrim _ => None 1046 | L'.PPrim _ => None
1086 | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) 1047 | L'.PCon (pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
1087 | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) 1048 | L'.PCon (pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
1088 | L'.PRecord xps => Record [foldl (fn ((x, p), fmap) => 1049 | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
1089 SM.insert (fmap, x, coverage p)) SM.empty xps] 1050 SM.insert (fmap, x, coverage p)) SM.empty xps]
1090 1051
1091 fun merge (c1, c2) = 1052 fun merge (c1, c2) =
1092 case (c1, c2) of 1053 case (c1, c2) of
1093 (None, _) => c2 1054 (None, _) => c2
1094 | (_, None) => c1 1055 | (_, None) => c1
1456 if total then 1417 if total then
1457 () 1418 ()
1458 else 1419 else
1459 expError env (Inexhaustive loc); 1420 expError env (Inexhaustive loc);
1460 1421
1461 ((L'.ECase (e', pes', result), loc), result, gs' @ gs) 1422 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs)
1462 end 1423 end
1463 end 1424 end
1464 1425
1465 1426
1466 datatype decl_error = 1427 datatype decl_error =