-- juno2.prettygrammar
-- Last Edited by: Gnelson, November 7, 1983 2:23 pm

S ::= ProcDef | PredDef | FunDef

Decl ::= new Assignment

	[new Assignment]

Assignment ::= VarID := Term

	[:= VarID Term]

ProcDef ::= Varlist : ProcID(Varlist)  ==  Command

	[== [: Varlist [( ProcID Varlist]] Command]

PredDef ::= PredID(Varlist) == Formula

	[== [( PredID Varlist] Formual]
	
FunDef ::= FunID(Varlist) = VarID  ==  Formula

  [== [= [( FunID Varlist] VarID] Formula]

Varlist ::=  VarID | VarID, Varlist

SimpleCommand ::= if GCList fi | do GCList od | Skip | Abort | Varlist := Termlist
					  | Varlist st Formula | Varlist : ProcID(Termlist)

	[if GCList]   [do GCLIst]   Skip   Abort   [:= Varlist Termlist]
	[st Varlist Formula] [: Varlist [( ProcID Termlist]]

Command ::= SimpleCommand | SimpleCommand ; Command

GCList ::= GC | GC || GCList

GC ::= Formula => Command | Varlist:Formula => Command

	[=> Formula Command]   [=> [: Varlist Formula] Command]

SimpleFormula ::= AtomicFormula  |  (Formula)  |  (some Varlist : Formula)

  [some [: Varlist Formula]]

Formula ::= SimpleFormula | SimpleFormula and Formula

AtomicFormula ::= Term < Term | Term > Term | Term le Term | Term ge Term
					|  Term = Term |  Term # Term | Term para Term | Term cong Term
					| Term perp Term | PredID(Termlist) | T | F
					
	[< Term Term]   ...   [( PredID Termlist]   

Termlist ::= Term | Term, Termlist

Term ::= Term + Term | Term - Term | Term / Term | Term * Term | - Term | 
		 |  (Term, Term) | [Termlist] | (Term) | Constant | FunID(Termlist) | VarID
		 
Constant ::= nbr