summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 15:12:13 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 15:12:13 -0500
commit0351ba637e206cdf397c85e3cfe2cfcf52aa4c9d (patch)
tree163895f20f3556dd9ebb32a2deb09842eced212e
parentff76ba5e41d9a10ec59b181bee87d3fe65d61fdc (diff)
Demos compile again, with manual folders
-rw-r--r--demo/crud.ur88
-rw-r--r--demo/crud.urs2
-rw-r--r--demo/crud1.ur6
-rw-r--r--demo/crud2.ur4
-rw-r--r--demo/metaform.ur5
-rw-r--r--demo/metaform.urs1
-rw-r--r--demo/metaform1.ur1
-rw-r--r--demo/metaform2.ur1
-rw-r--r--demo/sum.ur4
-rw-r--r--demo/tcSum.ur8
-rw-r--r--lib/ur/top.ur12
-rw-r--r--lib/ur/top.urs30
-rw-r--r--src/elaborate.sml120
-rw-r--r--src/urweb.grm1
14 files changed, 168 insertions, 115 deletions
diff --git a/demo/crud.ur b/demo/crud.ur
index b365f69b..a6a65bb3 100644
--- a/demo/crud.ur
+++ b/demo/crud.ur
@@ -33,6 +33,8 @@ fun bool name = {Nam = name,
functor Make(M : sig
con cols :: {(Type * Type)}
constraint [Id] ~ cols
+ val fl : folder cols
+
val tab : sql_table ([Id = int] ++ map fstTT cols)
val title : string
@@ -50,12 +52,12 @@ functor Make(M : sig
(fn (fs : {T : $([Id = int] ++ map fstTT M.cols)}) => <xml>
<tr>
<td>{[fs.T.Id]}</td>
- {foldT2RX2 [fstTT] [colMeta] [tr]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] v col => <xml>
- <td>{col.Show v}</td>
- </xml>)
- [M.cols] (fs.T -- #Id) M.cols}
+ {foldRX2 [fstTT] [colMeta] [tr]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] v col => <xml>
+ <td>{col.Show v}</td>
+ </xml>)
+ [M.cols] M.fl (fs.T -- #Id) M.cols}
<td>
<a link={upd fs.T.Id}>[Update]</a>
<a link={confirm fs.T.Id}>[Delete]</a>
@@ -66,12 +68,12 @@ functor Make(M : sig
<table border={1}>
<tr>
<th>ID</th>
- {foldT2RX [colMeta] [tr]
+ {foldRX [colMeta] [tr]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
[[nm] ~ rest] col => <xml>
<th>{cdata col.Nam}</th>
</xml>)
- [M.cols] M.cols}
+ [M.cols] M.fl M.cols}
</tr>
{rows}
</table>
@@ -79,14 +81,14 @@ functor Make(M : sig
<br/><hr/><br/>
<form>
- {foldT2R [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map sndTT rest)) => <xml>
- <li> {cdata col.Nam}: {col.Widget [nm]}</li>
- {useMore acc}
- </xml>)
+ {foldR [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map sndTT rest)) => <xml>
+ <li> {cdata col.Nam}: {col.Widget [nm]}</li>
+ {useMore acc}
+ </xml>)
<xml/>
- [M.cols] M.cols}
+ [M.cols] M.fl M.cols}
<submit action={create}/>
</form>
@@ -95,13 +97,13 @@ functor Make(M : sig
and create (inputs : $(map sndTT M.cols)) =
id <- nextval seq;
dml (insert tab
- (foldT2R2 [sndTT] [colMeta]
- [fn cols => $(map (fn t :: (Type * Type) =>
- sql_exp [] [] [] t.1) cols)]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] =>
- fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)})
- {} [M.cols] inputs M.cols
+ (foldR2 [sndTT] [colMeta]
+ [fn cols => $(map (fn t :: (Type * Type) =>
+ sql_exp [] [] [] t.1) cols)]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] =>
+ fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)})
+ {} [M.cols] M.fl inputs M.cols
++ {Id = (SQL {[id]})}));
ls <- list ();
return <xml><body>
@@ -113,17 +115,17 @@ functor Make(M : sig
and upd (id : int) =
let
fun save (inputs : $(map sndTT M.cols)) =
- dml (update [map fstTT M.cols]
- (foldT2R2 [sndTT] [colMeta]
- [fn cols => $(map (fn t :: (Type * Type) =>
- sql_exp [T = [Id = int]
- ++ map fstTT M.cols]
- [] [] t.1) cols)]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] =>
- fn input col acc => acc ++ {nm =
- @sql_inject col.Inject (col.Parse input)})
- {} [M.cols] inputs M.cols)
+ dml (update [map fstTT M.cols] !
+ (foldR2 [sndTT] [colMeta]
+ [fn cols => $(map (fn t :: (Type * Type) =>
+ sql_exp [T = [Id = int]
+ ++ map fstTT M.cols]
+ [] [] t.1) cols)]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] =>
+ fn input col acc => acc ++ {nm =
+ @sql_inject col.Inject (col.Parse input)})
+ {} [M.cols] M.fl inputs M.cols)
tab (WHERE T.Id = {[id]}));
ls <- list ();
return <xml><body>
@@ -136,16 +138,16 @@ functor Make(M : sig
case fso : (Basis.option {Tab : $(map fstTT M.cols)}) of
None => return <xml><body>Not found!</body></xml>
| Some fs => return <xml><body><form>
- {foldT2R2 [fstTT] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] (v : t.1) (col : colMeta t)
- (acc : xml form [] (map sndTT rest)) =>
- <xml>
- <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
- {useMore acc}
- </xml>)
- <xml/>
- [M.cols] fs.Tab M.cols}
+ {foldR2 [fstTT] [colMeta] [fn cols :: {(Type * Type)} => xml form [] (map sndTT cols)]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] (v : t.1) (col : colMeta t)
+ (acc : xml form [] (map sndTT rest)) =>
+ <xml>
+ <li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
+ {useMore acc}
+ </xml>)
+ <xml/>
+ [M.cols] M.fl fs.Tab M.cols}
<submit action={save}/>
</form></body></xml>
diff --git a/demo/crud.urs b/demo/crud.urs
index 8c9cebcf..b240b7c1 100644
--- a/demo/crud.urs
+++ b/demo/crud.urs
@@ -16,6 +16,8 @@ val bool : string -> colMeta (bool, bool)
functor Make(M : sig
con cols :: {(Type * Type)}
constraint [Id] ~ cols
+ val fl : folder cols
+
val tab : sql_table ([Id = int] ++ map fstTT cols)
val title : string
diff --git a/demo/crud1.ur b/demo/crud1.ur
index 3849e822..65140035 100644
--- a/demo/crud1.ur
+++ b/demo/crud1.ur
@@ -9,4 +9,10 @@ open Crud.Make(struct
B = Crud.string "B",
C = Crud.float "C",
D = Crud.bool "D"}
+
+ val fl = Folder.cons [#A] [_] !
+ (Folder.cons [#B] [_] !
+ (Folder.cons [#C] [_] !
+ (Folder.cons [#D] [_] !
+ Folder.nil)))
end)
diff --git a/demo/crud2.ur b/demo/crud2.ur
index 1db376d4..f7adf29b 100644
--- a/demo/crud2.ur
+++ b/demo/crud2.ur
@@ -31,4 +31,8 @@ open Crud.Make(struct
Inject = _
}
}
+
+ val fl = Folder.cons [#Nam] [_] !
+ (Folder.cons [#Ready] [_] !
+ Folder.nil)
end)
diff --git a/demo/metaform.ur b/demo/metaform.ur
index ae1197f4..0e2e5ee3 100644
--- a/demo/metaform.ur
+++ b/demo/metaform.ur
@@ -1,5 +1,6 @@
functor Make (M : sig
con fs :: {Unit}
+ val fl : folder fs
val names : $(mapUT string fs)
end) = struct
@@ -8,7 +9,7 @@ functor Make (M : sig
(fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name value => <xml>
<li> {[name]} = {[value]}</li>
</xml>)
- [M.fs] M.names values}
+ [M.fs] M.fl M.names values}
</body></xml>
fun main () = return <xml><body>
@@ -20,7 +21,7 @@ functor Make (M : sig
{useMore acc}
</xml>)
<xml/>
- [M.fs] M.names}
+ [M.fs] M.fl M.names}
<submit action={handler}/>
</form>
</body></xml>
diff --git a/demo/metaform.urs b/demo/metaform.urs
index 7a3fa62e..505cb906 100644
--- a/demo/metaform.urs
+++ b/demo/metaform.urs
@@ -1,5 +1,6 @@
functor Make (M : sig
con fs :: {Unit}
+ val fl : folder fs
val names : $(mapUT string fs)
end) : sig
val main : unit -> transaction page
diff --git a/demo/metaform1.ur b/demo/metaform1.ur
index c6a4664d..2f3356fa 100644
--- a/demo/metaform1.ur
+++ b/demo/metaform1.ur
@@ -1,3 +1,4 @@
open Metaform.Make(struct
val names = {A = "Tic", B = "Tac", C = "Toe"}
+ val fl = Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! (Folder.cons [#C] [()] ! Folder.nil))
end)
diff --git a/demo/metaform2.ur b/demo/metaform2.ur
index 430a42f0..87d40b18 100644
--- a/demo/metaform2.ur
+++ b/demo/metaform2.ur
@@ -1,5 +1,6 @@
structure MM = Metaform.Make(struct
val names = {X = "x", Y = "y"}
+ val fl = Folder.cons [#X] [()] ! (Folder.cons [#Y] [()] ! Folder.nil)
end)
fun diversion () = return <xml><body>
diff --git a/demo/sum.ur b/demo/sum.ur
index 87b2967a..62954e20 100644
--- a/demo/sum.ur
+++ b/demo/sum.ur
@@ -1,7 +1,7 @@
-fun sum (fs ::: {Unit}) (fold : folder fs) (x : $(mapUT int fs)) =
+fun sum (fs ::: {Unit}) (fl : folder fs) (x : $(mapUT int fs)) =
foldUR [int] [fn _ => int]
(fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
- 0 [fs] fold x
+ 0 [fs] fl x
fun main () = return <xml><body>
{[sum Folder.nil {}]}<br/>
diff --git a/demo/tcSum.ur b/demo/tcSum.ur
index 53679116..e3340021 100644
--- a/demo/tcSum.ur
+++ b/demo/tcSum.ur
@@ -1,9 +1,9 @@
-fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (x : $(mapUT t fs)) =
+fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (fl : folder fs) (x : $(mapUT t fs)) =
foldUR [t] [fn _ => t]
(fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc)
- zero [fs] x
+ zero [fs] fl x
fun main () = return <xml><body>
- {[sum {A = 0, B = 1}]}<br/>
- {[sum {C = 2.1, D = 3.2, E = 4.3}]}
+ {[sum (Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! Folder.nil)) {A = 0, B = 1}]}<br/>
+ {[sum (Folder.cons [#D] [()] ! (Folder.cons [#C] [()] ! (Folder.cons [#E] [()] ! Folder.nil))) {C = 2.1, D = 3.2, E = 4.3}]}
</body></xml>
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index bfee2dfb..48ee4dd0 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -74,7 +74,7 @@ fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
(f : nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf -> tr rest -> tr ([nm] ++ rest))
- (i : tr []) (r ::: {Unit}) (fold : folder r)=
+ (i : tr []) (r :: {Unit}) (fold : folder r)=
fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
(fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
[[nm] ~ rest] r =>
@@ -85,7 +85,7 @@ fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
(f : nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
- (i : tr []) (r ::: {Unit}) (fold : folder r) =
+ (i : tr []) (r :: {Unit}) (fold : folder r) =
fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
(fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
[[nm] ~ rest] r1 r2 =>
@@ -105,7 +105,7 @@ fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) (r ::: {K}) (fold : folder r) =
+ (i : tr []) (r :: {K}) (fold : folder r) =
fold [fn r :: {K} => $(map tf r) -> tr r]
(fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest)
[[nm] ~ rest] r =>
@@ -116,7 +116,7 @@ fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type)
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) (r ::: {K}) (fold : folder r) =
+ (i : tr []) (r :: {K}) (fold : folder r) =
fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
(fn (nm :: Name) (t :: K) (rest :: {K})
(acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
@@ -143,7 +143,7 @@ fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
<xml/>
fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
- (q : sql_query tables exps) [tables ~ exps]
+ [tables ~ exps] (q : sql_query tables exps)
(f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
-> xml ctx [] []) =
query q
@@ -151,7 +151,7 @@ fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
<xml/>
fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
- (q : sql_query tables exps) [tables ~ exps]
+ [tables ~ exps] (q : sql_query tables exps)
(f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
-> transaction (xml ctx [] [])) =
query q
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index a9e5b6b3..65da4a07 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -46,25 +46,25 @@ val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
-> (nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf -> tr rest -> tr ([nm] ++ rest))
- -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
+ -> tr [] -> r :: {Unit} -> folder r -> $(mapUT tf r) -> tr r
val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
-> (nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
- -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+ -> tr [] -> r :: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
-> (nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> xml ctx [] [])
- -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+ -> r :: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
+ -> tr [] -> r :: {K} -> folder r -> $(map tf r) -> tr r
val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
-> tr :: ({K} -> Type)
@@ -72,34 +72,34 @@ val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-> tr []
- -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
+ -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> xml ctx [] [])
- -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
+ -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] []
val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> xml ctx [] [])
- -> r ::: {K} -> folder r
+ -> r :: {K} -> folder r
-> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
- -> sql_query tables exps
-> [tables ~ exps] =>
- ($(exps ++ map (fn fields :: {Type} => $fields) tables)
- -> xml ctx [] [])
- -> transaction (xml ctx [] [])
+ sql_query tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> xml ctx [] [])
+ -> transaction (xml ctx [] [])
val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
- -> sql_query tables exps
-> [tables ~ exps] =>
- ($(exps ++ map (fn fields :: {Type} => $fields) tables)
- -> transaction (xml ctx [] []))
- -> transaction (xml ctx [] [])
+ sql_query tables exps
+ -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)
+ -> transaction (xml ctx [] []))
+ -> transaction (xml ctx [] [])
val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
-> [tables ~ exps] =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 201b9150..c88edd44 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -839,7 +839,7 @@
in
unfold (r, c)
end
- handle _ => (TextIO.print "Guess failure!\n"; raise ex)
+ handle _ => raise ex
in
case (#1 c1, #1 c2) of
(L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
@@ -874,7 +874,28 @@
("c2All", p_con env c2All)];*)
case (c1, c2) of
- (L'.CUnit, L'.CUnit) => ()
+ (L'.CError, _) => ()
+ | (_, L'.CError) => ()
+
+ | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
+ if r1 = r2 then
+ ()
+ else
+ (unifyKinds env k1 k2;
+ r1 := SOME c2All)
+
+ | (L'.CUnif (_, _, _, r), _) =>
+ if occursCon r c2All then
+ err COccursCheckFailed
+ else
+ r := SOME c2All
+ | (_, L'.CUnif (_, _, _, r)) =>
+ if occursCon r c1All then
+ err COccursCheckFailed
+ else
+ r := SOME c1All
+
+ | (L'.CUnit, L'.CUnit) => ()
| (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
(unifyCons' env d1 d2;
@@ -933,29 +954,63 @@
((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
handle ListPair.UnequalLengths => err CIncompatible)
- | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
- unifyCons' env (L'.CProj (c1, n1), loc) c2All
- | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
- unifyCons' env c1All (L'.CProj (c2, n2), loc)
- | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
+ | (L'.CProj (c1, n1), _) =>
let
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' env (List.nth (us, n - 1)) c2All
- end
- | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
- let
- val us = map (fn k => cunif (loc, k)) ks
+ fun trySnd () =
+ case #1 (hnormCon env c2All) of
+ L'.CProj (c2, n2) =>
+ let
+ fun tryNormal () =
+ if n1 = n2 then
+ unifyCons' env c1 c2
+ else
+ err CIncompatible
+ in
+ case #1 (hnormCon env c2) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c2
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env c1All (List.nth (us, n2 - 1))
+ end
+ | _ => tryNormal ())
+ | _ => tryNormal ()
+ end
+ | _ => err CIncompatible
in
- r := SOME (L'.CTuple us, loc);
- unifyCons' env c1All (List.nth (us, n - 1))
+ case #1 (hnormCon env c1) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c1
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env (List.nth (us, n1 - 1)) c2All
+ end
+ | _ => trySnd ())
+ | _ => trySnd ()
end
- | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
- if n1 = n2 then
- unifyCons' env c1 c2
- else
- err CIncompatible
+
+ | (_, L'.CProj (c2, n2)) =>
+ (case #1 (hnormCon env c2) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c2
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env c1All (List.nth (us, n2 - 1))
+ end
+ | _ => err CIncompatible)
+ | _ => err CIncompatible)
| (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
(unifyKinds env dom1 dom2;
@@ -969,32 +1024,11 @@
| (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
unifyCons' (E.pushKRel env x) c1 c2
- | (L'.CError, _) => ()
- | (_, L'.CError) => ()
-
| (L'.CRecord _, _) => isRecord ()
| (_, L'.CRecord _) => isRecord ()
| (L'.CConcat _, _) => isRecord ()
| (_, L'.CConcat _) => isRecord ()
- | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
- if r1 = r2 then
- ()
- else
- (unifyKinds env k1 k2;
- r1 := SOME c2All)
-
- | (L'.CUnif (_, _, _, r), _) =>
- if occursCon r c2All then
- err COccursCheckFailed
- else
- r := SOME c2All
- | (_, L'.CUnif (_, _, _, r)) =>
- if occursCon r c1All then
- err COccursCheckFailed
- else
- r := SOME c1All
-
| _ => err CIncompatible
end
diff --git a/src/urweb.grm b/src/urweb.grm
index 43c9947a..1cd3e5c9 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -961,6 +961,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
val e = (EVar (["Basis"], "update", Infer), loc)
val e = (ECApp (e, (CWild (KRecord (KType, loc), loc), loc)), loc)
+ val e = (EDisjointApp e, loc)
val e = (EApp (e, (ERecord fsets, loc)), loc)
val e = (EApp (e, texp), loc)
in