Commit d3622918 authored by Robbert Krebbers's avatar Robbert Krebbers

Proofmode clear intro pattern {H1 ... H2} like ssreflect.

parent 1190a321
Pipeline #560 passed with stage
...@@ -4,20 +4,21 @@ Inductive intro_pat := ...@@ -4,20 +4,21 @@ Inductive intro_pat :=
| IName : string intro_pat | IName : string intro_pat
| IAnom : intro_pat | IAnom : intro_pat
| IAnomPure : intro_pat | IAnomPure : intro_pat
| IClear : intro_pat | IDrop : intro_pat
| IFrame : intro_pat | IFrame : intro_pat
| IPersistent : intro_pat intro_pat | IPersistent : intro_pat intro_pat
| IList : list (list intro_pat) intro_pat | IList : list (list intro_pat) intro_pat
| ISimpl : intro_pat | ISimpl : intro_pat
| IAlways : intro_pat | IAlways : intro_pat
| INext : intro_pat. | INext : intro_pat
| IClear : list string intro_pat.
Module intro_pat. Module intro_pat.
Inductive token := Inductive token :=
| TName : string token | TName : string token
| TAnom : token | TAnom : token
| TAnomPure : token | TAnomPure : token
| TClear : token | TDrop : token
| TFrame : token | TFrame : token
| TPersistent : token | TPersistent : token
| TBar : token | TBar : token
...@@ -28,7 +29,9 @@ Inductive token := ...@@ -28,7 +29,9 @@ Inductive token :=
| TParenR : token | TParenR : token
| TSimpl : token | TSimpl : token
| TAlways : token | TAlways : token
| TNext : token. | TNext : token
| TClearL : token
| TClearR : token.
Fixpoint cons_name (kn : string) (k : list token) : list token := Fixpoint cons_name (kn : string) (k : list token) : list token :=
match kn with "" => k | _ => TName (string_rev kn) :: k end. match kn with "" => k | _ => TName (string_rev kn) :: k end.
...@@ -38,7 +41,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token := ...@@ -38,7 +41,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String " " s => tokenize_go s (cons_name kn k) "" | String " " s => tokenize_go s (cons_name kn k) ""
| String "?" s => tokenize_go s (TAnom :: cons_name kn k) "" | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
| String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) "" | String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) ""
| String "_" s => tokenize_go s (TClear :: cons_name kn k) "" | String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
| String "$" s => tokenize_go s (TFrame :: cons_name kn k) "" | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) "" | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "[" s => tokenize_go s (TBracketL :: cons_name kn k) "" | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
...@@ -49,6 +52,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token := ...@@ -49,6 +52,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "&" s => tokenize_go s (TAmp :: cons_name kn k) "" | String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
| String "!" s => tokenize_go s (TAlways :: cons_name kn k) "" | String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
| String ">" s => tokenize_go s (TNext :: cons_name kn k) "" | String ">" s => tokenize_go s (TNext :: cons_name kn k) ""
| String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
| String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) "" | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn) | String a s => tokenize_go s k (String a kn)
end. end.
...@@ -60,19 +65,19 @@ Inductive stack_item := ...@@ -60,19 +65,19 @@ Inductive stack_item :=
| SList : stack_item | SList : stack_item
| SConjList : stack_item | SConjList : stack_item
| SBar : stack_item | SBar : stack_item
| SAmp : stack_item. | SAmp : stack_item
| SClear : stack_item.
Notation stack := (list stack_item). Notation stack := (list stack_item).
Fixpoint close_list (k : stack) Fixpoint close_list (k : stack)
(ps : list intro_pat) (pss : list (list intro_pat)) : option stack := (ps : list intro_pat) (pss : list (list intro_pat)) : option stack :=
match k with match k with
| [] => None
| SList :: k => Some (SPat (IList (ps :: pss)) :: k) | SList :: k => Some (SPat (IList (ps :: pss)) :: k)
| SPat pat :: k => close_list k (pat :: ps) pss | SPat pat :: k => close_list k (pat :: ps) pss
| SPersistent :: k => | SPersistent :: k =>
'(p,ps) maybe2 (::) ps; close_list k (IPersistent p :: ps) pss '(p,ps) maybe2 (::) ps; close_list k (IPersistent p :: ps) pss
| SBar :: k => close_list k [] (ps :: pss) | SBar :: k => close_list k [] (ps :: pss)
| (SAmp | SConjList) :: _ => None | _ => None
end. end.
Fixpoint big_conj (ps : list intro_pat) : intro_pat := Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
...@@ -86,7 +91,6 @@ Fixpoint big_conj (ps : list intro_pat) : intro_pat := ...@@ -86,7 +91,6 @@ Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
Fixpoint close_conj_list (k : stack) Fixpoint close_conj_list (k : stack)
(cur : option intro_pat) (ps : list intro_pat) : option stack := (cur : option intro_pat) (ps : list intro_pat) : option stack :=
match k with match k with
| [] => None
| SConjList :: k => | SConjList :: k =>
ps match cur with ps match cur with
| None => guard (ps = []); Some [] | Some p => Some (p :: ps) | None => guard (ps = []); Some [] | Some p => Some (p :: ps)
...@@ -95,7 +99,14 @@ Fixpoint close_conj_list (k : stack) ...@@ -95,7 +99,14 @@ Fixpoint close_conj_list (k : stack)
| SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps | SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
| SPersistent :: k => p cur; close_conj_list k (Some (IPersistent p)) ps | SPersistent :: k => p cur; close_conj_list k (Some (IPersistent p)) ps
| SAmp :: k => p cur; close_conj_list k None (p :: ps) | SAmp :: k => p cur; close_conj_list k None (p :: ps)
| (SBar | SList) :: _ => None | _ => None
end.
Fixpoint close_clear (k : stack) (ss : list string) : option stack :=
match k with
| SPat (IName s) :: k => close_clear k (s :: ss)
| SClear :: k => Some (SPat (IClear (reverse ss)) :: k)
| _ => None
end. end.
Fixpoint parse_go (ts : list token) (k : stack) : option stack := Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
...@@ -104,7 +115,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack := ...@@ -104,7 +115,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TName s :: ts => parse_go ts (SPat (IName s) :: k) | TName s :: ts => parse_go ts (SPat (IName s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k) | TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k) | TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k)
| TClear :: ts => parse_go ts (SPat IClear :: k) | TDrop :: ts => parse_go ts (SPat IDrop :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k) | TFrame :: ts => parse_go ts (SPat IFrame :: k)
| TPersistent :: ts => parse_go ts (SPersistent :: k) | TPersistent :: ts => parse_go ts (SPersistent :: k)
| TBracketL :: ts => parse_go ts (SList :: k) | TBracketL :: ts => parse_go ts (SList :: k)
...@@ -116,6 +127,8 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack := ...@@ -116,6 +127,8 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k) | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
| TAlways :: ts => parse_go ts (SPat IAlways :: k) | TAlways :: ts => parse_go ts (SPat IAlways :: k)
| TNext :: ts => parse_go ts (SPat INext :: k) | TNext :: ts => parse_go ts (SPat INext :: k)
| TClearL :: ts => parse_go ts (SClear :: k)
| TClearR :: ts => close_clear k [] = parse_go ts
end. end.
Definition parse (s : string) : option (list intro_pat) := Definition parse (s : string) : option (list intro_pat) :=
match k parse_go (tokenize s) [SList]; close_list k [] [] with match k parse_go (tokenize s) [SList]; close_list k [] [] with
......
...@@ -547,7 +547,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := ...@@ -547,7 +547,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
lazymatch pat with lazymatch pat with
| IAnom => idtac | IAnom => idtac
| IAnomPure => iPure Hz | IAnomPure => iPure Hz
| IClear => iClear Hz | IDrop => iClear Hz
| IFrame => iFrame Hz | IFrame => iFrame Hz
| IName ?y => iRename Hz into y | IName ?y => iRename Hz into y
| IPersistent ?pat => iPersistent Hz; go Hz pat | IPersistent ?pat => iPersistent Hz; go Hz pat
...@@ -695,6 +695,7 @@ Tactic Notation "iIntros" constr(pat) := ...@@ -695,6 +695,7 @@ Tactic Notation "iIntros" constr(pat) :=
| ISimpl :: ?pats => simpl; go pats | ISimpl :: ?pats => simpl; go pats
| IAlways :: ?pats => iAlways; go pats | IAlways :: ?pats => iAlways; go pats
| INext :: ?pats => iNext; go pats | INext :: ?pats => iNext; go pats
| IClear ?Hs :: ?pats => iClear Hs; go pats
| IPersistent (IName ?H) :: ?pats => iIntro #H; go pats | IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
| IName ?H :: ?pats => iIntro H; go pats | IName ?H :: ?pats => iIntro H; go pats
| IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
......
...@@ -13,7 +13,8 @@ Proof. ...@@ -13,7 +13,8 @@ Proof.
{ iLeft. by iNext. } { iLeft. by iNext. }
iRight. iRight.
iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)". iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)".
iRevert {a b} "Ha Hb". iIntros {b a} "Hb Ha". iDuplicate "Hc" as "foo".
iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
iAssert (uPred_ownM (a core a))%I as "[Ha #Hac]" with "[Ha]". iAssert (uPred_ownM (a core a))%I as "[Ha #Hac]" with "[Ha]".
{ by rewrite cmra_core_r. } { by rewrite cmra_core_r. }
iFrame "Ha Hac". iFrame "Ha Hac".
......
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