uppaal.grm

(* $Id$
 *
 * Copyright (c) 2008 Timothy Bourke (University of NSW and NICTA)
 * All rights reserved.
 *
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the "BSD License" which is distributed with the
 * software in the file LICENSE.
 *
 * This program is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the BSD
 * License for more details.
 *
 * Based on the Uppaal Timed Automata Parser Library documentation.
 * http://www.cs.auc.dk/~behrmann/utap/syntax.html 20070424
 *
 * TODO:
 * - Build lists in order?
 *   Or build and then reverse?
 * - Rename rules to match C standard (where applicable).
 *)

structure E = Expression
structure D = Declaration

type symbol = Atom.atom

val boundsToType : E.ty -> E.unresolvedty list -> E.ty
    = foldl (fn (sub, ty) => E.ARRAY (ty, sub))

fun expandIdDecls (baseType : E.ty,
                   names : ((symbol * E.unresolvedty list) list))
                  (*    id____/         \__array bounds (opt.) *)
    : (symbol * E.ty) list
  = let
    val wrap = boundsToType baseType
  in
    map (fn (id, bounds) => (id, wrap bounds)) names
  end

fun dbg xs = Util.debugVeryDetailed (fn ()=>xs)

                                            (* could be type abbr. *)
fun checkUnresolved (E.VarExpr (E.SimpleVar s)) = E.Unresolved s
            (* subtract one because int[l, u] bounds are inclusive *) 
  | checkUnresolved (E.IntCExpr n) = E.Type (E.INT (SOME (E.IntCExpr 0,
                                                          E.IntCExpr (n - 1)),
                                                    E.NoQual))
  | checkUnresolved e = E.Type (E.INT (SOME (E.IntCExpr 0,
                             E.BinIntExpr {left=e, bop=E.MinusOp,
                                           right=E.IntCExpr 1}), E.NoQual))

%%
%name Uppaal
%eop EOF
%pos FilePos.pos
%pure
%noshift EOF
%verbose

%header (functor UppaalLrFun
                       (structure Token      : TOKEN
                        structure FilePos    : FILE_POS
                        structure Expression : EXPRESSION
                        structure Declaration : DECLARATION
                          sharing type Declaration.pos  = FilePos.pos
                          sharing type Declaration.ty   = Expression.ty
                          sharing type Declaration.expr = Expression.expr
                        structure Result : RESULT
                          sharing type Result.expr = Expression.expr
                          sharing type Result.boundid = Expression.boundid
                          sharing type Result.direction = Expression.direction
                          sharing type Result.decl = Declaration.decl
                          sharing type Result.param = Declaration.param
                       ))

%term PARSEEXPR | PARSEDECL | PARSESELECT | PARSESYNC |
      PARSEEXPRLIST | PARSEPARAMS |  (* ML-Yacc man. 10.1 *)
      ID of Atom.atom | INTEGER of int |
      VOID | INT | BOOL | SCALAR | TYPEDEF | CLOCK | CHAN |
      TRUE | FALSE |
      LPAR | RPAR | LSQPAR | RSQPAR | LBRACE | RBRACE |
      QUESTION | COLON | SEMICOLON | DOT | COMMA |
      EXCLAM | UMINUS |
      PLUSPLUS | MINUSMINUS | MINUS |
      PLUS | TIMES | DIVIDE | MOD |
      AMPERSAND | BITOR | BITXOR |
      SHLEFT | SHRIGHT | LT | LE | EQ | NEQ | GE | GT | MIN | MAX |
      DBLAMPERSAND | DBLPIPE | AND | OR | IMPLY | FORALL | EXISTS | NOT |
      ASSIGNMENT | PLUSASSIGN | MINUSASSIGN | TIMESASSIGN | DIVIDEASSIGN |
      MODASSIGN | BITORASSIGN | BITANDASSIGN | BITXORASSIGN |
      SHLEFTASSIGN | SHRIGHTASSIGN |
      STRUCT | URGENT | BROADCAST | CONST |
      FOR | WHILE | DO | IF | ELSE | BREAK | CONTINUE | SWITCH |
      RETURN | CASE | DEFAULT | UNKNOWN | EOF |
      COMMIT | INIT | PROCESS | STATE | GUARD | SYNC |
      ASSIGN | SYSTEM | TRANS | DEADLOCK | RATE | BEFORE_UPDATE |
      AFTER_UPDATE | META | PRIORITY | PROGRESS | SELECT

(* Table 2-1, Kernighan and Ritchie, The C Programming Language 2ed.
   listed in order of increasing (tighter binding) precedence *)
%left  COMMA
%left  FORALL EXISTS
%left  IMPLY OR
%left  AND
%right NOT
%right ASSIGNMENT PLUSASSIGN MINUSASSIGN TIMESASSIGN DIVIDEASSIGN MODASSIGN
       BITORASSIGN BITANDASSIGN BITXORASSIGN SHLEFTASSIGN SHRIGHTASSIGN
%right QUESTION COLON
%left  DBLPIPE
%left  DBLAMPERSAND
%left  BITOR
%left  BITXOR
%left  AMPERSAND (*BITAND*)
%left  EQ NEQ
%left  LT LE GE GT
%left  MIN MAX
%left  SHLEFT SHRIGHT
%left  PLUS MINUS
%left  TIMES DIVIDE MOD
%right EXCLAM UMINUS PLUSPLUS MINUSMINUS
%left  DOT
                            
%nonterm start         of Result.t
       | expr          of E.expr
       | exprs         of E.expr list
       | varExpr       of E.var
       | assignOp      of E.assignOp
       | argList       of E.expr list
       | args          of E.expr list
       | typeExpr      of E.ty
       | typePrefix    of E.tyqual
       | fieldDecl     of (symbol * E.ty) list
       | fieldDecls    of (symbol * E.ty) list
       | idDecl        of symbol * E.unresolvedty list
       | idDecls       of (symbol * E.unresolvedty list) list
       | tyDeclExpr    of E.unresolvedty
       | tyDeclSubs    of E.unresolvedty list
       | declarations  of D.decl list
       | subscripts    of E.expr list
       | varDecl       of D.decl list
       | varIDs        of (E.ty -> D.decl) list
       | varID         of E.ty -> D.decl (* inherit base type *)
       | initialiser   of D.initialiser
       | initialisers  of D.initialiser list
       | typeDecl      of D.decl list
       | function      of D.decl
       | params        of D.param list
       | param         of D.param
       | stmtlist      of D.stmt list
       | block         of D.stmt
       | blockcontent  of D.decl list * D.stmt list
       | stmt          of D.stmt
       | chanPriority  of D.decl
       | chanOrd       of D.chanexpr list list
       | chanSame      of D.chanexpr list
       | chanExpr      of D.chanexpr
       | selectList    of E.boundid list
       | syncLabel     of symbol * E.direction * E.expr list

%keyword STRUCT FOR WHILE DO IF ELSE BREAK CONTINUE SWITCH RETURN CASE DEFAULT
         TYPEDEF
%value ID  (Atom.atom "dummy")
%value INTEGER (0)

%%

start: PARSEEXPR expr         (Result.Expr expr)
     | PARSEDECL declarations (Result.Decls declarations)
     | PARSESELECT selectList (Result.Select selectList)
     | PARSESYNC syncLabel    (Result.Sync syncLabel)
     | PARSEEXPRLIST exprs    (Result.ExprList exprs)
     | PARSEPARAMS params     (Result.Params params)

expr: varExpr             (E.VarExpr varExpr)
    | INTEGER             (E.IntCExpr INTEGER)
    | TRUE                (E.BoolCExpr true)
    | FALSE               (E.BoolCExpr false)
    | ID LPAR args RPAR   (E.CallExpr {func=ID, args=args})
                          (* see also: varExpr *)
    | LPAR expr RPAR      (expr)
    | expr PLUSPLUS       (E.UnaryModExpr {uop=E.PostIncOp, expr=expr})
    | PLUSPLUS expr       (E.UnaryModExpr {uop=E.PreIncOp, expr=expr})
    | expr MINUSMINUS     (E.UnaryModExpr {uop=E.PostDecOp, expr=expr})
    | MINUSMINUS expr     (E.UnaryModExpr {uop=E.PreDecOp, expr=expr})

    | MINUS expr %prec UMINUS (E.NegExpr expr)
    | EXCLAM expr         (E.NotExpr expr)
    | NOT expr            (E.NotExpr expr)

    | expr LT expr        (E.RelExpr {left=expr1, rel=E.LtOp, right=expr2})
    | expr LE expr        (E.RelExpr {left=expr1, rel=E.LeOp, right=expr2})
    | expr EQ expr        (E.RelExpr {left=expr1, rel=E.EqOp, right=expr2})
    | expr NEQ expr       (E.RelExpr {left=expr1, rel=E.NeOp, right=expr2})
    | expr GE expr        (E.RelExpr {left=expr1, rel=E.GeOp, right=expr2})
    | expr GT expr        (E.RelExpr {left=expr1, rel=E.GtOp, right=expr2})

    | expr PLUS expr      (E.BinIntExpr {left=expr1,bop=E.PlusOp, right=expr2})
    | expr MINUS expr     (E.BinIntExpr {left=expr1,bop=E.MinusOp, right=expr2})
    | expr TIMES expr     (E.BinIntExpr {left=expr1,bop=E.TimesOp, right=expr2})
    | expr DIVIDE expr    (E.BinIntExpr {left=expr1,bop=E.DivideOp,right=expr2})
    | expr MOD expr       (E.BinIntExpr {left=expr1,bop=E.ModOp, right=expr2})
    | expr AMPERSAND expr (E.BinIntExpr {left=expr1,bop=E.BAndOp, right=expr2})
    | expr BITOR expr     (E.BinIntExpr {left=expr1,bop=E.BOrOp, right=expr2})
    | expr BITXOR expr    (E.BinIntExpr {left=expr1,bop=E.BXorOp, right=expr2})
    | expr SHLEFT expr    (E.BinIntExpr {left=expr1,bop=E.ShlOp, right=expr2})
    | expr SHRIGHT expr   (E.BinIntExpr {left=expr1,bop=E.ShrOp, right=expr2})
    | expr MIN expr       (E.BinIntExpr {left=expr1,bop=E.MinOp, right=expr2})
    | expr MAX expr       (E.BinIntExpr {left=expr1,bop=E.MaxOp, right=expr2})

    | expr DBLAMPERSAND expr (E.BinBoolExpr{left=expr1,bop=E.AndOp,right=expr2})
    | expr AND expr       (E.BinBoolExpr {left=expr1,bop=E.AndOp, right=expr2})
    | expr DBLPIPE expr   (E.BinBoolExpr {left=expr1,bop=E.OrOp, right=expr2})
    | expr OR expr        (E.BinBoolExpr {left=expr1,bop=E.OrOp, right=expr2})
    | expr IMPLY expr     (E.BinBoolExpr {left=expr1,bop=E.ImplyOp,right=expr2})

    | expr QUESTION expr COLON expr
                        (E.CondExpr {test=expr1,trueexpr=expr2,falseexpr=expr3})

    | expr assignOp expr   %prec ASSIGNMENT
                        (E.AssignExpr {var=expr1,aop=assignOp,expr=expr2})

    | FORALL LPAR ID COLON typeExpr RPAR expr %prec FORALL
                              (E.ForAllExpr  {id=ID, ty=typeExpr, expr=expr})
    | EXISTS LPAR ID COLON typeExpr RPAR expr %prec EXISTS
                              (E.ExistsExpr  {id=ID, ty=typeExpr, expr=expr})
    | DEADLOCK                (E.Deadlock)

exprs: expr                   ([expr])
     | expr COMMA exprs       (expr::exprs)

varExpr: ID                         (E.SimpleVar ID)
       | ID LPAR args RPAR DOT ID   (E.RecordVar (
                                      E.ReturnVar {func=ID1, args=args}, ID))
       | varExpr LSQPAR expr RSQPAR (E.SubscriptVar (varExpr, expr))
       | varExpr DOT ID             (E.RecordVar (varExpr, ID))

assignOp: ASSIGNMENT      (E.AssignOp)
        | PLUSASSIGN      (E.PlusEqOp)
        | MINUSASSIGN     (E.MinusEqOp)
        | TIMESASSIGN     (E.TimesEqOp)
        | DIVIDEASSIGN    (E.DivideEqOp)
        | MODASSIGN       (E.ModEqOp)
        | BITORASSIGN     (E.BOrEqOp)
        | BITANDASSIGN    (E.BAndEqOp)
        | BITXORASSIGN    (E.BXorEqOp)
        | SHLEFTASSIGN    (E.ShlEqOp)
        | SHRIGHTASSIGN   (E.ShrEqOp)

args: (* empty *)               ([])
    | argList                   (argList)

argList: expr                    ([expr])
       | expr COMMA argList      (expr :: argList)

typeExpr: typePrefix INT          (E.INT (NONE, typePrefix))
        | typePrefix INT LSQPAR expr COMMA expr RSQPAR
                                  (E.INT (SOME (expr1, expr2), typePrefix))
        | typePrefix BOOL         (E.BOOL typePrefix)
        | typePrefix ID           (E.NAME (ID, typePrefix, NONE))
        | typePrefix SCALAR LSQPAR expr RSQPAR
                                  (E.SCALAR (expr, typePrefix, E.uniqueTag()))
        | CLOCK                   (E.CLOCK)
        | VOID                    (E.VOID)
        | URGENT CHAN             (E.CHANNEL {urgent=true, broadcast=false})
        | URGENT BROADCAST CHAN   (E.CHANNEL {urgent=true, broadcast=true})
        | BROADCAST CHAN          (E.CHANNEL {urgent=false, broadcast=true})
        | CHAN                    (E.CHANNEL {urgent=false, broadcast=false})
        | typePrefix STRUCT LBRACE fieldDecls RBRACE
                                  (E.RECORD (fieldDecls, typePrefix,
                                             E.uniqueTag()))

        (* Allowing an empty typePrefix gives reduce/reduce conflicts. *)
        | INT                     (E.INT (NONE, E.NoQual))
        | INT LSQPAR expr COMMA expr RSQPAR
                                  (E.INT (SOME (expr1, expr2), E.NoQual))
        | BOOL                    (E.BOOL E.NoQual)
        | ID                      (E.NAME (ID, E.NoQual, NONE))
        | SCALAR LSQPAR expr RSQPAR (E.SCALAR (expr, E.NoQual, E.uniqueTag()))
        | STRUCT LBRACE fieldDecls RBRACE
                                  (E.RECORD (fieldDecls, E.NoQual,
                                             E.uniqueTag()))

typePrefix: META                  (E.Meta)
          | CONST                 (E.Const)

fieldDecls: fieldDecl             (fieldDecl)
          | fieldDecls fieldDecl  (fieldDecl @ fieldDecls)

fieldDecl: typeExpr idDecls SEMICOLON (expandIdDecls (typeExpr, idDecls))

idDecls: idDecl                   ([idDecl])
       | idDecls COMMA idDecl     (idDecl :: idDecls)

idDecl: ID tyDeclSubs             ((ID, tyDeclSubs))

tyDeclExpr: expr            (checkUnresolved expr)
          | INT LSQPAR expr COMMA expr RSQPAR
                            (E.Type (E.INT (SOME (expr1, expr2), E.NoQual)))
          | SCALAR LSQPAR expr RSQPAR
                            (E.Type (E.SCALAR (expr, E.NoQual, E.uniqueTag())))

tyDeclSubs: (* empty *)                           ([])
          | LSQPAR tyDeclExpr RSQPAR tyDeclSubs   (tyDeclExpr :: tyDeclSubs)

declarations: (* empty *)               ([])
            | varDecl declarations      (varDecl @ declarations)
            | typeDecl declarations     (typeDecl @ declarations)
            | function declarations     (function :: declarations)
            | chanPriority declarations (chanPriority :: declarations)

varDecl: typeExpr varIDs SEMICOLON      (map (fn f => f typeExpr) varIDs)

varIDs: varID                           ([varID])
      | varID COMMA varIDs              (varID::varIDs)

varID: ID tyDeclSubs                    (fn baseTy => D.VarDecl {id=ID,
                                         ty=boundsToType baseTy tyDeclSubs,
                                         initial=NONE, pos=IDleft})
     | ID tyDeclSubs ASSIGNMENT initialiser (fn baseTy =>
                      D.VarDecl {id=ID, ty=boundsToType baseTy tyDeclSubs,
                                     initial=SOME initialiser, pos=IDleft})

initialiser: expr                            (D.SimpleInit expr)
     | LBRACE initialisers RBRACE            (D.ArrayInit initialisers)

initialisers: initialiser                    ([initialiser])
            | initialiser COMMA initialisers (initialiser::initialisers)

typeDecl: TYPEDEF typeExpr idDecls SEMICOLON
                                      (map (fn (id, ty) => D.TyDecl {id=id,
                                                    ty=ty, pos=TYPEDEFleft})
                                         (expandIdDecls (typeExpr, idDecls)))

function: typeExpr ID LPAR params RPAR block
                                      (D.FunDecl {id=ID, rty=typeExpr,
                                       params=params, body=block, pos=IDleft})

params: (* empty *)                     ([])
      | param                           ([param])
      | param COMMA params              (param::params)

param: typeExpr ID tyDeclSubs           (D.ValParam {id=ID,ty=boundsToType
                                                     typeExpr tyDeclSubs})
     | typeExpr AMPERSAND ID tyDeclSubs (D.RefParam {id=ID,ty=boundsToType
                                                     typeExpr tyDeclSubs})

block: LBRACE blockcontent RBRACE       (D.BlockStmt {decls=(#1 blockcontent),
                                                      body=(#2 blockcontent)})

blockcontent: (* empty *)               (([], []))
            | stmtlist                  (([], stmtlist))
            | varDecl blockcontent      ((varDecl @ (#1 blockcontent),
                                          #2 blockcontent))
            | typeDecl blockcontent     ((typeDecl @ (#1 blockcontent),
                                          #2 blockcontent))
            | function blockcontent     ((function :: (#1 blockcontent),
                                          #2 blockcontent))
            | chanPriority blockcontent ((chanPriority::(#1 blockcontent),
                                          #2 blockcontent))

stmtlist: stmt                          ([stmt])
        | stmt stmtlist                 (stmt::stmtlist)

stmt: block                             (block)
    | SEMICOLON                         (D.NothingStmt)
    | expr SEMICOLON                    (D.ExprStmt (expr, exprleft))
    | FOR LPAR exprs SEMICOLON exprs SEMICOLON exprs RPAR stmt
                                        (D.ForStmt {init=exprs1, cond=exprs2,
                                         step=exprs3, body=stmt, pos=FORleft})
    | FOR LPAR ID COLON typeExpr RPAR stmt  (D.IterateStmt {id=ID, ty=typeExpr,
                                               body=stmt, pos=FORleft})
    | WHILE LPAR exprs RPAR stmt         (D.WhileStmt {cond=exprs,
                                            body=stmt, pos=WHILEleft})
    | DO stmt WHILE LPAR exprs RPAR      (D.DoWhileStmt {cond=exprs,
                                            body=stmt, pos=DOleft})
    | IF LPAR exprs RPAR stmt            (D.IfStmt {cond=exprs, thenb=stmt,
                                          elseb=D.NothingStmt, pos=IFleft})
    | IF LPAR exprs RPAR stmt ELSE stmt  (D.IfStmt {cond=exprs, thenb=stmt1,
                                                    elseb=stmt2, pos=IFleft})
    | RETURN SEMICOLON                  (D.Return (NONE, RETURNleft))
    | RETURN expr SEMICOLON             (D.Return (SOME expr, RETURNleft))

chanPriority: CHAN PRIORITY chanOrd SEMICOLON
                                        (D.ChanPriDecl (chanOrd, CHANleft))

chanOrd: chanSame                       ([chanSame])
       | chanSame LT chanOrd            (chanSame::chanOrd)

chanSame: chanExpr                      ([chanExpr])
        | DEFAULT                       ([D.ChanDefault])
        | chanExpr COMMA chanSame       (chanExpr::chanSame)
        | DEFAULT COMMA chanSame        (D.ChanDefault::chanSame)

chanExpr: ID                            (D.ChanSingle ID)
        | chanExpr LSQPAR expr RSQPAR   (D.ChanArray (chanExpr, expr))

selectList : ID COLON typeExpr          ([E.BoundId (ID, typeExpr)])
           | ID COLON typeExpr COMMA selectList
                            (E.BoundId (ID, typeExpr) :: selectList)

syncLabel : ID subscripts QUESTION        (ID, E.Input, subscripts)
          | ID subscripts EXCLAM          (ID, E.Output, subscripts)

subscripts: (* empty *)                     ([])
          | LSQPAR expr RSQPAR subscripts   (expr :: subscripts)