changeset 1287:5137b0537c92

Polymorphic variants
author Adam Chlipala <adam@chlipala.net>
date Thu, 19 Aug 2010 17:28:52 -0400
parents 829da30fb808
children fc7ecf8883b1
files CHANGELOG lib/ur/basis.urs src/mono_opt.sml src/monoize.sml tests/pvar.ur tests/pvar.urp tests/pvar.urs
diffstat 7 files changed, 151 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/CHANGELOG	Tue Aug 10 16:02:55 2010 -0400
+++ b/CHANGELOG	Thu Aug 19 17:28:52 2010 -0400
@@ -1,3 +1,10 @@
+========
+Next
+========
+
+- Polymorphic variants (see Basis.variant)
+- (* *) and <!-- --> comments in XML
+
 ========
 20100603
 ========
--- a/lib/ur/basis.urs	Tue Aug 10 16:02:55 2010 -0400
+++ b/lib/ur/basis.urs	Thu Aug 19 17:28:52 2010 -0400
@@ -14,6 +14,13 @@
 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
--- a/src/mono_opt.sml	Tue Aug 10 16:02:55 2010 -0400
+++ b/src/mono_opt.sml	Thu Aug 19 17:28:52 2010 -0400
@@ -526,6 +526,8 @@
         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
 
--- a/src/monoize.sml	Tue Aug 10 16:02:55 2010 -0400
+++ b/src/monoize.sml	Thu Aug 19 17:28:52 2010 -0400
@@ -36,11 +36,47 @@
 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 @@
                   | 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 @@
     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 @@
             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 @@
 
 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 @@
                             | _ => 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 @@
                                                                    :: 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
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/pvar.ur	Thu Aug 19 17:28:52 2010 -0400
@@ -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>})
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/pvar.urp	Thu Aug 19 17:28:52 2010 -0400
@@ -0,0 +1,1 @@
+pvar
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/pvar.urs	Thu Aug 19 17:28:52 2010 -0400
@@ -0,0 +1,1 @@
+val main : unit -> transaction page