Mercurial > urweb

comparison lib/ur/top.ur @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 8998114760c1
children f4f2b09a533a
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
1 (** Row folding *)
2
3 con folder = K ==> fn r :: {K} =>
4 tf :: ({K} -> Type)
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
6 -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
7 -> tf [] -> tf r
8
9
1 fun not b = if b then False else True 10 fun not b = if b then False else True
2 11
3 con idT (t :: Type) = t 12 con idT (t :: Type) = t
4 con record (t :: {Type}) = $t 13 con record (t :: {Type}) = $t
5 con fstTT (t :: (Type * Type)) = t.1 14 con fstTT (t :: (Type * Type)) = t.1
25 34
26 fun foldUR (tf :: Type) (tr :: {Unit} -> Type) 35 fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
27 (f : nm :: Name -> rest :: {Unit} 36 (f : nm :: Name -> rest :: {Unit}
28 -> fn [[nm] ~ rest] => 37 -> fn [[nm] ~ rest] =>
29 tf -> tr rest -> tr ([nm] ++ rest)) 38 tf -> tr rest -> tr ([nm] ++ rest))
30 (i : tr []) = 39 (i : tr []) (r ::: {Unit}) (fold : folder r)=
31 fold [fn r :: {Unit} => $(mapUT tf r) -> tr r] 40 fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
32 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc 41 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
33 [[nm] ~ rest] r => 42 [[nm] ~ rest] r =>
34 f [nm] [rest] r.nm (acc (r -- nm))) 43 f [nm] [rest] r.nm (acc (r -- nm)))
35 (fn _ => i) 44 (fn _ => i)
36 45
37 fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) 46 fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
38 (f : nm :: Name -> rest :: {Unit} 47 (f : nm :: Name -> rest :: {Unit}
39 -> fn [[nm] ~ rest] => 48 -> fn [[nm] ~ rest] =>
40 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) 49 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
41 (i : tr []) = 50 (i : tr []) (r ::: {Unit}) (fold : folder r) =
42 fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] 51 fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
43 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc 52 (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
44 [[nm] ~ rest] r1 r2 => 53 [[nm] ~ rest] r1 r2 =>
45 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 54 f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
46 (fn _ _ => i) 55 (fn _ _ => i)
47 56
48 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) 57 fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
49 (f : nm :: Name -> rest :: {Unit} 58 (f : nm :: Name -> rest :: {Unit}
50 -> fn [[nm] ~ rest] => 59 -> fn [[nm] ~ rest] =>
51 tf1 -> tf2 -> xml ctx [] []) = 60 tf1 -> tf2 -> xml ctx [] []) =
52 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] 61 foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
53 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => 62 (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc =>
54 <xml>{f [nm] [rest] v1 v2}{acc}</xml>) 63 <xml>{f [nm] [rest] v1 v2}{acc}</xml>)
55 <xml/> 64 <xml/>
56 65
57 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) 66 fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
58 (f : nm :: Name -> t :: Type -> rest :: {Type} 67 (f : nm :: Name -> t :: K -> rest :: {K}
59 -> fn [[nm] ~ rest] => 68 -> fn [[nm] ~ rest] =>
60 tf t -> tr rest -> tr ([nm = t] ++ rest)) 69 tf t -> tr rest -> tr ([nm = t] ++ rest))
61 (i : tr []) = 70 (i : tr []) (r ::: {K}) (fold : folder r) =
62 fold [fn r :: {Type} => $(map tf r) -> tr r] 71 fold [fn r :: {K} => $(map tf r) -> tr r]
63 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) 72 (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest)
64 [[nm] ~ rest] r => 73 [[nm] ~ rest] r =>
65 f [nm] [t] [rest] r.nm (acc (r -- nm))) 74 f [nm] [t] [rest] r.nm (acc (r -- nm)))
66 (fn _ => i) 75 (fn _ => i)
67 76
68 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) 77 fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type)
69 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 78 (f : nm :: Name -> t :: K -> rest :: {K}
70 -> fn [[nm] ~ rest] =>
71 tf t -> tr rest -> tr ([nm = t] ++ rest))
72 (i : tr []) =
73 fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r]
74 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
75 (acc : _ -> tr rest) [[nm] ~ rest] r =>
76 f [nm] [t] [rest] r.nm (acc (r -- nm)))
77 (fn _ => i)
78
79 fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type)
80 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
81 -> fn [[nm] ~ rest] =>
82 tf t -> tr rest -> tr ([nm = t] ++ rest))
83 (i : tr []) =
84 fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r]
85 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
86 (acc : _ -> tr rest) [[nm] ~ rest] r =>
87 f [nm] [t] [rest] r.nm (acc (r -- nm)))
88 (fn _ => i)
89
90 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
91 (f : nm :: Name -> t :: Type -> rest :: {Type}
92 -> fn [[nm] ~ rest] => 79 -> fn [[nm] ~ rest] =>
93 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 80 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
94 (i : tr []) = 81 (i : tr []) (r ::: {K}) (fold : folder r) =
95 fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r] 82 fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
96 (fn (nm :: Name) (t :: Type) (rest :: {Type}) 83 (fn (nm :: Name) (t :: K) (rest :: {K})
97 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => 84 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
98 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) 85 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
99 (fn _ _ => i) 86 (fn _ _ => i)
100 87
101 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) 88 fun foldRX K (tf :: K -> Type) (ctx :: {Unit})
102 (tr :: {(Type * Type)} -> Type) 89 (f : nm :: Name -> t :: K -> rest :: {K}
103 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
104 -> fn [[nm] ~ rest] =>
105 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
106 (i : tr []) =
107 fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
108 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
109 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
110 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
111 (fn _ _ => i)
112
113 fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
114 (tr :: {(Type * Type * Type)} -> Type)
115 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
116 -> fn [[nm] ~ rest] =>
117 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
118 (i : tr []) =
119 fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
120 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
121 (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
122 f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
123 (fn _ _ => i)
124
125 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
126 (f : nm :: Name -> t :: Type -> rest :: {Type}
127 -> fn [[nm] ~ rest] => 90 -> fn [[nm] ~ rest] =>
128 tf t -> xml ctx [] []) = 91 tf t -> xml ctx [] []) =
129 foldTR [tf] [fn _ => xml ctx [] []] 92 foldR [tf] [fn _ => xml ctx [] []]
130 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc => 93 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc =>
131 <xml>{f [nm] [t] [rest] r}{acc}</xml>) 94 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
132 <xml/> 95 <xml/>
133 96
134 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) 97 fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
135 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} 98 (f : nm :: Name -> t :: K -> rest :: {K}
136 -> fn [[nm] ~ rest] =>
137 tf t -> xml ctx [] []) =
138 foldT2R [tf] [fn _ => xml ctx [] []]
139 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
140 [[nm] ~ rest] r acc =>
141 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
142 <xml/>
143
144 fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit})
145 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
146 -> fn [[nm] ~ rest] =>
147 tf t -> xml ctx [] []) =
148 foldT3R [tf] [fn _ => xml ctx [] []]
149 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
150 [[nm] ~ rest] r acc =>
151 <xml>{f [nm] [t] [rest] r}{acc}</xml>)
152 <xml/>
153
154 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
155 (f : nm :: Name -> t :: Type -> rest :: {Type}
156 -> fn [[nm] ~ rest] => 99 -> fn [[nm] ~ rest] =>
157 tf1 t -> tf2 t -> xml ctx [] []) = 100 tf1 t -> tf2 t -> xml ctx [] []) =
158 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] 101 foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
159 (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] 102 (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest]
160 r1 r2 acc => 103 r1 r2 acc =>
161 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) 104 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
162 <xml/> 105 <xml/>
163
164 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
165 (ctx :: {Unit})
166 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
167 -> fn [[nm] ~ rest] =>
168 tf1 t -> tf2 t -> xml ctx [] []) =
169 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
170 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
171 [[nm] ~ rest] r1 r2 acc =>
172 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
173 <xml/>
174
175 fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
176 (ctx :: {Unit})
177 (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
178 -> fn [[nm] ~ rest] =>
179 tf1 t -> tf2 t -> xml ctx [] []) =
180 foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []]
181 (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
182 [[nm] ~ rest] r1 r2 acc =>
183 <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
184 <xml/>
185 106
186 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) 107 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
187 (q : sql_query tables exps) [tables ~ exps] 108 (q : sql_query tables exps) [tables ~ exps]
188 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) 109 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables)
189 -> xml ctx [] []) = 110 -> xml ctx [] []) =