intro_patterns.v 7 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.prelude Require Export strings.
2
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5 6

Inductive intro_pat :=
  | IName : string  intro_pat
  | IAnom : intro_pat
7
  | IDrop : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  | IFrame : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  | IList : list (list intro_pat)  intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11
  | IPureElim : intro_pat
  | IAlwaysElim : intro_pat  intro_pat
12
  | IModalElim : intro_pat  intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14
  | IPureIntro : intro_pat
  | IAlwaysIntro : intro_pat
15
  | IModalIntro : intro_pat
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  | ISimpl : intro_pat
17 18
  | IForall : intro_pat
  | IAll : intro_pat
19
  | IClear : list (bool * string)  intro_pat. (* true = frame, false = clear *)
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22 23 24

Module intro_pat.
Inductive token :=
  | TName : string  token
  | TAnom : token
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  | TFrame : token
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29 30 31
  | TBar : token
  | TBracketL : token
  | TBracketR : token
  | TAmp : token
  | TParenL : token
  | TParenR : token
Robbert Krebbers's avatar
Robbert Krebbers committed
32 33
  | TPureElim : token
  | TAlwaysElim : token
34
  | TModalElim : token
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36
  | TPureIntro : token
  | TAlwaysIntro : token
37
  | TModalIntro : token
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  | TSimpl : token
39
  | TForall : token
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42
  | TAll : token
  | TClearL : token
  | TClearR : token.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49

Fixpoint cons_name (kn : string) (k : list token) : list token :=
  match kn with "" => k | _ => TName (string_rev kn) :: k end.
Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
  match s with
  | "" => rev (cons_name kn k)
  | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55 56
  | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
  | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
  | String "|" s => tokenize_go s (TBar :: cons_name kn k) ""
  | String "(" s => tokenize_go s (TParenL :: cons_name kn k) ""
  | String ")" s => tokenize_go s (TParenR :: cons_name kn k) ""
  | String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
  | String "%" s => tokenize_go s (TPureElim :: cons_name kn k) ""
  | String "#" s => tokenize_go s (TAlwaysElim :: cons_name kn k) ""
59
  | String ">" s => tokenize_go s (TModalElim :: cons_name kn k) ""
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
  | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
  | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
62
  | String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_name kn k) ""
63 64
  | String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
  | String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
66 67
  | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
68 69 70
  | String a s =>
     if is_space a then tokenize_go s (cons_name kn k) ""
     else tokenize_go s k (String a kn)
71
  (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77 78 79
  end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".

Inductive stack_item :=
  | SPat : intro_pat  stack_item
  | SList : stack_item
  | SConjList : stack_item
  | SBar : stack_item
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81
  | SAmp : stack_item
  | SAlwaysElim : stack_item
82
  | SModalElim : stack_item.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88 89
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
90 91
  | SAlwaysElim :: k =>
     '(p,ps)  maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
92 93
  | SModalElim :: k =>
     '(p,ps)  maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  | SBar :: k => close_list k [] (ps :: pss)
95
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
  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
115
  | SAlwaysElim :: k => p  cur; close_conj_list k (Some (IAlwaysElim p)) ps
116
  | SModalElim :: k => p  cur; close_conj_list k (Some (IModalElim p)) ps
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  | SAmp :: k => p  cur; close_conj_list k None (p :: ps)
118 119 120
  | _ => None
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123
Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
  match ts with
  | [] => Some k
124
  | TName "_" :: ts => parse_go ts (SPat IDrop :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  | 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
127
  | TFrame :: ts => parse_go ts (SPat IFrame :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130 131 132 133
  | 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
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135
  | TPureElim :: ts => parse_go ts (SPat IPureElim :: k)
  | TAlwaysElim :: ts => parse_go ts (SAlwaysElim :: k)
136
  | TModalElim :: ts => parse_go ts (SModalElim :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
  | TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
  | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
139
  | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
141 142
  | TAll :: ts => parse_go ts (SPat IAll :: k)
  | TForall :: ts => parse_go ts (SPat IForall :: k)
143 144 145 146 147 148 149 150 151 152
  | TClearL :: ts => parse_clear ts [] k
  | _ => None
  end
with parse_clear (ts : list token)
    (ss : list (bool * string)) (k : stack) : option stack :=
  match ts with
  | TFrame :: TName s :: ts => parse_clear ts ((true,s) :: ss) k
  | TName s :: ts => parse_clear ts ((false,s) :: ss) k
  | TClearR :: ts => parse_go ts (SPat (IClear (reverse ss)) :: k)
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  end.
154

Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158 159 160 161 162 163
Definition parse (s : string) : option (list intro_pat) :=
  match k  parse_go (tokenize s) [SList]; close_list k [] [] with
  | Some [SPat (IList [ps])] => Some ps
  | _ => None
  end.

Ltac parse s :=
  lazymatch type of s with
  | list intro_pat => s
164 165 166 167 168 169 170 171
  | 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
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174 175
  end.
Ltac parse_one s :=
  lazymatch type of s with
  | intro_pat => s
176 177 178 179
  | string =>
     lazymatch eval vm_compute in (parse s) with
     | Some [?pat] => pat | _ => fail "invalid intro_pat" s
     end
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181
  end.
End intro_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198

Fixpoint intro_pat_persistent (p : intro_pat) :=
  match p with
  | IPureElim => true
  | IAlwaysElim _ => true
  | IList pps => forallb (forallb intro_pat_persistent) pps
  | _ => false
  end.

Ltac intro_pat_persistent p :=
  lazymatch type of p with
  | intro_pat => eval cbv in (intro_pat_persistent p)
  | string =>
     let pat := intro_pat.parse_one p in
     eval cbv in (intro_pat_persistent pat)
  | _ => p
  end.