diff options
Diffstat (limited to 'src/Reflection/Z/Reify.v')
| -rw-r--r-- | src/Reflection/Z/Reify.v | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index 87c3e29e7..3c42c162c 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -1,9 +1,13 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. +Require Import Crypto.Reflection.InputSyntax. Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.Reflection.WfReflective. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Inline. +Require Import Crypto.Reflection.InlineInterp. Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.LinearizeInterp. Ltac base_reify_op op op_head ::= lazymatch op_head with @@ -26,5 +30,16 @@ Ltac Reify' e := Reflection.Reify.Reify' base_type interp_base_type op e. Ltac Reify e := let v := Reflection.Reify.Reify base_type interp_base_type op e in constr:((*Inline _*) ((*CSE _*) (InlineConst (Linearize v)))). +Ltac prove_InlineConst_Linearize_Compile_correct := + fun _ + => lazymatch goal with + | [ |- Syntax.interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (InlineConst (Linearize _))) _ ] + => etransitivity; + [ apply (@Interp_InlineConst base_type_code interp_base_type op interp_op t); + reflect_Wf base_type_eq_semidec_is_dec op_beq_bl + | etransitivity; + [ apply (@Interp_Linearize base_type_code interp_base_type op interp_op t) + | prove_compile_correct () ] ] + end. Ltac Reify_rhs := - Reflection.Reify.Reify_rhs_gen Reify ltac:(fun _ => idtac) interp_op ltac:(fun tac => try tac ()). + Reflection.Reify.Reify_rhs_gen Reify prove_InlineConst_Linearize_Compile_correct interp_op ltac:(fun tac => tac ()). |