Permalink
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
192 lines (159 sloc) 7.12 KB
entrypoints Module, Clafer, Constraint, Assertion, Goal ;
-- To regenerate grammar (see src/Makefile, the goal 'grammar'):
-- cd src/
-- bnfc -p "Language.Clafer.Front" --ghc clafer.cf
-- happy -gca Language/Clafer/Front/Parclafer.y
-- alex -g Language/Clafer/Front/Lexclafer.x
Module. Module ::= [Declaration] ;
EnumDecl. Declaration ::= "enum" PosIdent "=" [EnumId] ;
ElementDecl. Declaration ::= Element ;
Clafer. Clafer ::= Abstract [TempModifier] GCard PosIdent Super Reference Card Init Transition Elements ;
Constraint. Constraint ::= "[" [Exp] "]" ;
Assertion. Assertion ::= "assert" "[" [Exp] "]";
GoalMinDeprecated. Goal ::= "<<" "min" [Exp] ">>" ;
GoalMaxDeprecated. Goal ::= "<<" "max" [Exp] ">>" ;
GoalMinimize. Goal ::= "<<" "minimize" [Exp] ">>" ;
GoalMaximize. Goal ::= "<<" "maximize" [Exp] ">>" ;
Initial. TempModifier ::= "initial";
Final. TempModifier ::= "final";
FinalRef. TempModifier ::= "finalref";
FinalTarget. TempModifier ::= "finaltarget";
TransitionEmpty. Transition ::= ;
Transition. Transition ::= TransArrow Exp;
AbstractEmpty. Abstract ::= ;
Abstract. Abstract ::= "abstract" ;
ElementsEmpty. Elements ::= ;
ElementsList. Elements ::= "{" [Element] "}" ;
Subclafer. Element ::= Clafer ;
ClaferUse. Element ::= "`" Name Card Elements ;
Subconstraint. Element ::= Constraint ;
Subgoal. Element ::= Goal;
SubAssertion. Element ::= Assertion;
SuperEmpty. Super ::= ;
SuperSome. Super ::= ":" Exp26 ;
ReferenceEmpty. Reference ::= ;
ReferenceSet. Reference ::= "->" Exp23 ;
ReferenceBag. Reference ::= "->>" Exp23 ;
InitEmpty. Init ::= ;
InitSome. Init ::= InitHow Exp ;
InitConstant. InitHow ::= "=" ;
InitDefault. InitHow ::= ":=" ;
GCardEmpty. GCard ::= ;
GCardXor. GCard ::= "xor" ;
GCardOr. GCard ::= "or" ;
GCardMux. GCard ::= "mux" ;
GCardOpt. GCard ::= "opt" ;
GCardInterval. GCard ::= NCard ;
CardEmpty. Card ::= ;
CardLone. Card ::= "?" ;
CardSome. Card ::= "+" ;
CardAny. Card ::= "*" ;
CardNum. Card ::= PosInteger ;
CardInterval. Card ::= NCard ;
NCard. NCard ::= PosInteger ".." ExInteger ;
ExIntegerAst. ExInteger ::= "*" ;
ExIntegerNum. ExInteger ::= PosInteger ;
Path. Name ::= [ModId] ;
-- Transition expressions are right associative and has lowest precedence
TransitionExp. Exp ::= Exp1 TransArrow Exp ;
EDeclAllDisj. Exp1 ::= "all" "disj" Decl "|" Exp1 ;
EDeclAll. Exp1 ::= "all" Decl "|" Exp1 ;
EDeclQuantDisj. Exp1 ::= Quant "disj" Decl "|" Exp1 ;
EDeclQuant. Exp1 ::= Quant Decl "|" Exp1 ;
EImpliesElse. Exp1 ::= "if" Exp1 "then" Exp1 "else" Exp1 ;
LetExp. Exp1 ::= "let" VarBinding "in" Exp1;
TmpPatNever. Exp2 ::= "never" Exp3 PatternScope;
TmpPatSometime. Exp2 ::= "sometime" Exp3 PatternScope;
TmpPatLessOrOnce. Exp2 ::= "lonce" Exp3 PatternScope;
TmpPatAlways. Exp2 ::= "always" Exp3 PatternScope;
TmpPatPrecede. Exp2 ::= Exp3 "must" "precede" Exp3 PatternScope;
TmpPatFollow. Exp2 ::= Exp3 "must" "follow" Exp3 PatternScope;
TmpInitially. Exp2 ::= "initially" Exp3;
TmpFinally. Exp2 ::= "finally" Exp3;
EIff. Exp3 ::= Exp3 "<=>" Exp4 ;
EImplies. Exp4 ::= Exp4 "=>" Exp5 ;
EOr. Exp5 ::= Exp5 "||" Exp6 ;
EXor. Exp6 ::= Exp6 "xor" Exp7 ;
EAnd. Exp7 ::= Exp7 "&&" Exp8 ;
LtlU. Exp8 ::= Exp8 "U" Exp9 ;
TmpUntil. Exp8 ::= Exp8 "until" Exp9 ;
LtlW. Exp9 ::= Exp9 "W" Exp10 ;
TmpWUntil. Exp9 ::= Exp9 "weakuntil" Exp10 ;
LtlF. Exp10 ::= "F" Exp10 ;
TmpEventually. Exp10 ::= "eventually" Exp10 ;
LtlG. Exp10 ::= "G" Exp10 ;
TmpGlobally. Exp10 ::= "globally" Exp10 ;
LtlX. Exp10 ::= "X" Exp10 ;
TmpNext. Exp10 ::= "next" Exp10 ;
ENeg. Exp11 ::= "!" Exp11 ;
ELt. Exp15 ::= Exp15 "<" Exp16 ;
EGt. Exp15 ::= Exp15 ">" Exp16 ;
EEq. Exp15 ::= Exp15 "=" Exp16 ;
ELte. Exp15 ::= Exp15 "<=" Exp16 ;
EGte. Exp15 ::= Exp15 ">=" Exp16 ;
ENeq. Exp15 ::= Exp15 "!=" Exp16 ;
EIn. Exp15 ::= Exp15 "in" Exp16 ;
ENin. Exp15 ::= Exp15 "not" "in" Exp16 ;
EQuantExp. Exp16 ::= Quant Exp20 ;
EAdd. Exp17 ::= Exp17 "+" Exp18 ;
ESub. Exp17 ::= Exp17 "-" Exp18 ;
EMul. Exp18 ::= Exp18 "*" Exp19 ;
EDiv. Exp18 ::= Exp18 "/" Exp19 ;
ERem. Exp18 ::= Exp18 "%" Exp19 ;
EGMax. Exp19 ::= "max" Exp20 ;
EGMin. Exp19 ::= "min" Exp20 ;
ESum. Exp20 ::= "sum" Exp21;
EProd. Exp20 ::= "product" Exp21;
ECard. Exp20 ::= "#" Exp21 ;
EMinExp. Exp20 ::= "-" Exp21 ;
EDomain. Exp21 ::= Exp21 "<:" Exp22 ;
ERange. Exp22 ::= Exp22 ":>" Exp23 ;
EUnion. Exp23 ::= Exp23 "++" Exp24 ;
EUnionCom. Exp23 ::= Exp23 "," Exp24 ;
EDifference. Exp24 ::= Exp24 "--" Exp25 ;
EIntersection. Exp25 ::= Exp25 "**" Exp26 ;
EIntersectionDeprecated. Exp26 ::= Exp26 "&" Exp27 ;
EJoin. Exp26 ::= Exp26 "." Exp27 ;
ClaferId. Exp27 ::= Name ;
EInt. Exp27 ::= PosInteger ;
EDouble. Exp27 ::= PosDouble ;
EReal. Exp27 ::= PosReal ;
EStr. Exp27 ::= PosString ;
TransGuard. TransGuard ::= Exp1;
SyncTransArrow. TransArrow ::= "-->>";
GuardedSyncTransArrow. TransArrow ::= "-[" TransGuard "]->>";
NextTransArrow. TransArrow ::= "-->";
GuardedNextTransArrow. TransArrow ::= "-[" TransGuard "]->";
PatScopeBefore. PatternScope ::= "before" Exp11 ;
PatScopeAfter. PatternScope ::= "after" Exp11 ;
PatScopeBetweenAnd. PatternScope ::= "between" Exp11 "and" Exp11 ;
PatScopeAfterUntil. PatternScope ::= "after" Exp11 "until" Exp11 ;
PatScopeEmpty. PatternScope ::= ;
Decl. Decl ::= [LocId] ":" Exp21 ;
VarBinding. VarBinding ::= LocId "=" Name ;
QuantNo. Quant ::= "no" ;
QuantNot. Quant ::= "not" ;
QuantLone. Quant ::= "lone" ;
QuantOne. Quant ::= "one" ;
QuantSome. Quant ::= "some" ;
EnumIdIdent. EnumId ::= PosIdent ;
ModIdIdent. ModId ::= PosIdent ;
LocIdIdent. LocId ::= PosIdent ;
separator Declaration "" ;
separator nonempty EnumId "|" ;
separator Element "" ;
separator Exp "" ;
separator TempModifier "" ;
separator nonempty LocId ";" ;
separator nonempty ModId "\\" ;
coercions Exp 27 ;
position token PosInteger (digit+) ;
position token PosDouble (digit+ '.' digit+ 'e' '-'? digit+) ;
position token PosReal (digit+ '.' digit+) ;
position token PosString '"' ((char - ["\"\\"]) | ('\\' ["\"\\nt"]))* '"' ;
position token PosIdent (letter (letter|digit|'_'|'\'')*) ;
-- non-parseable tokens
position token PosLineComment {"//"} (char-'\n')* ;
position token PosBlockComment {"/*"} ( (char-'*') | ('*'+ (char-["*/"]) ) )* '*'+ '/' ;
position token PosAlloy {"[alloy|"} ( char-'|' | ('|'+ (char-']')) )* {"|]"} ;
position token PosChoco {"[choco|"} ( char-'|' | ('|'+ (char-']')) )* {"|]"} ;