Changed Arbiter_trace_t to Implementation_t

coq2/Arbiter.v

@@ -3,6 +3,7 @@ Set Printing Projections.
 From sdram Require Export Trace.
 
 Section Arbiter.
+
   Context {REQESTOR_CFG : Requestor_configuration}.
   Context {ARBITER_CFG  : Arbiter_configuration}.
   Context {BANK_CFG     : Bank_configuration}.
@@ -22,6 +23,8 @@ Section Arbiter.
   {
     Arbiter_Commands : Commands_t;
     Arbiter_Time     : nat;
+
+    (* This is implementation specific *)
     Arbiter_State    : State_t;
 
     Arbiter_Commands_date :
@@ -29,7 +32,7 @@ Section Arbiter.
         c \in Arbiter_Commands -> c.(CDate) <= Arbiter_Time
   }.
 
-  Class Arbiter_trace_t := mkArbiterTrace
+  Class Implementation_t := mkImplementation
   {
     Init : Requests_t -> Arbiter_state_t;
     Next : Requests_t -> Arbiter_state_t -> Arbiter_state_t;
@@ -93,14 +96,14 @@ Section Arbiter.
     by rewrite filter_uniq.
   Qed.
 
-  Fixpoint Default_arbitrate {AF : Arrival_function_t} {AT : Arbiter_trace_t} t : Arbiter_state_t :=
+  Fixpoint Default_arbitrate {AF : Arrival_function_t} {IM : Implementation_t} t : Arbiter_state_t :=
     let R := Arrival_at t in
       match t with
         | 0     => Init R
         | S(t') => Next R (Default_arbitrate t')
       end.
 
-  Lemma Default_arbitrate_time_match {AF: Arrival_function_t} {AT : Arbiter_trace_t} t:
+  Lemma Default_arbitrate_time_match {AF: Arrival_function_t} {IM : Implementation_t} t:
       (Default_arbitrate t).(Arbiter_Time) == t.
     Proof.
       induction t; unfold Default_arbitrate.
@@ -111,13 +114,13 @@ Section Arbiter.
         by rewrite IHt in H.
     Qed.
 
-  Lemma Default_arbitrate_time {AF: Arrival_function_t} {AT : Arbiter_trace_t} t:
+  Lemma Default_arbitrate_time {AF: Arrival_function_t} {IM : Implementation_t} t:
     (Default_arbitrate t).(Arbiter_Time) = t.
   Proof.
     apply /eqP. apply Default_arbitrate_time_match.
   Qed.
 
-  Lemma Default_arbitrate_cmds_sorted {AF: Arrival_function_t} {AT : Arbiter_trace_t} t:
+  Lemma Default_arbitrate_cmds_sorted {AF: Arrival_function_t} {IM : Implementation_t} t:
     seq_sorted Command_lt (Default_arbitrate t).(Arbiter_Commands).
   Proof.
     induction t; simpl.
@@ -137,7 +140,7 @@ Section Arbiter.
           - move : Hd => /eqP Hd. by rewrite Hd.
   Qed.
     
-  Lemma Default_arbitrate_notin_cmd {AF: Arrival_function_t} {AT : Arbiter_trace_t} t (c : Command_t):
+  Lemma Default_arbitrate_notin_cmd {AF: Arrival_function_t} {IM : Implementation_t} t (c : Command_t):
     c.(CDate) > t -> c \notin (Default_arbitrate t).(Arbiter_Commands).
   Proof.
     intros.
@@ -152,7 +155,7 @@ Section Arbiter.
       by apply /negPn.
   Qed.
 
-  Lemma Default_arbitrate_cmds_uniq {AF: Arrival_function_t} {AT : Arbiter_trace_t} t:
+  Lemma Default_arbitrate_cmds_uniq {AF: Arrival_function_t} {IM : Implementation_t} t:
     uniq ((Default_arbitrate t).(Arbiter_Commands)).
   Proof.
     induction t; simpl.
@@ -171,7 +174,7 @@ Section Arbiter.
         - done.
   Qed.
 
-  Lemma Default_arbitrate_cmds_date {AF: Arrival_function_t} {AT : Arbiter_trace_t} t cmd:
+  Lemma Default_arbitrate_cmds_date {AF: Arrival_function_t} {IM : Implementation_t} t cmd:
     cmd \in (Default_arbitrate t).(Arbiter_Commands) -> cmd.(CDate) <= (Default_arbitrate t).(Arbiter_Time).
   Proof.
     rewrite Default_arbitrate_time.

coq2/FIFO.v

@@ -195,8 +195,8 @@ Section FIFO.
     all: move : eqseq_cons H => -> /andP [/eqP H _]; by rewrite <- H.
   Qed.
 
-  Global Instance FIFO_arbiter_trace : Arbiter_trace_t := 
-    mkArbiterTrace Init_state Next_state Init_time Next_time Init_Cmds Next_Cmds Next_CDate.
+  Global Instance FIFO_arbiter_trace : Implementation_t := 
+  mkImplementation Init_state Next_state Init_time Next_time Init_Cmds Next_Cmds Next_CDate.
 
   Ltac isCommand :=
     unfold isPRE, isACT, isCAS, PRE_of_req, ACT_of_req, CAS_of_req, Kind_of_req; 
@@ -1127,6 +1127,11 @@ Section FIFO.
   (* ------------------------------------------------------------------ *)
 
   (* TODO: remove *)
+
+  (* At this point, two things have to be defined *)
+  (* 1 - Arbiter_trace_t : has definitions of Init and Next *)
+  (* 2 - An arrival function : here this is just defined in the context *)
+
   Obligation Tactic := simpl.
   Program Definition FIFO_arbitrate t :=
     mkTrace (Default_arbitrate t).(Arbiter_Commands) (Default_arbitrate t).(Arbiter_Time)

coq2/TDM.v

@@ -340,8 +340,8 @@ Section TDM.
   Qed.
 
   (* Instantiation of Arbiter_trace_t class *)
-  Local Instance TDM_arbiter_trace : Arbiter_trace_t := 
-    mkArbiterTrace Init_state Next_state Init_time Next_time Init_Cmds Next_Cmds Next_CDate.
+  Local Instance TDM_arbiter_trace : Implementation_t := 
+    mkImplementation Init_state Next_state Init_time Next_time Init_Cmds Next_Cmds Next_CDate.
 
   Lemma ACT_neq_ZCycle:
     (OACT_date == OZCycle) = false.