Mercurial > urweb

comparison src/elaborate.sml @ 8:a455a9f85cc3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing basic expressions
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 17:10:26 -0500
parents 38bf996e1c2e
children 14b533dbe6cc
comparison
equal deleted inserted replaced
7:2ce5bf227d01 8:a455a9f85cc3
217 in 217 in
218 checkKind env c1' k1 (L'.KArrow (dom, ran), loc); 218 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
219 checkKind env c2' k2 dom; 219 checkKind env c2' k2 dom;
220 ((L'.CApp (c1', c2'), loc), ran) 220 ((L'.CApp (c1', c2'), loc), ran)
221 end 221 end
222 | L.CAbs (e, x, k, t) => 222 | L.CAbs (x, k, t) =>
223 let 223 let
224 val e' = elabExplicitness e
225 val k' = elabKind k 224 val k' = elabKind k
226 val env' = E.pushCRel env x k' 225 val env' = E.pushCRel env x k'
227 val (t', tk) = elabCon env' t 226 val (t', tk) = elabCon env' t
228 in 227 in
229 ((L'.CAbs (e', x, k', t'), loc), 228 ((L'.CAbs (x, k', t'), loc),
230 (L'.KArrow (k', tk), loc)) 229 (L'.KArrow (k', tk), loc))
231 end 230 end
232 231
233 | L.CName s => 232 | L.CName s =>
234 ((L'.CName s, loc), kname) 233 ((L'.CName s, loc), kname)