diff options
| -rw-r--r-- | src/Reflection/InputSyntax.v | 19 | ||||
| -rw-r--r-- | src/Reflection/Reify.v | 33 | ||||
| -rw-r--r-- | src/Reflection/Z/Reify.v | 2 |
3 files changed, 31 insertions, 23 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 15f7515b3..1c97d2174 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -105,18 +105,23 @@ Section language. end. Qed. - Lemma Compile_correct {t : flat_type} (e : @Expr t) - : Syntax.Interp interp_op (Compile e) = Interp interp_op e. + Lemma Compile_correct {t} (e : @Expr t) + : interp_type_gen_rel_pointwise (fun _ => @eq _) + (Syntax.Interp interp_op (Compile e)) + (Interp interp_op e). Proof. unfold Interp, Compile, Syntax.Interp; simpl. pose (e interp_flat_type) as E. repeat match goal with |- context[e ?f] => change (e f) with E end. - refine match E with - | Abs _ _ _ => fun x : Prop => x (* small inversions *) - | Return _ _ => _ - end. - apply compilef_correct. + clearbody E; clear e. + induction E. + { apply compilef_correct. } + { simpl; auto. } Qed. + + Lemma Compile_flat_correct {t : flat_type} (e : @Expr t) + : Syntax.Interp interp_op (Compile e) = Interp interp_op e. + Proof. exact (@Compile_correct t e). Qed. End compile_correct. End expr_param. End language. 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 ()). diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index 9500b2b88..87c3e29e7 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -27,4 +27,4 @@ Ltac Reify e := let v := Reflection.Reify.Reify base_type interp_base_type op e in constr:((*Inline _*) ((*CSE _*) (InlineConst (Linearize v)))). Ltac Reify_rhs := - etransitivity; [ | Reflection.Reify.Reify_rhs base_type interp_base_type op interp_op ]. + Reflection.Reify.Reify_rhs_gen Reify ltac:(fun _ => idtac) interp_op ltac:(fun tac => try tac ()). |