bedrock.lang.cpp.syntax.name_notation.parser

(*
 * Copyright (C) BlueRock Security Inc. 2023-2024
 *
 * This software is distributed under the terms of the BedRock Open-Source License.
 * See the LICENSE-BedRock file in the repository root for details.
 *)
Require Import stdpp.prelude.
Require Import bedrock.prelude.base.
Require Import bedrock.prelude.bytestring.
Require Import bedrock.upoly.upoly.
Require Import bedrock.upoly.option.
Require Import bedrock.upoly.list.
Require Import bedrock.prelude.parsec.
Require Import bedrock.lang.cpp.syntax.core.
Require Import bedrock.lang.cpp.syntax.types.

Definition ident_char (b : Byte.byte) : bool :=
  let n := Byte.to_N b in
  bool_decide ((Reduce (Byte.to_N "a") ≤ n ≤ Reduce (Byte.to_N "z")) \/
               (Reduce (Byte.to_N "A") ≤ n ≤ Reduce (Byte.to_N "Z")) \/
               b = "_"%byte)%N.

Module parser.
  Import parsec.
  Import UPoly.

  #[local] Open Scope monad_scope.

  Section with_M.
    Context {Mbase : Type -> Type}.
    Context {RET : MRet Mbase} {FMAP : FMap Mbase} {AP : Ap Mbase} {MBIND : MBind Mbase}.

    Notation M := (parsec.M@{Set _ _ _ _ _ _ _ _} bs Mbase).

    Definition digit_char (b : Byte.byte) : bool :=
      bool_decide (Byte.to_N "0" ≤ Byte.to_N b ≤ Byte.to_N "9")%N.

    Definition ident : M bs :=
      let* f := char ident_char in
      (fun xs _ => BS.String f $ BS.parse xs)
        <$> star (char ident_char <|> digit)
        <*> not (charP (fun a => ident_char a || digit_char a)).

    Notation exact bs := (exact_bs bs).

    (* a maximal identifier *)
    Definition keyword_no_ws (b : bs) : M unit :=
      let* _ := exact b in
      let* _ := not $ char (fun a => ident_char a || digit_char a) in
      mret ().

    Definition keyword (b : bs) : M unit :=
      (fun _ _ _ => ()) <$> ws <*> keyword_no_ws b <*> ws.

    Definition punct_char (b : Byte.byte) : Prop :=
      let c : N := Byte.to_N b in
      (Reduce (Byte.to_N "!") <= c < Reduce (Byte.to_N "0"))%N \/
      (Reduce (Byte.to_N "9") < c < Reduce (Byte.to_N "A"))%N \/
      (Reduce (Byte.to_N "Z") < c < Reduce (Byte.to_N "a"))%N \/
      (Reduce (Byte.to_N "z") < c < 127)%N.

    Definition space_char (b : Byte.byte) : Prop :=
      let c : N := Byte.to_N b in
      c ∈ [9; 10; 11; 12; 13; 32]%N.

    (* TODO: ideally, i would like to say that this does not contain additional characters. *)
    Definition op_token (b : bs) : M unit :=
      let* _ := ws in
      let* _ := exact b in
      ws.

    Definition decimal : M N :=
      let make ls := fold_left (fun acc x => 10 * acc + x)%N ls 0%N in
      make <$> plus ((fun x => Byte.to_N x - Byte.to_N "0")%N <$> digit).

    Definition parse_qualifiers : M function_qualifiers.t :=
      let quals :=
        star (anyOf $ [const function_qualifiers.Nc <$> keyword "const";
                       const function_qualifiers.Nv <$> keyword "volatile";
                       const function_qualifiers.Nr <$> op_token "&&";
                       const function_qualifiers.Nl <$> op_token "&"]) in
      fold_right function_qualifiers.join function_qualifiers.N <$> quals.

    Definition basic_types {lang} : list (list bs * type' lang) :=
      let s_or_u_l (b : list bs) (s u : type' lang) :=
        [(b, s); ("signed" :: b, s); ("unsigned" :: b, u)]%bs
      in
      let s_or_u b := s_or_u_l [b] in
      [ (["bool"], Tbool)
      ; (["void"], Tvoid)
      ; (["char"], Tchar)
      ; (["unsigned"; "char"], Tuchar)
      ; (["signed"; "char"], Tschar)
      ; (["uint128_t"], Tuint128_t)
      ; (["int128_t"], Tint128_t) ]%bs ++
      s_or_u "int128"%bs Tint128_t Tuint128_t ++
      s_or_u "__int128"%bs Tint128_t Tuint128_t ++
      s_or_u_l ["short";"int"]%bs Tshort Tushort ++
      s_or_u "short"%bs Tshort Tushort ++
      s_or_u "int"%bs Tint Tuint ++
      s_or_u_l ["long";"long";"int"]%bs Tlonglong Tulonglong ++
      s_or_u_l ["long";"long"]%bs Tlonglong Tulonglong ++
      s_or_u_l ["long";"int"]%bs Tlong Tulong ++
      s_or_u "long"%bs Tlong Tulong ++
      [ (["unsigned"], Tuint)
      ; (["signed"], Tint)
      ; (["nullptr_t"], Tnullptr)
      ; (["float16"], Tfloat16)
      ; (["float128"], Tfloat128)
      ; (["float"], Tfloat)
      ; (["double"], Tdouble)
      ; (["long"; "double"], Tlongdouble) ]%bs.

    Fixpoint interleave {A} (p : A) (ls : list A) : list A :=
      match ls with
      | nil => p :: nil
      | l :: ls => p :: l :: interleave p ls
      end.

    #[local] Definition basic_type_otree {lang} :=
      Eval vm_compute in keyword_set.compile 1000 $ (fun '(x,y) => (interleave None (List.map Some x), y)) <$> @basic_types lang.

    Definition basic_type {lang} : M (type' lang) :=
      Eval red in
      match basic_type_otree as X return X = basic_type_otree -> _ with
      | None => fun pf => ltac:(exfalso; inversion pf)
      | Some o => fun _ =>
        let token x := match x with
                       | None => ws
                       | Some b => keyword_no_ws b
                       end in
        keyword_set.interp token o
      end eq_refl.

    Definition operators : list (bs * OverloadableOperator) :=
      (* this is used in an early commit manner, so longer operators
         need to come first
         TODO: list is incomplete
       *)
      [ ("~", OOTilde)
      ; ("<=>", OOSpaceship)
      ; ("!=", OOExclaimEqual)
      ; ("!", OOExclaim)
      ; ("++", OOPlusPlus)
      ; ("--", OOMinusMinus)
      ; ("&&", OOAmpAmp)
      ; ("||", OOPipePipe)
      ; ("==", OOEqualEqual)
      ; ("=", OOEqual)
      ; ("<<=", OOLessLessEqual)
      ; (">>=", OOGreaterGreaterEqual)
      ; ("<=", OOLessEqual)
      ; ("<<", OOLessLess)
      ; (">=", OOGreaterEqual)
      ; (">>", OOGreaterGreater)
      ; ("+=", OOPlusEqual)
      ; ("-=", OOMinusEqual)
      ; ("%=", OOPercentEqual)
      ; ("/=", OOSlashEqual)
      ; ("*=", OOStarEqual)
      ; ("&=", OOAmpEqual)
      ; ("|=", OOPipeEqual)
      ; ("^=", OOCaretEqual)
      ; ("->*", OOArrowStar)
      ; ("->", OOArrow)
      ; ("<", OOLess)
      ; (">", OOGreater)
      ; ("[]", OOSubscript)
      ; ("()", OOCall)
      ; ("new[]", OONew true)
      ; ("delete[]", OODelete true)
      ; ("new", OONew false)
      ; ("delete", OODelete false)
      ; ("co_await", OOCoawait)
      ; (",", OOComma)
      ; ("*", OOStar)
      ; ("+", OOPlus)
      ; ("-", OOMinus)
      ; ("/", OOSlash)
      ; ("%", OOPercent)
      ; ("&", OOAmp)
      ; ("^", OOCaret)
      ; ("|", OOPipe)
      ]%bs.

    Definition operator : M OverloadableOperator :=
      let* _ := ws in
      let* res := (anyOf $ (fun '(lex, syn) => const syn <$> exact lex) <$> operators) in
      let* _ := ws in
      mret res.

    Definition spaced (b : bs) : M unit :=
      let* _ := ws in
      let* _ := exact b in
      ws.

    Definition get_args {lang} (ls : list (type' lang)) : list (type' lang) :=
      match ls with
      | [Tvoid] => []
      | _ => ls
      end.

    Definition NEXT {T} (n : nat) (f : nat -> M T) : M T :=
      match n with
      | 0 => mfail
      | S n => f n
      end.

  End with_M.

  #[local] Definition M := (parsec.M bs (eta option)).

  #[local] Instance M_ret : MRet M := _.
  #[local] Instance M_map : FMap M := _.
  #[local] Instance M_ap : Ap M := _.
  #[local] Instance M_bind : MBind M := _.
  #[local] Instance M_alt : Alternative M := _.

  Definition run {T} (m : M T) (str : bs) : option (bs * T) :=
    match parsec.run_bs m str with
    | Some (Datatypes.Some (rest, result)) => Some (rest, result)
    | _ => None
    end.

  Definition run_full {T} (p : M T) (str : bs) : option T :=
    let m : M T := (fun x _ => x) <$> p <*> eos in
    fmap (M:=eta option) (fun '(_,b) => b) $ run m str.

  Notation exact bs := (exact_bs bs).

  Section with_lang.
    Context {lang : lang.t}.
    Notation type := (type' lang).
    Notation name := (name' lang).

    Variant name_type : Set :=
      | Simple (_ : bs)
      | Dtor (_ : bs)
      | FirstDecl (_ : bs)
      | FirstChild (_ : bs)
      | Anon (_ : N)
      | Op (_ : OverloadableOperator)
      | OpConv (_ : type)
      | OpLit (_ : bs).

    Section body.
      Variable parse_type : unit -> M type.
      Variable parse_name : unit -> M name.
      Variable parse_name_component : unit -> M (atomic_name' lang * option (list (temp_arg' lang))).
      Variable parse_expr : unit -> M (Expr' lang).

      Definition parse_args : M (list type * function_arity) :=
        let args := sepBy (spaced ",") (parse_type ()) in
        let arity :=
          let arity a :=
            match a with
            | None => Ar_Definite
            | Some _ => Ar_Variadic
            end
          in
          arity <$> optional ((fun _ _ => ()) <$> spaced "," <*> spaced "...")
        in
        quoted (spaced "(") (spaced ")") (pair <$> (get_args <$> args) <*> arity).

      Definition parse_postfix_type : M (type -> type) :=
        let entry :=
          let* _ := ws in
          (let* _ := exact "&&" in mret Trv_ref) <|>
            (let* _ := exact "&" in mret Tref) <|>
            (let* _ := exact "*" in mret Tptr) <|>
            (let* _ := keyword "const" in mret $ fun x => tqualified QC x) <|>
            (let* _ := keyword "volatile" in mret $ fun x => tqualified QV x) <|>
            (let* _ := spaced "[]" in
             mret (fun x => Tincomplete_array x)) <|>
            (let* _ := exact "[" in
             let* n := decimal in
             let* _ := exact "]" in
             mret (fun x => Tarray x n)) <|>
            (let* _ := exact "[" in
             let* n := parse_expr () in
             let* _ := exact "]" in
             mret (fun x => Tvariable_array x n)) <|>
            (let* _ := spaced "(" in
             let* _ := exact "*" in
             let* _ := spaced ")" in
             let* '(args, ar) := parse_args in
             mret (fun rt => Tptr $ Tfunction (FunctionType (ft_arity:=ar) rt args))) <|>
            (let* _ := spaced "(" in
             let* nm := parse_name () in
             let* _ := spaced "::" in
             let* _ := exact "*" in
             let* _ := spaced ")" in
             let* '(args, ar) := parse_args in
             mret (fun rt => Tmember_pointer (Tnamed nm) $ Tfunction (FunctionType (ft_arity:=ar) rt args)))
        in
        fold_left (fun t f => f t) <$> star entry.

    (* The core parsers are based on fuel to handle the mutual recursion *)
    Definition parse_type' : M type :=
      let* quals :=
        star (((fun _ => tqualified (lang:=lang) QC) <$> keyword "const") <|>
              ((fun _ => tqualified QV) <$> keyword "volatile"))
      in
      let* t :=
        basic_type <|>
        ((fun _ => Tparam) <$> exact "$" <*> ident) <|>
        ((fun _ => Tenum) <$> (exact "#" <|> spaced "enum") <*> parse_name ()) <|>
        ((fun _ => Tnamed) <$> optional (spaced "struct" <|> spaced "class") <*> parse_name ())
      in
      let* post := parse_postfix_type in
      mret $ post (List.fold_right (fun f x => f x) t quals).

   Definition parse_name': M name :=
     ((fun _ => Ndependent) <$> spaced "typename" <*> parse_type ()) <|>
     (let* (x : list (atomic_name' _ * _)) :=
        (fun _ x => x) <$> optional (spaced "::") <*> sepBy (spaced "::") (parse_name_component ())
      in
      match x with
      | nil => mfail (* unreachable *)
      | (nm, oinst) :: xs =>
          let sp oi :=
            match oi with
            | None => fun x => x
            | Some i => fun x => Ninst x i
            end
          in
          let* root :=
            (mret $ sp oinst $ Nglobal nm)
          in
          mret (List.fold_left (fun '(acc, last) '(nm, oinst) =>
                                  match nm with
                                  | Nfunction function_qualifiers.N (Nf fnm) args =>
                                      if bool_decide (Nid fnm = last) then
                                        (sp oinst (Nscoped acc $ Nfunction function_qualifiers.N Nctor args), nm)
                                      else
                                        (sp oinst (Nscoped acc nm), nm)
                                  | _ =>
                                      (sp oinst (Nscoped acc nm), nm)
                                  end) xs
            (root, nm)).1
      end).

    (* name components basically amount to atomic names with an optional template
       specialization after them. They are complex because function names include their
       arguments.
     *)
    Definition parse_name_component' : M (atomic_name' lang * option (list (temp_arg' lang))) :=
      let* (nm : name_type) :=
        let* op := optional (keyword "operator") in
        match op with
        | None => let* d := optional (op_token "~") in
                 match d with
                 | None =>
                     let* d := optional (exact "@") in
                     match d with
                     | None =>
                         let* d := optional (exact ".") in
                         match d with
                         | None => Simple <$> ident
                         | Some _ => FirstChild <$> ident
                         end
                     | Some _ => (Anon <$> decimal) <|> (FirstDecl <$> ident)
                     end
                 | Some _ => Dtor <$> ident
                 end
        | Some _ =>
            (Op <$> operator) <|>
            (OpConv <$> parse_type ()) <|>
            (const OpLit <$> exact """""_" <*> ident)
        end
      in
      let mk_atomic_name (nm : name_type) (args : option _) : M (atomic_name' _) :=
        match args with
        | None => match nm with
                 | Simple nm => mret $ Nid nm
                 | FirstDecl nm => mret $ Nfirst_decl nm
                 | FirstChild nm => mret $ Nfirst_child nm
                 | Anon n => mret $ Nanon n
                 | Dtor _
                 | Op _
                 | OpLit _
                 | OpConv _ => mfail
                 end
        | Some (args, ar, quals) =>
            (fun nm => Nfunction quals nm args) <$>
              match nm with
              | Dtor _ => mret $ Ndtor
              | Simple nm => mret $ Nf nm
              | Op oo => mret $ Nop oo
              | OpConv t => mret $ Nop_conv t
              | OpLit n => mret $ Nop_lit n
              | FirstDecl n => mfail
              | FirstChild n => mfail
              | Anon _ => mfail
              end
        end
      in
      let parse_args : M _ :=
        optional (let* '(args, arity) := parse_args in
                  let* quals := parse_qualifiers in
                  mret (args, arity, quals))
      in
      let* template_args :=
        let template_arg :=
          (Atype <$> parse_type ()) <|> (Avalue <$> parse_expr ()) in
        optional (quoted (spaced "<") (spaced ">") $ sepBy (op_token ",") template_arg) in
      let* nm := let* a := parse_args in mk_atomic_name nm a in
      mret (nm, template_args)
    .

    Definition parse_z : M Z :=
      let num sgn n :=
        match sgn with
        | None => Z.of_N n
        | Some _ => Z.opp $ Z.of_N n
        end
      in
      num <$> optional (op_token "-") <*> decimal.

    Definition parse_expr' : M (Expr' lang) :=
      let* _ := ws in
      let int_literal :=
        let* num := parse_z in
        let* suffix := optional (anyOf [(const Tlonglong <$> keyword "ll");
                                        (const Tlong <$> keyword "l");
                                        (const Tulonglong <$> keyword "ull");
                                        (const Tulong <$> keyword "ul");
                                        (const Tuint <$> keyword "u")]) in
        let ty :=
          match suffix with
          | None => Tint
          | Some ty => ty
          end
        in
        mret $ Eint num ty
      in
      let char_literal :=
        let* ty := optional (anyOf [(const Tchar8 <$> keyword "u8");
                                     (const Tchar16 <$> keyword "u");
                                     (const Tchar32 <$> keyword "U");
                                     (const Twchar <$> keyword "L")]) in
        let ty : type :=
          match ty with
          | None => Tchar
          | Some t => t
          end
        in
        let* _ := optional (exact "'") in
        mfail
      in
      let simple_literal :=
        anyOf [(const (Ebool true) <$> keyword "true");
                 (const (Ebool false) <$> keyword "false");
                 (const Enull <$> keyword "nullptr")]
      in
      let global :=
        (* NOTE: there is no way to get the type of the global here.
           To make this work, we need to remove this information from
           the expression. *)
        Eglobal <$> parse_name () <*> mfail
      in
      int_literal <|> char_literal <|> simple_literal <|> global.
    End body.

    Fixpoint parse_type (fuel : nat) :=
      parse_type' (fun _ => NEXT fuel parse_type) (fun _ => NEXT fuel parse_name) (fun _ => NEXT fuel parse_expr)
    with parse_name (fuel : nat) :=
      parse_name' (fun _ => NEXT fuel parse_type) (fun _ => NEXT fuel parse_name_component)
    with parse_name_component (fuel : nat) :=
      parse_name_component' (fun _ => NEXT fuel parse_type) (fun _ => NEXT fuel parse_expr)
    with parse_expr (fuel : nat) :=
      parse_expr' (fun _ => NEXT fuel parse_name).

  End with_lang.

End parser.

Definition parse_name (input : bs) : option name :=
  parser.run_full (parser.parse_name 1000) input.

Definition parse_type (input : bs) : option type :=
  parser.run_full (parser.parse_type 1000) input.

Module Type TESTS.
  #[local] Definition TEST (input : bs) (nm : name) : Prop :=
    (parse_name input) = Some nm.

  #[local] Definition Msg : name := Nglobal $ Nid "Msg".

  Succeed Example _0 : TEST "Msg" Msg := eq_refl.
  Succeed Example _0 : TEST "::Msg" Msg := eq_refl.
  Succeed Example _0 : TEST "Msg::@0" (Nscoped Msg (Nanon 0)) := eq_refl.
  Succeed Example _0 : TEST "Msg::Msg()" (Nscoped Msg (Nfunction function_qualifiers.N Nctor [])) := eq_refl.
  Succeed Example _0 : TEST "Msg::~Msg()" (Nscoped Msg (Nfunction function_qualifiers.N Ndtor [])) := eq_refl.
  Succeed Example _0 :
    let targs := Avalue <$> [Eint 1 Tulong;
                             Eint (-2) Tlong;
                             Eint 3 Tulonglong;
                             Eint (-4) Tlonglong;
                             Eint 5 Tuint;
                             Eint 6 Tint] in
    TEST "Msg<1ul, -2l, 3ull, -4ll, 5u, 6>::Msg()" (Nscoped (Ninst Msg targs) (Nfunction function_qualifiers.N Nctor [])) := eq_refl.
  Succeed Example _0 :
    let targs := Atype <$> [Tulong;
                            Tlong;
                            Tulonglong;
                            Tlonglong;
                            Tuint; Tint] in
    TEST "Msg<unsigned long, long, unsigned long long, long long, unsigned int, int>::Msg()" (Nscoped (Ninst Msg targs) (Nfunction function_qualifiers.N Nctor [])) := eq_refl.
  Succeed Example _0 : TEST "Msg::Msg(int)" (Nscoped Msg (Nfunction function_qualifiers.N Nctor [Tint])) := eq_refl.
  Succeed Example _0 : TEST "Msg::Msg(long)" (Nscoped Msg (Nfunction function_qualifiers.N Nctor [Tlong])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator=(const Msg&)" (Nscoped Msg (Nfunction function_qualifiers.N (Nop OOEqual) [Tref (Tconst (Tnamed $ Nglobal (Nid "Msg")))])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator=(const Msg&&)" (Nscoped Msg (Nfunction function_qualifiers.N (Nop OOEqual) [Trv_ref (Tconst (Tnamed $ Nglobal (Nid "Msg")))])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator new()" (Nscoped Msg (Nfunction function_qualifiers.N (Nop (OONew false)) [])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator new[]()" (Nscoped Msg (Nfunction function_qualifiers.N (Nop (OONew true)) [])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator delete()" (Nscoped Msg (Nfunction function_qualifiers.N (Nop (OODelete false)) [])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator delete[]()" (Nscoped Msg (Nfunction function_qualifiers.N (Nop (OODelete true)) [])) := eq_refl.
  Succeed Example _0 : TEST "Msg::operator int()" (Nscoped Msg (Nfunction function_qualifiers.N (Nop_conv Tint) [])) := eq_refl.
  Succeed Example _0 : TEST "foo_client(int[2]&, int const*, bool*, int**, char*)" (Nglobal (Nfunction function_qualifiers.N (Nf "foo_client") [Tref (Tarray Tint 2); Tptr (Tconst Tint); Tptr Tbool; Tptr (Tptr Tint); Tptr Tchar])) := eq_refl.
  Succeed Example _0 : TEST "DlistInternal::iterator::operator!=(const DlistInternal::iterator&) const"
                 (Nscoped (Nscoped (Nglobal (Nid "DlistInternal")) (Nid "iterator"))
                    (Nfunction function_qualifiers.Nc (Nop OOExclaimEqual) [Tref (Tqualified QC (Tnamed (Nscoped (Nglobal (Nid "DlistInternal")) (Nid "iterator"))))])) := eq_refl.
  Succeed Example _0 : TEST "intrusive::List_internal::iterator::iterator(intrusive::List_internal::Node*)"
                 (Nscoped (Nscoped (Nscoped (Nglobal (Nid "intrusive")) (Nid "List_internal")) (Nid "iterator"))
                    (Nfunction function_qualifiers.N Nctor [Tptr (Tnamed (Nscoped (Nscoped (Nglobal (Nid "intrusive")) (Nid "List_internal")) (Nid "Node")))])) := eq_refl.
  Succeed Example _0 : TEST "span<const int, 1ul>::span(const int*, unsigned long)"
                         (Nscoped (Ninst (Nglobal (Nid "span")) [Atype (Tqualified QC Tint);
                                                                 Avalue (Eint 1 Tulong)])
                            (Nfunction function_qualifiers.N Nctor [Tptr (Tqualified QC Tint); Tulong])) := eq_refl.
  Succeed Example _0 : TEST "integral" (Nglobal $ Nid "integral") := eq_refl.
  Succeed Example _0 : TEST "f<int>(int, int)" (Ninst (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tint; Tint]) [Atype Tint]) := eq_refl.
  Succeed Example _0 : TEST "f<int>(#e1, const #e2)" (Ninst (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tenum (Nglobal (Nid "e1")); Tconst $ Tenum (Nglobal (Nid "e2"))]) [Atype Tint]) := eq_refl.
  Succeed Example _0 : TEST "f(int[], int[3])" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tincomplete_array Tint; Tarray Tint 3]) := eq_refl.
  Succeed Example _0 : TEST "f(const volatile int[], int[3])" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tincomplete_array (Tqualified QCV Tint); Tarray Tint 3]) := eq_refl.
  Succeed Example _0 : TEST "f(void)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") []) := eq_refl.
  Succeed Example _0 : TEST "::f(void)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") []) := eq_refl.
  Succeed Example _0 : TEST "::f(#::foo)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tenum $ Nglobal $ Nid "foo"]) := eq_refl.

  Succeed Example _0 : TEST "operator """"_f(enum ::foo)" (Nglobal $ Nfunction function_qualifiers.N (Nop_lit "f") [Tenum $ Nglobal $ Nid "foo"]) := eq_refl.

  Succeed Example _0 : TEST "::f(enum ::foo)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tenum $ Nglobal $ Nid "foo"]) := eq_refl.
  Succeed Example _0 : TEST "::f(struct ::foo)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tnamed $ Nglobal $ Nid "foo"]) := eq_refl.
  Succeed Example _0 : TEST "::f(class ::foo)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tnamed $ Nglobal $ Nid "foo"]) := eq_refl.
  Succeed Example _0 : TEST "::f(::foo)" (Nglobal $ Nfunction function_qualifiers.N (Nf "f") [Tnamed $ Nglobal $ Nid "foo"]) := eq_refl.
  Succeed Example _0 : TEST "CpuSet::forall(void (*)(int)) const"
                 (Nscoped (Nglobal (Nid "CpuSet")) (Nfunction function_qualifiers.Nc (Nf "forall") [Tptr $ Tfunction (FunctionType Tvoid [Tint])])) := eq_refl.
  Succeed Example _0 : TEST "CpuSet::forall(void (C::*)(int)) const"
                         (Nscoped (Nglobal (Nid "CpuSet")) (Nfunction function_qualifiers.Nc (Nf "forall") [Tmember_pointer (Tnamed (Nglobal $ Nid "C")) $ Tfunction (FunctionType Tvoid [Tint])])) := eq_refl.

  Succeed Example _0 : TEST "CpuSet::forall(void (C::*)(int), ...) const"
                         (Nscoped (Nglobal (Nid "CpuSet")) (Nfunction function_qualifiers.Nc (Nf "forall") [Tmember_pointer (Tnamed (Nglobal $ Nid "C")) $ Tfunction (FunctionType Tvoid [Tint])])) := eq_refl.
  Succeed Example _0 : TEST "CpuSet::forall(void (C::*)(int, ...), ...) const"
                         (Nscoped (Nglobal (Nid "CpuSet")) (Nfunction function_qualifiers.Nc (Nf "forall") [Tmember_pointer (Tnamed (Nglobal $ Nid "C")) $ Tfunction (FunctionType (ft_arity:=Ar_Variadic) Tvoid [Tint])])) := eq_refl.

  Succeed Example _0 : TEST "foo(unsigned int128, int128)" (Nglobal (Nfunction function_qualifiers.N (Nf "foo") [Tuint128_t; Tint128_t])) := eq_refl.

  Succeed Example _0 : TEST "foo(unsigned, signed, char,unsigned char,signed char,short, short int, unsigned short, unsigned short int, signed short, signed short int, int, unsigned int, signed int, long, long int, unsigned long, unsigned long int, signed long, signed long int, long long, long long int, unsigned long long, unsigned long long int, signed long long, signed long long int)" (Nglobal (Nfunction function_qualifiers.N (Nf "foo") [Tuint;Tint;Tchar; Tuchar; Tschar; Tshort; Tshort; Tushort; Tushort; Tshort; Tshort; Tint; Tuint; Tint; Tlong; Tlong; Tulong; Tulong; Tlong; Tlong; Tlonglong; Tlonglong;Tulonglong;Tulonglong;Tlonglong;Tlonglong])) := eq_refl.

  (* NOTE: non-standard names *)
  Succeed Example _0 : TEST "Msg::@msg" (Nscoped Msg (Nfirst_decl "msg")) := eq_refl.
  Succeed Example _0 : TEST "Msg::.msg" (Nscoped Msg (Nfirst_child "msg")) := eq_refl.
  Succeed Example _0 : TEST "typename foo" (Ndependent (Tnamed (Nglobal (Nid "foo")))) := eq_refl.
  Succeed Example _0 : TEST "typename foo<int>::type"
                 (Ndependent (Tnamed (Nscoped (Ninst (Nglobal (Nid "foo")) [Atype Tint]) (Nid "type")))) := eq_refl.

  Succeed Example _0 : TEST "Msg<int& &&>" (Ninst (Nglobal (Nid "Msg")) [Atype (Trv_ref (Tref Tint))]) := eq_refl.

End TESTS.