From 73b3f4158297d0161e1d18c24ff9a4604f07c32c 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 --- src/unpoly.sml | 155 +++++++++++++++++++++++++++++++-------------------------- 1 file changed, 85 insertions(+), 70 deletions(-) (limited to 'src/unpoly.sml') 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