From 934b137726cf0ef093db0a7bb8112326e29b256f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 24 Oct 2021 19:59:09 +0100 Subject: Add type-class proofs to Predicate.v --- src/hls/RTLBlockInstr.v | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'src/hls/RTLBlockInstr.v') diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 51beedc..e9e85f7 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -100,14 +100,16 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := Definition regset := Regmap.t val. Definition predset := PMap.t bool. -Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := - match p with - | Pvar (b, p') => if b then PMap.get p' pr else negb (PMap.get p' pr) - | Ptrue => true - | Pfalse => false - | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') - | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') - end. +Definition eval_predf (pr: predset) (p: pred_op) := + sat_predicate p (fun x => pr !! (Pos.of_nat x)). + +#[global] +Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf. +Proof. + unfold Proper. simplify. unfold "==>". + intros. + unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0. +Qed. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with -- cgit