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.