A refining local module may be employed in any context in which the refined local module is permitted by the base language, including a program module (as in section 16.4), an implementation module of a separate library module, or a local module contained within either.
Example 1: Generic modules to implement structures and those to implement data manipulation can be defined as in the examples in 16.2.1 and then combined in a new generic definition module using local modules. First create the generic definition module.
GENERIC DEFINITION MODULE ValidStacks (PType : TYPE; PValidProc : ValidProcType); TYPE ValidProcType = PROCEDURE (item : PType) : BOOLEAN; PROCEDURE PushValid (item : PType); END ValidStacks.
Then, combine the two by refining both within the implementation via local modules and then employing services from both so that, in this case, only valid items are pushed on the stack. In addition, note that the data items are to be defined in another module and are assumed to have ADT components available for use as follows:
(i) PType that can be mapped both to the Element required by Stacksand to the Item required by Validate
and
(ii) PValidProc compatible with the Validation required by Validate.
GENERIC IMPLEMENTATION MODULE ValidStacks (PType : TYPE; PValidProc : ValidProcType);
IMPORT Stacks, Validate;
MODULE MyStacks = Stacks (PType);
EXPORT QUALIFIED StackSize, Push, Pop, Empty;
END MyStacks;
MODULE MyValidate = Validate (PType, PValidProc);
EXPORT QUALIFIED Valid;
END MyValidate;
PROCEDURE PushValid (item : PType);
BEGIN
IF MyValidate.Valid (item) THEN
MyStacks.Push (item)
END (* if *)
END PushValid;
END ValidStacks.
These may then be refined further for a specific data type and validation procedure.