Bug: kore-match-disjunction returns \bottom when it should not

[dwightguth]

How to run:

The --bug-report flag seems to generate an archive that is completely empty except for an empty text file, so I pushed the files involved to the search-example branch of kframework/k. You can reproduce by running cd k-distribution/tests/regression-new/imp++-llvm/; kore-match-disjunction definition.kore --module IMP --disjunction disjunction.kore --match pattern.kore

Expected behavior: should return 4 solutions. Actual behavior: returns \bottom

[andreiburdusa]

In Kore.Builtin.List.unifyEquals we are trying to unify two lists, each formed by applying concatenation symbol to two arguments. But we only treat two cases: either each list consists of a builtin list concatenated to a variable (framed right) or of a variable concatenated to a builtin list (framed left). In the present case we receive a concatenation between a variable and a list, to be unified with a concatenation between two lists, none of the list being builtin lists (InternalList_). Should it be possible to unify something framed with something which is not framed?

[dwightguth]

A better question might be, why isn't the contents of the <output> cell in disjunction.kore being represented as an internal list? it's a fully concrete list, so I see no reason why it shouldn't be represented by whatever your internal type is.

[andreiburdusa]

@virgil-serbanuta I see you did some work on this, three years ago. By any chance, do you remember how it should work? Should the lists be represented as InternalList_ at that point? Can you help us answer Dwight's question?

[virgil-serbanuta]

I don't fully understand the problem, and it would take me a while to figure out all the missing details. Should we try a video conference on Hangouts or Slack tomorrow? I'll send you more details over Slack.

[virgil-serbanuta]

Summary of the meeting:

1. It's not 100% clear (at least to me) whether one should do matching or unification. They would work mostly the same, with differences for terms that are not fully constructor-based (including maps and sets). We assumed that unification is the right answer, since this should probably work the same way as the normal Haskell backend search, which probably uses unification.
2. It's not 100% clear to me whether the terms involved are fully simplified or not. I assumed that the disjunction is produced by the LLVM backend while executing, so it's probably fully simplified, but the target pattern might not be so.
3. I don't know what design choices are preferable for the Haskell backend team.
4. Also, it's not clear to me how much performance matters, and how much it will be affected by the things I'll mention below.

With that being said:

List unification currently expects internalized lists, which can be achieved either through Builtin.internalize, or through simplification. The former is probably faster, but the patterns should already be fully simplified, while the latter is slower, but it will work in more cases. This may not matter since things like parsing and normalizing the definition may dominate the run time, but I have no way of knowing that.

One could also try to implement list unification on non-internalized lists, but my guess is that it's not really desirable. IIRC, when I worked on map unification, it did initially work on non-internalized maps, but Tom (I think) removed that, which made the code look better. By analogy, I assume that lists should also be internalized when unifying.

[andreiburdusa]

If unificationProcedure is replaced with matchIncremental the result becomes

Result

``` /* Spa */ \or{SortGeneratedTopCell{}}( /* Spa */ \or{SortGeneratedTopCell{}}( /* Spa */ \or{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \equals{SortThreadsCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'0:SortThreadsCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'threads'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}( dotk{}() ), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("0") ) ) ), Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}( dotk{}() ), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) ) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("2") ) ) ), /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}( dotk{}() ), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("4") ) ) ) )) ) ), /* Spa */ \equals{SortInputCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'1:SortInputCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'input'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}( /* Fl Fn D Sfa Cl */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("") ), /* Fl Fn D Sfa Cl */ dotk{}() ) ) ) ), Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'istream'LParUndsRParUnds'STDIN-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) )) ) ) ), /* Spa */ \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar0:SortGeneratedCounterCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5") ) ) ), /* Spa */ \equals{SortList{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortList{}, /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'ostream'LParUndsRParUnds'STDOUT-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ) ) ) ), /* Spa */ \equals{SortString{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStdout:SortString{}, /* Fl Fn D Sfa Cl */ \dv{SortString{}}("x = 16\x0a") ) ), /* Spa */ \equals{SortMap{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStore:SortMap{}, /* Fl Fn D Sfa Cl */ /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("4") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("16") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2") ) ) )) ) ), /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \equals{SortThreadsCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'0:SortThreadsCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'threads'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}( dotk{}() ), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("0") ) ) ), Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}( dotk{}() ), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) ) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("2") ) ) ), /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}( dotk{}() ), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("4") ) ) ) )) ) ), /* Spa */ \equals{SortInputCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'1:SortInputCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'input'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}( /* Fl Fn D Sfa Cl */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("") ), /* Fl Fn D Sfa Cl */ dotk{}() ) ) ) ), Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'istream'LParUndsRParUnds'STDIN-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) )) ) ) ), /* Spa */ \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar0:SortGeneratedCounterCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5") ) ) ), /* Spa */ \equals{SortList{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortList{}, /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'ostream'LParUndsRParUnds'STDOUT-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ) ) ) ), /* Spa */ \equals{SortString{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStdout:SortString{}, /* Fl Fn D Sfa Cl */ \dv{SortString{}}("x = 11\x0a") ) ), /* Spa */ \equals{SortMap{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStore:SortMap{}, /* Fl Fn D Sfa Cl */ /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("4") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("11") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2") ) ) )) ) ) ), /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \equals{SortThreadsCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'0:SortThreadsCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'threads'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}(dotk{}()), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("0") ) ) ), Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}(dotk{}()), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) ) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("2") ) ) ), /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}(dotk{}()), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("4") ) ) ) )) ) ), /* Spa */ \equals{SortInputCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'1:SortInputCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'input'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}( /* Fl Fn D Sfa Cl */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("") ), /* Fl Fn D Sfa Cl */ dotk{}() ) ) ) ), Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'istream'LParUndsRParUnds'STDIN-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) )) ) ) ), /* Spa */ \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar0:SortGeneratedCounterCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5") ) ) ), /* Spa */ \equals{SortList{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortList{}, /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'ostream'LParUndsRParUnds'STDOUT-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ) ) ) ), /* Spa */ \equals{SortString{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStdout:SortString{}, /* Fl Fn D Sfa Cl */ \dv{SortString{}}("x = 33\x0a") ) ), /* Spa */ \equals{SortMap{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStore:SortMap{}, /* Fl Fn D Sfa Cl */ /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("4") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("33") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2") ) ) )) ) ) ), /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}( /* Spa */ \equals{SortThreadsCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'0:SortThreadsCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'threads'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}(dotk{}()), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("0") ) ) ), Lbl'Unds'ThreadCellSet'Unds'{}( /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}(dotk{}()), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) ) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("2") ) ) ), /* concrete element: */ LblThreadCellSetItem{}( Lbl'-LT-'thread'-GT-'{}( Lbl'-LT-'k'-GT-'{}(dotk{}()), Lbl'-LT-'env'-GT-'{}( /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t2") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("3") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("x") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortId{}, SortKItem{}}( \dv{SortId{}}("t1") ), /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("1") ) ) )) ), Lbl'-LT-'id'-GT-'{}( \dv{SortInt{}}("4") ) ) ) )) ) ), /* Spa */ \equals{SortInputCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'1:SortInputCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'input'-GT-'{}( /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}( /* Fl Fn D Sfa Cl */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("") ), /* Fl Fn D Sfa Cl */ dotk{}() ) ) ) ), Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'istream'LParUndsRParUnds'STDIN-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) )) ) ) ), /* Spa */ \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar0:SortGeneratedCounterCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("5") ) ) ), /* Spa */ \equals{SortList{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ Var'Unds'DotVar2:SortList{}, /* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Unds'List'Unds'{}( LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortStream{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ Lbl'Hash'ostream'LParUndsRParUnds'STDOUT-STREAM'Unds'Stream'Unds'Int{}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) ), LblListItem{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortString{}}("off") ) ) ) ) ), /* Spa */ \equals{SortString{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStdout:SortString{}, /* Fl Fn D Sfa Cl */ \dv{SortString{}}("x = 21\x0a") ) ), /* Spa */ \equals{SortMap{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa */ VarStore:SortMap{}, /* Fl Fn D Sfa Cl */ /* InternalMap: */ Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3")), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("4") ) ), Lbl'Unds'Map'Unds'{}( /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("0")), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("21") ) ), /* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}( /* Inj: */ inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("2") ) ) )) ) ) ) ```

[andreiburdusa]

I looked at the matchPattern, the first item of disjunctionPattern and the first item of the result and tried to understand what the result means in terms of K cells from the input patterns using pencil and paper. All the \equals s seem to equate variables with the corect terms.

[andreiburdusa]

I inspected all the four terms from the result and they seem correct. @dwightguth Can you also check if the result is what you expected? (I posted the result two comments above)

[dwightguth]

Looks fine to me.