(Message dnj:1526)
Date: Thu, 01 Nov 2001 18:01:44 EST
To: alloy-dev@geyer.lcs.mit.edu
From: Manu Sridharan <msridhar@MIT.EDU>
Subject: updated alloy grammar

Return-Path: <msridhar@MIT.EDU>
X-Sender: msridhar@hesiod (Unverified)
X-Mailer: QUALCOMM Windows Eudora Version 5.0.2
Mime-Version: 1.0
Content-Type: multipart/mixed;
	      boundary="=====================_359459275==_"

here's a readable Alloy grammar corresponding to what is currentlly 
parsed.  it probably could be cleaned up in some ways, but in any case it 
should be correct.

-manuGrammar
-------
module ::= moduleDecl import* paragraph*
moduleDecl ::= "module" [ packageName / ] moduleName
moduleName ::= id
packageName ::= dir*  id
dir ::= id /
import ::= ("open" | "uses") packageSpecifier
packageSpecifier ::= packageName [ / "*" ]

paragraph ::= signature | fact | assertion | function | run | check | eval

signature ::= [ "static" ] qualifier* "sig" signame [ typeparams ] [ extension ] "{" decl,... "}" [ formulaseq ]
typeparams ::= "[" typeparam,... "]"
extension ::= "extends" sig,...
fact ::= "fact" [ paraname ] [ typeparams ] formulaseq
assertion ::= "assert" [ paraname ]  [ typeparams ] formulaseq
function ::= [ "det" ] "fun" [ thisarg ] paraname  [ typeparams ] "(" [ decl,... ] ")" [ : multexpr ] formulaseq
thisarg ::= sig . | sig ::

run ::= "run"  paraname [ scope ] [ excluded ] [ "expect" number ]
check ::= "check" [ paraname ] [ scope ] [ excluded ] [ "expect" number ]
eval ::= "eval" paraname "using" paraname [ scope ] [ excluded ]
scope ::= "for" [ number "but" ] typescope,...
typescope ::= number (sig | "int")
excluded ::= "without" global,...
global ::= "facts" | "constraints" | paraname

decl ::= var,... compop multexpr | qualifier+ var,... : multexpr
qualifier ::= "part" | "disj" | "exh"
multexpr ::= [ setmult ] expr | expr [ mult ] -> [ mult ] expr
setmult ::= "set" | "option" | "scalar"
letdecl ::= var "=" expr
expr ::= var | sig $ var | expr binop expr | expr "[" expr "]" | unop expr
	| { decl,... [formulabody] }
        | "(" expr ")"
	| invocation | "this" | "result" | sig 
	| "with" expr,... "|" expr
        | "let" letdecl,... "|" expr
	| ("none" | "univ" | "iden") "[" expr "]"
        | "if" formula "then" expr "else" expr
        | "Int" intexpr

invocation ::= [ expr ".." ] paraname ( [ expr,... ] )

intexpr ::= number | "#" expr | "sum" expr | "int" expr 
           | "(" intexpr ")"
           | "if" formula "then" intexpr "else" intexpr
           | intexpr intop intexpr
           | "sum" decl,... "|" intexpr
           | "with" expr,... "|" intexpr
           | "let" letdecl,... "|" intexpr

intop ::= "+" | "-"

formulabody ::= formulaseq | "|" formula
formulaseq ::= { formula* }
formula ::= expr compop expr
        | intexpr intcompop intexpr
        | "(" formula ")"
	| neg formula | formula logicop formula | formula then_op formula [else_op formula]
	| formulaseq
	| quantifier decl,... formulabody
	| "with" expr,... formulabody
        | "let" letdecl,... formulabody
	| quantifier expr
	| invocation

then_op ::= "=>" | "implies"
else_op ::= "else" | ","
	
neg ::= "not" | !
logicop ::= && | "||" | "iff" | <=> | "and" | "or" 
quantifier ::= all | no | some | sole | one | two
binop ::= + | - | & | . | :: | -> 
unop ::= ~ | * | ^
mult ::= ! | ? | +
compop ::= [neg] ( : | = | "in" )
intop ::= [neg] ( = | =< | >= | < | > )

signame ::= ([ packageName "/" ] id) | "Int" 
sig ::= signame | paramsigname | typeparam
paramsigname ::= signame "[" sig,... "]"
paraname ::= id
var ::= id
name ::= id
typeparam ::= id

Precedence and Associativity
----------------------------

Precedence order for formula operators (tightest binding first):
!, &&, =>, <=>, ||

Precedence order for expression operators (tightest binding first):
::, ~/*/^ (transitive closure not union), . , [], ->, &, +/-


Associativity
-, & to the left
:: and . to the left (essential for type inference)
=> to the right
other operators are associative