From cb95f631364d06620ce24ff01cf44b7d2035a705 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 18 Oct 2017 00:09:13 -0400
Subject: Add basesystem_partial_evaluation_unfolder db

---
 src/Arithmetic/Core.v               | 23 +++++++++++++++++++++++
 src/Arithmetic/Saturated/AddSub.v   | 11 +++++++++++
 src/Arithmetic/Saturated/Core.v     | 10 ++++++++++
 src/Arithmetic/Saturated/Freeze.v   |  6 +++++-
 src/Arithmetic/Saturated/MulSplit.v |  3 +++
 src/Arithmetic/Saturated/Wrappers.v |  4 ++++
 6 files changed, 56 insertions(+), 1 deletion(-)

(limited to 'src/Arithmetic')

diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 8e7f3cb23..f3c435a09 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -995,6 +995,29 @@ End DivMod.
 
 Import B.
 
+Create HintDb basesystem_partial_evaluation_unfolder.
+
+Hint Unfold
+     id
+     Positional.to_associational_cps Positional.to_associational
+     Positional.eval Positional.zeros Positional.add_to_nth_cps
+     Positional.add_to_nth Positional.place_cps Positional.place
+     Positional.from_associational_cps Positional.from_associational
+     Positional.carry_cps Positional.carry
+     Positional.chained_carries_cps Positional.chained_carries
+     Positional.sub_cps Positional.sub Positional.split_cps
+     Positional.scmul_cps Positional.unbalanced_sub_cps
+     Positional.negate_snd_cps Positional.add_cps Positional.opp_cps
+     Associational.eval Associational.multerm Associational.mul_cps
+     Associational.mul Associational.split_cps Associational.split
+     Associational.reduce_cps Associational.reduce
+     Associational.carryterm_cps Associational.carryterm
+     Associational.carry_cps Associational.carry
+     Associational.negate_snd_cps Associational.negate_snd div modulo
+     id_tuple_with_alt id_tuple'_with_alt
+     Z.add_get_carry_full
+  : basesystem_partial_evaluation_unfolder.
+
 Ltac basesystem_partial_evaluation_unfolder t :=
   eval
     cbv
diff --git a/src/Arithmetic/Saturated/AddSub.v b/src/Arithmetic/Saturated/AddSub.v
index c1c701870..e34230904 100644
--- a/src/Arithmetic/Saturated/AddSub.v
+++ b/src/Arithmetic/Saturated/AddSub.v
@@ -238,3 +238,14 @@ End B.
 Hint Opaque B.Positional.sat_sub B.Positional.sat_add B.Positional.chain_op B.Positional.chain_op' : uncps.
 Hint Rewrite @B.Positional.sat_sub_id @B.Positional.sat_add_id @B.Positional.chain_op_id @B.Positional.chain_op' : uncps.
 Hint Rewrite @B.Positional.sat_sub_mod @B.Positional.sat_sub_div @B.Positional.sat_add_mod @B.Positional.sat_add_div using (omega || assumption) : push_basesystem_eval.
+
+Hint Unfold
+     B.Positional.chain_op'_cps
+     B.Positional.chain_op'
+     B.Positional.chain_op_cps
+     B.Positional.chain_op
+     B.Positional.sat_add_cps
+     B.Positional.sat_add
+     B.Positional.sat_sub_cps
+     B.Positional.sat_sub
+     : basesystem_partial_evaluation_unfolder.
diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v
index ce9888b74..e34a37501 100644
--- a/src/Arithmetic/Saturated/Core.v
+++ b/src/Arithmetic/Saturated/Core.v
@@ -432,6 +432,16 @@ Hint Rewrite
      @Columns.eval_nils
   using (assumption || omega): push_basesystem_eval.
 
+Hint Unfold
+     Columns.eval Columns.eval_from
+     Columns.compact_digit_cps Columns.compact_digit
+     Columns.compact_step_cps Columns.compact_step
+     Columns.compact_cps Columns.compact
+     Columns.cons_to_nth_cps Columns.cons_to_nth
+     Columns.nils
+     Columns.from_associational_cps Columns.from_associational
+  : basesystem_partial_evaluation_unfolder.
+
 Ltac basesystem_partial_evaluation_unfolder t :=
   let t :=
       (eval
diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v
index 735663636..65b8ee55d 100644
--- a/src/Arithmetic/Saturated/Freeze.v
+++ b/src/Arithmetic/Saturated/Freeze.v
@@ -119,4 +119,8 @@ Section Freeze.
       rewrite Z.add_0_r, Z.mod_mod by assumption.
       reflexivity. }
   Qed.
-End Freeze.
\ No newline at end of file
+End Freeze.
+
+Hint Unfold
+     freeze freeze_cps
+  : basesystem_partial_evaluation_unfolder.
diff --git a/src/Arithmetic/Saturated/MulSplit.v b/src/Arithmetic/Saturated/MulSplit.v
index 45f37ef56..98d8d0e0c 100644
--- a/src/Arithmetic/Saturated/MulSplit.v
+++ b/src/Arithmetic/Saturated/MulSplit.v
@@ -71,3 +71,6 @@ Hint Opaque B.Associational.sat_mul B.Associational.sat_multerm : uncps.
 Hint Rewrite @B.Associational.sat_mul_id @B.Associational.sat_multerm_id : uncps.
 Hint Rewrite @B.Associational.eval_sat_mul @B.Associational.eval_map_sat_multerm using (omega || assumption) : push_basesystem_eval.
 
+Hint Unfold
+     B.Associational.sat_multerm_cps B.Associational.sat_multerm B.Associational.sat_mul_cps B.Associational.sat_mul
+  : basesystem_partial_evaluation_unfolder.
diff --git a/src/Arithmetic/Saturated/Wrappers.v b/src/Arithmetic/Saturated/Wrappers.v
index e9b73dd10..6fe466967 100644
--- a/src/Arithmetic/Saturated/Wrappers.v
+++ b/src/Arithmetic/Saturated/Wrappers.v
@@ -52,6 +52,10 @@ Hint Unfold
      Columns.unbalanced_sub_cps
      Columns.mul_cps.
 
+Hint Unfold
+     Columns.add_cps Columns.unbalanced_sub_cps Columns.mul_cps Columns.conditional_add_cps
+  : basesystem_partial_evaluation_unfolder.
+
 Ltac basesystem_partial_evaluation_unfolder t :=
   let t := (eval cbv delta [Columns.add_cps Columns.unbalanced_sub_cps Columns.mul_cps Columns.conditional_add_cps] in t) in
   let t := Saturated.Core.basesystem_partial_evaluation_unfolder t in
-- 
cgit v1.2.3