intro_patterns.v 6.59 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export strings.
2
From iris.proofmode Require Import base tokens sel_patterns.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5 6 7 8
Inductive gallina_ident :=
  | IGallinaNamed : string  gallina_ident
  | IGallinaAnon : gallina_ident.

Robbert Krebbers's avatar
Robbert Krebbers committed
9
Inductive intro_pat :=
10
  | IIdent : ident  intro_pat
11
  | IFresh : intro_pat
12
  | IDrop : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  | IFrame : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  | IList : list (list intro_pat)  intro_pat
15
  | IPure : gallina_ident  intro_pat
16
  | IIntuitionistic : intro_pat  intro_pat
17
  | ISpatial : intro_pat  intro_pat
18
  | IModalElim : intro_pat  intro_pat
19
  | IRewrite : direction  intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  | IPureIntro : intro_pat
21
  | IModalIntro : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  | ISimpl : intro_pat
23
  | IDone : intro_pat
24 25
  | IForall : intro_pat
  | IAll : intro_pat
26 27
  | IClear : sel_pat  intro_pat
  | IClearFrame : sel_pat  intro_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30

Module intro_pat.
Inductive stack_item :=
31 32 33 34 35
  | StPat : intro_pat  stack_item
  | StList : stack_item
  | StConjList : stack_item
  | StBar : stack_item
  | StAmp : stack_item
36
  | StIntuitionistic : stack_item
37
  | StSpatial : stack_item
38
  | StModalElim : stack_item.
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40 41 42 43
Notation stack := (list stack_item).

Fixpoint close_list (k : stack)
    (ps : list intro_pat) (pss : list (list intro_pat)) : option stack :=
  match k with
44 45
  | StList :: k => Some (StPat (IList (ps :: pss)) :: k)
  | StPat pat :: k => close_list k (pat :: ps) pss
46
  | StIntuitionistic :: k =>
47
     '(p,ps)  maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
48
  | StModalElim :: k =>
49
     '(p,ps)  maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
50
  | StBar :: k => close_list k [] (ps :: pss)
51
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54 55 56 57 58 59 60 61 62 63 64
  end.

Fixpoint big_conj (ps : list intro_pat) : intro_pat :=
  match ps with
  | [] => IList [[]]
  | [p] => IList [[ p ]]
  | [p1;p2] => IList [[ p1 ; p2 ]]
  | p :: ps => IList [[ p ; big_conj ps ]]
  end.

Fixpoint close_conj_list (k : stack)
    (cur : option intro_pat) (ps : list intro_pat) : option stack :=
  match k with
65
  | StConjList :: k =>
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68
     ps  match cur with
          | None => guard (ps = []); Some [] | Some p => Some (p :: ps)
          end;
69 70
     Some (StPat (big_conj ps) :: k)
  | StPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
71
  | StIntuitionistic :: k => p  cur; close_conj_list k (Some (IIntuitionistic p)) ps
72
  | StSpatial :: k => p  cur; close_conj_list k (Some (ISpatial p)) ps
73 74
  | StModalElim :: k => p  cur; close_conj_list k (Some (IModalElim p)) ps
  | StAmp :: k => p  cur; close_conj_list k None (p :: ps)
75 76 77
  | _ => None
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
78 79 80
Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
  match ts with
  | [] => Some k
81 82
  | TName "_" :: ts => parse_go ts (StPat IDrop :: k)
  | TName s :: ts => parse_go ts (StPat (IIdent s) :: k)
83
  | TAnon :: ts => parse_go ts (StPat IFresh :: k)
84 85 86
  | TFrame :: ts => parse_go ts (StPat IFrame :: k)
  | TBracketL :: ts => parse_go ts (StList :: k)
  | TBar :: ts => parse_go ts (StBar :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  | TBracketR :: ts => close_list k [] [] = parse_go ts
88 89
  | TParenL :: ts => parse_go ts (StConjList :: k)
  | TAmp :: ts => parse_go ts (StAmp :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  | TParenR :: ts => close_conj_list k None [] = parse_go ts
91 92
  | TPure (Some s) :: ts => parse_go ts (StPat (IPure (IGallinaNamed s)) :: k)
  | TPure None :: ts => parse_go ts (StPat (IPure IGallinaAnon) :: k)
93
  | TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
94
  | TMinus :: TIntuitionistic :: ts => parse_go ts (StSpatial :: k)
95 96 97
  | 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)
98
  | (TModalIntro | TIntuitionisticIntro) :: ts => parse_go ts (StPat IModalIntro :: k)
99 100 101 102
  | TSimpl :: ts => parse_go ts (StPat ISimpl :: k)
  | TDone :: ts => parse_go ts (StPat IDone :: k)
  | TAll :: ts => parse_go ts (StPat IAll :: k)
  | TForall :: ts => parse_go ts (StPat IForall :: k)
103
  | TBraceL :: ts => parse_clear ts k
104 105
  | _ => None
  end
106
with parse_clear (ts : list token) (k : stack) : option stack :=
107
  match ts with
108
  | TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
109
  | TFrame :: TPure None :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
110
  | TFrame :: TIntuitionistic :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
111 112
  | TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
  | TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
113
  | TPure None :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
114
  | TIntuitionistic :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
115
  | TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
116
  | TBraceR :: ts => parse_go ts k
117
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
118
  end.
119

120 121 122
Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
  match k with
  | [] => Some ps
123
  | StPat pat :: k => close k (pat :: ps)
124 125 126
  | StIntuitionistic :: k => '(p,ps)  maybe2 (::) ps; close k (IIntuitionistic p :: ps)
  | StSpatial :: k => '(p,ps)  maybe2 (::) ps; close k (ISpatial p :: ps)
  | StModalElim :: k => '(p,ps)  maybe2 (::) ps; close k (IModalElim p :: ps)
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129
  | _ => None
  end.

130 131 132
Definition parse (s : string) : option (list intro_pat) :=
  k  parse_go (tokenize s) []; close k [].

Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135
Ltac parse s :=
  lazymatch type of s with
  | list intro_pat => s
136
  | intro_pat => constr:([s])
137 138
  | list string =>
     lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
139
     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
140 141 142
     end
  | string =>
     lazymatch eval vm_compute in (parse s) with
143
     | Some ?pats => pats | _ => fail "intro_pat.parse: cannot parse" s
144
     end
145
  | ident => constr:([IIdent s])
146
  | ?X => fail "intro_pat.parse:" s "has unexpected type" X
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149 150
  end.
Ltac parse_one s :=
  lazymatch type of s with
  | intro_pat => s
151 152
  | string =>
     lazymatch eval vm_compute in (parse s) with
153
     | Some [?pat] => pat | _ => fail "intro_pat.parse_one: cannot parse" s
154
     end
155
  | ?X => fail "intro_pat.parse_one:" s "has unexpected type" X
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157
  end.
End intro_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
158

159
Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  match p with
161
  | IPure _ => true
162
  | IIntuitionistic _ => true
163
  | IList pps => forallb (forallb intro_pat_intuitionistic) pps
164 165 166
  | ISimpl => true
  | IClear _ => true
  | IClearFrame _ => true
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169
  | _ => false
  end.

170
Ltac intro_pat_intuitionistic p :=
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  lazymatch type of p with
172 173
  | intro_pat => eval cbv in (intro_pat_intuitionistic p)
  | list intro_pat => eval cbv in (forallb intro_pat_intuitionistic p)
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  | string =>
175
     let pat := intro_pat.parse p in
176
     eval cbv in (forallb intro_pat_intuitionistic pat)
177
  | ident => false
178
  | bool => p
179
  | ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  end.