Reduce concatenations of the empty record; unpoly non-recursive functions

4 files changed, 94 insertions, 70 deletions

diff --git a/lib/ur/string.ur b/lib/ur/string.ur
index 41ec666d..4025cf68 100644
--- a/lib/ur/string.ur
+++ b/lib/ur/string.ur
@@ -37,3 +37,8 @@ fun all f s =
     in
         al 0
     end
+
+fun newlines [ctx] [[Body] ~ ctx] s : xml ([Body] ++ ctx) [] [] =
+    case split s #"\n" of
+        None => cdata s
+      | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
diff --git a/lib/ur/string.urs b/lib/ur/string.urs
index fda30ad9..5590b50c 100644
--- a/lib/ur/string.urs
+++ b/lib/ur/string.urs
@@ -20,3 +20,5 @@ val split : t -> char -> option (string * string)
 val msplit : {Haystack : t, Needle : t} -> option (string * char * string)
 
 val all : (char -> bool) -> string -> bool
+
+val newlines : ctx ::: {Unit} -> [[Body] ~ ctx] => string -> xml ([Body] ++ ctx) [] []
diff --git a/src/reduce.sml b/src/reduce.sml
index 95b26da8..cc8ba0fd 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -291,6 +291,8 @@ fun kindConAndExp (namedC, namedE) =
                     case (#1 c1, #1 c2) of
                         (CRecord (k, xcs1), CRecord (_, xcs2)) =>
                         (CRecord (kind env k, xcs1 @ xcs2), loc)
+                      | (CRecord (_, []), _) => c2
+                      | (_, CRecord (_, [])) => c1
                       | _ => (CConcat (c1, c2), loc)
                 end
               | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc)
diff --git a/src/unpoly.sml b/src/unpoly.sml
index 14ab4563..0d239cb9 100644
--- a/src/unpoly.sml
+++ b/src/unpoly.sml
@@ -207,79 +207,94 @@ fun exp (e, st : state) =
 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
 
 fun decl (d, st : state) =
-    case d of
-        DValRec (vis as ((x, n, t, e, s) :: rest)) =>
-        let
-            fun unravel (e, cargs) =
-                case e of
-                    (ECAbs (_, k, e), _) =>
-                    unravel (e, k :: cargs)
-                  | _ => rev cargs
-
-            val cargs = unravel (e, [])
-
-            fun unravel (e, cargs) =
-                case (e, cargs) of
-                    ((ECAbs (_, k, e), _), k' :: cargs) =>
-                    U.Kind.compare (k, k') = EQUAL
-                    andalso unravel (e, cargs)
-                  | (_, []) => true
-                  | _ => false
-        in
-            if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
-                (d, st)
-            else
-                let
-                    val ns = IS.addList (IS.empty, map #2 vis)
-                    val nargs = length cargs
-
-                    fun deAbs (e, cargs) =
-                        case (e, cargs) of
-                            ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
-                          | (_, []) => e
-                          | _ => raise Fail "Unpoly: deAbs"
-
-                    (** Verifying lack of polymorphic recursion *)
+    let
+        fun unravel (e, cargs) =
+            case e of
+                (ECAbs (_, k, e), _) =>
+                unravel (e, k :: cargs)
+              | _ => rev cargs
+    in
+        case d of
+            DVal (vi as (x, n, t, e, s)) =>
+            let
+                val cargs = unravel (e, [])
 
-                    fun kind _ = false
-                    fun con _ = false
+                val ns = IS.singleton n
+            in
+                (d, {funcs = IM.insert (#funcs st, n, {kinds = cargs,
+                                                       defs = [vi],
+                                                       replacements = M.empty}),
+                     decls = #decls st,
+                     nextName = #nextName st})
+            end
+          | DValRec (vis as ((x, n, t, e, s) :: rest)) =>
+            let
+                val cargs = unravel (e, [])
+
+                fun unravel (e, cargs) =
+                    case (e, cargs) of
+                        ((ECAbs (_, k, e), _), k' :: cargs) =>
+                        U.Kind.compare (k, k') = EQUAL
+                        andalso unravel (e, cargs)
+                      | (_, []) => true
+                      | _ => false
+                             
+                fun deAbs (e, cargs) =
+                    case (e, cargs) of
+                        ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
+                      | (_, []) => e
+                      | _ => raise Fail "Unpoly: deAbs"
 
-                    fun exp e =
-                        case e of
-                            ECApp (e, c) =>
-                            let
-                                fun isIrregular (e, pos) =
-                                    case #1 e of
-                                        ENamed n =>
-                                        IS.member (ns, n)
-                                        andalso
-                                        (case #1 c of
-                                             CRel i => i <> nargs - pos
-                                           | _ => true)
-                                      | ECApp (e, _) => isIrregular (e, pos + 1)
-                                      | _ => false
-                            in
-                                isIrregular (e, 1)
-                            end
-                          | ECAbs _ => true
-                          | _ => false
-
-                    val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
-                in
-                    if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
-                        (d, st)
-                    else
-                        (d, {funcs = foldl (fn (vi, funcs) =>
-                                               IM.insert (funcs, #2 vi, {kinds = cargs,
-                                                                         defs = vis,
-                                                                         replacements = M.empty}))
-                                           (#funcs st) vis,
-                             decls = #decls st,
-                             nextName = #nextName st})
-                end
-        end
+            in
+                if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
+                    (d, st)
+                else
+                    let
+                        val ns = IS.addList (IS.empty, map #2 vis)
+                        val nargs = length cargs
+
+                        (** Verifying lack of polymorphic recursion *)
+
+                        fun kind _ = false
+                        fun con _ = false
+
+                        fun exp e =
+                            case e of
+                                ECApp (e, c) =>
+                                let
+                                    fun isIrregular (e, pos) =
+                                        case #1 e of
+                                            ENamed n =>
+                                            IS.member (ns, n)
+                                            andalso
+                                            (case #1 c of
+                                                 CRel i => i <> nargs - pos
+                                               | _ => true)
+                                          | ECApp (e, _) => isIrregular (e, pos + 1)
+                                          | _ => false
+                                in
+                                    isIrregular (e, 1)
+                                end
+                              | ECAbs _ => true
+                              | _ => false
+
+                        val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
+                    in
+                        if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
+                            (d, st)
+                        else
+                            (d, {funcs = foldl (fn (vi, funcs) =>
+                                                   IM.insert (funcs, #2 vi, {kinds = cargs,
+                                                                             defs = vis,
+                                                                             replacements = M.empty}))
+                                               (#funcs st) vis,
+                                 decls = #decls st,
+                                 nextName = #nextName st})
+                    end
+            end
 
-      | _ => (d, st)
+          | _ => (d, st)
+    end
 
 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}