Mercurial > urweb

comparison src/core_util.sml @ 807:61a1f5c5ae2c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Effectize
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:45:12 -0400
parents ef6de4075dc1
children ed06e25c70ef
comparison
equal deleted inserted replaced
806:0e554bfd6d6a 807:61a1f5c5ae2c
908 S.bind2 (mfk ctx k, 908 S.bind2 (mfk ctx k,
909 fn k' => 909 fn k' =>
910 S.map2 (mfc ctx c, 910 S.map2 (mfc ctx c,
911 fn c' => 911 fn c' =>
912 (DCon (x, n, k', c'), loc))) 912 (DCon (x, n, k', c'), loc)))
913 | DDatatype (x, n, xs, xncs) => 913 | DDatatype dts =>
914 let 914 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
915 val k = (KType, loc) 915 let
916 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs 916 val k = (KType, loc)
917 val ctx' = bind (ctx, NamedC (x, n, k', NONE)) 917 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
918 in 918 val ctx' = bind (ctx, NamedC (x, n, k', NONE))
919 S.map2 (ListUtil.mapfold (fn (x, n, c) => 919 in
920 case c of 920 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
921 NONE => S.return2 (x, n, c) 921 case c of
922 | SOME c => 922 NONE => S.return2 (x, n, c)
923 S.map2 (mfc ctx' c, 923 | SOME c =>
924 fn c' => (x, n, SOME c'))) xncs, 924 S.map2 (mfc ctx' c,
925 fn xncs' => 925 fn c' => (x, n, SOME c'))) xncs,
926 (DDatatype (x, n, xs, xncs'), loc)) 926 fn xncs' => (x, n, xs, xncs'))
927 end 927 end) dts,
928 fn dts' =>
929 (DDatatype dts', loc))
928 | DVal vi => 930 | DVal vi =>
929 S.map2 (mfvi ctx vi, 931 S.map2 (mfvi ctx vi,
930 fn vi' => 932 fn vi' =>
931 (DVal vi', loc)) 933 (DVal vi', loc))
932 | DValRec vis => 934 | DValRec vis =>
1057 fn d' => 1059 fn d' =>
1058 let 1060 let
1059 val ctx' = 1061 val ctx' =
1060 case #1 d' of 1062 case #1 d' of
1061 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c)) 1063 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
1062 | DDatatype (x, n, xs, xncs) => 1064 | DDatatype dts =>
1063 let 1065 foldl (fn ((x, n, xs, xncs), ctx) =>
1064 val loc = #2 d' 1066 let
1065 val k = (KType, loc) 1067 val loc = #2 d'
1066 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs 1068 val k = (KType, loc)
1067 1069 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
1068 val ctx = bind (ctx, NamedC (x, n, k', NONE)) 1070
1069 val t = (CNamed n, #2 d') 1071 val ctx = bind (ctx, NamedC (x, n, k', NONE))
1070 val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc)) 1072 val t = (CNamed n, #2 d')
1071 t xs 1073 val t = ListUtil.foldli (fn (i, _, t) =>
1072 in 1074 (CApp (t, (CRel i, loc)), loc))
1073 foldl (fn ((x, n, to), ctx) => 1075 t xs
1074 let 1076 in
1075 val t = case to of 1077 foldl (fn ((x, n, to), ctx) =>
1076 NONE => t 1078 let
1077 | SOME t' => (TFun (t', t), #2 d') 1079 val t = case to of
1078 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) 1080 NONE => t
1079 t xs 1081 | SOME t' => (TFun (t', t), #2 d')
1080 in 1082 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
1081 bind (ctx, NamedE (x, n, t, NONE, "")) 1083 t xs
1082 end) 1084 in
1083 ctx xncs 1085 bind (ctx, NamedE (x, n, t, NONE, ""))
1084 end 1086 end)
1087 ctx xncs
1088 end)
1089 ctx dts
1085 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s)) 1090 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
1086 | DValRec vis => 1091 | DValRec vis =>
1087 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s))) 1092 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
1088 ctx vis 1093 ctx vis
1089 | DExport _ => ctx 1094 | DExport _ => ctx
1172 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible" 1177 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
1173 1178
1174 val maxName = foldl (fn ((d, _) : decl, count) => 1179 val maxName = foldl (fn ((d, _) : decl, count) =>
1175 case d of 1180 case d of
1176 DCon (_, n, _, _) => Int.max (n, count) 1181 DCon (_, n, _, _) => Int.max (n, count)
1177 | DDatatype (_, n, _, ns) => 1182 | DDatatype dts => foldl (fn ((_, n, _, ns), count) =>
1178 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1183 foldl (fn ((_, n', _), m) => Int.max (n', m))
1179 (Int.max (n, count)) ns 1184 (Int.max (n, count)) ns) count dts
1180 | DVal (_, n, _, _, _) => Int.max (n, count) 1185 | DVal (_, n, _, _, _) => Int.max (n, count)
1181 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis 1186 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
1182 | DExport _ => count 1187 | DExport _ => count
1183 | DTable (_, n, _, _, _, _, _, _) => Int.max (n, count) 1188 | DTable (_, n, _, _, _, _, _, _) => Int.max (n, count)
1184 | DSequence (_, n, _) => Int.max (n, count) 1189 | DSequence (_, n, _) => Int.max (n, count)