diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 88f135544..c152f34bc 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -521,6 +521,9 @@ struct ^^ string "Require Import" ^^ space ^^ string path_string ^^ dot ^^ break 1 ^^ string "Export" ^^ space ^^ string path_string ^^ dot + method item_quote_origin ~item_kind:_ ~item_ident:_ ~position:_ = + default_document_for "item_quote_origin" + method lhs_LhsArbitraryExpr ~e:_ ~witness = match witness with _ -> . method lhs_LhsArrayAccessor ~e:_ ~typ:_ ~index:_ ~witness = diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index dbdb24aae..68e550321 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -114,10 +114,13 @@ type item_kind = [@@deriving show, yojson, hash, compare, sexp, hash, eq] (** Describes the (shallow) kind of an item. *) +type item_quote_origin_position = [ `Before | `After | `Replace ] +[@@deriving show, yojson, hash, compare, sexp, hash, eq] + type item_quote_origin = { item_kind : item_kind; item_ident : concrete_ident; - position : [ `Before | `After | `Replace ]; + position : item_quote_origin_position; } [@@deriving show, yojson, hash, compare, sexp, hash, eq] (** From where does a quote item comes from? *) diff --git a/engine/lib/generic_printer/generic_printer_template.ml b/engine/lib/generic_printer/generic_printer_template.ml index 60c76d2a4..af2f5ce73 100644 --- a/engine/lib/generic_printer/generic_printer_template.ml +++ b/engine/lib/generic_printer/generic_printer_template.ml @@ -245,6 +245,9 @@ struct method item'_Use ~super:_ ~path:_ ~is_external:_ ~rename:_ = default_document_for "item'_Use" + method item_quote_origin ~item_kind:_ ~item_ident:_ ~position:_ = + default_document_for "item_quote_origin" + method lhs_LhsArbitraryExpr ~e:_ ~witness:_ = default_document_for "lhs_LhsArbitraryExpr" diff --git a/engine/utils/generate_from_ast/codegen_visitor.ml b/engine/utils/generate_from_ast/codegen_visitor.ml index 45034152e..afea4a868 100644 --- a/engine/utils/generate_from_ast/codegen_visitor.ml +++ b/engine/utils/generate_from_ast/codegen_visitor.ml @@ -232,7 +232,8 @@ let is_allowed_opaque name = "todo"; "float_kind"; "int_kind"; - "item_quote_origin"; + "item_quote_origin_position"; + "item_kind"; ] in List.mem ~equal:String.equal allowlist name diff --git a/engine/utils/generate_from_ast/generate_from_ast.ml b/engine/utils/generate_from_ast/generate_from_ast.ml index 7526afa76..ac2cbe562 100644 --- a/engine/utils/generate_from_ast/generate_from_ast.ml +++ b/engine/utils/generate_from_ast/generate_from_ast.ml @@ -13,7 +13,9 @@ let _main = (* We only look at certain types in the AST.ml module *) String.is_prefix ~prefix:"Make." path || List.mem ~equal:String.equal - [ "mutability"; "literal"; "attrs"; "quote" ] + [ + "mutability"; "literal"; "attrs"; "quote"; "item_quote_origin"; + ] path) |> List.map ~f:(fun (path, td) -> ( String.chop_prefix ~prefix:"Make." path