refactor(engine): rename pat'.PConstruct fields similarly to `expr'…

….Construct`

This commits makes the node for constructors on patterns and
expressions use the same names.

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)
     | _ -> .
 

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) *)

engine/backends/fstar/fstar_backend.ml

@@ -401,23 +401,26 @@ struct
         Error.unimplemented p.span ~issue_id:463
           ~details:"The F* backend doesn't support nested disjuntive patterns"
     | 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)
     | _ -> .
 

engine/backends/proverif/proverif_backend.ml

@@ -242,8 +242,8 @@ module Make (Options : OPTS) : MAKE = struct
           let body = print#expr_at Arm_body body in
           match arm_pat with
           | { p = PWild; _ } -> body
-          | { p = PConstruct { name; _ } }
-            when Global_ident.eq_name Core__result__Result__Err name ->
+          | { p = PConstruct { constructor; _ } }
+            when Global_ident.eq_name Core__result__Result__Err constructor ->
               print#pv_letfun_call (print#error_letfun_name body_typ) []
           | _ ->
               let pat =
@@ -296,16 +296,18 @@ module Make (Options : OPTS) : MAKE = struct
             fun pat ->
               match pat with
               | PConstant { lit } -> string "=" ^^ print#literal Pat lit
-              | PConstruct { name; args }
-                when Global_ident.eq_name Core__option__Option__None name ->
+              | PConstruct { constructor; fields }
+                when Global_ident.eq_name Core__option__Option__None constructor
+                ->
                   string "None()"
-              | PConstruct { name; args }
+              | PConstruct { constructor; fields }
               (* The `Some` constructor in ProVerif expects a
                  bitstring argument, so we use the appropriate
                  `_to_bitstring` type converter on the inner
                  expression. *)
-                when Global_ident.eq_name Core__option__Option__Some name ->
-                  let inner_field = List.hd_exn args in
+                when Global_ident.eq_name Core__option__Option__Some constructor
+                ->
+                  let inner_field = List.hd_exn fields in
                   let inner_field_type_doc =
                     print#ty AlreadyPar inner_field.pat.typ
                   in
@@ -322,21 +324,23 @@ module Make (Options : OPTS) : MAKE = struct
                           ^^ iblock parens inner_field_doc)
                   in
                   string "Some" ^^ inner_block
-              | PConstruct { name; args }
+              | PConstruct { constructor; fields }
               (* We replace applications of the `Ok` constructor
                  with their contents. *)
-                when Global_ident.eq_name Core__result__Result__Ok name ->
-                  let inner_field = List.hd_exn args in
+                when Global_ident.eq_name Core__result__Result__Ok constructor
+                ->
+                  let inner_field = List.hd_exn fields in
                   let inner_field_type_doc =
                     print#ty AlreadyPar inner_field.pat.typ
                   in
                   let inner_field_doc = print#pat ctx inner_field.pat in
                   inner_field_doc
-              | PConstruct { name; args } -> (
+              | PConstruct { constructor; fields } -> (
                   match
-                    translate_known_name name ~dict:library_constructor_patterns
+                    translate_known_name constructor
+                      ~dict:library_constructor_patterns
                   with
-                  | Some (_, translation) -> translation args
+                  | Some (_, translation) -> translation fields
                   | None -> super#pat' ctx pat)
               | PWild ->
                   print#typed_wildcard

engine/lib/ast.ml

@@ -196,10 +196,10 @@ functor
       | PWild
       | PAscription of { typ : ty; typ_span : span; pat : pat }
       | PConstruct of {
-          name : global_ident;
+          constructor : global_ident;
           is_record : bool; (* are fields named? *)
           is_struct : bool; (* a struct has one constructor *)
-          args : field_pat list;
+          fields : field_pat list;
         }
       (* An or-pattern, e.g. `p | q`.
          Invariant: `List.length subpats >= 2`. *)

engine/lib/ast_utils.ml

@@ -704,7 +704,7 @@ module Make (F : Features.T) = struct
   (* TODO: Those tuple1 things are wrong! Tuples of size one exists in Rust! e.g. `(123,)` *)
   let rec remove_tuple1_pat (p : pat) : pat =
     match p.p with
-    | PConstruct { name = `TupleType 1; args = [ { pat; _ } ]; _ } ->
+    | PConstruct { constructor = `TupleType 1; fields = [ { pat; _ } ]; _ } ->
         remove_tuple1_pat pat
     | _ -> p
 
@@ -745,7 +745,7 @@ module Make (F : Features.T) = struct
         pat_is_expr p e
     | PBinding { subpat = None; var = pv; _ }, LocalVar ev ->
         [%eq: local_ident] pv ev
-    | ( PConstruct { name = pn; args = pargs; _ },
+    | ( PConstruct { constructor = pn; fields = pargs; _ },
         Construct { constructor = en; fields = eargs; base = None; _ } )
       when [%eq: global_ident] pn en -> (
         match List.zip pargs eargs with
@@ -827,10 +827,10 @@ module Make (F : Features.T) = struct
           p =
             PConstruct
               {
-                name = `TupleCons len;
-                args = tuple;
+                constructor = `TupleCons len;
                 is_record = false;
                 is_struct = true;
+                fields = tuple;
               };
           typ = make_tuple_typ @@ List.map ~f:(fun { pat; _ } -> pat.typ) tuple;
           span;

engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml

@@ -216,17 +216,17 @@ module Make (F : Features.T) = struct
       method pat' : par_state -> pat' fn =
         fun _ -> function
           | PConstant { lit } -> print#literal Pat lit
-          | PConstruct { name; args; is_record; is_struct } -> (
-              match name with
+          | PConstruct { constructor; is_record; is_struct; fields } -> (
+              match constructor with
               | `Concrete constructor ->
                   print#doc_construct_inductive ~is_record ~is_struct
                     ~constructor ~base:None
                     (List.map
                        ~f:(fun fp ->
                          (fp.field, print#pat_at Pat_ConcreteInductive fp.pat))
-                       args)
+                       fields)
               | `TupleCons _ ->
-                  List.map ~f:(fun fp -> fp.pat) args
+                  List.map ~f:(fun fp -> fp.pat) fields
                   |> print#pat_construct_tuple
               | `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ ->
                   print#assertion_failure "todo err")

engine/lib/import_thir.ml

@@ -866,14 +866,14 @@ end) : EXPR = struct
           let var = local_ident Expr var in
           PBinding { mut; mode; var; typ; subpat }
       | Variant { info; subpatterns; _ } ->
-          let name =
+          let constructor =
             def_id (Constructor { is_struct = info.typ_is_struct }) info.variant
           in
-          let args = List.map ~f:(c_field_pat info) subpatterns in
+          let fields = List.map ~f:(c_field_pat info) subpatterns in
           PConstruct
             {
-              name;
-              args;
+              constructor;
+              fields;
               is_record = info.variant_is_record;
               is_struct = info.typ_is_struct;
             }
@@ -1375,12 +1375,12 @@ let cast_of_enum typ_name generics typ thir_span
             {
               is_record = variant.is_record;
               is_struct = false;
-              args =
+              fields =
                 List.map
                   ~f:(fun (cid, typ, _) ->
                     { field = `Concrete cid; pat = { p = PWild; typ; span } })
                   variant.arguments;
-              name = `Concrete variant.name;
+              constructor = `Concrete variant.name;
             }
         in
         let pat = { p = pat; typ = self; span } in

engine/lib/phases/phase_drop_match_guards.ml

@@ -119,7 +119,7 @@ module%inlined_contents Make (F : Features.T) = struct
           in
 
           let mk_opt_pattern (binding : B.pat option) : B.pat =
-            let (name : Concrete_ident.name), (args : B.field_pat list) =
+            let (name : Concrete_ident.name), (fields : B.field_pat list) =
               match binding with
               | Some b ->
                   ( Core__option__Option__Some,
@@ -130,11 +130,11 @@ module%inlined_contents Make (F : Features.T) = struct
               p =
                 PConstruct
                   {
-                    name =
+                    constructor =
                       Global_ident.of_name
                         (Constructor { is_struct = false })
                         name;
-                    args;
+                    fields;
                     is_record = false;
                     is_struct = false;
                   };

engine/lib/phases/phase_hoist_disjunctive_patterns.ml

@@ -64,18 +64,18 @@ module Make (F : Features.T) =
             in
 
             match p.p with
-            | PConstruct { name; args; is_record; is_struct } ->
-                let args_as_pat =
-                  List.rev_map args ~f:(fun arg -> self#visit_pat () arg.pat)
+            | PConstruct { constructor; fields; is_record; is_struct } ->
+                let fields_as_pat =
+                  List.rev_map fields ~f:(fun arg -> self#visit_pat () arg.pat)
                 in
                 let subpats =
-                  List.map (treat_args [ [] ] args_as_pat)
-                    ~f:(fun args_as_pat ->
-                      let args =
-                        List.map2_exn args_as_pat args
+                  List.map (treat_args [ [] ] fields_as_pat)
+                    ~f:(fun fields_as_pat ->
+                      let fields =
+                        List.map2_exn fields_as_pat fields
                           ~f:(fun pat { field; _ } -> { field; pat })
                       in
-                      PConstruct { name; args; is_record; is_struct }
+                      PConstruct { constructor; fields; is_record; is_struct }
                       |> return_pat)
                 in