Make user-defined sorts accessible in "\dl_" escapes

[WolframPfeifer]

As described in #3402, user-defined sorts (from a .key file) cannot be used inside "\dl_" escapes. This PR changes this by reading the sorts and function/predicate definitions of the .key file before parsing JML. Note that the PR should also work for datatypes, since they are pretransformed into sorts and rules before reading the file. However, this is still untested.

In addition, this PR changes the handling of default values (relevant when declaring a ghost field of a user-defined sort).
Earlier, the default value was read from a doc comment /*! @defaultValue(x) */ attached to the sort declaration. However, this has drawbacks:

• The semantics depend on comments, changing the comments might change the semantics of the specification.
• x was only allowed to be a constant, which is quite restrictive
  With this PR, the existing sort-depending constant x::defaultValue (from heap.key) is used as default. A concrete value can be assigned with a taclet.

Here is a small example with the sort IntPair:

\sorts {
    /*! @defaultValue(emptyPair) */    // <-- not needed anymore with this PR
    IntPair;
}

\functions {
    // IntPair emptyPair;              // <-- not needed anymore with this PR
    \unique IntPair ip(int, int);   // constructor
    int fst(IntPair);               // selector function
    int snd(IntPair);               // selector function
}

\rules {
    defaultValueOfIntPair {
        \find (IntPair::defaultValue)
        \replacewith (ip(0,0))
        \heuristics(simplify)
    };

    fstOfIp {
        \schemaVar \term int a, b;
        \find (fst(ip(a, b)))
        \replacewith (a)
        \heuristics(simplify)
    };

    sndOfIp {
        \schemaVar \term int a, b;
        \find (snd(ip(a, b)))
        \replacewith (b)
        \heuristics(simplify)
    };
}

\javaSource ".";

\chooseContract

Java File:

class IntTriple {
                        // abstract state
    //@ ghost int x;
    //@ ghost \dl_IntPair yz;                     // default value is needed here!

    int a, b, c;        // concrete state

                        // coupling invariant
    //@ invariant a == x && \dl_fst(yz) == b && \dl_snd(yz) == c;

    //@ ensures yz == \dl_ip(0,0);      // (auto) provable
    IntTriple() {
    }

    /*@ normal_behavior
      @  requires true;
      @  ensures \result == \dl_fst(yz);   // (auto) provable
      @  assignable \nothing;
      @*/
    int getSecond() {
        return b;
    }
}

The PR is still a draft because I want to see if the tests succeed first. Also, the x instanceof KeYFile seems a bit hacky, I don't know if it works for other cases ...

Related Issue

This pull request resolves #3402.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: Manually with the example given above.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[WolframPfeifer]

The removal of @defaultValue treatment does not really seem like a huge breaking change, since it was not even used once in the KeY repo.