adamc@1: (* Copyright (c) 2008, Adam Chlipala adamc@1: * All rights reserved. adamc@1: * adamc@1: * Redistribution and use in source and binary forms, with or without adamc@1: * modification, are permitted provided that the following conditions are met: adamc@1: * adamc@1: * - Redistributions of source code must retain the above copyright notice, adamc@1: * this list of conditions and the following disclaimer. adamc@1: * - Redistributions in binary form must reproduce the above copyright notice, adamc@1: * this list of conditions and the following disclaimer in the documentation adamc@1: * and/or other materials provided with the distribution. adamc@1: * - The names of contributors may not be used to endorse or promote products adamc@1: * derived from this software without specific prior written permission. adamc@1: * adamc@1: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@1: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@1: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@1: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@1: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@1: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@1: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@1: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@1: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@1: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@1: * POSSIBILITY OF SUCH DAMAGE. adamc@1: *) adamc@1: adamc@1: (* Grammar for Laconic/Web programs *) adamc@1: adamc@4: open Source adamc@1: adamc@1: val s = ErrorMsg.spanOf adamc@1: adamc@1: %% adamc@1: %header (functor LacwebLrValsFn(structure Token : TOKEN)) adamc@1: adamc@1: %term adamc@1: EOF adamc@14: | STRING of string | INT of Int64.int | FLOAT of Real64.real adamc@1: | SYMBOL of string | CSYMBOL of string adamc@1: | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE adamc@18: | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER adamc@82: | CON | LTYPE | VAL | FOLD | UNIT | KUNIT adamc@7: | TYPE | NAME adamc@1: | ARROW | LARROW | DARROW adamc@84: | FN | PLUSPLUS | DOLLAR | TWIDDLE adamc@88: | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN adamc@88: | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS adamc@1: adamc@30: %nonterm adamc@1: file of decl list adamc@1: | decls of decl list adamc@1: | decl of decl adamc@1: adamc@30: | sgn of sgn adamc@42: | sgntm of sgn adamc@30: | sgi of sgn_item adamc@30: | sgis of sgn_item list adamc@30: adamc@30: | str of str adamc@30: adamc@1: | kind of kind adamc@1: | kcolon of explicitness adamc@1: adamc@34: | path of string list * string adamc@34: | spath of str adamc@59: | mpath of string list adamc@34: adamc@1: | cexp of con adamc@1: | capps of con adamc@1: | cterm of con adamc@1: | ident of con adamc@1: | rcon of (con * con) list adamc@83: | rconn of (con * con) list adamc@1: | rcone of (con * con) list adamc@1: adamc@8: | eexp of exp adamc@8: | eapps of exp adamc@8: | eterm of exp adamc@12: | rexp of (con * exp) list adamc@8: adamc@1: %verbose (* print summary of errors *) adamc@1: %pos int (* positions *) adamc@1: %start file adamc@1: %pure adamc@1: %eop EOF adamc@1: %noshift EOF adamc@1: adamc@1: %name Lacweb adamc@1: adamc@1: %nonassoc DARROW adamc@1: %nonassoc COLON adamc@6: %nonassoc DCOLON TCOLON adamc@1: %right COMMA adamc@1: %right ARROW LARROW adamc@1: %right PLUSPLUS adamc@84: %nonassoc TWIDDLE adamc@1: %nonassoc DOLLAR adamc@1: %left DOT adamc@1: adamc@1: %% adamc@1: adamc@1: file : decls (decls) adamc@54: | SIG sgis ([(DSgn ("?", (SgnConst sgis, s (SIGleft, sgisright))), adamc@54: s (SIGleft, sgisright))]) adamc@1: adamc@1: decls : ([]) adamc@1: | decl decls (decl :: decls) adamc@1: adamc@1: decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)) adamc@1: | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) adamc@7: | LTYPE SYMBOL EQ cexp (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), adamc@7: s (LTYPEleft, cexpright)) adamc@8: | VAL SYMBOL EQ eexp (DVal (SYMBOL, NONE, eexp), s (VALleft, eexpright)) adamc@8: | VAL SYMBOL COLON cexp EQ eexp (DVal (SYMBOL, SOME cexp, eexp), s (VALleft, eexpright)) adamc@1: adamc@30: | SIGNATURE CSYMBOL EQ sgn (DSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) adamc@30: | STRUCTURE CSYMBOL EQ str (DStr (CSYMBOL, NONE, str), s (STRUCTUREleft, strright)) adamc@30: | STRUCTURE CSYMBOL COLON sgn EQ str (DStr (CSYMBOL, SOME sgn, str), s (STRUCTUREleft, strright)) adamc@42: | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN EQ str adamc@42: (DStr (CSYMBOL1, NONE, adamc@42: (StrFun (CSYMBOL2, sgn1, NONE, str), s (FUNCTORleft, strright))), adamc@42: s (FUNCTORleft, strright)) adamc@42: | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn EQ str adamc@42: (DStr (CSYMBOL1, NONE, adamc@42: (StrFun (CSYMBOL2, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))), adamc@42: s (FUNCTORleft, strright)) adamc@48: | EXTERN STRUCTURE CSYMBOL COLON sgn (DFfiStr (CSYMBOL, sgn), s (EXTERNleft, sgnright)) adamc@61: | OPEN mpath (case mpath of adamc@61: [] => raise Fail "Impossible mpath parse [1]" adamc@61: | m :: ms => (DOpen (m, ms), s (OPENleft, mpathright))) adamc@88: | OPEN CONSTRAINTS mpath (case mpath of adamc@88: [] => raise Fail "Impossible mpath parse [3]" adamc@88: | m :: ms => (DOpenConstraints (m, ms), s (OPENleft, mpathright))) adamc@88: | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) adamc@30: adamc@42: sgn : sgntm (sgntm) adamc@40: | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn adamc@40: (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) adamc@30: adamc@42: sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) adamc@59: | mpath (case mpath of adamc@61: [] => raise Fail "Impossible mpath parse [2]" adamc@59: | [x] => SgnVar x adamc@59: | m :: ms => SgnProj (m, adamc@59: List.take (ms, length ms - 1), adamc@59: List.nth (ms, length ms - 1)), adamc@59: s (mpathleft, mpathright)) adamc@42: | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) adamc@42: | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) adamc@42: | LPAREN sgn RPAREN (sgn) adamc@42: adamc@30: sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, kindright)) adamc@30: | LTYPE SYMBOL (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))), adamc@30: s (LTYPEleft, SYMBOLright)) adamc@30: | CON SYMBOL EQ cexp (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)) adamc@30: | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) adamc@30: | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), adamc@30: s (LTYPEleft, cexpright)) adamc@30: | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) adamc@30: adamc@30: | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) adamc@59: | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) adamc@42: | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn adamc@42: (SgiStr (CSYMBOL1, adamc@42: (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), adamc@42: s (FUNCTORleft, sgn2right)) adamc@58: | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright)) adamc@88: | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) adamc@30: adamc@30: sgis : ([]) adamc@30: | sgi sgis (sgi :: sgis) adamc@30: adamc@30: str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright)) adamc@34: | spath (spath) adamc@40: | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN DARROW str adamc@40: (StrFun (CSYMBOL, sgn, NONE, str), s (FUNCTORleft, strright)) adamc@40: | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn DARROW str adamc@40: (StrFun (CSYMBOL, sgn1, SOME sgn2, str), s (FUNCTORleft, strright)) adamc@44: | spath LPAREN str RPAREN (StrApp (spath, str), s (spathleft, RPARENright)) adamc@34: adamc@34: spath : CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) adamc@34: | spath DOT CSYMBOL (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright)) adamc@30: adamc@1: kind : TYPE (KType, s (TYPEleft, TYPEright)) adamc@1: | NAME (KName, s (NAMEleft, NAMEright)) adamc@1: | LBRACE kind RBRACE (KRecord kind, s (LBRACEleft, RBRACEright)) adamc@1: | kind ARROW kind (KArrow (kind1, kind2), s (kind1left, kind2right)) adamc@1: | LPAREN kind RPAREN (#1 kind, s (LPARENleft, RPARENright)) adamc@82: | KUNIT (KUnit, s (KUNITleft, KUNITright)) adamc@18: | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) adamc@1: adamc@1: capps : cterm (cterm) adamc@1: | capps cterm (CApp (capps, cterm), s (cappsleft, ctermright)) adamc@1: adamc@1: cexp : capps (capps) adamc@1: | cexp ARROW cexp (TFun (cexp1, cexp2), s (cexp1left, cexp2right)) adamc@15: | SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright)) adamc@1: adamc@1: | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) adamc@1: adamc@67: | FN SYMBOL DARROW cexp (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright)) adamc@67: | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright)) adamc@84: | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) adamc@85: | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) adamc@1: adamc@8: | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) adamc@6: adamc@18: | UNDER DCOLON kind (CWild kind, s (UNDERleft, UNDERright)) adamc@18: adamc@1: kcolon : DCOLON (Explicit) adamc@1: | TCOLON (Implicit) adamc@1: adamc@34: path : SYMBOL ([], SYMBOL) adamc@34: | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) adamc@34: adamc@59: mpath : CSYMBOL ([CSYMBOL]) adamc@59: | CSYMBOL DOT mpath (CSYMBOL :: mpath) adamc@59: adamc@1: cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) adamc@1: | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) adamc@83: | LBRACK rconn RBRACK (CRecord rconn, s (LBRACKleft, RBRACKright)) adamc@1: | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)), adamc@1: s (LBRACEleft, RBRACEright)) adamc@1: | DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright)) adamc@1: | HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright)) adamc@1: adamc@34: | path (CVar path, s (pathleft, pathright)) adamc@18: | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) adamc@67: | FOLD (CFold, s (FOLDleft, FOLDright)) adamc@82: | UNIT (CUnit, s (UNITleft, UNITright)) adamc@1: adamc@1: rcon : ([]) adamc@1: | ident EQ cexp ([(ident, cexp)]) adamc@1: | ident EQ cexp COMMA rcon ((ident, cexp) :: rcon) adamc@1: adamc@83: rconn : ident ([(ident, (CUnit, s (identleft, identright)))]) adamc@83: | ident COMMA rconn ((ident, (CUnit, s (identleft, identright))) :: rconn) adamc@83: adamc@1: rcone : ([]) adamc@1: | ident COLON cexp ([(ident, cexp)]) adamc@1: | ident COLON cexp COMMA rcone ((ident, cexp) :: rcone) adamc@1: adamc@1: ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) adamc@34: | SYMBOL (CVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright)) adamc@8: adamc@8: eapps : eterm (eterm) adamc@8: | eapps eterm (EApp (eapps, eterm), s (eappsleft, etermright)) adamc@8: | eapps LBRACK cexp RBRACK (ECApp (eapps, cexp), s (eappsleft, RBRACKright)) adamc@8: adamc@8: eexp : eapps (eapps) adamc@8: | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright)) adamc@8: | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright)) adamc@8: | FN SYMBOL DARROW eexp (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright)) adamc@85: | FN cterm TWIDDLE cterm DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (cterm1left, eexpright)) adamc@8: adamc@8: | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright)) adamc@12: | eterm DOT ident (EField (eterm, ident), s (etermleft, identright)) adamc@8: adamc@8: eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) adamc@8: adamc@34: | path (EVar path, s (pathleft, pathright)) adamc@12: | LBRACE rexp RBRACE (ERecord rexp, s (LBRACEleft, RBRACEright)) adamc@12: adamc@14: | INT (EPrim (Prim.Int INT), s (INTleft, INTright)) adamc@14: | FLOAT (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright)) adamc@14: | STRING (EPrim (Prim.String STRING), s (STRINGleft, STRINGright)) adamc@14: adamc@71: | FOLD (EFold, s (FOLDleft, FOLDright)) adamc@71: adamc@12: rexp : ([]) adamc@12: | ident EQ eexp ([(ident, eexp)]) adamc@12: | ident EQ eexp COMMA rexp ((ident, eexp) :: rexp)