diff src/lacweb.grm @ 82:b4f2a258e52c

Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents 6431b315a1e3
children 0a1baddd8ab2
line wrap: on
line diff
--- a/src/lacweb.grm	Tue Jul 01 09:29:49 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 10:55:38 2008 -0400
@@ -40,7 +40,7 @@
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
- | CON | LTYPE | VAL | FOLD
+ | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
  | TYPE | NAME
  | ARROW | LARROW | DARROW
  | FN | PLUSPLUS | DOLLAR
@@ -179,6 +179,7 @@
        | LBRACE kind RBRACE             (KRecord kind, s (LBRACEleft, RBRACEright))
        | kind ARROW kind                (KArrow (kind1, kind2), s (kind1left, kind2right))
        | LPAREN kind RPAREN             (#1 kind, s (LPARENleft, RPARENright))
+       | KUNIT                          (KUnit, s (KUNITleft, KUNITright))
        | UNDERUNDER                     (KWild, s (UNDERUNDERleft, UNDERUNDERright))
 
 capps  : cterm                          (cterm)
@@ -216,6 +217,7 @@
        | path                           (CVar path, s (pathleft, pathright))
        | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
        | FOLD                           (CFold, s (FOLDleft, FOLDright))
+       | UNIT                           (CUnit, s (UNITleft, UNITright))
 
 rcon   :                                ([])
        | ident EQ cexp                  ([(ident, cexp)])