Better documentation for new naming.

engine/lib/concrete_ident/concrete_ident.ml

@@ -184,7 +184,7 @@ let to_view (ident : t) : Concrete_ident_view.t =
   in
   { mod_path; rel_path }
 
-(** Stateful store that maps [def_id]s to implementation informations
+(** Stateful store that maps [def_id]s to implementation information
 (which trait is implemented? for which type? under which constraints?) *)
 module ImplInfoStore = struct
   include Explicit_def_id.ImplInfoStore
@@ -195,18 +195,16 @@ end
 module MakeToString (R : VIEW_RENDERER) = struct
   open Concrete_ident_render_sig
 
-  (** For each module namespace, we store three different pieces of data:
-      - a map from relative paths (i.e. the non-module part of a path) to full
-        identifiers
-      - an set of rendered names in this namespace
+  (** For each module namespace, we store two different pieces of data:
+      - a set of rendered names in this namespace
       - a memoization map from full identifiers to rendered names
 
       If an identifier was already rendered, we just use this already rendered
       name.
 
       Otherwise, when we print a name under a fresh module, we take a look at
-      the first map: if there is already an identifier in the fresh module with
-      the exact same relative path, then we have a collision, and we need to
+      the set: if there is already an identifier in the fresh module with
+      the exact same rendered name, then we have a collision, and we need to
       generate a fresh name.
 
       To generate a fresh name, we use the set of rendered names.
@@ -466,7 +464,7 @@ module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct
         else rendered
     end
 
-    (** [pretty_impl_name ~namespace impl_infos] computes a pretty impl name given impl informations and a namespace.
+    (** [pretty_impl_name ~namespace impl_infos] computes a pretty impl name given impl information and a namespace.
         A pretty name can be computed when:
         - (1) the impl, (2) the type and (3) the trait implemented all live in the same namespace
         - the impl block has no generics

engine/lib/concrete_ident/concrete_ident.mli

@@ -47,7 +47,7 @@ val eq_name : name -> t -> bool
 (** [eq_name name identifier] is true whenever [identifier] is [name].  *)
 
 val to_debug_string : t -> string
-(** Format a identifier as a (ppx) debug string. The default debug pretty prints the identifier. *)
+(** Format an identifier as a (ppx) debug string. The default debug pretty prints the identifier. *)
 
 val fresh_module : label:string -> t list -> Fresh_module.t
 (** [fresh_module ~label hints] creates a fresh module given a non-empty list of
@@ -72,6 +72,7 @@ val map_path_strings : f:(string -> string) -> t -> t
   any integer type, please do not use it elsewhere. *)
 
 val is_constructor : t -> bool
+(** Returns true if the ident represents a constructor. *)
 
 type comparator_witness
 
@@ -90,7 +91,7 @@ module ImplInfoStore : sig
   val init : (Types.def_id * Types.impl_infos) list -> unit
 
   val lookup_raw : t -> Types.impl_infos option
-  (** Lookup the (raw[1]) implementation informations given a concrete
+  (** Lookup the (raw[1]) implementation information given a concrete
   ident. Returns `Some _` if and only if the supplied identifier points
   to an `Impl`.
   

engine/lib/concrete_ident/concrete_ident_view.ml

@@ -1,10 +1,10 @@
 open! Prelude
 include Concrete_ident_view_types
 
-(** Rust paths comes with invariants (e.g. a function is always a `ValueNs _`), this function raises an error if a path doesn't respect those. *)
+(** Rust paths come with invariants (e.g. a function is always a `ValueNs _`), this function raises an error if a path doesn't respect those. *)
 let broken_invariant (type t) msg (did : Explicit_def_id.t) : t =
   let msg =
-    "Explicit_def_id: an invariant have been broken. Expected " ^ msg
+    "Explicit_def_id: an invariant has been broken. Expected " ^ msg
     ^ ".\n\ndid="
     ^ [%show: Explicit_def_id.t] did
   in
@@ -131,8 +131,8 @@ let rec poly :
     | SyntheticCoroutineBody ->
         (* It should be impossible for such items to ever be referenced by anyting in hax. *)
         broken_invariant
-          "non (TyAlias | TyParam | ConstParam | InlineConst | LifetimeParam | \
-           Closure | SyntheticCoroutineBody) identifier"
+          "non (TyParam | ConstParam | InlineConst | LifetimeParam | Closure | \
+           SyntheticCoroutineBody) identifier"
           did
   in
   result
@@ -156,7 +156,7 @@ let of_def_id (did : Explicit_def_id.t) : t =
          (Explicit_def_id.parents did |> List.rev)
      in *)
   (* `rest` is a list of identifiers of items nested each in the others. *)
-  (* We want to process those items begining with most nested one. *)
+  (* We want to process those items beginning with most nested one. *)
   (* let rest = List.rev rest in *)
   (* We distinguish between:
      - a chain of identifiers that have a relation with each other (e.g. if `k::E::C` is a constructor and `k::E` a enum)
@@ -200,6 +200,8 @@ let of_def_id (did : Explicit_def_id.t) : t =
                  "A `Mod` identifier must a `TypeNs` as its last path" m)
          ns_chunks
   in
+  (* This is a hack: we remove a prefix that we add in
+     https://github.com/cryspen/hax/blob/02d67770f2626e4bb27fc2a1ba9cfe612819d4a8/hax-lib/macros/src/implementation.rs#L897 *)
   let mod_path =
     List.filter mod_path ~f:(fun ds ->
         String.is_prefix ds.data ~prefix:"hax__autogenerated_refinement_" |> not)

engine/lib/concrete_ident/concrete_ident_view_types.ml

@@ -2,19 +2,19 @@ open! Prelude
 
 (** This modules defines what is the view over a concrete identifiers.
 
-    Hax manipulates concrete identifiers (that is global identifiers refering to
+    Hax manipulates concrete identifiers (that is global identifiers referring to
     concrete Rust items -- not built-in operators) as raw Rust identifiers
     augmented with some metadata.
 
     Rust represents identifiers as a crate and a path. Each chunk of the path is
-    roughly a level of nest in Rust. The path lacks informations about
+    roughly a level of nest in Rust. The path lacks information about
     definition kinds.
 
     There is two kinds of nesting for items.
-    - Confort: e.g. the user decides to embed a struct within a function to work
+    - Comfort: e.g. the user decides to embed a struct within a function to work
       with it locally.
     - Relational: e.g. an associated method has to be under a trait, or a field
-      as to be under a constructor.
+      has to be under a constructor.
 
     This module provides a view to those paths: a path in the view is a list of
     smaller relational paths. For instance, consider the following piece of
@@ -33,7 +33,7 @@ open! Prelude
     ]}
 
     Here, the Rust raw definition identifier of [LocalStruct] is roughly
-    [a::my_crate::<Impl 0>::assoc_fn::LocalStruct::field].
+    [my_crate::a::<Impl 0>::assoc_fn::LocalStruct::field].
 
     The view for [LocalStruct] looks like:
     [{
@@ -102,7 +102,7 @@ module RelPath = struct
 
     and 'name maybe_associated = [ `Fn of 'name | `Const of 'name ]
     [@@deriving show, hash, compare, sexp, hash, eq, map]
-    (** Helper type for function and constants: those exists both as associated
+    (** Helper type for function and constants: those exist both as associated
       in an impl block or a trait, and as standalone. *)
 
     type 'name associated = [ 'name maybe_associated | `Type of 'name ]

engine/lib/concrete_ident/explicit_def_id.ml

@@ -90,7 +90,7 @@ let rec parents (did : t) =
 let to_def_id { def_id; _ } = def_id
 let is_constructor { is_constructor; _ } = is_constructor
 
-(** Stateful store that maps [def_id]s to implementation informations
+(** Stateful store that maps [def_id]s to implementation information
 (which trait is implemented? for which type? under which constraints?) *)
 module ImplInfoStore = struct
   let state : (Types.def_id_contents, Types.impl_infos) Hashtbl.t option ref =

engine/lib/concrete_ident/explicit_def_id.mli

@@ -8,8 +8,8 @@ open! Prelude
     struct S;
     fn f() -> S { S }
     ```
-    Here, the return type of `f` (that is, `S`) and the constructor `S` in the body of `f` refers to the exact same identifier `mycrate::S`.
-    Yet, they denotes two very different objects: a type versus a constructor.
+    Here, the return type of `f` (that is, `S`) and the constructor `S` in the body of `f` refer to the exact same identifier `mycrate::S`.
+    Yet, they denote two very different objects: a type versus a constructor.
 
     [ExplicitDefId.t] clears up this ambiguity, making constructors and types two separate things.
 
@@ -32,9 +32,9 @@ val of_def_id : ?constructor:bool -> Types.def_id -> t option
   *)
 
 val of_def_id_exn : ?constructor:bool -> Types.def_id -> t
-(** Exception-throwing variant of [make].
+(** Exception-throwing variant of [of_def_id].
       This should be used when we know statically that the conditions 
-      described in the documentation of [make] are met. 
+      described in the documentation of [of_def_id] are met. 
 
       For instance, with static [Types.def_id]s or in [Import_thir].
   *)
@@ -70,7 +70,7 @@ module ImplInfoStore : sig
   val init : (Types.def_id * Types.impl_infos) list -> unit
 
   val lookup_raw : t -> Types.impl_infos option
-  (** Lookup the (raw[1]) implementation informations given a concrete
+  (** Lookup the (raw[1]) implementation information given a concrete
   ident. Returns `Some _` if and only if the supplied identifier points
   to an `Impl`.
   

engine/lib/concrete_ident/impl_infos.ml

@@ -11,7 +11,7 @@ type t = {
 }
 (** metadata of an [impl] block *)
 
-(** Lookup the implementation informations given a concrete
+(** Lookup the implementation information given a concrete
 ident. Returns [Some _] if and only if the supplied identifier points
 to an [Impl].