blob: b8fe6afc62b3994bbef44d61c4ae99387c1ff5b3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
Require Import Crypto.Arithmetic.CoreUnfolder.
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.
(**
<<
#!/bin/bash
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."
>> *)
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.
|
