diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 12:35:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 12:35:06 -0400 |
| commit | 7a9faafa8a3507bc20ae15bbe71200d9c4b5a12b (patch) | |
| tree | cb1efeaf96cea972407717c9fa967cc1d4c8baf3 /src/Reflection/Reify.v | |
| parent | 71b2c82fab79b17a8eef0c596f6bb81291ca9968 (diff) | |
Generalize InputSyntax.Compile_correct
Diffstat (limited to 'src/Reflection/Reify.v')
| -rw-r--r-- | src/Reflection/Reify.v | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 7b20f5efe..7ad4f42c1 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -240,7 +240,7 @@ 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_gen Reify prove_interp_compile_correct interp_op := +Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := let rhs := rhs_of_goal in let RHS := Reify rhs in let RHS' := (eval vm_compute in RHS) in @@ -252,18 +252,20 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op := 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) ] ] ]. + | try_tac + ltac:(fun _ + => (* 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 @@ -271,6 +273,7 @@ Ltac Reify_rhs base_type_code interp_base_type op interp_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) + => exact (@InputSyntax.Compile_flat_correct base_type_code interp_base_type op interp_op t e) end) - interp_op. + interp_op + ltac:(fun tac => tac ()). |