Merge pull request #1206 from hacspec/fix-visitors-quote

fix(engine) Make sub-parts of `Quote` visited by visitors
hacspec · Jan 6, 2025 · ffcd803 · ffcd803
2 parents b2f930b + ba1fcc1
commit ffcd803
Show file tree

Hide file tree

Showing 11 changed files with 45 additions and 64 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -692,10 +692,10 @@ struct
   and pquote span { contents; _ } =
     List.map
       ~f:(function
-        | `Verbatim code -> code
-        | `Expr e -> pexpr e |> term_to_string
-        | `Pat p -> ppat p |> pat_to_string
-        | `Typ p -> pty span p |> term_to_string)
+        | Verbatim code -> code
+        | Expr e -> pexpr e |> term_to_string
+        | Pattern p -> ppat p |> pat_to_string
+        | Typ p -> pty span p |> term_to_string)
       contents
     |> String.concat
 

diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
@@ -328,12 +328,13 @@ functor
               interleaved with Rust code *)
 
     and expr = { e : expr'; span : span; typ : ty }
+    and quote = { contents : quote_content list; witness : F.quote }
 
-    and quote = {
-      contents :
-        [ `Verbatim of string | `Expr of expr | `Pat of pat | `Typ of ty ] list;
-      witness : F.quote;
-    }
+    and quote_content =
+      | Verbatim of string
+      | Expr of expr
+      | Pattern of pat
+      | Typ of ty
 
     and supported_monads =
       | MException of ty

diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml b/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml
@@ -234,10 +234,10 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
         method quote { contents; _ } =
           List.map
             ~f:(function
-              | `Verbatim code -> string code
-              | `Expr e -> print#expr_at Expr_Quote e
-              | `Pat p -> print#pat_at Expr_Quote p
-              | `Typ p -> print#ty_at Expr_Quote p)
+              | Verbatim code -> string code
+              | Expr e -> print#expr_at Expr_Quote e
+              | Pattern p -> print#pat_at Expr_Quote p
+              | Typ p -> print#ty_at Expr_Quote p)
             contents
           |> concat
 

diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
@@ -231,15 +231,13 @@ module Make (F : Features.T) = struct
       [local] is true, otherwise it prints the full path, separated by
       `module_path_separator`. *)
 
-      method quote (quote : quote) : document =
-        List.map
-          ~f:(function
-            | `Verbatim code -> string code
-            | `Expr e -> self#print_expr AstPosition_Quote e
-            | `Pat p -> self#print_pat AstPosition_Quote p
-            | `Typ p -> self#print_ty AstPosition_Quote p)
-          quote.contents
-        |> concat
+      method quote ~contents ~witness:_ : document =
+        List.map ~f:(fun doc -> doc#p) contents |> concat
+
+      method quote_content_Verbatim v = string v
+      method quote_content_Expr e = e#p
+      method quote_content_Pattern p = p#p
+      method quote_content_Typ t = t#p
 
       (** {2:specialize-expr Specialized printers for [expr]} *)
 
@@ -629,10 +627,6 @@ module Make (F : Features.T) = struct
                   ^ "]"))
           ast_position id
 
-      method _do_not_override_lazy_of_quote ast_position (value : quote)
-          : quote lazy_doc =
-        lazy_doc (fun (value : quote) -> self#quote value) ast_position value
-
       method! _do_not_override_lazy_of_item ast_position (value : item)
           : item lazy_doc =
         let module View = (val concrete_ident_view) in

diff --git a/engine/lib/generic_printer/generic_printer_template.ml b/engine/lib/generic_printer/generic_printer_template.ml
@@ -35,6 +35,11 @@ struct
       method borrow_kind_Mut _x1 = default_document_for "borrow_kind_Mut"
       method borrow_kind_Shared = default_document_for "borrow_kind_Shared"
       method borrow_kind_Unique = default_document_for "borrow_kind_Unique"
+      method cf_kind_BreakOnly = default_document_for "cf_kind_BreakOnly"
+
+      method cf_kind_BreakOrReturn =
+        default_document_for "cf_kind_BreakOrReturn"
+
       method common_array _x1 = default_document_for "common_array"
 
       method dyn_trait_goal ~trait:_ ~non_self_args:_ =
@@ -124,10 +129,6 @@ struct
       method expr'_Return ~super:_ ~e:_ ~witness:_ =
         default_document_for "expr'_Return"
 
-      method cf_kind_BreakOrReturn =
-        default_document_for "cf_kind_BreakOrReturn"
-
-      method cf_kind_BreakOnly = default_document_for "cf_kind_BreakOnly"
       method field_pat ~field:_ ~pat:_ = default_document_for "field_pat"
 
       method generic_constraint_GCLifetime _x1 _x2 =

diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml
@@ -2,7 +2,6 @@ open! Prelude
 open! Ast
 
 module%inlined_contents Make (F : Features.T) = struct
-  open Ast
   module FA = F
 
   module FB = struct
@@ -96,7 +95,7 @@ module%inlined_contents Make (F : Features.T) = struct
                 Error.assertion_failure span
                   "Malformed call to 'inline': cannot find string payload."
           in
-          let code =
+          let code : B.quote_content list =
             List.map bindings ~f:(fun (pat, e) ->
                 match
                   UB.Expect.pbinding_simple pat
@@ -112,7 +111,7 @@ module%inlined_contents Make (F : Features.T) = struct
                                 this may be a bug in the quote macros in \
                                 hax-lib.")
                     in
-                    `Expr { e with e = GlobalVar id }
+                    B.Expr { e with e = GlobalVar id }
                 | Some "_pat" ->
                     let pat =
                       extract_pattern e
@@ -121,7 +120,7 @@ module%inlined_contents Make (F : Features.T) = struct
                                "Could not extract pattern (case pat): this may \
                                 be a bug in the quote macros in hax-lib.")
                     in
-                    `Pat pat
+                    Pattern pat
                 | Some "_ty" ->
                     let typ =
                       match pat.typ with
@@ -134,33 +133,22 @@ module%inlined_contents Make (F : Features.T) = struct
                             "Malformed call to 'inline': expected type \
                              `Option<_>`."
                     in
-                    `Typ typ
-                | _ -> `Expr e)
+                    Typ typ
+                | _ -> Expr e)
           in
           let verbatim = split_str ~on:"SPLIT_QUOTE" str in
           let contents =
-            let rec f verbatim
-                (code :
-                  [ `Verbatim of string
-                  | `Expr of B.expr
-                  | `Pat of B.pat
-                  | `Typ of B.ty ]
-                  list) =
+            let rec f verbatim (code : B.quote_content list) =
               match (verbatim, code) with
-              | s :: s', code :: code' -> `Verbatim s :: code :: f s' code'
-              | [ s ], [] -> [ `Verbatim s ]
+              | s :: s', code :: code' -> B.Verbatim s :: code :: f s' code'
+              | [ s ], [] -> [ Verbatim s ]
               | [], [] -> []
               | _ ->
                   Error.assertion_failure span
                   @@ "Malformed call to 'inline'." ^ "\nverbatim="
                   ^ [%show: string list] verbatim
                   ^ "\ncode="
-                  ^ [%show:
-                      [ `Verbatim of string
-                      | `Expr of B.expr
-                      | `Pat of B.pat
-                      | `Typ of B.ty ]
-                      list] code
+                  ^ [%show: B.quote_content list] code
             in
             f verbatim code
           in

diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml
@@ -235,10 +235,10 @@ module Raw = struct
     !"quote!("
     & List.map
         ~f:(function
-          | `Verbatim code -> !code
-          | `Expr e -> pexpr e
-          | `Pat p -> ppat p
-          | `Typ t -> pty span t)
+          | Verbatim code -> !code
+          | Expr e -> pexpr e
+          | Pattern p -> ppat p
+          | Typ t -> pty span t)
         quote.contents
       |> concat ~sep:!""
     & !")"

diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
@@ -305,10 +305,10 @@ struct
 
   and dquote (span : span) ({ contents; witness } : A.quote) : B.quote =
     let f = function
-      | `Verbatim code -> `Verbatim code
-      | `Expr e -> `Expr (dexpr e)
-      | `Pat p -> `Pat (dpat p)
-      | `Typ p -> `Typ (dty span p)
+      | A.Verbatim code -> B.Verbatim code
+      | Expr e -> Expr (dexpr e)
+      | Pattern p -> Pattern (dpat p)
+      | Typ p -> Typ (dty span p)
     in
     { contents = List.map ~f contents; witness = S.quote span witness }
 

diff --git a/engine/utils/generate_from_ast/codegen_printer.ml b/engine/utils/generate_from_ast/codegen_printer.ml
@@ -327,9 +327,7 @@ let mk datatypes =
   in
   let state =
     let names_with_doc = List.map ~f:(fun dt -> dt.name) datatypes in
-    let names_with_doc =
-      "quote" :: "concrete_ident" :: "local_ident" :: names_with_doc
-    in
+    let names_with_doc = "concrete_ident" :: "local_ident" :: names_with_doc in
     { names_with_doc }
   in
   let positions = ref [ "AstPos_Entrypoint"; "AstPos_NotApplicable" ] in

diff --git a/engine/utils/generate_from_ast/codegen_visitor.ml b/engine/utils/generate_from_ast/codegen_visitor.ml
@@ -230,7 +230,6 @@ let is_allowed_opaque name =
       "span";
       "string";
       "todo";
-      "quote";
       "float_kind";
       "int_kind";
       "item_quote_origin";

diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
@@ -660,7 +660,7 @@ let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
     (fun count i ->
         let count:u64 = count in
         let i:usize = i in
-        i <= Core.Slice.impl__len #v_T slice)
+        i <= Core.Slice.impl__len #v_T slice <: usize)
     count
     (fun count i ->
         let count:u64 = count in