Mercurial > urweb

comparison src/elab_env.sml @ 203:dd82457fda82

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing and elaborating 'table'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 13:20:29 -0400
parents aa54250f58ac
children cb8f69556975
comparison
equal deleted inserted replaced
202:af5bd54cbbd7 203:dd82457fda82
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) =>
408 (case lookupStr env "Basis" of
409 NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis"
410 | SOME (n, _) =>
411 let
412 val t = (CApp ((CModProj (n, [], "table"), loc), c), loc)
413 in
414 pushENamedAs env x n t
415 end)
416
407 fun sgnSeek f sgis = 417 fun sgnSeek f sgis =
408 let 418 let
409 fun seek (sgis, sgns, strs, cons) = 419 fun seek (sgis, sgns, strs, cons) =
410 case sgis of 420 case sgis of
411 [] => NONE 421 [] => NONE
429 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 439 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
430 | SgiVal _ => seek (sgis, sgns, strs, cons) 440 | SgiVal _ => seek (sgis, sgns, strs, cons)
431 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) 441 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
432 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) 442 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
433 | SgiConstraint _ => seek (sgis, sgns, strs, cons) 443 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
444 | SgiTable _ => seek (sgis, sgns, strs, cons)
434 in 445 in
435 seek (sgis, IM.empty, IM.empty, IM.empty) 446 seek (sgis, IM.empty, IM.empty, IM.empty)
436 end 447 end
437 448
438 fun id x = x 449 fun id x = x
664 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 675 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
665 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 676 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
666 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 677 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
667 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 678 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
668 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 679 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
680 | SgiTable _ => seek (sgis, sgns, strs, cons, acc)
669 in 681 in
670 seek (sgis, IM.empty, IM.empty, IM.empty, []) 682 seek (sgis, IM.empty, IM.empty, IM.empty, [])
671 end 683 end
672 684
673 fun projectConstraints env {sgn, str} = 685 fun projectConstraints env {sgn, str} =
723 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 735 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
724 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn 736 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
725 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn 737 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
726 | DConstraint _ => env 738 | DConstraint _ => env
727 | DExport _ => env 739 | DExport _ => env
740 | DTable (x, n, c) =>
741 (case lookupStr env "Basis" of
742 NONE => raise Fail "ElabEnv.declBinds: Can't find Basis"
743 | SOME (n, _) =>
744 let
745 val t = (CApp ((CModProj (n, [], "table"), loc), c), loc)
746 in
747 pushENamedAs env x n t
748 end)
728 749
729 end 750 end