Skip to content

Overhaul evaluators #2474

Open
Open
@ttuegel

Description

@ttuegel

Before #1978, I want to overhaul the function and simplification rule evaluators.

Move Kore.Step.Simplification to Kore.Simplify. This is one of the most important sub-domains, so it belongs at the top level of the hierarchy.

We will introduce a new class Evaluator with a single member evaluate with the same signature as BuiltinAndAxiomSimplifier. The latter will be an instance of the class. We will introduce an existential data type SomeEvaluator which can wrap a value of any instance of Evaluator. The Simplifier monad will by modified to hold a map of SomeEvaluator instead of BuiltinAndAxiomSimplifier.

We will move Kore.Step.Function to Kore.Function. definitionEvaluation will become Kore.Function.User.User (user-defined function evaluators) an instance of Evaluator. simplificationEvaluation will become Kore.Simplify.User.User (user-defined simplification evaluators), also a distinct instance of Evaluator. Basically, we will de-functionalize definitionEvaluation and simplificationEvaluation.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions