Commit 6ca015ff authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify introduction pattern parser.

parent 16b514a8
...@@ -16,7 +16,8 @@ Inductive intro_pat := ...@@ -16,7 +16,8 @@ Inductive intro_pat :=
| ISimpl : intro_pat | ISimpl : intro_pat
| IForall : intro_pat | IForall : intro_pat
| IAll : intro_pat | IAll : intro_pat
| IClear : list (bool * string) intro_pat. (* true = frame, false = clear *) | IClear : string intro_pat
| IClearFrame : string intro_pat.
Module intro_pat. Module intro_pat.
Inductive token := Inductive token :=
...@@ -140,15 +141,14 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack := ...@@ -140,15 +141,14 @@ 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)
| TAll :: ts => parse_go ts (SPat IAll :: k) | TAll :: ts => parse_go ts (SPat IAll :: k)
| TForall :: ts => parse_go ts (SPat IForall :: k) | TForall :: ts => parse_go ts (SPat IForall :: k)
| TClearL :: ts => parse_clear ts [] k | TClearL :: ts => parse_clear ts k
| _ => None | _ => None
end end
with parse_clear (ts : list token) with parse_clear (ts : list token) (k : stack) : option stack :=
(ss : list (bool * string)) (k : stack) : option stack :=
match ts with match ts with
| TFrame :: TName s :: ts => parse_clear ts ((true,s) :: ss) k | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k)
| TName s :: ts => parse_clear ts ((false,s) :: ss) k | TName s :: ts => parse_clear ts (SPat (IClear s) :: k)
| TClearR :: ts => parse_go ts (SPat (IClear (reverse ss)) :: k) | TClearR :: ts => parse_go ts k
| _ => None | _ => None
end. end.
......
...@@ -780,13 +780,8 @@ Tactic Notation "iIntros" constr(pat) := ...@@ -780,13 +780,8 @@ Tactic Notation "iIntros" constr(pat) :=
| ISimpl :: ?pats => simpl; go pats | ISimpl :: ?pats => simpl; go pats
| IForall :: ?pats => repeat iIntroForall; go pats | IForall :: ?pats => repeat iIntroForall; go pats
| IAll :: ?pats => repeat (iIntroForall || iIntro); go pats | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
| IClear ?cpats :: ?pats => | IClear ?H :: ?pats => iClear H; go pats
let rec clr cpats := | IClearFrame ?H :: ?pats => iFrame H; go pats
match cpats with
| [] => go pats
| (false,?H) :: ?cpats => iClear H; clr cpats
| (true,?H) :: ?cpats => iFrame H; clr cpats
end in clr cpats
| IAlwaysElim ?pat :: ?pats => | IAlwaysElim ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
| ?pat :: ?pats => | ?pat :: ?pats =>
......
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