• Arch
• Equilty

What might an extension look like?

Profile of BLD, removing Equality:

Remove this production from the grammar:
   Equal = element Equal { side, side }

From this disjunction production, remove the "Equal" branch
   ATOMIC = Uniterm | Equal

or, in XML, something like:

<Profile>
   <changeList>
      <removeProduction>
         ... ID of that production?
      </removeProduction>
      <removeBranch>
         ... ID of the Equal non-terminal
      </removeBranch>
   <changeList>
   ... other information about the Profile
</Profile>

Let's call what that produces "BLDWOE" (BLD WithOutEquality).

The extension to BLDWOE to add Equality would look like this:

Add this production to the grammar:
   Equal = element Equal { side, side }

Modify this disjunctive production, adding an "Equal" branch:
   ATOMIC = Uniterm | Equal

or, in XML:

<Extension>
   <changeList>
      <addProduction>
         <Production>
             <result>Equal</result>
             <element>rif:Equal</element>
             <contentList>
                 <production>side</production>
                 <production>side</production>
             </contentList>
         </Production>
      </addProduction>
   ... the modify part...
   ... other information about the Profile
</Extension>

Now, ATOMIC is an intermedia class (non-terminal) without an disjunction, so it's purpose isn't clear. We might remove it. We might not have had it there in the first place.

Like this:

Remove this production from the grammar:
   Equal = element Equal { side, side }

Remove this production from the grammar:
   ATOMIC = Uniterm | Equal

Globally Replace the symbol "ATOMIC" with the symbol "Uniterm"

Let's say what that produces is BLDWOE2 (BLD WithOutEquality2).

To add Equality to BLDWOE2:

Add this production to the grammar:
   Equal = element Equal { side, side }

Add this production to the grammar:
   ATOMIC = Uniterm | Equal

In this production, replace "Uniterm" with "ATOMIC"
   RULE = Forall | Implies | Uniterm

In these production, replace "Uniterm" with "ATOMIC"
   RULE = Forall | Implies | Uniterm
   CONDITION = And | Or | Exists | Uniterm
   then = element then { Uniterm }

# note that we don't do it in 
#     TERM = Const | Var | Uniterm

If we write the grammars without intermedia classes, this is a lot simpler.