Coq: fix naming scheme

engine/backends/coq/coq/coq_backend.ml

@@ -94,8 +94,8 @@ module CoqNamePolicy = struct
 
   let named_field_prefix = Some `TypeName
   let struct_constructor_prefix = Some "Build_t_"
-  let enum_constructor_prefix = Some "AABBCC"
-  let union_constructor_prefix = Some "DDEEFF"
+  (* let enum_constructor_prefix = Some "AABBCC" *)
+  (* let union_constructor_prefix = Some "DDEEFF" *)
   let prefix__constructors_with_type = true
   let prefix_struct_constructors_with_type = true
   let prefix_enum_constructors_with_type = true
@@ -126,6 +126,10 @@ let hardcoded_coq_headers =
 
 module BasePrinter = Generic_printer.Make (InputLanguage)
 
+let module_name_from_path path =
+  String.concat ~sep:"_"
+    (List.map ~f:(map_first_letter String.uppercase) path)
+
 module Make
     (Default : sig
       val default : string -> string
@@ -193,6 +197,9 @@ struct
     object (self)
       inherit BasePrinter.base
 
+      val concrete_ident_view : (module Concrete_ident.RENDER_API) =
+        (module Concrete_ident.MakeRenderAPI (CoqNamePolicy))
+
       method private primitive_to_string (id : primitive_ident) : document =
         match id with
         | Deref -> default_document_for "(TODO: Deref)"
@@ -435,7 +442,16 @@ struct
       method impl_ident ~goal ~name:_ = goal#p
 
       method impl_item ~ii_span:_ ~ii_generics:_ ~ii_v ~ii_ident ~ii_attrs:_ =
-        ii_ident#p ^^ space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi
+        string
+          ((* if local *)
+           (* then (RenderId.render ii_ident#v).name *)
+            (* else *)
+            match String.chop_prefix ~prefix:"impl__" (RenderId.render ii_ident#v).name with
+            | Some chopped ->
+              chopped
+            | None -> (RenderId.render ii_ident#v).name
+          ) ^^
+        (* ii_ident#v ^^ *) space ^^ string ":=" ^^ space ^^ ii_v#p ^^ semi
 
       method impl_item'_IIFn ~body ~params =
         if List.length params == 0 then body#p
@@ -570,7 +586,7 @@ struct
         if Attrs.is_erased super.attrs then empty
         else
           CoqNotation.instance
-            (name#p ^^ string "_"
+            (string (RenderId.render name#v).name ^^ string "_"
             ^^ string (Int.to_string ([%hash: item] super)))
             generics#p []
             (name#p ^^ concat_map_with ~pre:space (fun x -> parens x#p) args)
@@ -579,8 +595,11 @@ struct
                   (concat_map_with
                      ~pre:
                        (break 1
-                       ^^ string ("implaabbcc_" ^ (RenderId.render name#v).name)
-                       ^^ !^"_")
+                        ^^ string (module_name_from_path (RenderId.render name#v).path) ^^ !^"."
+                        ^^ string (match String.chop_prefix ~prefix:"t_" (RenderId.render name#v).name with
+                            | Some chopped -> chopped
+                            | _ -> (RenderId.render name#v).name)
+                       ^^ !^"__")
                      (fun x -> x#p)
                      items)
                ^^ break 1))
@@ -996,25 +1015,22 @@ struct
                arguments
           ^^ space ^^ string "->" ^^ space ^^ string "_"
 
+      method concrete_ident ~local (id : Concrete_ident_render_sig.rendered) :
+          document =
+        string
+          (if local
+           then id.name
+           else
+             module_name_from_path id.path ^ "." ^ id.name
+             (* String.concat ~sep:self#module_path_separator *)
+             (*   (id.path) ^ self#module_name_separator ^ [ id.name ] *)
+          )
+      (** [concrete_ident ~local id] prints a name without path if [local] is
+          true, otherwise it prints the full path, separated by
+          `module_path_separator`. *)
+
       (* method quote (quote : quote) : document = empty *)
       method module_path_separator = "."
-
-      method concrete_ident ~local:_ id : document =
-        match id.name with
-        | "not" -> !^"negb"
-        | "eq" -> !^"PartialEq_f_eq"
-        | "lt" -> !^"PartialOrd_f_lt"
-        | "gt" -> !^"PartialOrd_f_gt"
-        | "le" -> !^"PartialOrd_f_le"
-        | "ge" -> !^"PartialOrd_f_ge"
-        | "rem" -> !^"Rem_f_rem"
-        | "add" -> !^"Add_f_add"
-        | "sub" -> !^"Sub_f_sub"
-        | "mul" -> !^"Mul_f_mul"
-        | "div" -> !^"Div_f_div"
-        | "index" -> !^"Index_f_index"
-        | "f_to_string" -> CoqNotation.comment !^"f_to_string"
-        | x -> !^x
     end
 
   let new_printer : BasePrinter.finalized_printer =
@@ -1046,10 +1062,7 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
   in
   (groupped_items
   |> List.map ~f:(fun (ns, items) ->
-         let mod_name =
-           String.concat ~sep:"_"
-             (List.map ~f:(map_first_letter String.uppercase) ns)
-         in
+         let mod_name = module_name_from_path ns in
          let sourcemap, contents =
            let annotated = my_printer#entrypoint_modul items in
            let open Generic_printer.AnnotatedString in

engine/lib/concrete_ident/concrete_ident.ml

@@ -578,16 +578,13 @@ module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct
          * Types.impl_infos option*)
       | `AssociatedItem
           ((`Type n | `Const n | `Fn n), `Impl (d, `Trait, impl_infos))
-        when not final ->
+        when (not final) || NP.prefix_associated_item_with_trait_name ->
           Concat
-            (prefix "f" (dstr n), render_impl_name ~always:true d impl_infos)
+            ( render_impl_name ~always:(not final) d impl_infos,
+              prefix "f" (dstr n) )
       (* Print the name of an associated item in a trait impl *)
-      | `AssociatedItem
-          ((`Type n | `Const n | `Fn n), `Impl (d, `Trait, impl_infos)) ->
-          if NP.prefix_associated_item_with_trait_name then
-            Concat
-              (render_impl_name ~always:true d impl_infos, prefix "f" (dstr n))
-          else prefix "f" (dstr n)
+      | `AssociatedItem ((`Type n | `Const n | `Fn n), `Impl (_, `Trait, _)) ->
+          prefix "f" (dstr n)
       | `AssociatedItem ((`Type n | `Const n | `Fn n), `Trait (trait_name, _))
         ->
           if NP.prefix_associated_item_with_trait_name then

examples/coverage/proofs/coq/extraction/Coverage.v

@@ -0,0 +1,16 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+From Core Require Import Core.
+
+
+
+(* NotImplementedYet *)

examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v

@@ -0,0 +1,121 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+From Core Require Import Core.
+
+(* NotImplementedYet *)
+
+Record C_test__Foo_Qux_record (v_T : Type) (v_N : t_usize) `{Core_Marker.t_Sized (v_T)} : Type :=
+  {
+    C_test__Foo_Qux_test__f_Foo_x : v_T;
+    C_test__Foo_Qux_test__f_Foo_y : t_Array (v_T) (v_N);
+    C_test__Foo_Qux_test__f_Foo_z : t_u8;
+  }.
+Arguments Build_C_test__Foo_Qux_record {_} {_} {_}.
+Arguments C_test__Foo_Qux_test__f_Foo_x {_} {_} {_}.
+Arguments C_test__Foo_Qux_test__f_Foo_y {_} {_} {_}.
+Arguments C_test__Foo_Qux_test__f_Foo_z {_} {_} {_}.
+#[export] Instance settable_C_test__Foo_Qux_record `{v_T : Type} `{v_N : t_usize} `{Core_Marker.t_Sized (v_T)} : Settable _ :=
+  settable! (Build_C_test__Foo_Qux_record (v_T := v_T) (v_N := v_N)) <C_test__Foo_Qux_test__f_Foo_x; C_test__Foo_Qux_test__f_Foo_y; C_test__Foo_Qux_test__f_Foo_z>.
+Inductive test__t_Foo (v_T : Type) (v_N : t_usize) `{Core_Marker.t_Sized (v_T)} : Type :=
+| C_test__Foo_Bar : t_u8 -> _
+| C_test__Foo_Baz
+| C_test__Foo_Qux : C_test__Foo_Qux_record  v_T v_N -> _.
+Arguments C_test__Foo_Bar {_} {_} {_}.
+Arguments C_test__Foo_Baz {_} {_} {_}.
+Arguments C_test__Foo_Qux {_} {_} {_}.
+
+Inductive test__t_AnimalA : Type :=
+| C_test__AnimalA_Dog
+| C_test__AnimalA_Cat.
+
+
+
+Definition test__t_AnimalA_cast_to_repr (x : test__t_AnimalA) : t_isize :=
+  match x with
+  | C_test__AnimalA_Dog =>
+    (0 : t_isize)
+  | C_test__AnimalA_Cat =>
+    (1 : t_isize)
+  end.
+
+Record C_test__AnimalB_Cat_record : Type :=
+  {
+    C_test__AnimalB_Cat_test__f_AnimalB_name : Alloc_String.t_String;
+    C_test__AnimalB_Cat_test__f_AnimalB_weight : float;
+  }.
+
+
+
+#[export] Instance settable_C_test__AnimalB_Cat_record : Settable _ :=
+  settable! (Build_C_test__AnimalB_Cat_record) <C_test__AnimalB_Cat_test__f_AnimalB_name; C_test__AnimalB_Cat_test__f_AnimalB_weight>.
+Inductive test__t_AnimalB : Type :=
+| C_test__AnimalB_Dog : Alloc_String.t_String -> float -> _
+| C_test__AnimalB_Cat : C_test__AnimalB_Cat_record  -> _.
+
+
+
+Record C_test__Examples_StructLike_record : Type :=
+  {
+    C_test__Examples_StructLike_test__f_Examples_value : t_i32;
+  }.
+
+
+#[export] Instance settable_C_test__Examples_StructLike_record : Settable _ :=
+  settable! (Build_C_test__Examples_StructLike_record) <C_test__Examples_StructLike_test__f_Examples_value>.
+Inductive test__t_Examples : Type :=
+| C_test__Examples_UnitLike
+| C_test__Examples_TupleLike : t_i32 -> _
+| C_test__Examples_StructLike : C_test__Examples_StructLike_record  -> _.
+
+
+
+
+Definition test '(_ : unit) : unit :=
+  let x : test__t_Foo ((t_u8)) ((12 : t_usize)) := C_test__Foo_Baz in
+  let _ := tt in
+  let a : test__t_AnimalA := C_test__AnimalA_Dog in
+  let a := C_test__AnimalA_Cat in
+  let _ := tt in
+  let a : test__t_AnimalB := C_test__AnimalB_Dog (Alloc_String.ToString__f_to_string (("Cocoa"%string : string))) ((37.2%float : float)) in
+  let a := C_test__AnimalB_Cat {| C_test__AnimalB_Cat_test__f_AnimalB_name := (Alloc_String.ToString__f_to_string (("Spotty"%string : string))); C_test__AnimalB_Cat_test__f_AnimalB_weight := ((2.7%float : float)) |} in
+  let _ := tt in
+  let x := C_test__Examples_UnitLike in
+  let x := C_test__Examples_UnitLike in
+  let y := C_test__Examples_TupleLike ((123 : t_i32)) in
+  let y := C_test__Examples_TupleLike ((123 : t_i32)) in
+  let z := C_test__Examples_StructLike {| C_test__Examples_StructLike_test__f_Examples_value := ((123 : t_i32)) |} in
+  let _ := tt in
+  tt.
+
+Record C_test__Enum_Struct_record : Type :=
+  {
+    C_test__Enum_Struct_test__f_Enum_a : t_u8;
+    C_test__Enum_Struct_test__f_Enum_b : t_u16;
+  }.
+
+
+
+#[export] Instance settable_C_test__Enum_Struct_record : Settable _ :=
+  settable! (Build_C_test__Enum_Struct_record) <C_test__Enum_Struct_test__f_Enum_a; C_test__Enum_Struct_test__f_Enum_b>.
+Inductive test__t_Enum : Type :=
+| C_test__Enum_Unit
+| C_test__Enum_Tuple : t_u16 -> _
+| C_test__Enum_Struct : C_test__Enum_Struct_record  -> _.
+
+
+
+
+Definition test__Enum_Unit__anon_const_0 : t_u8 :=
+  (3 : t_u8).
+
+Definition test__Enum_Struct__anon_const_0 : t_u8 :=
+  (1 : t_u8).

examples/coverage/proofs/coq/extraction/Coverage_Test_primitives.v

@@ -0,0 +1,35 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+From Core Require Import Core.
+
+(* NotImplementedYet *)
+
+Definition test_primtives '(_ : unit) : unit :=
+  let _ : bool := (false : bool) in
+  let _ : bool := (true : bool) in
+  let _ : t_u8 := (12 : t_u8) in
+  let _ : t_u16 := (123 : t_u16) in
+  let _ : t_u32 := (1234 : t_u32) in
+  let _ : t_u64 := (12345 : t_u64) in
+  let _ : t_u128 := (123456 : t_u128) in
+  let _ : t_usize := (32 : t_usize) in
+  let _ : t_i8 := (-12 : t_i8) in
+  let _ : t_i16 := (123 : t_i16) in
+  let _ : t_i32 := (-1234 : t_i32) in
+  let _ : t_i64 := (12345 : t_i64) in
+  let _ : t_i128 := (123456 : t_i128) in
+  let _ : t_isize := (-32 : t_isize) in
+  let _ : float := (1.2%float : float) in
+  let _ : float := ((-1.23)%float : float) in
+  let _ : ascii := ("c"%char : ascii) in
+  let _ : string := ("hello world"%string : string) in
+  tt.