path: root/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs

using System;
using System.Collections.Generic;
using System.Linq;
using Irony.Parsing;

namespace Demo
{
    [Language("Chalice", "1.0", "Chalice Programming Language")]
    public class Grammar : Irony.Parsing.Grammar
    {
      public Grammar() {
        #region 1. Terminals
        NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");

        IdentifierTerminal ident = new IdentifierTerminal("Identifier");
        /*     v.AddReservedWords("true", "false", "null", "if", "else",
                                "while", "for", "foreach", "in",
                                "switch", "case", "default", "break",
                                "continue", "return", "function", "is",
                                "pre", "post", "invariant", "new"); */
        this.MarkReservedWords(
          "class", "ghost", "var", "const", "method", "channel", "condition",
          "assert", "assume", "new", "this", "reorder",
          "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
          "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned",
          "call", "if", "else", "while",
          "invariant", "lockchange",
          "returns", "requires", "ensures", "where",
          "int", "bool", "false", "true", "null", "waitlevel", "lockbottom",
          "module", "external",
          "predicate", "function", "free", "send", "receive",
          "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
          "seq", "nil", "result", "eval", "token",
          "wait", "signal"
          );

        StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);

        Terminal dot = ToTerm(".", "dot");
        Terminal less = ToTerm("<");
        Terminal greater = ToTerm(">");
        Terminal arrow = ToTerm("->");
        Terminal LBracket = ToTerm("[");
        Terminal RBracket = ToTerm("]");
        Terminal LParen = ToTerm("(");
        Terminal RParen = ToTerm(")");
        Terminal RCurly = ToTerm("}");
        Terminal LCurly = ToTerm("{");
        Terminal LMb = ToTerm("<[");
        Terminal RMb = ToTerm("]>");
        Terminal comma = ToTerm(",");
        Terminal semicolon = ToTerm(";");
        Terminal colon = ToTerm(":");

        #endregion

        #region 2. Non-terminals
        #region 2.1 Expressions
        NonTerminal expression = new NonTerminal("Expr");
        NonTerminal BinOp = new NonTerminal("BinOp");
        NonTerminal LUnOp = new NonTerminal("LUnOp");
        NonTerminal RUnOp = new NonTerminal("RUnOp");

        NonTerminal ArrayConstructor = new NonTerminal("ArrayConstructor");
        NonTerminal MObjectConstructor = new NonTerminal("MObjectConstructor");
        NonTerminal MObjectList = new NonTerminal("MObjectList");
        #endregion

        #region 2.2 QualifiedName
        //Expression List:  expr1, expr2, expr3, ..
        NonTerminal expressionList = new NonTerminal("ExprList");
        NonTerminal identList = new NonTerminal("identList");
        //A name in form: a.b.c().d[1,2].e ....
        NonTerminal NewStmt = new NonTerminal("NewStmt");
        NonTerminal NewArrStmt = new NonTerminal("NewArrStmt");
        NonTerminal QualifiedName = new NonTerminal("QualifiedName");
        NonTerminal AccessQualName = new NonTerminal("AccessQualName");
        NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix");
        NonTerminal ArrayExpression = new NonTerminal("ArrayExpression");
        NonTerminal FunctionExpression = new NonTerminal("FunctionExpression");
        NonTerminal selectExpr = new NonTerminal("selectExpr");
        NonTerminal accessExpr = new NonTerminal("accessExpr");
        #endregion

        #region 2.3 Statement
        NonTerminal Condition = new NonTerminal("Condition");

        NonTerminal Statement = new NonTerminal("Statement");
        NonTerminal Statements = new NonTerminal("Statements");

        //Block
        NonTerminal blockStatement = new NonTerminal("CompoundStatement");
        #endregion

        #region 2.4 Program and Functions
        NonTerminal Prog = new NonTerminal("Prog");
        NonTerminal declaration = new NonTerminal("declaration");
        NonTerminal classDecl = new NonTerminal("class decl");
        NonTerminal memberDecl = new NonTerminal("member decl");
        NonTerminal fieldDecl = new NonTerminal("field declaration");
        NonTerminal idType = new NonTerminal("identifier type");
        NonTerminal typeDecl = new NonTerminal("type reference");
        NonTerminal methodDecl = new NonTerminal("method declaration");
        NonTerminal formalParameters = new NonTerminal("formals");
        NonTerminal methodSpec = new NonTerminal("method spec");
        NonTerminal formalsList = new NonTerminal("ParamaterListOpt");
        NonTerminal functionDecl = new NonTerminal("function declaration");
        NonTerminal predicateDecl = new NonTerminal("predicate declaration");
        NonTerminal invariantDecl = new NonTerminal("invariant declaration");
        NonTerminal Semi = new NonTerminal("semi");
        NonTerminal Rhs = new NonTerminal("right-hand side");
        NonTerminal FieldInit = new NonTerminal("field init");
        NonTerminal FieldInits = new NonTerminal("field inits");
        NonTerminal installBounds = new NonTerminal("installBounds");
        NonTerminal localVarStmt = new NonTerminal("localVarStmt");
        NonTerminal evalstate = new NonTerminal("evalstate");
        NonTerminal channelDecl = new NonTerminal("channel declaration");
        NonTerminal loopSpec = new NonTerminal("loop specification");
        NonTerminal rdPermArg = new NonTerminal("rdPermArg");
        #endregion

        #endregion

        #region 3. BNF rules

        Semi.Rule = semicolon;

        #region 3.1 Expressions
        selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName;
        accessExpr.Rule = (ToTerm("this") + ".").Q() + AccessQualName;
        evalstate.Rule =
          ident + ToTerm(".") +
          (ToTerm("acquire")
          | "release"
          | "fork" + FunctionExpression
          )
          ;
        rdPermArg.Rule = ToTerm("*") | expression;

        expression.Rule = ToTerm("true")
                    | "false"
                    | "null"
                    | "waitlevel"
                    | "lockbottom"
                    | "this"
                    | "result"
                    | s
                    | n
                    | QualifiedName
          // The following is needed: to parse "A<B ..." either as comparison or as beginning of GenericsPostfix
                    | QualifiedName + less + expression
                    //| QualifiedName + less + QualifiedName + greater
                    //| NewStmt
                    | NewArrStmt
                    | ArrayExpression
                    | FunctionExpression
                    | ArrayConstructor
                    | MObjectConstructor
                    | expression + BinOp + expression
                    | LUnOp + expression
                    | expression + RUnOp
                    | LMb + declaration.Star() + RMb
                    | LParen + expression + RParen
                    | ToTerm("unfolding") + expression + "in" + expression
                    | ToTerm("acc") + "(" + accessExpr  + (("," + expression) | Empty) + ")"
                    | ToTerm("old") + "(" + expression + ")"
                    | ToTerm("eval") + "(" + evalstate + "," + expression + ")"
                    | ToTerm("credit") + "(" + expression + "," + expression + ")"
                    | ToTerm("credit") + "(" + expression + ")"
                    | expression + PreferShiftHere() + "?" + expression + ":" + expression
                    | ToTerm("rd") +
                      (ToTerm("holds") + "(" + expression + ")"
                      | "(" + accessExpr + rdPermArg.Q() + ")"
                      )

                    ;
        expressionList.Rule = MakePlusRule(expressionList, comma, expression);
        identList.Rule = MakePlusRule(identList, comma, ident);
        NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen;
        NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket;
        BinOp.Rule = ToTerm("+") | "-" | "*" | "/" | "%" | "^" | "&" | "|"
                    | "&&" | "||" | "==" | "!=" | greater | less
                    | ">=" | "<=" | "is"
                    | "=" | "+=" | "-="
                    | "."
                    | "==>" | "<==>" | "<<"
                    ;

        LUnOp.Rule = ToTerm("-") | "~" | "!";
        RUnOp.Rule = ToTerm("++") | "--";

        ArrayConstructor.Rule = LBracket + expressionList + RBracket;
        MObjectConstructor.Rule = LBracket + ident + arrow + expression + MObjectList.Star() + RBracket;
        MObjectList.Rule = comma + ident + arrow + expression;
        #endregion

        #region 3.2 QualifiedName
        ArrayExpression.Rule = QualifiedName + LBracket + expressionList + RBracket;
        FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen;

        QualifiedName.Rule = ident | QualifiedName + dot + ident;
        AccessQualName.Rule = ident | "*" | QualifiedName + dot + (ident | "*");


        GenericsPostfix.Rule = less + QualifiedName + greater;

        //ExprList.Rule = Expr.Plus(comma);
        #endregion

        #region 3.3 Statement
        Condition.Rule = LParen + expression + RParen;
        installBounds.Rule
          = "installBounds"
          //= ToTerm("between") + expressionList + "and" + expressionList
          //| "below" + expressionList
          //| "below" + expressionList + "above" + expressionList
          //| "above" + expressionList
          //| "above" + expressionList + "below" + expressionList
          ;
        FieldInit.Rule
          = ident + ":=" + expression
          ;
        FieldInits.Rule = MakeStarRule(FieldInits, ToTerm(","), FieldInit);
        Rhs.Rule
          = ToTerm("new") + ident
          | ToTerm("new") + ident + "{" + FieldInits + "}"
          | ToTerm("new") + ident + installBounds
          | ToTerm("new") + ident + "{" + FieldInits + "}" + installBounds
          | expression
          ;
        localVarStmt.Rule
          = idType + ":=" + Rhs + Semi
          | idType + Semi
          ;
        loopSpec.Rule
          = ToTerm("invariant") + expression + Semi
          | "lockchange" + expressionList + Semi
          ;



        Statement.Rule = Semi
                        | "if" + Condition + Statement
                        | "if" + Condition + Statement + PreferShiftHere() + "else" + Statement
                        | "while" + Condition + loopSpec.Star() + Statement
                        | "for" + LParen + expression.Q() + Semi + expression.Q() + Semi + expression.Q() + RParen + Statement
                        | "foreach" + LParen + ident + "in" + expression + RParen + Statement
                        | blockStatement
                        | expression + Semi
                        | "break" + Semi
                        | "continue" + Semi
                        | "return" + expression + Semi
                        | QualifiedName + ":=" + Rhs

                        | "var" + localVarStmt
                        | "const" + localVarStmt

                        | "call" + identList + ":=" + FunctionExpression + Semi
                        | "call" + FunctionExpression + Semi
                        | "assert" + expression + Semi
                        | "assume" + expression + Semi
                        | "unshare" + expression + Semi
                        | "lock" + Condition + Statement
                        | "[[" + Statements + "]]"
                        | "acquire" + expression + Semi
                        | "release" + expression + Semi
                        | "downgrade" + expression + Semi
                        | "free" + expression + Semi
                        | "fold" + expression + Semi
                        | "unfold" + expression + Semi
                        | "reorder" + expression + installBounds + Semi
                        | "reorder" + expression + Semi
                        | "share" + expression + installBounds + Semi
                        | "share" + expression + Semi
                        | "fork" + identList + ":=" + FunctionExpression + Semi
                        | "fork" + FunctionExpression + Semi
                        | "join" + identList + ":=" + expression + Semi
                        | "join" + expression + Semi
                        | "send" + expression + Semi
                        | "receive" + identList + ":=" + expression + Semi
                        | "receive" + expression + Semi

                        ;
        Statements.Rule = MakeStarRule(Statements, null, Statement);
        blockStatement.Rule = LCurly + Statements + RCurly;


        #endregion

        #region 3.4 Prog
        Prog.Rule = declaration.Star() + Eof;
        idType.Rule
          = ident + ":" + typeDecl
          | ident
          ;

        typeDecl.Rule
          = (ToTerm("int") | "bool" | ident | "seq") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty)
          | ToTerm("token") + "<" + (typeDecl + ".") + ident + ">"
          ;

        fieldDecl.Rule
          = ToTerm("var") + idType + Semi
          | ToTerm("ghost") + "var" + idType + Semi
          ;

        methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi;

        formalsList.Rule = MakeStarRule(formalsList, comma, idType);
        formalParameters.Rule = LParen + formalsList + RParen;
        methodDecl.Rule = "method" + ident + formalParameters
          + (("returns" + formalParameters) | Empty)
          + methodSpec.Star()
          + blockStatement;
        functionDecl.Rule
          = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}";
        predicateDecl.Rule
          = ToTerm("predicate") + ident + "{" + expression + "}";
        invariantDecl.Rule
          = ToTerm("invariant") + expression + Semi;

        memberDecl.Rule
          = fieldDecl
          | invariantDecl
          | methodDecl
          //| conditionDecl
          | predicateDecl
          | functionDecl
          ;
        classDecl.Rule
          = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}";
        channelDecl.Rule
          = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi
          | ToTerm("channel") + ident + formalParameters + Semi;
        declaration.Rule = classDecl | channelDecl
          ;


        Terminal Comment = new CommentTerminal("Comment", "/*", "*/");
        NonGrammarTerminals.Add(Comment);
        Terminal LineComment = new CommentTerminal("LineComment", "//", "\n");
        NonGrammarTerminals.Add(LineComment);
        #endregion
        #endregion

        #region 4. Set starting symbol
        this.Root = Prog; // Set grammar root
        #endregion

        #region 5. Operators precedence
        RegisterOperators(1, "=", "+=", "-=");
        RegisterOperators(2, "+", "-");
        RegisterOperators(3, "*", "/", "%");
        RegisterOperators(4, Associativity.Right, "^");
        RegisterOperators(5, "|", "||");
        RegisterOperators(6, "&", "&&");
        RegisterOperators(7, "==", "!=", ">", "<", ">=", "<=", "<<");
        RegisterOperators(8, "is");
        RegisterOperators(9, "~", "!", "++", "--");
        RegisterOperators(10, "==>", "<==>");
        RegisterOperators(11, ".");

        //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}");
        //RegisterOperators(11, Associativity.Right, "else");
        #endregion

        #region 6. Punctuation symbols
        RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";");
        #endregion
      }
    }
}