diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-19 15:46:05 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-19 15:46:05 -0400 |
commit | 2f52a3d2e1df6a46d7a96471ae313ee61401446a (patch) | |
tree | a81770843dda891396d99604c01f885a316b6cc5 /src/Arithmetic/Saturated | |
parent | 7e939cd63236d0a6a492ddff5015daf3f706a3bc (diff) |
Add more unfolds to basesystem_partial_evaluation_unfolder
Diffstat (limited to 'src/Arithmetic/Saturated')
-rw-r--r-- | src/Arithmetic/Saturated/CoreUnfolder.v | 14 | ||||
-rw-r--r-- | src/Arithmetic/Saturated/FreezeUnfolder.v | 3 | ||||
-rw-r--r-- | src/Arithmetic/Saturated/MulSplitUnfolder.v | 5 | ||||
-rw-r--r-- | src/Arithmetic/Saturated/WrappersUnfolder.v | 5 |
4 files changed, 27 insertions, 0 deletions
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. |