Mercurial > urweb

comparison src/elab_env.sml @ 174:7ee424760d2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating module constructor patterns; parsing record patterns
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 11:28:55 -0400
parents c7a6e6dbc318
children 88d46972de53
comparison
equal deleted inserted replaced
173:8221b95cc24c 174:7ee424760d2f
568 | _ => NONE) sgis of 568 | _ => NONE) sgis of
569 NONE => NONE 569 NONE => NONE
570 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) 570 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
571 | _ => NONE 571 | _ => NONE
572 572
573 fun projectConstructor env {sgn, str, field} =
574 case #1 (hnormSgn env sgn) of
575 SgnConst sgis =>
576 let
577 fun consider (n, xncs) =
578 ListUtil.search (fn (x, n', to) =>
579 if x <> field then
580 NONE
581 else
582 SOME (n', to, (CNamed n, #2 str))) xncs
583 in
584 case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
585 | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
586 | _ => NONE) sgis of
587 NONE => NONE
588 | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t)
589 end
590 | _ => NONE
591
573 fun projectVal env {sgn, str, field} = 592 fun projectVal env {sgn, str, field} =
574 case #1 (hnormSgn env sgn) of 593 case #1 (hnormSgn env sgn) of
575 SgnConst sgis => 594 SgnConst sgis =>
576 let 595 let
577 fun seek (n, xncs) = 596 fun seek (n, xncs) =