Generalize KAST-to-KORE conversion for KSequence

[tothtamas28]

• Allow items of sort K to appear at any position within a KSequence, not just at the end. During _kast_to_kore, an application of append is generated in such cases.
• Conversely, during _kore_to_kast, generate a KSequence for each append.
• Fix KVariable sort inference so that it does not override declared sorts of KSequence items.
• Update test_kast_to_kore_frontend to compare the Frontend’s result against expected outputs, rather than pyk's results. This makes it easier to add new tests based on the Frontend’s output.

[tothtamas28]

Unfortunately, these need to be excluded from kast tests (similarly to other KSequence tests), because for some reason when converting from json to kore, the result is wrapped in an inj into SortKItem:

% kast --definition /tmp/pytest-of-ttoth/pytest-current/kompiled0/simple-proofs-llvm-0 --input json --output kore --expression '{"format": "KAST", "version": 3, "term": {"node": "KSequence", "items": [{"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "X1", "sort": {"node": "KSort", "name": "K"}}, {"node": "KVariable", "name": "X2", "sort": {"node": "KSort", "name": "K"}}, {"node": "KVariable", "name": "X3", "sort": {"node": "KSort", "name": "K"}}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "X4", "sort": {"node": "KSort", "name": "K"}}], "arity": 6}}' --sort K
inj{SortK{}, SortKItem{}}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")),append{}(VarX1:SortK{},append{}(VarX2:SortK{},append{}(VarX3:SortK{},kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("2")),VarX4:SortK{}))))))

Funnily enough, kast is happy to inject the result into any sort (including undefined ones), except for K:

% kast --definition /tmp/pytest-of-ttoth/pytest-current/kompiled0/simple-proofs-llvm-0 --input json --output kore --expression '{"format": "KAST", "version": 3, "term": "..."}' --sort Whatever
inj{SortK{}, SortWhatever{}}(...)

For conversion from rule syntax, kast works as expected:

$ kast --definition /tmp/pytest-of-ttoth/pytest-current/kompiled0/simple-proofs-llvm-0 --input rule --output kore --expression '1 ~> X1:K ~> X2:K ~> X3:K ~> 2 ~> X4:K' --sort K
kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")),append{}(VarX1:SortK{},append{}(VarX2:SortK{},append{}(VarX3:SortK{},kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("2")),VarX4:SortK{})))))%

[jberthold]

LGTM. Funny behaviour with the KItem injection, though.