From cc4d0cb6508f2dc366cc150ebd732c2b3d1fc0b2 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 20 Jun 2024 11:43:47 +0200 Subject: [PATCH] fix(engine): `Concrete_ident_generated`: rename `name` to `t`, derive more --- engine/backends/proverif/proverif_backend.ml | 8 ++++---- engine/lib/concrete_ident/concrete_ident.ml | 3 ++- engine/lib/concrete_ident/concrete_ident.mli | 4 +++- engine/lib/phases/phase_simplify_question_marks.ml | 4 ++-- engine/lib/phases/phase_specialize.ml | 8 ++++---- engine/names/extract/build.rs | 6 ++++-- 6 files changed, 19 insertions(+), 14 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 84eb582e1..241ac6845 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/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 diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 35907afa2..c8a1a49ec 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/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 diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index 1160da3be..8a5e413eb 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/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 diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml index 4182a43d2..7426b15b9 100644 --- a/engine/lib/phases/phase_simplify_question_marks.ml +++ b/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 diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index dd89b956e..fc8021dd1 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/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 () diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs index 4c25e6e53..209c9227d 100644 --- a/engine/names/extract/build.rs +++ b/engine/names/extract/build.rs @@ -91,7 +91,7 @@ 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}")) @@ -99,6 +99,8 @@ fn reader_to_str(s: String) -> String { .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}"))