Give Predicate a distinct internal representation

[MirceaS]

Fixes #1442

---

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock

[ttuegel]

Suggested change

	-- TODO (thomas.tuegel): Lift 'simplified' to the 'Conditional' level once we
	-- treat the latter as an aggregate root.

[MirceaS]

TODO:

• Add back the tests removed from Predicate.hs to the simplification stage

[ttuegel]

Here is the actual error message:

    Internal error: expected simplified results, but found:                                                                                                               
        \and{SortK{}}(                   
            /* term: */                 
            /* Fl Fn D Sfa */
            Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
                /* Fl Fn D Sfa */ X0:SortBool{},                                                                                                                          
                /* Fl Fn D Sfa */ X1:SortK{},
                /* Fl Fn D Sfa */ X2:SortK{}                               
            ),                         
        \and{SortK{}}(                                                               
            /* predicate: */
            /* Spa */                                                                
            \and(                      
                /* Sfa */ \top(),                                                    
                /* Spa */  
                \and(                                                                
                    /* Spa */ \and(/* Sfa */ \top(), /* Sfa */ \top()),
                    /* Spa */                                                        
                    \and(  
                        /* Spa */ \and(/* Sfa */ \top(), /* Sfa */ \top()),   
                        /* Spa */ \and(/* Sfa */ \top(), /* Sfa */ \top())
                    )                                                                
                )
            ),
            /* substitution: */
            \top{SortK{}}()
        ))
      while simplifying:
        /* Fl Fn D Spa */
        Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
            /* Fl Fn D Sfa */ X0:SortBool{},
            /* Fl Fn D Sfa */ X1:SortK{},
            /* Fl Fn D Sfa */ X2:SortK{}
        )
    CallStack (from HasCallStack):
      error, called at src/Kore/Step/Simplification/TermLike.hs:446:6 in kore-0.29.0.0-HuCMzubZJvo5rOwRZcR8X6:Kore.Step.Simplification.TermLike

It's not shown in Jenkins because many of the tests produce a lot of useless warnings, but you can copy and paste the failing command to remove the redirection.

This unsimplified predicate is a case which was handled by makeAndPredicate which must now be handled in the simplifier. As I said at the time, we need to add unit tests for these simplification cases.

[ttuegel]

@MirceaS The next thing we need to do here is check for performance regressions. You can start with the tests/regression-* tests in our own repository, but we also need to check these: https://github.com/kframework/evm-semantics/tree/master/tests/specs/benchmarks

We don't need to collect precise statistics here, just run everything once with the old and new versions to compare.

[MirceaS]

@ttuegel runs of tests in test/regression-evm-semantics-39dd1e5/ and test/regression-wasm-semantics-5372938/ are pretty much identical on both master and this branch in terms of time and memory allocation.
Also, looking on Jenkins, the integration tests took about 30 minutes on this branch while on master they seem to take about 32 minutes, so I don't think there's any performance regressions being introduced.
The EVM benchmark tests (test-prove-benchmarks make target) are very similar on both master and this branch.

[ttuegel]

What is the difference between prettyConditional and prettyConditional'?

[MirceaS]

prettyConditional' doesn't take a sort as input and is used to pretty print Conditionals that don't contain a TermLike that can be used to derive a sort (that is, Conditional variable (Predicate variable)).
See line 310 below.

[ttuegel]

Please add documentation to new types.

[MirceaS]

Is the comment I added good?

[ttuegel]

Suggested change

	makeTruePredicate' = (synthesize (TopF Top {topSort = ()})
	, NotChanged)
	makeTruePredicate' =
	(synthesize (TopF Top {topSort = ()}), NotChanged)

[MirceaS]

The reason why I wrote it like that is so that it is consistent in style with all the other maker functions: the body of the function followed by an extra, separate line where we specify whether the term changed or not. Should I still change it as in your example?

[ttuegel]

All of the make functions in this module should change to follow our style guide.

[ttuegel]

Why is this commented out?

[MirceaS]

For two reasons:

1. It might be inefficient to compare two entire predicate trees when calling this maker function (which I believe happens quite often).
2. This is not a simplification that existed in the original code, so this would change the behavior of the function. It might not break anything but it requires testing.

I left it in as a comment in case we decide at some point that we do want it.

[ttuegel]

Please remove the comment.