[KIP] - Allow function symbols on LHS of rules

[ehildenb]

Motivation

When the pyk library generates claims/rules to be re-injected into the semantics, it's often working with states that have function symbols present. These function symbols are always "fully defined", in the sense that all the variables which show up under the function symbol come from other places on the LHS of the rule.

Example K

The following definition:

module TEST
    imports INT

    configuration <k> $PGM:Int </k> <mem> 0 </mem>

    syntax Int ::= f ( Int ) [function]
    rule f(X) => 10 requires X <=Int 30
    rule f(X) => 9  requires 30 <Int X

    rule <k> f(X) => 4 ... </k> <mem> X </mem>
    rule <k> Y => 3 ... </k> [owise]
endmodule

Should be transformed in this way automatically by the frontend:

-    rule <k> f(X) => 4 ... </k> <mem> X </mem>
+    rule <k> V => 4 ... </k> <mem> X </mem> requires V ==K f(X)

Currently the pyk library will need to make a bunch of extra effort to identify when it's going to generate a rule like this one and do this transformation itself manually. In particular, currently none of the analysis which the pyk library does even requires to know if things are function symbols or not, and this would require adding that functionality to pyk (specifically, to be able to tell if something is a function symbol).

However, it seems perfectly sound to allow function symbols on the LHS of rules using the above transformation, so maybe we should just lift this restriction. Then the pyk library can stay dumb instead of having to actually inspect the contents of the definition it's working with.

Note that this situation would be even better if we had where clauses: https://github.com/kframework/k/issues/1685. We could instead generate where clauses (instead of requires clauses), which can be handled more efficiently by both backends. But both encodings (with requires or where) should be sound.

[radumereuta]

• Change the current function check to allow for this
• make this transformation
• modify some of the checks. Traverse the LHS of the rule and where we see free variables under a function are all bound in places which are not functions.
• care not to apply this check on certain cases like: key of map lookup. Basically anywhere where we already allow functions on LHS.