introduce two sided active memory for typing

Author: oskgo

src/ecEnv.ml

@@ -176,7 +176,8 @@ type preenv = {
   env_comps    : mc Mip.t;
   env_locals   : (EcIdent.t * EcTypes.ty) MMsym.t;
   env_memories : EcMemory.memtype Mmem.t;
-  env_actmem   : EcMemory.memory option;
+  env_actmem_ss: EcMemory.memory option;
+  env_actmem_ts: (EcMemory.memory * EcMemory.memory) option;
   env_abs_st   : EcModules.abs_uses Mid.t;
   env_tci      : ((ty_params * ty) * tcinstance) list;
   env_tc       : TC.graph;
@@ -305,7 +306,8 @@ let empty gstate =
     env_comps    = Mip.singleton (IPPath path) (empty_mc None);
     env_locals   = MMsym.empty;
     env_memories = Mmem.empty;
-    env_actmem   = None;
+    env_actmem_ss= None;
+    env_actmem_ts= None;
     env_abs_st   = Mid.empty;
     env_tci      = [];
     env_tc       = TC.Graph.empty;
@@ -1258,18 +1260,36 @@ module Memory = struct
     try Some (Mmem.bysym me env.env_memories)
     with Not_found -> None
 
-  let set_active (me : memory) (env : env) =
+  let set_active_ss (me : memory) (env : env) =
     match byid me env with
     | None   -> raise (MEError (UnknownMemory (`Memory me)))
-    | Some _ -> { env with env_actmem = Some me }
+    | Some _ -> { env with env_actmem_ss = Some me }
 
-  let get_active (env : env) =
-    env.env_actmem
+  let get_active_ss (env : env) =
+    env.env_actmem_ss
 
-  let current (env : env) =
-    match env.env_actmem with
+  let current_ss (env : env) =
+    match env.env_actmem_ss with
     | None    -> None
     | Some me -> byid me env
+  
+  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) }
+
+  let get_active_ts (env : env) =
+    env.env_actmem_ts
+
+  let current_ts (env : env) =
+    match env.env_actmem_ts with
+    | None -> None
+    | Some (ml, mr) ->
+        match byid ml env, byid mr env with
+        | Some mel, Some mer -> Some (mel, mer)
+        | _ -> None
 
   let update (me: EcMemory.memenv) (env : env) =
     { env with env_memories = Mmem.add (fst me) (snd me) env.env_memories; }
@@ -1284,10 +1304,14 @@ module Memory = struct
       (fun env m -> push m env)
       env memenvs
 
-  let push_active memenv env =
-    set_active (EcMemory.memory memenv)
+  let push_active_ss memenv env =
+    set_active_ss (EcMemory.memory memenv)
       (push memenv env)
 
+  let push_active_ts mel mer env =
+    set_active_ts (EcMemory.memory mel) (EcMemory.memory mer)
+      (push mer (push mel env))
+
 end
 
 (* -------------------------------------------------------------------- *)
@@ -1690,15 +1714,15 @@ module Fun = struct
 
   let inv_memenv1 env =
     let mem  = EcMemory.abstract EcCoreFol.mhr in
-    Memory.push_active mem env
+    Memory.push_active_ss mem env
 
   let prF_memenv m path env =
     let fun_ = by_xpath path env in
     actmem_post m fun_
 
   let prF path env =
     let post = prF_memenv EcCoreFol.mhr path env in
-    Memory.push_active post env
+    Memory.push_active_ss post env
 
   let hoareF_memenv mem path env =
     let (ip, _) = oget (ipath_of_xpath path) in
@@ -1709,12 +1733,12 @@ module Fun = struct
 
   let hoareF mem path env =
     let pre, post = hoareF_memenv mem path env in
-    Memory.push_active pre env, Memory.push_active post env
+    Memory.push_active_ss pre env, Memory.push_active_ss post env
 
   let hoareS mem path env =
     let fun_ = by_xpath path env in
     let fd, memenv = actmem_body mem fun_ in
-    memenv, fd, Memory.push_active memenv env
+    memenv, fd, Memory.push_active_ss memenv env
 
   let equivF_memenv ml mr path1 path2 env =
     let (ip1, _) = oget (ipath_of_xpath path1) in
@@ -3588,8 +3612,11 @@ module LDecl = struct
   let fresh_ids hyps s = snd (fresh_ids (tohyps hyps) s)
 
   (* ------------------------------------------------------------------ *)
-  let push_active m lenv =
-    { lenv with le_env = Memory.push_active m lenv.le_env }
+  let push_active_ss m lenv =
+    { lenv with le_env = Memory.push_active_ss m lenv.le_env }
+
+  let push_active_ts ml mr lenv =
+    { lenv with le_env = Memory.push_active_ts ml mr lenv.le_env }
 
   let push_all l lenv =
     { lenv with le_env = Memory.push_all l lenv.le_env }

src/ecEnv.mli

@@ -64,16 +64,20 @@ type meerror =
 exception MEError of meerror
 
 module Memory : sig
-  val all         : env -> memenv list
-  val set_active  : memory -> env -> env
-  val get_active  : env -> memory option
-
-  val byid        : memory -> env -> memenv option
-  val lookup      : symbol -> env -> memenv option
-  val current     : env -> memenv option
-  val push        : memenv -> env -> env
-  val push_all    : memenv list -> env -> env
-  val push_active : memenv -> env -> env
+  val all           : env -> memenv list
+  val set_active_ss : memory -> env -> env
+  val get_active_ss : env -> memory option
+  val set_active_ts : memory -> memory -> env -> env
+  val get_active_ts : env -> (memory * memory) option
+
+  val byid          : memory -> env -> memenv option
+  val lookup        : symbol -> env -> memenv option
+  val current_ss    : env -> memenv option
+  val current_ts    : env -> (memenv * memenv) option
+  val push          : memenv -> env -> env
+  val push_all      : memenv list -> env -> env
+  val push_active_ss: memenv -> env -> env
+  val push_active_ts: memenv -> memenv -> env -> env
 end
 
 (* -------------------------------------------------------------------- *)
@@ -502,8 +506,9 @@ module LDecl : sig
 
   val clear : ?leniant:bool -> EcIdent.Sid.t -> hyps -> hyps
 
-  val push_all    : memenv list -> hyps -> hyps
-  val push_active : memenv -> hyps -> hyps
+  val push_all       : memenv list -> hyps -> hyps
+  val push_active_ss : memenv -> hyps -> hyps
+  val push_active_ts : memenv -> memenv -> hyps -> hyps
 
   val hoareF : memory -> xpath -> hyps -> hyps * hyps
   val equivF : memory -> memory -> xpath -> xpath -> hyps -> hyps * hyps

src/ecPrinting.ml

@@ -58,7 +58,7 @@ module PPEnv = struct
     | None   -> ppe
     | Some m ->
       { ppe with
-        ppe_env = EcEnv.Memory.set_active (fst m) ppe.ppe_env }
+        ppe_env = EcEnv.Memory.set_active_ss (fst m) ppe.ppe_env }
 
   let push_mem ppe ?(active = false) m =
     let ppe = { ppe with ppe_env = EcEnv.Memory.push m ppe.ppe_env } in
@@ -568,7 +568,7 @@ let msymbol_of_pv (ppe : PPEnv.t) p =
   | PVglob xp ->
     let mem =
       let env = ppe.PPEnv.ppe_env in
-      obind (EcEnv.Memory.byid^~ env) (EcEnv.Memory.get_active env) in
+      obind (EcEnv.Memory.byid^~ env) (EcEnv.Memory.get_active_ss env) in
 
     let exception Default in
 
@@ -598,7 +598,7 @@ let pp_pv ppe fmt p = pp_msymbol fmt (msymbol_of_pv ppe p)
 exception NoProjArg
 
 let get_projarg_for_var ppe x i =
-  let m = oget ~exn:NoProjArg (EcEnv.Memory.current ppe.PPEnv.ppe_env) in
+  let m = oget ~exn:NoProjArg (EcEnv.Memory.current_ss ppe.PPEnv.ppe_env) in
   if is_glob x then raise NoProjArg;
   oget ~exn:NoProjArg (EcMemory.get_name (get_loc x) (Some i) m)
 
@@ -1749,7 +1749,7 @@ and match_pp_notations
       let ue = EcUnify.UniEnv.create None in
       let ov = EcUnify.UniEnv.opentvi ue tv None in
       let hy = EcEnv.LDecl.init ppe.PPEnv.ppe_env [] in
-      let bd = match (EcEnv.Memory.get_active ppe.PPEnv.ppe_env) with
+      let bd = match (EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env) with
       | None -> form_of_expr nt.ont_body
       | Some m -> (ss_inv_of_expr m nt.ont_body).inv in
       let bd = Fsubst.f_subst_tvar ~freshen:true ov bd in
@@ -1863,15 +1863,15 @@ and pp_form_core_r
 
       if force || debug_mode then default true else
 
-      match EcEnv.Memory.get_active ppe.PPEnv.ppe_env with
+      match EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env with
       | Some i' when EcMemory.mem_equal i i' ->
           Format.fprintf fmt "%a" (pp_pv ppe) x
       | _ ->
         default false
     end
 
   | Fglob (mp, i) -> begin
-    match EcEnv.Memory.get_active ppe.PPEnv.ppe_env with
+    match EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env with
     | Some i' when EcMemory.mem_equal i i' ->
         Format.fprintf fmt "(glob %a)" (pp_topmod ppe) (EcPath.mident mp)
     | _ ->
@@ -2087,7 +2087,7 @@ and pp_form ppe fmt f =
   pp_form_r ppe (min_op_prec, `NonAssoc) fmt f
 
 and pp_expr ppe fmt e =
-  let f = match (EcEnv.Memory.get_active ppe.PPEnv.ppe_env) with
+  let f = match (EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env) with
   | None -> form_of_expr e
   | Some m -> (ss_inv_of_expr m e).inv in
   pp_form ppe fmt f

src/ecProofTyping.ml

@@ -122,7 +122,7 @@ let tc1_process_prhl_formula tc pf =
 (* ------------------------------------------------------------------ *)
 let tc1_process_stmt  ?map tc mt c =
   let hyps   = FApi.tc1_hyps tc in
-  let hyps   = LDecl.push_active (mhr,mt) hyps in
+  let hyps   = LDecl.push_active_ss (mhr,mt) hyps in
   let env    = LDecl.toenv hyps in
   let ue     = unienv_of_hyps hyps in
   let c      = Exn.recast_pe !!tc hyps (fun () -> EcTyping.transstmt ?map env ue c) in
@@ -142,7 +142,7 @@ let tc1_process_Xhl_exp tc side ty e =
   let hyps, concl = FApi.tc1_flat tc in
   let m = fst (EcFol.destr_programS side concl) in
 
-  let hyps = LDecl.push_active m hyps in
+  let hyps = LDecl.push_active_ss m hyps in
   pf_process_exp !!tc hyps `InProc ty e
 
 (* ------------------------------------------------------------------ *)
@@ -158,7 +158,7 @@ let tc1_process_Xhl_form ?side tc ty pf =
     | _            -> None
   in
 
-  let hyps = LDecl.push_active m hyps in
+  let hyps = LDecl.push_active_ss m hyps in
 
   let mv =
     Option.map
@@ -180,21 +180,21 @@ let tc1_process_Xhl_formula_xreal tc pf =
 let tc1_process_codepos_range tc (side, cpr) =
   let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
   let env = FApi.tc1_env tc in
-  let env = EcEnv.Memory.push_active me env in
+  let env = EcEnv.Memory.push_active_ss me env in
   EcTyping.trans_codepos_range env cpr
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos tc (side, cpos) =
   let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
   let env = FApi.tc1_env tc in
-  let env = EcEnv.Memory.push_active me env in
+  let env = EcEnv.Memory.push_active_ss me env in
   EcTyping.trans_codepos env cpos
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos1 tc (side, cpos) =
   let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
   let env = FApi.tc1_env tc in
-  let env = EcEnv.Memory.push_active me env in
+  let env = EcEnv.Memory.push_active_ss me env in
   EcTyping.trans_codepos1 env cpos
 
 (* ------------------------------------------------------------------ *)