From 0ce75d20f86a287a1b179bd429b30d758f1c4716 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 13 Oct 2016 14:02:17 -0400 Subject: Revert "Eta-expand pairs in Eta.v" This reverts commit 778c1906711f68bed5760710712bb16eeb9c2365. It's not particularly useful, I think, and might be counterproductive; most of the unfolded pair projections in x86 are applied to variables, not instructions, and some instructions don't have pair projections directly applied to them. --- src/BoundedArithmetic/Eta.v | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) (limited to 'src/BoundedArithmetic/Eta.v') diff --git a/src/BoundedArithmetic/Eta.v b/src/BoundedArithmetic/Eta.v index bc9b0e940..b48b8cff1 100644 --- a/src/BoundedArithmetic/Eta.v +++ b/src/BoundedArithmetic/Eta.v @@ -2,33 +2,30 @@ (** This is useful for allowing us to refold the projections. *) Require Import Crypto.BoundedArithmetic.Interface. -Local Notation eta x := (fst x, snd x). -Local Notation eta3 x := (fst x, eta (snd x)). - Definition eta_decode {n W} (x : decoder n W) : decoder n W := {| decode := decode |}. Section InstructionGallery. Context {n W} {Wdecoder : decoder n W}. Definition eta_ldi (x : load_immediate W) := {| ldi := ldi |}. Definition eta_shrd (x : shift_right_doubleword_immediate W) := {| shrd := shrd |}. - Definition eta_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf a b c := eta (shrdf a b c) |}. + Definition eta_shrdf (x : shift_right_doubleword_immediate_with_CF W) := {| shrdf := shrdf |}. Definition eta_shl (x : shift_left_immediate W) := {| shl := shl |}. - Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf a b := eta (shlf a b) |}. + Definition eta_shlf (x : shift_left_immediate_with_CF W) := {| shlf := shlf |}. Definition eta_shr (x : shift_right_immediate W) := {| shr := shr |}. - Definition eta_shrf (x : shift_right_immediate_with_CF W) := {| shrf a b := eta (shrf a b) |}. - Definition eta_sprl (x : spread_left_immediate W) := {| sprl a b := eta (sprl a b) |}. + Definition eta_shrf (x : shift_right_immediate_with_CF W) := {| shrf := shrf |}. + Definition eta_sprl (x : spread_left_immediate W) := {| sprl := sprl |}. Definition eta_mkl (x : mask_keep_low W) := {| mkl := mkl |}. Definition eta_and (x : bitwise_and W) := {| and := and |}. - Definition eta_andf (x : bitwise_and_with_CF W) := {| andf a b := eta (andf a b) |}. + Definition eta_andf (x : bitwise_and_with_CF W) := {| andf := andf |}. Definition eta_or (x : bitwise_or W) := {| or := or |}. - Definition eta_orf (x : bitwise_or_with_CF W) := {| orf a b := eta (orf a b) |}. - Definition eta_adc (x : add_with_carry W) := {| adc a b c := eta (adc a b c) |}. - Definition eta_subc (x : sub_with_carry W) := {| subc a b c := eta (subc a b c) |}. + Definition eta_orf (x : bitwise_or_with_CF W) := {| orf := orf |}. + Definition eta_adc (x : add_with_carry W) := {| adc := adc |}. + Definition eta_subc (x : sub_with_carry W) := {| subc := subc |}. Definition eta_mul (x : multiply W) := {| mul := mul |}. Definition eta_mulhwll (x : multiply_low_low W) := {| mulhwll := mulhwll |}. Definition eta_mulhwhl (x : multiply_high_low W) := {| mulhwhl := mulhwhl |}. Definition eta_mulhwhh (x : multiply_high_high W) := {| mulhwhh := mulhwhh |}. - Definition eta_muldw (x : multiply_double W) := {| muldw a b := eta (muldw a b) |}. - Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf a b := eta3 (muldwf a b) |}. + Definition eta_muldw (x : multiply_double W) := {| muldw := muldw |}. + Definition eta_muldwf (x : multiply_double_with_CF W) := {| muldwf := muldwf |}. Definition eta_selc (x : select_conditional W) := {| selc := selc |}. Definition eta_addm (x : add_modulo W) := {| addm := addm |}. End InstructionGallery. -- cgit v1.2.3