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

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

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

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

36 37 38 39 40
Inductive state :=
  | StTop : state
  | StAssert : bool  list string  state.

Fixpoint parse_go (ts : list token) (s : state)
Robbert Krebbers's avatar
Robbert Krebbers committed
41
    (k : list spec_pat) : option (list spec_pat) :=
42 43
  match s with
  | StTop =>
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45
     match ts with
     | [] => Some (rev k)
46 47 48 49 50 51
     | 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)
     | TBracketL :: ts => parse_go ts (StAssert false []) k
     | 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
52 53
     | _ => None
     end
54
  | StAssert neg ss =>
Robbert Krebbers's avatar
Robbert Krebbers committed
55
     match ts with
56 57 58
     | TMinus :: ts => guard (¬neg  ss = []); parse_go ts (StAssert true ss) k
     | TName s :: ts => parse_go ts (StAssert neg (s :: ss)) k
     | TBracketR :: ts => parse_go ts StTop (SGoal neg (rev ss) :: k)
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61 62
     | _ => None
     end
  end.
Definition parse (s : string) : option (list spec_pat) :=
63
  parse_go (tokenize s) StTop [].
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78

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