modify definitions of priority policy compliance

The current definitions of respects_JLFP_policy_at_preemption_time and respects_FP_policy_at_preemption_time use the predicate hep_job_at. This predicate does not make sense for JLFP and FP policies. To avoid this, these definitions should instead use the definition respects_JLDP_policy_at_preemption_point. Doing this requires coercions from JLFP to JLDP and from FP to JLFP. This patch also introduces these coercions.

I'm surprised we didn't need the coercions before. I guess all prior cases of "JLFP as JLDP reasoning" happened to be type-class resolution, not coercions?

@sbozhko: Sergey, could you please double-check and confirm that this patch makes sense?

added 23 commits

• ee6b5cb3...db563557 - 22 commits from branch RT-PROOFS:master
• 39502caf - modify definitions of priority policy compliance

Compare with previous version

added 1 commit

• 8be64d05 - add coercions to the list of exceptions

Compare with previous version

resolved all threads

merged