Rewrite module

Rewrite module

The rewrite procedure is shown in Figure 6.2 below. In addition to implementation of the $R_{wrt}$ rules defined in Section~\ref{sec:link_rewrite}, the rewrite module $R_{wrt}$ has other practical considerations, such as identifier naming pattern checking, global schemas localisation, and schemas as predicates to predicates in the behavioural part. These are discussed as follows. The input to the rewrite module is AST$_+$ from the \Circus\ typechecker. Since inheriting sections are new to ISO Z but not in ZRM Z, our first step of rewrite is to combine them together into one big section.