From 32d98fc732fe9f9be911552c7fa7cb8947e55096 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 22 Sep 2016 14:49:26 -0400 Subject: Drop CSE from Fancy Machine By being careful about building the expressions in the first place, we no longer need it, and can rely on dead code elimination. --- src/ModularArithmetic/Montgomery/ZBounded.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v index 2da20ddcf..97bcf87b9 100644 --- a/src/ModularArithmetic/Montgomery/ZBounded.v +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -10,6 +10,7 @@ Require Import Crypto.ModularArithmetic.ZBounded. Require Import Crypto.BaseSystem. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Local Open Scope small_zlike_scope. @@ -22,6 +23,19 @@ Section montgomery. (modulus'_valid : small_valid modulus') (modulus_nonzero : modulus <> 0). + (** pull out a common subexpression *) + Local Ltac cse := + let RHS := match goal with |- _ = ?decode ?RHS /\ _ => RHS end in + let v := fresh in + match RHS with + | context[?e] => not is_var e; set (v := e) at 1 2; test clearbody v + end; + revert v; + match goal with + | [ |- let v := ?val in ?LHS = ?decode ?RHS /\ ?P ] + => change (LHS = decode (dlet v := val in RHS) /\ P) + end. + Definition partial_reduce : forall v : LargeT, { partial_reduce : SmallT | large_valid v @@ -38,6 +52,7 @@ Section montgomery. rewrite <- partial_reduce_alt_eq by omega. cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce]. pull_zlike_decode. + cse. subst pr; split; [ reflexivity | exact _ ]. Defined. @@ -58,6 +73,7 @@ Section montgomery. rewrite <- partial_reduce_alt_eq by omega. cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce]. pull_zlike_decode. + cse. subst pr; split; [ reflexivity | exact _ ]. Defined. -- cgit v1.2.3