Mercurial > urweb

comparison src/elab_util.sml @ 10:dde5c52e5e5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of elaborating expressions
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 13:59:03 -0400
parents 14b533dbe6cc
children e97c6d335869
comparison
equal deleted inserted replaced
9:14b533dbe6cc 10:dde5c52e5e5e
160 S.Return _ => true 160 S.Return _ => true
161 | S.Continue _ => false 161 | S.Continue _ => false
162 162
163 end 163 end
164 164
165 structure Exp = struct
166
167 fun mapfold {kind = fk, con = fc, exp = fe} =
168 let
169 val mfk = Kind.mapfold fk
170 val mfc = Con.mapfold {kind = fk, con = fc}
171
172 fun mfe e acc =
173 S.bindP (mfe' e acc, fe)
174
175 and mfe' (eAll as (e, loc)) =
176 case e of
177 ERel _ => S.return2 eAll
178 | ENamed _ => S.return2 eAll
179 | EApp (e1, e2) =>
180 S.bind2 (mfe e1,
181 fn e1' =>
182 S.map2 (mfe e2,
183 fn e2' =>
184 (EApp (e1', e2'), loc)))
185 | EAbs (x, t, e) =>
186 S.bind2 (mfc t,
187 fn t' =>
188 S.map2 (mfe e,
189 fn e' =>
190 (EAbs (x, t', e'), loc)))
191
192 | ECApp (e, c) =>
193 S.bind2 (mfe e,
194 fn e' =>
195 S.map2 (mfc c,
196 fn c' =>
197 (ECApp (e', c'), loc)))
198 | ECAbs (expl, x, k, e) =>
199 S.bind2 (mfk k,
200 fn k' =>
201 S.map2 (mfe e,
202 fn e' =>
203 (ECAbs (expl, x, k', e'), loc)))
204
205 | EError => S.return2 eAll
206 in
207 mfe
208 end
209
210 fun exists {kind, con, exp} k =
211 case mapfold {kind = fn k => fn () =>
212 if kind k then
213 S.Return ()
214 else
215 S.Continue (k, ()),
216 con = fn c => fn () =>
217 if con c then
218 S.Return ()
219 else
220 S.Continue (c, ()),
221 exp = fn e => fn () =>
222 if exp e then
223 S.Return ()
224 else
225 S.Continue (e, ())} k () of
226 S.Return _ => true
227 | S.Continue _ => false
228
229 end
230
165 structure E = ElabEnv 231 structure E = ElabEnv
166 232
167 fun declBinds env (d, _) = 233 fun declBinds env (d, _) =
168 case d of 234 case d of
169 DCon (x, n, k, _) => E.pushCNamedAs env x n k 235 DCon (x, n, k, _) => E.pushCNamedAs env x n k