Flatten, but issues with records?

hacspec · Jul 7, 2023 · c12f54d · c12f54d
1 parent a6203f0
commit c12f54d
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 32 deletions.
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -572,25 +572,6 @@ struct
         | _ ->
             C.AST.InductiveCase
               (name, C.AST.Product (List.map ~f:(snd >> pty span) arguments)))
-  (* match variants with _ -> [] *)
-  (* TODO: I don't get this pattern maching below. Variant with more than one payloads are rejected implicitely? *)
-  (* | { name; arguments = [ (arg_name, arg_ty) ] } :: xs -> *)
-  (*     if (index_of_field >> Option.is_some) arg_name then *)
-  (*       C.AST.InductiveCase (U.Concrete_ident_view.to_definition_name name, pty span arg_ty) *)
-  (*       :: p_inductive span xs parrent_name *)
-  (*     else *)
-  (*       C.AST.InductiveCase (U.Concrete_ident_view.to_definition_name arg_name, pty span arg_ty) *)
-  (*       :: p_inductive span xs parrent_name *)
-  (* | { name; arguments = [] } :: xs -> *)
-  (*     C.AST.BaseCase (U.Concrete_ident_view.to_definition_name name) *)
-  (*     :: p_inductive span xs parrent_name *)
-  (* | { name; arguments } :: xs -> *)
-  (*     C.AST.InductiveCase *)
-  (*       ( U.Concrete_ident_view.to_definition_name name, *)
-  (*         C.AST.RecordTy (pglobal_ident name, p_record_record span arguments) *)
-  (*       ) *)
-  (*     :: p_inductive span xs parrent_name *)
-  (* | _ -> [] *)
 
   and p_record span variants : (string * C.AST.ty) list =
     match variants with

diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml
@@ -243,9 +243,9 @@ functor
       | AST.Var s -> (s, false)
       | AST.Name s -> (s, false)
       | AST.RecordConstructor (f, args) ->
-          ( "Build_"
-            ^ term_to_string_without_paren f depth
-            ^ record_args_to_string args depth,
+          ( "{|"
+            ^ record_args_to_string args depth
+            ^ "|}",
             true )
       | AST.Type t ->
           let _, ty_str = ty_to_string t in
@@ -310,8 +310,10 @@ functor
     and record_args_to_string (args : (string * AST.term) list) depth : string =
       match args with
       | (i, t) :: xs ->
-          " "
-          ^ term_to_string_with_paren t depth
+        " "
+        ^ i ^ " " ^ ":=" ^ " "
+        ^ term_to_string_without_paren t depth
+        ^ ";" ^ " "
           ^ record_args_to_string xs depth
       | _ -> ""
 
@@ -479,7 +481,7 @@ functor
       List.fold_left ~init:([], "")
         ~f:(fun (variant_definitions, variants_str) (ty_name, ty) ->
           let ty_definitions, ty_str = ty_to_string ty in
-          ( ty_definitions @ variant_definitions,
-            pre ^ ty_name ^ " " ^ ":" ^ " " ^ ty_str ^ post ^ variants_str ))
+          ( variant_definitions @ ty_definitions,
+            variants_str ^ pre ^ ty_name ^ " " ^ ":" ^ " " ^ ty_str ^ post ))
         variants
   end
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -1013,7 +1013,7 @@ module Exn = struct
             in
             match v with
             | Tuple (fields, _, _) -> mk fields false
-            | Struct ((_ :: _ as fields), _) -> mk fields true
+            | Struct ((_ :: _ as fields), _) -> mk fields true (* Why is this true? *)
             | _ -> { name; arguments = []; is_record = None }
           in
           let variants = [ v ] in

diff --git a/engine/lib/phases/phase_record_variants.ml b/engine/lib/phases/phase_record_variants.ml
@@ -15,11 +15,19 @@ module Make (FA : Features.T) = struct
         include Feature_gate.DefaultSubtype
 
         let record_variants = reject
+        (* let record_variants _ = Features.Off.Record_variants *)
 
         let metadata =
           Phase_utils.Metadata.make Diagnostics.Phase.RecordVariants
       end)
 
+  let dvariant (span : Ast.span) (v : A.variant) : B.variant =
+    {
+      name = v.name;
+      arguments = List.map ~f:(map_snd @@ dty span) v.arguments;
+      is_record = None;
+    }
+
   let rec ditems (items : A.item list) : B.item list =
     List.concat_map
       ~f:(fun item ->
@@ -44,6 +52,21 @@ module Make (FA : Features.T) = struct
                   ident = item.ident;
                 };
               ]
+        | Type { name; generics; variants; is_struct = true } ->
+          [
+            {
+              v =
+                B.Type
+                  {
+                    name;
+                    generics = dgenerics item.span generics;
+                    variants = List.map ~f:(dvariant item.span) variants;
+                    is_struct = true;
+                  };
+              span = item.span;
+              ident = item.ident;
+            };
+          ]
         | _ ->
             [
               {
@@ -54,8 +77,7 @@ module Make (FA : Features.T) = struct
             ])
       items
 
-  and flatten_variants span generics (v : A.variant) : B.variant * B.item option
-      =
+  and flatten_variants span generics (v : A.variant) : B.variant * B.item option =
     let b_v = dvariant span v in
     if Option.is_some v.is_record then
       let new_name : Ast.concrete_ident =
@@ -68,9 +90,8 @@ module Make (FA : Features.T) = struct
       let b_v' : B.variant =
         {
           name = b_v.name;
-          arguments =
-            [ (new_name, B.TApp { ident = `Concrete new_name; args = [] }) ];
-          is_record = b_v.is_record;
+          arguments = [ (new_name, B.TApp { ident = `Concrete new_name; args = [] }) ];
+          is_record = None;
         }
       in
       ( b_v',