Commit a2bd2a04 authored by charguer's avatar charguer

factorized tactics

parent 69220d28
......@@ -8,7 +8,7 @@ From Sep Require Import LambdaSep.
Require Import SepGPM.
Module ProofMode.
Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicTactics.SS.
Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicTactics.SS SepBasicTactics.
Export SepBasicGPM.ProofMode.
Definition wp (t:trm) (Q:val->hprop) : hprop :=
......@@ -40,42 +40,4 @@ Proof.
Qed.
(**--- TODO: factorize in SepGPM (with tactic rebinding?) *)
(* ProofMode's [iIntros] tend to move pure facts in Coq's context.
While, in general, this is desirable, this is not what we want
after having applied [local_ramified_frame] because we would loose
pure facts that will not be unified in [Q] when [Q] is an evar. As
a result, we use a specific version of this lemma where Q1 is
locked, and hence pure facts cannot escape.
This specific version is only used when the post-condition is
indeed an evar. *)
Lemma local_ramified_frame_locked {B} : forall (Q1 : B hprop) H1 F H Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* (locked Q1 \---* Q) ->
F H Q.
Proof using. unlock. apply local_ramified_frame. Qed.
Ltac ram_apply lem :=
lazymatch goal with
| |- ?F _ ?Q =>
(is_evar Q; eapply local_ramified_frame_locked) ||
eapply local_ramified_frame
end; [xlocal_core tt|eapply lem|iPrepare].
(* TODO: try to factorize this: *)
Ltac hpull_xpull_iris_hook tt ::=
unfold_proofmode.
End ProofMode.
......@@ -11,10 +11,35 @@ Global Generalizable No Variables.
Global Obligation Tactic := Coq.Program.Tactics.program_simpl.
Module SepLogicGPM (SL : SepLogicCore) (SS : SepLogicSetupSig SL).
Export SS.
(* ********************************************************************** *)
(* * Subset of the interface of SepTactics that needs to be exposed to GPM *)
Module Type SepLogicTacticsSig (SL : SepLogicCore) (SS : SepLogicSetupSig SL).
Import SL SS.
Ltac hpull_xpull_iris_hook := idtac.
Ltac xlocal_core := idtac.
Parameter local_ramified_frame : forall B (Q1:B->hprop) H1 F H Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* (Q1 \---* Q) ->
F H Q.
End SepLogicTacticsSig.
(* ********************************************************************** *)
(* * Proof Mode *)
Module SepLogicGPM (SL : SepLogicCore) (SS : SepLogicSetupSig SL)
(ST : SepLogicTacticsSig SL SS).
Export SS.
Import ST.
(* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *)
......@@ -302,7 +327,6 @@ Ltac iPrepare :=
eapply tac_prepare; [apply _|cbv beta].
(* TODO: try to factorize this (using tactic rebinding?
(* ProofMode's [iIntros] tend to move pure facts in Coq's context.
While, in general, this is desirable, this is not what we want
......@@ -327,18 +351,13 @@ Ltac ram_apply lem :=
eapply local_ramified_frame
end; [xlocal_core tt|eapply lem|iPrepare].
*)
(* TODO: try to factorize this:
(** Fix for hpull/xpull to unfold proof mode functions *)
Ltac hpull_xpull_iris_hook tt ::=
ProofModeInstantiate.unfold_proofmode.
*)
End ProofMode.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment