summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/ur/string.ur5
-rw-r--r--lib/ur/string.urs2
-rw-r--r--src/reduce.sml2
-rw-r--r--src/unpoly.sml155
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}