diff lib/basis.urs @ 345:b85e6ba56618

Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents f55034419a07
children 58eeeb3cbf40
line wrap: on
line diff
--- a/lib/basis.urs	Thu Sep 18 15:01:01 2008 -0400
+++ b/lib/basis.urs	Sat Oct 04 15:50:28 2008 -0400
@@ -189,7 +189,7 @@
         -> 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 @@
         -> 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 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 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 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 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 *)