Previously, unification utilities and simplification tactics were added in an ad hoc manner. We are in a better position to understand the variations we need and to unify them. So, doing that.
Also, the previous version was too spaghetti to work on because of this series of ad hoc extensions... (I did write it before, so... oops)
The end goal is to also combine some of these to produce a parallel rewrite system with substitution inference, so this PR completely supersedes #148.
Worklist:
:heavy_check_mark: matching
:heavy_check_mark: context discovery with substitution inference
:heavy_check_mark: substitution with automatic instantiation inference
Moved old Substitution to Substitution2, slowly replacing and deprecating its methods. (Next PR!)
Same with old UnificationUtils
Previously, unification utilities and simplification tactics were added in an ad hoc manner. We are in a better position to understand the variations we need and to unify them. So, doing that.
Also, the previous version was too spaghetti to work on because of this series of ad hoc extensions... (I did write it before, so... oops)
The end goal is to also combine some of these to produce a parallel rewrite system with substitution inference, so this PR completely supersedes #148.
Worklist:
:heavy_check_mark: matching :heavy_check_mark: context discovery with substitution inference :heavy_check_mark: substitution with automatic instantiation inference
Moved old Substitution to
Substitution2, slowly replacing and deprecating its methods. (Next PR!)Same with old UnificationUtils