Mercurial > urweb

comparison lib/top.urs @ 445:dfc8c991abd0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replace 'with' with '++'
author Adam Chlipala <adamc@hcoop.net>
date Fri, 31 Oct 2008 09:30:22 -0400
parents 19d7f79cd584
children b393c2fc80f8
comparison
equal deleted inserted replaced
444:f45f23ae20ed 445:dfc8c991abd0
2 2
3 con idT = fn t :: Type => t 3 con idT = fn t :: Type => t
4 con record = fn t :: {Type} => $t 4 con record = fn t :: {Type} => $t
5 con fstTT = fn t :: (Type * Type) => t.1 5 con fstTT = fn t :: (Type * Type) => t.1
6 con sndTT = fn t :: (Type * Type) => t.2 6 con sndTT = fn t :: (Type * Type) => t.2
7 con fstTTT = fn t :: (Type * Type * Type) => t.1
8 con sndTTT = fn t :: (Type * Type * Type) => t.2
9 con thdTTT = fn t :: (Type * Type * Type) => t.3
7 10
8 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => 11 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
9 [nm = f t] ++ acc) [] 12 [nm = f t] ++ acc) []
10 13
11 con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => 14 con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
12 [nm = f] ++ acc) [] 15 [nm = f] ++ acc) []
13 16
14 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => 17 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
15 [nm = f t] ++ acc) [] 18 [nm = f t] ++ acc) []
19
20 con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
21 [nm = f t] ++ acc) []
16 22
17 con ex = fn tf :: (Type -> Type) => 23 con ex = fn tf :: (Type -> Type) =>
18 res ::: Type -> (choice :: Type -> tf choice -> res) -> res 24 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
19 25
20 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf 26 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
53 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 59 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
54 -> fn [[nm] ~ rest] => 60 -> fn [[nm] ~ rest] =>
55 tf t -> tr rest -> tr ([nm = t] ++ rest)) 61 tf t -> tr rest -> tr ([nm = t] ++ rest))
56 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r 62 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
57 63
64 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
65 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
66 -> fn [[nm] ~ rest] =>
67 tf t -> tr rest -> tr ([nm = t] ++ rest))
68 -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r
69
58 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) 70 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
59 -> tr :: ({Type} -> Type) 71 -> tr :: ({Type} -> Type)
60 -> (nm :: Name -> t :: Type -> rest :: {Type} 72 -> (nm :: Name -> t :: Type -> rest :: {Type}
61 -> fn [[nm] ~ rest] => 73 -> fn [[nm] ~ rest] =>
62 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 74 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
69 -> fn [[nm] ~ rest] => 81 -> fn [[nm] ~ rest] =>
70 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 82 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
71 -> tr [] -> r :: {(Type * Type)} 83 -> tr [] -> r :: {(Type * Type)}
72 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r 84 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
73 85
86 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
87 -> tr :: ({(Type * Type * Type)} -> Type)
88 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
89 -> fn [[nm] ~ rest] =>
90 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
91 -> tr [] -> r :: {(Type * Type * Type)}
92 -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r
93
74 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} 94 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
75 -> (nm :: Name -> t :: Type -> rest :: {Type} 95 -> (nm :: Name -> t :: Type -> rest :: {Type}
76 -> fn [[nm] ~ rest] => 96 -> fn [[nm] ~ rest] =>
77 tf t -> xml ctx [] []) 97 tf t -> xml ctx [] [])
78 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] 98 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
80 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} 100 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
81 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 101 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
82 -> fn [[nm] ~ rest] => 102 -> fn [[nm] ~ rest] =>
83 tf t -> xml ctx [] []) 103 tf t -> xml ctx [] [])
84 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] 104 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
105
106 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
107 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
108 -> fn [[nm] ~ rest] =>
109 tf t -> xml ctx [] [])
110 -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] []
85 111
86 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} 112 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
87 -> (nm :: Name -> t :: Type -> rest :: {Type} 113 -> (nm :: Name -> t :: Type -> rest :: {Type}
88 -> fn [[nm] ~ rest] => 114 -> fn [[nm] ~ rest] =>
89 tf1 t -> tf2 t -> xml ctx [] []) 115 tf1 t -> tf2 t -> xml ctx [] [])
95 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 121 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
96 -> fn [[nm] ~ rest] => 122 -> fn [[nm] ~ rest] =>
97 tf1 t -> tf2 t -> xml ctx [] []) 123 tf1 t -> tf2 t -> xml ctx [] [])
98 -> r :: {(Type * Type)} 124 -> r :: {(Type * Type)}
99 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] 125 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
126
127
128 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
129 -> ctx :: {Unit}
130 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
131 -> fn [[nm] ~ rest] =>
132 tf1 t -> tf2 t -> xml ctx [] [])
133 -> r :: {(Type * Type * Type)}
134 -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] []
100 135
101 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 136 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
102 -> sql_query tables exps 137 -> sql_query tables exps
103 -> fn [tables ~ exps] => 138 -> fn [tables ~ exps] =>
104 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => 139 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>