From 28508c6fa3ee811d8e51f365cd6cbdabe96352cd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 22 Oct 2017 16:09:02 -0400 Subject: Add another unfolding database --- src/Arithmetic/Core.v | 4 ++-- src/Arithmetic/CoreUnfolder.v | 6 ++++++ src/Arithmetic/Saturated/CoreUnfolder.v | 2 ++ src/Arithmetic/Saturated/WrappersUnfolder.v | 2 ++ 4 files changed, 12 insertions(+), 2 deletions(-) (limited to 'src/Arithmetic') diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 5104a21aa..4df36a0aa 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1133,7 +1133,7 @@ Ltac pattern_strip_full t := let t := (eval pattern (@Let_In Z (fun _ => Z)), @Z.add_get_carry_cps, @Z.mul_split_at_bitwidth_cps, - Z.eq_dec_cps, Z.eqb_cps, + (@Z.eq_dec_cps), (@Z.eqb_cps), @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor, (@id_with_alt Z), @Z.add_get_carry, @Z.zselect, @Z.mul_split_at_bitwidth, @@ -1165,7 +1165,7 @@ Ltac apply_patterned_full t1 := (@Let_In) (@id_with_alt) (@Let_In Z (fun _ => Z)) (@Z.add_get_carry_cps) (@Z.mul_split_at_bitwidth_cps) - Z.eq_dec_cps Z.eqb_cps + (@Z.eq_dec_cps) (@Z.eqb_cps) (@runtime_mul) (@runtime_add) (@runtime_opp) (@runtime_shr) (@runtime_and) (@runtime_lor) (@id_with_alt Z) (@Z.add_get_carry) (@Z.zselect) (@Z.mul_split_at_bitwidth) diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v index 05aa2f498..a7a7286d1 100644 --- a/src/Arithmetic/CoreUnfolder.v +++ b/src/Arithmetic/CoreUnfolder.v @@ -1,9 +1,15 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.CPS. Require Import Crypto.Util.IdfunWithAlt. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Util.Tactics.VM. +Create HintDb arithmetic_cps_unfolder. + +Hint Unfold Core.div Core.modulo : arithmetic_cps_unfolder. + Ltac make_parameterized_sig t := refine (_ : { v : _ | v = t }); eexists; cbv delta [t diff --git a/src/Arithmetic/Saturated/CoreUnfolder.v b/src/Arithmetic/Saturated/CoreUnfolder.v index 2b2b2ed09..9a0e0c06a 100644 --- a/src/Arithmetic/Saturated/CoreUnfolder.v +++ b/src/Arithmetic/Saturated/CoreUnfolder.v @@ -1,6 +1,8 @@ Require Import Crypto.Arithmetic.CoreUnfolder. Require Import Crypto.Arithmetic.Saturated.Core. +Hint Unfold Core.Columns.compact_digit_cps Core.Columns.compact_step_cps Core.Columns.compact_cps : arithmetic_cps_unfolder. + Module Columns. (** << diff --git a/src/Arithmetic/Saturated/WrappersUnfolder.v b/src/Arithmetic/Saturated/WrappersUnfolder.v index d28719af8..b8fe6afc6 100644 --- a/src/Arithmetic/Saturated/WrappersUnfolder.v +++ b/src/Arithmetic/Saturated/WrappersUnfolder.v @@ -3,6 +3,8 @@ Require Import Crypto.Arithmetic.Saturated.CoreUnfolder. Require Import Crypto.Arithmetic.Saturated.MulSplitUnfolder. Require Import Crypto.Arithmetic.Saturated.Wrappers. +Hint Unfold Wrappers.Columns.add_cps Wrappers.Columns.unbalanced_sub_cps Wrappers.Columns.mul_cps : arithmetic_cps_unfolder. + Module Columns. (** << -- cgit v1.2.3