Skip to content
Snippets Groups Projects
Commit 89a90377 authored by Alban Gruin's avatar Alban Gruin
Browse files

modular_definitions: remove unused definitions


Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent 773f2fc5
Branches
No related tags found
No related merge requests found
...@@ -3,13 +3,10 @@ Import ListNotations. ...@@ -3,13 +3,10 @@ Import ListNotations.
Module Type Sig. Module Type Sig.
Parameter opcode : Set. Parameter opcode : Set.
Axiom opcode_beq : opcode -> opcode -> bool.
Axiom opcode_eq_dec : forall (o o' : opcode), {o = o'} + {o <> o'}.
Parameter stage : Set. Parameter stage : Set.
Axiom first_stage : stage. Axiom first_stage : stage.
Axiom stage_beq : stage -> stage -> bool. 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 stage_beq_eq_true : forall s, stage_beq s s = true.
Axiom leb : stage -> stage -> bool. Axiom leb : stage -> stage -> bool.
...@@ -41,17 +38,17 @@ Module Pipeline (Def : Sig). ...@@ -41,17 +38,17 @@ Module Pipeline (Def : Sig).
end. end.
Definition next_id (trace : trace_kind) := 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 | [] => 0
| (opc, _) :: r => | id :: r => List.fold_left Nat.min r id
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
end. end.
Lemma state_leb_eq_true : forall st, state_leb st st = true. Lemma state_leb_eq_true : forall st, state_leb st st = true.
...@@ -62,13 +59,6 @@ Module Pipeline (Def : Sig). ...@@ -62,13 +59,6 @@ Module Pipeline (Def : Sig).
now rewrite stage_beq_eq_true, Nat.leb_le. now rewrite stage_beq_eq_true, Nat.leb_le.
Qed. 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) := Definition compare_two (e1 e2 : option instr_kind) :=
match e1, e2 with match e1, e2 with
| None, _ | None, _
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment