Mercurial > urweb

comparison src/monoize.sml @ 1288:fc7ecf8883b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some post-type-checking support for polymorphic variants
author Adam Chlipala <adam@chlipala.net>
date Sat, 21 Aug 2010 10:58:13 -0400
parents 5137b0537c92
children 6791454653c5
comparison
equal deleted inserted replaced
1287:5137b0537c92 1288:fc7ecf8883b1
51 end) 51 end)
52 52
53 val nextPvar = ref 0 53 val nextPvar = ref 0
54 val pvars = ref (RM.empty : (int * (string * int * L'.typ) list) RM.map) 54 val pvars = ref (RM.empty : (int * (string * int * L'.typ) list) RM.map)
55 val pvarDefs = ref ([] : L'.decl list) 55 val pvarDefs = ref ([] : L'.decl list)
56 val pvarOldDefs = ref ([] : (int * (string * int * L.con option) list) list)
56 57
57 fun choosePvar () = 58 fun choosePvar () =
58 let 59 let
59 val n = !nextPvar 60 val n = !nextPvar
60 in 61 in
61 nextPvar := n + 1; 62 nextPvar := n + 1;
62 n 63 n
63 end 64 end
64 65
65 fun pvar (r, loc) = 66 fun pvar (r, r', loc) =
66 case RM.find (!pvars, r) of 67 case RM.find (!pvars, r') of
67 NONE => 68 NONE =>
68 let 69 let
69 val n = choosePvar () 70 val n = choosePvar ()
70 val fs = map (fn (x, t) => (x, choosePvar (), t)) r 71 val fs = map (fn (x, t) => (x, choosePvar (), t)) r'
71 val fs' = foldl (fn ((x, n, _), fs') => SM.insert (fs', x, n)) SM.empty fs 72 val (r, fs') = ListPair.foldr (fn ((_, t), (x, n, _), (r, fs')) =>
73 ((x, n, SOME t) :: r,
74 SM.insert (fs', x, n))) ([], SM.empty) (r, fs)
72 in 75 in
73 pvars := RM.insert (!pvars, r, (n, fs)); 76 pvars := RM.insert (!pvars, r', (n, fs));
74 pvarDefs := (L'.DDatatype [("$poly" ^ Int.toString n, n, map (fn (x, n, t) => (x, n, SOME t)) fs)], loc) 77 pvarDefs := (L'.DDatatype [("$poly" ^ Int.toString n, n, map (fn (x, n, t) => (x, n, SOME t)) fs)], loc)
75 :: !pvarDefs; 78 :: !pvarDefs;
79 pvarOldDefs := (n, r) :: !pvarOldDefs;
76 (n, fs) 80 (n, fs)
77 end 81 end
78 | SOME v => v 82 | SOME v => v
79 83
80 val singletons = SS.addList (SS.empty, 84 val singletons = SS.addList (SS.empty,
156 | L.CApp ((L.CFfi ("Basis", "list"), _), t) => 160 | L.CApp ((L.CFfi ("Basis", "list"), _), t) =>
157 (L'.TList (mt env dtmap t), loc) 161 (L'.TList (mt env dtmap t), loc)
158 162
159 | L.CApp ((L.CFfi ("Basis", "variant"), _), (L.CRecord ((L.KType, _), xts), _)) => 163 | L.CApp ((L.CFfi ("Basis", "variant"), _), (L.CRecord ((L.KType, _), xts), _)) =>
160 let 164 let
161 val xts = map (fn (x, t) => (monoName env x, mt env dtmap t)) xts 165 val xts' = map (fn (x, t) => (monoName env x, mt env dtmap t)) xts
162 val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts 166 val xts' = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts'
163 val (n, cs) = pvar (xts, loc) 167 val (n, cs) = pvar (xts, xts', loc)
164 val cs = map (fn (x, n, t) => (x, n, SOME t)) cs 168 val cs = map (fn (x, n, t) => (x, n, SOME t)) cs
165 in 169 in
166 (L'.TDatatype (n, ref (ElabUtil.classifyDatatype cs, cs)), loc) 170 (L'.TDatatype (n, ref (ElabUtil.classifyDatatype cs, cs)), loc)
167 end 171 end
168 172
814 end 818 end
815 | L.ECon _ => poly () 819 | L.ECon _ => poly ()
816 820
817 | L.ECApp ( 821 | L.ECApp (
818 (L.ECApp ( 822 (L.ECApp (
819 (L.ECApp ((L.EFfi ("Basis", "make"), _), (L.CName nm, _)), _), 823 (L.ECApp ((L.EFfi ("Basis", "make"), _), nmC as (L.CName nm, _)), _),
820 t), _), 824 t), _),
821 (L.CRecord (_, xts), _)) => 825 (L.CRecord (_, xts), _)) =>
822 let 826 let
823 val t = monoType env t 827 val t' = monoType env t
824 val xts = map (fn (x, t) => (monoName env x, monoType env t)) xts 828 val xts' = map (fn (x, t) => (monoName env x, monoType env t)) xts
825 val xts = (nm, t) :: xts 829 val xts' = (nm, t') :: xts'
826 val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts 830 val xts' = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts'
827 val (n, cs) = pvar (xts, loc) 831 val (n, cs) = pvar ((nmC, t) :: xts, xts', loc)
828 val cs' = map (fn (x, n, t) => (x, n, SOME t)) cs 832 val cs' = map (fn (x, n, t) => (x, n, SOME t)) cs
829 val cl = ElabUtil.classifyDatatype cs' 833 val cl = ElabUtil.classifyDatatype cs'
830 in 834 in
831 case List.find (fn (nm', _, _) => nm' = nm) cs of 835 case List.find (fn (nm', _, _) => nm' = nm) cs of
832 NONE => raise Fail "Monoize: Polymorphic variant tag mismatch for 'make'" 836 NONE => raise Fail "Monoize: Polymorphic variant tag mismatch for 'make'"
833 | SOME (_, n', _) => ((L'.EAbs ("x", t, (L'.TDatatype (n, ref (cl, cs')), loc), 837 | SOME (_, n', _) => ((L'.EAbs ("x", t', (L'.TDatatype (n, ref (cl, cs')), loc),
834 (L'.ECon (cl, L'.PConVar n', SOME (L'.ERel 0, loc)), loc)), loc), 838 (L'.ECon (cl, L'.PConVar n', SOME (L'.ERel 0, loc)), loc)), loc),
835 fm) 839 fm)
836 end 840 end
837 841
838 | L.ECApp ( 842 | L.ECApp (
839 (L.ECApp ((L.EFfi ("Basis", "match"), _), (L.CRecord (_, xts), _)), _), 843 (L.ECApp ((L.EFfi ("Basis", "match"), _), (L.CRecord (_, xts), _)), _),
840 t) => 844 t) =>
841 let 845 let
842 val t = monoType env t 846 val t = monoType env t
843 val xts = map (fn (x, t) => (monoName env x, monoType env t)) xts 847 val xts' = map (fn (x, t) => (monoName env x, monoType env t)) xts
844 val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts 848 val xts' = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts'
845 val (n, cs) = pvar (xts, loc) 849 val (n, cs) = pvar (xts, xts', loc)
846 val cs' = map (fn (x, n, t) => (x, n, SOME t)) cs 850 val cs' = map (fn (x, n, t) => (x, n, SOME t)) cs
847 val cl = ElabUtil.classifyDatatype cs' 851 val cl = ElabUtil.classifyDatatype cs'
848 val fs = (L'.TRecord (map (fn (x, t') => (x, (L'.TFun (t', t), loc))) xts), loc) 852 val fs = (L'.TRecord (map (fn (x, t') => (x, (L'.TFun (t', t), loc))) xts'), loc)
849 val dt = (L'.TDatatype (n, ref (cl, cs')), loc) 853 val dt = (L'.TDatatype (n, ref (cl, cs')), loc)
850 in 854 in
851 ((L'.EAbs ("v", 855 ((L'.EAbs ("v",
852 dt, 856 dt,
853 (L'.TFun (fs, t), loc), 857 (L'.TFun (fs, t), loc),
4097 :: (dIni, loc) 4101 :: (dIni, loc)
4098 :: ds) 4102 :: ds)
4099 end 4103 end
4100 | _ => 4104 | _ =>
4101 (pvarDefs := []; 4105 (pvarDefs := [];
4106 pvarOldDefs := [];
4102 case monoDecl (env, fm) d of 4107 case monoDecl (env, fm) d of
4103 NONE => (env, fm, ds) 4108 NONE => (env, fm, ds)
4104 | SOME (env, fm, ds') => 4109 | SOME (env, fm, ds') =>
4105 (env, 4110 (foldr (fn ((n, cs), env) =>
4111 Env.declBinds env (L.DDatatype [("$poly" ^ Int.toString n,
4112 n,
4113 [],
4114 cs)], loc))
4115 env (!pvarOldDefs),
4106 Fm.enter fm, 4116 Fm.enter fm,
4107 ds' @ Fm.decls fm @ !pvarDefs @ ds))) 4117 ds' @ Fm.decls fm @ !pvarDefs @ ds)))
4108 (env, Fm.empty mname, []) file 4118 (env, Fm.empty mname, []) file
4109 in 4119 in
4110 pvars := RM.empty; 4120 pvars := RM.empty;
4111 pvarDefs := []; 4121 pvarDefs := [];
4122 pvarOldDefs := [];
4112 rev ds 4123 rev ds
4113 end 4124 end
4114 4125
4115 end 4126 end