spec_patterns.v 3.64 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
From iris.prelude Require Export strings.

3
Record spec_goal := SpecGoal {
4
  spec_goal_modal : bool;
5
  spec_goal_negate : bool;
6
  spec_goal_frame : list string;
7
8
  spec_goal_hyps : list string
}.
9

Robbert Krebbers's avatar
Robbert Krebbers committed
10
Inductive spec_pat :=
11
  | SGoal : spec_goal  spec_pat
12
13
  | SGoalPersistent : spec_pat
  | SGoalPure : spec_pat
14
  | SName : string  spec_pat
15
  | SForall : 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
  | TForall : token
26
  | TModal : token
27
  | TFrame : token.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
33
34
35
36
37
38

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

49
50
Inductive state :=
  | StTop : state
51
  | StAssert : spec_goal  state.
52

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

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.
100
End spec_pat.