Mercurial > urweb

comparison lib/ur/top.urs @ 621:8998114760c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
"Hello world" compiles, after replacing type-level fold with map
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 15:33:20 -0500
parents 1d34d916c206
children 588b9d16b00a
comparison
equal deleted inserted replaced
620:d828b143e147 621:8998114760c1
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 7 con fstTTT = fn t :: (Type * Type * Type) => t.1
8 con sndTTT = fn t :: (Type * Type * Type) => t.2 8 con sndTTT = fn t :: (Type * Type * Type) => t.2
9 con thdTTT = fn t :: (Type * Type * Type) => t.3 9 con thdTTT = fn t :: (Type * Type * Type) => t.3
10 10
11 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => 11 con mapUT = fn f :: Type => map (fn _ :: Unit => f)
12 [nm = f t] ++ acc) []
13
14 con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
15 [nm = f] ++ acc) []
16
17 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ 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) []
22 12
23 con ex = fn tf :: (Type -> Type) => 13 con ex = fn tf :: (Type -> Type) =>
24 res ::: Type -> (choice :: Type -> tf choice -> res) -> res 14 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
25 15
26 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf 16 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
51 41
52 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) 42 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
53 -> (nm :: Name -> t :: Type -> rest :: {Type} 43 -> (nm :: Name -> t :: Type -> rest :: {Type}
54 -> fn [[nm] ~ rest] => 44 -> fn [[nm] ~ rest] =>
55 tf t -> tr rest -> tr ([nm = t] ++ rest)) 45 tf t -> tr rest -> tr ([nm = t] ++ rest))
56 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r 46 -> tr [] -> r :: {Type} -> $(map tf r) -> tr r
57 47
58 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) 48 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
59 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 49 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
60 -> fn [[nm] ~ rest] => 50 -> fn [[nm] ~ rest] =>
61 tf t -> tr rest -> tr ([nm = t] ++ rest)) 51 tf t -> tr rest -> tr ([nm = t] ++ rest))
62 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r 52 -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r
63 53
64 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) 54 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
65 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} 55 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
66 -> fn [[nm] ~ rest] => 56 -> fn [[nm] ~ rest] =>
67 tf t -> tr rest -> tr ([nm = t] ++ rest)) 57 tf t -> tr rest -> tr ([nm = t] ++ rest))
68 -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r 58 -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r
69 59
70 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) 60 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
71 -> tr :: ({Type} -> Type) 61 -> tr :: ({Type} -> Type)
72 -> (nm :: Name -> t :: Type -> rest :: {Type} 62 -> (nm :: Name -> t :: Type -> rest :: {Type}
73 -> fn [[nm] ~ rest] => 63 -> fn [[nm] ~ rest] =>
74 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 64 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
75 -> tr [] 65 -> tr []
76 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r 66 -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r
77 67
78 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) 68 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
79 -> tr :: ({(Type * Type)} -> Type) 69 -> tr :: ({(Type * Type)} -> Type)
80 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 70 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
81 -> fn [[nm] ~ rest] => 71 -> fn [[nm] ~ rest] =>
82 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 72 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
83 -> tr [] -> r :: {(Type * Type)} 73 -> tr [] -> r :: {(Type * Type)}
84 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r 74 -> $(map tf1 r) -> $(map tf2 r) -> tr r
85 75
86 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) 76 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
87 -> tr :: ({(Type * Type * Type)} -> Type) 77 -> tr :: ({(Type * Type * Type)} -> Type)
88 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} 78 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
89 -> fn [[nm] ~ rest] => 79 -> fn [[nm] ~ rest] =>
90 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 80 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
91 -> tr [] -> r :: {(Type * Type * Type)} 81 -> tr [] -> r :: {(Type * Type * Type)}
92 -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r 82 -> $(map tf1 r) -> $(map tf2 r) -> tr r
93 83
94 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} 84 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
95 -> (nm :: Name -> t :: Type -> rest :: {Type} 85 -> (nm :: Name -> t :: Type -> rest :: {Type}
96 -> fn [[nm] ~ rest] => 86 -> fn [[nm] ~ rest] =>
97 tf t -> xml ctx [] []) 87 tf t -> xml ctx [] [])
98 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] 88 -> r :: {Type} -> $(map tf r) -> xml ctx [] []
99 89
100 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} 90 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
101 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 91 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
102 -> fn [[nm] ~ rest] => 92 -> fn [[nm] ~ rest] =>
103 tf t -> xml ctx [] []) 93 tf t -> xml ctx [] [])
104 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] 94 -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] []
105 95
106 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} 96 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
107 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} 97 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
108 -> fn [[nm] ~ rest] => 98 -> fn [[nm] ~ rest] =>
109 tf t -> xml ctx [] []) 99 tf t -> xml ctx [] [])
110 -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] [] 100 -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] []
111 101
112 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} 102 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
113 -> (nm :: Name -> t :: Type -> rest :: {Type} 103 -> (nm :: Name -> t :: Type -> rest :: {Type}
114 -> fn [[nm] ~ rest] => 104 -> fn [[nm] ~ rest] =>
115 tf1 t -> tf2 t -> xml ctx [] []) 105 tf1 t -> tf2 t -> xml ctx [] [])
116 -> r :: {Type} 106 -> r :: {Type}
117 -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] 107 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
118 108
119 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) 109 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
120 -> ctx :: {Unit} 110 -> ctx :: {Unit}
121 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 111 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
122 -> fn [[nm] ~ rest] => 112 -> fn [[nm] ~ rest] =>
123 tf1 t -> tf2 t -> xml ctx [] []) 113 tf1 t -> tf2 t -> xml ctx [] [])
124 -> r :: {(Type * Type)} 114 -> r :: {(Type * Type)}
125 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] 115 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
126 116
127 117
128 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) 118 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
129 -> ctx :: {Unit} 119 -> ctx :: {Unit}
130 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} 120 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
131 -> fn [[nm] ~ rest] => 121 -> fn [[nm] ~ rest] =>
132 tf1 t -> tf2 t -> xml ctx [] []) 122 tf1 t -> tf2 t -> xml ctx [] [])
133 -> r :: {(Type * Type * Type)} 123 -> r :: {(Type * Type * Type)}
134 -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] 124 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
135 125
136 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 126 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
137 -> sql_query tables exps 127 -> sql_query tables exps
138 -> fn [tables ~ exps] => 128 -> fn [tables ~ exps] =>
139 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => 129 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
140 [nm = $fields] ++ acc) [] tables)
141 -> xml ctx [] []) 130 -> xml ctx [] [])
142 -> transaction (xml ctx [] []) 131 -> transaction (xml ctx [] [])
143 132
144 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 133 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
145 -> sql_query tables exps 134 -> sql_query tables exps
146 -> fn [tables ~ exps] => 135 -> fn [tables ~ exps] =>
147 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => 136 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
148 [nm = $fields] ++ acc) [] tables)
149 -> transaction (xml ctx [] [])) 137 -> transaction (xml ctx [] []))
150 -> transaction (xml ctx [] []) 138 -> transaction (xml ctx [] [])
151 139
152 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} 140 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
153 -> sql_query tables exps 141 -> sql_query tables exps
154 -> fn [tables ~ exps] => 142 -> fn [tables ~ exps] =>
155 transaction 143 transaction
156 (option 144 (option
157 $(exps 145 $(exps
158 ++ fold (fn nm (fields :: {Type}) acc 146 ++ map (fn fields :: {Type} => $fields) tables))
159 [[nm] ~ acc] =>
160 [nm = $fields] ++ acc)
161 [] tables))
162 147
163 val oneRow : tables ::: {{Type}} -> exps ::: {Type} 148 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
164 -> sql_query tables exps 149 -> sql_query tables exps
165 -> fn [tables ~ exps] => 150 -> fn [tables ~ exps] =>
166 transaction 151 transaction
167 $(exps 152 $(exps
168 ++ fold (fn nm (fields :: {Type}) acc 153 ++ map (fn fields :: {Type} => $fields) tables)
169 [[nm] ~ acc] =>
170 [nm = $fields] ++ acc)
171 [] tables)
172 154
173 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 155 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
174 -> t ::: Type -> sql_injectable (option t) 156 -> t ::: Type -> sql_injectable (option t)
175 -> sql_exp tables agg exps (option t) 157 -> sql_exp tables agg exps (option t)
176 -> sql_exp tables agg exps (option t) 158 -> sql_exp tables agg exps (option t)