for_expr

Local Expressions

local_expr ::=

local opt-decl-string in value_expr end

Let Expressions

let_expr ::=

let let_def-list in value_expr end

let_def ::=

typing |

explicit_let |

implicit_let

explicit_let ::=

let_binding = value_expr

implicit_let ::=

single_typing restriction

let_binding ::=

binding |

record_pattern |

list_pattern

If Expressions

if_expr ::=

if logical-value_expr then

value_expr

opt-elsif_branch-string

opt-else_branch

end

elsif_branch ::=

elsif logical-value_expr then value_expr

else_branch ::=

else value_expr

Case Expressions

case_expr ::=

case value_expr of case_branch-list end

case_branch ::=

pattern  value_expr

While Expressions

while_expr ::=

while logical-value_expr

do unit-value_expr end

Until Expressions

until_expr ::=

do unit-value_expr

until logical-value_expr end

For Expressions

for_expr ::=

for list_limitation do unit-value_expr end

Bindings

binding ::=

id_or_op |

product_binding

product_binding ::=

( binding-list2 )

Typings

typing ::=

single_typing |

multiple_typing

single_typing ::=

binding : type_expr

multiple_typing ::=

binding-list2 : type_expr

commented_typing ::=

opt-comment-string typing

Patterns

pattern ::=

value_literal |

pure_value-name |

wildcard_pattern |

product_pattern |

record_pattern |

list_pattern

Wildcard Patterns

wildcard_pattern ::=



Product Patterns

product_pattern ::=

( inner_pattern-llst2 )

Record Patterns

record_pattern ::=

pure_value-name ( inner_pattern-list )

List Patterns

list_pattern ::=

enumerated_list_pattern |

concatenated_list_pattern

Enumerated List Patterns

enumerated_list_pattern ::=

( opt-inner_pattern-llst )

Concatenated List Patterns

concatenated_list_pattern ::=

enumerated_list_pattern ^ inner_pattern

Inner Patterns

Inner_pattern ::=

value_literal |

id_or_op |

wildcard_pattern |

product_pattern |

record_pattern |

list_pattern |

equality_pattern

Equality Patterns

equality_pattern ::=

= pure_value-name

Names

name ::=

qualified_id |qualified_op

Qualified Identifiers

qualified_id ::=

opt-qualification id

qualification ::=

element-object_expr

Qualified Operators

qualified_op ::=

opt-qualification ( op )

Identifiers and Operators

id_or_op ::=

id |op

op ::=

infix_op |prefix_op

Infix Operators

infix_op ::=

  | | | | | | | | | | | |\ |^ | |

† | |  | | |

Prefix Operators

prefix_op ::=

abs |int |real |card |len |inds |

elems |hd |tl |dom |rng

Connectives

connective ::=

infix_connective |

prefix_connective

Infix Connectives

infix_connective ::=

 | |

Prefix Connectives

prefix_connective ::=



Infix Combinators

infix_combinator ::=

 | | | |;

APPENDIX B

Precedence and Associativity of Operators

Value operator precedence - increasing
Prec	Operator(s)	Assotiativity
14	    	Right
13	 post
12	   	Right
11	;	Right
10	:=
9		Right
8		Right
7		Right
6	           
5	     †	Left
4	   	Left
3	
2	:
1	~ prefix_op

Type operator precedence - increasing
Prec	Operator(s)	Associativity
3		Right
2	
1	-set -infset * **

APPENDIX C

Lexical Matters

This chapter describes lexical matters, i.e. the microsyntax for RSL.

Basically, RSL follows the rules now in current practice for most programming languages:text (i.e. an RSL specification) is represented as a string of characters, which is interpreted left-to-right and broken into a string of tokens. The characters are drawn from a superset of the ASCIIcharacters called the full RSL character set. Tokens may be separated by 'whitespace', which isstrings of one or more of the following characters: line-feed, carriage-return, space and tab. (Note that comments are part of the RSL syntax and thus cannot be used freely as whitespace. Also note that comments may not be nested.)

There are two types of tokens in RSL: varying and fixed.

Varying Tokens

The microsyntax for varying tokens is defined by the syntax rules below, where the charactersused in forming tokens are shown in quotes, as in '$'. Furthermore, LF, CR and TAB are used to denote the ASCII characters line-feed, carriage-return and tab.

id ::=

letter opt-letter_or_digit_or_underline_or_prime-string

letter_or_digit_or_underline_or_prime ::=

letter | digit | underline | prime

letter ::=

ascii_letter | greek_letter

comment ::=

‘/’ ‘*’ comment_item-string ‘*’ ’/’

comment_item ::=

comment_char

comment_char ::=

LF | CR | TAB | ascii_letter | digit | graphic | prime | quote | backslash

int_literal ::=

digit-string

real_literal ::=

digit-string ’.’ digit-string

text_literal ::=

‘’opt-text_character-string ‘’

char_literal ::=

‘’char_character ‘’

text_character ::=

character | prime

char_character ::=

character | quote

character ::=

ascii_letter | digit | graphic | escape

digit ::=

‘0’ |’1’ |’ 2’ |’ 3’ |’ 4’ |’ 5’ |’ 6’ |’ 7’ |’ 8’ |’ 9’

ascii_letter ::=

‘a’ | ’b’ | ’c’ | ’d’ | ’e’ | ’f’ | ’g‘ | ’h’ | ’i’ | ’j’ | ’k’ | ’l’ | ’m’ |’n’ | ’o’ | ’p’ | ’q’ | ’r’ | ’s’ | ’t’ | ’u’ | ’v’ | ’w’ | ’x’ | ’y’ |

’z’ |‘A’ | ’B’ | ’C’ | ’D’ | ’E’ | ’F’ | ’G’ | ’H’ | ’I’ | ’J’ | ’K’ | ’L’ | ’M’ |’N’ | ’O’ | ’P’ | ’Q’ | ’R’ | ’S’ | ’T’ | ’U’ | ’V’ |

’W’ | ’X’ | ’Y’ | ’Z’

greek_letter ::=

‘`alpha’|’`beta’|’`gamma’|’`delta’|’`epsilon’|’`zeta’|’`eta’|’`theta’|’`iota’|‘`kappa’|’`mu’|’`nu’|’`xi’|’`pi’|’`rho’|’`sigma’|

’`tau’|’`upsilon’|’`phi’|’`chi’|’`psi’|’`omega’|’`Gamma’|’`Delta’|’`Theta’|’`Lambda’|’`Xi’|’`Pi’|’`Sigma’|’`Upsilon’|

’`Phi’|’`Psi’|’`Omega’

underline ::=

‘_’

prime ::=

‘’

quote ::=

‘’

backslash ::=

‘\’

graphic ::=

‘ ’ | ‘!’ | ‘#’ | ‘$’ | ‘%’ | ‘&’ | ‘(’ | ‘)’ | ‘*’ | ‘+’ | ‘,’ | ‘-’ | ‘.’ | ‘/’ | ‘:’ | ‘;’ |‘<’ | ‘=’ | ‘>’ | ‘?’ | ‘@’ | ‘[’ | ‘]’ | ‘^’ | ‘_’ | ‘`’ |

‘{’ | ‘|’ | ‘}’ | ‘~’

escape ::=

‘\’’r’|‘\’’n’|‘\’’t’|‘\’’a’|‘\’’b’|‘\’’f’|‘\’’v’|‘\’’?’|‘\’’\’|‘\’’ ’|‘\’’ ’| ‘\’ oct_constant | ‘\’ ‘x’ hex_constant

oct_constant ::= oct_digit | oct_digit oct_digit | oct_digit oct_digit oct_digit

hex_constant ::=

hex_digit-string

oct_digit ::=

‘0’ |’1’ |’ 2’ |’ 3’ |’ 4’ |’ 5’ |’ 6’ |’ 7’

hex_digit ::=

digit | ‘a’ | ’b’ | ’c’ | ’d’ | ’e’ | ’f’ | ‘A’ | ’B’ | ’C’ | ’D’ | ’E’ | ’F’

ASCII forms of Greek Letters

Greek letters, which may be used in identifiers, have ASCII forms are follows :

ASCII	Full	ASCII	Full
`alpha `beta `gamma `delta `epsilon `zeta `eta `theta `iota `kappa `mu `nu `xi `pi `rho `sigma `tau `upsilon `phi `chi `psi `omega	                     	`Gamma `Delta `Theta `Lambda `Xi `Pi `Sigma `Upsilon `Phi `Psi `Omega’	          

Fixed Tokens

The representation of individual fixed token is given directly in the syntax rules for RSL. However, a representation using only ASCII characters is possible, as denied in the following table:

ASCII	Full	ASCII	Full	ASCII	Full
><		isin		~isin	
||		++		-\	
|=|		|^|		-list	
**		-inflist		~=	
/\		\/		+>	
>=		exists		all	
<=		union		!!	†
inter		<<		always	
-m->		<<=		=>	
-~->		>>		is	
->		>>=		<->	
#		<.		.>	
:-	

The word equivalents of certain symbols: all, exists, union, inter, isin, always are reserved, and cannot be used as identifiers.

RSL Keywords

The RSL keywords are listed below. They cannot be used as identifiers.

Keywords for RSL
Bool	class	inds	skip
Char	do	initialise	stop
Int	dom	int	swap
Nat	elems	len	then
Real	else	let	tl
Text	elsif	local	true
Unit	end	object	type
abs	extend	of	until
any	false	out	use
as	for	post	value
axiom	forall	pre	variable
card	hd	read	while
case	hide	real	with
channel	if	rng	write
chaos	in	scheme