Adding phase to simplify enum and record matching statements

Update proverif

Fix

engine/backends/coq/coq/coq_backend.ml

@@ -12,6 +12,7 @@ include
       include On.Monadic_binding
       include On.Macro
       include On.Construct_base
+      include On.Project_instead_of_match
     end)
     (struct
       let backend = Diagnostics.Backend.Coq
@@ -36,6 +37,8 @@ module SubtypeToInputLanguage
              and type nontrivial_lhs = Features.Off.nontrivial_lhs
              and type loop = Features.Off.loop
              and type block = Features.Off.block
+             and type project_instead_of_match =
+              Features.On.project_instead_of_match
              and type for_loop = Features.Off.for_loop
              and type for_index_loop = Features.Off.for_index_loop
              and type state_passing_loop = Features.Off.state_passing_loop) =
@@ -52,6 +55,7 @@ struct
         include Features.SUBTYPE.On.Construct_base
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
+        include Features.SUBTYPE.On.Project_instead_of_match
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -216,9 +220,9 @@ struct
         __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 } ->
+    | PConstruct { name; args; is_record = Some _ } ->
         C.AST.RecordPat (pglobal_ident name, pfield_pats args)
-    | PConstruct { name; args; is_record = false } ->
+    | PConstruct { name; args; is_record = None } ->
         C.AST.ConstructorPat
           (pglobal_ident name, List.map ~f:(fun p -> ppat p.pat) args)
     | PConstant { lit } -> C.AST.Lit (pliteral p.span lit)

engine/backends/easycrypt/easycrypt_backend.ml

@@ -15,6 +15,7 @@ include
       include On.Mutable_variable
       include On.Macro
       include On.Construct_base
+      include On.Project_instead_of_match
     end)
     (struct
       let backend = Diagnostics.Backend.EasyCrypt
@@ -60,6 +61,7 @@ module RejectNotEC (FA : Features.T) = struct
         let state_passing_loop = reject
         let nontrivial_lhs = reject
         let block = reject
+        let project_instead_of_match _ _ = Features.On.project_instead_of_match
         let for_loop = reject
         let construct_base _ _ = Features.On.construct_base
         let for_index_loop _ _ = Features.On.for_index_loop

engine/backends/fstar/fstar_backend.ml

@@ -11,6 +11,7 @@ include
       include On.Slice
       include On.Macro
       include On.Construct_base
+      include On.Project_instead_of_match
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -35,6 +36,8 @@ module SubtypeToInputLanguage
              and type nontrivial_lhs = Features.Off.nontrivial_lhs
              and type loop = Features.Off.loop
              and type block = Features.Off.block
+             and type project_instead_of_match =
+              Features.On.project_instead_of_match
              and type for_loop = Features.Off.for_loop
              and type for_index_loop = Features.Off.for_index_loop
              and type state_passing_loop = Features.Off.state_passing_loop) =
@@ -51,6 +54,7 @@ struct
         include Features.SUBTYPE.On.Construct_base
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
+        include Features.SUBTYPE.On.Project_instead_of_match
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -354,12 +358,12 @@ struct
         let pat_rec () =
           F.pat @@ F.AST.PatRecord (List.map ~f:pfield_pat args)
         in
-        if is_struct && is_record then pat_rec ()
+        if is_struct && Option.is_some is_record then pat_rec ()
         else
           let pat_name = F.pat @@ F.AST.PatName (pglobal_ident p.span name) in
           F.pat_app pat_name
           @@
-          if is_record then [ pat_rec () ]
+          if Option.is_some is_record then [ pat_rec () ]
           else List.map ~f:(fun { field; pat } -> ppat pat) args
     | PConstant { lit } -> F.pat @@ F.AST.PatConst (pliteral p.span lit)
     | _ -> .

engine/backends/proverif/proverif_backend.ml

@@ -8,6 +8,7 @@ include
       open Features
       include Off
       include On.Macro
+      include On.Project_instead_of_match
     end)
     (struct
       let backend = Diagnostics.Backend.ProVerif
@@ -51,6 +52,7 @@ struct
 
         let continue = reject
         let loop = reject
+        let project_instead_of_match _ _ = Features.On.project_instead_of_match
         let for_loop = reject
         let for_index_loop = reject
         let state_passing_loop = reject

engine/lib/ast.ml

@@ -271,13 +271,16 @@ functor
 
     and trait_ref = { trait : concrete_ident; args : generic_value list }
 
+    (* and is_record_construct = { witness : F.project_instead_of_match } *)
     and pat' =
       | PWild
       | PAscription of { typ : ty; typ_span : span; pat : pat }
       | PConstruct of {
           name : global_ident;
           args : field_pat list;
-          is_record : bool; (* are fields named? *)
+          is_record : F.project_instead_of_match option;
+          (* are fields named? *)
+          (* F.project_instead_of_match *)
           is_struct : bool; (* a struct has one constructor *)
         }
       (* An or-pattern, e.g. `p | q`.

engine/lib/ast_utils.ml

@@ -688,7 +688,7 @@ module Make (F : Features.T) = struct
               {
                 name = `TupleCons len;
                 args = tuple;
-                is_record = false;
+                is_record = None;
                 is_struct = true;
               };
           typ = make_tuple_typ @@ List.map ~f:(fun { pat; _ } -> pat.typ) tuple;

engine/lib/diagnostics.ml

@@ -37,6 +37,7 @@ module Phase = struct
     | TrivializeAssignLhs
     | CfIntoMonads
     | FunctionalizeLoops
+    | ProjectInsteadOfMatch
     | DummyA
     | DummyB
     | DummyC

engine/lib/features.ml

@@ -21,7 +21,8 @@ loop,
   construct_base,
   monadic_action,
   monadic_binding,
-  block]
+  block,
+  project_instead_of_match]
 
 module Full = On
 

engine/lib/generic_printer/generic_printer_base.ml

@@ -213,7 +213,8 @@ module Make (F : Features.T) = struct
           | PConstruct { name; args; is_record; is_struct } -> (
               match name with
               | `Concrete constructor ->
-                  print#doc_construct_inductive ~is_record ~is_struct
+                  print#doc_construct_inductive
+                    ~is_record:(Option.is_some is_record) ~is_struct
                     ~constructor ~base:None
                     (List.map
                        ~f:(fun fp ->

engine/lib/import_thir.ml

@@ -752,7 +752,12 @@ end) : EXPR = struct
             {
               name;
               args;
-              is_record = info.variant_is_record;
+              is_record =
+                (if info.variant_is_record then Some W.project_instead_of_match
+                else None (* W.project_instead_of_match *));
+              (* if info.variant_is_record *)
+              (* then Some W.project_instead_of_match *)
+              (* else None; *)
               is_struct = info.typ_is_struct;
             }
       | Tuple { subpatterns } ->

engine/lib/phases.ml

@@ -9,3 +9,4 @@ module Cf_into_monads = Phase_cf_into_monads.Make
 module Functionalize_loops = Phase_functionalize_loops.Make
 module Reject = Phase_reject
 module Local_mutation = Phase_local_mutation.Make
+module Project_instead_of_match = Phase_project_instead_of_match.Make