diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-15 18:33:55 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-15 21:25:38 -0400 |
| commit | 32107e1115481c124cb966c1df6bf3d2c29013cc (patch) | |
| tree | c572b01b20817aabae86f74fb29e7aed728477e4 /src/Arithmetic/Saturated | |
| parent | 676e93c06a448259783f5934f37e1219265b7726 (diff) | |
Extend basesystem_partial_evaluation_RHS
Now there's a version that handles things in Saturated.Core, and in
Wrappers.
Diffstat (limited to 'src/Arithmetic/Saturated')
| -rw-r--r-- | src/Arithmetic/Saturated/Core.v | 20 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated/Wrappers.v | 11 |
2 files changed, 30 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v index 355d6b429..face608ab 100644 --- a/src/Arithmetic/Saturated/Core.v +++ b/src/Arithmetic/Saturated/Core.v @@ -427,3 +427,23 @@ Hint Rewrite @Columns.eval_from_associational @Columns.eval_nils using (assumption || omega): push_basesystem_eval. + +Ltac basesystem_partial_evaluation_unfolder t := + let t := + (eval + cbv + delta [ + (* this list must contain all definitions referenced by t that reference [Let_In], [runtime_add], [runtime_opp], [runtime_mul], [runtime_shr], or [runtime_and] *) + Columns.eval Columns.eval_from + Columns.compact_digit_cps Columns.compact_digit + Columns.compact_step_cps Columns.compact_step + Columns.compact_cps Columns.compact + Columns.cons_to_nth_cps Columns.cons_to_nth + Columns.nils + Columns.from_associational_cps Columns.from_associational + ] in t) in + let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in + t. + +Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::= + basesystem_partial_evaluation_unfolder t. diff --git a/src/Arithmetic/Saturated/Wrappers.v b/src/Arithmetic/Saturated/Wrappers.v index e1da74e60..e9b73dd10 100644 --- a/src/Arithmetic/Saturated/Wrappers.v +++ b/src/Arithmetic/Saturated/Wrappers.v @@ -50,4 +50,13 @@ Hint Unfold Columns.conditional_add_cps Columns.add_cps Columns.unbalanced_sub_cps - Columns.mul_cps.
\ No newline at end of file + Columns.mul_cps. + +Ltac basesystem_partial_evaluation_unfolder t := + let t := (eval cbv delta [Columns.add_cps Columns.unbalanced_sub_cps Columns.mul_cps Columns.conditional_add_cps] in t) in + let t := Saturated.Core.basesystem_partial_evaluation_unfolder t in + let t := Arithmetic.Core.basesystem_partial_evaluation_unfolder t in + t. + +Ltac Arithmetic.Core.basesystem_partial_evaluation_default_unfolder t ::= + basesystem_partial_evaluation_unfolder t. |