Make sure origins are renamed in bundles.

cryspen · Feb 4, 2025 · 8f355b8 · 8f355b8
1 parent 8381810
commit 8f355b8
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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