Commit 09b1563c authored by Robbert Krebbers's avatar Robbert Krebbers

Make iFresh faster on environments containing evars.

Generating a fresh name consists of two stages:
+ Use [cbv] to compute a list representing the domain of the environment. This
  is a very simply computation that just erases the hypotheses.
+ Use [vm_compute] to compute a fresh name based on the list representing the
  domain. The domain itself should never contain evars, so [vm_compute] will
  do the job.
parent 1662c1dc
Pipeline #1234 passed with stage
......@@ -33,8 +33,8 @@ Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Instance envs_dom {M} : Dom (envs M) stringset := λ Δ,
dom stringset (env_persistent Δ) dom stringset (env_spatial Δ).
Definition envs_dom {M} (Δ : envs M) : list string :=
env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
let (Γp,Γs) := Δ in
......
......@@ -32,11 +32,8 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
Coercion env_to_list : env >-> list.
Instance: Params (@env_to_list) 1.
Instance env_dom {A} : Dom (env A) stringset :=
fix go Γ := let _ : Dom _ _ := @go in
match Γ with Enil => | Esnoc Γ i _ => {[ i ]} dom stringset Γ end.
Fixpoint env_dom_list {A} (Γ : env A) : list string :=
match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom_list Γ end.
Fixpoint env_dom {A} (Γ : env A) : list string :=
match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
Fixpoint env_fold {A B} (f : B A A) (x : A) (Γ : env B) : A :=
match Γ with
......
......@@ -22,13 +22,10 @@ Ltac env_cbv :=
Ltac iFresh :=
lazymatch goal with
|- of_envs ?Δ _ =>
match goal with
| _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
| _ =>
(* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
let Hs := eval cbv in (dom stringset Δ) in
eval vm_compute in (fresh_string_of_set "~" Hs)
end
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
first use [cbv] to compute the domain of [Δ] *)
let Hs := eval cbv in (envs_dom Δ) in
eval vm_compute in (fresh_string_of_set "~" (of_list Hs))
| _ => constr:"~"
end.
......@@ -383,8 +380,7 @@ Tactic Notation "iFrame" :=
| ?H :: ?Hs => try iFrame H; go Hs
end in
match goal with
| |- of_envs ?Δ _ =>
let Hs := eval cbv in (env_dom_list (env_spatial Δ)) in go Hs
| |- of_envs ?Δ _ => let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
end.
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
......@@ -681,7 +677,7 @@ idents I do not know how to do this better. *)
Local Ltac iLöbHelp IH tac_before tac_after :=
match goal with
| |- of_envs ?Δ _ =>
let Hs := constr:(reverse (env_dom_list (env_spatial Δ))) in
let Hs := constr:(reverse (env_dom (env_spatial Δ))) in
iRevert ["★"]; tac_before;
eapply tac_löb with _ IH;
[reflexivity
......
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