From 3b25cdd34516b1b89f265624003c518922727edc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 1 May 2022 16:03:40 +0200
Subject: Perform more renamings

---
 src/ExtractToFStar.ml |  2 +-
 src/PrintPure.ml      |  8 ++++----
 src/Pure.ml           | 14 ++++++--------
 src/SymbolicToPure.ml |  6 +++---
 4 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index e00a4e53..0bcf66bd 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -986,7 +986,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
 
 (** Subcase of the app case: ADT field projector.  *)
 and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (original_app : texpression) (proj : proj_kind)
+    (inside : bool) (original_app : texpression) (proj : projection)
     (_proj_type_params : ty list) (args : texpression list) : unit =
   (* We isolate the first argument (if there is), in order to pretty print the
    * projection (`x.field` instead of `MkAdt?.field x` *)
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index b29f6e70..2da653bb 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -201,12 +201,12 @@ let var_to_string (fmt : type_formatter) (v : var) : string =
   let varname = var_to_varname v in
   "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")"
 
-let rec projection_to_string (fmt : ast_formatter) (inside : string)
-    (p : projection) : string =
+let rec mprojection_to_string (fmt : ast_formatter) (inside : string)
+    (p : mprojection) : string =
   match p with
   | [] -> inside
   | pe :: p' -> (
-      let s = projection_to_string fmt inside p' in
+      let s = mprojection_to_string fmt inside p' in
       match pe.pkind with
       | E.ProjOption variant_id ->
           assert (variant_id = T.option_some_id);
@@ -232,7 +232,7 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
    * regular places use indices for the pure variables: we want to make
    * this explicit, otherwise it is confusing. *)
   let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in
-  projection_to_string fmt name p.projection
+  mprojection_to_string fmt name p.projection
 
 let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
     (variant_id : VariantId.id option) : string =
diff --git a/src/Pure.ml b/src/Pure.ml
index 3798c555..9cf7a077 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -152,15 +152,15 @@ type var = {
  * Also: tuples...
  * Rmk: projections are actually only used as meta-data.
  * *)
-type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
+type mprojection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
 [@@deriving show]
 
-type projection = projection_elem list [@@deriving show]
+type mprojection = mprojection_elem list [@@deriving show]
 
 type mplace = {
   var_id : V.VarId.id;
   name : string option;
-  projection : projection;
+  projection : mprojection;
 }
 [@@deriving show]
 (** "Meta" place.
@@ -360,17 +360,15 @@ type adt_cons_id = { adt_id : type_id; variant_id : variant_id option }
 [@@deriving show]
 (** An identifier for an ADT constructor *)
 
-type proj_kind = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
-(** Projection kind - For now we don't support projection of tuple fields 
+type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
+(** Projection - For now we don't support projection of tuple fields 
     (because not all the backends have syntax for this).
-    
-    TODO: rename
  *)
 
 type qualif_id =
   | Func of fun_id
   | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
-  | Proj of proj_kind  (** Field projector *)
+  | Proj of projection  (** Field projector *)
 [@@deriving show]
 
 type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 64b3929f..14a844a1 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -808,13 +808,13 @@ let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : texpression list =
   log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs));
   List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
 
-let translate_mprojection_elem (pe : E.projection_elem) : projection_elem option
-    =
+let translate_mprojection_elem (pe : E.projection_elem) :
+    mprojection_elem option =
   match pe with
   | Deref | DerefBox -> None
   | Field (pkind, field_id) -> Some { pkind; field_id }
 
-let translate_mprojection (p : E.projection) : projection =
+let translate_mprojection (p : E.projection) : mprojection =
   List.filter_map translate_mprojection_elem p
 
 (** Translate a "meta"-place *)
-- 
cgit v1.2.3