From 89a90377bb3289a8378a739adf546e3a275120e9 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Thu, 29 Dec 2022 21:56:39 +0100
Subject: [PATCH] modular_definitions: remove unused definitions
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/modular_definitions.v | 30 ++++++++++--------------------
1 file changed, 10 insertions(+), 20 deletions(-)
diff --git a/src/modular_definitions.v b/src/modular_definitions.v
index bbe116a..8406180 100644
--- a/src/modular_definitions.v
+++ b/src/modular_definitions.v
@@ -3,13 +3,10 @@ Import ListNotations.
Module Type Sig.
Parameter opcode : Set.
- Axiom opcode_beq : opcode -> opcode -> bool.
- Axiom opcode_eq_dec : forall (o o' : opcode), {o = o'} + {o <> o'}.
Parameter stage : Set.
Axiom first_stage : stage.
Axiom stage_beq : stage -> stage -> bool.
- Axiom stage_eq_dec : forall (s s' : stage), {s = s'} + {s <> s'}.
Axiom stage_beq_eq_true : forall s, stage_beq s s = true.
Axiom leb : stage -> stage -> bool.
@@ -41,17 +38,17 @@ Module Pipeline (Def : Sig).
end.
Definition next_id (trace : trace_kind) :=
- match trace with
+ let filtered := List.filter (fun (elt : instr_kind) =>
+ match elt with
+ | (_, (st, _)) => stage_beq st first_stage
+ end) trace in
+ let mapped := List.map (fun (elt : instr_kind) =>
+ match elt with
+ | (opc, _) => idx opc
+ end) filtered in
+ match mapped with
| [] => 0
- | (opc, _) :: r =>
- let id := idx opc in
- List.fold_left (fun cid (elt : instr_kind) =>
- let (opc, st) := elt in
- let (s, _) := st in
- if stage_beq s first_stage then
- Nat.min cid (idx opc)
- else
- cid) r id
+ | id :: r => List.fold_left Nat.min r id
end.
Lemma state_leb_eq_true : forall st, state_leb st st = true.
@@ -62,13 +59,6 @@ Module Pipeline (Def : Sig).
now rewrite stage_beq_eq_true, Nat.leb_le.
Qed.
- Lemma instr_kind_is_comparable : forall (e e' : instr_kind), {e = e'} + {e <> e'}.
- Proof.
- repeat decide equality.
- - apply stage_eq_dec.
- - apply opcode_eq_dec.
- Qed.
-
Definition compare_two (e1 e2 : option instr_kind) :=
match e1, e2 with
| None, _
--
GitLab