spec_patterns.v 3.78 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp 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
16
  | SForall : spec_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

18
19
20
Definition spec_pat_modal (p : spec_pat) : bool :=
  match p with SGoal g => spec_goal_modal g | _ => false end.

Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
27
28
Module spec_pat.
Inductive token :=
  | TName : string  token
  | TMinus : token
  | TBracketL : token
  | TBracketR : token
  | TPersistent : token
  | TPure : token
29
  | TForall : token
30
  | TModal : token
31
  | TFrame : token.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
34
35
36
37
38
39
40
41
42

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

53
54
Inductive state :=
  | StTop : state
55
  | StAssert : spec_goal  state.
56

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

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