Frontend generated semantics to implement the `SUBSTITION` module

Start by locating the frontend compiler pass and the SUBSTITUTION module implementation. Compare the generated free-variable, fresh-variable, and substitution semantics against the specification, including the binder cases. Done means the frontend generates these declarations and rules without hooked sorts or function symbols, with coverage for the stated binder conditions.

Here's a rough specification of how a frontend pass in the compiler pipeline would implement variable binding semantics for the SUBSTITUTION module without using any hooked sorts or function symbols.

First, the user would import the SUBSTITUTION module.

Then, the user defines a symbol with the binder attribute:

  syntax S1 ::= binder( KVar, S2 ) [binder]

• It must have exactly 2 nonterminals
• The first nonterminal must be KVar, which is imported from SUBSTITUTION

If the user hasn't declared KVar as a subsort of S2, then the compiler will create that declaration so variables can appear in productions of sort S2.

Syntax/Rule generation

Given the above binder production, the compiler will generate the following productions/rules:

The free variable set

A function to obtain the set of free variables for any production of sort S2 get produced.

  syntax Set ::= freeVars(S2) [function]
  rule freeVars(V:KVar) => SetItem(V)
  // rules for every production of sort P
  rule freeVars(symbol(X0,...,Xn):S2) => {freeVars(X) for X:S2 in X0,...,Xn}

If the binder production itself is of sort S2, then it has a special case:

  rule freeVars(binder(V, X)) => freeVars(X) -Set SetItem(V)

The fresh variable generation

Given a set of free variables, produce a fresh variable that doesn't collide with any of the free variables

  syntax KVar ::= freshVar(KVar, Int, Set) [function]
  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi

(KVar is going to be a subsort of Id, so we use Id manipulation functions to create the fresh variables)

The substitution function

Substitute the occurrence of a variable in a production of sort S2 with a production also of sort S2

  syntax S2 ::= S2 "[" S2 "/" KVar "]" [function]

  rule X [_ / _] => X [owise]
  rule X:KVar [ V / X ] => V

  // rules for all other productions of sort P
  rule symbol(X0,...,Xn):S2 [V / X] => symbol([Y [V / X] if Y:S2 else Y for Y in X0,...Xn])

If the binder production itself is of sort S2, then it has a special case for substitution semantics:

  rule binder(X,E) [_ / X] => binder(X,E)
  rule binder(X,E) [V / Y] => binder(X,E[V / Y]) requires X =/=K Y andBool notBool X in freeVars(E)
  rule binder(X,E) [V / Y] => #let Z = freshVar(X, 0, freeVars(E) freeVars(V)) #in binder(Z,E[Z/X][V/Y])
    requires X =/=K Y andBool X in freeVars(E)

These transformations should be an adequate replacement of the hooked symbols in the SUBSTITUTION module. There's possibly an improvement to be made by making some slightly different rules depending on whether kompilation is being done on a concrete or symbolic backend (ie. on a symbolic backend, fresh variable generation can be freshVar(_,_,S) => ?X:KVar ensures notBool ?X in S)