view src/lacweb.grm @ 19:e634ae817a8e

Testing constructor equivalences
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 14:42:12 -0400
parents 9a578171de9e
children e6ccf961d8a3
line wrap: on
line source
(* Copyright (c) 2008, Adam Chlipala
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * - Redistributions of source code must retain the above copyright notice,
 *   this list of conditions and the following disclaimer.
 * - Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 * - The names of contributors may not be used to endorse or promote products
 *   derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

(* Grammar for Laconic/Web programs *)

open Source

val s = ErrorMsg.spanOf

%%
%header (functor LacwebLrValsFn(structure Token : TOKEN))

%term 
   EOF
 | STRING of string | INT of Int64.int | FLOAT of Real64.real
 | SYMBOL of string | CSYMBOL of string
 | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
 | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
 | CON | LTYPE | VAL
 | TYPE | NAME
 | ARROW | LARROW | DARROW
 | FN | PLUSPLUS | DOLLAR

%nonterm 
   file of decl list
 | decls of decl list
 | decl of decl

 | kind of kind
 | kcolon of explicitness

 | cexp of con
 | capps of con
 | cterm of con
 | ident of con
 | rcon of (con * con) list
 | rcone of (con * con) list

 | eexp of exp
 | eapps of exp
 | eterm of exp
 | rexp of (con * exp) list

%verbose                                (* print summary of errors *)
%pos int                                (* positions *)
%start file
%pure
%eop EOF
%noshift EOF

%name Lacweb

%nonassoc DARROW
%nonassoc COLON
%nonassoc DCOLON TCOLON
%right COMMA
%right ARROW LARROW
%right PLUSPLUS
%nonassoc DOLLAR
%left DOT

%%

file   : decls                          (decls)

decls  :                                ([])
       | decl decls                     (decl :: decls)

decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
       | 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))
       | VAL SYMBOL EQ eexp             (DVal (SYMBOL, NONE, eexp), s (VALleft, eexpright))
       | VAL SYMBOL COLON cexp EQ eexp  (DVal (SYMBOL, SOME cexp, eexp), s (VALleft, eexpright))

kind   : TYPE                           (KType, s (TYPEleft, TYPEright))
       | NAME                           (KName, s (NAMEleft, NAMEright))
       | 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))
       | UNDERUNDER                     (KWild, s (UNDERUNDERleft, UNDERUNDERright))

capps  : cterm                          (cterm)
       | capps cterm                    (CApp (capps, cterm), s (cappsleft, ctermright))

cexp   : capps                          (capps)
       | cexp ARROW cexp                (TFun (cexp1, cexp2), s (cexp1left, cexp2right))
       | SYMBOL kcolon kind ARROW cexp  (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright))

       | cexp PLUSPLUS cexp             (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))

       | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, kind, cexp), s (FNleft, cexpright))

       | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))

       | UNDER DCOLON kind              (CWild kind, s (UNDERleft, UNDERright))

kcolon : DCOLON                         (Explicit)
       | TCOLON                         (Implicit)

cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
       | LBRACK rcon RBRACK             (CRecord rcon, s (LBRACKleft, RBRACKright))
       | LBRACE rcone RBRACE            (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
					 s (LBRACEleft, RBRACEright))
       | DOLLAR cterm                   (TRecord cterm, s (DOLLARleft, ctermright))
       | HASH CSYMBOL                   (CName CSYMBOL, s (HASHleft, CSYMBOLright))

       | SYMBOL                         (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
       | UNDER                          (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))

rcon   :                                ([])
       | ident EQ cexp                  ([(ident, cexp)])
       | ident EQ cexp COMMA rcon       ((ident, cexp) :: rcon)

rcone  :                                ([])
       | ident COLON cexp               ([(ident, cexp)])
       | ident COLON cexp COMMA rcone   ((ident, cexp) :: rcone)

ident  : CSYMBOL                        (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
       | SYMBOL                         (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))

eapps  : eterm                          (eterm)
       | eapps eterm                    (EApp (eapps, eterm), s (eappsleft, etermright))
       | eapps LBRACK cexp RBRACK       (ECApp (eapps, cexp), s (eappsleft, RBRACKright))

eexp   : eapps                          (eapps)
       | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright))
       | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright))
       | FN SYMBOL DARROW eexp          (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))

       | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
       | eterm DOT ident                (EField (eterm, ident), s (etermleft, identright))

eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))

       | SYMBOL                         (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
       | LBRACE rexp RBRACE             (ERecord rexp, s (LBRACEleft, RBRACEright))

       | INT                            (EPrim (Prim.Int INT), s (INTleft, INTright))
       | FLOAT                          (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright))
       | STRING                         (EPrim (Prim.String STRING), s (STRINGleft, STRINGright))

rexp   :                                ([])
       | ident EQ eexp                  ([(ident, eexp)])
       | ident EQ eexp COMMA rexp       ((ident, eexp) :: rexp)