Commit 13c1d3dc authored by Janno's avatar Janno

Define Mtac2 version of `wp_store`.

Todo: move `first` and `|| [ .. ]` to Mtac2 repo.
parent 9744f976
......@@ -236,16 +236,15 @@ Definition wp_bind (efoc : expr) : tactic :=
.
Tactic Notation "wp_bind" open_constr(efoc) := mrun (wp_bind efoc).
(*
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
|| fail "wp_bind: cannot find" efoc "in" e
| _ => fail "wp_bind: not a 'wp'"
end.
*)
(* Tactic Notation "wp_bind" open_constr(efoc) := *)
(* iStartProof; *)
(* lazymatch goal with *)
(* | |- envs_entails _ (wp ?s ?E ?e ?Q) => *)
(* reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K) *)
(* || fail "wp_bind: cannot find" efoc "in" e *)
(* | _ => fail "wp_bind: not a 'wp'" *)
(* end. *)
(** Heap tactics *)
Section heap.
......@@ -461,33 +460,124 @@ Definition iAssumptionLookup {A : ucmraT} {Δ} {P : uPred A} {b : bool} {i : ide
| _, _, _ => M.print_term (evi, evP, evb);; mfail "iAssumptionLookup: search problem underconstrained."
end.
Definition wp_load : tactic :=
iStartProof $ iStartHeapProof "wp_load" $ λ '(IHeapGoal Σ _ Δ s e E Φ),
mtry
reshape_expr_wp e $ λ K e',
mmatch e' as e' return M (envs_entails _ (WP fill K e' @ _ ; _ {{ _ }}) *m _) with
| [? l : loc] (Lit (LitLoc l)) =u>
(* We need to find the "real" context to be filled with `Load …` later *)
mmatch K as K return M (envs_entails _ (WP fill K _ @ _ ; _ {{ _ }}) *m _) with
| [#] cons LoadCtx | K =n>
' v q i <- M.evar _;
TT.apply (tac_wp_load Δ Δ' s E i K l q v Φ)
<**> TT.apply_ (* IntoLaterEnvs *)
<**> (mtry iAssumptionLookup with
| NotFoundInEnv => mfail "Cannot find " l " ↦ ?"
end)
<**> `e' <- M.evar _;
wp_expr_simpl_subst e'
<**> TT.try wp_value_head
| _ => raise TryNextDecomposition
Structure CanonicalException {T : Prop} :=
mkCanonicalException {
canon_excn_term : T;
_ : Exception;
}.
Arguments mkCanonicalException {_} _ _.
Arguments CanonicalException _ : clear implicits.
Definition canon_excn_excn {T} : CanonicalException T -> Exception. destruct 1 as [_ E]. exact E. Defined.
Definition catch_canonical_exception {T} {C : CanonicalException (M T)} (t r : M T) (_ : canon_excn_term C = t)
:=
mtry' t (fun e' =>
let e := reduce (RedWhd [rl: RedBeta; RedMatch; RedDelta]) (canon_excn_excn C) in
mmatch e' with
| e =n> r
| _ => raise NotCaught
end).
Notation "t '||[_' ] r" :=
(catch_canonical_exception t r (@eq_refl _ t%MC))
(at level 100, format "t ||[_ ] r").
Notation "t '||[' e1 .. en ] r" :=
(mtry' t (fun e => mmatch' (P:=fun _ => _)
NotCaught e
(mcons (e1 =n> r)%branch .. (mcons (en =n> r)%branch mnil) ..))
) (at level 100, e1 at level 0, en at level 0).
Definition compute_canon_excn (e : Exception):
forall {P : Prop} (p : P), M { T : Prop & T } :=
mfix2 go (P : Prop) (p : P) : M { T : Prop & T } :=
mmatch existT (P:=fun P: Prop=>P) P p return M {T : Prop & T} with
| [? T (t : M T)] existT (M T) (t) =u> M.ret (existT (CanonicalException (M T)) (mkCanonicalException t e))
| [? X (F : X -> Prop) (f : forall x:X, F x)] existT (forall x : X, F x) (f) =u>
\nu_f for f as x,
let F := reduce (RedOneStep [rl: RedBeta]) (F x) in
let f := reduce (RedOneStep [rl: RedBeta]) (f x) in
''(existT T t) <- go (F) (f);
T <- M.abs_prod_prop x T;
mmatch T with
| [!Prop] forall _ : X, F =n> (
x <- M.coerce x;
t <- M.coerce (B := F x) t;
t <- M.abs_fun (P:=F) x t;
t <- M.coerce t;
M.ret (existT T t)
)
end
| _ => raise TryNextDecomposition
end
.
Import Ascii.
Definition name_of_canon_excn {P} (p : P) : M string :=
M.pretty_print p >>=
(fix go acc s {struct s} :=
match s with
| String c s =>
match c with
| "("%char | "@"%char | ")"%char => go acc s
| "."%char => go (String "_" acc) s
| _ => go (String c acc) s
end
with ReshapeExprExc =>
mfail "wp_pure: cannot find 'Load' in in " e
end.
| EmptyString =>
match acc with
| EmptyString => mfail "Cannot compute name for CanonicalException structure."
| _ => let r := reduce (RedStrong RedAll) (String.concat "_" ["canon_excn_auto"; string_rev acc]) in
M.ret r
end
end) EmptyString.
Definition declare_canon_excn {P : Prop} (p : P) (e : Exception) :=
''(existT T t) <- compute_canon_excn e p;
name <- name_of_canon_excn p;
M.declare dok_CanonicalStructure name false t;; M.ret ().
Tactic Notation "wp_load" := mrun (wp_load).
Mtac Do (declare_canon_excn (@TT.change_dep) TT.TTchange_Exception).
Mtac Do (declare_canon_excn (@TT.change) TT.TTchange_Exception).
Mtac Do (declare_canon_excn (@reshape_expr_wp) ReshapeExprExc).
Mtac Do (declare_canon_excn (@iAssumptionLookup) NotFoundInEnv).
Definition wp_load : tactic :=
iStartProof $ iStartHeapProof "wp_load" $ λ '(IHeapGoal Σ _ Δ s e E Φ),
(reshape_expr_wp e $ λ K e',
' v q i l <- M.evar _;
TT.change_dep (λ e, envs_entails _ (WP e @ _ ; _ {{ _ }})) _ (
TT.apply (tac_wp_load Δ Δ' s E i K l q v Φ)
<**> TT.apply_
<**> (iAssumptionLookup ||[NotFoundInEnv] mfail "Cannot find " l " ↦ ?")
<**> `e' <- M.evar _;
wp_expr_simpl_subst e'
<**> TT.try wp_value_head
) ||[TT.TTchange_Exception] raise TryNextDecomposition
) ||[ReshapeExprExc] mfail "wp_load: cannot find 'Load' in " e.
(* with *)
(* | TT.TTchange_Exception => raise TryNextDecomposition *)
(* end *)
(* mmatch e' as e' return M (envs_entails _ (WP fill K e' @ _ ; _ {{ _ }}) *m _) with *)
(* | [? l : loc] (Lit (LitLoc l)) =u> *)
(* (* We need to find the "real" context to be filled with `Load …` later *) *)
(* mmatch K as K return M (envs_entails _ (WP fill K _ @ _ ; _ {{ _ }}) *m _) with *)
(* | [#] cons LoadCtx | K =n> *)
(* `Δ' v q i <- M.evar _; *)
(* TT.apply (tac_wp_load Δ Δ' s E i K l q v Φ) *)
(* <**> TT.apply_ (* IntoLaterEnvs *) *)
(* <**> (mtry iAssumptionLookup with *)
(* | NotFoundInEnv => mfail "Cannot find " l " ↦ ?" *)
(* end) *)
(* <**> `e' <- M.evar _; *)
(* wp_expr_simpl_subst e' *)
(* <**> TT.try wp_value_head *)
(* | _ => raise TryNextDecomposition *)
(* end *)
(* | _ => raise TryNextDecomposition *)
(* end *)
Tactic Notation "wp_load" :=
mrun (wp_load).
(* iStartProof; *)
(* lazymatch goal with *)
(* | |- envs_entails _ (wp ?s ?E ?e ?Q) => *)
......@@ -510,33 +600,21 @@ Fixpoint first {A} (ls: mlist (TT.ttac A)) : TT.ttac A :=
Definition wp_store : tactic :=
iStartProof $ iStartHeapProof "wp_store" $ λ '(IHeapGoal Σ _ Δ s e E Φ),
mtry
reshape_expr_wp e $ λ K e',
mmatch e' as e' return M (envs_entails _ (WP fill K e' @ _ ; _ {{ _ }}) *m _) with
| [? l : loc] (Lit (LitLoc l)) =u>
(* We need to find the "real" context to be filled with `Load …` later *)
mmatch K as K return M (envs_entails _ (WP fill K _ @ _ ; _ {{ _ }}) *m _) with
| [? e K] cons (StoreLCtx e) K =n>
' Δ'' v v' i <- M.evar _;
TT.apply (tac_wp_store Δ Δ' Δ'' s E i K l v _ v' Φ)
<**> TT.apply_ (* IntoVal *)
<**> TT.apply_ (* IntoLaterEnvs *)
<**> (mtry iAssumptionLookup with
| NotFoundInEnv => mfail "Cannot find " l " ↦ ?"
end)
<**> TT.use (env_cbv;; T.reflexivity)
<**> `e' <- M.evar _;
wp_expr_simpl_subst e'
<**> first [m: `e'' <- M.evar _;
TT.change_dep (fun e => envs_entails _ (wp _ _ e _)) e' (wp_pure (Seq (Lit LitUnit) e''))
| TT.try wp_value_head]
| _ => raise TryNextDecomposition
end
| _ => raise TryNextDecomposition
end
with ReshapeExprExc =>
mfail "wp_pure: cannot find 'Store' in in " e
end.
(reshape_expr_wp e $ λ K e',
' Δ'' v v' i l e'' <- M.evar _;
TT.change_dep (λ e, envs_entails _ (WP e @ _ ; _ {{ _ }})) _ (
TT.apply (tac_wp_store Δ Δ' Δ'' s E i K l v e'' v' Φ)
<**> TT.apply_ (* IntoVal *)
<**> TT.apply_ (* IntoLaterEnvs *)
<**> (iAssumptionLookup ||[NotFoundInEnv] mfail "Cannot find " l " ↦ ?")
<**> TT.use (env_cbv;; T.reflexivity)
<**> `e' <- M.evar _;
wp_expr_simpl_subst e'
<**> first [m: `e'' <- M.evar _;
TT.change_dep (fun e => envs_entails _ (wp _ _ e _)) e' (wp_pure (Seq (Lit LitUnit) e''))
| TT.try wp_value_head]
) ||[TT.TTchange_Exception] raise TryNextDecomposition
) ||[ReshapeExprExc] mfail "wp_store: cannot find 'Store' in " e.
Tactic Notation "wp_store" := mrun (wp_store).
(* iStartProof; *)
......
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