Mercurial > urweb
comparison src/urweb.grm @ 628:12b73f3c108e
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 |