diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 12:43:07 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:43:07 -0400 |
| commit | 5bef18ca16a008e49b7b7bca5f7920149bd1bbaf (patch) | |
| tree | 0e9f083f4def6e608f0c6010fe26954a4e8d1e4f /src/Reflection/Reify.v | |
| parent | dcff7c65666a13a95950adcd933ca162db32622c (diff) | |
Factor out prove_compile_correct
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index fbe718f6c..ce6a8db08 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -273,13 +273,17 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := end; cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; simplify_projections; reflexivity) ] ] ]. +Ltac prove_compile_correct := + fun _ => lazymatch goal with + | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] + => exact (@InputSyntax.Compile_flat_correct base_type_code interp_base_type op interp_op t e) + | [ |- interp_type_gen_rel_pointwise _ (@Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t (@Compile _ _ _ _ ?e)) _ ] + => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e) + end. + Ltac Reify_rhs base_type_code interp_base_type op interp_op := Reify_rhs_gen ltac:(Reify base_type_code interp_base_type op) - ltac:(fun _ - => lazymatch goal with - | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] - => exact (@InputSyntax.Compile_flat_correct base_type_code interp_base_type op interp_op t e) - end) - interp_op - ltac:(fun tac => tac ()). + prove_compile_correct + interp_op + ltac:(fun tac => tac ()). |