more principled generic printer

engine/backends/coq/coq/coq_backend.ml

@@ -215,16 +215,16 @@ struct
         C.AST.Ident var.name
     | POr { subpats } -> C.AST.DisjunctivePat (List.map ~f:ppat subpats)
     | PArray _ -> __TODO_pat__ p.span "Parray?"
-    | PConstruct { name = `TupleCons 0; args = []; _ } -> C.AST.UnitPat
-    | PConstruct { name = `TupleCons 1; args = [ _ ]; _ } ->
+    | PConstruct { constructor = `TupleCons 0; fields = []; _ } -> C.AST.UnitPat
+    | PConstruct { constructor = `TupleCons 1; fields = [ _ ]; _ } ->
         __TODO_pat__ p.span "tuple 1"
-    | PConstruct { name = `TupleCons _n; args; _ } ->
-        C.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) args)
-    | PConstruct { name; args; is_record = true; _ } ->
-        C.AST.RecordPat (pglobal_ident name, pfield_pats args)
-    | PConstruct { name; args; is_record = false; _ } ->
+    | PConstruct { constructor = `TupleCons _n; fields; _ } ->
+        C.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) fields)
+    | PConstruct { constructor; fields; is_record = true; _ } ->
+        C.AST.RecordPat (pglobal_ident constructor, pfield_pats fields)
+    | PConstruct { constructor; fields; is_record = false; _ } ->
         C.AST.ConstructorPat
-          (pglobal_ident name, List.map ~f:(fun p -> ppat p.pat) args)
+          (pglobal_ident constructor, List.map ~f:(fun p -> ppat p.pat) fields)
     | PConstant { lit } -> C.AST.Lit (pliteral p.span lit)
     | _ -> .
 
@@ -582,7 +582,7 @@ struct
     | Impl { generics; self_ty; of_trait = name, gen_vals; items } ->
         [
           C.AST.Instance
-            ( pglobal_ident name,
+            ( pconcrete_ident name,
               List.map ~f:(pgeneric_param_as_argument span) generics.params,
               pty span self_ty,
               args_ty span gen_vals,
@@ -694,6 +694,7 @@ let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
              path = mod_name ^ ".v";
              contents =
                hardcoded_coq_headers ^ "\n" ^ string_of_items items ^ "\n";
+             sourcemap = None;
            })
 
 open Phase_utils

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -792,25 +792,26 @@ struct
         SSP.AST.Ident (plocal_ident var) (* TODO Mutable binding ! *)
     | POr { subpats } -> SSP.AST.DisjunctivePat (List.map ~f:ppat subpats)
     | PArray _ -> __TODO_pat__ p.span "Parray?"
-    | PConstruct { name = `TupleCons 0; args = []; _ } ->
+    | PConstruct { constructor = `TupleCons 0; fields = []; _ } ->
         SSP.AST.WildPat (* UnitPat *)
-    | PConstruct { name = `TupleCons 1; args = [ _ ]; _ } ->
+    | PConstruct { constructor = `TupleCons 1; fields = [ _ ]; _ } ->
         __TODO_pat__ p.span "tuple 1"
-    | PConstruct { name = `TupleCons _n; args; _ } ->
-        SSP.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) args)
+    | PConstruct { constructor = `TupleCons _n; fields; _ } ->
+        SSP.AST.TuplePat (List.map ~f:(fun { pat; _ } -> ppat pat) fields)
     (* Record *)
     | PConstruct { is_record = true; _ } -> __TODO_pat__ p.span "record pattern"
-    (* (\* SSP.AST.Ident (pglobal_ident name) *\) *)
-    (* SSP.AST.RecordPat (pglobal_ident name, List.map ~f:(fun {field; pat} -> (pglobal_ident field, ppat pat)) args) *)
-    (*       (\* SSP.AST.ConstructorPat (pglobal_ident name ^ "_case", [SSP.AST.Ident "temp"]) *\) *)
-    (*       (\* List.map ~f:(fun {field; pat} -> (pat, SSP.AST.App (SSP.AST.Var (pglobal_ident field), [SSP.AST.Var "temp"]))) args *\) *)
+    (* (\* SSP.AST.Ident (pglobal_ident constructor) *\) *)
+    (* SSP.AST.RecordPat (pglobal_ident constructor, List.map ~f:(fun {field; pat} -> (pglobal_ident field, ppat pat)) fields) *)
+    (*       (\* SSP.AST.ConstructorPat (pglobal_ident constructor ^ "_case", [SSP.AST.Ident "temp"]) *\) *)
+    (*       (\* List.map ~f:(fun {field; pat} -> (pat, SSP.AST.App (SSP.AST.Var (pglobal_ident field), [SSP.AST.Var "temp"]))) fields *\) *)
     (* Enum *)
-    | PConstruct { name; args; is_record = false; _ } ->
+    | PConstruct { constructor; fields; is_record = false; _ } ->
         SSP.AST.ConstructorPat
-          ( pglobal_ident name,
-            match args with
+          ( pglobal_ident constructor,
+            match fields with
             | [] -> []
-            | _ -> [ SSP.AST.TuplePat (List.map ~f:(fun p -> ppat p.pat) args) ]
+            | _ ->
+                [ SSP.AST.TuplePat (List.map ~f:(fun p -> ppat p.pat) fields) ]
           )
     | PConstant { lit } -> SSP.AST.Lit (pliteral lit)
     | _ -> .
@@ -959,7 +960,7 @@ struct
                           p =
                             PConstruct
                               {
-                                args = [ { pat; _ } ];
+                                fields = [ { pat; _ } ];
                                 is_record = false;
                                 is_struct = true;
                                 _;
@@ -990,16 +991,21 @@ struct
                 ~f:(fun { arm = { arm_pat; body }; _ } ->
                   match arm_pat.p with
                   | PConstruct
-                      { name; args; is_record = false; is_struct = false } -> (
+                      {
+                        constructor;
+                        fields;
+                        is_record = false;
+                        is_struct = false;
+                      } -> (
                       let arg_tuple =
                         SSP.AST.TuplePat
-                          (List.map ~f:(fun p -> ppat p.pat) args)
+                          (List.map ~f:(fun p -> ppat p.pat) fields)
                       in
                       ( SSP.AST.ConstructorPat
-                          ( pglobal_ident name ^ "_case",
-                            match args with [] -> [] | _ -> [ arg_tuple ] ),
+                          ( pglobal_ident constructor ^ "_case",
+                            match fields with [] -> [] | _ -> [ arg_tuple ] ),
                         match
-                          (args, SSPExtraDefinitions.pat_as_expr arg_tuple)
+                          (fields, SSPExtraDefinitions.pat_as_expr arg_tuple)
                         with
                         | _ :: _, Some (redefine_pat, redefine_expr) ->
                             SSPExtraDefinitions.letb
@@ -1016,14 +1022,14 @@ struct
                                               (List.map
                                                  ~f:(fun x ->
                                                    pty arm_pat.span x.pat.typ)
-                                                 args) );
+                                                 fields) );
                                       ] );
                                 body = (pexpr env true) body;
                                 value_typ =
                                   SSP.AST.Product
                                     (List.map
                                        ~f:(fun x -> pty arm_pat.span x.pat.typ)
-                                       args);
+                                       fields);
                                 monad_typ = None;
                               }
                         | _, _ -> (pexpr env true) body ))
@@ -1103,8 +1109,8 @@ struct
                               p =
                                 PConstruct
                                   {
-                                    name = `TupleCons 0;
-                                    args = [];
+                                    constructor = `TupleCons 0;
+                                    fields = [];
                                     is_record = false;
                                     is_struct = false;
                                   };
@@ -1299,9 +1305,9 @@ struct
     match pat.p with
     | PWild -> false
     | PAscription { pat; _ } -> is_mutable_pat pat
-    | PConstruct { name = `TupleCons _; args; _ } ->
+    | PConstruct { constructor = `TupleCons _; fields; _ } ->
         List.fold ~init:false ~f:( || )
-          (List.map ~f:(fun p -> is_mutable_pat p.pat) args)
+          (List.map ~f:(fun p -> is_mutable_pat p.pat) fields)
     | PConstruct _ -> false
     | PArray _ ->
         (* List.fold ~init:false ~f:(||) (List.map ~f:(fun p -> is_mutable_pat p) args) *)
@@ -1793,7 +1799,7 @@ struct
             items
           @ [
               SSP.AST.ProgramInstance
-                ( pglobal_ident name,
+                ( pconcrete_ident name,
                   pgeneric span generics,
                   pty span self_ty,
                   args_ty span gen_vals,
@@ -1859,7 +1865,9 @@ struct
                              ])
                        items) );
             ]
-          @ [ SSP.AST.HintUnfold (pglobal_ident name, Some (pty span self_ty)) ]
+          @ [
+              SSP.AST.HintUnfold (pconcrete_ident name, Some (pty span self_ty));
+            ]
     in
     decls_from_item
 
@@ -2422,7 +2430,8 @@ let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
            ^ "\n"
          in
 
-         Types.{ path = mod_name ^ ".v"; contents = file_content })
+         Types.
+           { path = mod_name ^ ".v"; contents = file_content; sourcemap = None })
 
 let apply_phases (_bo : BackendOptions.t) (i : Ast.Rust.item list) :
     AST.item list =

engine/backends/fstar/fstar_backend.ml

@@ -409,23 +409,26 @@ struct
           "Nested disjuntive patterns should have been eliminated by phase \
            `HoistDisjunctions` (see PR #830)."
     | PArray { args } -> F.pat @@ F.AST.PatList (List.map ~f:ppat args)
-    | PConstruct { name = `TupleCons 0; args = [] } ->
+    | PConstruct { constructor = `TupleCons 0; fields = [] } ->
         F.pat @@ F.AST.PatConst F.Const.Const_unit
-    | PConstruct { name = `TupleCons 1; args = [ { pat } ] } -> ppat pat
-    | PConstruct { name = `TupleCons n; args } ->
+    | PConstruct { constructor = `TupleCons 1; fields = [ { pat } ] } ->
+        ppat pat
+    | PConstruct { constructor = `TupleCons n; fields } ->
         F.pat
-        @@ F.AST.PatTuple (List.map ~f:(fun { pat } -> ppat pat) args, false)
-    | PConstruct { name; args; is_record; is_struct } ->
+        @@ F.AST.PatTuple (List.map ~f:(fun { pat } -> ppat pat) fields, false)
+    | PConstruct { constructor; fields; is_record; is_struct } ->
         let pat_rec () =
-          F.pat @@ F.AST.PatRecord (List.map ~f:pfield_pat args)
+          F.pat @@ F.AST.PatRecord (List.map ~f:pfield_pat fields)
         in
         if is_struct && is_record then pat_rec ()
         else
-          let pat_name = F.pat @@ F.AST.PatName (pglobal_ident p.span name) in
+          let pat_name =
+            F.pat @@ F.AST.PatName (pglobal_ident p.span constructor)
+          in
           F.pat_app pat_name
           @@
           if is_record then [ pat_rec () ]
-          else List.map ~f:(fun { field; pat } -> ppat pat) args
+          else List.map ~f:(fun { field; pat } -> ppat pat) fields
     | PConstant { lit } -> F.pat @@ F.AST.PatConst (pliteral p.span lit)
     | _ -> .
 
@@ -1416,7 +1419,7 @@ struct
         in
         let typ =
           F.mk_e_app
-            (F.term @@ F.AST.Name (pglobal_ident e.span trait))
+            (F.term @@ F.AST.Name (pconcrete_ident trait))
             (List.map ~f:(pgeneric_value e.span) generic_args)
         in
         let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in
@@ -1678,7 +1681,8 @@ let fstar_headers (bo : BackendOptions.t) =
   in
   [ opts; "open Core"; "open FStar.Mul" ] |> String.concat ~sep:"\n"
 
-let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list)
+(** Translate as F* (the "legacy" printer) *)
+let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list list)
     (items : AST.item list) : Types.file list =
   let show_view Concrete_ident.{ crate; path; definition } =
     crate :: (path @ [ definition ]) |> String.concat ~sep:"::"
@@ -1710,11 +1714,19 @@ let translate m (bo : BackendOptions.t) ~(bundles : AST.item list list)
                    contents =
                      "module " ^ mod_name ^ "\n" ^ fstar_headers bo ^ "\n\n"
                      ^ body ^ "\n";
+                   sourcemap = None;
                  }
          in
          List.filter_map ~f:Fn.id
            [ make ~ext:"fst" impl; make ~ext:"fsti" intf ])
 
+let translate =
+  if
+    Sys.getenv "HAX_ENGINE_EXPERIMENTAL_RUST_PRINTER_INSTEAD_OF_FSTAR"
+    |> Option.is_some
+  then failwith "todo"
+  else translate_as_fstar
+
 open Phase_utils
 module DepGraphR = Dependencies.Make (Features.Rust)