From bdcf695651fbeff603d6f1c061b410c0cb733dcb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Jan 2010 13:44:22 -0500 Subject: Reduce concatenations of the empty record; unpoly non-recursive functions --- lib/ur/string.ur | 5 ++ lib/ur/string.urs | 2 + src/reduce.sml | 2 + src/unpoly.sml | 155 ++++++++++++++++++++++++++++++------------------------ 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) => {[s1]}
{newlines s2} 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} -- cgit v1.2.3