Merge CDisjoint and TDisjoint

3 files changed, 31 insertions, 31 deletions

diff --git a/lib/basis.urs b/lib/basis.urs
index 3fe80d38..3dec0461 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -189,7 +189,7 @@ val bind : t1 ::: Type -> t2 ::: Type
         -> transaction t2
 
 val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
-        -> state ::: Type
+        => state ::: Type
         -> sql_query tables exps
         -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
                 -> state
@@ -210,7 +210,7 @@ val insert : fields ::: {Type}
         -> dml
 
 val update : changed :: {Type} -> unchanged ::: {Type} -> changed ~ unchanged
-        -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
+        => $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
                 [nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed)
         -> sql_table (changed ++ unchanged)
         -> sql_exp [T = changed ++ unchanged] [] [] bool
@@ -235,22 +235,22 @@ con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
 con xml :: {Unit} -> {Type} -> {Type} -> Type
 val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
 val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent
-        -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
+        => ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
         -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner
-        -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
-        -> $attrsGiven
+        => bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
+        => $attrsGiven
         -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter
         -> xml ctxInner useInner bindInner
         -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
 val join : ctx ::: {Unit} 
         -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
-        -> use1 ~ bind1 -> bind1 ~ bind2
-        -> xml ctx use1 bind1
+        -> use1 ~ bind1 => bind1 ~ bind2
+        => xml ctx use1 bind1
         -> xml ctx (use1 ++ bind1) bind2
         -> xml ctx use1 (bind1 ++ bind2)
 val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type}
         -> use1 ~ use2
-        -> xml ctx use1 bind
+        => xml ctx use1 bind
         -> xml ctx (use1 ++ use2) bind
 
 con xhtml = xml [Html]
@@ -272,9 +272,9 @@ val head : unit -> tag [] html head [] []
 val title : unit -> tag [] head [] [] []
 
 val body : unit -> tag [] html body [] []
-con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
+con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
         -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
-con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
+con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
         -> tag attrs ([Body] ++ ctx) [] [] []
 
 val br : bodyTagStandalone []
@@ -289,12 +289,12 @@ val li : bodyTag []
 
 val a : bodyTag [Link = transaction page]
 
-val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type}
+val lform : ctx ::: {Unit} -> [Body] ~ ctx => bind ::: {Type}
         -> xml form [] bind
         -> xml ([Body] ++ ctx) [] []
 con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} =>
         ctx ::: {Unit} -> [LForm] ~ ctx
-        -> nm :: Name -> unit
+        => nm :: Name -> unit
         -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty]
 val textbox : lformTag string [] [Value = string]
 val password : lformTag string [] []
@@ -311,7 +311,7 @@ val lselect : lformTag string select []
 val loption : unit -> tag [Value = string] select [] [] []
 
 val submit : ctx ::: {Unit} -> [LForm] ~ ctx
-        -> use ::: {Type} -> unit
+        => use ::: {Type} -> unit
         -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []
 
 (*** Tables *)
diff --git a/lib/top.ur b/lib/top.ur
index 990a18fa..e7c4a988 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -22,7 +22,7 @@ fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = c
 
 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) =>
@@ -32,7 +32,7 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
 
 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) =>
@@ -42,7 +42,7 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
 
 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
@@ -52,7 +52,7 @@ fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
 
 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         (i : tr []) =
         fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) =>
@@ -62,7 +62,7 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :
 
 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> xml ctx [] []) =
+                => tf t -> xml ctx [] []) =
         foldTR [tf] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
                         [[nm] ~ rest] =>
@@ -71,7 +71,7 @@ fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
 
 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> xml ctx [] []) =
+                => tf t -> xml ctx [] []) =
         foldT2R [tf] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
                         [[nm] ~ rest] =>
@@ -80,7 +80,7 @@ fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
 
 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] []) =
+                => tf1 t -> tf2 t -> xml ctx [] []) =
         foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
                         [[nm] ~ rest] =>
@@ -89,7 +89,7 @@ fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
 
 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit})
         (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] []) =
+                => tf1 t -> tf2 t -> xml ctx [] []) =
         foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
                 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
                         [[nm] ~ rest] =>
diff --git a/lib/top.urs b/lib/top.urs
index add94578..684ebfb8 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -22,52 +22,52 @@ val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
 
 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
 
 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
 
 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
 
 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
         -> tr :: ({(Type * Type)} -> Type)
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+                => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
         -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
 
 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf t -> xml ctx [] [])
+                => tf t -> xml ctx [] [])
         -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
 
 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf t -> xml ctx [] [])
+                => tf t -> xml ctx [] [])
         -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
 
 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] [])
+                => tf1 t -> tf2 t -> xml ctx [] [])
         -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
 
 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit}
         -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
-                -> tf1 t -> tf2 t -> xml ctx [] [])
+                => tf1 t -> tf2 t -> xml ctx [] [])
         -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
 
 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
         -> sql_query tables exps -> tables ~ exps
-        -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+        => ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
                 -> xml ctx [] [])
         -> transaction (xml ctx [] [])
 
 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} -> sql_query tables exps
         -> tables ~ exps
-        -> transaction
+        => transaction
                 (option $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables))