From 50af296306bfee9f0b127dde8abe5fb0ec1b0acb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 1 Aug 2023 11:16:06 +0200
Subject: Start adding support for const generics

---
 compiler/Values.ml | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

(limited to 'compiler/Values.ml')

diff --git a/compiler/Values.ml b/compiler/Values.ml
index d4eff58a..3d6bc9c1 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -14,7 +14,7 @@ module LoopId = IdGen ()
 
 type big_int = PrimitiveValues.big_int [@@deriving show, ord]
 type scalar_value = PrimitiveValues.scalar_value [@@deriving show, ord]
-type primitive_value = PrimitiveValues.primitive_value [@@deriving show, ord]
+type literal = PrimitiveValues.literal [@@deriving show, ord]
 type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
 type symbolic_value_id_set = SymbolicValueId.Set.t [@@deriving show, ord]
 type loop_id = LoopId.id [@@deriving show, ord]
@@ -110,10 +110,7 @@ type loan_id_set = BorrowId.Set.t [@@deriving show, ord]
 class ['self] iter_typed_value_base =
   object (self : 'self)
     inherit [_] iter_symbolic_value
-
-    method visit_primitive_value : 'env -> primitive_value -> unit =
-      fun _ _ -> ()
-
+    method visit_literal : 'env -> literal -> unit = fun _ _ -> ()
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
     method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
@@ -131,9 +128,7 @@ class ['self] iter_typed_value_base =
 class ['self] map_typed_value_base =
   object (self : 'self)
     inherit [_] map_symbolic_value
-
-    method visit_primitive_value : 'env -> primitive_value -> primitive_value =
-      fun _ cv -> cv
+    method visit_literal : 'env -> literal -> literal = fun _ cv -> cv
 
     method visit_erased_region : 'env -> erased_region -> erased_region =
       fun _ r -> r
@@ -152,7 +147,7 @@ class ['self] map_typed_value_base =
 
 (** An untyped value, used in the environments *)
 type value =
-  | Primitive of primitive_value  (** Non-symbolic primitive value *)
+  | Primitive of literal  (** Non-symbolic primitive value *)
   | Adt of adt_value  (** Enumerations and structures *)
   | Bottom  (** No value (uninitialized or moved value) *)
   | Borrow of borrow_content  (** A borrowed value *)
@@ -1019,7 +1014,7 @@ type abs = {
     TODO: this should rather be name "expanded_symbolic"
  *)
 type symbolic_expansion =
-  | SePrimitive of primitive_value
+  | SePrimitive of literal
   | SeAdt of (VariantId.id option * symbolic_value list)
   | SeMutRef of BorrowId.id * symbolic_value
   | SeSharedRef of BorrowId.Set.t * symbolic_value
-- 
cgit v1.2.3


From 9d27e2e27db06eaad7565b55366ca8734b364fca Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 11:03:59 +0200
Subject: Make progress proapagating the changes

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

(limited to 'compiler/Values.ml')

diff --git a/compiler/Values.ml b/compiler/Values.ml
index 3d6bc9c1..f70b9b4b 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -147,7 +147,7 @@ class ['self] map_typed_value_base =
 
 (** An untyped value, used in the environments *)
 type value =
-  | Primitive of literal  (** Non-symbolic primitive value *)
+  | Literal of literal  (** Non-symbolic primitive value *)
   | Adt of adt_value  (** Enumerations and structures *)
   | Bottom  (** No value (uninitialized or moved value) *)
   | Borrow of borrow_content  (** A borrowed value *)
@@ -1014,7 +1014,7 @@ type abs = {
     TODO: this should rather be name "expanded_symbolic"
  *)
 type symbolic_expansion =
-  | SePrimitive of literal
+  | SeLiteral of literal
   | SeAdt of (VariantId.id option * symbolic_value list)
   | SeMutRef of BorrowId.id * symbolic_value
   | SeSharedRef of BorrowId.Set.t * symbolic_value
-- 
cgit v1.2.3


From c6f0a8c8bfe04e83de4692a389daf8cde47b74d5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 00:24:02 +0200
Subject: Fix issues

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

(limited to 'compiler/Values.ml')

diff --git a/compiler/Values.ml b/compiler/Values.ml
index f70b9b4b..d884c319 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -50,6 +50,8 @@ type sv_kind =
       (** A value given back by a loop (when ending abstractions while going backwards) *)
   | LoopJoin
       (** The result of a loop join (when computing loop fixed points) *)
+  | Aggregate
+      (** A symbolic value we introduce in place of an aggregate value *)
 [@@deriving show, ord]
 
 (** Ancestor for {!symbolic_value} iter visitor *)
-- 
cgit v1.2.3