blob: e9747eb79ba738d308b9e326e6398e54928582d2 (
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.MulSplit.
Module B.
Module Associational.
(**
<<
#!/bin/bash
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."
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.
End B.
|
