From 73ef593adbefaddbb32ceac16c3ae05b277920af Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jan 2022 12:23:26 +0100
Subject: Finish implementing SymbolicToPure.translate_expansion

---
 src/SymbolicToPure.ml | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'src/SymbolicToPure.ml')

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 469021a0..bae2925b 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -406,7 +406,21 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
   let scrutinee = Place (mk_place_from_var scrutinee_var) in
   (* Translate the branches *)
   match exp with
-  | ExpandNoBranch (_, _) -> raise Unimplemented
+  | ExpandNoBranch (sexp, e) -> (
+      match sexp with
+      | V.SeConcrete _ ->
+          (* Actually, we don't *register* symbolic expansions to constant
+           * values in the symbolic ADT *)
+          failwith "Unreachable"
+      | SeMutRef (_, sv) | SeSharedRef (_, sv) ->
+          (* The (mut/shared) borrow type is extracted to identity: we thus simply
+           * introduce an reassignment *)
+          let ctx, var = fresh_var_for_symbolic_value sv ctx in
+          let e = translate_expression e ctx in
+          Let (Assignment (var, scrutinee), e)
+      | SeAdt _ ->
+          (* Should be in the [ExpandAdt] case *)
+          failwith "Unreachable")
   | ExpandAdt branches -> (
       (* We don't do the same thing if there is a branching or not *)
       match branches with
-- 
cgit v1.2.3