Commit 4e597ea3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename constructors of intro pattern stack_items (used in the parser).

This is to avoid confusion with those of selection patterns.
parent b1270b7d
...@@ -24,25 +24,25 @@ Inductive intro_pat := ...@@ -24,25 +24,25 @@ Inductive intro_pat :=
Module intro_pat. Module intro_pat.
Inductive stack_item := Inductive stack_item :=
| SPat : intro_pat stack_item | StPat : intro_pat stack_item
| SList : stack_item | StList : stack_item
| SConjList : stack_item | StConjList : stack_item
| SBar : stack_item | StBar : stack_item
| SAmp : stack_item | StAmp : stack_item
| SAlwaysElim : stack_item | StAlwaysElim : stack_item
| SModalElim : stack_item. | StModalElim : 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
| SList :: k => Some (SPat (IList (ps :: pss)) :: k) | StList :: k => Some (StPat (IList (ps :: pss)) :: k)
| SPat pat :: k => close_list k (pat :: ps) pss | StPat pat :: k => close_list k (pat :: ps) pss
| SAlwaysElim :: k => | StAlwaysElim :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss ''(p,ps) maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
| SModalElim :: k => | StModalElim :: k =>
''(p,ps) maybe2 (::) ps; close_list k (IModalElim p :: ps) pss ''(p,ps) maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| SBar :: k => close_list k [] (ps :: pss) | StBar :: k => close_list k [] (ps :: pss)
| _ => None | _ => None
end. end.
...@@ -57,55 +57,55 @@ Fixpoint big_conj (ps : list intro_pat) : intro_pat := ...@@ -57,55 +57,55 @@ 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
| SConjList :: k => | StConjList :: 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)
end; end;
Some (SPat (big_conj ps) :: k) Some (StPat (big_conj ps) :: k)
| SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps | StPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
| SAlwaysElim :: k => p cur; close_conj_list k (Some (IAlwaysElim p)) ps | StAlwaysElim :: k => p cur; close_conj_list k (Some (IAlwaysElim p)) ps
| SModalElim :: k => p cur; close_conj_list k (Some (IModalElim p)) ps | StModalElim :: k => p cur; close_conj_list k (Some (IModalElim p)) ps
| SAmp :: k => p cur; close_conj_list k None (p :: ps) | StAmp :: k => p cur; close_conj_list k None (p :: ps)
| _ => None | _ => None
end. end.
Fixpoint parse_go (ts : list token) (k : stack) : option stack := Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
match ts with match ts with
| [] => Some k | [] => Some k
| TName "_" :: ts => parse_go ts (SPat IDrop :: k) | TName "_" :: ts => parse_go ts (StPat IDrop :: k)
| TName s :: ts => parse_go ts (SPat (IIdent s) :: k) | TName s :: ts => parse_go ts (StPat (IIdent s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k) | TAnom :: ts => parse_go ts (StPat IAnom :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k) | TFrame :: ts => parse_go ts (StPat IFrame :: k)
| TBracketL :: ts => parse_go ts (SList :: k) | TBracketL :: ts => parse_go ts (StList :: k)
| TBar :: ts => parse_go ts (SBar :: k) | TBar :: ts => parse_go ts (StBar :: k)
| TBracketR :: ts => close_list k [] [] = parse_go ts | TBracketR :: ts => close_list k [] [] = parse_go ts
| TParenL :: ts => parse_go ts (SConjList :: k) | TParenL :: ts => parse_go ts (StConjList :: k)
| TAmp :: ts => parse_go ts (SAmp :: k) | TAmp :: ts => parse_go ts (StAmp :: k)
| TParenR :: ts => close_conj_list k None [] = parse_go ts | TParenR :: ts => close_conj_list k None [] = parse_go ts
| TPure :: ts => parse_go ts (SPat IPureElim :: k) | TPure :: ts => parse_go ts (StPat IPureElim :: k)
| TAlways :: ts => parse_go ts (SAlwaysElim :: k) | TAlways :: ts => parse_go ts (StAlwaysElim :: k)
| TModal :: ts => parse_go ts (SModalElim :: k) | TModal :: ts => parse_go ts (StModalElim :: k)
| TArrow d :: ts => parse_go ts (SPat (IRewrite d) :: k) | TArrow d :: ts => parse_go ts (StPat (IRewrite d) :: k)
| TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k) | TPureIntro :: ts => parse_go ts (StPat IPureIntro :: k)
| TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k) | TAlwaysIntro :: ts => parse_go ts (StPat IAlwaysIntro :: k)
| TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k) | TModalIntro :: ts => parse_go ts (StPat IModalIntro :: k)
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k) | TSimpl :: ts => parse_go ts (StPat ISimpl :: k)
| TDone :: ts => parse_go ts (SPat IDone :: k) | TDone :: ts => parse_go ts (StPat IDone :: k)
| TAll :: ts => parse_go ts (SPat IAll :: k) | TAll :: ts => parse_go ts (StPat IAll :: k)
| TForall :: ts => parse_go ts (SPat IForall :: k) | TForall :: ts => parse_go ts (StPat IForall :: k)
| TBraceL :: ts => parse_clear ts k | TBraceL :: ts => parse_clear ts k
| _ => None | _ => None
end end
with parse_clear (ts : list token) (k : stack) : option stack := with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with match ts with
| TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelIdent s)) :: k) | TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k) | TFrame :: TPure :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k) | TFrame :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelPersistent) :: k)
| TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k) | TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
| TName s :: ts => parse_clear ts (SPat (IClear (SelIdent s)) :: k) | TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k) | TPure :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
| TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k) | TAlways :: ts => parse_clear ts (StPat (IClear SelPersistent) :: k)
| TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k) | TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
| TBraceR :: ts => parse_go ts k | TBraceR :: ts => parse_go ts k
| _ => None | _ => None
end. end.
...@@ -113,9 +113,9 @@ with parse_clear (ts : list token) (k : stack) : option stack := ...@@ -113,9 +113,9 @@ with parse_clear (ts : list token) (k : stack) : option stack :=
Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) := Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match k with match k with
| [] => Some ps | [] => Some ps
| SPat pat :: k => close k (pat :: ps) | StPat pat :: k => close k (pat :: ps)
| SAlwaysElim :: k => ''(p,ps) maybe2 (::) ps; close k (IAlwaysElim p :: ps) | StAlwaysElim :: k => ''(p,ps) maybe2 (::) ps; close k (IAlwaysElim p :: ps)
| SModalElim :: k => ''(p,ps) maybe2 (::) ps; close k (IModalElim p :: ps) | StModalElim :: k => ''(p,ps) maybe2 (::) ps; close k (IModalElim p :: ps)
| _ => None | _ => None
end. end.
......
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