Merge pull request #49 from AeneasVerif/son_merge_back

Allow the extraction of structures as tuples

compiler/Config.ml

@@ -338,7 +338,7 @@ let type_check_pure_code = ref false
     as far as possible while leaving "holes" in the generated code? *)
 let fail_hard = ref true
 
-(** if true, add the type name as a prefix
+(** If true, add the type name as a prefix
     to the variant names.
     Ex.:
     In Rust:
@@ -364,3 +364,19 @@ let fail_hard = ref true
       ]}
  *)
 let variant_concatenate_type_name = ref true
+
+(** If true, extract the structures with unnamed fields as tuples.
+
+    ex.:
+    {[
+      // Rust
+      struct Foo(u32)
+
+      // OCaml
+      type Foo = (u32)
+    ]}
+ *)
+let use_tuple_structs = ref true
+
+let backend_has_tuple_projectors () =
+  match !backend with Lean -> true | Coq | FStar | HOL4 -> false

compiler/Extract.ml

@@ -111,7 +111,7 @@ let extract_global_decl_register_names (ctx : extraction_ctx)
     context updated with new bindings.
 
     [is_single_pat]: are we extracting a single pattern (a pattern for a let-binding
-    or a lambda).
+    or a lambda)?
 
     TODO: we don't need something very generic anymore (some definitions used
     to be polymorphic).
@@ -121,38 +121,53 @@ let extract_adt_g_value
     (fmt : F.formatter) (ctx : extraction_ctx) (is_single_pat : bool)
     (inside : bool) (variant_id : VariantId.id option) (field_values : 'v list)
     (ty : ty) : extraction_ctx =
+  let extract_as_tuple () =
+    (* This is very annoying: in Coq, we can't write [()] for the value of
+       type [unit], we have to write [tt]. *)
+    if !backend = Coq && field_values = [] then (
+      F.pp_print_string fmt "tt";
+      ctx)
+    else
+      (* If there is exactly one value, we don't print the parentheses *)
+      let lb, rb =
+        if List.length field_values = 1 then ("", "") else ("(", ")")
+      in
+      F.pp_print_string fmt lb;
+      let ctx =
+        Collections.List.fold_left_link
+          (fun () ->
+            F.pp_print_string fmt ",";
+            F.pp_print_space fmt ())
+          (fun ctx v -> extract_value ctx false v)
+          ctx field_values
+      in
+      F.pp_print_string fmt rb;
+      ctx
+  in
   match ty with
   | TAdt (TTuple, generics) ->
       (* Tuple *)
       (* For now, we only support fully applied tuple constructors *)
       assert (List.length generics.types = List.length field_values);
       assert (generics.const_generics = [] && generics.trait_refs = []);
-      (* This is very annoying: in Coq, we can't write [()] for the value of
-         type [unit], we have to write [tt]. *)
-      if !backend = Coq && field_values = [] then (
-        F.pp_print_string fmt "tt";
-        ctx)
-      else (
-        F.pp_print_string fmt "(";
-        let ctx =
-          Collections.List.fold_left_link
-            (fun () ->
-              F.pp_print_string fmt ",";
-              F.pp_print_space fmt ())
-            (fun ctx v -> extract_value ctx false v)
-            ctx field_values
-        in
-        F.pp_print_string fmt ")";
-        ctx)
+      extract_as_tuple ()
   | TAdt (adt_id, _) ->
       (* "Regular" ADT *)
-
-      (* If we are generating a pattern for a let-binding and we target Lean,
-         the syntax is: `let ⟨ x0, ..., xn ⟩ := ...`.
-
-         Otherwise, it is: `let Cons x0 ... xn = ...`
-      *)
-      if is_single_pat && !Config.backend = Lean then (
+      (* We may still extract the ADT as a tuple, if none of the fields are
+         named *)
+      if
+        PureUtils.type_decl_from_type_id_is_tuple_struct
+          ctx.trans_ctx.type_ctx.type_infos adt_id
+      then (* Extract as a tuple *)
+        extract_as_tuple ()
+      else if
+        (* If we are generating a pattern for a let-binding and we target Lean,
+           the syntax is: `let ⟨ x0, ..., xn ⟩ := ...`.
+
+           Otherwise, it is: `let Cons x0 ... xn = ...`
+        *)
+        is_single_pat && !Config.backend = Lean
+      then (
         F.pp_print_string fmt "⟨";
         F.pp_print_space fmt ();
         let ctx =
@@ -516,21 +531,41 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
    * projection ([x.field] instead of [MkAdt?.field x] *)
   match args with
   | [ arg ] ->
-      (* Exactly one argument: pretty-print *)
-      let field_name = ctx_get_field proj.adt_id proj.field_id ctx in
-      (* Open a box *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Extract the expression *)
-      extract_texpression ctx fmt true arg;
-      (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
-      if !backend <> Lean then F.pp_print_break fmt 0 0;
-      F.pp_print_string fmt ".";
-      (* If in Coq, the field projection has to be parenthesized *)
-      (match !backend with
-      | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
-      | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
-      (* Close the box *)
-      F.pp_close_box fmt ()
+      let is_tuple_struct =
+        PureUtils.type_decl_from_type_id_is_tuple_struct
+          ctx.trans_ctx.type_ctx.type_infos proj.adt_id
+      in
+      (* Check if we extract the type as a tuple, and it only has one field.
+         In this case, there is no projection. *)
+      let has_one_field =
+        match proj.adt_id with
+        | TAdtId id -> (
+            let d = TypeDeclId.Map.find id ctx.trans_types in
+            match d.kind with Struct [ _ ] -> true | _ -> false)
+        | _ -> false
+      in
+      if is_tuple_struct && has_one_field then
+        extract_texpression ctx fmt inside arg
+      else
+        (* Exactly one argument: pretty-print *)
+        let field_name =
+          (* Check if we need to extract the type as a tuple *)
+          if is_tuple_struct then FieldId.to_string proj.field_id
+          else ctx_get_field proj.adt_id proj.field_id ctx
+        in
+        (* Open a box *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        (* Extract the expression *)
+        extract_texpression ctx fmt true arg;
+        (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
+        if !backend <> Lean then F.pp_print_break fmt 0 0;
+        F.pp_print_string fmt ".";
+        (* If in Coq, the field projection has to be parenthesized *)
+        (match !backend with
+        | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
+        | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+        (* Close the box *)
+        F.pp_close_box fmt ()
   | arg :: args ->
       (* Call extract_App again, but in such a way that the first argument is
        * isolated *)

compiler/ExtractBase.ml

@@ -109,7 +109,7 @@ let decl_is_first_from_group (kind : decl_kind) : bool =
 let decl_is_not_last_from_group (kind : decl_kind) : bool =
   not (decl_is_last_from_group kind)
 
-type type_decl_kind = Enum | Struct [@@deriving show]
+type type_decl_kind = Enum | Struct | Tuple [@@deriving show]
 
 (** We use identifiers to look for name clashes *)
 type id =
@@ -1194,12 +1194,13 @@ let type_decl_kind_to_qualif (kind : decl_kind)
       | Declared -> Some "val")
   | Coq -> (
       match (kind, type_kind) with
+      | SingleNonRec, Some Tuple -> Some "Definition"
       | SingleNonRec, Some Enum -> Some "Inductive"
       | SingleNonRec, Some Struct -> Some "Record"
       | (SingleRec | MutRecFirst), Some _ -> Some "Inductive"
       | (MutRecInner | MutRecLast), Some _ ->
           (* Coq doesn't support groups of mutually recursive definitions which mix
-           * records and inducties: we convert everything to records if this happens
+           * records and inductives: we convert everything to records if this happens
            *)
           Some "with"
       | (Assumed | Declared), None -> Some "Axiom"
@@ -1214,12 +1215,12 @@ let type_decl_kind_to_qualif (kind : decl_kind)
                ^ ")")))
   | Lean -> (
       match kind with
-      | SingleNonRec ->
-          if type_kind = Some Struct then Some "structure" else Some "inductive"
-      | SingleRec -> Some "inductive"
-      | MutRecFirst -> Some "inductive"
-      | MutRecInner -> Some "inductive"
-      | MutRecLast -> Some "inductive"
+      | SingleNonRec -> (
+          match type_kind with
+          | Some Tuple -> Some "def"
+          | Some Struct -> Some "structure"
+          | _ -> Some "inductive")
+      | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> Some "inductive"
       | Assumed -> Some "axiom"
       | Declared -> Some "axiom")
   | HOL4 -> None