Mercurial > urweb

comparison src/elab_env.sml @ 205:cb8f69556975

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating 'SELECT *' queries
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 15:24:59 -0400
parents dd82457fda82
children e86411f647c6
comparison
equal deleted inserted replaced
204:241c9a0e3397 205:cb8f69556975
402 | SgiVal (x, n, t) => pushENamedAs env x n t 402 | SgiVal (x, n, t) => pushENamedAs env x n t
403 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 403 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
404 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 404 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
405 | SgiConstraint _ => env 405 | SgiConstraint _ => env
406 406
407 | SgiTable (x, n, c) => 407 | SgiTable (tn, x, n, c) =>
408 (case lookupStr env "Basis" of 408 let
409 NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis" 409 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
410 | SOME (n, _) => 410 in
411 let 411 pushENamedAs env x n t
412 val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) 412 end
413 in
414 pushENamedAs env x n t
415 end)
416 413
417 fun sgnSeek f sgis = 414 fun sgnSeek f sgis =
418 let 415 let
419 fun seek (sgis, sgns, strs, cons) = 416 fun seek (sgis, sgns, strs, cons) =
420 case sgis of 417 case sgis of
735 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 732 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
736 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn 733 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
737 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn 734 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
738 | DConstraint _ => env 735 | DConstraint _ => env
739 | DExport _ => env 736 | DExport _ => env
740 | DTable (x, n, c) => 737 | DTable (tn, x, n, c) =>
741 (case lookupStr env "Basis" of 738 let
742 NONE => raise Fail "ElabEnv.declBinds: Can't find Basis" 739 val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc)
743 | SOME (n, _) => 740 in
744 let 741 pushENamedAs env x n t
745 val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) 742 end
746 in
747 pushENamedAs env x n t
748 end)
749 743
750 end 744 end