refreshVariable should avoid allocation

[ttuegel]

refreshVariable is performance critical and instances should avoid allocating whenever possible. Profiling indicates this is a significant hot spot. I suggest the following refactoring so that we can use a non-allocating implementation whenever possible:

class SortedVariable variable where
    -- New: A Lens to get *or* set the Sort
    lensVariableSort :: Lens' variable sort

    sortedVariableSort = Lens.view lensVariableSort

class (Ord variable, SortedVariable variable) =>  FreshVariable variable where
    -- New: The greatest lower bound on variables
    -- with the same name as the given variable.
    infVariable :: variable -> variable
    -- New: The least upper bound on variables
    -- with the same name as the given variable.
    supVariable :: variable -> variable
    -- New: The least variable greater than the given variable.
    nextVariable :: variable -> variable

    -- This is a default implementation in terms of the above.
    -- The default implementation is suitable for most types
    -- and does O(1) allocation.
    refreshVariable :: Set variable -> variable -> Maybe variable

[ttuegel]

As an example, the instance for the basic Variable type would be

instance FreshVariable Variable where
    infVariable variable = variable { variableCounter = Nothing }
    supVariable variable = variable { variableCounter = Just Sup }
    nextVariable variable = {- already implemented, see below -}
    refreshVariable avoiding variable = do
        fixedLargest <- Lens.set lensVariableSort theSort <$> Set.lookupLT pivotMax avoiding
        Monad.guard (fixedLargest >= pivotMin)
        return (nextVariable fixedLargest)
      where
        pivotMax = supVariable variable
        pivotMin = infVariable variable
        theSort = Lens.view lensVariableSort variable

The nextVariable function is already implemented, but it's not a member of the class.

Some pseudo-code properties:

properties = do -- this line is to make GitHub's syntax highlighting happy
    -- generators for different variable types in Test.Kore
    variable <- ...

    -- any variable is between infVariable and supVariable:
    infVariable variable <= variable
    variable < supVariable variable

    -- nextVariable generates an increasing sequence of variables with the same "stem" (the text part of the name):
    variable < nextVariable variable
    nextVariable variable < nextVariable (nextVariable variable)
    --      etc.

    -- supVariable is strictly greater than every variable in the sequence:
    nextVariable variable < supVariable variable
    nextVariable (nextVariable variable) < supVariable variable
    --      etc.

    -- refreshVariable keeps the same sort:
    refreshVariable _ variable = Nothing or (Just variable' and sort variable' == sort variable)

    -- refreshVariable never returns the same variable:
    refreshVariable _ variable = Nothing or (Just variable' and variable' /= variable)

    -- refreshVariable must return a new variable if its argument appears in the set:
    Set.member variable avoiding `implies` refreshVariable avoiding variable = Just _

[ttuegel]

We are having some problems implementing this because the Target variable type has two responsibilities and one of them is at odds with the FreshVariable class. The first responsibility of Target is the Ord instance, which ensures that we prefer to instantiate rule variables (Target-ed variables) instead of narrowing configuration variables; this is not a problem for FreshVariable. The second responsibility is renaming rule variables; this conflicts with FreshVariable.

I think we should drop the second responsibility. The code is cleaner when each thing has one responsibility. We still must rename rule variables when we un-Target them. I think the straightforward solution for that is:

1. Fix mapVariables so that it does not capture variables. (Related: Create a Substitute class #1383)
2. Modify Kore.Variables.Target.unwrapVariable Add Kore.Variables.Target.wrapTarget to use refreshVariable so that Target variables are renamed after before the rule is applied.

EDIT: The second item above will not work. I don't think we can use the Ord instance of Target for both fresh names and prioritizing variables during unification. One way to resolve this tension would be to remove Target and have the unifier store the priority order of variables in its internal state. I favor this solution, as opposed to annotating variables like we do now, because it seems to me that the priority order actually is part of the internal state of the unifier. We could also give a finer order to variables than the Target vs NonTarget distinction we make now. However, I also can't think of any other solution at the moment, so I'd like to hear everyone else's brainstorms.