Mercurial > urweb
diff lib/top.urs @ 445:dfc8c991abd0
Replace 'with' with '++'
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 31 Oct 2008 09:30:22 -0400 |
parents | 19d7f79cd584 |
children | b393c2fc80f8 |
line wrap: on
line diff
--- a/lib/top.urs Thu Oct 30 17:07:34 2008 -0400 +++ b/lib/top.urs Fri Oct 31 09:30:22 2008 -0400 @@ -4,6 +4,9 @@ con record = fn t :: {Type} => $t con fstTT = fn t :: (Type * Type) => t.1 con sndTT = fn t :: (Type * Type) => t.2 +con fstTTT = fn t :: (Type * Type * Type) => t.1 +con sndTTT = fn t :: (Type * Type * Type) => t.2 +con thdTTT = fn t :: (Type * Type * Type) => t.3 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => [nm = f t] ++ acc) [] @@ -14,6 +17,9 @@ con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => [nm = f t] ++ acc) [] +con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -55,6 +61,12 @@ tf t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r +val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r + val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) -> (nm :: Name -> t :: Type -> rest :: {Type} @@ -71,6 +83,14 @@ -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r +val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) + -> tr :: ({(Type * Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type * Type)} + -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r + val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -83,6 +103,12 @@ tf t -> xml ctx [] []) -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] +val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] [] + val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -98,6 +124,15 @@ -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] + +val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) + -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r :: {(Type * Type * Type)} + -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] + val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> fn [tables ~ exps] =>