From 3ab14222b0fa2b4f14cb927db4ed01c3f7e37166 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jan 2022 23:27:46 +0100
Subject: Make minor updates to InterpreterBorrows and InterpreterExpansion

---
 src/InterpreterBorrows.ml   | 16 ++++++++++------
 src/InterpreterExpansion.ml | 41 ++++++++++++++++++-----------------------
 2 files changed, 28 insertions(+), 29 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 38447fd1..eea60833 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -952,9 +952,11 @@ and end_borrows (config : C.config) (chain : borrow_or_abs_ids)
     (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun
     =
  fun cf ->
-  V.BorrowId.Set.fold
-    (fun id cf -> end_borrow config chain allowed_abs id cf)
-    lset cf
+  (* This is not necessary, but we prefer to reorder the borrow ids,
+   * so that we actually end from the smallest id to the highest id - just
+   * a matter of taste, and may make debugging easier *)
+  let ids = V.BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
+  List.fold_left (fun cf id -> end_borrow config chain allowed_abs id cf) cf ids
 
 and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
     (abs_id : V.AbstractionId.id) : cm_fun =
@@ -1035,9 +1037,11 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
 and end_abstractions (config : C.config) (chain : borrow_or_abs_ids)
     (abs_ids : V.AbstractionId.Set.t) : cm_fun =
  fun cf ->
-  V.AbstractionId.Set.fold
-    (fun id cf -> end_abstraction config chain id cf)
-    abs_ids cf
+  (* This is not necessary, but we prefer to reorder the abstraction ids,
+   * so that we actually end from the smallest id to the highest id - just
+   * a matter of taste, and may make debugging easier *)
+  let abs_ids = V.AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
+  List.fold_left (fun cf id -> end_abstraction config chain id cf) cf abs_ids
 
 and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
     (abs_id : V.AbstractionId.id) : cm_fun =
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index b3a0e3f2..734160f9 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -428,34 +428,29 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
    fun cf ctx ->
     match rty with
     (* "Regular" ADTs *)
-    | T.Adt (T.AdtId def_id, regions, types) -> (
+    | T.Adt (T.AdtId def_id, regions, types) ->
         (* Compute the expanded value - there should be exactly one because we
          * don't allow to expand enumerations with strictly more than one variant *)
         let expand_enumerations = false in
-        match
+        let seel =
           compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
             def_id regions types ctx
-        with
-        | seel ->
-            (* Check for branching *)
-            assert (List.length seel <= 1 || allow_branching);
-            (* Apply in the context *)
-            let ctxl =
-              List.map
-                (fun see ->
-                  apply_symbolic_expansion_non_borrow config original_sv see ctx)
-                seel
-            in
-            (* Continue *)
-            let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in
-            (* Synthesize *)
-            let res = S.synthesize_symbolic_expansion original_sv resl in
-            (* Return *)
-            Some res
-        | _ ->
-            failwith
-              "expand_symbolic_value_no_branching: the expansion lead to \
-               branching")
+        in
+        (* Check for branching *)
+        assert (List.length seel <= 1 || allow_branching);
+        (* Apply in the context *)
+        let ctxl =
+          List.map
+            (fun see ->
+              apply_symbolic_expansion_non_borrow config original_sv see ctx)
+            seel
+        in
+        (* Continue *)
+        let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in
+        (* Synthesize *)
+        let res = S.synthesize_symbolic_expansion original_sv resl in
+        (* Return *)
+        Some res
     (* Tuples *)
     | T.Adt (T.Tuple, [], tys) ->
         (* Generate the field values *)
-- 
cgit v1.2.3