WIP

cryspen · Jan 8, 2024 · 7644d99 · 7644d99
1 parent 1b8c590
commit 7644d99
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 14 deletions.
diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -17,7 +17,6 @@ include
       include On.For_loop
       include On.For_index_loop
       include On.State_passing_loop
-      (* include On.Project_struct_pattern *)
     end)
     (struct
       let backend = Diagnostics.Backend.SSProve
@@ -39,7 +38,6 @@ module SubtypeToInputLanguage
              and type monadic_action = Features.Off.monadic_action
              and type arbitrary_lhs = Features.Off.arbitrary_lhs
              and type nontrivial_lhs = Features.Off.nontrivial_lhs
-             and type struct_pattern = Features.Off.struct_pattern
              and type block = Features.Off.block) =
 struct
   module FB = InputLanguage
@@ -58,7 +56,6 @@ struct
         include Features.SUBTYPE.On.For_loop
         include Features.SUBTYPE.On.For_index_loop
         include Features.SUBTYPE.On.State_passing_loop
-        (* include Features.SUBTYPE.Off.Struct_pattern *)
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -625,7 +622,6 @@ module TransformToInputLanguage (* : PHASE *) =
     |> Phases.Reject.EarlyExit
     (* |> Phases.Functionalize_loops *)
     |> Phases.Reject.As_pattern
-    |> Phases.Struct_pattern
     |> SubtypeToInputLanguage
     |> Identity
   ]
@@ -858,14 +854,15 @@ struct
         __TODO_pat__ p.span "tuple 1"
     | PConstruct { name = `TupleCons n; args } ->
         SSP.AST.TuplePat (List.map ~f:(fun { pat } -> ppat pat) args)
-    (* (\* Record *\) *)
-    (*     | PConstruct { name; args; is_record = Some _ } -> *)
+    (* Record *)
+    | PConstruct { name; args; 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 *\) *)
     (* Enum *)
-    | PConstruct { name; args; is_record = None } ->
+    | PConstruct { name; args; is_record = false } ->
         SSP.AST.ConstructorPat
           ( pglobal_ident name,
             match args with
@@ -1020,7 +1017,7 @@ struct
                               {
                                 name;
                                 args = [ { field; pat } ];
-                                is_record = None;
+                                is_record = false;
                                 is_struct = true;
                               };
                         };
@@ -1047,7 +1044,7 @@ struct
                 ~f:(fun { arm = { arm_pat; body } } ->
                   match arm_pat.p with
                   | PConstruct
-                      { name; args; is_record = None; is_struct = false } -> (
+                      { name; args; is_record = false; is_struct = false } -> (
                       let arg_tuple =
                         SSP.AST.TuplePat
                           (List.map ~f:(fun p -> ppat p.pat) args)
@@ -1162,7 +1159,7 @@ struct
                                   {
                                     name = `TupleCons 0;
                                     args = [];
-                                    is_record = None;
+                                    is_record = false;
                                     is_struct = false;
                                   };
                               span = Span.dummy ();

diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
@@ -25,7 +25,7 @@ end)
 module Attrs = Attr_payloads.MakeBase (Error)
 
 let import_thir_items (include_clauses : Types.inclusion_clause list)
-    (items : Types.item_for__decorated_for__expr_kind list) : Ast.Rust.item list
+    (items : Types.item_for__decorated_for__expr_kind list) (options : Types.engine_options) : Ast.Rust.item list
     =
   let result = List.map ~f:Import_thir.import_item items |> List.map ~f:snd in
   let items = List.concat_map ~f:fst result in
@@ -43,8 +43,11 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
         match Attrs.status i.attrs with Included _ -> true | _ -> false)
       items
   in
-  (* TODO: should keep order for non-dependent functions by default? This breaks ssprove extraction. *)
-  let items = Deps.sort items in
+  (* TODO: should keep order for non-dependent functions by default? This breaks ssprove extraction. Alternatively this should be a phase *)
+  let items =
+    match options.backend.backend with
+    | Coq | Ssprove -> items
+    | _ -> Deps.sort items in
   let reports =
     List.concat_map
       ~f:(fun (item : Ast.Rust.item) ->
@@ -67,7 +70,7 @@ let run (options : Types.engine_options) : Types.output =
     let include_clauses =
       options.backend.translation_options.include_namespaces
     in
-    let items = import_thir_items include_clauses options.input in
+    let items = import_thir_items include_clauses options.input options in
     Logs.info (fun m ->
         m "Applying phase for backend %s"
           ([%show: Diagnostics.Backend.t] M.backend));