blob: 9a0e0c06a2a49f904d474b7b185296a003b7af1e (
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
Require Import Crypto.Arithmetic.CoreUnfolder.
Require Import Crypto.Arithmetic.Saturated.Core.
Hint Unfold Core.Columns.compact_digit_cps Core.Columns.compact_step_cps Core.Columns.compact_cps : arithmetic_cps_unfolder.
Module Columns.
(**
<<
#!/bin/bash
for i in eval eval_from compact_digit_cps compact_digit compact_step_cps compact_step compact_cps compact cons_to_nth_cps cons_to_nth nils from_associational_cps from_associational; do
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."
>> *)
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.
|
