summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 13:41:03 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 13:41:03 -0400
commit69559dc94815a000729c7ccef8216dec5b5158cc (patch)
treebea645178c714fbf1a04173bb04a9dbe22c634b7
parentac6a32c651d76d10650fffb99f77f05c583ff0cf (diff)
listFun uses length
-rw-r--r--demo/listFun.ur2
-rw-r--r--src/unpoly.sml144
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)