make differently-sided active memories exclusive

Author: oskgo

src/ecEnv.ml

@@ -167,6 +167,11 @@ end = struct
     }
 end
 
+type actmem = [
+  | `SS of EcMemory.memory
+  | `TS of EcMemory.memory * EcMemory.memory
+]
+
 (* -------------------------------------------------------------------- *)
 type preenv = {
   env_top      : EcPath.path option;
@@ -176,8 +181,7 @@ type preenv = {
   env_comps    : mc Mip.t;
   env_locals   : (EcIdent.t * EcTypes.ty) MMsym.t;
   env_memories : EcMemory.memtype Mmem.t;
-  env_actmem_ss: EcMemory.memory option;
-  env_actmem_ts: (EcMemory.memory * EcMemory.memory) option;
+  env_actmem   : actmem option;
   env_abs_st   : EcModules.abs_uses Mid.t;
   env_tci      : ((ty_params * ty) * tcinstance) list;
   env_tc       : TC.graph;
@@ -306,8 +310,7 @@ let empty gstate =
     env_comps    = Mip.singleton (IPPath path) (empty_mc None);
     env_locals   = MMsym.empty;
     env_memories = Mmem.empty;
-    env_actmem_ss= None;
-    env_actmem_ts= None;
+    env_actmem   = None;
     env_abs_st   = Mid.empty;
     env_tci      = [];
     env_tc       = TC.Graph.empty;
@@ -1260,33 +1263,40 @@ module Memory = struct
   let set_active_ss (me : memory) (env : env) =
     match byid me env with
     | None   -> raise (MEError (UnknownMemory (`Memory me)))
-    | Some _ -> { env with env_actmem_ss = Some me }
+    | Some _ -> { env with env_actmem = Some (`SS me) }
 
   let get_active_ss (env : env) =
-    env.env_actmem_ss
+    match env.env_actmem with
+    | Some (`SS me) -> Some me
+    | _             -> None
 
   let current_ss (env : env) =
-    match env.env_actmem_ss with
-    | None    -> None
-    | Some me -> byid me env
-  
+    match env.env_actmem with
+    | Some (`SS me) -> byid me env
+    | _             -> None
+
+
   let set_active_ts (ml: memory) (mr: memory) (env : env) =
     match byid ml env, byid mr env with
     | None, _ -> raise (MEError (UnknownMemory (`Memory ml)))
     | _, None -> raise (MEError (UnknownMemory (`Memory mr)))
     | Some _, Some _ ->
-        { env with env_actmem_ts = Some (ml, mr) }
+        { env with env_actmem = Some (`TS (ml, mr)) }
 
   let get_active_ts (env : env) =
-    env.env_actmem_ts
+    match env.env_actmem with
+    | Some (`TS (ml, mr)) -> Some (ml, mr)
+    | _                   -> None
 
   let current_ts (env : env) =
-    match env.env_actmem_ts with
-    | None -> None
-    | Some (ml, mr) ->
+    match env.env_actmem with
+    | Some (`TS (ml, mr)) -> begin
         match byid ml env, byid mr env with
         | Some mel, Some mer -> Some (mel, mer)
         | _ -> None
+    end
+    | _ -> None
+
 
   let update (me: EcMemory.memenv) (env : env) =
     { env with env_memories = Mmem.add (fst me) (snd me) env.env_memories; }