Accept name quotes ``​`%`` in patterns

[W95Psp]

Hi,

This PR adds a rule to the parser and adds a node PatVQuote to the surface AST so that ​`%foo is now a legal pattern.

PatVQuote nodes are desugared similarly to VQuote ones. The pattern ​`%foo where foo is a name declared in a module X.Y.Z is desugared into the constant string pattern "X.Y.Z.foo".

Motivation for this PR

While working with attributes, I found this to be particularly nice when interpreting a term as one of the various constructors of an inductive, for instance:

open FStar.Tactics
open FStar.List.Tot
open FStar.Option

let const_int_of_term (t: term): option int
= match inspect_ln t with
| Tv_Const (C_Int x) -> Some x
| _                  -> None

type foo = | Foo | Bar: int -> foo

let term_to_maybe_foo (t: term): option foo
= let head, args = collect_app t in
  let? head = match inspect_ln head with 
            | Tv_UInst v _ | Tv_FVar v 
                -> Some (implode_qn (inspect_fv v))
            | _ -> None in
    match head, args with
  | `%Foo,     [] -> Some Foo
  | `%Bar, [n, _] -> let? n = const_int_of_term n in
                    Some (Bar n)
  | _          -> None

let _ = assert_norm (
term_to_maybe_foo (`(Bar 3)) == Some (Bar 3)
/\ term_to_maybe_foo (`Foo)     == Some Foo
)

// now I can extract a `foo` from the attributes of a binder
let attributes_of_binder (bd: binder): list term // helper
= let _, (_, attrs) = inspect_binder bd in attrs
let foo_of_binder_attrs (bd: binder): option foo
= tryPick term_to_maybe_foo (attributes_of_binder bd)