diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-21 13:41:03 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-21 13:41:03 -0400 |
| commit | 69559dc94815a000729c7ccef8216dec5b5158cc (patch) | |
| tree | bea645178c714fbf1a04173bb04a9dbe22c634b7 | |
| parent | ac6a32c651d76d10650fffb99f77f05c583ff0cf (diff) | |
listFun uses length
| -rw-r--r-- | demo/listFun.ur | 2 | ||||
| -rw-r--r-- | src/unpoly.sml | 144 |
2 files changed, 76 insertions, 70 deletions
diff --git a/demo/listFun.ur b/demo/listFun.ur index 74f249b6..c4451e1d 100644 --- a/demo/listFun.ur +++ b/demo/listFun.ur @@ -12,6 +12,8 @@ functor Make(M : sig fun console (ls : list M.t) = return <xml><body> Current list: {toXml ls}<br/> + Length: {[length ls]}<br/> + <br/> <form> Add element: <textbox{#X}/> <submit action={cons ls}/> diff --git a/src/unpoly.sml b/src/unpoly.sml index 5236961b..17878508 100644 --- a/src/unpoly.sml +++ b/src/unpoly.sml @@ -46,17 +46,18 @@ val subConInCon = E.subConInCon val liftConInExp = E.liftConInExp val subConInExp = E.subConInExp +val isOpen = U.Con.exists {kind = fn _ => false, + con = fn c => + case c of + CRel _ => true + | _ => false} + fun unpolyNamed (xn, rep) = U.Exp.map {kind = fn k => k, con = fn c => c, exp = fn e => case e of - ENamed xn' => - if xn' = xn then - rep - else - e - | ECApp (e', _) => + ECApp (e', _) => let fun isTheOne (e, _) = case e of @@ -65,7 +66,7 @@ fun unpolyNamed (xn, rep) = | _ => false in if isTheOne e' then - #1 e' + rep else e end @@ -96,71 +97,74 @@ fun exp (e, st : state) = case unravel (e, []) of NONE => (e, st) | SOME (n, cargs) => - case IM.find (#funcs st, n) of - NONE => (e, st) - | SOME (ks, vis) => - let - val (vis, nextName) = ListUtil.foldlMap - (fn ((x, n, t, e, s), nextName) => - ((x, nextName, n, t, e, s), nextName + 1)) - (#nextName st) vis - - fun specialize (x, n, n_old, t, e, s) = - let - fun trim (t, e, cargs) = - case (t, e, cargs) of - ((TCFun (_, _, t), _), - (ECAbs (_, _, e), _), - carg :: cargs) => - let - val t = subConInCon (length cargs, carg) t - val e = subConInExp (length cargs, carg) e - in - trim (t, e, cargs) - end - | (_, _, []) => - let - val e = foldl (fn ((_, n, n_old, _, _, _), e) => - unpolyNamed (n_old, ENamed n) e) - e vis - in - SOME (t, e) - end - | _ => NONE - in - (*Print.prefaces "specialize" - [("t", CorePrint.p_con CoreEnv.empty t), - ("e", CorePrint.p_exp CoreEnv.empty e), - ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) - Option.map (fn (t, e) => (x, n, n_old, t, e, s)) - (trim (t, e, cargs)) - end + if List.exists isOpen cargs then + (e, st) + else + case IM.find (#funcs st, n) of + NONE => (e, st) + | SOME (ks, vis) => + let + val (vis, nextName) = ListUtil.foldlMap + (fn ((x, n, t, e, s), nextName) => + ((x, nextName, n, t, e, s), nextName + 1)) + (#nextName st) vis - val vis = List.map specialize vis - in - if List.exists (not o Option.isSome) vis orelse length cargs > length ks then - (e, st) - else - let - val vis = List.mapPartial (fn x => x) vis - val vis = map (fn (x, n, n_old, t, e, s) => - (x ^ "_unpoly", n, n_old, t, e, s)) vis - val vis' = map (fn (x, n, _, t, e, s) => - (x, n, t, e, s)) vis + fun specialize (x, n, n_old, t, e, s) = + let + fun trim (t, e, cargs) = + case (t, e, cargs) of + ((TCFun (_, _, t), _), + (ECAbs (_, _, e), _), + carg :: cargs) => + let + val t = subConInCon (length cargs, carg) t + val e = subConInExp (length cargs, carg) e + in + trim (t, e, cargs) + end + | (_, _, []) => + let + val e = foldl (fn ((_, n, n_old, _, _, _), e) => + unpolyNamed (n_old, ENamed n) e) + e vis + in + SOME (t, e) + end + | _ => NONE + in + (*Print.prefaces "specialize" + [("t", CorePrint.p_con CoreEnv.empty t), + ("e", CorePrint.p_exp CoreEnv.empty e), + ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) + Option.map (fn (t, e) => (x, n, n_old, t, e, s)) + (trim (t, e, cargs)) + end - val ks' = List.drop (ks, length cargs) - in - case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of - NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" - | SOME (_, n, _, _, _, _) => - (ENamed n, - {funcs = foldl (fn (vi, funcs) => - IM.insert (funcs, #2 vi, (ks', vis'))) - (#funcs st) vis', - decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, - nextName = nextName}) - end - end + val vis = List.map specialize vis + in + if List.exists (not o Option.isSome) vis orelse length cargs > length ks then + (e, st) + else + let + val vis = List.mapPartial (fn x => x) vis + val vis = map (fn (x, n, n_old, t, e, s) => + (x ^ "_unpoly", n, n_old, t, e, s)) vis + val vis' = map (fn (x, n, _, t, e, s) => + (x, n, t, e, s)) vis + + val ks' = List.drop (ks, length cargs) + in + case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of + NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" + | SOME (_, n, _, _, _, _) => + (ENamed n, + {funcs = foldl (fn (vi, funcs) => + IM.insert (funcs, #2 vi, (ks', vis'))) + (#funcs st) vis', + decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, + nextName = nextName}) + end + end end | _ => (e, st) |