Merge pull request #727 from hacspec/refactor-concrete-ident-generated

fix(engine): `Concrete_ident_generated`: `name` -> `t`, derive more

engine/backends/proverif/proverif_backend.ml

@@ -147,20 +147,20 @@ module Make (Options : OPTS) : MAKE = struct
 
     (* TODO: Give definitions for core / known library functions, cf issues #447, #448 *)
     let library_functions :
-        (Concrete_ident_generated.name * (AST.expr list -> document)) list =
+        (Concrete_ident_generated.t * (AST.expr list -> document)) list =
       []
 
     let library_constructors :
-        (Concrete_ident_generated.name
+        (Concrete_ident_generated.t
         * ((global_ident * AST.expr) list -> document))
         list =
       []
 
     let library_constructor_patterns :
-        (Concrete_ident_generated.name * (field_pat list -> document)) list =
+        (Concrete_ident_generated.t * (field_pat list -> document)) list =
       []
 
-    let library_types : (Concrete_ident_generated.name * document) list = []
+    let library_types : (Concrete_ident_generated.t * document) list = []
 
     let assoc_known_name name (known_name, _) =
       Global_ident.eq_name known_name name

engine/lib/concrete_ident/concrete_ident.ml

@@ -420,7 +420,8 @@ module T = struct
   let hash x = [%hash: Imported.def_id] x.def_id
   let hash_fold_t s x = Imported.hash_fold_def_id s x.def_id
 
-  type name = Concrete_ident_generated.name
+  type name = Concrete_ident_generated.t
+  [@@deriving show, yojson, compare, sexp, eq, hash]
 
   let of_name k = Concrete_ident_generated.def_id_of >> of_def_id k
 

engine/lib/concrete_ident/concrete_ident.mli

@@ -1,5 +1,7 @@
 type t [@@deriving show, yojson, compare, sexp, eq, hash]
-type name = Concrete_ident_generated.name
+
+type name = Concrete_ident_generated.t
+[@@deriving show, yojson, compare, sexp, eq, hash]
 
 module ImplInfoStore : sig
   val init : (Types.def_id * Types.impl_infos) list -> unit

engine/lib/phases/phase_simplify_question_marks.ml

@@ -106,8 +106,8 @@ module%inlined_contents Make (FA : Features.T) = struct
         Some call
 
       let mk_pconstruct ~is_struct ~is_record ~span ~typ
-          (constructor : Concrete_ident_generated.name)
-          (fields : (Concrete_ident_generated.name * pat) list) =
+          (constructor : Concrete_ident_generated.t)
+          (fields : (Concrete_ident_generated.t * pat) list) =
         let name =
           Global_ident.of_name (Constructor { is_struct }) constructor
         in

engine/lib/phases/phase_specialize.ml

@@ -17,8 +17,8 @@ module Make (F : Features.T) =
         open Concrete_ident_generated
 
         type pattern = {
-          fn : name;
-          fn_replace : name;
+          fn : t;
+          fn_replace : t;
           args : (expr -> bool) list;
           ret : ty -> bool;
         }
@@ -30,7 +30,7 @@ module Make (F : Features.T) =
 
         (** Constructs a predicate out of predicates and names *)
         let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate)
-            (fn : name) (fn_replace : name) : pattern =
+            (fn : t) (fn_replace : t) : pattern =
           let args = List.map ~f:(fun p x -> p x |> Option.is_some) args in
           let ret t = ret t |> Option.is_some in
           { fn; fn_replace; args; ret }
@@ -51,7 +51,7 @@ module Make (F : Features.T) =
            fun ~eq x x' -> if eq x x' then Some x' else None
 
           let eq_global_ident :
-              name -> (Ast.Global_ident.t, Ast.Global_ident.t) predicate =
+              t -> (Ast.Global_ident.t, Ast.Global_ident.t) predicate =
             eq ~eq:Ast.Global_ident.eq_name
 
           let erase : 'a. ('a, unit) predicate = fun _ -> Some ()

engine/names/extract/build.rs

@@ -91,14 +91,16 @@ fn reader_to_str(s: String) -> String {
     const TAB: &str = "    ";
     let mut result = String::new();
     result += &format!(
-        "type name = \n{TAB}  {}\n",
+        "type t = \n{TAB}  {}[@@deriving show, yojson, compare, sexp, eq, hash]\n",
         def_ids
             .iter()
             .map(|(_, def_name)| format!("{def_name}"))
             .collect::<Vec<_>>()
             .join(&format!("\n{TAB}| "))
     );
 
+    result += "\n";
+    result += "include (val Base.Comparator.make ~compare ~sexp_of_t)";
     result += "\n";
     result += "module Values = struct\n";
     for (json, name) in &def_ids {
@@ -107,7 +109,7 @@ fn reader_to_str(s: String) -> String {
     result += "end\n\n";
 
     result += &format!(
-        "let def_id_of: name -> Types.def_id = function\n{TAB}  {}\n\n",
+        "let def_id_of: t -> Types.def_id = function\n{TAB}  {}\n\n",
         def_ids
             .iter()
             .map(|(_, n)| format!("{n} -> Values.parsed_{n}"))