Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/src/urweb.grm Sun Feb 22 17:39:55 2009 -0500 +++ b/src/urweb.grm Tue Feb 24 12:01:24 2009 -0500 @@ -594,6 +594,7 @@ | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) + | LBRACK cexp TWIDDLE cexp RBRACK DARROW cexp (TDisjoint (cexp1, cexp2, cexp3), s (LBRACKleft, cexp3right)) | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -657,13 +658,7 @@ ((CAbs (SYMBOL, SOME kind, c), loc), (KArrow (kind, k), loc)) end) - | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => - let - val loc = s (LBRACKleft, RBRACKright) - in - ((CDisjoint (cexp1, cexp2, c), loc), - k) - end) + path : SYMBOL ([], SYMBOL) | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) @@ -849,14 +844,14 @@ val loc = s (LPARENleft, RPARENright) in ((EDisjoint (cexp1, cexp2, e), loc), - (CDisjoint (cexp1, cexp2, t), loc)) + (TDisjoint (cexp1, cexp2, t), loc)) end) | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) => let val loc = s (LBRACKleft, RBRACKright) in ((EDisjoint (cexp1, cexp2, e), loc), - (CDisjoint (cexp1, cexp2, t), loc)) + (TDisjoint (cexp1, cexp2, t), loc)) end) | CSYMBOL (fn (e, t) => let