split confluence constraints out of syntactic
Initial Q-Rewriting support.

- Missing graph transformation processors
- Missing efficient Q-condition checking
- Missing tests !
- Beefed support for Observable
- Introduced FrameworkXXX constraint synonyms
- Improved TPDB pretty printing
Changes:
* Observable
- Introduced observable variants of several key functions and type classes
- Introduced the necessary new Observable and Observable1 instances

* Constraints
- Usable rules now operates on problems, as Icap.

* Terms
- Efficient matching via a custom Match instance

* NarradarTRS
- NarradarTRS is now a Hask Functor, via the functor-normal-form trick
- Substitution is now a Hask Functor, as above
- Signature is now a Hask Functor, as above
- Fixed the NFData instance for NarradarTRS
- Enhanced the Observable instance for NarradarTRS
- computeInverseUnifiers preserves the problem type when creating the inverse problem. This is needed to have full icap resolution
- The dpTRS function is no longer a constructor but a "normalising function".

* Problems
- Removed the monolithical MkDPProblem InitialGoal instances. No longer needed as we can now normalise the problem after constructing it
- ExpandDPair is now a class, parameterised by problem type

* Processors
- The QRewriting usable rules processor now avoids recomputing the DP unifiers
- The Proof datatypes are now observable and (most) have Ord instances. Used only in an experimental prune function for proof trees
- The UsableRules and Graph processors for QRewriting avoid recalculating the DP unifiers when not needed
- The Narrowing processor for QRewriting allows restricting the position where it is applied
- There is now an Instantiation processor for QRewriting
- There is now a forward instantiation processor for QRewriting
- There is now a rewriting processor for QRewriting

* Others
- Fixed definition of intersections in Utils
Strategies for QRewriting
Term: replaced Match instance by Applicative instance
Removed dependency on reflection and added dependency on applicative-extras (for the Compose functor)
Implemented Thiemann's pair-graph expansion for Q-Rewriting
NOTE: untested
fix RPO for InitialGoal Gen problems
Missing imports, pragmas, observables, instances.
Removed redundant imports and some orphan instances.
Problem - introduced unchecked versions of setP/setR for use during construction (in dpTRS)
QRewriting - The problem type now carries a fast matcher (although it is not being used at the moment).
.gitignore
Trivial Local to Global processor for initial goal problems
restored the LOPSTR09 processor back to life
pragmas, imports, instances, etc.
Fix a bug in the definition of HT
Follow changes in the definition of the Substitution type - now an Observable instance is required.
fix a comment
fix a bug in the Rewriting processor
Drop the SATSymbol class as it was leading to ambiguous types.
Making it explicit helped fix the RPO Processor instances for initial goals, which require a circuit to be used polymorphically
added observations