From 38a877a0db9980d234cfe89a5528bef99620cab1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 14 Jan 2022 16:32:18 +0100
Subject: Start working on greedy symbolic value expansion and expansion before
 assignment

---
 src/Invariants.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 7664f70e..5009410e 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -621,7 +621,16 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
   in
   visitor#visit_eval_ctx (None : V.abs option) ctx
 
+(** TODO:
+    
+    - a symbolic value can't be both in proj_borrows and in the concrete env
+      (this is why we preemptively expand copyable symbolic values)
+
+ *)
+let check_symbolic_values (ctx : C.eval_ctx) : unit = raise Errors.Unimplemented
+
 let check_invariants (ctx : C.eval_ctx) : unit =
   check_loans_borrows_relation_invariant ctx;
   check_borrowed_values_invariant ctx;
-  check_typing_invariant ctx
+  check_typing_invariant ctx;
+  check_symbolic_values ctx
-- 
cgit v1.2.3