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/Pure.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ac4ca081..55513cc2 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -37,6 +37,7 @@ module ConstGenericVarId = T.ConstGenericVarId
 type integer_type = T.integer_type [@@deriving show, ord]
 type const_generic_var = T.const_generic_var [@@deriving show, ord]
 type const_generic = T.const_generic [@@deriving show, ord]
+type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -536,6 +537,7 @@ class virtual ['self] mapreduce_expression_base =
  *)
 type expression =
   | Var of var_id  (** a variable *)
+  | CVar of const_generic_var_id  (** a const generic var *)
   | Const of literal
   | App of texpression * texpression
       (** Application of a function to an argument.
-- 
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/Pure.ml | 100 +++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 89 insertions(+), 11 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 55513cc2..147c14b9 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -13,6 +13,9 @@ module FieldId = T.FieldId
 module SymbolicValueId = V.SymbolicValueId
 module FunDeclId = A.FunDeclId
 module GlobalDeclId = A.GlobalDeclId
+module TraitDeclId = T.TraitDeclId
+module TraitImplId = T.TraitImplId
+module TraitClauseId = T.TraitClauseId
 
 (** We redefine identifiers for loop: in {!Values}, the identifiers are global
     (they monotonically increase across functions) while in {!module:Pure} we want
@@ -38,6 +41,10 @@ type integer_type = T.integer_type [@@deriving show, ord]
 type const_generic_var = T.const_generic_var [@@deriving show, ord]
 type const_generic = T.const_generic [@@deriving show, ord]
 type const_generic_var_id = T.const_generic_var_id [@@deriving show, ord]
+type trait_decl_id = T.trait_decl_id [@@deriving show, ord]
+type trait_impl_id = T.trait_impl_id [@@deriving show, ord]
+type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
+type trait_item_name = T.trait_item_name [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -177,6 +184,14 @@ class ['self] iter_ty_base =
     inherit! [_] T.iter_const_generic
     inherit! [_] PV.iter_literal_type
     method visit_type_var_id : 'env -> type_var_id -> unit = fun _ _ -> ()
+    method visit_trait_decl_id : 'env -> trait_decl_id -> unit = fun _ _ -> ()
+    method visit_trait_impl_id : 'env -> trait_impl_id -> unit = fun _ _ -> ()
+
+    method visit_trait_clause_id : 'env -> trait_clause_id -> unit =
+      fun _ _ -> ()
+
+    method visit_trait_item_name : 'env -> trait_item_name -> unit =
+      fun _ _ -> ()
   end
 
 (** Ancestor for map visitor for [ty] *)
@@ -186,6 +201,18 @@ class ['self] map_ty_base =
     inherit! [_] T.map_const_generic
     inherit! [_] PV.map_literal_type
     method visit_type_var_id : 'env -> type_var_id -> type_var_id = fun _ x -> x
+
+    method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id =
+      fun _ x -> x
+
+    method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id =
+      fun _ x -> x
+
+    method visit_trait_clause_id : 'env -> trait_clause_id -> trait_clause_id =
+      fun _ x -> x
+
+    method visit_trait_item_name : 'env -> trait_item_name -> trait_item_name =
+      fun _ x -> x
   end
 
 (** Ancestor for reduce visitor for [ty] *)
@@ -195,6 +222,18 @@ class virtual ['self] reduce_ty_base =
     inherit! [_] T.reduce_const_generic
     inherit! [_] PV.reduce_literal_type
     method visit_type_var_id : 'env -> type_var_id -> 'a = fun _ _ -> self#zero
+
+    method visit_trait_decl_id : 'env -> trait_decl_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_trait_impl_id : 'env -> trait_impl_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_trait_clause_id : 'env -> trait_clause_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_trait_item_name : 'env -> trait_item_name -> 'a =
+      fun _ _ -> self#zero
   end
 
 (** Ancestor for mapreduce visitor for [ty] *)
@@ -206,10 +245,24 @@ class virtual ['self] mapreduce_ty_base =
 
     method visit_type_var_id : 'env -> type_var_id -> type_var_id * 'a =
       fun _ x -> (x, self#zero)
+
+    method visit_trait_decl_id : 'env -> trait_decl_id -> trait_decl_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_trait_impl_id : 'env -> trait_impl_id -> trait_impl_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_trait_clause_id
+        : 'env -> trait_clause_id -> trait_clause_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_trait_item_name
+        : 'env -> trait_item_name -> trait_item_name * 'a =
+      fun _ x -> (x, self#zero)
   end
 
 type ty =
-  | Adt of type_id * ty list * const_generic list
+  | Adt of type_id * generic_args
       (** {!Adt} encodes ADTs and tuples and assumed types.
 
           TODO: what about the ended regions? (ADTs may be parameterized
@@ -220,6 +273,23 @@ type ty =
   | TypeVar of type_var_id
   | Literal of literal_type
   | Arrow of ty * ty
+
+and trait_ref = { trait_id : trait_instance_id; generics : generic_args }
+
+and generic_args = {
+  types : ty list;
+  const_generics : const_generic list;
+  trait_refs : trait_ref list;
+}
+
+and trait_instance_id =
+  | Self
+  | TraitImpl of trait_impl_id
+  | Clause of trait_clause_id
+  | ParentClause of trait_instance_id * trait_clause_id
+  | ItemClause of trait_instance_id * trait_item_name * trait_clause_id
+  | TraitRef of trait_ref
+  | UnknownTrait of string
 [@@deriving
   show,
     visitors
@@ -265,11 +335,24 @@ type type_decl_kind = Struct of field list | Enum of variant list | Opaque
 
 type type_var = T.type_var [@@deriving show]
 
+type trait_clause = {
+  clause_id : trait_clause_id;
+  trait_id : trait_decl_id;
+  generics : generic_args;
+}
+[@@deriving show]
+
+type generic_params = {
+  types : type_var list;
+  const_generics : const_generic_var list;
+  trait_clauses : trait_clause list;
+}
+[@@deriving show]
+
 type type_decl = {
   def_id : TypeDeclId.id;
   name : name;
-  type_params : type_var list;
-  const_generic_params : const_generic_var list;
+  generics : generic_params;
   kind : type_decl_kind;
 }
 [@@deriving show]
@@ -463,18 +546,13 @@ type qualif_id =
   | Proj of projection  (** Field projector *)
 [@@deriving show]
 
-(** An instantiated qualified.
+(** An instantiated qualifier.
 
     Note that for now we have a clear separation between types and expressions,
-    which explains why we have the [type_params] field: a function or ADT
+    which explains why we have the [generics] field: a function or ADT
     constructor is always fully instantiated.
  *)
-type qualif = {
-  id : qualif_id;
-  type_args : ty list;
-  const_generic_args : const_generic list;
-}
-[@@deriving show]
+type qualif = { id : qualif_id; generics : generic_args } [@@deriving show]
 
 type field_id = FieldId.id [@@deriving show, ord]
 type var_id = VarId.id [@@deriving show, ord]
-- 
cgit v1.2.3


From 33bb0b7dbdf5cce28b58793e5fb280668a644525 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 31 Aug 2023 16:56:26 +0200
Subject: Finish updating SymbolicToPure.ml

---
 compiler/Pure.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 147c14b9..272ec328 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -273,6 +273,8 @@ type ty =
   | TypeVar of type_var_id
   | Literal of literal_type
   | Arrow of ty * ty
+  | TraitType of trait_ref * generic_args * string
+      (** The string is for the name of the associated type *)
 
 and trait_ref = { trait_id : trait_instance_id; generics : generic_args }
 
@@ -867,11 +869,10 @@ type fun_sig_info = {
     - etc.
  *)
 type fun_sig = {
-  type_params : type_var list;
-  const_generic_params : const_generic_var list;
+  generics : generic_params;
       (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *)
   inputs : ty list;
-      (** The input types.
+      (** The types of the inputs.
 
           Note that those input types take into account the [fuel] parameter,
           if the function uses fuel for termination, and the [state] parameter,
-- 
cgit v1.2.3


From 0cafb31dd42c95f22e0b6680531c27fa0508e376 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 13:32:43 +0200
Subject: Make progress on the extraction

---
 compiler/Pure.ml | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 272ec328..725f71ad 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -276,7 +276,16 @@ type ty =
   | TraitType of trait_ref * generic_args * string
       (** The string is for the name of the associated type *)
 
-and trait_ref = { trait_id : trait_instance_id; generics : generic_args }
+and trait_ref = {
+  trait_id : trait_instance_id;
+  generics : generic_args;
+  trait_decl_ref : trait_decl_ref;
+}
+
+and trait_decl_ref = {
+  trait_decl_id : trait_decl_id;
+  decl_generics : generic_args; (* The name: annoying field collisions... *)
+}
 
 and generic_args = {
   types : ty list;
@@ -288,8 +297,9 @@ and trait_instance_id =
   | Self
   | TraitImpl of trait_impl_id
   | Clause of trait_clause_id
-  | ParentClause of trait_instance_id * trait_clause_id
-  | ItemClause of trait_instance_id * trait_item_name * trait_clause_id
+  | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id
+  | ItemClause of
+      trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id
   | TraitRef of trait_ref
   | UnknownTrait of string
 [@@deriving
-- 
cgit v1.2.3


From b42c0a8fa4708d6bf8424d63b6a7fe4964ba0e3d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 3 Sep 2023 15:18:36 +0200
Subject: Make progress on the extraction

---
 compiler/Pure.ml | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 725f71ad..6c9f41f1 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -45,6 +45,8 @@ type trait_decl_id = T.trait_decl_id [@@deriving show, ord]
 type trait_impl_id = T.trait_impl_id [@@deriving show, ord]
 type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
 type trait_item_name = T.trait_item_name [@@deriving show, ord]
+type global_decl_id = T.global_decl_id [@@deriving show, ord]
+type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -361,11 +363,23 @@ type generic_params = {
 }
 [@@deriving show]
 
+type trait_type_constraint = {
+  trait_ref : trait_ref;
+  generics : generic_args;
+  type_name : trait_item_name;
+  ty : ty;
+}
+[@@deriving show]
+
+type predicates = { trait_type_constraints : trait_type_constraint list }
+[@@deriving show]
+
 type type_decl = {
   def_id : TypeDeclId.id;
   name : name;
   generics : generic_params;
   kind : type_decl_kind;
+  preds : predicates;
 }
 [@@deriving show]
 
@@ -881,6 +895,7 @@ type fun_sig_info = {
 type fun_sig = {
   generics : generic_params;
       (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *)
+  preds : predicates;
   inputs : ty list;
       (** The types of the inputs.
 
@@ -952,8 +967,11 @@ type fun_body = {
 }
 [@@deriving show]
 
+type fun_kind = A.fun_kind [@@deriving show]
+
 type fun_decl = {
   def_id : FunDeclId.id;
+  kind : fun_kind;
   num_loops : int;
       (** The number of loops in the parent forward function (basically the number
           of loops appearing in the original Rust functions, unless some loops are
@@ -973,3 +991,29 @@ type fun_decl = {
   body : fun_body option;
 }
 [@@deriving show]
+
+type trait_decl = {
+  def_id : trait_decl_id;
+  name : name;
+  generics : generic_params;
+  preds : predicates;
+  all_trait_clauses : trait_clause list;
+  consts : (trait_item_name * (ty * global_decl_id option)) list;
+  types : (trait_item_name * (trait_clause list * ty option)) list;
+  required_methods : (trait_item_name * fun_decl_id) list;
+  provided_methods : trait_item_name list;
+}
+[@@deriving show]
+
+type trait_impl = {
+  def_id : trait_impl_id;
+  name : name;
+  impl_trait : trait_decl_ref;
+  generics : generic_params;
+  preds : predicates;
+  consts : (trait_item_name * (ty * global_decl_id)) list;
+  types : (trait_item_name * (trait_ref list * ty)) list;
+  required_methods : (trait_item_name * fun_decl_id) list;
+  provided_methods : (trait_item_name * fun_decl_id) list;
+}
+[@@deriving show]
-- 
cgit v1.2.3


From c6b88a2e54b7697262ad3677ad7500471c68e332 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 10 Sep 2023 21:07:06 +0200
Subject: Add support for the trait associated constants

---
 compiler/Pure.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 6c9f41f1..81060c43 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -567,9 +567,11 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
 
 type qualif_id =
   | FunOrOp of fun_or_op_id  (** A function or an operation *)
-  | Global of GlobalDeclId.id
+  | Global of global_decl_id
   | AdtCons of adt_cons_id  (** A function or ADT constructor identifier *)
   | Proj of projection  (** Field projector *)
+  | TraitConst of trait_ref * generic_args * string
+      (** A trait associated constant *)
 [@@deriving show]
 
 (** An instantiated qualifier.
-- 
cgit v1.2.3


From 5921be8e2e8955db5101354d8bf29ae6a3693f48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Sep 2023 06:35:07 +0200
Subject: Make progress on correctly handling trait method calls in the
 symbolic execution

---
 compiler/Pure.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 81060c43..47c7beb4 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -306,6 +306,7 @@ and trait_instance_id =
   | UnknownTrait of string
 [@@deriving
   show,
+    ord,
     visitors
       {
         name = "iter_ty";
@@ -369,7 +370,7 @@ type trait_type_constraint = {
   type_name : trait_item_name;
   ty : ty;
 }
-[@@deriving show]
+[@@deriving show, ord]
 
 type predicates = { trait_type_constraints : trait_type_constraint list }
 [@@deriving show]
@@ -530,8 +531,15 @@ type pure_assumed_fun_id =
   | FuelEqZero  (** Test if some fuel is equal to 0 - TODO: ugly *)
 [@@deriving show, ord]
 
+type fun_id_or_trait_method_ref =
+  | FunId of A.fun_id
+  | TraitMethod of trait_ref * string * fun_decl_id
+      (** The fun decl id is not really needed and here for convenience purposes *)
+[@@deriving show, ord]
+
 (** A function id for a non-assumed function *)
-type regular_fun_id = A.fun_id * LoopId.id option * T.RegionGroupId.id option
+type regular_fun_id =
+  fun_id_or_trait_method_ref * LoopId.id option * T.RegionGroupId.id option
 [@@deriving show, ord]
 
 (** A function identifier *)
@@ -1003,7 +1011,7 @@ type trait_decl = {
   consts : (trait_item_name * (ty * global_decl_id option)) list;
   types : (trait_item_name * (trait_clause list * ty option)) list;
   required_methods : (trait_item_name * fun_decl_id) list;
-  provided_methods : trait_item_name list;
+  provided_methods : (trait_item_name * fun_decl_id option) list;
 }
 [@@deriving show]
 
-- 
cgit v1.2.3


From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 23 Oct 2023 13:47:39 +0200
Subject: Remove some assumed types and add more support for builtin
 definitions

---
 compiler/Pure.ml | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 47c7beb4..81e13af7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -64,17 +64,7 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
         this state is opaque to Aeneas (the user can define it, or leave it as
         assumed)
   *)
-type assumed_ty =
-  | State
-  | Result
-  | Error
-  | Fuel
-  | Vec
-  | Option
-  | Array
-  | Slice
-  | Str
-  | Range
+type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
 [@@deriving show, ord]
 
 (* TODO: we should never directly manipulate [Return] and [Fail], but rather
-- 
cgit v1.2.3


From ece74df70f12790bab7ecfe0c590c2c637e89801 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 11:40:31 +0200
Subject: Update following the addition of raw pointers

---
 compiler/Pure.ml | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 81e13af7..9a3654b8 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -47,6 +47,7 @@ type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
 type trait_item_name = T.trait_item_name [@@deriving show, ord]
 type global_decl_id = T.global_decl_id [@@deriving show, ord]
 type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
+type mutability = Mut | Const [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -64,7 +65,22 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
         this state is opaque to Aeneas (the user can define it, or leave it as
         assumed)
   *)
-type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
+type assumed_ty =
+  | State
+  | Result
+  | Error
+  | Fuel
+  | Array
+  | Slice
+  | Str
+  | RawPtr of mutability
+      (** The bool
+          Raw pointers don't make sense in the pure world, but we don't know
+          how to translate them yet and we have to handle some functions which
+          use raw pointers in their signature (for instance some trait declarations
+          for the slices). For now, we use a dedicated type to "mark" the raw pointers,
+          and make sure that those functions are actually not used in the translation.
+       *)
 [@@deriving show, ord]
 
 (* TODO: we should never directly manipulate [Return] and [Fail], but rather
-- 
cgit v1.2.3


From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 18:44:28 +0200
Subject: Make the hashmap files typecheck again in Lean

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

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 9a3654b8..a5aa0edd 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -24,8 +24,6 @@ module TraitClauseId = T.TraitClauseId
 module LoopId =
 IdGen ()
 
-type loop_id = LoopId.id [@@deriving show, ord]
-
 (** We give an identifier to every phase of the synthesis (forward, backward
     for group of regions 0, etc.) *)
 module SynthPhaseId =
@@ -47,6 +45,8 @@ type trait_clause_id = T.trait_clause_id [@@deriving show, ord]
 type trait_item_name = T.trait_item_name [@@deriving show, ord]
 type global_decl_id = T.global_decl_id [@@deriving show, ord]
 type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
+type loop_id = LoopId.id [@@deriving show, ord]
+type region_group_id = T.region_group_id [@@deriving show, ord]
 type mutability = Mut | Const [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
-- 
cgit v1.2.3


From dc0032f6ce3b837ba2f431bbb5c9a92c625f629f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 30 Oct 2023 12:24:05 +0100
Subject: Make minor updates following changes in Charon

---
 compiler/Pure.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index a5aa0edd..70653e57 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1013,7 +1013,6 @@ type trait_decl = {
   name : name;
   generics : generic_params;
   preds : predicates;
-  all_trait_clauses : trait_clause list;
   consts : (trait_item_name * (ty * global_decl_id option)) list;
   types : (trait_item_name * (trait_clause list * ty option)) list;
   required_methods : (trait_item_name * fun_decl_id) list;
-- 
cgit v1.2.3


From 4ba7d73fa3bfbf9ef41b2d9d5595f28fb67b8e47 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 6 Nov 2023 18:11:24 +0100
Subject: Update following some changes in Charon

---
 compiler/Pure.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 70653e57..c33a745c 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1013,6 +1013,7 @@ type trait_decl = {
   name : name;
   generics : generic_params;
   preds : predicates;
+  parent_clauses : trait_clause list;
   consts : (trait_item_name * (ty * global_decl_id option)) list;
   types : (trait_item_name * (trait_clause list * ty option)) list;
   required_methods : (trait_item_name * fun_decl_id) list;
-- 
cgit v1.2.3


From ed788eec1d8be1656c0ad7dab25975ad3f5497c2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Nov 2023 10:40:27 +0100
Subject: Update the normalization of associated types

---
 compiler/Pure.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index c33a745c..e6a3dab5 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1027,6 +1027,7 @@ type trait_impl = {
   impl_trait : trait_decl_ref;
   generics : generic_params;
   preds : predicates;
+  parent_trait_refs : trait_ref list;
   consts : (trait_item_name * (ty * global_decl_id)) list;
   types : (trait_item_name * (trait_ref list * ty)) list;
   required_methods : (trait_item_name * fun_decl_id) list;
-- 
cgit v1.2.3