summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-08-19 17:28:52 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-08-19 17:28:52 -0400
commit458bed0042d7bb206138ba6dce98686b056ae5c0 (patch)
tree025b60966e74a3a00397814e167b4c71e1a63783
parent9da36d3a4dd89b2486b832384321c7a548ac67ca (diff)
Polymorphic variants
-rw-r--r--CHANGELOG7
-rw-r--r--lib/ur/basis.urs7
-rw-r--r--src/mono_opt.sml2
-rw-r--r--src/monoize.sml139
-rw-r--r--tests/pvar.ur5
-rw-r--r--tests/pvar.urp1
-rw-r--r--tests/pvar.urs1
7 files changed, 151 insertions, 11 deletions
diff --git a/CHANGELOG b/CHANGELOG
index 14983d28..3d3506f6 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,4 +1,11 @@
========
+Next
+========
+
+- Polymorphic variants (see Basis.variant)
+- (* *) and <!-- --> comments in XML
+
+========
20100603
========
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index f6141bc7..d9967d12 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -14,6 +14,13 @@ datatype option t = None | Some of t
datatype list t = Nil | Cons of t * list t
+(** Polymorphic variants *)
+
+con variant :: {Type} -> Type
+val make : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => t -> variant ([nm = t] ++ ts)
+val match : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (fn t' => t' -> t) ts) -> t
+
+
(** Basic type classes *)
class eq
diff --git a/src/mono_opt.sml b/src/mono_opt.sml
index cf1b1cfe..c3bd0b2d 100644
--- a/src/mono_opt.sml
+++ b/src/mono_opt.sml
@@ -526,6 +526,8 @@ fun exp e =
EFfiApp ("Basis", "attrifyChar", [e])
| EFfiApp ("Basis", "attrifyString_w", [(EFfiApp ("Basis", "str1", [e]), _)]) =>
EFfiApp ("Basis", "attrifyChar_w", [e])
+
+ | EBinop ("+", (EPrim (Prim.Int n1), _), (EPrim (Prim.Int n2), _)) => EPrim (Prim.Int (Int64.+ (n1, n2)))
| _ => e
diff --git a/src/monoize.sml b/src/monoize.sml
index d43002cb..a7f790c3 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -36,11 +36,47 @@ structure L' = Mono
structure IM = IntBinaryMap
structure IS = IntBinarySet
-structure SS = BinarySetFn(struct
- type ord_key = string
- val compare = String.compare
+structure SK = struct
+type ord_key = string
+val compare = String.compare
+end
+
+structure SS = BinarySetFn(SK)
+structure SM = BinaryMapFn(SK)
+
+structure RM = BinaryMapFn(struct
+ type ord_key = (string * L'.typ) list
+ fun compare (r1, r2) = MonoUtil.Typ.compare ((L'.TRecord r1, E.dummySpan),
+ (L'.TRecord r2, E.dummySpan))
end)
+val nextPvar = ref 0
+val pvars = ref (RM.empty : (int * (string * int * L'.typ) list) RM.map)
+val pvarDefs = ref ([] : L'.decl list)
+
+fun choosePvar () =
+ let
+ val n = !nextPvar
+ in
+ nextPvar := n + 1;
+ n
+ end
+
+fun pvar (r, loc) =
+ case RM.find (!pvars, r) of
+ NONE =>
+ let
+ val n = choosePvar ()
+ val fs = map (fn (x, t) => (x, choosePvar (), t)) r
+ val fs' = foldl (fn ((x, n, _), fs') => SM.insert (fs', x, n)) SM.empty fs
+ in
+ pvars := RM.insert (!pvars, r, (n, fs));
+ pvarDefs := (L'.DDatatype [("$poly" ^ Int.toString n, n, map (fn (x, n, t) => (x, n, SOME t)) fs)], loc)
+ :: !pvarDefs;
+ (n, fs)
+ end
+ | SOME v => v
+
val singletons = SS.addList (SS.empty,
["link",
"br",
@@ -120,6 +156,16 @@ fun monoType env =
| L.CApp ((L.CFfi ("Basis", "list"), _), t) =>
(L'.TList (mt env dtmap t), loc)
+ | L.CApp ((L.CFfi ("Basis", "variant"), _), (L.CRecord ((L.KType, _), xts), _)) =>
+ let
+ val xts = map (fn (x, t) => (monoName env x, mt env dtmap t)) xts
+ val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts
+ val (n, cs) = pvar (xts, loc)
+ val cs = map (fn (x, n, t) => (x, n, SOME t)) cs
+ in
+ (L'.TDatatype (n, ref (ElabUtil.classifyDatatype cs, cs)), loc)
+ end
+
| L.CApp ((L.CFfi ("Basis", "monad"), _), _) =>
(L'.TRecord [], loc)
@@ -348,8 +394,24 @@ fun empty count = {
decls = []
}
+fun chooseNext count =
+ let
+ val n = !nextPvar
+ in
+ if count < n then
+ (count, count+1)
+ else
+ (nextPvar := n + 1;
+ (n, n+1))
+ end
+
fun enter ({count, map, listMap, ...} : t) = {count = count, map = map, listMap = listMap, decls = []}
-fun freshName {count, map, listMap, decls} = (count, {count = count + 1, map = map, listMap = listMap, decls = decls})
+fun freshName {count, map, listMap, decls} =
+ let
+ val (next, count) = chooseNext count
+ in
+ (next, {count = count , map = map, listMap = listMap, decls = decls})
+ end
fun decls ({decls, ...} : t) = decls
fun lookup (t as {count, map, listMap, decls}) k n thunk =
@@ -752,6 +814,53 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
end
| L.ECon _ => poly ()
+ | L.ECApp (
+ (L.ECApp (
+ (L.ECApp ((L.EFfi ("Basis", "make"), _), (L.CName nm, _)), _),
+ t), _),
+ (L.CRecord (_, xts), _)) =>
+ let
+ val t = monoType env t
+ val xts = map (fn (x, t) => (monoName env x, monoType env t)) xts
+ val xts = (nm, t) :: xts
+ val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts
+ val (n, cs) = pvar (xts, loc)
+ val cs' = map (fn (x, n, t) => (x, n, SOME t)) cs
+ val cl = ElabUtil.classifyDatatype cs'
+ in
+ case List.find (fn (nm', _, _) => nm' = nm) cs of
+ NONE => raise Fail "Monoize: Polymorphic variant tag mismatch for 'make'"
+ | SOME (_, n', _) => ((L'.EAbs ("x", t, (L'.TDatatype (n, ref (cl, cs')), loc),
+ (L'.ECon (cl, L'.PConVar n', SOME (L'.ERel 0, loc)), loc)), loc),
+ fm)
+ end
+
+ | L.ECApp (
+ (L.ECApp ((L.EFfi ("Basis", "match"), _), (L.CRecord (_, xts), _)), _),
+ t) =>
+ let
+ val t = monoType env t
+ val xts = map (fn (x, t) => (monoName env x, monoType env t)) xts
+ val xts = ListMergeSort.sort (fn ((x, _), (y, _)) => String.compare (x, y) = GREATER) xts
+ val (n, cs) = pvar (xts, loc)
+ val cs' = map (fn (x, n, t) => (x, n, SOME t)) cs
+ val cl = ElabUtil.classifyDatatype cs'
+ val fs = (L'.TRecord (map (fn (x, t') => (x, (L'.TFun (t', t), loc))) xts), loc)
+ val dt = (L'.TDatatype (n, ref (cl, cs')), loc)
+ in
+ ((L'.EAbs ("v",
+ dt,
+ (L'.TFun (fs, t), loc),
+ (L'.EAbs ("fs", fs, t,
+ (L'.ECase ((L'.ERel 1, loc),
+ map (fn (x, n', t') =>
+ ((L'.PCon (cl, L'.PConVar n', SOME (L'.PVar ("x", t'), loc)), loc),
+ (L'.EApp ((L'.EField ((L'.ERel 1, loc), x), loc),
+ (L'.ERel 0, loc)), loc))) cs,
+ {disc = dt, result = t}), loc)), loc)), loc),
+ fm)
+ end
+
| L.ECApp ((L.EFfi ("Basis", "eq"), _), t) =>
let
val t = monoType env t
@@ -3821,6 +3930,8 @@ datatype expungable = Client | Channel
fun monoize env file =
let
+ val () = pvars := RM.empty
+
(* Calculate which exported functions need cookie signature protection *)
val rcook = foldl (fn ((d, _), rcook) =>
case d of
@@ -3958,6 +4069,9 @@ fun monoize env file =
| _ => e) e file
end
+ val mname = CoreUtil.File.maxName file + 1
+ val () = nextPvar := mname
+
val (_, _, ds) = List.foldl (fn (d, (env, fm, ds)) =>
case #1 d of
L.DDatabase s =>
@@ -3984,14 +4098,17 @@ fun monoize env file =
:: ds)
end
| _ =>
- case monoDecl (env, fm) d of
- NONE => (env, fm, ds)
- | SOME (env, fm, ds') =>
- (env,
- Fm.enter fm,
- ds' @ Fm.decls fm @ ds))
- (env, Fm.empty (CoreUtil.File.maxName file + 1), []) file
+ (pvarDefs := [];
+ case monoDecl (env, fm) d of
+ NONE => (env, fm, ds)
+ | SOME (env, fm, ds') =>
+ (env,
+ Fm.enter fm,
+ ds' @ Fm.decls fm @ !pvarDefs @ ds)))
+ (env, Fm.empty mname, []) file
in
+ pvars := RM.empty;
+ pvarDefs := [];
rev ds
end
diff --git a/tests/pvar.ur b/tests/pvar.ur
new file mode 100644
index 00000000..6b90e2c0
--- /dev/null
+++ b/tests/pvar.ur
@@ -0,0 +1,5 @@
+val v1 : variant [A = int, B = float] = make [#A] 1
+val v2 : variant [A = int, B = float] = make [#B] 2.3
+
+fun main () = return (match v1 {A = fn n => <xml>A: {[n]}</xml>,
+ B = fn n => <xml>B: {[n]}</xml>})
diff --git a/tests/pvar.urp b/tests/pvar.urp
new file mode 100644
index 00000000..f86c4a2e
--- /dev/null
+++ b/tests/pvar.urp
@@ -0,0 +1 @@
+pvar
diff --git a/tests/pvar.urs b/tests/pvar.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/tests/pvar.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page