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