Mercurial > urweb
view src/lacweb.grm @ 163:80192edca30d
Datatypes through corify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 29 Jul 2008 13:16:21 -0400 |
parents | adc4e42e3adc |
children | a158f8c5aa55 |
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 | 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 | 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 | 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 | 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 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)) | 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)) 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 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)) | 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)) 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)) 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)