view

view <name> from <modname> to <modname> { <viewelems> }

A view specifies ways to bind actual parameters to formal parameters (see parameterized module). The view has to specify the mapping of the sorts as well as the operators.

The <viewelems> is a comma-separated list of expressions specifying these mappings:

sort <sortname> -> <sortname>
hsort <sortname> -> <sortname>
op <opname> -> <opname>
bop <opname> -> <opname>

and also can contain variable declarations.

Infix operators are represented as terms containing the operator with either literal underscores _, or variables: _*_ or X * Y. The <opname> can be qualified.

In specifying views some rules can be omitted:

1. If the source and target modules have common submodules, all the sorts and modules declared therein are assumed to be mapped to themselves;

2. If the source and target modules have sorts and/or operators with identical names, they are mapped to their respective counterparts;

3. If the source module has a single sort and the target has a principal sort, the single sort is mapped to the principal sort.

Example

Assume a module MONOID with sort M and ops e and * are given, and another SIMPLE-NAT with sort Nat and operators 0 and + (with the same arity). Then the following expression constitutes a view:

view NAT-AS-MONOID from MONOID to SIMPLE-NAT {
  sort M -> Nat,
  op   e -> 0,
  op _*_ -> _+_
}