# HG changeset patch # User Adam Chlipala # Date 1263149062 18000 # Node ID 85d194409b170b98dc3e59c67807a1b99498b01a # Parent 0cee0c8d8c378bc79b91346a3204521be3c16e3d Reduce concatenations of the empty record; unpoly non-recursive functions diff -r 0cee0c8d8c37 -r 85d194409b17 lib/ur/string.ur --- a/lib/ur/string.ur Sun Jan 10 10:40:57 2010 -0500 +++ b/lib/ur/string.ur Sun Jan 10 13:44:22 2010 -0500 @@ -37,3 +37,8 @@ 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 -r 0cee0c8d8c37 -r 85d194409b17 lib/ur/string.urs --- a/lib/ur/string.urs Sun Jan 10 10:40:57 2010 -0500 +++ b/lib/ur/string.urs Sun Jan 10 13:44:22 2010 -0500 @@ -20,3 +20,5 @@ 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 -r 0cee0c8d8c37 -r 85d194409b17 src/reduce.sml --- a/src/reduce.sml Sun Jan 10 10:40:57 2010 -0500 +++ b/src/reduce.sml Sun Jan 10 13:44:22 2010 -0500 @@ -291,6 +291,8 @@ 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 -r 0cee0c8d8c37 -r 85d194409b17 src/unpoly.sml --- a/src/unpoly.sml Sun Jan 10 10:40:57 2010 -0500 +++ b/src/unpoly.sml Sun Jan 10 13:44:22 2010 -0500 @@ -207,79 +207,94 @@ 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 + 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, []) - val cargs = unravel (e, []) + 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 - 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 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 deAbs (e, cargs) = - case (e, cargs) of - ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs) - | (_, []) => e - | _ => raise Fail "Unpoly: deAbs" + 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 *) + (** Verifying lack of polymorphic recursion *) - fun kind _ = false - fun con _ = false + 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 + 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 + 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}