Skip to content

Commit

Permalink
Merge pull request #1332 from cryspen/add-cons-name-gen-printer
Browse files Browse the repository at this point in the history
fix(engine/gen-printer): fixes #1294
  • Loading branch information
W95Psp authored Mar 5, 2025
2 parents 7a40e7c + f768e96 commit c26f582
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 9 deletions.
4 changes: 2 additions & 2 deletions engine/backends/coq/coq/coq_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -443,8 +443,8 @@ struct
string "Notation" ^^ space ^^ string "\"'" ^^ name#p ^^ string "'\""
^^ space ^^ string ":=" ^^ space ^^ ty#p ^^ dot

method item'_Type_struct ~super:_ ~name ~generics ~tuple_struct:_
~arguments =
method item'_Type_struct ~super:_ ~type_name:name ~constructor_name:_
~generics ~tuple_struct:_ ~arguments =
CoqNotation.record name#p generics#p [] (string "Type")
(braces
(nest 2
Expand Down
17 changes: 12 additions & 5 deletions engine/lib/generic_printer/generic_printer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -345,15 +345,18 @@ module Make (F : Features.T) = struct

method virtual item'_Type_struct
: super:item ->
name:concrete_ident lazy_doc ->
type_name:concrete_ident lazy_doc ->
constructor_name:concrete_ident lazy_doc ->
generics:generics lazy_doc ->
tuple_struct:bool ->
arguments:
(concrete_ident lazy_doc * ty lazy_doc * attr list lazy_doc) list ->
document
(** [item'_Type_struct ~super ~name ~generics ~tuple_struct ~arguments] prints the struct definition [struct name<generics> arguments]. `tuple_struct` says whether we are dealing with a tuple struct
(** [item'_Type_struct ~super ~type_name ~constructor_name ~generics ~tuple_struct ~arguments] prints the struct definition [struct name<generics> arguments]. `tuple_struct` says whether we are dealing with a tuple struct
(e.g. [struct Foo(T1, T2)]) or a named struct
(e.g. [struct Foo {field: T1, other: T2}])? *)
(e.g. [struct Foo {field: T1, other: T2}])?
`type_name` is the identifier of the type itself, while `constructor_name` is the identifier of the constructor of the struct. Depending on the naming policy, those can be rendered as the same name or not. *)

method virtual item'_Type_enum
: super:item ->
Expand Down Expand Up @@ -578,8 +581,12 @@ module Make (F : Features.T) = struct
attrs ))
variant#v.arguments
in
self#item'_Type_struct ~super ~name ~generics
~tuple_struct:(not variant#v.is_record)
let constructor_name =
self#_do_not_override_lazy_of_concrete_ident
AstPos_variant__name variant#v.name
in
self#item'_Type_struct ~super ~type_name:name ~constructor_name
~generics ~tuple_struct:(not variant#v.is_record)
~arguments:variant_arguments
| _ -> self#unreachable ()
else self#item'_Type_enum ~super ~name ~generics ~variants
Expand Down
4 changes: 2 additions & 2 deletions engine/lib/generic_printer/generic_printer_template.ml
Original file line number Diff line number Diff line change
Expand Up @@ -238,8 +238,8 @@ struct
method item'_Type_enum ~super:_ ~name:_ ~generics:_ ~variants:_ =
default_document_for "item'_Type_enum"

method item'_Type_struct ~super:_ ~name:_ ~generics:_ ~tuple_struct:_
~arguments:_ =
method item'_Type_struct ~super:_ ~type_name:_ ~constructor_name:_
~generics:_ ~tuple_struct:_ ~arguments:_ =
default_document_for "item'_Type_struct"

method item'_Use ~super:_ ~path:_ ~is_external:_ ~rename:_ =
Expand Down

0 comments on commit c26f582

Please sign in to comment.