Add more versions of basesystem_partial_evaluation_unfolder

5 files changed, 82 insertions, 0 deletions

diff --git a/src/Arithmetic/Saturated/AddSub.v b/src/Arithmetic/Saturated/AddSub.v
index e886c36de..d3ab6897f 100644
--- a/src/Arithmetic/Saturated/AddSub.v
+++ b/src/Arithmetic/Saturated/AddSub.v
@@ -265,3 +265,21 @@ Hint Unfold
      B.Positional.sat_sub_cps
      B.Positional.sat_sub
      : basesystem_partial_evaluation_unfolder.
+
+Ltac basesystem_partial_evaluation_unfolder t :=
+  let t := (eval cbv delta [
+                   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
+                 ] in t) in
+  let t := Arithmetic.Saturated.Core.basesystem_partial_evaluation_unfolder t in
+  let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in
+  t.
+
+Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::=
+  basesystem_partial_evaluation_unfolder t.
diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v
index 658eb867d..563d9afc5 100644
--- a/src/Arithmetic/Saturated/Freeze.v
+++ b/src/Arithmetic/Saturated/Freeze.v
@@ -127,3 +127,13 @@ End Freeze.
 Hint Unfold
      freeze freeze_cps
   : basesystem_partial_evaluation_unfolder.
+
+Ltac basesystem_partial_evaluation_unfolder t :=
+  let t := (eval cbv delta [freeze freeze_cps] in t) in
+  let t := Saturated.Wrappers.basesystem_partial_evaluation_unfolder t in
+  let t := Saturated.Core.basesystem_partial_evaluation_unfolder t in
+  let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in
+  t.
+
+Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::=
+  basesystem_partial_evaluation_unfolder t.
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index 49e45663d..01672c61c 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -616,3 +616,48 @@ Section API.
   End Proofs.
 End API.
 Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps.
+
+Hint Unfold
+     nonzero_cps
+     nonzero
+     scmul_cps
+     scmul
+     add_cps
+     add
+     add_S1_cps
+     add_S1
+     add_S2_cps
+     add_S2
+     sub_then_maybe_add_cps
+     sub_then_maybe_add
+     conditional_sub_cps
+     conditional_sub
+     eval
+  : basesystem_partial_evaluation_unfolder.
+
+Ltac basesystem_partial_evaluation_unfolder t :=
+  let t := (eval cbv delta [
+                   nonzero_cps
+                     nonzero
+                     scmul_cps
+                     scmul
+                     add_cps
+                     add
+                     add_S1_cps
+                     add_S1
+                     add_S2_cps
+                     add_S2
+                     sub_then_maybe_add_cps
+                     sub_then_maybe_add
+                     conditional_sub_cps
+                     conditional_sub
+                     eval
+                 ] in t) in
+  let t := Saturated.AddSub.basesystem_partial_evaluation_unfolder t in
+  let t := Saturated.Wrappers.basesystem_partial_evaluation_unfolder t in
+  let t := Saturated.Core.basesystem_partial_evaluation_unfolder t in
+  let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in
+  t.
+
+Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::=
+  basesystem_partial_evaluation_unfolder t.
diff --git a/src/Arithmetic/Saturated/MulSplit.v b/src/Arithmetic/Saturated/MulSplit.v
index 4947f422a..cd86a8b48 100644
--- a/src/Arithmetic/Saturated/MulSplit.v
+++ b/src/Arithmetic/Saturated/MulSplit.v
@@ -90,3 +90,11 @@ Hint Rewrite @B.Associational.eval_sat_mul @B.Associational.eval_map_sat_multerm
 Hint Unfold
      B.Associational.sat_multerm_cps B.Associational.sat_multerm B.Associational.sat_mul_cps B.Associational.sat_mul
   : basesystem_partial_evaluation_unfolder.
+
+Ltac basesystem_partial_evaluation_unfolder t :=
+  let t := (eval cbv delta [B.Associational.sat_multerm_cps B.Associational.sat_multerm B.Associational.sat_mul_cps B.Associational.sat_mul] in t) in
+  let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in
+  t.
+
+Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::=
+  basesystem_partial_evaluation_unfolder t.
diff --git a/src/Arithmetic/Saturated/Wrappers.v b/src/Arithmetic/Saturated/Wrappers.v
index e750cfd36..cbd4c42b5 100644
--- a/src/Arithmetic/Saturated/Wrappers.v
+++ b/src/Arithmetic/Saturated/Wrappers.v
@@ -59,6 +59,7 @@ Hint Unfold
 
 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.MulSplit.basesystem_partial_evaluation_unfolder t in
   let t := Saturated.Core.basesystem_partial_evaluation_unfolder t in
   let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in
   t.