Commit f0582c61 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Support strong framing of the whole spatial context.

parent 95b3911c
Pipeline #3990 passed with stage
in 3 minutes and 44 seconds
......@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
Inductive sel_pat :=
| SelPure
| SelPersistent
| SelSpatial
| SelSpatial : bool sel_pat
| SelName : bool string sel_pat.
Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
......@@ -23,7 +23,8 @@ Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :
| TName s :: ts => parse_go ts (SelName false s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
| TAlways :: ts => parse_go ts (SelPersistent :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
| THat :: TSep :: ts => parse_go ts (SelSpatial true :: k)
| TSep :: ts => parse_go ts (SelSpatial false :: k)
| _ => None
end.
Definition parse (s : string) : option (list sel_pat) :=
......
......@@ -76,7 +76,7 @@ Ltac iElaborateSelPat pat tac :=
let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
go pat Δ' ((ESelName true <$> Hs') ++ Hs)
| SelSpatial :: ?pat =>
| SelSpatial _ :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
go pat Δ' ((ESelName false <$> Hs') ++ Hs)
......@@ -202,15 +202,15 @@ Local Ltac iFrameAnyPersistent :=
let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
end.
Local Ltac iFrameAnySpatial :=
Local Ltac iFrameAnySpatial strong :=
let rec go Hs :=
match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp true H; go Hs end in
match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp strong H; go Hs end in
match goal with
| |- of_envs ?Δ _ =>
let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
end.
Tactic Notation "iFrame" := iFrameAnySpatial.
Tactic Notation "iFrame" := iFrameAnySpatial false.
Tactic Notation "iFrame" "(" constr(t1) ")" :=
iFramePure t1.
......@@ -239,7 +239,7 @@ Tactic Notation "iFrame" constr(Hs) :=
| [] => idtac
| SelPure :: ?Hs => iFrameAnyPure; go Hs
| SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
| SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
| SelSpatial ?b :: ?Hs => iFrameAnySpatial b; go Hs
| SelName ?b ?H :: ?Hs => iFrameHyp b H; go Hs
end
in let Hs := sel_pat.parse Hs in go Hs.
......
Supports Markdown
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