Mercurial > urweb
comparison 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 |
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] => |