From 3750a2ad965b4959f6535aeeb9075dbd1a7c0527 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 Mar 2019 22:44:31 +0100 Subject: selectl generation --- mppa_k1c/ValueAOp.v | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'mppa_k1c/ValueAOp.v') diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index f181c0ea..a3843301 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -52,8 +52,8 @@ Definition select (v0 v1 vselect : aval) : aval := Definition selectl (v0 v1 vselect : aval) : aval := match vselect with - | I iselect => - if Int.eq Int.zero iselect + | L iselect => + if Int64.eq Int64.zero iselect then binop_long (fun x0 x1 => x0) v0 v1 else binop_long (fun x0 x1 => x1) v0 v1 | _ => Vtop @@ -272,12 +272,8 @@ Proof. destruct a1; destruct a0; eauto; constructor. (* selectl *) - inv H2; simpl; try constructor. - + destruct (Int.eq _ _); apply binop_long_sound; trivial. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); + + destruct (Int64.eq _ _); apply binop_long_sound; trivial. + + destruct (Int64.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. -- cgit