spec_patterns.v 2.93 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
6
Inductive goal_kind := GSpatial | GModal | GPersistent.

7
Record spec_goal := SpecGoal {
8
  spec_goal_kind : goal_kind;
9
  spec_goal_negate : bool;
10
  spec_goal_frame : list string;
11
12
  spec_goal_hyps : list string;
  spec_goal_done : bool
13
}.
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15
Inductive spec_pat :=
16
  | SForall : spec_pat
17
  | SName : string  spec_pat
18
19
20
  | SPureGoal : bool  spec_pat
  | SGoal : spec_goal  spec_pat
  | SAutoFrame : goal_kind  spec_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22
23
Definition goal_kind_modal (k : goal_kind) : bool :=
  match k with GModal => true | _ => false end.
24
Definition spec_pat_modal (p : spec_pat) : bool :=
25
26
27
28
29
  match p with
  | SGoal g => goal_kind_modal (spec_goal_kind g)
  | SAutoFrame k => goal_kind_modal k
  | _ => false
  end.
30

Robbert Krebbers's avatar
Robbert Krebbers committed
31
Module spec_pat.
32
33
Inductive state :=
  | StTop : state
34
  | StAssert : spec_goal  state.
35

36
37
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
  match ts with
38
  | [] => Some (reverse k)
39
  | TName s :: ts => parse_go ts (SName s :: k)
40
41
42
43
  | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
     parse_go ts (SAutoFrame GPersistent :: k)
  | TBracketL :: TFrame :: TBracketR :: ts =>
     parse_go ts (SAutoFrame GSpatial :: k)
44
  | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
45
46
47
48
     parse_go ts (SAutoFrame GModal :: k)
  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
  | TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
  | TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
49
  | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
50
  | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
51
52
53
  | TForall :: ts => parse_go ts (SForall :: k)
  | _ => None
  end
54
55
with parse_goal (ts : list token)
    (ki : goal_kind) (neg : bool) (frame hyps : list string)
56
    (k : list spec_pat) : option (list spec_pat) :=
57
  match ts with
58
  | TMinus :: ts =>
59
60
61
62
63
64
     guard (¬neg  frame = []  hyps = []);
     parse_goal ts ki true frame hyps k
  | TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
  | TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
  | TDone :: TBracketR :: ts =>
     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
65
  | TBracketR :: ts =>
66
     parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false) :: k)
67
  | _ => None
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
  end.
Definition parse (s : string) : option (list spec_pat) :=
70
  parse_go (tokenize s) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85

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