diff options
| -rw-r--r-- | demo/crud.ur | 88 | ||||
| -rw-r--r-- | demo/crud.urs | 2 | ||||
| -rw-r--r-- | demo/crud1.ur | 6 | ||||
| -rw-r--r-- | demo/crud2.ur | 4 | ||||
| -rw-r--r-- | demo/metaform.ur | 5 | ||||
| -rw-r--r-- | demo/metaform.urs | 1 | ||||
| -rw-r--r-- | demo/metaform1.ur | 1 | ||||
| -rw-r--r-- | demo/metaform2.ur | 1 | ||||
| -rw-r--r-- | demo/sum.ur | 4 | ||||
| -rw-r--r-- | demo/tcSum.ur | 8 | ||||
| -rw-r--r-- | lib/ur/top.ur | 12 | ||||
| -rw-r--r-- | lib/ur/top.urs | 30 | ||||
| -rw-r--r-- | src/elaborate.sml | 120 | ||||
| -rw-r--r-- | src/urweb.grm | 1 |
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 |