diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-30 12:21:57 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:21:57 -0400 |
commit | 71b2c82fab79b17a8eef0c596f6bb81291ca9968 (patch) | |
tree | d56fa5642478952614e6dd833103c9f115ebf4c8 /src | |
parent | 422325d2b34a099f4599fa8096ceebf022b5358d (diff) |
Factor Reify_rhs so that it's more reusable
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Reify.v | 54 |
1 files changed, 32 insertions, 22 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 2631a8a21..7b20f5efe 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -240,27 +240,37 @@ Ltac Reify base_type_code interp_base_type op e := Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. -Ltac Reify_rhs base_type_code interp_base_type op interp_op := +Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op := let rhs := rhs_of_goal in - let RHS := Reify base_type_code interp_base_type op rhs in - transitivity (Syntax.Interp interp_op RHS); + let RHS := Reify rhs in + let RHS' := (eval vm_compute in RHS) in + transitivity (Syntax.Interp interp_op RHS'); [ - | etransitivity; (* first we strip off the [InputSyntax.Compile] - bit; Coq is bad at inferring the type, so we - help it out by providing it *) - [ lazymatch goal with - | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] - => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e) - end - | ((* now we unfold the interpretation function, including the - parameterized bits; we assume that [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 = _ ] - => 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'; - change interp_op with interp_op' - end; - cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; simplify_projections; reflexivity) ] ]. + | transitivity (Syntax.Interp interp_op RHS); + [ apply f_equal; vm_compute; reflexivity + | etransitivity; (* first we strip off the [InputSyntax.Compile] + bit; Coq is bad at inferring the type, so we + help it out by providing it *) + [ prove_interp_compile_correct () + | ((* now we unfold the interpretation function, including the + parameterized bits; we assume that [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 = _ ] + => 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'; + change interp_op with interp_op' + end; + cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type interp interpf]; simplify_projections; reflexivity) ] ] ]. + +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_correct base_type_code interp_base_type op interp_op t e) + end) + interp_op. |