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

3 4
Inductive spec_goal_kind := GoalStd | GoalPvs.

Robbert Krebbers's avatar
Robbert Krebbers committed
5
Inductive spec_pat :=
6
  | SGoal : spec_goal_kind  bool  list string  spec_pat
7 8 9
  | SGoalPersistent : spec_pat
  | SGoalPure : spec_pat
  | SName : bool  string  spec_pat (* first arg = persistent *)
10
  | SForall : spec_pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15 16 17 18 19

Module spec_pat.
Inductive token :=
  | TName : string  token
  | TMinus : token
  | TBracketL : token
  | TBracketR : token
  | TPersistent : token
  | TPure : token
20 21
  | TForall : token
  | TPvs : token.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24 25 26 27 28 29 30 31 32 33

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 (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) ""
34
  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
35 36
  | String "|" (String "=" (String "=" (String ">" s))) =>
     tokenize_go s (TPvs :: cons_name kn k) ""
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38 39 40
  | String a s => tokenize_go s k (String a kn)
  end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".

41 42
Inductive state :=
  | StTop : state
43
  | StAssert : spec_goal_kind  bool  list string  state.
44 45

Fixpoint parse_go (ts : list token) (s : state)
Robbert Krebbers's avatar
Robbert Krebbers committed
46
    (k : list spec_pat) : option (list spec_pat) :=
47 48
  match s with
  | StTop =>
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50
     match ts with
     | [] => Some (rev k)
51 52 53
     | TName s :: ts => parse_go ts StTop (SName false s :: k)
     | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
     | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
54 55 56
     | TBracketL :: ts => parse_go ts (StAssert GoalStd false []) k
     | TPvs :: TBracketL :: ts => parse_go ts (StAssert GoalPvs false []) k
     | TPvs :: ts => parse_go ts StTop (SGoal GoalPvs true [] :: k)
57 58
     | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
     | TForall :: ts => parse_go ts StTop (SForall :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60
     | _ => None
     end
61
  | StAssert kind neg ss =>
Robbert Krebbers's avatar
Robbert Krebbers committed
62
     match ts with
63 64 65
     | TMinus :: ts => guard (¬neg  ss = []); parse_go ts (StAssert kind true ss) k
     | TName s :: ts => parse_go ts (StAssert kind neg (s :: ss)) k
     | TBracketR :: ts => parse_go ts StTop (SGoal kind neg (rev ss) :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68 69
     | _ => None
     end
  end.
Definition parse (s : string) : option (list spec_pat) :=
70
  parse_go (tokenize s) StTop [].
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.