Mercurial > urweb

comparison src/urweb.grm @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 588b9d16b00a
children e68de2a5506b
comparison
equal deleted inserted replaced
627:f4f2b09a533a 628:12b73f3c108e
592 | CSYMBOL KARROW cexp (TKFun (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) 592 | CSYMBOL KARROW cexp (TKFun (CSYMBOL, cexp), s (CSYMBOLleft, cexpright))
593 593
594 | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) 594 | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
595 595
596 | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) 596 | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
597 | LBRACK cexp TWIDDLE cexp RBRACK DARROW cexp (TDisjoint (cexp1, cexp2, cexp3), s (LBRACKleft, cexp3right))
597 | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) 598 | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright))
598 599
599 | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) 600 | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
600 601
601 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright)) 602 | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright))
655 val loc = s (LPARENleft, RPARENright) 656 val loc = s (LPARENleft, RPARENright)
656 in 657 in
657 ((CAbs (SYMBOL, SOME kind, c), loc), 658 ((CAbs (SYMBOL, SOME kind, c), loc),
658 (KArrow (kind, k), loc)) 659 (KArrow (kind, k), loc))
659 end) 660 end)
660 | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => 661
661 let
662 val loc = s (LBRACKleft, RBRACKright)
663 in
664 ((CDisjoint (cexp1, cexp2, c), loc),
665 k)
666 end)
667 662
668 path : SYMBOL ([], SYMBOL) 663 path : SYMBOL ([], SYMBOL)
669 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) 664 | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
670 665
671 cpath : CSYMBOL ([], CSYMBOL) 666 cpath : CSYMBOL ([], CSYMBOL)
847 | LPAREN cexp TWIDDLE cexp RPAREN (fn (e, t) => 842 | LPAREN cexp TWIDDLE cexp RPAREN (fn (e, t) =>
848 let 843 let
849 val loc = s (LPARENleft, RPARENright) 844 val loc = s (LPARENleft, RPARENright)
850 in 845 in
851 ((EDisjoint (cexp1, cexp2, e), loc), 846 ((EDisjoint (cexp1, cexp2, e), loc),
852 (CDisjoint (cexp1, cexp2, t), loc)) 847 (TDisjoint (cexp1, cexp2, t), loc))
853 end) 848 end)
854 | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) => 849 | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) =>
855 let 850 let
856 val loc = s (LBRACKleft, RBRACKright) 851 val loc = s (LBRACKleft, RBRACKright)
857 in 852 in
858 ((EDisjoint (cexp1, cexp2, e), loc), 853 ((EDisjoint (cexp1, cexp2, e), loc),
859 (CDisjoint (cexp1, cexp2, t), loc)) 854 (TDisjoint (cexp1, cexp2, t), loc))
860 end) 855 end)
861 | CSYMBOL (fn (e, t) => 856 | CSYMBOL (fn (e, t) =>
862 let 857 let
863 val loc = s (CSYMBOLleft, CSYMBOLright) 858 val loc = s (CSYMBOLleft, CSYMBOLright)
864 in 859 in