-- (C) Copyright International Business Machines Corporation 23 January 
-- 1990.  All Rights Reserved. 
--  
-- See the file USERAGREEMENT distributed with this software for full 
-- terms and conditions of use. 
-- SCCS Info: @(#)predefined.d	1.7 3/13/90

predefined: using ()
definitions

-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
--------------------------- Fundamental Types ---------------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------

empty: enumeration ();

option: enumeration ( 'present', 'absent' );

integer: integer;

boolean: boolean ( true: 'true', false: 'false' );

char: ordered enumeration (
  'NUL','SOH','STX','ETX','EOT','ENQ','ACK','BEL',
  'BS','HT','NL','VT','NP','CR','SO','SI',
  'DLE','DC1','DC2','DC3','DC4','NAK','SYN','ETB',
  'CAN','EM','SUB','ESC','FS','GS','RS','US',
  ' ','!','"','#','$','%','&','''',
  '(',')','*','+',',','-','.','/',
  '0','1','2','3','4','5','6','7',
  '8','9',':',';','<','=','>','?',
  '@','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','{','|','}','~','DEL'
);

charstring: ordered table of char { init } ;

-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
------------------------ The Abstract Program Object --------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------

program: pragma "program" record (
  definitions_modules: definitions_modules,-- imported modules
  main_program: processid,		-- the main program
  programs: processes			-- one or more programs
  -- there can be multiple programs because of program literals
);
 
definitions_modules: table of definitions_module
    { full /* , checkeddefinitions */ } keys (id);
 
definitions_module: record (
  id: moduleid,				-- unique id of module
  type_definitions: type_definitions,	-- type definitions
  attr_definitions: attr_definitions	-- attribute definitions
);

-------------------------------------------------------------------------------
------------------------------ Names and IDs ----------------------------------
-------------------------------------------------------------------------------

processid: nominal;			-- identifies a process object
clauseid: nominal;			-- clause identifiers
rootid: nominal;			-- root name identifiers
typeid: nominal;			-- type identifiers
moduleid: nominal;			-- module id
scopeid: nominal;			-- scope identifier
componentid: nominal;			-- component identifier
exceptionid: nominal;			-- exception id
statementid: nominal;			-- statement identifier
attributeid: nominal;			-- attribute identifier
exitid: nominal;			-- id of exit handler

-- The following is to allow, in absprog, variables with undeclared
-- types.  For example, temporaries that get introduced when expanding
-- expressions to assignment statements.  Their types are not known
-- until the type checking phase which comes after resolution.

typename_option: enumeration ( 'named', 'unnamed');

optional_typename: variant of typename_option (
  'unnamed' -> noname:   empty { },
  'named'   -> typename: typename { full }
);


typename: record (
  moduleid: moduleid,			-- time stamp of module
  typeid: typeid			-- type id within module
);
 
constraintname: record (
  moduleid: moduleid,			-- time stamp of module
  attributeid: attributeid		-- attribute id within module
);

-- an object (variable) gives (i) the scope where it is declared, (ii)
-- its rootid, and (iii) if it is a component, its compoenent id.
-- e.g., if in scope s there is the declaration r: Q, where Q is a
-- record having a component z, then the object r.z gets would have
-- the objectname (s, r, z).

rootname: record (
  scope: scopeid,			-- scope of root declaration
  root: rootid				-- root identifier used to
					-- refer to this object 
);


objectname: record (
  root: rootname,			-- root object
  components: component_list		-- identifiers of components
);
 
component_list: ordered table of componentid { full };
 
objectnames: ordered table of objectname { full } ;
 
 
-------------------------------------------------------------------------------
-------------------------- Type Definitions -----------------------------------
-------------------------------------------------------------------------------

type_definitions: table of type_definition { full } keys (id);

-- Each type has a unique (within its definitions module) type id, a
-- set of typed components (empty except for records, variants and
-- callmessages), a specification consisting of a primitive type and
-- associated information, and a pragma string

type_definition: record (
  id: typeid,
  component_declarations: component_declarations,
  specification: specification_type,
  prag: charstring
);

component_declarations: ordered table of component_declaration { full }
  keys (id)  ;

component_declaration: record (
  id: componentid,			-- unique name of component  
  type: typename			-- declared type
);
 
primitive_types: ordered enumeration (
  'nominaltype', 'integertype', 'booleantype', 'enumerationtype', 'realtype',
  'recordtype', 'varianttype', 'tabletype',
  'inporttype', 'outporttype', 'callmessagetype',
  'polymorphtype' );

specification_type: variant of primitive_types(
  'nominaltype'-> nominal_info: empty { },
  'integertype' -> integer_info: empty { },
  'booleantype' -> boolean: boolean_info { full },
  'enumerationtype' -> enumeration: enumeration_info { full },
  'realtype' -> accuracy_info: accuracy_info { full },

  'recordtype' -> record_info: empty { },
  'varianttype' -> variant_info: variant_info { full },
  'tabletype' -> table_info: table_info { full },

  'inporttype' -> inport_info: inport_info { full },
  'outporttype' -> outport_info: typename { full },
  'callmessagetype' -> callmessage_info: callmessage_info { full },

  'polymorphtype' -> polymorph_info: empty { }
);

 
-- Specific information needed to completely specify a type falling in
-- each of the various primitive type categories

boolean_info: record (
  true_name: charstring,
  false_name: charstring
);

enumeration_info: record (
  ordered: boolean,			-- is it an ordered enumeration?
  values: enumeration_values		-- components
);

enumeration_values: ordered table of charstring { init } keys (*);

accuracy_info: record (			-- for real types
  accuracy_numerator: integer,
  accuracy_denominator: integer
);

variant_info: record (
  case_type: typename,			-- the enumeration tagging the variant
  case_mapping: partitionset		-- maps case tags (from case-type
					-- enumeration) to components
);

partitionset: table of partition_info { full } keys (component_id);

partition_info: record (
  component_id: componentid,		-- component of variant
  case_id: integer,			-- corresponding enumeration value
  case_typestate: formal_typestate	-- typestate of component
);


table_info: record (
  ordered_table: boolean,		-- is the table ordered?
  keys: keyset,				-- all the keys
  element_type: typename,		-- type of each table element
  element_typestate: formal_typestate	-- typestate of each table element
);

keyset: ordered table of formal_objects { full } keys (*);

-- Each key consists of a set of (sub-)components of the element type.
-- An empty set indicates the entire element object

formal_objects: ordered table of component_list { full };

inport_info: record (
  message_type: typename,		-- type of each queued message
  message_typestate: formal_typestate	-- typestate of each queued message
);


callmessage_info: record (
  constants: component_set,		-- which components are held constant
  normal: formal_typestate,		-- exit typestate for normal return
  -- following identifies the Discarded exception for this
  -- callmessage.  The associated exit typestate is the minimum
  -- typestate for the callmessage type.
  minimum: exceptionid,
  -- following associates exit typestates with exceptions
  exception_specifications: exception_specifications
);

component_set: table of componentid { init } keys (*);
 
exception_specifications: table of exception { full } keys (exceptionid);

exception: record (
  exceptionid: exceptionid,		-- unique name of exception
  post_typestate: formal_typestate	-- typestate on that outcome
);
 
-------------------------------------------------------------------------------
------------------------ Attribute Definitions --------------------------------
-------------------------------------------------------------------------------

attr_definitions: table of attr_definition { full } keys (attributeid);

-- An attribute definition includes a unique (within a definitions
-- module) identifier, the code that evaluates the attribute,
-- parameters, and the required entry typestate of the parameters.
-- The parameters exist in the outer scope of the code.

attr_definition: record (
   attributeid: attributeid,		-- unique id of attribute
   execution_environment: execution_environment,-- expression to evaluate
   parameters: rootids,			-- declared in the outer scope
   returnvalue: objectname,		-- boolean object 
   pretypestate: typestate,		-- typestate on entry
   prag: charstring			-- pragma
);

rootids: ordered table of rootid { init };

-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
---------------------------- Process Modules ----------------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------

processes: table of proc { full } keys (id);
 
-- Each process has a unique identifier.  The code is an object of
-- type execution_environment, which includes the statements appearing
-- in the code, as well as declarations for all the root objects
-- introduced by included scopes.  The initport is always an object in
-- the outermost scope.

proc: record (
    id: processid,
    executable_part: execution_environment,  -- dcls + statements
    initport: rootid,			-- name of initialization port
    prag: charstring			-- pragma
);

-- Following record represents a piece of code, either from a process
-- module or from an attribute definition.  The code is represented as
-- a collection of nested scopes, with a single main, or outermost
-- scope.  Each scope introduces new declarations for root objects,
-- and is associated with a clause.  A clause is a list of statements,
-- some of which introduce nested scopes.  Execution of the code
-- always begins with the clause associated with the outermost scope.

execution_environment: record ( 
  scopes: scopes,
  clauses: clauses,
  main_scope: scopeid
);
 
scopes: table of scope { full } keys (id);
 
scope: record (
  id: scopeid,				-- scope identifier
  declarations: declarations,		-- declarations introduced by scope
  clause: clauseid			-- statements to execute in scope
);
 
-- Each declaration identifies the declared root object, and
-- optionally associates a type with the object.  If no type is
-- supplied in a declaration, the type must be inferrable from
-- context.

declarations: table of declaration { full } keys (id);
 
declaration: record (
  id: rootid,				-- id used for reference
  typename: optional_typename,		-- type of object
  prag: charstring			-- pragma
);
 
-- Each clause has a unique (within an execution environment) id and a
-- list of the statements that make up the clause

clauses: table of clause { full } keys (id);
 
clause: record (
  id: clauseid,				-- identifier of clause
  statements: statements		-- statements of clause
);

-- Each statement has a unique (within an execution environment)
-- identifier, an operator and operands, and possibly additional data
-- specified in is qualifier.  Any information that is needed for the
-- proper execution of the statement and cannot not be made available
-- via accessible program objects at runtime, must be provided in the
-- qualifier.  The precise contents of the qualifier depends on the
-- operator.

statements: ordered table of statement { full } keys (id);
 
statement: record (
  id: statementid,
  operator: operator,
  operands: objectnames,
  qualifier: qualifier,
  prag: charstring
);
 

-- Here are all the Hermes operators

operator: ordered enumeration (
  'print',
  'and', 'add',
  'assert', 'case', 'concatenate', 'connect', 'convert', 'copy', 'create',
  'checkdefinitions', 'greater', 'greater_equal', 'less', 'less_equal',
  'currentprogram', 'discard', 'dissolve', 'divide', 'drop', 'empty',
  'every', 'equal', 'exists', 'extract', 'forall', 'hide', 'insert',
  'insert_at',  'integer_literal', 'merge', 'merge_at', 'mod', 'move',
  'multiply',  'named_literal', 'unary_minus', 'new',
  'not', 'not_equal', 'or', 'program_literal', 'real_literal',
  'rem', 'receive', 'remove', 'return', 'return_exception', 'reveal', 'send',
  'size', 'subtract', 'the_element', 'unite', 'unique', 'unwrap', 'wrap',
  'block', 'call', 'select', 'exit',
  'position_of_element',  'position_of_selector', 'type', 'typestate',
  'procedure', 'string_literal', 'while',
  'for_inspect', 'for_enumerate', 
  'inspect_table', 'inspect_polymorph', 'expression_block', 'if',
  'typename', 'attributename'
);

-------------------------------------------------------------------------------
---------------------------- Operation Qualifiers -----------------------------
-------------------------------------------------------------------------------

-- Names of all the qualifier types... comments identify which
-- operators use each qualifier type

qualifier_types: ordered enumeration (
  'absent',
  'selector',				-- every, exists, extract,
					-- forall, remove,
					-- the_element, position_of_selector
  'constraintname',			-- assert, drop
  'literal',				-- integer_literal,
					-- real_literal, named_literal
  'return exception',			-- return_exception 
  'program literal',			-- program_literal
  'wrap',				-- wrap, unwrap
  'exit',				-- exit
  'block',				-- block
  'while',				-- while
  'inspect table',			-- for_inspect, inspect_table
  'inspect polymorph',			-- inspect_polymorph 
  'for enumerate',			-- for_enumerate
  'select',				-- select
  'expression block',			-- expression_block
  'if',					-- if-then-else
  'typename',				-- typename literal
  'attributename'			-- attributename literal
);

-- Following is the variant used to represent all statement qualifiers

qualifier: variant of qualifier_types(
   'absent'   -> empty: empty { },                     -- no qualifier
   'selector' -> selector: selector { full },
   'constraintname' -> constraintname: constraintname { full },  
   'literal' -> literal: charstring { full },  
   'return exception' -> exceptionid: exceptionid { full },
   'program literal' -> program_literal: processid { full },
   'wrap' -> formal_typestate: formal_typestate { full },
   'exit' -> exit: exitid { full },
   'block' -> block: block_qualifier { full },
   'while' -> while: while_qualifier { full },
   'inspect table' -> inspect_table: inspect_table_qualifier { full },
   'inspect polymorph' -> 
       inspect_polymorph: inspect_polymorph_qualifier {full},
   'for enumerate' -> for_enumerate: for_enumerate_qualifier { full },
   'select' -> select: select_qualifier { full },
   'expression block' -> expression: expression_qualifier { full },
   'if' -> if: if_qualifier { full },
   'typename' -> typename: typename { full },
   'attributename' -> attributename: attribute_name { full }
);


-- A selector qualifies many table-related statements, and encodes the
-- information contained in the WHERE (...) clause of such statements.
-- The selector introduces a scope which encodes the selector
-- expression.  The 'element' root variable appears in that scope and
-- holds a table element whenever the selector is executed.  The
-- 'result' object holds the result of evaluating the selector for a
-- the table element.

selector: record (
  scope: scopeid,               -- scope introduced by the selector
  element: rootid,              -- the element being selected
  result: objectname            -- boolean value of selector expression
);

-- A block statement qualifier identifies the scope holding the
-- declarations and main body code of the block, the root objects held
-- constant within the block, and all the handlers associated with the
-- block.

block_qualifier: record (
  scope: scopeid,			-- new scope introduced by the block
  constants: rootnames,			-- objects not changed in this scope
  handlers: handlers			-- exception and exit handlers
);

rootnames: table of rootname { full } keys (*);
 
-- Each handler names the exceptions or exit conditions that it
-- handles, and supplies a clause (not a scope) containing the body of
-- the handler.

handlers: table of handler { full } keys (id);

handler: record (
  id: handlername,
  clause: clauseid
);

-- Handlers come in four varieties...

handler_type: ordered enumeration (
  'builtin',				-- builtin exceptions
  'user',				-- user exceptions (defined
					-- with callmessages)
  'exit',				-- exit conditions
  'others'				-- exceptions not otherwise handled
);

-- Each handler type requires type-specific additional information to
-- fully specify the condition handled

handlername: variant of handler_type (
  'builtin' -> builtin: builtin_exception { init },
  'user' -> user: user_exception { full },
  'exit' -> exit: exitid { init },
  'others' -> others: empty {} 
);

-- Here are all the builtin exceptions

builtin_exception: ordered enumeration (
  'CaseError', 'ConstraintError', 'ConstraintFailure', 'Depletion', 
  'Disconnected', 'DivideByZero', 'DuplicateKey', 'InterfaceMismatch', 
  'NotFound', 'PolymorphMismatch', 'DefinitionError', 'RangeError',
  'Uncopyable' 
);

-- A user exception is specified by the callmessage type and one of
-- the exceptions defined with that type

user_exception: record (
  type: typename,
  exceptionid: exceptionid
);
 
-- The qualifier for a while statement identifies the clause that
-- evaluates the entry test at the top of the loop, the variable that
-- will hold the result of the test, and the clause containing the
-- loop body.

while_qualifier: record (
  test_clause: clauseid,
  result: objectname,
  repeated_clause: clauseid
);

-- Following qualifier is used for inspect_table and for_inspect
-- statements.  In addition to the same sort of selector as that used
-- for other table operations, a body scope is included, as well as
-- the id of the root object that holds the inspected table element
-- throughout the body scope.  The inspecting root object is contained
-- in the body scope.  Note that it IS NOT the same object as the
-- element object in the selector itself, as they declared in disjoint
-- scopes.

inspect_table_qualifier: record (
  scope: scopeid,			-- scope of statement body
  element: rootid,			-- inspection variable
  selector: selector			-- table selector 
);

-- The qualifier for an inspect_polymorph statement identifies the
-- scope forming the statement body, the root variable (declared in
-- the body scope) that will hold the unwrapped polymorph value
-- throughout the body scope, and the typestate required for the
-- unwrapped value.

inspect_polymorph_qualifier: record (
  scope: scopeid,
  element: rootid,
  typestate: formal_typestate
);

-- For a for_enumerate statement, the qualifier identifies the body
-- scope, as well as the root variable that is used to iterate through
-- the enumeration.  The iteration variable is declared in the body
-- scope.

for_enumerate_qualifier: record (
  scope: scopeid,
  enumerator: rootid
);

-- A select statement qualifier includes a "select clause" for each
-- guarded arm of the select statement, identifying the guard
-- condition for the arm and the clause to be executed when the arm
-- is selected.    In addition, a clause to be executed when all
-- guards are disabled is specified.

select_qualifier: record (
  clauses: select_clauses,
  otherwise_clause: clauseid		-- otherwise clause is mandatory
);

select_clauses: table of select_clause { full } ;

select_clause: record (
	clause: clauseid,
	info: clause_info
);

-- Each arm can be guarded by a boolean condition, an "events" on a
-- given inport, or both.

guard_type: enumeration ( 'boolean', 'event' ,'both' );

clause_info: variant of guard_type (
  'boolean' -> boolean: boolguard { full },
  'event' -> portname: objectname { full },
  'both' -> both: bothguard { full }
);

-- A boolean guard (or the boolean part of a "both" guard) identifies
-- the clause to be executed to evaluate the guard, and the object
-- where the result of that execution will be placed.

boolguard: record (
  clause: clauseid,
  result: objectname
);

bothguard: record (
  boolean: boolguard,
  portname: objectname
);

-- The qualifier for an expression block identifies the scope to be
-- executed and the root variable that will hold the expression
-- result.  The root variable is the only variable outside the
-- expression block scope that is not held constant within the scope.

expression_qualifier: record (
  scope: scopeid,
  result: rootname
);

-- The qualifier for an if statement identifies the clause that will
-- evaluate the test expression, the object that will hold the
-- expression result, and the clause to be executed if the expression
-- yields a true result.  In addition, an 'else' clause may optionally
-- be supplied, identifying the clause to be executed when the test
-- expression is false.

if_qualifier: record (
  test_clause: clauseid,
  test_result: objectname,
  then_clause: clauseid,
  opt_else_clause: optional_clauseid
);

optional_clauseid: variant of option (
  'present' -> clauseid: clauseid { init },
  'absent' -> empty: empty { }
);


-- Following types definitions are for the values resulting from
-- TYPE OF and TYPESTATE OF expressions, which inspect values wrapped
-- in polymorphs

typeof_value: record (
  typename: typename,			-- name of the type
  definitions: definitions_modules	-- resolution environment for that type
);

typestateof_value: record (
  typestate: formal_typestate,		-- typestate of wrapped value
  definitions: definitions_modules	-- resolution environment for
					-- attributes appearing in typestate
);



-------------------------------------------------------------------------------
------------------------- Typestates and Formal Typestate ---------------------
-------------------------------------------------------------------------------

-- A typestate is a set of attributes, each of which constist of an
-- attribute name and a list of objects that are the parameters of the
-- attribute. 

typestate: table of attribute { full } keys (*) ;
 
attribute: record (
  name: attribute_name,
  objects: objectnames 
);

-- There are three built-in attributes: init and case.  An attribute
-- can also name a user-defined attribute, or constraint.  The 'full'
-- attribute is an abbreviation for several init attributes, and may
-- be dropped from this list at some future time.

attribute_type: enumeration ( 'initialized', 'case', 'constraint', 'full' );

attribute_name: variant of attribute_type(
  'initialized' -> init: empty { },
  'case' -> case: empty { },
  'constraint' -> constraint: constraintname { full },
  'full' -> full: empty { }
);

-- A formal typestate is like a typestate, but no root variable is
-- mentioned.  Instead, the component lists are interpreted relative
-- to some variable (not necessarily a root object) depending on
-- context.  An empty component list indicates the associated variable
-- itself, rather than any of its (sub-)components.

formal_typestate: table of formal_attribute { full } keys (*) ;

formal_attribute: record (
  attribute_name: attribute_name,
  parameters: formal_object_list
);

formal_object_list: ordered table of component_list { full } ;

-- OMIT REMAINDER FROM MANUAL APPENDIX
-- The remaining definitions do not properly belong to the predefined
-- module at all.  They will someday be excised from this file.  Their
-- purpose is to relate elements of an abstract program or definitions
-- module to names and positions within a concrete syntactic
-- representation from which the object was derived.  For instance,
-- root variables are mapped to variable names.  Such mappings make
-- sense only in the context of some given concrete syntax, and so
-- should not appear here, where we are concerned only with abstract
-- program objects.



-------------------------------------------------------------------------------
-------------------------------------------------------------------------------
-------------------------------- Print Mappings -------------------------------
-------------------------------------------------------------------------------
-------------------------------------------------------------------------------

definitions_printmappings: table of definitions_printmap { full } keys (id);

definitions_printmap: record (
    id: moduleid,
    name: charstring,
    types: type_printmap,
    attributes: attribute_printmap,
    components: component_printmap,
    exceptions: exception_printmap );

type_printmap: table of type_printrec { full } keys (id) (name);

type_printrec: record (
    id: typeid,
    name: charstring );

attribute_printmap: table of attribute_printrec { full }
    keys (attribute) (name);

attribute_printrec: record (
    attribute: attributeid,
    name: charstring );

component_printmap: table of component_printrec { full }
    keys (type, component) (type,name);

component_printrec: record (
    type: typeid,
    component: componentid,
    name: charstring );

exception_printmap: table of exception_printrec { full }
    keys (type, exception) (type,name);

exception_printrec: record (    -- callmessage exceptions
    type: typeid,
    exception: exceptionid,
    name: charstring );

-------------------------------------------------------------------------------
-------------------- Printmaps for Executable Entities ------------------------
-------------------------------------------------------------------------------

executable_thing: enumeration ( 'process', 'constraint' );

executable_id: variant of executable_thing (
    'process' -> pid: processid { init },
    'constraint' -> cid: attributeid { init }
);

executable_printmappings: table of executable_printmap { full }
    keys (id);

executable_printmap: record (
    id: executable_id,
    name: charstring,
    roots: root_printmap,
    exits: exit_printmap );

root_printmap: table of root_printrec { full } 
    keys (scope,root) (scope,name) ;

root_printrec: record (
    scope: scopeid,
    root: rootid,
    name: charstring );

exit_printmap: table of exit_printrec { full }
    keys (exit) (name);

exit_printrec: record (
    exit: exitid,
    name: charstring );

end definitions
