witness added

hacspec · Jul 6, 2023 · a6203f0 · a6203f0
1 parent 17c2271
commit a6203f0
Show file tree

Hide file tree

Showing 6 changed files with 31 additions and 34 deletions.
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -564,20 +564,14 @@ struct
         ]
 
   and p_inductive span variants parrent_name : C.AST.inductive_case list =
-    List.map variants ~f:(fun { name; arguments; is_record } ->
-        if is_record then
-          C.AST.InductiveCase
-            ( U.Concrete_ident_view.to_definition_name name,
-              C.AST.RecordTy
-                (pconcrete_ident name, p_record_record span arguments) )
-        else
-          let name = U.Concrete_ident_view.to_definition_name name in
-          match arguments with
-          | [] -> C.AST.BaseCase name
-          | [ (arg_name, arg_ty) ] -> C.AST.InductiveCase (name, pty span arg_ty)
-          | _ ->
-              C.AST.InductiveCase
-                (name, C.AST.Product (List.map ~f:(snd >> pty span) arguments)))
+    List.map variants ~f:(fun { name; arguments; is_record = None } ->
+        let name = U.Concrete_ident_view.to_definition_name name in
+        match arguments with
+        | [] -> C.AST.BaseCase name
+        | [ (arg_name, arg_ty) ] -> C.AST.InductiveCase (name, pty span arg_ty)
+        | _ ->
+            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 -> *)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -548,7 +548,7 @@ struct
         {
           name;
           generics;
-          variants = [ { arguments; is_record = true; _ } ];
+          variants = [ { arguments; is_record = Some _; _ } ];
           is_struct = true;
         } ->
         F.decls
@@ -582,7 +582,7 @@ struct
                   (let field_indexes =
                      List.map ~f:(fst >> index_of_field_concrete) arguments
                    in
-                   if is_record then
+                   if Option.is_some is_record then
                      F.AST.VpRecord
                        ( List.map
                            ~f:(fun (field, ty) ->

diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
@@ -524,7 +524,7 @@ functor
     and variant = {
       name : concrete_ident;
       arguments : (concrete_ident * ty) list;
-      is_record : bool; (* F.record_variants option; *)
+      is_record : F.record_variants option;
     }
 
     and item' =

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -982,7 +982,11 @@ module Exn = struct
                         fields
                   | Unit _ -> []
                 in
-                { name; arguments; is_record })
+                {
+                  name;
+                  arguments;
+                  is_record = Option.some_if is_record W.record_variants;
+                })
               variants
           in
           let name = Concrete_ident.of_def_id Type def_id in
@@ -1001,12 +1005,16 @@ module Exn = struct
                     (Concrete_ident.of_def_id Field id, c_ty span ty))
                   fields
               in
-              { name; arguments; is_record }
+              {
+                name;
+                arguments;
+                is_record = Option.some_if is_record W.record_variants;
+              }
             in
             match v with
             | Tuple (fields, _, _) -> mk fields false
             | Struct ((_ :: _ as fields), _) -> mk fields true
-            | _ -> { name; arguments = []; is_record = false }
+            | _ -> { name; arguments = []; is_record = None }
           in
           let variants = [ v ] in
           let name = Concrete_ident.of_def_id Type def_id in

diff --git a/engine/lib/phases/phase_record_variants.ml b/engine/lib/phases/phase_record_variants.ml
@@ -57,11 +57,11 @@ module Make (FA : Features.T) = struct
   and flatten_variants span generics (v : A.variant) : B.variant * B.item option
       =
     let b_v = dvariant span v in
-    if b_v.is_record then
+    if Option.is_some v.is_record then
       let new_name : Ast.concrete_ident =
         Concrete_ident.of_def_id Type
           {
-            krate = "temp_name";
+            krate = "";
             path = [ { data = TypeNs "my_temp_name"; disambiguator = 4 } ];
           }
       in
@@ -70,16 +70,7 @@ module Make (FA : Features.T) = struct
           name = b_v.name;
           arguments =
             [ (new_name, B.TApp { ident = `Concrete new_name; args = [] }) ];
-          is_record = false;
-        }
-      in
-      let temp (n, t) : B.variant =
-        {
-          name = n;
-          arguments = [ (n, t) ];
-          is_record = false;
-          (* Should this be false? *)
-          (* F.record_variants option; *)
+          is_record = b_v.is_record;
         }
       in
       ( b_v',
@@ -90,7 +81,11 @@ module Make (FA : Features.T) = struct
                 {
                   name = new_name;
                   generics = dgenerics span generics;
-                  variants = List.map ~f:temp b_v.arguments;
+                  variants =
+                    List.map
+                      ~f:(fun (n, t) : B.variant ->
+                        { name = n; arguments = [ (n, t) ]; is_record = None })
+                      b_v.arguments;
                   is_struct = true;
                 };
             span;

diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
@@ -308,7 +308,7 @@ struct
       {
         name = v.name;
         arguments = List.map ~f:(map_snd @@ dty span) v.arguments;
-        is_record = v.is_record;
+        is_record = Option.map ~f:S.record_variants v.is_record;
       }
 
     let rec dtrait_item' (span : span) (ti : A.trait_item') : B.trait_item' =