====== The refine sublanguage ======

The ''refine'' sub-language takes the form

<code act>
refine {
    /* any standard ACT body element can appear here */
}
</code>

This is used to provide an implementation of a process that replaces the CHP, dataflow, HSE, or PRS body. For example, imagine you had a process defined at the CHP level

<code act>
defproc example (...)
{
   int x;
   chp {
      *[ L?x; R!x ]
   }
}
</code>

You can include its production-rule level description in the same process definition, as follows:

<code act>
defproc example (...)
{
   ...
   chp {
      *[ L?x; R!x ]
   }
   prs {
      // circuit goes here
   }
 }    
</code>
At this point, a tool can select the level of abstraction/detail for the process by picking one of the two sub-languages provided.

Now imagine that instead of writing the production rules directly, you'd like to instantiate a set of gates to implement the circuit. Suppose we write the following:
<code act>
defproc example(...)
{
  ...
  chp {
    *[ L?x; R!x ]
  }
  inst1 i1;
  inst2 i2;
  // the other instances and connctions...
}
</code>
As written, this means that the process has a CHP definition, and //in addition// it has the specified instances! This is not what we intended to specify; we'd like to use the CHP definition //or// the instances. 

To provide support for this, the ''refine'' body is used. The example would be written:
<code act>
defproc example(...)
{
  ...
  chp {
    *[ L?x; R!x ]
  }
  refine {
     inst1 i1;
     inst2 i2;
     // the other instances and connctions...
   }
}
</code>
Now you can //pick// the refined version of the process by using the ACT command-line option ''-ref=1'', and so a tool can pick either the ''chp'' or the ''refine'' sub-language, giving us the desired effect.

This approach is used in the ''chp2prs'' tool to provide an implementation of the CHP. This is the standard convention used in any tool that takes CHP and generates a circuit-level description. By augmenting the definition of the process in this manner, you can model the process at both the CHP level of abstraction as well as a more detailed representation containing a collection of instances that implement the CHP.

===== Nested refinements =====

Since ''refine { ... }'' blocks contain normal ACT statements, they can also include refine blocks within them.
Hence, you can say:

<code act>
refine {
    inst i1;
    chp { ... }
    refine { inst i2; }
}
</code>

When ACT selects the outer refinement block for the process, it decrements the refinement level before proceeding; the level is restored at the end of the refinement block. Hence, if  ''-ref=1'' were specified, then
the block:
<code act>
  inst i1;
  chp { ... }
  refine { inst i2; }
</code>
would be processed with the refinement level set to zero; hence, the ''chp { ... }'' body would be selected, and
not the nested refinement. To replace the CHP with the nested refinement block, use ''-ref=2''. Note that in both cases the instance ''i1'' would be processed.
  
===== Multiple refinement options =====

While the nested refinement approach works nicely when designs are recursively refined, it may not
be suitable for transformations where an existing refinement block needs to be completely replaced.
ACT has a mechanism to support this in the following manner:

<code act>
refine { 
    inst i1; 
    chp { ... }
}    
refine<2> {
    inst j1;
    prs { ... }
}
</code>

In this case, "-ref=2" will //replace// the first refine block with the second. In other words, instance ''i1'' will not
be created, and ''-ref=2'' will select instance ''j2'' and the ''prs { ... }'' body.

In general, a refine block has an associated integer refinement level (the default is one). When ACT processes a block with refinement level //r//, it searches for the largest refinement block with level that is at most //r//. (Note: this may be no block, in which case the block is processed as normal.) If a refine block with level //l// is found, then it processes all non-language constructs within the block and then expands the refinement block with level //l// by decrementing the current refinement level by //l//.