view 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 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

fun uppercaseFirst "" = ""
  | uppercaseFirst s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE)

%%
%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 | BAR
 | DIVIDE | GT | DOTDOTDOT
 | CON | LTYPE | VAL | REC | AND | FOLD | UNIT | KUNIT
 | DATATYPE | OF
 | TYPE | NAME
 | ARROW | LARROW | DARROW
 | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE
 | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
 | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT
 | CASE | IF | THEN | ELSE

 | XML_BEGIN of string | XML_END
 | NOTAGS of string 
 | BEGIN_TAG of string | END_TAG of string

%nonterm
   file of decl list
 | decls of decl list
 | decl of decl
 | 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

 | sgn of sgn
 | sgntm of sgn
 | sgi of sgn_item
 | sgis of sgn_item list

 | str of str

 | kind of kind
 | kcolon of explicitness

 | path of string list * string
 | cpath of string list * string
 | spath of str
 | mpath of string list

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

 | eexp of exp
 | eapps of exp
 | eterm of exp
 | rexp of (con * exp) list
 | xml of exp
 | xmlOne of exp
 | tag of string * exp
 | tagHead of string * exp

 | branch of pat * exp
 | branchs of (pat * exp) list
 | pat of pat
 | pterm of pat
 | rpat of (string * pat) list * bool

 | attrs of (con * exp) list
 | attr of con * exp
 | attrv of exp

%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 MINUSMINUS
%nonassoc TWIDDLE
%nonassoc DOLLAR
%left DOT

%%

file   : decls                          (decls)
       | SIG sgis                       ([(DSgn ("?", (SgnConst sgis, s (SIGleft, sgisright))),
                                           s (SIGleft, sgisright))])

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))
       | 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))

       | SIGNATURE CSYMBOL EQ sgn       (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
       | STRUCTURE CSYMBOL EQ str       (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright))
       | STRUCTURE CSYMBOL COLON sgn EQ str (DStr (CSYMBOL, SOME sgn, str), s (STRUCTUREleft, strright))
       | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN EQ str
                                        (DStr (CSYMBOL1, NONE,
                                               (StrFun (CSYMBOL2, sgn1, NONE, str), s (FUNCTORleft, strright))),
                                         s (FUNCTORleft, strright))
       | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn EQ str
                                        (DStr (CSYMBOL1, NONE,
                                               (StrFun (CSYMBOL2, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))),
                                         s (FUNCTORleft, strright))
       | EXTERN STRUCTURE CSYMBOL COLON sgn (DFfiStr (CSYMBOL, sgn), s (EXTERNleft, sgnright))
       | OPEN mpath                     (case mpath of
                                             [] => raise Fail "Impossible mpath parse [1]"
                                           | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright)))
       | OPEN CONSTRAINTS mpath         (case mpath of
                                             [] => raise Fail "Impossible mpath parse [3]"
                                           | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright)))
       | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
       | EXPORT spath                   (DExport spath, s (EXPORTleft, spathright))

dargs  :                                ([])
       | SYMBOL dargs                   (SYMBOL :: dargs)

barOpt :                                ()
       | BAR                            ()

dcons  : dcon                           ([dcon])
       | dcon BAR dcons                 (dcon :: dcons)

dcon   : CSYMBOL                        (CSYMBOL, NONE)
       | CSYMBOL OF cexp                (CSYMBOL, SOME cexp)

vali   : SYMBOL EQ eexp                 (SYMBOL, NONE, eexp)
       | SYMBOL COLON cexp EQ eexp      (SYMBOL, SOME cexp, eexp)

valis  : vali                           ([vali])
       | vali AND valis                 (vali :: valis)

sgn    : sgntm                          (sgntm)
       | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
                                        (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right))

sgntm  : SIG sgis END                   (SgnConst sgis, s (SIGleft, ENDright))
       | mpath                          (case mpath of
                                             [] => raise Fail "Impossible mpath parse [2]"
                                           | [x] => SgnVar x
                                           | m :: ms => SgnProj (m,
                                                                 List.take (ms, length ms - 1),
                                                                 List.nth (ms, length ms - 1)),
                                         s (mpathleft, mpathright))
       | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
       | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
       | LPAREN sgn RPAREN              (sgn)

sgi    : CON SYMBOL DCOLON kind         (SgiConAbs (SYMBOL, kind), s (CONleft, kindright))
       | LTYPE SYMBOL                   (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
                                         s (LTYPEleft, SYMBOLright))
       | CON SYMBOL EQ cexp             (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
       | 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 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))
       | SIGNATURE CSYMBOL EQ sgn       (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
       | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
                                        (SgiStr (CSYMBOL1,
                                                 (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
                                         s (FUNCTORleft, sgn2right))
       | INCLUDE sgn                    (SgiInclude sgn, s (INCLUDEleft, sgnright))
       | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))

sgis   :                                ([])
       | sgi sgis                       (sgi :: sgis)

str    : STRUCT decls END               (StrConst decls, s (STRUCTleft, ENDright))
       | spath                          (spath)
       | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN DARROW str
                                        (StrFun (CSYMBOL, sgn, NONE, str), s (FUNCTORleft, strright))
       | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn DARROW str
                                        (StrFun (CSYMBOL, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))
       | spath LPAREN str RPAREN        (StrApp (spath, str), s (spathleft, RPARENright))

spath  : CSYMBOL                        (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
       | spath DOT CSYMBOL              (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright))

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))
       | KUNIT                          (KUnit, s (KUNITleft, KUNITright))
       | 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 DARROW cexp          (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright))
       | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright))
       | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
       | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, 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)

path   : SYMBOL                         ([], SYMBOL)
       | CSYMBOL DOT path               (let val (ms, x) = path in (CSYMBOL :: ms, x) end)

cpath  : CSYMBOL                        ([], CSYMBOL)
       | CSYMBOL DOT cpath              (let val (ms, x) = cpath in (CSYMBOL :: ms, x) end)

mpath  : CSYMBOL                        ([CSYMBOL])
       | CSYMBOL DOT mpath              (CSYMBOL :: mpath)

cterm  : LPAREN cexp RPAREN             (#1 cexp, s (LPARENleft, RPARENright))
       | LBRACK rcon RBRACK             (CRecord rcon, s (LBRACKleft, RBRACKright))
       | LBRACK rconn RBRACK            (CRecord rconn, 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))

       | 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)])
       | ident EQ cexp COMMA rcon       ((ident, cexp) :: rcon)

rconn  : ident                          ([(ident, (CUnit, s (identleft, identright)))])
       | ident COMMA rconn              ((ident, (CUnit, s (identleft, identright))) :: rconn)

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

ident  : CSYMBOL                        (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
       | path                           (CVar path, s (pathleft, pathright))

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))
       | LBRACK cterm TWIDDLE cterm RBRACK DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (LBRACKleft, RBRACKright))
       | FN UNIT DARROW eexp            (let
                                             val loc = s (FNleft, eexpright)
                                         in
                                             (EAbs ("_", SOME (TRecord (CRecord [], loc), loc), eexp), loc)
                                         end)

       | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
       | eexp MINUSMINUS cexp           (ECut (eexp, cexp), s (eexpleft, cexpright))
       | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright))
       | IF eexp THEN eexp ELSE eexp    (let
                                             val loc = s (IFleft, eexp3right)
                                         in
                                             (ECase (eexp1, [((PCon (["Basis"], "True", NONE), loc), eexp2),
                                                             ((PCon (["Basis"], "False", NONE), loc), eexp3)]), loc)
                                         end)

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

       | path                           (EVar path, s (pathleft, pathright))
       | cpath                          (EVar cpath, s (cpathleft, cpathright))
       | LBRACE rexp RBRACE             (ERecord rexp, s (LBRACEleft, RBRACEright))
       | UNIT                           (ERecord [], s (UNITleft, UNITright))

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

       | path DOT ident                 (EField ((EVar path, s (pathleft, pathright)), ident), s (pathleft, identright))
       | FOLD                           (EFold, s (FOLDleft, FOLDright))

       | XML_BEGIN xml XML_END          (xml)
       | XML_BEGIN XML_END              (EApp ((EVar (["Basis"], "cdata"), s (XML_BEGINleft, XML_ENDright)),
                                               (EPrim (Prim.String ""), s (XML_BEGINleft, XML_ENDright))),
                                         s (XML_BEGINleft, XML_ENDright))

branch : pat DARROW eexp                (pat, eexp)

branchs:                                ([])
       | BAR branch branchs             (branch :: branchs)

pat    : pterm                          (pterm)
       | cpath pterm                    (PCon (#1 cpath, #2 cpath, SOME pterm), s (cpathleft, ptermright))

pterm  : SYMBOL                         (PVar SYMBOL, s (SYMBOLleft, SYMBOLright))
       | cpath                          (PCon (#1 cpath, #2 cpath, NONE), s (cpathleft, cpathright))
       | UNDER                          (PWild, s (UNDERleft, UNDERright))
       | INT                            (PPrim (Prim.Int INT), s (INTleft, INTright))
       | STRING                         (PPrim (Prim.String STRING), s (STRINGleft, STRINGright))
       | LPAREN pat RPAREN              (pat)
       | LBRACE RBRACE                  (PRecord ([], false), s (LBRACEleft, RBRACEright))
       | UNIT                           (PRecord ([], false), s (UNITleft, UNITright))
       | LBRACE rpat RBRACE             (PRecord rpat, s (LBRACEleft, RBRACEright))

rpat   : CSYMBOL EQ pat                 ([(CSYMBOL, pat)], false)
       | DOTDOTDOT                      ([], true)
       | CSYMBOL EQ pat COMMA rpat      ((CSYMBOL, pat) :: #1 rpat, #2 rpat)

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

xml    : xmlOne xml                     (let
                                             val pos = s (xmlOneleft, xmlright)
                                         in
                                             (EApp ((EApp (
                                                     (EVar (["Basis"], "join"), pos),
                                                  xmlOne), pos),
                                                    xml), pos)
                                         end)
       | xmlOne                         (xmlOne)

xmlOne : NOTAGS                         (EApp ((EVar (["Basis"], "cdata"), s (NOTAGSleft, NOTAGSright)),
                                               (EPrim (Prim.String NOTAGS), s (NOTAGSleft, NOTAGSright))),
                                         s (NOTAGSleft, NOTAGSright))
       | tag DIVIDE GT                  (let
                                             val pos = s (tagleft, GTright)
                                         in
                                             (EApp (#2 tag,
                                                    (EApp ((EVar (["Basis"], "cdata"), pos),
                                                           (EPrim (Prim.String ""), pos)),
                                                     pos)), pos)
                                         end)
         
       | tag GT xml END_TAG             (let
                                             val pos = s (tagleft, GTright)
                                         in
                                             if #1 tag = END_TAG then
                                                 if END_TAG = "lform" then
                                                     (EApp ((EVar (["Basis"], "lform"), pos),
                                                            xml), pos)
                                                 else
                                                     (EApp (#2 tag, xml), pos)
                                             else
                                                 (ErrorMsg.errorAt pos "Begin and end tags don't match.";
                                                  (EFold, pos))
                                         end)
       | LBRACE eexp RBRACE             (eexp)

tag    : tagHead attrs                  (let
                                             val pos = s (tagHeadleft, attrsright)
                                         in
                                             (#1 tagHead,
                                              (EApp ((EApp ((EVar (["Basis"], "tag"), pos),
                                                            (ERecord attrs, pos)), pos),
                                                     (EApp (#2 tagHead,
                                                            (ERecord [], pos)), pos)),
                                               pos))
                                         end)

tagHead: BEGIN_TAG                      (let
                                             val pos = s (BEGIN_TAGleft, BEGIN_TAGright)
                                         in
                                             (BEGIN_TAG,
                                              (EVar ([], BEGIN_TAG), pos))
                                         end)
       | tagHead LBRACE cexp RBRACE     (#1 tagHead, (ECApp (#2 tagHead, cexp), s (tagHeadleft, RBRACEright)))
                                          
attrs  :                                ([])
       | attr attrs                     (attr :: attrs)

attr   : SYMBOL EQ attrv                ((CName (uppercaseFirst SYMBOL), s (SYMBOLleft, SYMBOLright)), attrv)

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