Subject: Turing Web

From: [email-masked]
Date: Mon, 17 Jun 1991 07:42:57 PDT

I have an updated version of Turing Web, which I enclose.

					Kostas

# Version of June 1991.

# ********
# Named types seem to be O.K.
# Unions have to be tested with named types.
# ********

# Kostas N. Oikonomou, April 1990 and on ...
# Thanks to Norman Ramsey for helpful suggestions.

# NOTE: newlines are important in the WeB file. They designate the end of statements.

language Turing extension t

at_sign @

# This says how to treat "@<...@> =" and "@<...@>". See "Specifying the 
# treatment of modules" in the Spider User's Guide.
module definition stmt use stmt

comment begin <"%"> end newline
macros begin
\def \commentbegin {\%}
macros end

# Line numbers are not necessary. The compiler handles the tangled output
# with no problem. However, there is no way to turn line numbers off!
line begin <"%"-"line"> end <"">

default translation <*> mathness yes
default mathness yes translation <*>

#----------------------------------------------------------------------------
# 				Tokens
#----------------------------------------------------------------------------

token identifier category expn mathness yes
token number category expn mathness yes
# Note: newline's have to be treated carefully; for example, if they are
# found in math mode, webmac.tex ignores them.
token newline category newl translation <> mathness maybe 
token pseudo_semi translation <> category semi mathness maybe

token ( category open 
token ) category close 
token * category star
token + category binop
token . category binop
token , category comma translation <",\\,"-opt-3>
token - category unorbinop
token / category binop
# This definition seems to be needed for good formatting of labels of case statements.
token : category colon translation <"\\mathbin{:}"> mathness yes
token < category binop
token = category equal
token > category binop
token # category expn translation <"\\#"> 
token -> category binop translation <"\\rightarrow">
token .. category dotdot translation <"\\mathbin{..}">
# We want the exponentiation operator "**" to be formatted as "^". However,
# "^" is defined in webmac.tex, so we need the following definition:
token ** category binop translation <"\\char`^">
token := category assign translation <"\\mathbin{:=}"> mathness yes
token >= category binop translation <"\\ge"> 
token <= category binop translation <"\\le">
token @ category atsign

# In the following, section references are to the Turing Report, in
# "The Turing Programming Language: Design and Definition", 1988.

#----------------------------------------------------------------------------
# 			Section 4.2: Programs and Declarations
#----------------------------------------------------------------------------

# 4.2.3, 4.2.4. Constant and variable declarations. See pp. 12-13 of the
# Spider User's Guide for the "*" s.
reserved var ilk varconst_like
reserved const ilk varconst_like
ilk varconst_like category varconst
reserved pervasive ilk pervasive_like
ilk pervasive_like category pervasive
varconst <"\\"-space> pervasive --> varconst
# For "var r := 3.141":
varconst <"\\"-space> expn* assign expn newl --> stmt
# NOTES for the following production:
# 1. "idtypespec" is an auxiliary category which we will also use later.
# 2.  "typespec" is defined in sec. 4.3 on types.
# 3. See 4.6.1b for the "id, id" case.
# 4. For the "|dotdot", see the Turing+ extensions, section 6.10.
[ expn colon (typespec|expn) ] !dotdot --> idtypespec !dotdot
# "vcidtypespec" is another auxiliary category, which is also used later.
varconst <"\\"-space> idtypespec* --> vcidtypespec
# For "var r : real", or "var x : named_type":
vcidtypespec newl --> stmt
# For "var r : real := 3.141":
vcidtypespec assign expn newl --> stmt
# Initializing value:
reserved init ilk init_like
ilk init_like category init
# The context is so that the "init" rule in 4.4.6 can work.
[ init <"\\,"> expn ] !assign --> expn !assign

# 4.2.4. Collections:
reserved collection ilk collection_like
ilk collection_like category collection
reserved forward ilk forward_like
ilk forward_like category forward
reserved of ilk of_like
ilk of_like category of
forward <"\\"-space> expn --> typespec
collection <"\\"-space> of <"\\"-space> (typespec|expn) --> typespec

# 4.2.5. Bindings:
reserved bind ilk bind_like
ilk bind_like category bind
# We introduce the auxiliary category "binding". To correctly parse 
# "bind a to A.a", etc, we need a context:
[ expn <"\\"-space> to <"\\"-space> expn ] !(binop|open) --> binding !(binop|open)
varconst <"\\"-space> binding --> binding
binding comma binding --> binding
bind <"\\"-space> binding newl --> stmt

#----------------------------------------------------------------------------
# 			Section 4.3: Types
#----------------------------------------------------------------------------

# Type declaration:
reserved type ilk type_like
ilk type_like category type
type <"\\"-space> pervasive --> type
type <"\\"-space> idtypespec* newl --> stmt

# Typespec:
# a. Standard type:
reserved boolean ilk typespec_like
reserved char ilk typespec_like
reserved int ilk typespec_like
reserved int1 ilk typespec_like
reserved int2 ilk typespec_like
reserved int4 ilk typespec_like
reserved nat ilk typespec_like
reserved real ilk typespec_like
reserved real4 ilk typespec_like
reserved real8 ilk typespec_like
ilk typespec_like category typespec
# Strings are tricky (see 4.4.4), so define a new category:
reserved string ilk strng_like
ilk strng_like category strng
[ strng ] !open --> typespec !open
strng <"\\,"> open (expn|star) close --> typespec
# To allow the typespec to be on a line by itself (e.g. ... newl record ... end record):
newl typespec --> typespec

# b. Subrange type. This is tricky! If the context were not there, 
# then, for example, "1..a+b" would be parsed as "typespec + b".
# Also, note that if spaces are not left around the "..", parsing will be 
# confused because, e.g., "1..expn" is indistinguishable from "1.expn".
# Finally, see sec. 4.6.1 for "star".
[ expn dotdot (expn|star) ] !(binop|star|unorbinop|open) --> typespec !(binop|star|unorbinop|open)

# c. Enumerated type:
reserved enum ilk enum_like
ilk enum_like category enum
enum <"\\,"> expn --> typespec

# d. Array type:
reserved array ilk array_like
ilk array_like category array
typespec comma typespec --> typespec
array <"\\"-space> typespec <"\\"-space> of <"\\"-space> (typespec|expn) --> typespec

# e. Set type:
reserved set ilk set_like
ilk set_like category set
set <"\\"-space> of <"\\"-space> typespec --> typespec

# f. Record type. We use the auxiliary category "recordbody".
# Some of the productions are also used by "union" and "case".
reserved record ilk record_like
ilk record_like category record
<force-indent-indent> record <force-indent> --> recordbody
# Eat up a newline, if present (this is to allow free formatting of the record).
(recordbody|unionbody|casebody) newl --> #1
recordbody idtypespec <force> --> recordbody
# End rule for record and union:
(recordbody|unionbody) <outdent-force> end <"\\"-space> (record|union) <outdent-outdent-force> --> typespec

# g. Union type. Based on "record".
reserved union ilk union_like
ilk union_like category union
reserved label ilk label_like
ilk label_like category label
label <"\\"-space> expn colon <"\\"-space> --> labelexpn
label colon <"\\"-space> --> labelexpn
<force-indent-indent> union <"\\"-space> idtypespec <"\\"-space> of <force-indent> --> unionbody
<force-indent-indent> union colon typespec <"\\"-space> of <force-indent> --> unionbody
(unionbody|casebody) labelexpn <force> --> #1
unionbody <indent> idtypespec <force-outdent> --> unionbody

# h. Pointer type:
reserved pointer ilk pointer_like
ilk pointer_like category pointer
reserved to ilk to_like
ilk to_like category to
pointer <"\\"-space> to <"\\"-space> expn --> typespec

# i. Named type:
# Named typed are taken care of by productions in 4.2.3, 4.2.4, and 4.3d.

#----------------------------------------------------------------------------
# 			Section 4.4: Subprograms and Modules.
#----------------------------------------------------------------------------

# 4.4.1. Subprogram declarations.

reserved body ilk body_like
ilk body_like category body
reserved procedure ilk subprog_like
reserved function ilk subprog_like
ilk subprog_like category subprog
# 4.4.1 b, c.
# NOTES on the next production:
# 1. It is extended to Turing Plus ("stub").
# 2. It's too hard to handle the fact that a subprogram stub may be followed
# by an import list, which must be indented, but then we must outdent, with no
# matching "end"! So, for
# 		external, forward, and stub
# subprograms, do the outdenting MANUALLY by @+@t\2@>.
# Module stubs, however, are handled nicely. See the Turing+ extensions section.
(external|forward|stub) <"\\"-space> subprog --> subprog

# 4.4.1 d.
body <"\\"-space> (subprog|module) <"\\"-space> expn* newl <force-indent> --> stmt

# 2. Subprogram headers. We use the auxiliary categories "subproghead" and
# "parlist". ("parlist" is defined in no. 3 below.)
(subprog|module) <"\\"-space> expn* --> subproghead
# The following also handles functions that return named types.
subproghead colon (typespec|expn) --> subproghead
subproghead <"\\,"> open parlist close --> subproghead
subproghead <"\\"-space> idtypespec --> subproghead
subproghead newl <force-indent> --> stmt 

# 3. Parameter declarations:
open [ (idtypespec|vcidtypespec) ] --> open parlist
parlist comma (idtypespec|vcidtypespec) --> parlist
# To ensure that the "subproghead" productions above have priority:
open [ subproghead ] !(open|colon) --> open parlist !(open|colon)
[ parlist comma subproghead ] !(open|colon) --> parlist !(open|colon)

# 4. Parameter types:
# Array parameters: see 4.3b and 4.3d.

# 5. Import. This should not be so complicated!
reserved import ilk import_like
ilk import_like category import
import <"\\"-space> open --> importlist
importlist (expn|comma) --> importlist
importlist (varconst|forward) <"\\"-space> expn --> importlist
importlist close newl --> stmt

# 6. Subprogram body:
reserved pre ilk result_like
reserved post ilk result_like
# We use the auxiliary category "initstmt".
init <"\\"-space> expn assign --> initstmt
initstmt (expn|comma|assign) --> initstmt
initstmt newl --> stmt
<outdent-force> end <"\\"-space> expn newl --> stmt

# 4.4.2. Module declarations:
reserved module ilk module_like
ilk module_like category module
reserved export ilk import_like
reserved opaque ilk forward_like

#----------------------------------------------------------------------------
# 			Section 4.5: Statements and I/O.
#----------------------------------------------------------------------------

# Statements:
# a. Assignments.
expn assign expn newl --> stmt
# b. Procedure call on a line by itself.
expn newl --> stmt

# c, e, h, k, l, n:
reserved assert ilk result_like
reserved result ilk result_like
reserved when ilk result_like
reserved new ilk result_like
reserved free ilk result_like
reserved tag ilk result_like
ilk result_like category result
# Note: if the "newl" were not there, the "assert i" part of "assert i > 0"
# would fire the production!
result <"\\"-space> expn newl --> stmt

# d, h. Return and exit:
reserved exit ilk return_like
reserved return ilk return_like
ilk return_like category return
return newl --> stmt
# This is for "exit when ...".
return <"\\"-space> result <"\\"-space> expn newl --> stmt

# j. Begin, end:
reserved begin ilk begin_like
ilk begin_like category begin
<force> begin <force-indent> --> stmt
reserved end ilk end_like
ilk end_like category end
<outdent-force> end newl  --> stmt

# f. If statements:
reserved if ilk if_like
ilk if_like category if
reserved then ilk then_like
ilk then_like category then
reserved else ilk else_like
ilk else_like category else
reserved elsif ilk elsif_like
ilk elsif_like category elsif
if <"\\"-space> expn <"\\"-space> then <force-indent> --> stmt
<force-outdent> else <force-indent> --> stmt
<force-outdent> elsif <"\\"-space> expn <"\\"-space> then <force-indent> --> stmt
# The "end if" rule is in fgm.

# g. Loop statements:
reserved loop ilk loop_like
ilk loop_like category loop
reserved invariant ilk result_like
loop <force-indent> --> stmt
# The "end loop" rule is in fgm.

# i. Case statements. Also see "Union".
reserved case ilk case_like
ilk case_like category case
case <"\\"-space> expn <"\\"-space> of <force-indent> --> casebody
casebody <indent> stmt <force-outdent> --> casebody
casebody <outdent-force> end <"\\"-space> case newl --> stmt

# m. For statements:
reserved for ilk for_like
ilk for_like category for
reserved decreasing ilk decreasing_like
ilk decreasing_like category decreasing
for <"\\"-space> decreasing --> for
for <"\\"-space> expn --> for
for colon typespec --> for
for newl <force-indent> --> stmt
# The "end for" rule is in fgm.

# fgm: the common "end ..." rule:
<outdent-force> end <"\\"-space> (for|if|loop) newl --> stmt

# o. Put statements:
reserved put ilk put_like
ilk put_like category put
reserved skip ilk skip_like
ilk skip_like category expn
# Context needed for correct parsing of e.g. "put a(i)/b(i)".
[ put <"\\"-space> expn ] !(open|star|unorbinop|binop|comma) --> put !(open|star|unorbinop|binop|comma)
[ put colon expn ] !comma --> put !comma
put <"\\"-space> dotdot --> put
put newl --> stmt

# p. Get statements:
reserved get ilk get_like
ilk get_like category get
# A getItem.
expn colon star --> expn
[ get <"\\"-space> expn ] !(comma|colon|open) --> get !(comma|colon|open)
[ get colon expn ] !(comma|colon|open) --> get !(comma|colon|open)
get newl --> stmt

# Formatting rules for statements.
# The first rule is needed for statements separated by blank lines:
stmt newl --> stmt
stmt <force> stmt --> stmt

#----------------------------------------------------------------------------
# 			Section 4.6: References and Expressions.
#----------------------------------------------------------------------------

ilk expn_like category expn

# 4.6.1. References:
# a. An identifier is already an expression, hence a reference.
# b.
# Note: because of its role in strings, * is "star", and has to be handled explicitly.
[ expn (star|unorbinop|binop|comma) expn ] !open --> expn !open
expn open expn close --> expn
open expn close --> expn

# 4.6.2. Expressions:
# b. Constants:
reserved false ilk expn_like
reserved true ilk expn_like
# c. Substrings:
open [ star ] close --> open expn close
open [ star unorbinop expn ] close --> open expn close
# d. Set constructors:
expn open close --> expn
reserved all ilk expn_like
# e. Binary operators:
# See 4.6.1b. However, "div" and "mod" are handled specially:
ilk mod_like category mod
reserved div ilk mod_like
reserved mod ilk mod_like
[ expn <"\\"-space> mod <"\\"-space> expn ] !open --> expn !open
# f. Unary operators:
!expn [ unorbinop expn ] --> !expn expn
# g: see 4.6.1b.

# Special handling of boolean expressions:
reserved and ilk and_like
ilk and_like category binop translation <"\\land"> 
reserved or ilk or_like
ilk or_like category binop translation <"\\lor"> 
# "not" requires special handling because of "not=" and "not in".
# First, "not" itself:
reserved not ilk not_like
ilk not_like category not translation <"\\">
not <"neg"> expn --> expn
# Now "not=":
!not [ equal ] --> !not binop
not <"not"> equal --> binop
# Now "in":
reserved in ilk in_like
ilk in_like category in translation <"\\">
!not [ in <"in"> ] --> !not binop
# Finally, "not in":
not <"not"> in <"in"> --> binop

#----------------------------------------------------------------------------
#			Section 4.6.9: Predefined Functions
#----------------------------------------------------------------------------

#reserved eof ilk expn_like
#reserved pred ilk expn_like
#reserved succ ilk expn_like
#reserved length ilk expn_like
#reserved index ilk expn_like
#reserved repeat ilk expn_like
#reserved abs ilk expn_like
#reserved max ilk expn_like
#reserved min ilk expn_like
#reserved sign ilk expn_like
#reserved sqrt ilk expn_like
#reserved sin ilk expn_like
#reserved cos ilk expn_like
#reserved arctan ilk expn_like
#reserved sind ilk expn_like
#reserved sind ilk expn_like
#reserved cosd ilk expn_like
#reserved arctand ilk expn_like
#reserved ln ilk expn_like
#reserved exp ilk expn_like
#reserved floor ilk expn_like
#reserved ceil ilk expn_like
#reserved round ilk expn_like
#reserved intreal ilk expn_like
#reserved chr ilk expn_like
#reserved ord ilk expn_like
#reserved intstr ilk expn_like
#reserved strint ilk expn_like
#reserved erealstr ilk expn_like
#reserved frealstr ilk expn_like
#reserved realstr ilk expn_like
#reserved strreal ilk expn_like

#----------------------------------------------------------------------------
#			Section 4.6.10: Attributes
#----------------------------------------------------------------------------

#reserved lower ilk expn_like
#reserved upper ilk expn_like
#reserved nil ilk expn_like

#----------------------------------------------------------------------------
#			Section 4.6.11: Predefined Procedures
#----------------------------------------------------------------------------

#reserved rand ilk expn_like
#reserved randint ilk expn_like
#reserved randomize ilk expn_like
#reserved randnext ilk expn_like
#reserved randseed ilk expn_like
#reserved open ilk expn_like
#reserved close ilk expn_like

#----------------------------------------------------------------------------
#			Section 4.7: Source Inclusion Facility
#----------------------------------------------------------------------------

reserved include ilk result_like

#----------------------------------------------------------------------------
#			Section 4.13: External Subprograms
#----------------------------------------------------------------------------

reserved external ilk ext_like
ilk ext_like category external
external <"\\"-space> expn --> external
# Now see 4.4.1.

#----------------------------------------------------------------------------
#----------------------------------------------------------------------------
#	Turing Plus Extensions: from the Turing Plus Report, August 1988.
#----------------------------------------------------------------------------
#----------------------------------------------------------------------------

# -------------------------------
# Section 5: Separate Compilation
# -------------------------------

reserved child ilk result_like
reserved parent ilk result_like
reserved grant ilk import_like

reserved stub ilk stub_like
ilk stub_like category stub
# For subprogram stubs, see 4.4.1.
# Module stubs. This is nice! I am (pleasantly) surprised that it works.
stub <"\\"-space> module <"\\"-space> expn newl <force-indent> --> modulestub
modulestub <force> stmt <force> --> modulestub
modulestub <force> subproghead newl <force> --> modulestub
modulestub <outdent-force> end <"\\"-space> expn newl --> stmt

# --------------------------------------------------------
# Section 6.6: Type Cheats
# --------------------------------------------------------

type <"\\,"> open (typespec|strng) comma expn close --> expn

# --------------------------------------------------------
# Section 6.9: External Variables and External Subprograms
# --------------------------------------------------------

# For the external subprograms, see the Turing section 4.13.
external <"\\"-space> varconst --> varconst

# -------------------------------------------
# Section 6.10: Variable Number of Parameters
# -------------------------------------------

expn colon dotdot --> idtypespec

# ---------------------------------------
# Section 6.11: The Indirection Operation
# ---------------------------------------

(typespec|strng) <"\\,"> atsign <"\\,"> open expn close --> expn

# -----------------------------------
# Section 6.12: Addresses as Integers
# -----------------------------------

reserved addressint ilk typespec_like

# ---------------------------------
# Section 6.17: Control of checking
# ---------------------------------

reserved checked ilk return_like
reserved unchecked ilk uncheck_like
ilk uncheck_like category unchecked
unchecked newl --> stmt
unchecked <"\\"-space> collection --> collection

? ignore_scrap --> #1