intro_patterns.v 5.93 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

Inductive intro_pat :=
  | IName : string  intro_pat
  | IAnom : intro_pat
8
  | IDrop : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  | IFrame : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  | IList : list (list intro_pat)  intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
  | IPureElim : intro_pat
  | IAlwaysElim : intro_pat  intro_pat
13
  | IModalElim : intro_pat  intro_pat
14
  | IRewrite : direction  intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
  | IPureIntro : intro_pat
  | IAlwaysIntro : intro_pat
17
  | IModalIntro : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
18
  | ISimpl : intro_pat
19
  | IDone : intro_pat
20
21
  | IForall : intro_pat
  | IAll : intro_pat
22
23
  | IClear : sel_pat  intro_pat
  | IClearFrame : sel_pat  intro_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
27
28
29
30

Module intro_pat.
Inductive stack_item :=
  | SPat : intro_pat  stack_item
  | SList : stack_item
  | SConjList : stack_item
  | SBar : stack_item
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
  | SAmp : stack_item
  | SAlwaysElim : stack_item
33
  | SModalElim : stack_item.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
39
40
Notation stack := (list stack_item).

Fixpoint close_list (k : stack)
    (ps : list intro_pat) (pss : list (list intro_pat)) : option stack :=
  match k with
  | SList :: k => Some (SPat (IList (ps :: pss)) :: k)
  | SPat pat :: k => close_list k (pat :: ps) pss
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
  | SAlwaysElim :: k =>
     '(p,ps)  maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
43
44
  | SModalElim :: k =>
     '(p,ps)  maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  | SBar :: k => close_list k [] (ps :: pss)
46
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
  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
  | SConjList :: k =>
     ps  match cur with
          | None => guard (ps = []); Some [] | Some p => Some (p :: ps)
          end;
     Some (SPat (big_conj ps) :: k)
  | SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  | SAlwaysElim :: k => p  cur; close_conj_list k (Some (IAlwaysElim p)) ps
67
  | SModalElim :: k => p  cur; close_conj_list k (Some (IModalElim p)) ps
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  | SAmp :: k => p  cur; close_conj_list k None (p :: ps)
69
70
71
  | _ => None
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
  match ts with
  | [] => Some k
75
  | TName "_" :: ts => parse_go ts (SPat IDrop :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
  | TName s :: ts => parse_go ts (SPat (IName s) :: k)
  | TAnom :: ts => parse_go ts (SPat IAnom :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  | TFrame :: ts => parse_go ts (SPat IFrame :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81
82
83
84
  | TBracketL :: ts => parse_go ts (SList :: k)
  | TBar :: ts => parse_go ts (SBar :: k)
  | TBracketR :: ts => close_list k [] [] = parse_go ts
  | TParenL :: ts => parse_go ts (SConjList :: k)
  | TAmp :: ts => parse_go ts (SAmp :: k)
  | TParenR :: ts => close_conj_list k None [] = parse_go ts
85
86
87
  | TPure :: ts => parse_go ts (SPat IPureElim :: k)
  | TAlways :: ts => parse_go ts (SAlwaysElim :: k)
  | TModal :: ts => parse_go ts (SModalElim :: k)
88
  | TArrow d :: ts => parse_go ts (SPat (IRewrite d) :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
  | TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
  | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
91
  | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
93
  | TDone :: ts => parse_go ts (SPat IDone :: k)
94
95
  | TAll :: ts => parse_go ts (SPat IAll :: k)
  | TForall :: ts => parse_go ts (SPat IForall :: k)
96
  | TBraceL :: ts => parse_clear ts k
97
98
  | _ => None
  end
99
with parse_clear (ts : list token) (k : stack) : option stack :=
100
  match ts with
101
102
103
104
105
106
107
108
  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
  | TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
  | TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
  | TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
  | TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
  | TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
  | TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
  | TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
109
  | TBraceR :: ts => parse_go ts k
110
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  end.
112

113
114
115
116
117
118
Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
  match k with
  | [] => Some ps
  | SPat pat :: k => close k (pat :: ps)
  | SAlwaysElim :: k => '(p,ps)  maybe2 (::) ps; close k (IAlwaysElim p :: ps)
  | SModalElim :: k => '(p,ps)  maybe2 (::) ps; close k (IModalElim p :: ps)
Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
121
  | _ => None
  end.

122
123
124
Definition parse (s : string) : option (list intro_pat) :=
  k  parse_go (tokenize s) []; close k [].

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

Fixpoint intro_pat_persistent (p : intro_pat) :=
  match p with
  | IPureElim => true
  | IAlwaysElim _ => true
  | IList pps => forallb (forallb intro_pat_persistent) pps
155
156
157
  | ISimpl => true
  | IClear _ => true
  | IClearFrame _ => true
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
161
162
163
  | _ => false
  end.

Ltac intro_pat_persistent p :=
  lazymatch type of p with
  | intro_pat => eval cbv in (intro_pat_persistent p)
164
  | list intro_pat => eval cbv in (forallb intro_pat_persistent p)
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  | string =>
166
167
168
169
     let pat := intro_pat.parse p in
     eval cbv in (forallb intro_pat_persistent pat)
  | bool => p
  | ?X => fail "intro_pat_persistent:" p "has unexpected type" X
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  end.