diff src/lacweb.grm @ 191:aa54250f58ac

Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 3eb53c957d10
children 85b5f663bb86
line wrap: on
line diff
--- a/src/lacweb.grm	Thu Aug 07 13:09:26 2008 -0400
+++ b/src/lacweb.grm	Fri Aug 08 10:28:32 2008 -0400
@@ -64,6 +64,7 @@
  | vali of string * con option * exp
  | valis of (string * con option * exp) list
 
+ | dargs of string list
  | barOpt of unit
  | dcons of (string * con option) list
  | dcon of string * con option
@@ -142,9 +143,11 @@
        | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
-       | DATATYPE SYMBOL EQ barOpt dcons(DDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright))
-       | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path
-                (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+       | DATATYPE SYMBOL dargs EQ barOpt dcons(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
+       | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
+                (case dargs of
+                     [] => (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+                   | _ => raise Fail "Arguments specified for imported datatype")
        | VAL vali                       (DVal vali, s (VALleft, valiright))
        | VAL REC valis                  (DValRec valis, s (VALleft, valisright))
 
@@ -169,6 +172,9 @@
        | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
        | EXPORT spath                   (DExport spath, s (EXPORTleft, spathright))
 
+dargs  :                                ([])
+       | SYMBOL dargs                   (SYMBOL :: dargs)
+
 barOpt :                                ()
        | BAR                            ()
 
@@ -207,9 +213,11 @@
        | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
        | LTYPE SYMBOL EQ cexp           (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
                                          s (LTYPEleft, cexpright))
-       | DATATYPE SYMBOL EQ barOpt dcons(SgiDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright))
-       | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path
-                (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+       | DATATYPE SYMBOL dargs EQ barOpt dcons(SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
+       | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
+                (case dargs of
+                     [] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
+                   | _ => raise Fail "Arguments specified for imported datatype")
        | VAL SYMBOL COLON cexp          (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
 
        | STRUCTURE CSYMBOL COLON sgn    (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))