diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 12:54:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:54:31 -0400 |
| commit | 15a026fc6aead83edd616ffd870a383a8d0d1210 (patch) | |
| tree | 33052846c888a8566034bdd3225df937fc52d739 /src/Reflection | |
| parent | 5bef18ca16a008e49b7b7bca5f7920149bd1bbaf (diff) | |
Make Z Reification handle correctness proofs
Diffstat (limited to 'src/Reflection')
| -rw-r--r-- | src/Reflection/Reify.v | 2 | ||||
| -rw-r--r-- | src/Reflection/Z/Reify.v | 17 |
2 files changed, 17 insertions, 2 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index ce6a8db08..3606cae99 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -265,7 +265,7 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := [hnf] is enough to unfold the interpretation functions that we're parameterized over. *) lazymatch goal with - | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ] + | [ |- ?R (@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e) _ ] => let interp_base_type' := (eval hnf in interp_base_type) in let interp_op' := (eval hnf in interp_op) in change interp_base_type with interp_base_type'; 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 ()). |