spec_patterns.v 2.55 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export strings.
2
From iris.proofmode Require Import tokens.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4

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

Robbert Krebbers's avatar
Robbert Krebbers committed
12
Inductive spec_pat :=
13
  | SGoal : spec_goal  spec_pat
14
15
  | SGoalPersistent : spec_pat
  | SGoalPure : spec_pat
16
  | SName : string  spec_pat
17
  | SForall : spec_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19
20
21
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
22
Module spec_pat.
23
24
Inductive state :=
  | StTop : state
25
  | StAssert : spec_goal  state.
26

27
28
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
  match ts with
29
  | [] => Some (reverse k)
30
  | TName s :: ts => parse_go ts (SName s :: k)
31
  | TBracketL :: TAlways :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
32
  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
33
  | TBracketL :: ts => parse_goal ts (SpecGoal false false [] []) k
34
35
  | TModal :: TBracketL :: ts => parse_goal ts (SpecGoal true false [] []) k
  | TModal :: ts => parse_go ts (SGoal (SpecGoal true true [] []) :: k)
36
37
38
  | TForall :: ts => parse_go ts (SForall :: k)
  | _ => None
  end
39
40
with parse_goal (ts : list token) (g : spec_goal)
    (k : list spec_pat) : option (list spec_pat) :=
41
  match ts with
42
  | TMinus :: ts =>
43
     guard (¬spec_goal_negate g  spec_goal_frame g = []  spec_goal_hyps g = []);
44
     parse_goal ts (SpecGoal (spec_goal_modal g) true
45
       (spec_goal_frame g) (spec_goal_hyps g)) k
46
  | TName s :: ts =>
47
     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
48
49
       (spec_goal_frame g) (s :: spec_goal_hyps g)) k
  | TFrame :: TName s :: ts =>
50
     parse_goal ts (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
51
       (s :: spec_goal_frame g) (spec_goal_hyps g)) k
52
  | TBracketR :: ts =>
53
     parse_go ts (SGoal (SpecGoal (spec_goal_modal g) (spec_goal_negate g)
54
       (reverse (spec_goal_frame g)) (reverse (spec_goal_hyps g))) :: k)
55
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
  end.
Definition parse (s : string) : option (list spec_pat) :=
58
  parse_go (tokenize s) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

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