Commit fdaee774 authored by Janno's avatar Janno

Code beautification.

parent b8bff04f
......@@ -124,17 +124,16 @@ Definition wp_expr_simpl_value_head {Σ} {hG : heapG Σ} {Δ s E Φ e} :=
Local Open Scope MC.
Definition wp_pure `{heapG Σ} {Δ s e E Φ} (efoc : expr) :
TT.ttac (envs_entails Δ (WP e @ s ; E {{ Φ }}))
:=
TT.ttac (envs_entails Δ (WP e @ s ; E {{ Φ }})) :=
let e := rsimpl e in
mtry reshape_expr_wp e (λ K e',
mtry M.unify_or_fail UniEvarconv e' efoc
with NotUnifiable e' efoc => raise TryNextDecomposition end;;
' e2 φ <- M.evar _;
TT.apply (tac_wp_pure _ Δ' _ _ (fill K e') e2 φ _)
<**> (mtry TT.apply_ with | _ => raise TryNextDecomposition end)
<**> (mtry TT.apply_ with _ => raise TryNextDecomposition end)
(* PureExec *)
<**> TT.use (T.try fast_done) (* The pure condition for PureExec *)
<**> TT.try (TT.use fast_done) (* The pure condition for PureExec *)
<**> TT.apply_ (* IntoLaters *)
<**> `e' <- M.evar _; (* new goal *)
wp_expr_simpl_subst e'
......
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