Library rt.implementation.jitter.job

Require Import rt.util.all.
Require Import rt.implementation.jitter.task.

Module ConcreteJob.

  Import ConcreteTask.

  Section Defs.

    (* Definition of a concrete task. *)
    Record concrete_job :=
    {
      job_id: nat;
      job_cost: nat;
      job_deadline: nat;
      job_jitter: nat;
      job_task: concrete_task_eqType
    }.

    (* To make it compatible with ssreflect, we define a decidable
       equality for concrete jobs. *)
    Definition job_eqdef (j1 j2: concrete_job) :=
      (job_id j1 = job_id j2) ∧
      (job_cost j1 = job_cost j2) ∧
      (job_deadline j1 = job_deadline j2) ∧
      (job_jitter j1 = job_jitter j2) ∧
      (job_task j1 = job_task j2).

    (* Next, we prove that job_eqdef is indeed an equality, ... *)
    Lemma eqn_job : Equality.axiom job_eqdef.

    (* ..., which allows instantiating the canonical structure. *)
    Canonical concrete_job_eqMixin := EqMixin eqn_job.
    Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin.

   End Defs.

End ConcreteJob.