From 26c25bf375742cf4d5a0ab160b9646e90c067f18 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 18 Aug 2023 10:27:55 +0200
Subject: Update following the introduction of ConstantExpr

---
 compiler/Contexts.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2ca5653d..14b5d559 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -263,6 +263,10 @@ type eval_ctx = {
   region_groups : RegionGroupId.id list;
   type_vars : type_var list;
   const_generic_vars : const_generic_var list;
+  const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
+      (** The map from const generic vars to their values. Those values
+          can be symbolic values or concrete values (in the latter case:
+          if we run in interpreter mode) *)
   env : env;
   ended_regions : RegionId.Set.t;
 }
@@ -312,6 +316,11 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
 let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
   env_lookup_var_value ctx.env vid
 
+(** Retrieve a const generic value in an evaluation context *)
+let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
+    : typed_value =
+  Types.ConstGenericVarId.Map.find vid ctx.const_generic_vars_map
+
 (** Update a variable's value in the current frame.
 
     This is a helper function: it can break invariants and doesn't perform
-- 
cgit v1.2.3


From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 12:47:43 +0200
Subject: Start adding support for traits

---
 compiler/Contexts.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 14b5d559..2d396924 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -255,11 +255,28 @@ type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
 type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
 [@@deriving show]
 
+type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t }
+[@@deriving show]
+
+type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t }
+[@@deriving show]
+
+type decls_ctx = {
+  type_ctx : type_context;
+  fun_ctx : fun_context;
+  global_ctx : global_context;
+  trait_decls_ctx : trait_decls_context;
+  trait_impls_ctx : trait_impls_context;
+}
+[@@deriving show]
+
 (** Evaluation context *)
 type eval_ctx = {
   type_context : type_context;
   fun_context : fun_context;
   global_context : global_context;
+  trait_decls_context : trait_decls_context;
+  trait_impls_context : trait_impls_context;
   region_groups : RegionGroupId.id list;
   type_vars : type_var list;
   const_generic_vars : const_generic_var list;
@@ -267,6 +284,7 @@ type eval_ctx = {
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
           if we run in interpreter mode) *)
+  trait_clauses : etrait_ref list;
   env : env;
   ended_regions : RegionId.Set.t;
 }
@@ -308,6 +326,12 @@ let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
     global_decl =
   GlobalDeclId.Map.find gid ctx.global_context.global_decls
 
+let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl =
+  TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls
+
+let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
+  TraitImplId.Map.find id ctx.trait_impls_context.trait_impls
+
 (** Retrieve a variable's value in the current frame *)
 let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
   snd (env_lookup_var env vid)
-- 
cgit v1.2.3


From 06360698561019d7f480dcb4263e2099d9a03ca5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 1 Sep 2023 12:01:03 +0200
Subject: Implement the normalization functions in AssociatedTypes

---
 compiler/Contexts.ml | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2d396924..0719364e 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -270,6 +270,37 @@ type decls_ctx = {
 }
 [@@deriving show]
 
+(** A reference to a trait associated type *)
+type 'r trait_type_ref = { trait_ref : 'r trait_ref; type_name : string }
+[@@deriving show, ord]
+
+type etrait_type_ref = erased_region trait_type_ref [@@deriving show, ord]
+
+type rtrait_type_ref = Types.RegionId.id Types.region trait_type_ref
+[@@deriving show, ord]
+
+(* TODO: correctly use the functors so as not to have a duplication below *)
+module ETraitTypeRefOrd = struct
+  type t = etrait_type_ref
+
+  let compare = compare_etrait_type_ref
+  let to_string = show_etrait_type_ref
+  let pp_t = pp_etrait_type_ref
+  let show_t = show_etrait_type_ref
+end
+
+module RTraitTypeRefOrd = struct
+  type t = rtrait_type_ref
+
+  let compare = compare_rtrait_type_ref
+  let to_string = show_rtrait_type_ref
+  let pp_t = pp_rtrait_type_ref
+  let show_t = show_rtrait_type_ref
+end
+
+module ETraitTypeRefMap = Collections.MakeMap (ETraitTypeRefOrd)
+module RTraitTypeRefMap = Collections.MakeMap (RTraitTypeRefOrd)
+
 (** Evaluation context *)
 type eval_ctx = {
   type_context : type_context;
@@ -285,6 +316,18 @@ type eval_ctx = {
           can be symbolic values or concrete values (in the latter case:
           if we run in interpreter mode) *)
   trait_clauses : etrait_ref list;
+  norm_trait_etypes : ety ETraitTypeRefMap.t;
+      (** The normalized trait types (a map from trait types to their representatives).
+          Note that this doesn't support account higher-order types. *)
+  norm_trait_rtypes : rty RTraitTypeRefMap.t;
+      (** We need this because we manipulate two kinds of types.
+          Note that we actually forbid regions from appearing both in the trait
+          references and in the constraints given to the associated types,
+          meaning that we don't have to worry about mismatches due to changes
+          in region ids.
+
+          TODO: how not to duplicate?
+       *)
   env : env;
   ended_regions : RegionId.Set.t;
 }
-- 
cgit v1.2.3


From 1e39985a44646f1c352def6e4b29365a113a5dee Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 1 Sep 2023 14:43:11 +0200
Subject: Compute the normalized trait types maps and update Interpreter

---
 compiler/Contexts.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 0719364e..9d22a643 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -40,6 +40,7 @@ type dummy_var_id = DummyVarId.id [@@deriving show, ord]
     fn f x : fun_type =
       let id = fresh_id () in
       ...
+      fun () -> ...
    
     let g = f x in   // <-- the fresh identifier gets generated here
     let x1 = g () in // <-- no fresh generation here
@@ -315,7 +316,6 @@ type eval_ctx = {
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
           if we run in interpreter mode) *)
-  trait_clauses : etrait_ref list;
   norm_trait_etypes : ety ETraitTypeRefMap.t;
       (** The normalized trait types (a map from trait types to their representatives).
           Note that this doesn't support account higher-order types. *)
-- 
cgit v1.2.3


From 78a2731924aa13989998c6be4a5a6865ce5098aa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 07:33:30 +0200
Subject: Make minor modifications

---
 compiler/Contexts.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 9d22a643..df77959e 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -333,9 +333,21 @@ type eval_ctx = {
 }
 [@@deriving show]
 
+let lookup_type_var_opt (ctx : eval_ctx) (vid : TypeVarId.id) : type_var option
+    =
+  if TypeVarId.to_int vid < List.length ctx.type_vars then
+    Some (TypeVarId.nth ctx.type_vars vid)
+  else None
+
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
+let lookup_const_generic_var_opt (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
+    const_generic_var option =
+  if ConstGenericVarId.to_int vid < List.length ctx.const_generic_vars then
+    Some (ConstGenericVarId.nth ctx.const_generic_vars vid)
+  else None
+
 let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
     const_generic_var =
   ConstGenericVarId.nth ctx.const_generic_vars vid
-- 
cgit v1.2.3


From 60aa9ff5b31e47ecc2ac2dff55ee06582af62806 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 23:39:13 +0200
Subject: Fix some issues

---
 compiler/Contexts.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index df77959e..65760d94 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -5,6 +5,7 @@ open LlbcAst
 module V = Values
 open ValuesUtils
 open Identifiers
+module L = Logging
 
 (** The [Id] module for dummy variables.
 
@@ -17,6 +18,9 @@ IdGen ()
 
 type dummy_var_id = DummyVarId.id [@@deriving show, ord]
 
+(** The local logger *)
+let log = L.contexts_log
+
 (** Some global counters.
 
   Note that those counters were initially stored in {!eval_ctx} values,
@@ -449,6 +453,15 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
 *)
 let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
     =
+  log#ldebug
+    (lazy
+      ("push_vars:\n"
+      ^ String.concat "\n"
+          (List.map
+             (fun (var, value) ->
+               (* We can unfortunately not use Print because it depends on Contexts... *)
+               show_var var ^ " -> " ^ V.show_typed_value value)
+             vars)));
   assert (
     List.for_all
       (fun (var, (value : typed_value)) -> var.var_ty = value.ty)
-- 
cgit v1.2.3


From 47bc2ba74c90c1a29a081b8950022f74408f037e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 05:15:18 +0200
Subject: Merge trans_ctx and decls_ctx

---
 compiler/Contexts.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 65760d94..a5bc7dc0 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -255,7 +255,11 @@ type type_context = {
 }
 [@@deriving show]
 
-type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
+type fun_context = {
+  fun_decls : fun_decl FunDeclId.Map.t;
+  fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
+}
+[@@deriving show]
 
 type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
 [@@deriving show]
-- 
cgit v1.2.3


From 353a9627cf39290f2fe841a45e52726aa9fe6512 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 06:58:17 +0200
Subject: Normalize the function signatures before translation to pure

---
 compiler/Contexts.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a5bc7dc0..dac64a9a 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -288,6 +288,9 @@ type etrait_type_ref = erased_region trait_type_ref [@@deriving show, ord]
 type rtrait_type_ref = Types.RegionId.id Types.region trait_type_ref
 [@@deriving show, ord]
 
+type strait_type_ref = Types.RegionVarId.id Types.region trait_type_ref
+[@@deriving show, ord]
+
 (* TODO: correctly use the functors so as not to have a duplication below *)
 module ETraitTypeRefOrd = struct
   type t = etrait_type_ref
@@ -307,8 +310,18 @@ module RTraitTypeRefOrd = struct
   let show_t = show_rtrait_type_ref
 end
 
+module STraitTypeRefOrd = struct
+  type t = strait_type_ref
+
+  let compare = compare_strait_type_ref
+  let to_string = show_strait_type_ref
+  let pp_t = pp_strait_type_ref
+  let show_t = show_strait_type_ref
+end
+
 module ETraitTypeRefMap = Collections.MakeMap (ETraitTypeRefOrd)
 module RTraitTypeRefMap = Collections.MakeMap (RTraitTypeRefOrd)
+module STraitTypeRefMap = Collections.MakeMap (STraitTypeRefOrd)
 
 (** Evaluation context *)
 type eval_ctx = {
@@ -336,6 +349,13 @@ type eval_ctx = {
 
           TODO: how not to duplicate?
        *)
+  norm_trait_stypes : sty STraitTypeRefMap.t;
+      (** We sometimes need to normalize types in non-instantiated signatures.
+
+          Note that we either need to use the etypes/rtypes maps, or the stypes map.
+          This means that we either compute the maps for etypes and rtypes, or compute
+          the one for stypes (we don't always compute and carry all the maps).
+       *)
   env : env;
   ended_regions : RegionId.Set.t;
 }
-- 
cgit v1.2.3


From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 12 Nov 2023 19:28:56 +0100
Subject: Remove the 'r type variable from the ty type definition

---
 compiler/Contexts.ml | 239 +++++++++++++++------------------------------------
 1 file changed, 69 insertions(+), 170 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index dac64a9a..9a20a6cc 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -112,16 +112,16 @@ let reset_global_counters () =
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
-(** Ancestor for {!var_binder} iter visitor *)
-class ['self] iter_var_binder_base =
+(** Ancestor for {!env} iter visitor *)
+class ['self] iter_env_base =
   object (_self : 'self)
     inherit [_] iter_abs
     method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
     method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for {!var_binder} map visitor *)
-class ['self] map_var_binder_base =
+(** Ancestor for {!env} map visitor *)
+class ['self] map_env_base =
   object (_self : 'self)
     inherit [_] map_abs
     method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x
@@ -135,97 +135,29 @@ type var_binder = {
   index : var_id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
 }
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_var_binder";
-        variety = "iter";
-        ancestors = [ "iter_var_binder_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_var_binder";
-        variety = "map";
-        ancestors = [ "map_var_binder_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
 
 (** A binder, for a "real" variable or a dummy variable *)
-type binder = VarBinder of var_binder | DummyBinder of dummy_var_id
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_binder";
-        variety = "iter";
-        ancestors = [ "iter_var_binder" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_binder";
-        variety = "map";
-        ancestors = [ "map_var_binder" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
-
-(** Ancestor for {!env_elem} iter visitor *)
-class ['self] iter_env_elem_base =
-  object (_self : 'self)
-    inherit [_] iter_binder
-  end
-
-(** Ancestor for {!env_elem} map visitor *)
-class ['self] map_env_elem_base =
-  object (_self : 'self)
-    inherit [_] map_binder
-  end
+and binder = BVar of var_binder | BDummy of dummy_var_id
 
 (** Environment value: mapping from variable to value, abstraction (only
     used in symbolic mode) or stack frame delimiter.
-    
-    TODO: rename Var (-> Binding?)
  *)
-type env_elem =
-  | Var of binder * typed_value
+and env_elem =
+  | EBinding of binder * typed_value
       (** Variable binding - the binder is None if the variable is a dummy variable
           (we use dummy variables to store temporaries while doing bookkeeping such
            as ending borrows for instance). *)
-  | Abs of abs
-  | Frame
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_env_elem";
-        variety = "iter";
-        ancestors = [ "iter_env_elem_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_env_elem";
-        variety = "map";
-        ancestors = [ "map_env_elem_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
+  | EAbs of abs
+  | EFrame
 
-type env = env_elem list
+and env = env_elem list
 [@@deriving
   show,
     visitors
       {
         name = "iter_env";
         variety = "iter";
-        ancestors = [ "iter_env_elem" ];
+        ancestors = [ "iter_env_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
@@ -233,7 +165,7 @@ type env = env_elem list
       {
         name = "map_env";
         variety = "map";
-        ancestors = [ "map_env_elem" ];
+        ancestors = [ "map_env_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
@@ -280,48 +212,20 @@ type decls_ctx = {
 [@@deriving show]
 
 (** A reference to a trait associated type *)
-type 'r trait_type_ref = { trait_ref : 'r trait_ref; type_name : string }
-[@@deriving show, ord]
-
-type etrait_type_ref = erased_region trait_type_ref [@@deriving show, ord]
-
-type rtrait_type_ref = Types.RegionId.id Types.region trait_type_ref
-[@@deriving show, ord]
-
-type strait_type_ref = Types.RegionVarId.id Types.region trait_type_ref
+type trait_type_ref = { trait_ref : trait_ref; type_name : string }
 [@@deriving show, ord]
 
 (* TODO: correctly use the functors so as not to have a duplication below *)
-module ETraitTypeRefOrd = struct
-  type t = etrait_type_ref
+module TraitTypeRefOrd = struct
+  type t = trait_type_ref
 
-  let compare = compare_etrait_type_ref
-  let to_string = show_etrait_type_ref
-  let pp_t = pp_etrait_type_ref
-  let show_t = show_etrait_type_ref
+  let compare = compare_trait_type_ref
+  let to_string = show_trait_type_ref
+  let pp_t = pp_trait_type_ref
+  let show_t = show_trait_type_ref
 end
 
-module RTraitTypeRefOrd = struct
-  type t = rtrait_type_ref
-
-  let compare = compare_rtrait_type_ref
-  let to_string = show_rtrait_type_ref
-  let pp_t = pp_rtrait_type_ref
-  let show_t = show_rtrait_type_ref
-end
-
-module STraitTypeRefOrd = struct
-  type t = strait_type_ref
-
-  let compare = compare_strait_type_ref
-  let to_string = show_strait_type_ref
-  let pp_t = pp_strait_type_ref
-  let show_t = show_strait_type_ref
-end
-
-module ETraitTypeRefMap = Collections.MakeMap (ETraitTypeRefOrd)
-module RTraitTypeRefMap = Collections.MakeMap (RTraitTypeRefOrd)
-module STraitTypeRefMap = Collections.MakeMap (STraitTypeRefOrd)
+module TraitTypeRefMap = Collections.MakeMap (TraitTypeRefOrd)
 
 (** Evaluation context *)
 type eval_ctx = {
@@ -337,25 +241,10 @@ type eval_ctx = {
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
           if we run in interpreter mode) *)
-  norm_trait_etypes : ety ETraitTypeRefMap.t;
+  norm_trait_types : ty TraitTypeRefMap.t;
       (** The normalized trait types (a map from trait types to their representatives).
-          Note that this doesn't support account higher-order types. *)
-  norm_trait_rtypes : rty RTraitTypeRefMap.t;
-      (** We need this because we manipulate two kinds of types.
-          Note that we actually forbid regions from appearing both in the trait
-          references and in the constraints given to the associated types,
-          meaning that we don't have to worry about mismatches due to changes
-          in region ids.
-
-          TODO: how not to duplicate?
-       *)
-  norm_trait_stypes : sty STraitTypeRefMap.t;
-      (** We sometimes need to normalize types in non-instantiated signatures.
-
-          Note that we either need to use the etypes/rtypes maps, or the stypes map.
-          This means that we either compute the maps for etypes and rtypes, or compute
-          the one for stypes (we don't always compute and carry all the maps).
-       *)
+          Note that this doesn't take into account higher-order type constraints
+          (of the shape `for<'a> ...`). *)
   env : env;
   ended_regions : RegionId.Set.t;
 }
@@ -389,10 +278,10 @@ let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
     match env with
     | [] ->
         raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
-    | Var (VarBinder var, v) :: env' ->
+    | EBinding (BVar var, v) :: env' ->
         if var.index = vid then (var, v) else lookup env'
-    | (Var (DummyBinder _, _) | Abs _) :: env' -> lookup env'
-    | Frame :: _ -> raise (Failure "End of frame")
+    | (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
+    | EFrame :: _ -> raise (Failure "End of frame")
   in
   lookup env
 
@@ -440,11 +329,11 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
   let rec update env =
     match env with
     | [] -> raise (Failure "Unexpected")
-    | Var ((VarBinder b as var), v) :: env' ->
-        if b.index = vid then Var (var, nv) :: env'
-        else Var (var, v) :: update env'
-    | ((Var (DummyBinder _, _) | Abs _) as ee) :: env' -> ee :: update env'
-    | Frame :: _ -> raise (Failure "End of frame")
+    | EBinding ((BVar b as var), v) :: env' ->
+        if b.index = vid then EBinding (var, nv) :: env'
+        else EBinding (var, v) :: update env'
+    | ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
+    | EFrame :: _ -> raise (Failure "End of frame")
   in
   update env
 
@@ -466,9 +355,9 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
     is important).
 *)
 let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
-  assert (var.var_ty = v.ty);
+  assert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty);
   let bv = var_to_binder var in
-  { ctx with env = Var (VarBinder bv, v) :: ctx.env }
+  { ctx with env = EBinding (BVar bv, v) :: ctx.env }
 
 (** Push a list of variables.
 
@@ -488,11 +377,12 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
              vars)));
   assert (
     List.for_all
-      (fun (var, (value : typed_value)) -> var.var_ty = value.ty)
+      (fun (var, (value : typed_value)) ->
+        TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
       vars);
   let vars =
     List.map
-      (fun (var, value) -> Var (VarBinder (var_to_binder var), value))
+      (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
       vars
   in
   let vars = List.rev vars in
@@ -501,7 +391,7 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
 (** Push a dummy variable in the context's environment. *)
 let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value)
     : eval_ctx =
-  { ctx with env = Var (DummyBinder vid, v) :: ctx.env }
+  { ctx with env = EBinding (BDummy vid, v) :: ctx.env }
 
 (** Remove a dummy variable from a context's environment. *)
 let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
@@ -509,7 +399,7 @@ let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
   let rec remove_var (env : env) : env * typed_value =
     match env with
     | [] -> raise (Failure "Could not lookup a dummy variable")
-    | Var (DummyBinder vid', v) :: env when vid' = vid -> (env, v)
+    | EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
     | ee :: env ->
         let env, v = remove_var env in
         (ee :: env, v)
@@ -522,27 +412,36 @@ let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
   let rec lookup_var (env : env) : typed_value =
     match env with
     | [] -> raise (Failure "Could not lookup a dummy variable")
-    | Var (DummyBinder vid', v) :: _env when vid' = vid -> v
+    | EBinding (BDummy vid', v) :: _env when vid' = vid -> v
     | _ :: env -> lookup_var env
   in
   lookup_var ctx.env
 
+let erase_regions (ty : ty) : ty =
+  let v =
+    object
+      inherit [_] map_ty
+      method! visit_region _ _ = RErased
+    end
+  in
+  v#visit_ty () ty
+
 (** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
-  ctx_push_var ctx var (mk_bottom var.var_ty)
+  ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
 
 (** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
-  let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in
+  let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
 
 let env_find_abs (env : env) (pred : V.abs -> bool) : V.abs option =
   let rec lookup env =
     match env with
     | [] -> None
-    | Var (_, _) :: env' -> lookup env'
-    | Abs abs :: env' -> if pred abs then Some abs else lookup env'
-    | Frame :: env' -> lookup env'
+    | EBinding (_, _) :: env' -> lookup env'
+    | EAbs abs :: env' -> if pred abs then Some abs else lookup env'
+    | EFrame :: env' -> lookup env'
   in
   lookup env
 
@@ -558,17 +457,17 @@ let env_remove_abs (env : env) (abs_id : V.AbstractionId.id) :
   let rec remove (env : env) : env * V.abs option =
     match env with
     | [] -> raise (Failure "Unreachable")
-    | Frame :: _ -> (env, None)
-    | Var (bv, v) :: env ->
+    | EFrame :: _ -> (env, None)
+    | EBinding (bv, v) :: env ->
         let env, abs_opt = remove env in
-        (Var (bv, v) :: env, abs_opt)
-    | Abs abs :: env ->
+        (EBinding (bv, v) :: env, abs_opt)
+    | EAbs abs :: env ->
         if abs.abs_id = abs_id then (env, Some abs)
         else
           let env, abs_opt = remove env in
           (* Update the parents set *)
           let parents = V.AbstractionId.Set.remove abs_id abs.parents in
-          (Abs { abs with V.parents } :: env, abs_opt)
+          (EAbs { abs with V.parents } :: env, abs_opt)
   in
   remove env
 
@@ -584,12 +483,12 @@ let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
   let rec update (env : env) : env * V.abs option =
     match env with
     | [] -> raise (Failure "Unreachable")
-    | Frame :: _ -> (* We're done *) (env, None)
-    | Var (bv, v) :: env ->
+    | EFrame :: _ -> (* We're done *) (env, None)
+    | EBinding (bv, v) :: env ->
         let env, opt_abs = update env in
-        (Var (bv, v) :: env, opt_abs)
-    | Abs abs :: env ->
-        if abs.abs_id = abs_id then (Abs nabs :: env, Some abs)
+        (EBinding (bv, v) :: env, opt_abs)
+    | EAbs abs :: env ->
+        if abs.abs_id = abs_id then (EAbs nabs :: env, Some abs)
         else
           let env, opt_abs = update env in
           (* Update the parents set *)
@@ -600,7 +499,7 @@ let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
               V.AbstractionId.Set.add nabs.abs_id parents
             else parents
           in
-          (Abs { abs with V.parents } :: env, opt_abs)
+          (EAbs { abs with V.parents } :: env, opt_abs)
   in
   update env
 
@@ -641,7 +540,7 @@ class ['self] iter_frame =
       fun acc env ->
         match env with
         | [] -> ()
-        | Frame :: _ -> (* We stop here *) ()
+        | EFrame :: _ -> (* We stop here *) ()
         | em :: env ->
             self#visit_env_elem acc em;
             self#visit_env acc env
@@ -656,7 +555,7 @@ class ['self] map_frame_concrete =
       fun acc env ->
         match env with
         | [] -> []
-        | Frame :: env -> (* We stop here *) Frame :: env
+        | EFrame :: env -> (* We stop here *) EFrame :: env
         | em :: env ->
             let em = self#visit_env_elem acc em in
             let env = self#visit_env acc env in
@@ -686,17 +585,17 @@ class ['self] map_eval_ctx =
 let env_iter_abs (f : V.abs -> unit) (env : env) : unit =
   List.iter
     (fun (ee : env_elem) ->
-      match ee with Var _ | Frame -> () | Abs abs -> f abs)
+      match ee with EBinding _ | EFrame -> () | EAbs abs -> f abs)
     env
 
 let env_map_abs (f : V.abs -> V.abs) (env : env) : env =
   List.map
     (fun (ee : env_elem) ->
-      match ee with Var _ | Frame -> ee | Abs abs -> Abs (f abs))
+      match ee with EBinding _ | EFrame -> ee | EAbs abs -> EAbs (f abs))
     env
 
 let env_filter_abs (f : V.abs -> bool) (env : env) : env =
   List.filter
     (fun (ee : env_elem) ->
-      match ee with Var _ | Frame -> true | Abs abs -> f abs)
+      match ee with EBinding _ | EFrame -> true | EAbs abs -> f abs)
     env
-- 
cgit v1.2.3


From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 13 Nov 2023 13:27:02 +0100
Subject: Add RegionsHierarchy.ml

---
 compiler/Contexts.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 9a20a6cc..12927aab 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -2,6 +2,7 @@ open Types
 open Expressions
 open Values
 open LlbcAst
+open LlbcAstUtils
 module V = Values
 open ValuesUtils
 open Identifiers
@@ -190,6 +191,7 @@ type type_context = {
 type fun_context = {
   fun_decls : fun_decl FunDeclId.Map.t;
   fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
+  regions_hierarchies : T.region_groups FunIdMap.t;
 }
 [@@deriving show]
 
-- 
cgit v1.2.3


From 4192258b7e5e3ed034ac16a326c455fe75fe6df4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 13 Nov 2023 14:49:00 +0100
Subject: Normalize the types when computing the regions hierarchies

---
 compiler/Contexts.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 12927aab..17ebd315 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -254,18 +254,14 @@ type eval_ctx = {
 
 let lookup_type_var_opt (ctx : eval_ctx) (vid : TypeVarId.id) : type_var option
     =
-  if TypeVarId.to_int vid < List.length ctx.type_vars then
-    Some (TypeVarId.nth ctx.type_vars vid)
-  else None
+  TypeVarId.nth_opt ctx.type_vars vid
 
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
 
 let lookup_const_generic_var_opt (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
     const_generic_var option =
-  if ConstGenericVarId.to_int vid < List.length ctx.const_generic_vars then
-    Some (ConstGenericVarId.nth ctx.const_generic_vars vid)
-  else None
+  ConstGenericVarId.nth_opt ctx.const_generic_vars vid
 
 let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
     const_generic_var =
-- 
cgit v1.2.3


From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 15 Nov 2023 22:03:21 +0100
Subject: Start updating the name type, cleanup the names and the module
 abbrevs

---
 compiler/Contexts.ml | 52 +++++++++++++++++++++++++---------------------------
 1 file changed, 25 insertions(+), 27 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 17ebd315..41c84141 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -3,7 +3,6 @@ open Expressions
 open Values
 open LlbcAst
 open LlbcAstUtils
-module V = Values
 open ValuesUtils
 open Identifiers
 module L = Logging
@@ -191,7 +190,7 @@ type type_context = {
 type fun_context = {
   fun_decls : fun_decl FunDeclId.Map.t;
   fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
-  regions_hierarchies : T.region_groups FunIdMap.t;
+  regions_hierarchies : region_groups FunIdMap.t;
 }
 [@@deriving show]
 
@@ -371,7 +370,7 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
           (List.map
              (fun (var, value) ->
                (* We can unfortunately not use Print because it depends on Contexts... *)
-               show_var var ^ " -> " ^ V.show_typed_value value)
+               show_var var ^ " -> " ^ show_typed_value value)
              vars)));
   assert (
     List.for_all
@@ -433,7 +432,7 @@ let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
 
-let env_find_abs (env : env) (pred : V.abs -> bool) : V.abs option =
+let env_find_abs (env : env) (pred : abs -> bool) : abs option =
   let rec lookup env =
     match env with
     | [] -> None
@@ -443,16 +442,15 @@ let env_find_abs (env : env) (pred : V.abs -> bool) : V.abs option =
   in
   lookup env
 
-let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
+let env_lookup_abs (env : env) (abs_id : AbstractionId.id) : abs =
   Option.get (env_find_abs env (fun abs -> abs.abs_id = abs_id))
 
 (** Remove an abstraction from the context, as well as all the references to
     this abstraction (for instance, remove the abs id from all the parent sets
     of all the other abstractions).
  *)
-let env_remove_abs (env : env) (abs_id : V.AbstractionId.id) :
-    env * V.abs option =
-  let rec remove (env : env) : env * V.abs option =
+let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
+  let rec remove (env : env) : env * abs option =
     match env with
     | [] -> raise (Failure "Unreachable")
     | EFrame :: _ -> (env, None)
@@ -464,8 +462,8 @@ let env_remove_abs (env : env) (abs_id : V.AbstractionId.id) :
         else
           let env, abs_opt = remove env in
           (* Update the parents set *)
-          let parents = V.AbstractionId.Set.remove abs_id abs.parents in
-          (EAbs { abs with V.parents } :: env, abs_opt)
+          let parents = AbstractionId.Set.remove abs_id abs.parents in
+          (EAbs { abs with parents } :: env, abs_opt)
   in
   remove env
 
@@ -476,9 +474,9 @@ let env_remove_abs (env : env) (abs_id : V.AbstractionId.id) :
     we also substitute the abstraction id wherever it is used (i.e., in the
     parent sets of the other abstractions).
  *)
-let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
-    env * V.abs option =
-  let rec update (env : env) : env * V.abs option =
+let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
+    env * abs option =
+  let rec update (env : env) : env * abs option =
     match env with
     | [] -> raise (Failure "Unreachable")
     | EFrame :: _ -> (* We're done *) (env, None)
@@ -492,34 +490,34 @@ let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
           (* Update the parents set *)
           let parents = abs.parents in
           let parents =
-            if V.AbstractionId.Set.mem abs_id parents then
-              let parents = V.AbstractionId.Set.remove abs_id parents in
-              V.AbstractionId.Set.add nabs.abs_id parents
+            if AbstractionId.Set.mem abs_id parents then
+              let parents = AbstractionId.Set.remove abs_id parents in
+              AbstractionId.Set.add nabs.abs_id parents
             else parents
           in
-          (EAbs { abs with V.parents } :: env, opt_abs)
+          (EAbs { abs with parents } :: env, opt_abs)
   in
   update env
 
-let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
+let ctx_lookup_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) : abs =
   env_lookup_abs ctx.env abs_id
 
-let ctx_find_abs (ctx : eval_ctx) (p : V.abs -> bool) : V.abs option =
+let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
   env_find_abs ctx.env p
 
 (** See the comments for {!env_remove_abs} *)
-let ctx_remove_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) :
-    eval_ctx * V.abs option =
+let ctx_remove_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) :
+    eval_ctx * abs option =
   let env, abs = env_remove_abs ctx.env abs_id in
   ({ ctx with env }, abs)
 
 (** See the comments for {!env_subst_abs} *)
-let ctx_subst_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) (nabs : V.abs)
-    : eval_ctx * V.abs option =
+let ctx_subst_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
+    eval_ctx * abs option =
   let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
   ({ ctx with env }, abs_opt)
 
-let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : V.AbstractionId.id)
+let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
     (can_end : bool) : eval_ctx =
   let abs = ctx_lookup_abs ctx abs_id in
   let abs = { abs with can_end } in
@@ -580,19 +578,19 @@ class ['self] map_eval_ctx =
         { ctx with env }
   end
 
-let env_iter_abs (f : V.abs -> unit) (env : env) : unit =
+let env_iter_abs (f : abs -> unit) (env : env) : unit =
   List.iter
     (fun (ee : env_elem) ->
       match ee with EBinding _ | EFrame -> () | EAbs abs -> f abs)
     env
 
-let env_map_abs (f : V.abs -> V.abs) (env : env) : env =
+let env_map_abs (f : abs -> abs) (env : env) : env =
   List.map
     (fun (ee : env_elem) ->
       match ee with EBinding _ | EFrame -> ee | EAbs abs -> EAbs (f abs))
     env
 
-let env_filter_abs (f : V.abs -> bool) (env : env) : env =
+let env_filter_abs (f : abs -> bool) (env : env) : env =
   List.filter
     (fun (ee : env_elem) ->
       match ee with EBinding _ | EFrame -> true | EAbs abs -> f abs)
-- 
cgit v1.2.3


From a27efd1ed08bc9583752445d9eda7a693c0c7379 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 16 Nov 2023 10:13:28 +0100
Subject: Finish propagating the changes to the names and cleaning

---
 compiler/Contexts.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 41c84141..a2ae4f16 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -525,7 +525,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
-  match decl_group with Rec _ -> true | NonRec _ -> false
+  match decl_group with RecGroup _ -> true | NonRecGroup _ -> false
 
 (** Visitor to iterate over the values in the *current* frame *)
 class ['self] iter_frame =
-- 
cgit v1.2.3


From 6f8f1213e056804eda4c521922cdf45f4e92a509 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 15:57:55 +0100
Subject: Fix the issues with the cross-references for OCaml doc

---
 compiler/Contexts.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a2ae4f16..c93bb213 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -112,7 +112,7 @@ let reset_global_counters () =
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
-(** Ancestor for {!env} iter visitor *)
+(** Ancestor for {!type:env} iter visitor *)
 class ['self] iter_env_base =
   object (_self : 'self)
     inherit [_] iter_abs
@@ -120,7 +120,7 @@ class ['self] iter_env_base =
     method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for {!env} map visitor *)
+(** Ancestor for {!type:env} map visitor *)
 class ['self] map_env_base =
   object (_self : 'self)
     inherit [_] map_abs
@@ -423,11 +423,11 @@ let erase_regions (ty : ty) : ty =
   in
   v#visit_ty () ty
 
-(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *)
+(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
   ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
 
-(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *)
+(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
-- 
cgit v1.2.3


From 60ce69b83cbd749781543bb16becb5357f0e1a0a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 15:00:46 +0100
Subject: Update following changes in Charon

---
 compiler/Contexts.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index c93bb213..bbfd31e6 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -190,7 +190,7 @@ type type_context = {
 type fun_context = {
   fun_decls : fun_decl FunDeclId.Map.t;
   fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
-  regions_hierarchies : region_groups FunIdMap.t;
+  regions_hierarchies : region_var_groups FunIdMap.t;
 }
 [@@deriving show]
 
-- 
cgit v1.2.3


From df3587d14b1137d0961f5607b3d8309eddbe69ce Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 16:01:30 +0100
Subject: Fix a minor issue with the use of const generics

---
 compiler/Contexts.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index bbfd31e6..a30ed0f1 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -241,7 +241,11 @@ type eval_ctx = {
   const_generic_vars_map : typed_value Types.ConstGenericVarId.Map.t;
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
-          if we run in interpreter mode) *)
+          if we run in interpreter mode).
+
+          TODO: this is actually not used in symbolic mode, where we
+          directly introduce fresh symbolic values.
+       *)
   norm_trait_types : ty TraitTypeRefMap.t;
       (** The normalized trait types (a map from trait types to their representatives).
           Note that this doesn't take into account higher-order type constraints
-- 
cgit v1.2.3