blob: bae1a87f32e4013b3e7bccddc918314b53e45933 (
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
|
Require Import Crypto.Arithmetic.CoreUnfolder.
Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
Require Import Crypto.Arithmetic.Saturated.WrappersUnfolder.
Require Import Crypto.Arithmetic.Saturated.Freeze.
(**
<<
#!/bin/bash
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.
|
