this is an attempt to standardize the simplifier functions into uniform "strategies" that can be combined together. Specifically, each strategy defines separate setup and execution phases. Strategies can be combined by combining these phases separately, so that their individual setup steps still only occur once in the resulting composite strategy.
this is motivated by an observation that multiple calls to a given simplification strategy (in the same
assumption context) should always use the same cache. However top-level entry point for simplifiers usually implicitly allocates a fresh cache. Multiple executions of that simplifier would therefore not use the same cache.
this is an attempt to standardize the simplifier functions into uniform "strategies" that can be combined together. Specifically, each strategy defines separate setup and execution phases. Strategies can be combined by combining these phases separately, so that their individual setup steps still only occur once in the resulting composite strategy.
this is motivated by an observation that multiple calls to a given simplification strategy (in the same assumption context) should always use the same cache. However top-level entry point for simplifiers usually implicitly allocates a fresh cache. Multiple executions of that simplifier would therefore not use the same cache.