summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 15:33:20 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 15:33:20 -0500
commite44434a592770472b58f4ba052404824442ace23 (patch)
tree6ec268a6e7aaa927f41c76e354e78ca55585f69a /src
parent7406aaad6e8b732009a0a80d48240fd9ec37a122 (diff)
"Hello world" compiles, after replacing type-level fold with map
Diffstat (limited to 'src')
-rw-r--r--src/core.sml2
-rw-r--r--src/core_print.sml2
-rw-r--r--src/core_util.sml10
-rw-r--r--src/corify.sml2
-rw-r--r--src/disjoint.sml33
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_ops.sml253
-rw-r--r--src/elab_print.sml2
-rw-r--r--src/elab_util.sml4
-rw-r--r--src/elaborate.sml176
-rw-r--r--src/elisp/urweb-defs.el4
-rw-r--r--src/elisp/urweb-mode.el2
-rw-r--r--src/expl.sml2
-rw-r--r--src/expl_print.sml2
-rw-r--r--src/expl_util.sml4
-rw-r--r--src/explify.sml2
-rw-r--r--src/monoize.sml2
-rw-r--r--src/reduce.sml13
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml2
-rw-r--r--src/urweb.grm4
-rw-r--r--src/urweb.lex1
22 files changed, 190 insertions, 336 deletions
diff --git a/src/core.sml b/src/core.sml
index c6e0cfef..d7a57493 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -54,7 +54,7 @@ datatype con' =
| CRecord of kind * (con * con) list
| CConcat of con * con
- | CFold of kind * kind
+ | CMap of kind * kind
| CUnit
diff --git a/src/core_print.sml b/src/core_print.sml
index 405ae14e..db8c3907 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -138,7 +138,7 @@ fun p_con' par env (c, _) =
string "++",
space,
p_con env c2])
- | CFold _ => string "fold"
+ | CMap _ => string "map"
| CUnit => string "()"
| CTuple cs => box [string "(",
diff --git a/src/core_util.sml b/src/core_util.sml
index a222dca4..e76da387 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -178,11 +178,11 @@ fun compare ((c1, _), (c2, _)) =
| (CConcat _, _) => LESS
| (_, CConcat _) => GREATER
- | (CFold (d1, r1), CFold (d2, r2)) =>
+ | (CMap (d1, r1), CMap (d2, r2)) =>
join (Kind.compare (d1, r2),
fn () => Kind.compare (r1, r2))
- | (CFold _, _) => LESS
- | (_, CFold _) => GREATER
+ | (CMap _, _) => LESS
+ | (_, CMap _) => GREATER
| (CUnit, CUnit) => EQUAL
| (CUnit, _) => LESS
@@ -261,12 +261,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
S.map2 (mfc ctx c2,
fn c2' =>
(CConcat (c1', c2'), loc)))
- | CFold (k1, k2) =>
+ | CMap (k1, k2) =>
S.bind2 (mfk k1,
fn k1' =>
S.map2 (mfk k2,
fn k2' =>
- (CFold (k1', k2'), loc)))
+ (CMap (k1', k2'), loc)))
| CUnit => S.return2 cAll
diff --git a/src/corify.sml b/src/corify.sml
index 2383ee03..c464e5a5 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -473,7 +473,7 @@ fun corifyCon st (c, loc) =
| L.CRecord (k, xcs) =>
(L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
| L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
- | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
+ | L.CMap (k1, k2) => (L'.CMap (corifyKind k1, corifyKind k2), loc)
| L.CUnit => (L'.CUnit, loc)
| L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
diff --git a/src/disjoint.sml b/src/disjoint.sml
index c6a8d50f..81023972 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -213,37 +213,8 @@ fun decomposeRow (env, denv) c =
("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
case #1 (#1 (hnormCon (env, denv) c)) of
CApp (
- (CApp (
- (CApp ((CFold (dom, ran), _), f), _),
- i), _),
- r) =>
- let
- val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
- val (env', v) = E.pushCNamed env' "v" dom NONE
- val (env', st) = E.pushCNamed env' "st" ran NONE
-
- val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
- (CUnit, loc))]), loc),
- (CNamed st, loc))
-
- val c' = (CApp (f, (CNamed nm, loc)), loc)
- val c' = (CApp (c', (CNamed v, loc)), loc)
- val c' = (CApp (c', (CNamed st, loc)), loc)
- val (ps, gs'') = decomposeRow (env', denv') c'
-
- fun covered p =
- case p of
- Unknown _ => false
- | Piece p =>
- case p of
- (NameN n, []) => n = nm
- | (RowN n, []) => n = st
- | _ => false
-
- val ps = List.filter (not o covered) ps
- in
- decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
- end
+ (CApp ((CMap _, _), _), _),
+ r) => decomposeRow' (r, (acc, gs))
| _ => default ()
end
in
diff --git a/src/elab.sml b/src/elab.sml
index 8e44c43c..ec8a910a 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -66,7 +66,7 @@ datatype con' =
| CRecord of kind * (con * con) list
| CConcat of con * con
- | CFold of kind * kind
+ | CMap of kind * kind
| CUnit
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 0648d704..c3e9274c 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -114,181 +114,98 @@ fun hnormCon env (cAll as (c, loc)) =
("sc", ElabPrint.p_con env sc)];*)
sc
end
- | c1' as CApp (c', i) =>
+ | c1' as CApp (c', f) =>
let
fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
in
case #1 (hnormCon env c') of
- CApp (c', f) =>
- (case #1 (hnormCon env c') of
- CFold ks =>
- (case #1 (hnormCon env c2) of
- CRecord (_, []) => hnormCon env i
- | CRecord (k, (x, c) :: rest) =>
- hnormCon env
- (CApp ((CApp ((CApp (f, x), loc), c), loc),
- (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
- (CRecord (k, rest), loc)), loc)), loc)
- | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
- let
- val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
-
- (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
- (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
- rest''), loc)), loc)*)
- in
- (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
- hnormCon env
- (CApp ((CApp ((CApp (f, x), loc), c), loc),
- (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
- rest''), loc)), loc)
- end
- | _ =>
- let
- fun cunif () =
- let
- val r = ref NONE
- in
- (r, (CUnif (loc, (KType, loc), "_", r), loc))
- end
-
- val (nmR, nm) = cunif ()
- val (vR, v) = cunif ()
- val (rR, r) = cunif ()
-
- val c = f
- val c = (CApp (c, nm), loc)
- val c = (CApp (c, v), loc)
- val c = (CApp (c, r), loc)
- fun unconstraint c =
- case hnormCon env c of
- (CDisjoint (_, _, _, c), _) => unconstraint c
- | c => c
- val c = unconstraint c
-
- fun tryDistributivity () =
- let
- fun distribute (c1, c2) =
- let
- val c = (CFold ks, loc)
- val c = (CApp (c, f), loc)
- val c = (CApp (c, i), loc)
-
- val c1 = (CApp (c, c1), loc)
- val c2 = (CApp (c, c2), loc)
- val c = (CConcat (c1, c2), loc)
- in
- hnormCon env c
- end
- in
- case (hnormCon env i, hnormCon env c2, hnormCon env c) of
- ((CRecord (_, []), _),
- (CConcat (arg1, arg2), _),
- (CConcat (c1, c2'), _)) =>
- (case (hnormCon env c1, hnormCon env c2') of
- ((CRecord (_, [(nm', v')]), _),
- (CUnif (_, _, _, rR'), _)) =>
- (case hnormCon env nm' of
- (CUnif (_, _, _, nmR'), _) =>
- if nmR' = nmR andalso rR' = rR then
- distribute (arg1, arg2)
- else
- default ()
- | _ => default ())
- | _ => default ())
- | _ => default ()
- end
-
- fun tryFusion () =
- let
- fun fuse (dom, new_v, r') =
- let
- val ran = #2 ks
-
- val f = (CApp (f, (CRel 2, loc)), loc)
- val f = (CApp (f, new_v), loc)
- val f = (CApp (f, (CRel 0, loc)), loc)
- val f = (CAbs ("acc", ran, f), loc)
- val f = (CAbs ("v", dom, f), loc)
- val f = (CAbs ("nm", (KName, loc), f), loc)
-
- val c = (CFold (dom, ran), loc)
- val c = (CApp (c, f), loc)
- val c = (CApp (c, i), loc)
- val c = (CApp (c, r'), loc)
- in
- hnormCon env c
- end
- in
- case #1 (hnormCon env c2) of
- CApp (f, r') =>
- (case #1 (hnormCon env f) of
- CApp (f, inner_i) =>
- (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of
- (CApp (f, inner_f), CRecord (_, [])) =>
- (case #1 (hnormCon env f) of
- CFold (dom, _) =>
- let
- val c = inner_f
- val c = (CApp (c, nm), loc)
- val c = (CApp (c, v), loc)
- val c = (CApp (c, r), loc)
- val c = unconstraint c
-
- (*val () = Print.prefaces "Onto something!"
- [("c", ElabPrint.p_con env cAll),
- ("c'", ElabPrint.p_con env c)]*)
-
- in
- case #1 (hnormCon env c) of
- CConcat (first, rest) =>
- (case (#1 (hnormCon env first),
- #1 (hnormCon env rest)) of
- (CRecord (_, [(nm', v')]),
- CUnif (_, _, _, rR')) =>
- (case #1 (hnormCon env nm') of
- CUnif (_, _, _, nmR') =>
- if rR' = rR andalso nmR' = nmR then
- (nmR := SOME (CRel 2, loc);
- vR := SOME (CRel 1, loc);
- rR := SOME (CError, loc);
- fuse (dom, v', r'))
- else
- tryDistributivity ()
- | _ => tryDistributivity ())
- | _ => tryDistributivity ())
- | _ => tryDistributivity ()
- end
- | _ => tryDistributivity ())
- | _ => tryDistributivity ())
- | _ => tryDistributivity ())
- | _ => tryDistributivity ()
- end
-
- in
- (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
- case (hnormCon env i, unconstraint c) of
- ((CRecord (_, []), _),
- (CConcat (c1, c2'), _)) =>
- (case (hnormCon env c1, hnormCon env c2') of
- ((CRecord (_, [(nm', v')]), _),
- (CUnif (_, _, _, rR'), _)) =>
- (case (hnormCon env nm', hnormCon env v') of
- ((CUnif (_, _, _, nmR'), _),
- (CUnif (_, _, _, vR'), _)) =>
- if nmR' = nmR andalso vR' = vR andalso rR' = rR then
- hnormCon env c2
- else
- tryFusion ()
- | _ => tryFusion ())
- | _ => tryFusion ())
- | _ => tryFusion ()
- end)
- | _ => default ())
+ CMap (ks as (k1, k2)) =>
+ (case #1 (hnormCon env c2) of
+ CRecord (_, []) => (CRecord (k2, []), loc)
+ | CRecord (_, (x, c) :: rest) =>
+ hnormCon env
+ (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+ (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
+ | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+ let
+ val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+ in
+ hnormCon env
+ (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+ (CApp (c1, rest''), loc)), loc)
+ end
+ | _ =>
+ let
+ fun unconstraint c =
+ case hnormCon env c of
+ (CDisjoint (_, _, _, c), _) => unconstraint c
+ | c => c
+
+ fun tryDistributivity () =
+ case hnormCon env c2 of
+ (CConcat (c1, c2'), _) =>
+ let
+ val c = (CMap ks, loc)
+ val c = (CApp (c, f), loc)
+
+ val c1 = (CApp (c, c1), loc)
+ val c2 = (CApp (c, c2'), loc)
+ val c = (CConcat (c1, c2), loc)
+ in
+ hnormCon env c
+ end
+ | _ => default ()
+
+ fun tryFusion () =
+ case #1 (hnormCon env c2) of
+ CApp (f', r') =>
+ (case #1 (hnormCon env f') of
+ CApp (f', inner_f) =>
+ (case #1 (hnormCon env f') of
+ CMap (dom, _) =>
+ let
+ val f' = (CApp (inner_f, (CRel 0, loc)), loc)
+ val f' = (CApp (f, f'), loc)
+ val f' = (CAbs ("v", dom, f'), loc)
+
+ val c = (CMap (dom, k2), loc)
+ val c = (CApp (c, f'), loc)
+ val c = (CApp (c, r'), loc)
+ in
+ hnormCon env c
+ end
+ | _ => tryDistributivity ())
+ | _ => tryDistributivity ())
+ | _ => tryDistributivity ()
+
+ fun tryIdentity () =
+ let
+ fun cunif () =
+ let
+ val r = ref NONE
+ in
+ (r, (CUnif (loc, (KType, loc), "_", r), loc))
+ end
+
+ val (vR, v) = cunif ()
+
+ val c = (CApp (f, v), loc)
+ in
+ case unconstraint c of
+ (CUnif (_, _, _, vR'), _) =>
+ if vR' = vR then
+ hnormCon env c2
+ else
+ tryFusion ()
+ | _ => tryFusion ()
+ end
+ in
+ tryIdentity ()
+ end)
| _ => default ()
end
| c1' => (CApp ((c1', loc), hnormCon env c2), loc))
-
+
| CConcat (c1, c2) =>
(case (hnormCon env c1, hnormCon env c2) of
((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 0e6c9767..098c9259 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -167,7 +167,7 @@ fun p_con' par env (c, _) =
string "++",
space,
p_con env c2])
- | CFold _ => string "fold"
+ | CMap _ => string "map"
| CUnit => string "()"
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 6e78907d..f052a06d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -168,12 +168,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
S.map2 (mfc ctx c2,
fn c2' =>
(CConcat (c1', c2'), loc)))
- | CFold (k1, k2) =>
+ | CMap (k1, k2) =>
S.bind2 (mfk k1,
fn k1' =>
S.map2 (mfk k2,
fn k2' =>
- (CFold (k1', k2'), loc)))
+ (CMap (k1', k2'), loc)))
| CUnit => S.return2 cAll
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 39cb85b2..fa97bdf8 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -182,13 +182,10 @@
| L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
| L.KWild => kunif loc
- fun foldKind (dom, ran, loc)=
- (L'.KArrow ((L'.KArrow ((L'.KName, loc),
- (L'.KArrow (dom,
- (L'.KArrow (ran, ran), loc)), loc)), loc),
- (L'.KArrow (ran,
- (L'.KArrow ((L'.KRecord dom, loc),
- ran), loc)), loc)), loc)
+ fun mapKind (dom, ran, loc)=
+ (L'.KArrow ((L'.KArrow (dom, ran), loc),
+ (L'.KArrow ((L'.KRecord dom, loc),
+ (L'.KRecord ran, loc)), loc)), loc)
fun hnormKind (kAll as (k, _)) =
case k of
@@ -355,13 +352,13 @@
((L'.CConcat (c1', c2'), loc), k,
D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
end
- | L.CFold =>
+ | L.CMap =>
let
val dom = kunif loc
val ran = kunif loc
in
- ((L'.CFold (dom, ran), loc),
- foldKind (dom, ran, loc),
+ ((L'.CMap (dom, ran), loc),
+ mapKind (dom, ran, loc),
[])
end
@@ -489,7 +486,7 @@
| L'.CRecord (k, _) => (L'.KRecord k, loc)
| L'.CConcat (c, _) => kindof env c
- | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
+ | L'.CMap (dom, ran) => mapKind (dom, ran, loc)
| L'.CUnit => (L'.KUnit, loc)
@@ -504,41 +501,21 @@
val hnormCon = D.hnormCon
- datatype con_summary =
- Nil
- | Cons
- | Unknown
-
- fun compatible cs =
- case cs of
- (Unknown, _) => false
- | (_, Unknown) => false
- | (s1, s2) => s1 = s2
-
- fun summarizeCon (env, denv) c =
+ fun deConstraintCon (env, denv) c =
let
val (c, gs) = hnormCon (env, denv) c
in
case #1 c of
- L'.CRecord (_, []) => (Nil, gs)
- | L'.CRecord (_, _ :: _) => (Cons, gs)
- | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
- | L'.CDisjoint (_, _, _, c) =>
+ L'.CDisjoint (_, _, _, c) =>
let
- val (s, gs') = summarizeCon (env, denv) c
+ val (c', gs') = deConstraintCon (env, denv) c
in
- (s, gs @ gs')
+ (c', gs @ gs')
end
- | _ => (Unknown, gs)
+ | _ => (c, gs)
end
- fun p_con_summary s =
- Print.PD.string (case s of
- Nil => "Nil"
- | Cons => "Cons"
- | Unknown => "Unknown")
-
- exception SummaryFailure
+ exception GuessFailure
fun isUnitCon env (c, loc) =
case c of
@@ -574,7 +551,7 @@
| L'.CRecord _ => false
| L'.CConcat _ => false
- | L'.CFold _ => false
+ | L'.CMap _ => false
| L'.CUnit => true
@@ -720,14 +697,14 @@
fun isGuessable (other, fs) =
let
- val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
+ val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure)
in
List.all (fn (loc, env, denv, c1, c2) =>
case D.prove env denv (c1, c2, loc) of
[] => true
| _ => false) gs
end
- handle SummaryFailure => false
+ handle GuessFailure => false
val (fs1, fs2, others1, others2) =
case (fs1, fs2, others1, others2) of
@@ -783,79 +760,68 @@
("#2", p_summary env s2)]*)
end
- and guessFold (env, denv) (c1, c2, gs, ex) =
+ and guessMap (env, denv) (c1, c2, gs, ex) =
let
val loc = #2 c1
- fun unfold (dom, ran, f, i, r, c) =
+ fun unfold (dom, ran, f, r, c) =
let
- val nm = cunif (loc, (L'.KName, loc))
- val v =
- case dom of
- (L'.KUnit, _) => (L'.CUnit, loc)
- | _ => cunif (loc, dom)
- val rest = cunif (loc, (L'.KRecord dom, loc))
- val acc = (L'.CFold (dom, ran), loc)
- val acc = (L'.CApp (acc, f), loc)
- val acc = (L'.CApp (acc, i), loc)
- val acc = (L'.CApp (acc, rest), loc)
-
- val (iS, gs3) = summarizeCon (env, denv) i
-
- val app = (L'.CApp (f, nm), loc)
- val app = (L'.CApp (app, v), loc)
- val app = (L'.CApp (app, acc), loc)
- val (appS, gs4) = summarizeCon (env, denv) app
-
- val (cS, gs5) = summarizeCon (env, denv) c
- in
- (*prefaces "Summaries" [("iS", p_con_summary iS),
- ("appS", p_con_summary appS),
- ("cS", p_con_summary cS)];*)
-
- if compatible (iS, appS) then
- raise ex
- else if compatible (cS, iS) then
+ fun unfold (r, c) =
let
- (*val () = prefaces "Same?" [("i", p_con env i),
- ("c", p_con env c)]*)
- val gs6 = unifyCons (env, denv) i c
- (*val () = TextIO.print "Yes!\n"*)
-
- val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+ val (c', gs1) = deConstraintCon (env, denv) c
in
- gs @ gs3 @ gs5 @ gs6 @ gs7
- end
- else if compatible (cS, appS) then
- let
- (*val () = prefaces "Same?" [("app", p_con env app),
- ("c", p_con env c),
- ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
- val gs6 = unifyCons (env, denv) app c
- (*val () = TextIO.print "Yes!\n"*)
-
- val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
- val concat = (L'.CConcat (singleton, rest), loc)
- (*val () = prefaces "Pre-crew" [("r", p_con env r),
- ("concat", p_con env concat)]*)
- val gs7 = unifyCons (env, denv) r concat
- in
- (*prefaces "The crew" [("nm", p_con env nm),
- ("v", p_con env v),
- ("rest", p_con env rest)];*)
+ case #1 c' of
+ L'.CRecord (_, []) =>
+ let
+ val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+ in
+ gs1 @ gs2
+ end
+ | L'.CRecord (_, [(x, v)]) =>
+ let
+ val v' = case dom of
+ (L'.KUnit, _) => (L'.CUnit, loc)
+ | _ => cunif (loc, dom)
+ val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc)
- gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
+ val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
+ in
+ gs1 @ gs2 @ gs3
+ end
+ | L'.CRecord (_, (x, v) :: rest) =>
+ let
+ val r1 = cunif (loc, (L'.KRecord dom, loc))
+ val r2 = cunif (loc, (L'.KRecord dom, loc))
+ val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+
+ val gs3 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
+ val gs4 = unfold (r2, (L'.CRecord (ran, rest), loc))
+ in
+ gs1 @ gs2 @ gs3 @ gs4
+ end
+ | L'.CConcat (c1', c2') =>
+ let
+ val r1 = cunif (loc, (L'.KRecord dom, loc))
+ val r2 = cunif (loc, (L'.KRecord dom, loc))
+ val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+
+ val gs3 = unfold (r1, c1')
+ val gs4 = unfold (r2, c2')
+ in
+ gs1 @ gs2 @ gs3 @ gs4
+ end
+ | _ => raise ex
end
- else
- raise ex
+ in
+ unfold (r, c)
end
handle _ => raise ex
in
case (#1 c1, #1 c2) of
- (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
- unfold (dom, ran, f, i, r, c2)
- | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
- unfold (dom, ran, f, i, r, c1)
+ (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
+ unfold (dom, ran, f, r, c2)
+ | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
+ unfold (dom, ran, f, r, c1)
| _ => raise ex
end
@@ -890,7 +856,7 @@
(Time.- (Time.now (), befor)))))];*)
gs1 @ gs2 @ gs3
end
- handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
+ handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
end
and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
@@ -1017,7 +983,7 @@
(r := SOME c1All;
[])
- | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
+ | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
(unifyKinds dom1 dom2;
unifyKinds ran1 ran2;
[])
@@ -2740,7 +2706,7 @@ fun positive self =
| CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
| CConcat (c1, c2) => none c1 andalso none c2
- | CFold => true
+ | CMap => true
| CUnit => true
@@ -2766,7 +2732,7 @@ fun positive self =
| CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
| CConcat (c1, c2) => pos c1 andalso pos c2
- | CFold => true
+ | CMap => true
| CUnit => true
diff --git a/src/elisp/urweb-defs.el b/src/elisp/urweb-defs.el
index 5551b7a2..e1382692 100644
--- a/src/elisp/urweb-defs.el
+++ b/src/elisp/urweb-defs.el
@@ -107,7 +107,7 @@ notion of \"the end of an outline\".")
"if" "then" "else" "case" "of" "fn" "fun" "val" "and"
"datatype" "type" "open" "include"
urweb-module-head-syms
- "con" "fold" "where" "extern" "constraint" "constraints"
+ "con" "map" "where" "extern" "constraint" "constraints"
"table" "sequence" "class" "cookie")
"Symbols starting an sexp.")
@@ -192,7 +192,7 @@ for all symbols and in all lines starting with the given symbol."
"The starters of new expressions.")
(defconst urweb-exptrail-syms
- '("if" "then" "else" "case" "of" "fn" "with" "fold"))
+ '("if" "then" "else" "case" "of" "fn" "with" "map"))
(defconst urweb-pipeheads
'("|" "of" "fun" "fn" "and" "datatype")
diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el
index 223006fc..e7615cc3 100644
--- a/src/elisp/urweb-mode.el
+++ b/src/elisp/urweb-mode.el
@@ -133,7 +133,7 @@ See doc for the variable `urweb-mode-info'."
(defconst urweb-keywords-regexp
(urweb-syms-re "and" "case" "class" "con" "constraint" "constraints"
- "datatype" "else" "end" "extern" "fn" "fold"
+ "datatype" "else" "end" "extern" "fn" "map"
"fun" "functor" "if" "include"
"of" "open" "let" "in"
"rec" "sequence" "sig" "signature" "cookie"
diff --git a/src/expl.sml b/src/expl.sml
index cce0fc22..c0d291b5 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -54,7 +54,7 @@ datatype con' =
| CRecord of kind * (con * con) list
| CConcat of con * con
- | CFold of kind * kind
+ | CMap of kind * kind
| CUnit
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 2ce0c5e2..7044bfa2 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -149,7 +149,7 @@ fun p_con' par env (c, _) =
string "++",
space,
p_con env c2])
- | CFold _ => string "fold"
+ | CMap _ => string "map"
| CUnit => string "()"
| CTuple cs => box [string "(",
diff --git a/src/expl_util.sml b/src/expl_util.sml
index d2073a23..a2b5f2f6 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -145,12 +145,12 @@ fun mapfoldB {kind = fk, con = fc, bind} =
S.map2 (mfc ctx c2,
fn c2' =>
(CConcat (c1', c2'), loc)))
- | CFold (k1, k2) =>
+ | CMap (k1, k2) =>
S.bind2 (mfk k1,
fn k1' =>
S.map2 (mfk k2,
fn k2' =>
- (CFold (k1', k2'), loc)))
+ (CMap (k1', k2'), loc)))
| CUnit => S.return2 cAll
diff --git a/src/explify.sml b/src/explify.sml
index a10037ef..a4eab0ba 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -63,7 +63,7 @@ fun explifyCon (c, loc) =
| L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
| L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
- | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
+ | L.CMap (dom, ran) => (L'.CMap (explifyKind dom, explifyKind ran), loc)
| L.CUnit => (L'.CUnit, loc)
diff --git a/src/monoize.sml b/src/monoize.sml
index 4efa2fea..898d3e61 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -206,7 +206,7 @@ fun monoType env =
| L.CRecord _ => poly ()
| L.CConcat _ => poly ()
- | L.CFold _ => poly ()
+ | L.CMap _ => poly ()
| L.CUnit => poly ()
| L.CTuple _ => poly ()
diff --git a/src/reduce.sml b/src/reduce.sml
index b428c01f..949b2a6d 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -103,14 +103,13 @@ fun conAndExp (namedC, namedE) =
CAbs (_, _, b) =>
con (KnownC c2 :: deKnown env) b
- | CApp ((CApp ((CFold _, _), f), _), i) =>
+ | CApp ((CMap (dom, ran), _), f) =>
(case #1 c2 of
- CRecord (_, []) => i
- | CRecord (k, (x, c) :: rest) =>
+ CRecord (_, []) => (CRecord (ran, []), loc)
+ | CRecord (_, (x, c) :: rest) =>
con (deKnown env)
- (CApp ((CApp ((CApp (f, x), loc), c), loc),
- (CApp (c1,
- (CRecord (k, rest), loc)), loc)), loc)
+ (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
+ (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
| _ => (CApp (c1, c2), loc))
| _ => (CApp (c1, c2), loc)
@@ -130,7 +129,7 @@ fun conAndExp (namedC, namedE) =
(CRecord (k, xcs1 @ xcs2), loc)
| _ => (CConcat (c1, c2), loc)
end
- | CFold _ => all
+ | CMap _ => all
| CUnit => all
diff --git a/src/source.sml b/src/source.sml
index a5c86f66..d70d0f5d 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -60,7 +60,7 @@ datatype con' =
| CRecord of (con * con) list
| CConcat of con * con
- | CFold
+ | CMap
| CUnit
diff --git a/src/source_print.sml b/src/source_print.sml
index d6568efe..148157c2 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -139,7 +139,7 @@ fun p_con' par (c, _) =
string "++",
space,
p_con c2])
- | CFold => string "fold"
+ | CMap => string "map"
| CUnit => string "()"
diff --git a/src/urweb.grm b/src/urweb.grm
index 5f2c0575..d425caec 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -184,7 +184,7 @@ fun tagIn bt =
| LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
| EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
| PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
- | CON | LTYPE | VAL | REC | AND | FUN | FOLD | UNIT | KUNIT | CLASS
+ | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS
| DATATYPE | OF
| TYPE | NAME
| ARROW | LARROW | DARROW | STAR | SEMI
@@ -681,7 +681,7 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
| path DOT INT (CProj ((CVar path, s (pathleft, pathright)), Int64.toInt INT),
s (pathleft, INTright))
| UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
- | FOLD (CFold, s (FOLDleft, FOLDright))
+ | MAP (CMap, s (MAPleft, MAPright))
| UNIT (CUnit, s (UNITleft, UNITright))
| LPAREN ctuplev RPAREN (CTuple ctuplev, s (LPARENleft, RPARENright))
diff --git a/src/urweb.lex b/src/urweb.lex
index aef68ad1..29e07194 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -290,6 +290,7 @@ notags = [^<{\n]+;
<INITIAL> "and" => (Tokens.AND (pos yypos, pos yypos + size yytext));
<INITIAL> "fun" => (Tokens.FUN (pos yypos, pos yypos + size yytext));
<INITIAL> "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext));
+<INITIAL> "map" => (Tokens.MAP (pos yypos, pos yypos + size yytext));
<INITIAL> "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
<INITIAL> "case" => (Tokens.CASE (pos yypos, pos yypos + size yytext));
<INITIAL> "if" => (Tokens.IF (pos yypos, pos yypos + size yytext));