Some standard library reorgs and additions; handle mutual datatypes better in Specialize

9 files changed, 85 insertions, 60 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index c5c4f6f2..50909804 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -25,7 +25,6 @@ val eq_string : eq string
 val eq_char : eq char
 val eq_bool : eq bool
 val eq_time : eq time
-val eq_option : t ::: Type -> eq t -> eq (option t)
 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
 
 class num
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 2e62facb..b99ef515 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -10,6 +10,17 @@ val show = fn [a] (_ : show a) =>
                   mkShow show'
               end
 
+val eq = fn [a] (_ : eq a) =>
+            let
+                fun eq' (ls1 : list a) ls2 =
+                    case (ls1, ls2) of
+                        ([], []) => True
+                      | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
+                      | _ => False
+            in
+                mkEq eq'
+            end
+
 fun foldl [a] [b] f =
     let
         fun foldl' acc ls =
@@ -20,6 +31,19 @@ fun foldl [a] [b] f =
         foldl'
     end
 
+fun foldlPartial [a] [b] f =
+    let
+        fun foldlPartial' acc ls =
+            case ls of
+                [] => Some acc
+              | x :: ls =>
+                case f x acc of
+                    None => None
+                  | Some acc' => foldlPartial' acc' ls
+    in
+        foldlPartial'
+    end
+
 val rev = fn [a] =>
              let
                  fun rev' acc (ls : list a) =
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index daf81074..f5495d41 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -1,8 +1,10 @@
 datatype t = datatype Basis.list
 
-val show : a ::: Type -> show a -> show (list a)
+val show : a ::: Type -> show a -> show (t a)
+val eq : a ::: Type -> eq a -> eq (t a)
 
 val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
+val foldlPartial : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b
 
 val rev : a ::: Type -> t a -> t a
 
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
index 8d1c873e..745e436c 100644
--- a/lib/ur/listPair.ur
+++ b/lib/ur/listPair.ur
@@ -1,3 +1,17 @@
+fun foldlPartial [a] [b] [c] f =
+    let
+        fun foldlPartial' acc ls1 ls2 =
+            case (ls1, ls2) of
+                ([], []) => Some acc
+              | (x1 :: ls1, x2 :: ls2) =>
+                (case f x1 x2 acc of
+                     None => None
+                   | Some acc' => foldlPartial' acc' ls1 ls2)
+              | _ => None
+    in
+        foldlPartial'
+    end
+
 fun mapX [a] [b] [ctx ::: {Unit}] f =
     let
         fun mapX' ls1 ls2 =
diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs
index 0c5e5443..310a1a4e 100644
--- a/lib/ur/listPair.urs
+++ b/lib/ur/listPair.urs
@@ -1,3 +1,6 @@
+val foldlPartial : a ::: Type -> b ::: Type -> c ::: Type
+                   -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c
+
 val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit}
            -> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] []
 
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index 5ec093c0..1f044002 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -1,5 +1,12 @@
 datatype t = datatype Basis.option
 
+fun eq [a] (_ : eq a) =
+    mkEq (fn x y =>
+             case (x, y) of
+                 (None, None) => True
+               | (Some x, Some y) => x = y
+               | _ => False)
+
 fun isSome [a] x =
     case x of
         None => False
@@ -9,3 +16,8 @@ fun mp [a] [b] f x =
     case x of
         None => None
       | Some y => Some (f y)
+
+fun bind [a] [b] f x =
+    case x of
+        None => None
+      | Some y => f y
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index ced6156e..984bc681 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -1,5 +1,8 @@
 datatype t = datatype Basis.option
 
+val eq : a ::: Type -> eq a -> eq (t a)
+
 val isSome : a ::: Type -> t a -> bool
 
 val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
diff --git a/src/monoize.sml b/src/monoize.sml
index e0795b84..d3eb4874 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -778,47 +778,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                                  (L'.TFfi ("Basis", "bool"), loc),
                                  (L'.EBinop ("==", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
              fm)
-          | L.ECApp ((L.EFfi ("Basis", "eq_option"), _), t) =>
-            let
-                val t = monoType env t
-                val t' = (L'.TOption t, loc)
-                val bool = (L'.TFfi ("Basis", "bool"), loc)
-            in
-                ((L'.EAbs ("f", (L'.TFun (t, (L'.TFun (t, bool), loc)), loc),
-                           (L'.TFun (t', (L'.TFun (t', bool), loc)), loc),
-                           (L'.EAbs ("x", t', (L'.TFun (t', bool), loc),
-                                     (L'.EAbs ("y", t', bool,
-                                               (L'.ECase ((L'.ERecord [("1", (L'.ERel 1, loc), t'),
-                                                                       ("2", (L'.ERel 0, loc), t')], loc),
-                                                          [((L'.PRecord [("1", (L'.PNone t, loc), t'),
-                                                                         ("2", (L'.PNone t, loc), t')], loc),
-                                                            (L'.ECon (L'.Enum, L'.PConFfi {mod = "Basis",
-                                                                                           datatyp = "bool",
-                                                                                           con = "True",
-                                                                                           arg = NONE},
-                                                                      NONE), loc)),
-                                                           ((L'.PRecord [("1", (L'.PSome (t,
-                                                                                          (L'.PVar ("x1",
-                                                                                                    t), loc)),
-                                                                                loc), t'),
-                                                                         ("2", (L'.PSome (t,
-                                                                                          (L'.PVar ("x2",
-                                                                                                    t), loc)),
-                                                                                loc), t')], loc),
-                                                            (L'.EApp ((L'.EApp ((L'.ERel 4, loc),
-                                                                                (L'.ERel 1, loc)), loc),
-                                                                      (L'.ERel 0, loc)), loc)),
-                                                           ((L'.PWild, loc),
-                                                            (L'.ECon (L'.Enum, L'.PConFfi {mod = "Basis",
-                                                                                           datatyp = "bool",
-                                                                                           con = "False",
-                                                                                           arg = NONE},
-                                                                      NONE), loc))],
-                                                          {disc = (L'.TRecord [("1", t'), ("2", t')], loc),
-                                                           result = (L'.TFfi ("Basis", "bool"), loc)}),
-                                                loc)), loc)), loc)), loc),
-                 fm)
-            end
 
           | L.ECApp ((L.EFfi ("Basis", "mkEq"), _), t) =>
             let
diff --git a/src/specialize.sml b/src/specialize.sml
index b0e0aeae..b740ec8c 100644
--- a/src/specialize.sml
+++ b/src/specialize.sml
@@ -61,7 +61,7 @@ type state = {
      count : int,
      datatypes : datatyp IM.map,
      constructors : int IM.map,
-     decls : decl list     
+     decls : (string * int * string list * (string * int * con option) list) list     
 }
 
 fun kind (k, st) = (k, st)
@@ -115,15 +115,15 @@ fun considerSpecialization (st : state, n, args, dt : datatyp) =
                                                        ((x, n, SOME t), st)
                                                    end) st cons
 
-            val d = (DDatatype [(#name dt ^ "_s",
-                                 n',
-                                 [],
-                                 cons)], #2 (List.hd args))
+            val dt = (#name dt ^ "_s",
+                      n',
+                      [],
+                      cons)
         in
             (n', cmap, {count = #count st,
                         datatypes = #datatypes st,
                         constructors = #constructors st,
-                        decls = d :: #decls st})
+                        decls = dt :: #decls st})
         end
 
 and con (c, st : state) =
@@ -246,22 +246,31 @@ fun specialize file =
             let
                 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*)
                 val (d, st) = specDecl st d
+
+                val ds =
+                    case #decls st of
+                        [] => []
+                      | dts => [(DDatatype dts, #2 d)]
             in
                 case #1 d of
-                    DDatatype [(x, n, xs, xnts)] =>
-                    (rev (d :: #decls st),
+                    DDatatype dts =>
+                    (rev (d :: ds),
                      {count = #count st,
-                      datatypes = IM.insert (#datatypes st, n,
-                                             {name = x,
-                                              params = length xs,
-                                              constructors = xnts,
-                                              specializations = CM.empty}),
-                      constructors = foldl (fn ((_, n', _), constructors) =>
-                                               IM.insert (constructors, n', n))
-                                           (#constructors st) xnts,
+                      datatypes = foldl (fn ((x, n, xs, xnts), dts) =>
+                                            IM.insert (dts, n,
+                                                       {name = x,
+                                                        params = length xs,
+                                                        constructors = xnts,
+                                                        specializations = CM.empty}))
+                                        (#datatypes st) dts,
+                      constructors = foldl (fn ((x, n, xs, xnts), cs) =>
+                                               foldl (fn ((_, n', _), constructors) =>
+                                                         IM.insert (constructors, n', n))
+                                                     cs xnts)
+                                           (#constructors st) dts,
                       decls = []})
                   | _ =>
-                    (rev (d :: #decls st),
+                    (rev (d :: ds),
                      {count = #count st,
                       datatypes = #datatypes st,
                       constructors = #constructors st,