Commit 066b7f65 authored by Robbert Krebbers's avatar Robbert Krebbers

Make names of constructors of `intro_pat` consistent with names of `tac_` lemmas.

- Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic`
- Drop `IAlwaysIntro` (it's just `IModalIntro`).
parent 3b0457d4
......@@ -8,12 +8,11 @@ Inductive intro_pat :=
| IDrop : intro_pat
| IFrame : intro_pat
| IList : list (list intro_pat) intro_pat
| IPureElim : intro_pat
| IAlwaysElim : intro_pat intro_pat
| IPure : intro_pat
| IIntuitionistic : intro_pat intro_pat
| IModalElim : intro_pat intro_pat
| IRewrite : direction intro_pat
| IPureIntro : intro_pat
| IAlwaysIntro : intro_pat
| IModalIntro : intro_pat
| ISimpl : intro_pat
| IDone : intro_pat
......@@ -29,7 +28,7 @@ Inductive stack_item :=
| StConjList : stack_item
| StBar : stack_item
| StAmp : stack_item
| StAlwaysElim : stack_item
| StIntuitionistic : stack_item
| StModalElim : stack_item.
Notation stack := (list stack_item).
......@@ -38,8 +37,8 @@ Fixpoint close_list (k : stack)
match k with
| StList :: k => Some (StPat (IList (ps :: pss)) :: k)
| StPat pat :: k => close_list k (pat :: ps) pss
| StAlwaysElim :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
| StIntuitionistic :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
| StModalElim :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| StBar :: k => close_list k [] (ps :: pss)
......@@ -63,7 +62,7 @@ Fixpoint close_conj_list (k : stack)
end;
Some (StPat (big_conj ps) :: k)
| StPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
| StAlwaysElim :: k => p cur; close_conj_list k (Some (IAlwaysElim p)) ps
| StIntuitionistic :: k => p cur; close_conj_list k (Some (IIntuitionistic p)) ps
| StModalElim :: k => p cur; close_conj_list k (Some (IModalElim p)) ps
| StAmp :: k => p cur; close_conj_list k None (p :: ps)
| _ => None
......@@ -82,13 +81,12 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TParenL :: ts => parse_go ts (StConjList :: k)
| TAmp :: ts => parse_go ts (StAmp :: k)
| TParenR :: ts => close_conj_list k None [] = parse_go ts
| TPure :: ts => parse_go ts (StPat IPureElim :: k)
| TAlways :: ts => parse_go ts (StAlwaysElim :: k)
| TPure :: ts => parse_go ts (StPat IPure :: k)
| TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
| TModal :: ts => parse_go ts (StModalElim :: k)
| TArrow d :: ts => parse_go ts (StPat (IRewrite d) :: k)
| TPureIntro :: ts => parse_go ts (StPat IPureIntro :: k)
| TAlwaysIntro :: ts => parse_go ts (StPat IAlwaysIntro :: k)
| TModalIntro :: ts => parse_go ts (StPat IModalIntro :: k)
| (TModalIntro | TIntuitionisticIntro) :: ts => parse_go ts (StPat IModalIntro :: k)
| TSimpl :: ts => parse_go ts (StPat ISimpl :: k)
| TDone :: ts => parse_go ts (StPat IDone :: k)
| TAll :: ts => parse_go ts (StPat IAll :: k)
......@@ -100,11 +98,11 @@ with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
| TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
| TFrame :: TIntuitionistic :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
| TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
| TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
| TAlways :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
| TIntuitionistic :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
| TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
| TBraceR :: ts => parse_go ts k
| _ => None
......@@ -114,7 +112,7 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match k with
| [] => Some ps
| StPat pat :: k => close k (pat :: ps)
| StAlwaysElim :: k => ''(p,ps) maybe2 (::) ps; close k (IAlwaysElim p :: ps)
| StIntuitionistic :: k => ''(p,ps) maybe2 (::) ps; close k (IIntuitionistic p :: ps)
| StModalElim :: k => ''(p,ps) maybe2 (::) ps; close k (IModalElim p :: ps)
| _ => None
end.
......@@ -150,8 +148,8 @@ End intro_pat.
Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
match p with
| IPureElim => true
| IAlwaysElim _ => true
| IPure => true
| IIntuitionistic _ => true
| IList pps => forallb (forallb intro_pat_intuitionistic) pps
| ISimpl => true
| IClear _ => true
......
......@@ -1375,10 +1375,10 @@ Local Ltac iDestructHypGo Hz pat :=
| IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
| IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
| IPureElim => iPure Hz as ?
| IPure => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
| IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
| IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| _ => fail "iDestruct:" pat "invalid"
end.
......@@ -1473,13 +1473,12 @@ Ltac iIntros_go pats startproof :=
| false => idtac
end
(* Optimizations to avoid generating fresh names *)
| IPureElim :: ?pats => iIntro (?); iIntros_go pats startproof
| IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IPure :: ?pats => iIntro (?); iIntros_go pats startproof
| IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats => iIntro _; iIntros_go pats startproof
| IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof
(* Introduction patterns that can only occur at the top-level *)
| IPureIntro :: ?pats => iPureIntro; iIntros_go pats false
| IAlwaysIntro :: ?pats => iAlways; iIntros_go pats false
| IModalIntro :: ?pats => iModIntro; iIntros_go pats false
| IForall :: ?pats => repeat iIntroForall; iIntros_go pats startproof
| IAll :: ?pats => repeat (iIntroForall || iIntro); iIntros_go pats startproof
......@@ -1489,7 +1488,7 @@ Ltac iIntros_go pats startproof :=
| IClearFrame ?H :: ?pats => iFrame H; iIntros_go pats false
| IDone :: ?pats => try done; iIntros_go pats startproof
(* Introduction + destruct *)
| IAlwaysElim ?pat :: ?pats =>
| IIntuitionistic ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; iIntros_go pats false
| ?pat :: ?pats =>
let H := iFresh in iIntro H; iDestructHyp H as pat; iIntros_go pats false
......@@ -2092,7 +2091,7 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
fix_ihs ltac:(fun j =>
let IH' := eval vm_compute in
match j with 0%N => IH | _ => IH +:+ pretty j end in
iIntros [IAlwaysElim (IIdent IH')];
iIntros [IIntuitionistic (IIdent IH')];
let j := eval vm_compute in (1 + j)%N in
rev_tac j)
| _ => rev_tac 0%N
......
......@@ -21,7 +21,7 @@ Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SelIdent s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
| TAlways :: ts => parse_go ts (SelIntuitionistic :: k)
| TIntuitionistic :: ts => parse_go ts (SelIntuitionistic :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
| _ => None
end.
......
......@@ -54,7 +54,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
| TParenL :: TName s :: ts => parse_go ts (StIdent s :: k)
| TParenR :: ts => k close_ident k []; parse_go ts k
| TName s :: ts => parse_go ts (StPat (SIdent s []) :: k)
| TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
| TBracketL :: TIntuitionistic :: TFrame :: TBracketR :: ts =>
parse_go ts (StPat (SAutoFrame GIntuitionistic) :: k)
| TBracketL :: TFrame :: TBracketR :: ts =>
parse_go ts (StPat (SAutoFrame GSpatial) :: k)
......@@ -64,7 +64,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
parse_go ts (StPat (SPureGoal false) :: k)
| TBracketL :: TPure :: TDone :: TBracketR :: ts =>
parse_go ts (StPat (SPureGoal true) :: k)
| TBracketL :: TAlways :: ts => parse_goal ts GIntuitionistic false [] [] k
| TBracketL :: TIntuitionistic :: ts => parse_goal ts GIntuitionistic false [] [] k
| TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
| TBracketL :: ts => parse_goal ts GSpatial false [] [] k
| TForall :: ts => parse_go ts (StPat SForall :: k)
......
......@@ -15,10 +15,10 @@ Inductive token :=
| TBraceL : token
| TBraceR : token
| TPure : token
| TAlways : token
| TIntuitionistic : token
| TModal : token
| TPureIntro : token
| TAlwaysIntro : token
| TIntuitionisticIntro : token
| TModalIntro : token
| TSimpl : token
| TDone : token
......@@ -54,10 +54,10 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| String "{" s => tokenize_go s (TBraceL :: cons_state kn k) SNone
| String "}" s => tokenize_go s (TBraceR :: cons_state kn k) SNone
| String "%" s => tokenize_go s (TPure :: cons_state kn k) SNone
| String "#" s => tokenize_go s (TAlways :: cons_state kn k) SNone
| String "#" s => tokenize_go s (TIntuitionistic :: cons_state kn k) SNone
| String ">" s => tokenize_go s (TModal :: cons_state kn k) SNone
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_state kn k) SNone
| String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_state kn k) SNone
| String "!" (String "#" s) => tokenize_go s (TIntuitionisticIntro :: cons_state kn k) SNone
| String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_state kn k) SNone
| String "/" (String "/" (String "=" s)) =>
tokenize_go s (TSimpl :: TDone :: cons_state kn k) SNone
......
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