diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-02-24 12:01:24 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-02-24 12:01:24 -0500 |
| commit | 7b71af9c790abcff2bfe0a16a417a1023776351d (patch) | |
| tree | 9dd05f2dad9cc6d4e0e33af1e8f1cf0a1def9f15 /src/urweb.grm | |
| parent | bb4aed8e1304d5cb3cbe7ec5fdcf95344e9aa2d5 (diff) | |
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
Diffstat (limited to 'src/urweb.grm')
| -rw-r--r-- | src/urweb.grm | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/src/urweb.grm b/src/urweb.grm index b6e4ce72..86e8a5df 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -594,6 +594,7 @@ cexp : capps (capps) | 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 @@ cargp : SYMBOL (fn (c, k) => ((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 @@ eargp : SYMBOL (fn (e, t) => 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 |