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

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 38c6df3d..3d258b32 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1733,7 +1733,7 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
   and list_values (v : V.typed_value) : V.typed_avalue list * V.typed_value =
     let ty = v.V.ty in
     match v.V.value with
-    | Primitive _ -> ([], v)
+    | Literal _ -> ([], v)
     | Adt adt ->
         let avll, field_values =
           List.split (List.map list_values adt.field_values)
@@ -1841,7 +1841,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
 
     let ty = v.V.ty in
     match v.V.value with
-    | V.Primitive _ -> ([], v)
+    | V.Literal _ -> ([], v)
     | V.Bottom ->
         (* Can happen: we *do* convert dummy values to abstractions, and dummy
            values can contain bottoms *)
-- 
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/InterpreterBorrows.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterBorrows.ml')

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 3d258b32..4d67a4e4 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -452,8 +452,8 @@ let give_back_symbolic_value (_config : C.config)
   | V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
     ->
       ()
-  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin ->
-      raise (Failure "Unrechable"));
+  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate ->
+      raise (Failure "Unreachable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
-- 
cgit v1.2.3