Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
language:langs:refine [2024/08/11 10:21] rajitlanguage:langs:refine [2025/04/21 19:58] (current) – [Refinement overrides] rajit
Line 73: Line 73:
 ===== Nested refinements ===== ===== 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 ===== ===== 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//.
 +
 +===== Refinement overrides =====
 +
 +Sometimes a refinement body needs to [[language:impl#overrides|override]] types. To support this, refinement bodies can be accompanied by refinement overrides. These are overrides that are only applied when the refinement is used.
 +
 +The syntax for providing refinement overrides is below:
 +
 +<code act>
 +refine<2>  +{ e1of2 l; } {
 +       inst1 i1; 
 +       ...
 + }
 +</code>
 +
 +This will apply the refinement override for ''l'' when this particular refinement body is selected.
 +  
 +   
 +
 +</code>