[ProVerif] Renaming / AST transformation pseudophase

engine/backends/proverif/proverif_backend.ml

@@ -18,6 +18,13 @@ include
  let backend = Diagnostics.Backend.ProVerif
  end)
 
+module ConcreteIdentMap = Map.M (Concrete_ident_generated)
+
+let rename_map =
+ Map.of_alist_exn
+ (module Concrete_ident_generated)
+ Concrete_ident_generated.[ (Core__option__Option, "Option") ]
+
 module SubtypeToInputLanguage
  (FA : Features.T
  (* type loop = Features.Off.loop *)
@@ -147,20 +154,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
@@ -638,13 +645,19 @@ module Make (Options : OPTS) : MAKE = struct
 
  method! concrete_ident' ~(under_current_ns : bool) : concrete_ident fn =
  fun id ->
- if under_current_ns then print#name_of_concrete_ident id
- else
- let crate, path = print#namespace_of_concrete_ident id in
- let full_path = crate :: path in
- separate_map (underscore ^^ underscore) utf8string full_path
- ^^ underscore ^^ underscore
- ^^ print#name_of_concrete_ident id
+ match
+ List.find (Map.to_alist rename_map) ~f:(fun (name, _) ->
+ Concrete_ident.eq_name name id)
+ with
+ | Some (_, plain_name) -> string plain_name
+ | _ ->
+ if under_current_ns then print#name_of_concrete_ident id
+ else
+ let crate, path = print#namespace_of_concrete_ident id in
+ let full_path = crate :: path in
+ separate_map (underscore ^^ underscore) utf8string full_path
+ ^^ underscore ^^ underscore
+ ^^ print#name_of_concrete_ident id
 
  method! doc_construct_inductive
  : is_record:bool ->
@@ -726,17 +739,6 @@ module Make (Options : OPTS) : MAKE = struct
  | TApp { ident; args }
  when Global_ident.eq_name Alloc__vec__Vec ident ->
  string "bitstring"
- | TApp { ident; args }
- when Global_ident.eq_name Core__option__Option ident ->
- string "Option"
- | TApp { ident; args }
- when Global_ident.eq_name Core__result__Result ident -> (
- (* print first of args*)
- let result_ok_type = List.hd_exn args in
- match result_ok_type with
- | GType typ -> print#ty ctx typ
- | GConst e -> print#expr ctx e
- | _ -> empty (* Do not tranlsate lifetimes *))
  | TApp { ident; args } -> super#ty ctx ty
  (*(
  match translate_known_name ident ~dict:library_types with
@@ -861,6 +863,33 @@ module Make (Options : OPTS) : MAKE = struct
  end)
 end
 
+module ProVerifRename (F : Features.T) =
+ Phase_utils.MakeMonomorphicPhase
+ (F)
+ (struct
+ module Visitors = Ast_visitors.Make (F)
+ open Ast.Make (F)
+
+ let visitor =
+ object (self)
+ inherit [_] Visitors.map as super
+
+ method! visit_ty () (ty : ty) =
+ match super#visit_ty () ty with
+ | TApp { ident; args = [ GType typ; _ ] }
+ when Global_ident.eq_name Core__result__Result ident ->
+ typ
+ | TApp { ident; args }
+ when Map.existsi rename_map ~f:(fun ~key ~data:_ ->
+ Global_ident.eq_name key ident) ->
+ TApp { ident; args = [] }
+ | x -> x
+ end
+
+ let phase_id = Diagnostics.Phase.ProVerifRename
+ let ditems = List.map ~f:(visitor#visit_item ())
+ end)
+
 let translate m (bo : BackendOptions.t) (items : AST.item list) :
  Types.file list =
  let (module M : MAKE) =
@@ -899,8 +928,9 @@ module TransformToInputLanguage =
  |> Phases.Simplify_match_return
  |> Phases.Drop_needless_returns
  |> Phases.Local_mutation
- |> Phases.Reject.Continue
- |> SubtypeToInputLanguage
+ |> Phases.Reject.Continue
+ |> ProVerifRename
+ |> SubtypeToInputLanguage
  |> Identity
  ]
  [@ocamlformat "disable"]

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/diagnostics.ml

@@ -47,6 +47,7 @@ module Phase = struct
  | DropNeedlessReturns
  | TransformHaxLibInline
  | NewtypeAsRefinement
+ | ProVerifRename
  | DummyA
  | DummyB
  | DummyC

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

@@ -92,14 +92,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 {
@@ -108,7 +110,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}"))