Add more unfolds to basesystem_partial_evaluation_unfolder

5 files changed, 79 insertions, 0 deletions

diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v
index cb943e80a..05aa2f498 100644
--- a/src/Arithmetic/CoreUnfolder.v
+++ b/src/Arithmetic/CoreUnfolder.v
@@ -51,6 +51,7 @@ for i in eval multerm mul_cps mul split_cps split reduce_cps reduce negate_snd_c
     echo "    Definition ${i}_sig := parameterize_sig (@Core.B.Associational.${i}).";
     echo "    Definition ${i} := parameterize_from_sig ${i}_sig.";
     echo "    Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "    Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
     echo "    Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 echo "  End Associational."
@@ -59,6 +60,7 @@ for i in to_associational_cps to_associational eval zeros add_to_nth_cps add_to_
   echo "    Definition ${i}_sig := parameterize_sig (@Core.B.Positional.${i}).";
   echo "    Definition ${i} := parameterize_from_sig ${i}_sig.";
   echo "    Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+  echo "    Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
   echo "    Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 echo "  End Positional."
@@ -68,77 +70,92 @@ for i in modulo_cps div_cps modulo div; do
   echo "Definition ${i}_sig := parameterize_sig (@Core.${i}).";
   echo "Definition ${i} := parameterize_from_sig ${i}_sig.";
   echo "Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+  echo "Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
   echo "Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 >> *)
     Definition eval_sig := parameterize_sig (@Core.B.Associational.eval).
     Definition eval := parameterize_from_sig eval_sig.
     Definition eval_eq := parameterize_eq eval eval_sig.
+    Hint Unfold eval : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- eval_eq : pattern_runtime.
 
     Definition multerm_sig := parameterize_sig (@Core.B.Associational.multerm).
     Definition multerm := parameterize_from_sig multerm_sig.
     Definition multerm_eq := parameterize_eq multerm multerm_sig.
+    Hint Unfold multerm : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- multerm_eq : pattern_runtime.
 
     Definition mul_cps_sig := parameterize_sig (@Core.B.Associational.mul_cps).
     Definition mul_cps := parameterize_from_sig mul_cps_sig.
     Definition mul_cps_eq := parameterize_eq mul_cps mul_cps_sig.
+    Hint Unfold mul_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- mul_cps_eq : pattern_runtime.
 
     Definition mul_sig := parameterize_sig (@Core.B.Associational.mul).
     Definition mul := parameterize_from_sig mul_sig.
     Definition mul_eq := parameterize_eq mul mul_sig.
+    Hint Unfold mul : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- mul_eq : pattern_runtime.
 
     Definition split_cps_sig := parameterize_sig (@Core.B.Associational.split_cps).
     Definition split_cps := parameterize_from_sig split_cps_sig.
     Definition split_cps_eq := parameterize_eq split_cps split_cps_sig.
+    Hint Unfold split_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- split_cps_eq : pattern_runtime.
 
     Definition split_sig := parameterize_sig (@Core.B.Associational.split).
     Definition split := parameterize_from_sig split_sig.
     Definition split_eq := parameterize_eq split split_sig.
+    Hint Unfold split : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- split_eq : pattern_runtime.
 
     Definition reduce_cps_sig := parameterize_sig (@Core.B.Associational.reduce_cps).
     Definition reduce_cps := parameterize_from_sig reduce_cps_sig.
     Definition reduce_cps_eq := parameterize_eq reduce_cps reduce_cps_sig.
+    Hint Unfold reduce_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- reduce_cps_eq : pattern_runtime.
 
     Definition reduce_sig := parameterize_sig (@Core.B.Associational.reduce).
     Definition reduce := parameterize_from_sig reduce_sig.
     Definition reduce_eq := parameterize_eq reduce reduce_sig.
+    Hint Unfold reduce : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- reduce_eq : pattern_runtime.
 
     Definition negate_snd_cps_sig := parameterize_sig (@Core.B.Associational.negate_snd_cps).
     Definition negate_snd_cps := parameterize_from_sig negate_snd_cps_sig.
     Definition negate_snd_cps_eq := parameterize_eq negate_snd_cps negate_snd_cps_sig.
+    Hint Unfold negate_snd_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- negate_snd_cps_eq : pattern_runtime.
 
     Definition negate_snd_sig := parameterize_sig (@Core.B.Associational.negate_snd).
     Definition negate_snd := parameterize_from_sig negate_snd_sig.
     Definition negate_snd_eq := parameterize_eq negate_snd negate_snd_sig.
+    Hint Unfold negate_snd : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- negate_snd_eq : pattern_runtime.
 
     Definition carryterm_cps_sig := parameterize_sig (@Core.B.Associational.carryterm_cps).
     Definition carryterm_cps := parameterize_from_sig carryterm_cps_sig.
     Definition carryterm_cps_eq := parameterize_eq carryterm_cps carryterm_cps_sig.
+    Hint Unfold carryterm_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carryterm_cps_eq : pattern_runtime.
 
     Definition carryterm_sig := parameterize_sig (@Core.B.Associational.carryterm).
     Definition carryterm := parameterize_from_sig carryterm_sig.
     Definition carryterm_eq := parameterize_eq carryterm carryterm_sig.
+    Hint Unfold carryterm : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carryterm_eq : pattern_runtime.
 
     Definition carry_cps_sig := parameterize_sig (@Core.B.Associational.carry_cps).
     Definition carry_cps := parameterize_from_sig carry_cps_sig.
     Definition carry_cps_eq := parameterize_eq carry_cps carry_cps_sig.
+    Hint Unfold carry_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carry_cps_eq : pattern_runtime.
 
     Definition carry_sig := parameterize_sig (@Core.B.Associational.carry).
     Definition carry := parameterize_from_sig carry_sig.
     Definition carry_eq := parameterize_eq carry carry_sig.
+    Hint Unfold carry : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carry_eq : pattern_runtime.
 
   End Associational.
@@ -146,156 +163,187 @@ done
     Definition to_associational_cps_sig := parameterize_sig (@Core.B.Positional.to_associational_cps).
     Definition to_associational_cps := parameterize_from_sig to_associational_cps_sig.
     Definition to_associational_cps_eq := parameterize_eq to_associational_cps to_associational_cps_sig.
+    Hint Unfold to_associational_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- to_associational_cps_eq : pattern_runtime.
 
     Definition to_associational_sig := parameterize_sig (@Core.B.Positional.to_associational).
     Definition to_associational := parameterize_from_sig to_associational_sig.
     Definition to_associational_eq := parameterize_eq to_associational to_associational_sig.
+    Hint Unfold to_associational : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- to_associational_eq : pattern_runtime.
 
     Definition eval_sig := parameterize_sig (@Core.B.Positional.eval).
     Definition eval := parameterize_from_sig eval_sig.
     Definition eval_eq := parameterize_eq eval eval_sig.
+    Hint Unfold eval : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- eval_eq : pattern_runtime.
 
     Definition zeros_sig := parameterize_sig (@Core.B.Positional.zeros).
     Definition zeros := parameterize_from_sig zeros_sig.
     Definition zeros_eq := parameterize_eq zeros zeros_sig.
+    Hint Unfold zeros : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- zeros_eq : pattern_runtime.
 
     Definition add_to_nth_cps_sig := parameterize_sig (@Core.B.Positional.add_to_nth_cps).
     Definition add_to_nth_cps := parameterize_from_sig add_to_nth_cps_sig.
     Definition add_to_nth_cps_eq := parameterize_eq add_to_nth_cps add_to_nth_cps_sig.
+    Hint Unfold add_to_nth_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- add_to_nth_cps_eq : pattern_runtime.
 
     Definition add_to_nth_sig := parameterize_sig (@Core.B.Positional.add_to_nth).
     Definition add_to_nth := parameterize_from_sig add_to_nth_sig.
     Definition add_to_nth_eq := parameterize_eq add_to_nth add_to_nth_sig.
+    Hint Unfold add_to_nth : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- add_to_nth_eq : pattern_runtime.
 
     Definition place_cps_sig := parameterize_sig (@Core.B.Positional.place_cps).
     Definition place_cps := parameterize_from_sig place_cps_sig.
     Definition place_cps_eq := parameterize_eq place_cps place_cps_sig.
+    Hint Unfold place_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- place_cps_eq : pattern_runtime.
 
     Definition place_sig := parameterize_sig (@Core.B.Positional.place).
     Definition place := parameterize_from_sig place_sig.
     Definition place_eq := parameterize_eq place place_sig.
+    Hint Unfold place : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- place_eq : pattern_runtime.
 
     Definition from_associational_cps_sig := parameterize_sig (@Core.B.Positional.from_associational_cps).
     Definition from_associational_cps := parameterize_from_sig from_associational_cps_sig.
     Definition from_associational_cps_eq := parameterize_eq from_associational_cps from_associational_cps_sig.
+    Hint Unfold from_associational_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- from_associational_cps_eq : pattern_runtime.
 
     Definition from_associational_sig := parameterize_sig (@Core.B.Positional.from_associational).
     Definition from_associational := parameterize_from_sig from_associational_sig.
     Definition from_associational_eq := parameterize_eq from_associational from_associational_sig.
+    Hint Unfold from_associational : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- from_associational_eq : pattern_runtime.
 
     Definition carry_cps_sig := parameterize_sig (@Core.B.Positional.carry_cps).
     Definition carry_cps := parameterize_from_sig carry_cps_sig.
     Definition carry_cps_eq := parameterize_eq carry_cps carry_cps_sig.
+    Hint Unfold carry_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carry_cps_eq : pattern_runtime.
 
     Definition carry_sig := parameterize_sig (@Core.B.Positional.carry).
     Definition carry := parameterize_from_sig carry_sig.
     Definition carry_eq := parameterize_eq carry carry_sig.
+    Hint Unfold carry : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carry_eq : pattern_runtime.
 
     Definition chained_carries_cps_sig := parameterize_sig (@Core.B.Positional.chained_carries_cps).
     Definition chained_carries_cps := parameterize_from_sig chained_carries_cps_sig.
     Definition chained_carries_cps_eq := parameterize_eq chained_carries_cps chained_carries_cps_sig.
+    Hint Unfold chained_carries_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- chained_carries_cps_eq : pattern_runtime.
 
     Definition chained_carries_sig := parameterize_sig (@Core.B.Positional.chained_carries).
     Definition chained_carries := parameterize_from_sig chained_carries_sig.
     Definition chained_carries_eq := parameterize_eq chained_carries chained_carries_sig.
+    Hint Unfold chained_carries : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- chained_carries_eq : pattern_runtime.
 
     Definition encode_sig := parameterize_sig (@Core.B.Positional.encode).
     Definition encode := parameterize_from_sig encode_sig.
     Definition encode_eq := parameterize_eq encode encode_sig.
+    Hint Unfold encode : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- encode_eq : pattern_runtime.
 
     Definition add_cps_sig := parameterize_sig (@Core.B.Positional.add_cps).
     Definition add_cps := parameterize_from_sig add_cps_sig.
     Definition add_cps_eq := parameterize_eq add_cps add_cps_sig.
+    Hint Unfold add_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- add_cps_eq : pattern_runtime.
 
     Definition mul_cps_sig := parameterize_sig (@Core.B.Positional.mul_cps).
     Definition mul_cps := parameterize_from_sig mul_cps_sig.
     Definition mul_cps_eq := parameterize_eq mul_cps mul_cps_sig.
+    Hint Unfold mul_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- mul_cps_eq : pattern_runtime.
 
     Definition reduce_cps_sig := parameterize_sig (@Core.B.Positional.reduce_cps).
     Definition reduce_cps := parameterize_from_sig reduce_cps_sig.
     Definition reduce_cps_eq := parameterize_eq reduce_cps reduce_cps_sig.
+    Hint Unfold reduce_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- reduce_cps_eq : pattern_runtime.
 
     Definition carry_reduce_cps_sig := parameterize_sig (@Core.B.Positional.carry_reduce_cps).
     Definition carry_reduce_cps := parameterize_from_sig carry_reduce_cps_sig.
     Definition carry_reduce_cps_eq := parameterize_eq carry_reduce_cps carry_reduce_cps_sig.
+    Hint Unfold carry_reduce_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- carry_reduce_cps_eq : pattern_runtime.
 
     Definition negate_snd_cps_sig := parameterize_sig (@Core.B.Positional.negate_snd_cps).
     Definition negate_snd_cps := parameterize_from_sig negate_snd_cps_sig.
     Definition negate_snd_cps_eq := parameterize_eq negate_snd_cps negate_snd_cps_sig.
+    Hint Unfold negate_snd_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- negate_snd_cps_eq : pattern_runtime.
 
     Definition split_cps_sig := parameterize_sig (@Core.B.Positional.split_cps).
     Definition split_cps := parameterize_from_sig split_cps_sig.
     Definition split_cps_eq := parameterize_eq split_cps split_cps_sig.
+    Hint Unfold split_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- split_cps_eq : pattern_runtime.
 
     Definition scmul_cps_sig := parameterize_sig (@Core.B.Positional.scmul_cps).
     Definition scmul_cps := parameterize_from_sig scmul_cps_sig.
     Definition scmul_cps_eq := parameterize_eq scmul_cps scmul_cps_sig.
+    Hint Unfold scmul_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- scmul_cps_eq : pattern_runtime.
 
     Definition unbalanced_sub_cps_sig := parameterize_sig (@Core.B.Positional.unbalanced_sub_cps).
     Definition unbalanced_sub_cps := parameterize_from_sig unbalanced_sub_cps_sig.
     Definition unbalanced_sub_cps_eq := parameterize_eq unbalanced_sub_cps unbalanced_sub_cps_sig.
+    Hint Unfold unbalanced_sub_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- unbalanced_sub_cps_eq : pattern_runtime.
 
     Definition sub_cps_sig := parameterize_sig (@Core.B.Positional.sub_cps).
     Definition sub_cps := parameterize_from_sig sub_cps_sig.
     Definition sub_cps_eq := parameterize_eq sub_cps sub_cps_sig.
+    Hint Unfold sub_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- sub_cps_eq : pattern_runtime.
 
     Definition sub_sig := parameterize_sig (@Core.B.Positional.sub).
     Definition sub := parameterize_from_sig sub_sig.
     Definition sub_eq := parameterize_eq sub sub_sig.
+    Hint Unfold sub : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- sub_eq : pattern_runtime.
 
     Definition opp_cps_sig := parameterize_sig (@Core.B.Positional.opp_cps).
     Definition opp_cps := parameterize_from_sig opp_cps_sig.
     Definition opp_cps_eq := parameterize_eq opp_cps opp_cps_sig.
+    Hint Unfold opp_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- opp_cps_eq : pattern_runtime.
 
     Definition Fencode_sig := parameterize_sig (@Core.B.Positional.Fencode).
     Definition Fencode := parameterize_from_sig Fencode_sig.
     Definition Fencode_eq := parameterize_eq Fencode Fencode_sig.
+    Hint Unfold Fencode : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- Fencode_eq : pattern_runtime.
 
     Definition Fdecode_sig := parameterize_sig (@Core.B.Positional.Fdecode).
     Definition Fdecode := parameterize_from_sig Fdecode_sig.
     Definition Fdecode_eq := parameterize_eq Fdecode Fdecode_sig.
+    Hint Unfold Fdecode : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- Fdecode_eq : pattern_runtime.
 
     Definition eval_from_sig := parameterize_sig (@Core.B.Positional.eval_from).
     Definition eval_from := parameterize_from_sig eval_from_sig.
     Definition eval_from_eq := parameterize_eq eval_from eval_from_sig.
+    Hint Unfold eval_from : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- eval_from_eq : pattern_runtime.
 
     Definition select_cps_sig := parameterize_sig (@Core.B.Positional.select_cps).
     Definition select_cps := parameterize_from_sig select_cps_sig.
     Definition select_cps_eq := parameterize_eq select_cps select_cps_sig.
+    Hint Unfold select_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- select_cps_eq : pattern_runtime.
 
     Definition select_sig := parameterize_sig (@Core.B.Positional.select).
     Definition select := parameterize_from_sig select_sig.
     Definition select_eq := parameterize_eq select select_sig.
+    Hint Unfold select : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- select_eq : pattern_runtime.
 
   End Positional.
@@ -304,19 +352,23 @@ End B.
 Definition modulo_cps_sig := parameterize_sig (@Core.modulo_cps).
 Definition modulo_cps := parameterize_from_sig modulo_cps_sig.
 Definition modulo_cps_eq := parameterize_eq modulo_cps modulo_cps_sig.
+Hint Unfold modulo_cps : basesystem_partial_evaluation_unfolder.
 Hint Rewrite <- modulo_cps_eq : pattern_runtime.
 
 Definition div_cps_sig := parameterize_sig (@Core.div_cps).
 Definition div_cps := parameterize_from_sig div_cps_sig.
 Definition div_cps_eq := parameterize_eq div_cps div_cps_sig.
+Hint Unfold div_cps : basesystem_partial_evaluation_unfolder.
 Hint Rewrite <- div_cps_eq : pattern_runtime.
 
 Definition modulo_sig := parameterize_sig (@Core.modulo).
 Definition modulo := parameterize_from_sig modulo_sig.
 Definition modulo_eq := parameterize_eq modulo modulo_sig.
+Hint Unfold modulo : basesystem_partial_evaluation_unfolder.
 Hint Rewrite <- modulo_eq : pattern_runtime.
 
 Definition div_sig := parameterize_sig (@Core.div).
 Definition div := parameterize_from_sig div_sig.
 Definition div_eq := parameterize_eq div div_sig.
+Hint Unfold div : basesystem_partial_evaluation_unfolder.
 Hint Rewrite <- div_eq : pattern_runtime.
diff --git a/src/Arithmetic/Saturated/CoreUnfolder.v b/src/Arithmetic/Saturated/CoreUnfolder.v
index 243f8ea2b..2b2b2ed09 100644
--- a/src/Arithmetic/Saturated/CoreUnfolder.v
+++ b/src/Arithmetic/Saturated/CoreUnfolder.v
@@ -9,6 +9,7 @@ for i in eval eval_from compact_digit_cps compact_digit compact_step_cps compact
     echo "  Definition ${i}_sig := parameterize_sig (@Core.Columns.${i}).";
     echo "  Definition ${i} := parameterize_from_sig ${i}_sig.";
     echo "  Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "  Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
     echo "  Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 echo "End Columns."
@@ -16,66 +17,79 @@ echo "End Columns."
   Definition eval_sig := parameterize_sig (@Core.Columns.eval).
   Definition eval := parameterize_from_sig eval_sig.
   Definition eval_eq := parameterize_eq eval eval_sig.
+  Hint Unfold eval : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- eval_eq : pattern_runtime.
 
   Definition eval_from_sig := parameterize_sig (@Core.Columns.eval_from).
   Definition eval_from := parameterize_from_sig eval_from_sig.
   Definition eval_from_eq := parameterize_eq eval_from eval_from_sig.
+  Hint Unfold eval_from : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- eval_from_eq : pattern_runtime.
 
   Definition compact_digit_cps_sig := parameterize_sig (@Core.Columns.compact_digit_cps).
   Definition compact_digit_cps := parameterize_from_sig compact_digit_cps_sig.
   Definition compact_digit_cps_eq := parameterize_eq compact_digit_cps compact_digit_cps_sig.
+  Hint Unfold compact_digit_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- compact_digit_cps_eq : pattern_runtime.
 
   Definition compact_digit_sig := parameterize_sig (@Core.Columns.compact_digit).
   Definition compact_digit := parameterize_from_sig compact_digit_sig.
   Definition compact_digit_eq := parameterize_eq compact_digit compact_digit_sig.
+  Hint Unfold compact_digit : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- compact_digit_eq : pattern_runtime.
 
   Definition compact_step_cps_sig := parameterize_sig (@Core.Columns.compact_step_cps).
   Definition compact_step_cps := parameterize_from_sig compact_step_cps_sig.
   Definition compact_step_cps_eq := parameterize_eq compact_step_cps compact_step_cps_sig.
+  Hint Unfold compact_step_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- compact_step_cps_eq : pattern_runtime.
 
   Definition compact_step_sig := parameterize_sig (@Core.Columns.compact_step).
   Definition compact_step := parameterize_from_sig compact_step_sig.
   Definition compact_step_eq := parameterize_eq compact_step compact_step_sig.
+  Hint Unfold compact_step : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- compact_step_eq : pattern_runtime.
 
   Definition compact_cps_sig := parameterize_sig (@Core.Columns.compact_cps).
   Definition compact_cps := parameterize_from_sig compact_cps_sig.
   Definition compact_cps_eq := parameterize_eq compact_cps compact_cps_sig.
+  Hint Unfold compact_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- compact_cps_eq : pattern_runtime.
 
   Definition compact_sig := parameterize_sig (@Core.Columns.compact).
   Definition compact := parameterize_from_sig compact_sig.
   Definition compact_eq := parameterize_eq compact compact_sig.
+  Hint Unfold compact : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- compact_eq : pattern_runtime.
 
   Definition cons_to_nth_cps_sig := parameterize_sig (@Core.Columns.cons_to_nth_cps).
   Definition cons_to_nth_cps := parameterize_from_sig cons_to_nth_cps_sig.
   Definition cons_to_nth_cps_eq := parameterize_eq cons_to_nth_cps cons_to_nth_cps_sig.
+  Hint Unfold cons_to_nth_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- cons_to_nth_cps_eq : pattern_runtime.
 
   Definition cons_to_nth_sig := parameterize_sig (@Core.Columns.cons_to_nth).
   Definition cons_to_nth := parameterize_from_sig cons_to_nth_sig.
   Definition cons_to_nth_eq := parameterize_eq cons_to_nth cons_to_nth_sig.
+  Hint Unfold cons_to_nth : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- cons_to_nth_eq : pattern_runtime.
 
   Definition nils_sig := parameterize_sig (@Core.Columns.nils).
   Definition nils := parameterize_from_sig nils_sig.
   Definition nils_eq := parameterize_eq nils nils_sig.
+  Hint Unfold nils : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- nils_eq : pattern_runtime.
 
   Definition from_associational_cps_sig := parameterize_sig (@Core.Columns.from_associational_cps).
   Definition from_associational_cps := parameterize_from_sig from_associational_cps_sig.
   Definition from_associational_cps_eq := parameterize_eq from_associational_cps from_associational_cps_sig.
+  Hint Unfold from_associational_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- from_associational_cps_eq : pattern_runtime.
 
   Definition from_associational_sig := parameterize_sig (@Core.Columns.from_associational).
   Definition from_associational := parameterize_from_sig from_associational_sig.
   Definition from_associational_eq := parameterize_eq from_associational from_associational_sig.
+  Hint Unfold from_associational : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- from_associational_eq : pattern_runtime.
 
 End Columns.
diff --git a/src/Arithmetic/Saturated/FreezeUnfolder.v b/src/Arithmetic/Saturated/FreezeUnfolder.v
index 9545e23ed..bae1a87f3 100644
--- a/src/Arithmetic/Saturated/FreezeUnfolder.v
+++ b/src/Arithmetic/Saturated/FreezeUnfolder.v
@@ -10,15 +10,18 @@ for i in freeze freeze_cps; do
     echo "Definition ${i}_sig := parameterize_sig (@Freeze.${i}).";
     echo "Definition ${i} := parameterize_from_sig ${i}_sig.";
     echo "Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
     echo "Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 >> *)
 Definition freeze_cps_sig := parameterize_sig (@Freeze.freeze_cps).
 Definition freeze_cps := parameterize_from_sig freeze_cps_sig.
 Definition freeze_cps_eq := parameterize_eq freeze_cps freeze_cps_sig.
+Hint Unfold freeze_cps : basesystem_partial_evaluation_unfolder.
 Hint Rewrite <- freeze_cps_eq : pattern_runtime.
 
 Definition freeze_sig := parameterize_sig (@Freeze.freeze).
 Definition freeze := parameterize_from_sig freeze_sig.
 Definition freeze_eq := parameterize_eq freeze freeze_sig.
+Hint Unfold freeze : basesystem_partial_evaluation_unfolder.
 Hint Rewrite <- freeze_eq : pattern_runtime.
diff --git a/src/Arithmetic/Saturated/MulSplitUnfolder.v b/src/Arithmetic/Saturated/MulSplitUnfolder.v
index d74051e46..e9747eb79 100644
--- a/src/Arithmetic/Saturated/MulSplitUnfolder.v
+++ b/src/Arithmetic/Saturated/MulSplitUnfolder.v
@@ -11,6 +11,7 @@ for i in sat_multerm_cps sat_multerm sat_mul_cps sat_mul; do
     echo "    Definition ${i}_sig := parameterize_sig (@MulSplit.B.Associational.${i}).";
     echo "    Definition ${i} := parameterize_from_sig ${i}_sig.";
     echo "    Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "    Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
     echo "    Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 echo "  End Associational."
@@ -19,21 +20,25 @@ echo "End B."
     Definition sat_multerm_cps_sig := parameterize_sig (@MulSplit.B.Associational.sat_multerm_cps).
     Definition sat_multerm_cps := parameterize_from_sig sat_multerm_cps_sig.
     Definition sat_multerm_cps_eq := parameterize_eq sat_multerm_cps sat_multerm_cps_sig.
+    Hint Unfold sat_multerm_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- sat_multerm_cps_eq : pattern_runtime.
 
     Definition sat_multerm_sig := parameterize_sig (@MulSplit.B.Associational.sat_multerm).
     Definition sat_multerm := parameterize_from_sig sat_multerm_sig.
     Definition sat_multerm_eq := parameterize_eq sat_multerm sat_multerm_sig.
+    Hint Unfold sat_multerm : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- sat_multerm_eq : pattern_runtime.
 
     Definition sat_mul_cps_sig := parameterize_sig (@MulSplit.B.Associational.sat_mul_cps).
     Definition sat_mul_cps := parameterize_from_sig sat_mul_cps_sig.
     Definition sat_mul_cps_eq := parameterize_eq sat_mul_cps sat_mul_cps_sig.
+    Hint Unfold sat_mul_cps : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- sat_mul_cps_eq : pattern_runtime.
 
     Definition sat_mul_sig := parameterize_sig (@MulSplit.B.Associational.sat_mul).
     Definition sat_mul := parameterize_from_sig sat_mul_sig.
     Definition sat_mul_eq := parameterize_eq sat_mul sat_mul_sig.
+    Hint Unfold sat_mul : basesystem_partial_evaluation_unfolder.
     Hint Rewrite <- sat_mul_eq : pattern_runtime.
 
   End Associational.
diff --git a/src/Arithmetic/Saturated/WrappersUnfolder.v b/src/Arithmetic/Saturated/WrappersUnfolder.v
index 52006a702..d28719af8 100644
--- a/src/Arithmetic/Saturated/WrappersUnfolder.v
+++ b/src/Arithmetic/Saturated/WrappersUnfolder.v
@@ -11,6 +11,7 @@ for i in add_cps unbalanced_sub_cps mul_cps conditional_add_cps; do
     echo "  Definition ${i}_sig := parameterize_sig (@Wrappers.Columns.${i}).";
     echo "  Definition ${i} := parameterize_from_sig ${i}_sig.";
     echo "  Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "  Hint Unfold ${i} : basesystem_partial_evaluation_unfolder.";
     echo "  Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
 done
 echo "End Columns."
@@ -18,21 +19,25 @@ echo "End Columns."
   Definition add_cps_sig := parameterize_sig (@Wrappers.Columns.add_cps).
   Definition add_cps := parameterize_from_sig add_cps_sig.
   Definition add_cps_eq := parameterize_eq add_cps add_cps_sig.
+  Hint Unfold add_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- add_cps_eq : pattern_runtime.
 
   Definition unbalanced_sub_cps_sig := parameterize_sig (@Wrappers.Columns.unbalanced_sub_cps).
   Definition unbalanced_sub_cps := parameterize_from_sig unbalanced_sub_cps_sig.
   Definition unbalanced_sub_cps_eq := parameterize_eq unbalanced_sub_cps unbalanced_sub_cps_sig.
+  Hint Unfold unbalanced_sub_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- unbalanced_sub_cps_eq : pattern_runtime.
 
   Definition mul_cps_sig := parameterize_sig (@Wrappers.Columns.mul_cps).
   Definition mul_cps := parameterize_from_sig mul_cps_sig.
   Definition mul_cps_eq := parameterize_eq mul_cps mul_cps_sig.
+  Hint Unfold mul_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- mul_cps_eq : pattern_runtime.
 
   Definition conditional_add_cps_sig := parameterize_sig (@Wrappers.Columns.conditional_add_cps).
   Definition conditional_add_cps := parameterize_from_sig conditional_add_cps_sig.
   Definition conditional_add_cps_eq := parameterize_eq conditional_add_cps conditional_add_cps_sig.
+  Hint Unfold conditional_add_cps : basesystem_partial_evaluation_unfolder.
   Hint Rewrite <- conditional_add_cps_eq : pattern_runtime.
 
 End Columns.