Revise different test data generators for `TermLike`

[jberthold]

We currently have several test data generators that generate similar things, in Test.ConsistentKore and in Test.Kore. The TermLike generator in Test.ConsistentKore has been specialised to actual terms in #3256 but the one in Test.Kore continues to be provided to other modules from Test.Kore.TermLike.

• [x] Analyse what the different generators do differently. There seems to be a discrepancy wrt. their pool of free variables, and maybe the generators are incomplete (in a different way than the desired incompleteness from #3244 ).
• [x] Audit usage of the different generators in other test modules. Which one should be used where?
• [X] When generating applications with Map/Set symbols at the top, do not generate children terms with connectives.

  3262 addresses this more generally by avoiding connectives inside all function symbols.

• [ ] Check whether the mock setup for the ConsistentKore generator is complete. One of the requirements is to have nullary constructors for all possible sorts. (maybe related to #3257).
• [x] Analyse why the ConsistentKore generator loops when removing the \top generator.
• [ ] (after results from the above and #3257 are addressed) Is it possible to always use the ConsistentKore generator (maybe using the pattern generator) where previously we were using the TermLike generator?
• [ ] Remove code related to generating internalized maps and sets

[jberthold]

Test.ConsistentKore

• primarily a generator for Internal.Pattern
• generates term and predicate using separate generators
  • predicate can be something containing terms (\ceil, \floor, \in, \equals)
• Many non-terms (e.g., fix point operators, implication) have been removed from the generator in a recent PR
• Operates based on a Setup and a Context:
  • Setup contains "known" things like all sorts, specific sorts for built-in types like Bool and Int, symbols assumed to exist, etc.
  • Context contains available (element and set) variables as well as restriction flags to control term generation.
  • However does not modify the context when generating \forall or \exists predicates (which introduce fresh sorted variables)
• Code exists to generate Map and Set terms but the configuration seems to not trigger it.

Test.Kore

• defines a Gen type that uses an internal Context
  • Context contains "objectVariables" (just SomeVariables) and "ObjectSortVariables" (SortVariables), as well as optional lists of known symbols and sorts
  • Gen is again a ReaderT Context Hedgehog.Gen using the context for variables, sorts, and symbols during generation.
  • when generating sorts or applications, the lists are used if they are provided, otherwise a random symbol or sort will be generated.
  • No mechanism is provided to ensure that the given symbols only use the provided sorts.
• contains a generator for Predicates
  • parametric in the TermLike generator for its children
  • using an obsolete patternSort' :: Sort argument
• contains a generator for ParsedPattern (i.e., Syntax.PatternF)
• contains a sentence generator (Gen ParsedSentence, using the pattern generator)
  • this one is used in Unparse tests
• The provided Symbols are merely syntactic, not Kore.Internal.Symbol, and random Sorts (from the provided sorts) will be used when using a provided symbol to generate something

Test.Kore.Internal.TermLike

• contains a generator for TermLike, based on Test.Kore.Gen
• This generator uses its own symbolGen generating a (random!) Internal.Symbol (so again not sort-consistent or repeatable)
• Many (but not all) constructors for TermLike are used
  • in particular, no maps or sets are generated

Usage (including indirect)

• Test.ConsistentKore:
  • (termGen not exported)
  • patternGen used in Test.Kore.Simplify.IntegrationProperty, and in Test.Kore.Internal.TermLike for round trip testing with the syntactic Pattern type.
• Test.Kore:
  • standaloneGen is frequently used to generate element variables, and in some roundtrip tests for sentences, as well as predicate evaluation (bool predicates)
  • many of the generators are used in Unparse tests
  • predicateGen is unused, but predicateChildGen is (once)
  • idGen is used in several modules, including ConsistentKore
• Test.Kore.Internal.TermLike:
  • Directly used in Test.Kore.Internal.Pattern (round trip testing). This is probably the right choice, since the TermLike needs to be varied. One could start from a generated pattern, though.
  • Indirect use (producing a Pattern via Pattern.fromTermLike) in Test.Kore.Internal.OrPattern. This is suboptimal because fromTermLike blindly copies the given TermLike into the term field of the pattern (unmodified); parsePatternFromTermLike would be better here.

[ana-pantilie]

@ana-pantilie take a look at ^.

@jberthold when you see the simplification timeout happening please record the pattern here.

[jberthold]

Latest observed Timeout

WARNING: unable to simplify pattern
\and{mapSort{}}(
    /* term: */
    /*  */
    \or{mapSort{}}(
        /*  */
        \and{mapSort{}}(
            /* D Spa */
            elementMap{}(
                /* D Sfa Cl */
                sigma{}(
                    /* Fl Fn D Sfa Cl */ d{}(),
                    /* D Sfa Cl */
                    functionalConstr20{}(
                        /* D Sfa Cl */
                        functionalConstr30{}(
                            /* D Sfa Cl */
                            constr10{}(
                                /* D Sfa Cl */
                                functionalConstr30{}(
                                    /* D Sfa Cl */ constr00{}(),
                                    /* D Sfa Cl */
                                    functionalTopConstr20{}(
                                        /* Fl Fn D Sfa Cl */ aTopSort{}(),
                                        /* D Sfa Cl */
                                        constr10{}(/* Fl Fn D Sfa Cl */ a{}())
                                    ),
                                    /* D Sfa Cl */ constr00{}()
                                )
                            ),
                            /* D Sfa Cl */
                            functionalConstr21{}(
                                /* D Sfa Cl */
                                functionalConstr30{}(
                                    /* D Sfa Cl */
                                    constr11{}(
                                        /* Fl Fn D Sfa Cl */
                                        functionalConstr11{}(
                                            /* Fl Fn D Sfa Cl */ e{}()
                                        )
                                    ),
                                    /* D Sfa Cl */
                                    functionalConstr10{}(
                                        /* D Sfa Cl */
                                        constr11{}(/* Fl Fn D Sfa Cl */ b{}())
                                    ),
                                    /* Fl Fn D Sfa Cl */
                                    functionalConstr11{}(
                                        /* Fl Fn D Sfa Cl */
                                        functionalConstr11{}(
                                            /* Fl Fn D Sfa Cl */ a{}()
                                        )
                                    )
                                ),
                                /* Fl Fn D Sfa Cl */ d{}()
                            ),
                            /* Fl Fn D Sfa Cl */ c{}()
                        ),
                        /* D Sfa Cl */ constr00{}()
                    )
                ),
                /* D Sfa Cl */
                functionalConstr30{}(
                    /* D Sfa Cl */
                    functionalConstr30{}(
                        /* D Sfa Cl */
                        constr20{}(
                            /* D Sfa Cl */
                            constr20{}(
                                /* D Sfa Cl */
                                functionalConstr12{}(
                                    /* D Sfa Cl */
                                    constr10{}(/* D Sfa Cl */ constr00{}())
                                ),
                                /* D Sfa Cl */
                                sigma{}(
                                    /* Fl Fn D Sfa Cl */ b{}(),
                                    /* D Sfa Cl */
                                    constr11{}(
                                        /* Fl Fn D Sfa Cl */
                                        functionalConstr11{}(
                                            /* Fl Fn D Sfa Cl */ e{}()
                                        )
                                    )
                                )
                            ),
                            /* D Sfa Cl */
                            functionalConstr20{}(
                                /* D Sfa Cl */
                                functionalConstr21{}(
                                    /* D Sfa Cl */
                                    functionalConstr21{}(
                                        /* Fl Fn D Sfa Cl */ d{}(),
                                        /* D Sfa Cl */ constr00{}()
                                    ),
                                    /* D Sfa Cl */
                                    constr11{}(
                                        /* D Sfa Cl */
                                        constr10{}(/* Fl Fn D Sfa Cl */ a{}())
                                    )
                                ),
                                /* Fl Fn D Sfa Cl */ a{}()
                            )
                        ),
                        /* Fl Fn D Sfa Cl */ d{}(),
                        /* Fl Fn D Sfa Cl */
                        functionalConstr20{}(
                            /* Fl Fn D Sfa Cl */
                            functionalConstr10{}(
                                /* Fl Fn D Sfa Cl */
                                functionalConstr20{}(
                                    /* Fl Fn D Sfa Cl */
                                    sigma{}(
                                        /* Fl Fn D Sfa Cl */
                                        functionalTopConstr21{}(
                                            /* Fl Fn D Sfa Cl */ a{}(),
                                            /* Fl Fn D Sfa Cl */ aTopSort{}()
                                        ),
                                        /* Fl Fn D Sfa Cl */
                                        functionalTopConstr21{}(
                                            /* Fl Fn D Sfa Cl */ b{}(),
                                            /* Fl Fn D Sfa Cl */ aTopSort{}()
                                        )
                                    ),
                                    /* Fl Fn D Sfa Cl */ a{}()
                                )
                            ),
                            /* Fl Fn D Sfa Cl */ d{}()
                        )
                    ),
                    /* Fl Fn D Sfa Cl */
                    functionalConstr10{}(/* Fl Fn D Sfa Cl */ a{}()),
                    /* D Sfa Cl */ constr10{}(/* Fl Fn D Sfa Cl */ c{}())
                )
            ),
            /*  */
            \and{mapSort{}}(
                /* Fn */
                concatMap{}(
                    /* Fn */
                    concatMap{}(
                        /* Fl Fn D */ unitMap{}(),
                        /* Fl Fn D */ unitMap{}()
                    ),
                    /* Fn */
                    concatMap{}(
                        /* Fl Fn D */ unitMap{}(),
                        /* Fn */
                        opaqueMap{}(
                            /* Fn */
                            functionSMT{}(/* Fl Fn D */ functional00{}())
                        )
                    )
                ),
                /*  */
                \and{mapSort{}}(
                    /* D Spa */
                    elementMap{}(
                        /* Fl Fn D Sfa Cl */
                        functionalTopConstr20{}(
                            /* Fl Fn D Sfa Cl */ aTopSort{}(),
                            /* Fl Fn D Sfa Cl */ e{}()
                        ),
                        /* D Sfa Cl */
                        functionalConstr20{}(
                            /* Fl Fn D Sfa Cl */ b{}(),
                            /* D Sfa Cl */
                            functionalConstr30{}(
                                /* Fl Fn D Sfa Cl */ a{}(),
                                /* D Sfa Cl */
                                functionalConstr30{}(
                                    /* Fl Fn D Sfa Cl */
                                    functionalConstr11{}(
                                        /* Fl Fn D Sfa Cl */
                                        functionalConstr30{}(
                                            /* Fl Fn D Sfa Cl */ a{}(),
                                            /* Fl Fn D Sfa Cl */ b{}(),
                                            /* Fl Fn D Sfa Cl */ e{}()
                                        )
                                    ),
                                    /* D Sfa Cl */
                                    constr10{}(
                                        /* D Sfa Cl */
                                        constr20{}(
                                            /* Fl Fn D Sfa Cl */ e{}(),
                                            /* Fl Fn D Sfa Cl */ d{}()
                                        )
                                    ),
                                    /* Fl Fn D Sfa Cl */
                                    functionalTopConstr21{}(
                                        /* Fl Fn D Sfa Cl */ b{}(),
                                        /* Fl Fn D Sfa Cl */ aTopSort{}()
                                    )
                                ),
                                /* D Sfa Cl */
                                sigma{}(
                                    /* D Sfa Cl */
                                    constr10{}(/* Fl Fn D Sfa Cl */ c{}()),
                                    /* Fl Fn D Sfa Cl */
                                    functionalTopConstr20{}(
                                        /* Fl Fn D Sfa Cl */ aTopSort{}(),
                                        /* Fl Fn D Sfa Cl */ b{}()
                                    )
                                )
                            )
                        )
                    ),
                    /* D */
                    \or{mapSort{}}(
                        /*  */
                        \and{mapSort{}}(
                            /* D */
                            \or{mapSort{}}(
                                /* Fn Spa */
                                opaqueMap{}(/* Fl Fn D Sfa Cl */ c{}()),
                                /* Fl Fn D */ unitMap{}()
                            ),
                            /*  */
                            opaqueMap{}(
                                /*  */
                                functional11{}(
                                    /*  */ injective11{}(/* Fn */ cf{}())
                                )
                            )
                        ),
                        /* D Spa */
                        elementMap{}(
                            /* D Sfa Cl */
                            constr11{}(
                                /* D Sfa Cl */
                                functionalConstr30{}(
                                    /* D Sfa Cl */ constr00{}(),
                                    /* Fl Fn D Sfa Cl */
                                    functionalConstr21{}(
                                        /* Fl Fn D Sfa Cl */ e{}(),
                                        /* Fl Fn D Sfa Cl */ d{}()
                                    ),
                                    /* Fl Fn D Sfa Cl */
                                    functionalTopConstr20{}(
                                        /* Fl Fn D Sfa Cl */ aTopSort{}(),
                                        /* Fl Fn D Sfa Cl */ a{}()
                                    )
                                )
                            ),
                            /* D Sfa Cl */
                            functionalTopConstr21{}(
                                /* D Sfa Cl */
                                constr20{}(
                                    /* D Sfa Cl */
                                    functionalTopConstr21{}(
                                        /* D Sfa Cl */
                                        constr11{}(/* Fl Fn D Sfa Cl */ e{}()),
                                        /* Fl Fn D Sfa Cl */ aTopSort{}()
                                    ),
                                    /* Fl Fn D Sfa Cl */ b{}()
                                ),
                                /* Fl Fn D Sfa Cl */ aTopSort{}()
                            )
                        )
                    )
                )
            )
        ),
        /*  */
        concatMap{}(
            /*  */
            concatMap{}(
                /* D */
                \or{mapSort{}}(
                    /* Fl Fn D Spa */
                    elementMap{}(
                        /* Fl Fn D Sfa Cl */ d{}(),
                        /* Fl Fn D Sfa Cl */ b{}()
                    ),
                    /*  */
                    concatMap{}(
                        /*  */
                        \and{mapSort{}}(
                            /*  */
                            \and{mapSort{}}(
                                /*  */
                                \and{mapSort{}}(
                                    /* Fl Fn D */ unitMap{}(),
                                    /* D */
                                    \or{mapSort{}}(
                                        /* Fl Fn D */ unitMap{}(),
                                        /* Fn */
                                        concatMap{}(
                                            /* Fl Fn D */ unitMap{}(),
                                            /* Fl Fn D */ unitMap{}()
                                        )
                                    )
                                ),
                                /* Fn Spa */
                                opaqueMap{}(/* Fl Fn D Sfa Cl */ c{}())
                            ),
                            /*  */
                            concatMap{}(
                                /* Fn Spa */
                                opaqueMap{}(/* Fl Fn D Sfa Cl */ d{}()),
                                /*  */
                                concatMap{}(
                                    /* Fl Fn D Spa */
                                    elementMap{}(
                                        /* Fl Fn D Sfa Cl */ b{}(),
                                        /* Fl Fn D Sfa Cl */
                                        sigma{}(
                                            /* Fl Fn D Sfa Cl */ d{}(),
                                            /* Fl Fn D Sfa Cl */ d{}()
                                        )
                                    ),
                                    /*  */
                                    \and{mapSort{}}(
                                        /* Fn */ opaqueMap{}(/* Fn */ ch{}()),
                                        /* Fn */
                                        concatMap{}(
                                            /* Fl Fn D */ unitMap{}(),
                                            /* Fl Fn D */ unitMap{}()
                                        )
                                    )
                                )
                            )
                        ),
                        /*  */
                        \and{mapSort{}}(
                            /*  */
                            opaqueMap{}(
                                /*  */
                                \and{testSort{}}(
                                    /* Fn */ ch{}(),
                                    /* Fn */
                                    functionalConstr11{}(
                                        /* Fn */
                                        constrFunct20TestMap{}(
                                            /* Fn */ ch{}(),
                                            /* Fl Fn D */ unitMap{}()
                                        )
                                    )
                                )
                            ),
                            /* D Spa */
                            elementMap{}(
                                /* D Sfa Cl */
                                functionalConstr30{}(
                                    /* Fl Fn D Sfa Cl */
                                    functionalConstr30{}(
                                        /* Fl Fn D Sfa Cl */ b{}(),
                                        /* Fl Fn D Sfa Cl */
                                        functionalTopConstr21{}(
                                            /* Fl Fn D Sfa Cl */ e{}(),
                                            /* Fl Fn D Sfa Cl */ aTopSort{}()
                                        ),
                                        /* Fl Fn D Sfa Cl */
                                        sigma{}(
                                            /* Fl Fn D Sfa Cl */ c{}(),
                                            /* Fl Fn D Sfa Cl */ c{}()
                                        )
                                    ),
                                    /* D Sfa Cl */
                                    constr20{}(
                                        /* D Sfa Cl */
                                        constr11{}(/* Fl Fn D Sfa Cl */ a{}()),
                                        /* Fl Fn D Sfa Cl */ c{}()
                                    ),
                                    /* D Sfa Cl */
                                    constr20{}(
                                        /* D Sfa Cl */
                                        constr11{}(/* Fl Fn D Sfa Cl */ d{}()),
                                        /* D Sfa Cl */
                                        functionalConstr21{}(
                                            /* Fl Fn D Sfa Cl */ a{}(),
                                            /* D Sfa Cl */ constr00{}()
                                        )
                                    )
                                ),
                                /* Fl Fn D Sfa Cl */ d{}()
                            )
                        )
                    )
                ),
                /* Fl Fn D */ unitMap{}()
            ),
            /* D */
            \or{mapSort{}}(
                /*  */
                concatMap{}(
                    /*  */
                    concatMap{}(
                        /*  */
                        concatMap{}(
                            /*  */
                            \and{mapSort{}}(
                                /* Fl Fn D */ unitMap{}(),
                                /* D Spa */
                                elementMap{}(
                                    /* D Sfa Cl */
                                    functionalConstr30{}(
                                        /* D Sfa Cl */
                                        constr11{}(/* Fl Fn D Sfa Cl */ b{}()),
                                        /* Fl Fn D Sfa Cl */
                                        functionalConstr12{}(
                                            /* Fl Fn D Sfa Cl */ e{}()
                                        ),
                                        /* D Sfa Cl */
                                        constr10{}(/* D Sfa Cl */ constr00{}())
                                    ),
                                    /* Fl Fn D Sfa Cl */ e{}()
                                )
                            ),
                            /*  */
                            concatMap{}(
                                /*  */
                                concatMap{}(
                                    /*  */
                                    concatMap{}(
                                        /* Fn */
                                        opaqueMap{}(
                                            /* Fl Fn D */ functional00{}()
                                        ),
                                        /* D */
                                        \or{mapSort{}}(
                                            /* Fl Fn D */ unitMap{}(),
                                            /* Fl Fn D */ unitMap{}()
                                        )
                                    ),
                                    /*  */
                                    \and{mapSort{}}(
                                        /* Fl Fn D */ unitMap{}(),
                                        /* D */
                                        \or{mapSort{}}(
                                            /* Fl Fn D */ unitMap{}(),
                                            /* Fl Fn D */ unitMap{}()
                                        )
                                    )
                                ),
                                /* Spa */
                                concatMap{}(
                                    /* D Spa */
                                    elementMap{}(
                                        /* Fl Fn D Sfa Cl */ e{}(),
                                        /* D Sfa Cl */
                                        constr10{}(/* Fl Fn D Sfa Cl */ d{}())
                                    ),
                                    /* Fn Spa */
                                    opaqueMap{}(
                                        /* Fl Fn D Spa */
                                        functional10{}(
                                            /* Fl Fn D Sfa Cl */ c{}()
                                        )
                                    )
                                )
                            )
                        ),
                        /* Fn Spa */ opaqueMap{}(/* Fl Fn D Sfa Cl */ b{}())
                    ),
                    /* Fl Fn D */ unitMap{}()
                ),
                /* Fl Fn D */ unitMap{}()
            )
        )
    ),
\and{mapSort{}}(
    /* predicate: */
    /*  */
    \in{testSort{}, mapSort{}}(
        /* Fn */
        functionalConstr10{}(
            /* Fn */
            sigma{}(
                /* Fl Fn D Sfa Cl */ e{}(),
                /* Fn */
                function20MapTest{}(
                    /* Fl Fn D */ unitMap{}(),
                    /* Fn */
                    constrFunct20TestMap{}(
                        /* Fn */ f{}(/* Fn */ cg{}()),
                        /* Fn */
                        concatMap{}(
                            /* Fl Fn D */ unitMap{}(),
                            /* Fn */ opaqueMap{}(/* Fn */ ch{}())
                        )
                    )
                )
            )
        ),
        /* Fl Fn D Spa */ functional11{}(/* Fl Fn D Sfa Cl */ c{}())
    ),
    /* substitution: */
    \top{mapSort{}}()
))
TEST RUN PASSED

Duration:  35.251s
Passed:    5149

[ana-pantilie]

I found another instance of the failing property test, on https://github.com/runtimeverification/haskell-backend/pull/3276/commits/3c432059d822cc73f12066d89c56913441d47228.

Test suite kore-test: RUNNING...
↓ test/Driver.hs
↓ Test
↓ Kore
↓ Rewrite
↓ MockSymbols
↓ can generate consistent terms for all given sorts
↓ "mapSort"
✗ Size 9

  ✗ Size 9 failed at test/Test/Kore/Rewrite/MockSymbols.hs:2371:56
    after 1 test.

         ┏━━ test/Test/Kore/Rewrite/MockSymbols.hs ━━━
    2359 ┃ test_canGenerateConsistentTerms :: TestTree
    2360 ┃ test_canGenerateConsistentTerms =
    2361 ┃     testGroup "can generate consistent terms for all given sorts" $
    2362 ┃         map mkTest testSorts
    2363 ┃   where
    2364 ┃     testSorts = ConsistentKore.allSorts generatorSetup
    2365 ┃     sizes = map Range.Size [1 .. 10]
    2366 ┃ 
    2367 ┃     mkTest :: Sort -> TestTree
    2368 ┃     mkTest sort@(SortActualSort SortActual{sortActualName = InternedId{getInternedId}}) =
    2369 ┃         testGroup
    2370 ┃             (show getInternedId)
    2371 ┃             [ testProperty (show size) . withTests 1 . property $ do
         ┃             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
         ┃             │ ━━━ Exception (ErrorCall) ━━━
         ┃             │ Cannot generate terms for SortActualSort (SortActual {sortActualName = InternedId {getInternedId = "mapSort", internedIdLocation = AstLocationTest}, sortActualSorts = []})
         ┃             │ CallStack (from HasCallStack):
         ┃             │   error, called at test/Test/ConsistentKore.hs:231:20 in main:Test.ConsistentKore
    2372 ┃                 r <-
    2373 ┃                     forAll . Gen.resize size $
    2374 ┃                         ConsistentKore.runKoreGen
    2375 ┃                             generatorSetup
    2376 ┃                             (ConsistentKore.termLikeGenWithSort sort)
    2377 ┃                 -- just test that this works
    2378 ┃                 Hedgehog.diff 0 (<) (length $ show r)
    2379 ┃             | size <- sizes
    2380 ┃             ]
    2381 ┃     mkTest SortVariableSort{} =
    2382 ┃         error "Found a sort variable in the generator setup"

    This failure can be reproduced by running:
    > recheck (Size 0) (Seed 4041433232755941645 627379784105931223) Size 9

Use '--hedgehog-replay "Size 0 Seed 4041433232755941645 627379784105931223"' to reproduce.