/****
 *
 * Highly reduced FMSL grammar for initial integration into Eclipse.
 *
 */

Package parser;


Helpers

cr =			13;
lf =			10;
crlf =			[cr + lf];
tab =			9;
letter = 		[['A'..'Z'] + ['a'..'z']];
letter_or_underscore =	['_' + [['a' .. 'z'] + ['A' .. 'Z']]];
digit = 		['0' .. '9'];
alphanumeric =  	letter | digit;
other_id_char = 	'_';
prime = 		''';     /* ' */
quesmrk =		'$';
all =			[0 .. 0xFFFF];
non_star =		[all - '*'];
non_star_r_paren =	[non_star - ')'];
non_newline =		[all - crlf];
paren_star_comment =	'(*' non_star* '*'+ (non_star_r_paren non_star* '*'+)* ')';
//                      '/*' not_star* '*'+ (not_star_slash not_star* '*'+)* '/'
dash_dash_comment =	'--' non_newline*;
dot_dot_dot = '...';
integer_helper	= digit+;


Tokens

actions_token = 'actions';
all = 'all';
and = 'and';
attribute = 'attribute';
ax = 'ax';
axiom = 'axiom';
begin = 'begin';
components = 'components';
dataflow_token = 'dataflow';
define = 'define';
else = 'else';
end = 'end';
eqn = 'eq';
equations = 'equations';
except = 'except';
exists_token = 'exists';
export_token = 'export';
extends = 'extends';
forall_token = 'forall';
foreach = 'foreach';
from = 'from';
func = 'func';
function = 'function';
if = 'if';
iff = 'iff';
implies = 'implies' | '=>';
import_token = 'import';
in = 'in';
inherits = 'inherits';
inputs_token = 'inputs';
is = 'is';
ques_mark = '?';
isa = 'isa';
lambda_token = 'lambda';
let_token = 'let';
mod = 'mod';
module = 'module';
not = 'not';
obj = 'obj' | 'object';
op = 'op' | 'operation';
operations = 'operations';
ops_token = 'ops';
or = 'or';
out = 'out';
outputs_token = 'outputs';
parts_token = 'parts';
post = 'post';
postcondition = 'postcondition';
pre = 'pre';
precondition = 'precondition';
return_token = 'return';
then = 'then';
theorem = 'theorem';
thm = 'thm';
val = 'val';
value = 'value';
var = 'var';
variable = 'variable';
where_token = 'where';
while_token = 'while';
xor = 'xor';

neq = '!=' |'<>';
aeq = '~=';
pound = '#';
pound_pound = '##';
ampersand = '&';
l_paren = '(';
l_paren_two = '(';
r_paren = ')';
r_paren_two = ')';
star = '*';
plus = '+';
comma = ',';
minus = '-';
rt_arrow = '->' | '::=';
ques_rt_arrow = '?->';
dot = '.';
attr_select = '.-' | '.:';
dot_less = '.<';
dot_gtr = '.>';
divide = '/';
colon = ':';
colon_eq = ':=';
semi_colon = ';';
semi_colon_two = ';';
semi_colon_three = ';';
less = '<';
less_eq = '<=';
equiv = '<=>';
eq = '=';
eq_eq = '==';
gtr = '>';
gtr_eq = '>=';
ques_less = '?<';
l_bkt = '[';
r_bkt = ']';
caret = '^';
l_brace = '{';
bar = '|';
r_brace = '}';
dot_dot = '..';
nil = 'nil';

//ident = (quesmrk? letter_or_underscore ( alphanumeric | other_id_char)* prime*) | dot_dot_dot;

ident = letter*;

symlit = ''' all* ''';
number = integer_helper '.' integer_helper;
real = integer_helper '.' integer_helper;
integer = integer_helper;
string = '\"' all* '\"';
comment = paren_star_comment | dash_dash_comment;
whitespace = ' ' | 9 | 10 | 13 | 14;

Ignored Tokens
comment,
whitespace;


Productions

spec = 
    {empty}
		|
    {defs}
	defs
		;

defs =
    {def}
	def
		|
    {defs}
	defs def
		;

def =
    {empty}
	semi_colon
		|
    {module_def}
	module_def
		|
    {obj_def}
	obj_def
		|
    {op_def}
	op_def
		|
    {val_def}
	val_def
		;

module_def =
    {empty}
	module ident end
	|
    {module}
	module ident defs end
	;

obj_def =
	obj ident is obj_expr semi_colon
		;

op_def =
	op ident l_paren args r_paren semi_colon
		;

args =
    {empty}
		|
    {ident}
	ident
		|
    {args}
	args comma ident
		;

val_def =
	value ident eq expr
		;

obj_expr =
    {obj_and_expr}
	obj_and_expr
		|
    {obj_expr}
	obj_expr or obj_and_expr
		;

obj_and_expr =
    {obj_list_expr}
	obj_list_expr
		|
    {obj_and_expr}
	obj_and_expr and obj_list_expr
		;

obj_list_expr =
    {ident}
	ident
		|
    {obj_list_expr}
	obj_list_expr star
		;

expr =
    {mult_expr}
	mult_expr
		|
    {expr}
	expr rel_op mult_expr
		;

mult_expr =
    {add_expr}
	add_expr
		|
    {mult_expr}
	mult_expr mult_op add_expr
		;

add_expr =
    {primary_expr}
	primary_expr
		|
    {arith_op}
	add_expr arith_op primary_expr
		;

primary_expr =
    {ident}
	ident
		|
    {integer}
	integer
		|
    {real}
	real
		|
    {l_paren}
	l_paren expr r_paren
		;

rel_op =
    {less}
	less
		|
    {less_eq}
	less_eq
		|
    {gtr}
	gtr
		|
    {gtr_eq}
	gtr_eq
		|
    {eq}
	eq
		|
    {neq}
	neq
		;

mult_op =
    {and}
	and
		|
    {star}
	star
		|
    {divide}
	divide
		;

arith_op =
    {or}
	or
		|
    {plus}
	plus
		|
    {minus}
	minus
		;