summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 20:38:01 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 20:38:01 -0400
commited34aa061c7d9ba68d8f2419b22c2a0b6b6ce812 (patch)
tree27b25c9e8b68ae517100138ad652c03e538ddb05
parentab0bbbf29220a995f6fa83ae43e0a4a88c9b5159 (diff)
Get demo type-inferring again
-rw-r--r--src/elaborate.sml83
-rw-r--r--src/urweb.grm20
2 files changed, 39 insertions, 64 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 4971ec4c..874f6c82 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -463,10 +463,7 @@
| _ => false
fun cunifsRemain c =
case c of
- L'.CUnif (loc, (L'.KRecord k, _), _, r as ref NONE) =>
- (r := SOME (L'.CRecord (k, []), loc);
- NONE)
- | L'.CUnif (loc, _, _, ref NONE) => SOME loc
+ L'.CUnif (loc, _, _, ref NONE) => SOME loc
| _ => NONE
val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
@@ -727,6 +724,8 @@
c others
end
+ val empties = ([], [], [], [], [], [])
+
val (unifs1, fs1, others1, unifs2, fs2, others2) =
case (unifs1, fs1, others1, unifs2, fs2, others2) of
orig as ([(_, r)], [], [], _, _, _) =>
@@ -737,7 +736,7 @@
orig
else
(r := SOME c;
- ([], [], [], [], [], []))
+ empties)
end
| orig as (_, _, _, [(_, r)], [], []) =>
let
@@ -747,42 +746,24 @@
orig
else
(r := SOME c;
- ([], [], [], [], [], []))
+ empties)
end
+ | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) =>
+ if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
+ let
+ val kr = (L'.KRecord k, dummy)
+ val u = cunif (loc, kr)
+ in
+ r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc);
+ r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc);
+ empties
+ end
+ else
+ orig
| orig => orig
- fun unifFields (fs, others, unifs) =
- case (fs, others, unifs) of
- ([], [], _) => ([], [], unifs)
- | (_, _, []) => (fs, others, [])
- | (_, _, (_, r) :: rest) =>
- let
- val r' = ref NONE
- val kr = (L'.KRecord k, dummy)
- val cr' = (L'.CUnif (dummy, kr, ("recd" ^ Int.toString (!recdCounter)), r'), dummy)
- val () = recdCounter := 1 + !recdCounter
-
- val prefix = case (fs, others) of
- ([], other :: others) =>
- List.foldl (fn (other, c) =>
- (L'.CConcat (c, other), dummy))
- other others
- | (fs, []) =>
- (L'.CRecord (k, fs), dummy)
- | (fs, others) =>
- List.foldl (fn (other, c) =>
- (L'.CConcat (c, other), dummy))
- (L'.CRecord (k, fs), dummy) others
- in
- r := SOME (L'.CConcat (prefix, cr'), dummy);
- ([], [], (cr', r') :: rest)
- end
-
- val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
- val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
-
(*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
- ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
+ ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
fun isGuessable (other, fs) =
(guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure);
@@ -803,8 +784,6 @@
(fs1, fs2, others1, others2)
| _ => (fs1, fs2, others1, others2)
- val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (unifs1, unifs2)
-
(*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
@@ -812,32 +791,16 @@
([], [], [], []) => true
| _ => false
val empty = (L'.CRecord (k, []), dummy)
-
- fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
in
case (unifs1, fs1, others1, unifs2, fs2, others2) of
- ([(_, r)], [], [], _, _, _) =>
- let
- val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
- in
- if occursCon r c then
- failure ()
- else
- r := SOME c
- end
- | (_, _, _, [(_, r)], [], []) =>
- let
- val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
- in
- if occursCon r c then
- failure ()
- else
- r := SOME c
- end
+ (_, [], [], [], [], []) =>
+ app (fn (_, r) => r := SOME empty) unifs1
+ | ([], [], [], _, [], []) =>
+ app (fn (_, r) => r := SOME empty) unifs2
| _ => if clear then
()
else
- failure ()
+ raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
(*before eprefaces "Summaries'" [("#1", p_summary env s1),
("#2", p_summary env s2)]*)
end
diff --git a/src/urweb.grm b/src/urweb.grm
index 5539feff..fb31bd18 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -1204,11 +1204,23 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
s (NOTAGSleft, NOTAGSright))
| tag DIVIDE GT (let
val pos = s (tagleft, GTright)
+
+ val cdata =
+ if #1 tag = "submit" orelse #1 tag = "dyn" then
+ let
+ val e = (EVar (["Basis"], "cdata", DontInfer), pos)
+ val e = (ECApp (e, (CWild (KWild, pos), pos)), pos)
+ in
+ (ECApp (e, (CRecord [], pos)), pos)
+ end
+ else
+ (EVar (["Basis"], "cdata", Infer), pos)
+
+ val cdata = (EApp (cdata,
+ (EPrim (Prim.String ""), pos)),
+ pos)
in
- (EApp (#2 tag,
- (EApp ((EVar (["Basis"], "cdata", Infer), pos),
- (EPrim (Prim.String ""), pos)),
- pos)), pos)
+ (EApp (#2 tag, cdata), pos)
end)
| tag GT xml END_TAG (let