sel_patterns.v 1.31 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
From iris.prelude Require Export strings.

Inductive sel_pat :=
  | SelPure
  | SelPersistent
  | SelSpatial
  | SelName : string  sel_pat.

Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
  match ps with
  | [] => false
  | SelPure :: ps => true
  | _ :: ps => sel_pat_pure ps
  end.

Module sel_pat.
Fixpoint cons_name (kn : string) (k : list sel_pat) : list sel_pat :=
  match kn with "" => k | _ => SelName (string_rev kn) :: k end.

Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat :=
  match s with
  | "" => rev (cons_name kn k)
  | String " " s => parse_go s (cons_name kn k) ""
  | String "%" s => parse_go s (SelPure :: cons_name kn k) ""
  | String "#" s => parse_go s (SelPersistent :: cons_name kn k) ""
  | String (Ascii.Ascii false true false false false true true true) (* unicode ★ *)
      (String (Ascii.Ascii false false false true true false false true)
      (String (Ascii.Ascii true false true false false false false true) s)) =>
     parse_go s (SelSpatial :: cons_name kn k) ""
  | String a s => parse_go s k (String a kn)
  end.
Definition parse (s : string) : list sel_pat := parse_go s [] "".

Ltac parse s :=
  lazymatch type of s with
  | list sel_pat => s
  | list string => eval vm_compute in (SelName <$> s)
  | string => eval vm_compute in (parse s)
  end.
End sel_pat.