spec_patterns.v 3.52 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
Record spec_goal := SpecGoal {
5
  spec_goal_modal : bool;
6
  spec_goal_negate : bool;
7
  spec_goal_frame : list string;
8
9
  spec_goal_hyps : list string
}.
10

Robbert Krebbers's avatar
Robbert Krebbers committed
11
Inductive spec_pat :=
12
  | SGoal : spec_goal  spec_pat
13
14
  | SGoalPersistent : spec_pat
  | SGoalPure : spec_pat
15
  | SName : string  spec_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
21
22
23
24

Module spec_pat.
Inductive token :=
  | TName : string  token
  | TMinus : token
  | TBracketL : token
  | TBracketR : token
  | TPersistent : token
  | TPure : token
25
  | TModal : token
26
  | TFrame : token.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
29
30
31
32
33
34
35
36
37

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 (TMinus :: cons_name kn k) ""
  | 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 (TPersistent :: cons_name kn k) ""
  | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
38
  | String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
39
  | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
40
41
42
  | String a s =>
     if is_space a then tokenize_go s (cons_name kn k) ""
     else tokenize_go s k (String a kn)
43
  (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
  end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".

47
48
Inductive state :=
  | StTop : state
49
  | StAssert : spec_goal  state.
50

51
52
53
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
  match ts with
  | [] => Some (rev k)
54
  | TName s :: ts => parse_go ts (SName s :: k)
55
56
  | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
57
  | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
58
59
  | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
  | TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
60
61
  | _ => None
  end
62
63
with parse_goal (ts : list token) (g : spec_goal)
    (k : list spec_pat) : option (list spec_pat) :=
64
  match ts with
65
  | TMinus :: ts =>
66
     guard (¬spec_goal_negate g  spec_goal_frame g = []  spec_goal_hyps g = []);
67
     parse_goal ts (SpecGoal (spec_goal_modal g) true
68
       (spec_goal_frame g) (spec_goal_hyps g)) k
69
  | TName s :: ts =>
70
     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
71
72
       (spec_goal_frame g) (s :: spec_goal_hyps g)) k
  | TFrame :: TName s :: ts =>
73
     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
74
       (s :: spec_goal_frame g) (spec_goal_hyps g)) k
75
  | TBracketR :: ts =>
76
     parse_go ts (SGoal (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
77
       (reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
78
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
  end.
Definition parse (s : string) : option (list spec_pat) :=
81
  parse_go (tokenize s) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96

Ltac parse s :=
  lazymatch type of s with
  | list spec_pat => s
  | string => lazymatch eval vm_compute in (parse s) with
              | Some ?pats => pats | _ => fail "invalid list spec_pat" s
              end
  end.
Ltac parse_one s :=
  lazymatch type of s with
  | spec_pat => s
  | string => lazymatch eval vm_compute in (parse s) with
              | Some [?pat] => pat | _ => fail "invalid spec_pat" s
              end
  end.
97
End spec_pat.