instantiation

instantiation of parameterized modules

Parameterized modules allow for instantiation. The process of instantiation binds actual parameters to formal parameters. The result of an instantiation is a new module, obtained by replacing occurrences of parameter sorts and operators by their actual counterparts. If, as a result of instantiation, a module is imported twice, it is assumed to be imported once and shared throughout.

Instantiation is done by

<module_name> ( <bindings> )

where <module_name> is the name of a parameterized module, and <bindings> is a comma-separated list of binding constructs.

using declared views ~ you may bind an already declared view to a parameter:

`<parameter> <= <view_name>`

If a module `M` has a parameter `X :: T` and a view `V` from `T`
to `M'` is declared, `V` may be bound to `X`, with the effect that

1. The sort and operator names of `T` that appear in the body
   of `M` are replaced by those in `M'`, in accordance with `V`,

2. The common submodules of `M` and `M'` are shared.

using ephemeral views ~ In this case the view is declared and used at the same time.

`<parameter> <= view to <mod_name> { <view_elements> }`

See [`view`](/CafeOBJ/cafeobj/wiki/view) for details concerning `<view_elements>`. The
`from` parameter in the `view` declaration is taken from
`<parameter>`.

To make notation more succinct, parameters can be identified also by position instead of names as in

<mod_name> ( <view_name>, <view_name> )

which would bind the <view_name>s to the respective parameters of the parameterized module <mod_name>.

This can be combined with the ephemeral definition of a view like in the following example (assume ILIST has two parameters):

module NAT-ILIST {
  protecting ( ILIST(SIMPLE-NAT { sort Elt -> Nat },
                     DATATYPE   { sort Elt -> Data }) )
}