The `cpp.class` command

Usage

#[verbose, debug]
#[unsafe_learn_hint=local|export|global|none] (* Register unsafe learning hint? (default `global`) *)
cpp.class <matcher> [ prefix "prefix" ] from <translation-unit-name> <rep>
  [ { <class-attr> ; ... ; <class-attr> } ].

where

  <matcher> ::=
    "className"       (* E.g. `"Namespace::Foo"` *)
  | (<matcher-expr>)  (* E.g. `(name "Foo")` or `(exact "Foo")` *)

  <rep> ::=
    dataclass [ [ <dataclass-attr> ; ... ; <dataclass-attr> ] ]
  | rep <rep-name>

  <dataclass-attr> ::=
    no_register     (* Forget about any freshly synthesized model, rep *)
  | no_cfrac        (* Do not synthesize a `CFracSplittable` instance *)

  <class-attr> ::=  (* Additional specs to synthesize *)
    defaultable     (* default constructor *)
  | destructible    (* destructor *)
  | copyable        (* copy constructor, copy assignment *)
  | movable         (* move constructor, move assignment *)
  | default_specs   (* all supported default methods in the TU, and an abbreviation for the lot *)

Examples

We consider the C++ code

// dataclass_demo.hpp
namespace Test {
  class Base {
  public:
    int x{0};
    Base() = default;
  };

  class Client : public Base {
  public:
    int some_client_data{0};
    int other_client_data{0};
    bool client_has_feature_X{false};

    // ...
  };
};

Using prefix

Module Base.
  cpp.class "Test::Base"
    prefix ""
    from dataclass_demo_hpp.source
    dataclass[no_cfrac]
    { defaultable
    ; copyable
    ; movable }.
End Base.

generates, among many things,

• the model T
• the representation predicate R
• a default value of type T
• the specifications for constructors (including default and copy constructors), destructors, and copy assignment and move assignment operators
• various properties (but not CFracSplittable), learning hints and unfolding hints for R

As the generated definitions are put inside the Module Base with empty prefix, we can refer to them as, for example, Base.T and Base.R, and Base.default_ctor_spec.

Meanwhile,

cpp.class (exact "Test::Client")
  prefix "Base_"
  from dataclass_demo_hpp.source
  dataclass
  { default_specs }.

generates Base_T and Base_R and Base_default_ctor_spec, and so on. (exact "Test::Client") is a matcher expression.

Using dataclass

dataclass generates the model T as a Record, using the fields of the C++ class/struct, mapping primitives to their known Rocq types (e.g. int to Z) and internal classes/structs to the models registered with dataclass (e.g. those also generated by cpp.class). Meanwhile, the predicates R has type cQp.t -> T -> Rep.

For example, in

Module Base.
  cpp.class "Test::Base"
    prefix ""
    from dataclass_demo_hpp.source
    dataclass
    { defaultable
    ; copyable
    ; movable }.
End Base.

Module Client.
  cpp.class "Test::Client"
    prefix ""
    from dataclass_demo_hpp.source
    dataclass[no_register].
End Client.

Print Client.T. gives

Record T : Set := Build_T {
  Test_dot_Base : Base.T;
	some_client_data : Z;
  other_client_data : Z;
  client_has_feature_X : bool
} as record.

In Module Client, we use dataclass[no_register] to avoid registering the to-be-generated definitions with the dataclass database for known models.

Using existing handwritten model and predicate

Record MyModel : Set := mkMyModel { x : Z; client : Client.T }.

Definition I (m : MyModel) :=
  m.(client).(Client.some_client_data) = m.(client).(Client.other_client_data).

br.lock Definition Client_R `{Σ : cpp_logic, σ : genv} (q : cQp.t) (m : MyModel) : Rep :=
  pureR [| I m |] ** Client.R q m.(client).

cpp.class "Test::Client"
  from dataclass_demo_hpp.source
  rep Client_R
  { copyable
  ; movable }.

generates various hints and properites for Client_R, as well as specifications for copy/move contructors and assignment operators that use MyModel and Client_R. The generated definitions are prefixed by default with Test_Client_, for example, Test_Client_copy_ctor_spec and Test_Client_copy_assign_spec.

Using model and predicate generated by derive

Definition Base := CppKey dataclass_demo_hpp.source "Test::Base".
#[only(cpp_model,cpp_rep,default_ctor)] derive Base.

Definition Client := CppKey dataclass_demo_hpp.source "Test::Client".
#[only(cpp_model)] derive Client.
#[only(cpp_rep)] derive Client.
cpp.class (exact "Test::Client")
  prefix ""
  from dataclass_demo_hpp.source
  rep Client_R
  { defaultable
  ; copyable
  ; movable }.