WIP PR which rewrites the Chamelean backend using:

• the unification algorithm described in Section 4 of Generating Good Generators for Inductive Relations (GGG)
• the generator schedules in Testing Theorems, Fully Automatically (TT)

Overview:

• UnificationMonad.lean: The unification monad from Fig. 2 of GGG (called UnifyM in our implementation)
  • UnifyM combines the State, Option and MetaM monads (the latter is Lean's metaprogramming monad, needed for producing terms + error reporting)
• DeriveSubGenerator.lean: The algorithm in Fig. 4 of GGG for deriving one case of a generator
• ModeAnalysis.lean: Handles constraint-processing as described in section 3 of Computing Correctly for Inductive Relations (contains types corresponding to CC's notion of compatibility)
• Schedules.lean: Definitions of generator schedules from TT
• ScheduleUtils.lean: Functions for manipulating generator schedules
• GGGTests.lean: Tests corresponding to the example generators in GGG