cap_machine.proofmode.register_tactics
From Ltac2 Require Import Ltac2 Control Fresh.
Set Default Proof Mode "Classic".
From iris.proofmode Require Import reduction proofmode.
From iris.proofmode Require Import environments.
From cap_machine Require Import stdpp_extra rules_base map_simpl.
Section denote_domain.
Variable K: Type.
Hypothesis HeqdecK: EqDecision K.
Hypothesis HcountK: Countable K.
(* if map_simpl is called first, the below will not contain overhead *)
Fixpoint denote_domain {A : Type} (rm: @rgmap A) (fm: nat -> option K) (mdom : gset K): gset K :=
match rm with
| Ins k a rm =>
match fm k with
| Some k => {[k]} ∪ denote_domain rm fm mdom
| None => denote_domain rm fm mdom end
| Del k rm =>
match fm k with
| Some k => denote_domain rm fm mdom ∖ {[k]}
| None => denote_domain rm fm mdom end
| Symb => mdom
end.
Local Arguments denote {_ _ _ _} _ _ _.
Lemma denote_domain_correct {A : Type} (rm: @rgmap A) (fm: nat -> option K) (m : gmap K A) (mdom : gset K) : dom m = mdom → dom (denote rm fm m) = denote_domain rm fm mdom.
intro Hmdom.
induction rm; cbn [denote denote_domain].
- case_eq (fm k); intros; set_solver + IHrm.
- case_eq (fm k); intros; set_solver + IHrm.
- done.
Unshelve. Fail idtac. Admitted.
End denote_domain.
Arguments denote_domain {_ _ _ _} _ _ _.
Arguments denote {_ _ _ _} _ _ _.
Ltac2 get_map_dom0 k a m hdom :=
let (x', m, fm) := (reify_helper k a m []) in
let env := make_list fm in
assert ($hdom := denote_domain_correct $k _ _ $x' (fun n => @list_lookup _ n $env) $m _ ltac:(first [ assumption | set_solver+]) );
rewrite ?dom_empty_L in $hdom;
cbn [denote denote_domain list_lookup lookup] in $hdom.
Ltac get_map_dom0 k a m hdom :=
let f := ltac2:(k a m hdom |- get_map_dom0 (Option.get (Ltac1.to_constr k)) (Option.get (Ltac1.to_constr a)) (Option.get (Ltac1.to_constr m)) (Option.get (Ltac1.to_ident hdom))) in f k a m ident:(hdom).
(* generate a domain hypothesis for a given gmap *)
Tactic Notation "get_map_dom" constr(m) "as" ident(hdom) :=
match type of m with
| ?t => match eval compute in t with (* type will not compute for very large maps *)
| gmap ?K ?A => let hdom' := fresh "hdom" in get_map_dom0 K A m ident:(hdom'); rename hdom' into hdom end end.
(* solving goals with map domains faster than set_solver *)
Tactic Notation "solve_map_dom" :=
let Hdom := fresh "Hdom" in
match goal with | |- dom ?m = ?dom => get_map_dom m as Hdom; rewrite Hdom; clear Hdom; set_solver+ end.
(* try to find concrete value in gmap *)
Ltac solve_lookup_some :=
repeat (
lazymatch goal with
| |- (<[ ?reg := ?w ]> ?rmap) !! ?reg = Some _ =>
rewrite lookup_insert; reflexivity
| |- (<[ ?reg := ?w ]> ?rmap) !! ?reg' = Some _ =>
rewrite lookup_insert_ne; [ | solve [auto]]
| |- (delete ?reg ?rmap) !! ?reg' = Some _ =>
rewrite lookup_delete_ne; [ | solve [auto]]
| |- _ !! ?reg = Some _ => exact
end ); fail.
Ltac extract_pointsto_map regs Hmap rname Hrdom Hreg :=
let rval := fresh "v"rname in
let Hsome := fresh "Hsome" in
first [ eassert (regs !! rname = Some _) as Hsome by solve_lookup_some (* Try to reuse existing value, if any *) |
assert (is_Some (regs !! rname)) as [rval Hsome] by (rewrite -elem_of_dom Hrdom; set_solver +) ];
let str_destr := constr:(("[" ++ Hreg ++ " " ++ Hmap ++ "]")%string) in
iDestruct (big_sepM_delete _ _ rname with Hmap) as str_destr; first exact Hsome; clear Hsome.
Ltac iExtract_core m' Hmap rnames Hregs Hrdom :=
match rnames with
| nil => idtac
| ?rname :: ?rtail =>
match Hregs with
| nil => idtac
| ?Hname :: ?Htail =>
extract_pointsto_map m' Hmap rname Hrdom Hname;
apply (f_equal (fun x => x ∖ {[rname]})) in Hrdom;
rewrite -dom_delete_L in Hrdom;
iExtract_core (delete rname m') Hmap rtail Htail Hrdom
end
end.
Ltac iExtract0 Hmap rnames Hregs :=
lazymatch goal with
| |- envs_entails ?H _ =>
lazymatch pm_eval (envs_lookup Hmap H) with
| Some (_, ?X) =>
lazymatch X with
| ([∗ map] _↦_ ∈ ?m', _)%I =>
let Hrdom := fresh "Hrdom" in
get_map_dom m' as Hrdom;
iExtract_core m' Hmap rnames Hregs Hrdom;
clear Hrdom;
map_simpl Hmap
end
end
end.
Tactic Notation "iExtract" constr(Hmap) constr(rname) "as" constr(Hreg):=
iExtract0 Hmap [rname] [Hreg].
Tactic Notation "iExtractList" constr(Hmap) constr(rnames) "as" constr(Hregs):=
iExtract0 Hmap rnames Hregs.
Ltac insert_pointsto_map regs Hmap rname Hrdom Hreg :=
let Hsome := fresh "Hsome" in
assert (regs !! rname = None) as Hsome by (rewrite -not_elem_of_dom Hrdom; set_solver +);
let str_destr := constr:(("[ $" ++ Hmap ++ " $" ++ Hreg ++ "]")%string) in
iDestruct (big_sepM_insert _ _ rname with str_destr) as Hmap; first exact Hsome; clear Hsome.
Ltac iInsert_core m' Hmap rnames Hrdom :=
match rnames with
| nil => idtac
| ?rname :: ?rtail =>
match goal with |- context [ Esnoc _ (INamed ?Hname) ?mtch ] =>
lazymatch mtch with | context [(rname ↦ᵣ ?rval)%I] =>
insert_pointsto_map m' Hmap rname Hrdom Hname;
apply (f_equal (fun x => ({[rname]} ∪ x))) in Hrdom;
rewrite -(dom_insert_L _ _ rval) in Hrdom;
iInsert_core (<[rname:=rval]> m') Hmap rtail Hrdom
end
end
end.
Ltac iInsert0 Hmap rnames :=
lazymatch goal with
| |- envs_entails ?H _ =>
lazymatch pm_eval (envs_lookup Hmap H) with
| Some (_, ?X) =>
lazymatch X with
| ([∗ map] _↦_ ∈ ?m', _)%I =>
let Hrdom := fresh "Hrdom" in
get_map_dom m' as Hrdom;
iInsert_core m' Hmap rnames Hrdom;
clear Hrdom;
map_simpl Hmap
end
end
end.
Tactic Notation "iInsert" constr(Hmap) constr(rname):=
iInsert0 Hmap [rname].
Tactic Notation "iInsertList" constr(Hmap) constr(rnames):=
iInsert0 Hmap rnames.
Set Default Proof Mode "Classic".
From iris.proofmode Require Import reduction proofmode.
From iris.proofmode Require Import environments.
From cap_machine Require Import stdpp_extra rules_base map_simpl.
Section denote_domain.
Variable K: Type.
Hypothesis HeqdecK: EqDecision K.
Hypothesis HcountK: Countable K.
(* if map_simpl is called first, the below will not contain overhead *)
Fixpoint denote_domain {A : Type} (rm: @rgmap A) (fm: nat -> option K) (mdom : gset K): gset K :=
match rm with
| Ins k a rm =>
match fm k with
| Some k => {[k]} ∪ denote_domain rm fm mdom
| None => denote_domain rm fm mdom end
| Del k rm =>
match fm k with
| Some k => denote_domain rm fm mdom ∖ {[k]}
| None => denote_domain rm fm mdom end
| Symb => mdom
end.
Local Arguments denote {_ _ _ _} _ _ _.
Lemma denote_domain_correct {A : Type} (rm: @rgmap A) (fm: nat -> option K) (m : gmap K A) (mdom : gset K) : dom m = mdom → dom (denote rm fm m) = denote_domain rm fm mdom.
intro Hmdom.
induction rm; cbn [denote denote_domain].
- case_eq (fm k); intros; set_solver + IHrm.
- case_eq (fm k); intros; set_solver + IHrm.
- done.
Unshelve. Fail idtac. Admitted.
End denote_domain.
Arguments denote_domain {_ _ _ _} _ _ _.
Arguments denote {_ _ _ _} _ _ _.
Ltac2 get_map_dom0 k a m hdom :=
let (x', m, fm) := (reify_helper k a m []) in
let env := make_list fm in
assert ($hdom := denote_domain_correct $k _ _ $x' (fun n => @list_lookup _ n $env) $m _ ltac:(first [ assumption | set_solver+]) );
rewrite ?dom_empty_L in $hdom;
cbn [denote denote_domain list_lookup lookup] in $hdom.
Ltac get_map_dom0 k a m hdom :=
let f := ltac2:(k a m hdom |- get_map_dom0 (Option.get (Ltac1.to_constr k)) (Option.get (Ltac1.to_constr a)) (Option.get (Ltac1.to_constr m)) (Option.get (Ltac1.to_ident hdom))) in f k a m ident:(hdom).
(* generate a domain hypothesis for a given gmap *)
Tactic Notation "get_map_dom" constr(m) "as" ident(hdom) :=
match type of m with
| ?t => match eval compute in t with (* type will not compute for very large maps *)
| gmap ?K ?A => let hdom' := fresh "hdom" in get_map_dom0 K A m ident:(hdom'); rename hdom' into hdom end end.
(* solving goals with map domains faster than set_solver *)
Tactic Notation "solve_map_dom" :=
let Hdom := fresh "Hdom" in
match goal with | |- dom ?m = ?dom => get_map_dom m as Hdom; rewrite Hdom; clear Hdom; set_solver+ end.
(* try to find concrete value in gmap *)
Ltac solve_lookup_some :=
repeat (
lazymatch goal with
| |- (<[ ?reg := ?w ]> ?rmap) !! ?reg = Some _ =>
rewrite lookup_insert; reflexivity
| |- (<[ ?reg := ?w ]> ?rmap) !! ?reg' = Some _ =>
rewrite lookup_insert_ne; [ | solve [auto]]
| |- (delete ?reg ?rmap) !! ?reg' = Some _ =>
rewrite lookup_delete_ne; [ | solve [auto]]
| |- _ !! ?reg = Some _ => exact
end ); fail.
Ltac extract_pointsto_map regs Hmap rname Hrdom Hreg :=
let rval := fresh "v"rname in
let Hsome := fresh "Hsome" in
first [ eassert (regs !! rname = Some _) as Hsome by solve_lookup_some (* Try to reuse existing value, if any *) |
assert (is_Some (regs !! rname)) as [rval Hsome] by (rewrite -elem_of_dom Hrdom; set_solver +) ];
let str_destr := constr:(("[" ++ Hreg ++ " " ++ Hmap ++ "]")%string) in
iDestruct (big_sepM_delete _ _ rname with Hmap) as str_destr; first exact Hsome; clear Hsome.
Ltac iExtract_core m' Hmap rnames Hregs Hrdom :=
match rnames with
| nil => idtac
| ?rname :: ?rtail =>
match Hregs with
| nil => idtac
| ?Hname :: ?Htail =>
extract_pointsto_map m' Hmap rname Hrdom Hname;
apply (f_equal (fun x => x ∖ {[rname]})) in Hrdom;
rewrite -dom_delete_L in Hrdom;
iExtract_core (delete rname m') Hmap rtail Htail Hrdom
end
end.
Ltac iExtract0 Hmap rnames Hregs :=
lazymatch goal with
| |- envs_entails ?H _ =>
lazymatch pm_eval (envs_lookup Hmap H) with
| Some (_, ?X) =>
lazymatch X with
| ([∗ map] _↦_ ∈ ?m', _)%I =>
let Hrdom := fresh "Hrdom" in
get_map_dom m' as Hrdom;
iExtract_core m' Hmap rnames Hregs Hrdom;
clear Hrdom;
map_simpl Hmap
end
end
end.
Tactic Notation "iExtract" constr(Hmap) constr(rname) "as" constr(Hreg):=
iExtract0 Hmap [rname] [Hreg].
Tactic Notation "iExtractList" constr(Hmap) constr(rnames) "as" constr(Hregs):=
iExtract0 Hmap rnames Hregs.
Ltac insert_pointsto_map regs Hmap rname Hrdom Hreg :=
let Hsome := fresh "Hsome" in
assert (regs !! rname = None) as Hsome by (rewrite -not_elem_of_dom Hrdom; set_solver +);
let str_destr := constr:(("[ $" ++ Hmap ++ " $" ++ Hreg ++ "]")%string) in
iDestruct (big_sepM_insert _ _ rname with str_destr) as Hmap; first exact Hsome; clear Hsome.
Ltac iInsert_core m' Hmap rnames Hrdom :=
match rnames with
| nil => idtac
| ?rname :: ?rtail =>
match goal with |- context [ Esnoc _ (INamed ?Hname) ?mtch ] =>
lazymatch mtch with | context [(rname ↦ᵣ ?rval)%I] =>
insert_pointsto_map m' Hmap rname Hrdom Hname;
apply (f_equal (fun x => ({[rname]} ∪ x))) in Hrdom;
rewrite -(dom_insert_L _ _ rval) in Hrdom;
iInsert_core (<[rname:=rval]> m') Hmap rtail Hrdom
end
end
end.
Ltac iInsert0 Hmap rnames :=
lazymatch goal with
| |- envs_entails ?H _ =>
lazymatch pm_eval (envs_lookup Hmap H) with
| Some (_, ?X) =>
lazymatch X with
| ([∗ map] _↦_ ∈ ?m', _)%I =>
let Hrdom := fresh "Hrdom" in
get_map_dom m' as Hrdom;
iInsert_core m' Hmap rnames Hrdom;
clear Hrdom;
map_simpl Hmap
end
end
end.
Tactic Notation "iInsert" constr(Hmap) constr(rname):=
iInsert0 Hmap [rname].
Tactic Notation "iInsertList" constr(Hmap) constr(rnames):=
iInsert0 Hmap rnames.