nits + remove dead code

Author: strub

src/ecMatching.ml

@@ -19,14 +19,9 @@ module Position = struct
     | `If
     | `While
     | `Assign of lvmatch
-<<<<<<< HEAD
-    | `Sample
-    | `Call
-=======
     | `Sample of lvmatch
     | `Call   of lvmatch
     | `Match
->>>>>>> origin/main
   ]
 
   and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
@@ -36,16 +31,10 @@ module Position = struct
     | `ByMatch of int option * cp_match
   ]
 
-<<<<<<< HEAD
-  type codepos1    = int * cp_base
-  type codepos     = (codepos1 * int) list * codepos1
-  type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
-=======
   type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
   type codepos1      = int * cp_base
   type codepos       = (codepos1 * codepos_brsel) list * codepos1
   type codeoffset1   = [`ByOffset of int | `ByPosition of codepos1]
->>>>>>> origin/main
 
   let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 =
     (o + offset, p)
@@ -115,18 +104,12 @@ module Zipper = struct
         match ir.i_node, cm with
         | Swhile _, `While  -> i-1
         | Sif    _, `If     -> i-1
-<<<<<<< HEAD
-        | Srnd   _, `Sample -> i-1
-        | Scall  _, `Call   -> i-1
-
-=======
         | Smatch _, `Match  -> i-1
 
         | Scall  (None, _, _), `Call `LvmNone -> i-1
 
         | Scall  (Some lv, _, _), `Call lvm
         | Srnd   (lv, _), `Sample lvm
->>>>>>> origin/main
         | Sasgn  (lv, _), `Assign lvm -> begin
             match lv, lvm with
             | _, `LvmNone -> i-1
@@ -207,35 +190,14 @@ module Zipper = struct
 
   let zipper_at_nm_cpos1
     (env        : EcEnv.env)
-<<<<<<< HEAD
-    ((cp1, sub) : codepos1 * int)
-    (s          : stmt)
-    (zpr        : ipath)
-  : (ipath * stmt) * (codepos1 * int)
-=======
     ((cp1, sub) : codepos1 * codepos_brsel)
     (s          : stmt)
     (zpr        : ipath)
   : (ipath * stmt) * (codepos1 * codepos_brsel)
->>>>>>> origin/main
   =
     let (s1, i, s2) = find_by_cpos1 env cp1 s in
     let zpr =
       match i.i_node, sub with
-<<<<<<< HEAD
-      | Swhile (e, sw), 0 ->
-          (ZWhile (e, ((s1, s2), zpr)), sw)
-
-      | Sif (e, ifs1, ifs2), 0 ->
-          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1)
-
-      | Sif (e, ifs1, ifs2), 1 ->
-          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2)
-
-      | _ -> raise InvalidCPos
-    in zpr, ((0, `ByPos (1 + List.length s1)), sub)
-
-=======
       | Swhile (e, sw), `Cond true ->
           (ZWhile (e, ((s1, s2), zpr)), sw)
 
@@ -259,7 +221,6 @@ module Zipper = struct
       | _ -> raise InvalidCPos
     in zpr, ((0, `ByPos (1 + List.length s1)), sub)
 
->>>>>>> origin/main
   let zipper_of_cpos_r (env : EcEnv.env) ((nm, cp1) : codepos) (s : stmt) =
     let (zpr, s), nm =
       List.fold_left_map

src/ecMatching.mli

@@ -14,16 +14,10 @@ module Position : sig
   type cp_match = [
     | `If
     | `While
-<<<<<<< HEAD
-    | `Assign of lvmatch
-    | `Sample
-    | `Call
-=======
     | `Match
     | `Assign of lvmatch
     | `Sample of lvmatch
     | `Call   of lvmatch
->>>>>>> origin/main
   ]
 
   and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
@@ -33,16 +27,10 @@ module Position : sig
     | `ByMatch of int option * cp_match
   ]
 
-<<<<<<< HEAD
-  type codepos1    = int * cp_base
-  type codepos     = (codepos1 * int) list * codepos1
-  type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
-=======
   type codepos_brsel = [`Cond of bool | `Match of EcSymbols.symbol]
   type codepos1      = int * cp_base
   type codepos       = (codepos1 * codepos_brsel) list * codepos1
   type codeoffset1   = [`ByOffset of int | `ByPosition of codepos1]
->>>>>>> origin/main
 
   val shift1 : offset:int -> codepos1 -> codepos1
   val shift  : offset:int -> codepos  -> codepos
@@ -54,15 +42,12 @@ end
 module Zipper : sig
   open Position
 
-<<<<<<< HEAD
-=======
   type spath_match_ctxt = {
     locals : (EcIdent.t * ty) list;
     prebr  : ((EcIdent.t * ty) list * stmt) list;
     postbr : ((EcIdent.t * ty) list * stmt) list;
   }
 
->>>>>>> origin/main
   type ipath =
   | ZTop
   | ZWhile  of expr * spath
@@ -127,18 +112,11 @@ module Zipper : sig
    *)
   val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
 
-<<<<<<< HEAD
-    (* [map cpos f s] is a special case of [fold] where the state and the
-   * out-of-band data are absent
-   *)
-   val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
-=======
   (* [map cpos env f s] is a special case of [fold] where the state and the
    * out-of-band data are absent
    *)
   val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
 
->>>>>>> origin/main
 end
 
 (* -------------------------------------------------------------------- *)

src/ecParser.mly

@@ -1459,13 +1459,8 @@ lvalue_u:
 | LPAREN p=plist2(qident, COMMA) RPAREN
    { PLvTuple p }
 
-<<<<<<< HEAD
-| x=lvalue_var DLBRACKET ti=tvars_app? es=plist1(expr, COMMA) RBRACKET
-   { PLvMap (x, ti, es) }
-=======
 | x=lvalue_var DLBRACKET ti=tvars_app? e=plist1(expr, COMMA) RBRACKET
    { PLvMap (x, ti, e) }
->>>>>>> origin/main
 
 %inline lvalue:
 | x=loc(lvalue_u) { x }
@@ -2623,16 +2618,10 @@ tac_dir:
 icodepos_r:
 | IF       { (`If     :> pcp_match) }
 | WHILE    { (`While  :> pcp_match) }
-<<<<<<< HEAD
-| LESAMPLE { (`Sample :> pcp_match) }
-| LEAT     { (`Call   :> pcp_match) }
-
-=======
 | MATCH    { (`Match  :> pcp_match) }
 
 | lvm=lvmatch LESAMPLE { (`Sample lvm :> pcp_match) }
 | lvm=lvmatch LEAT { (`Call lvm :> pcp_match) }
->>>>>>> origin/main
 | lvm=lvmatch LARROW { (`Assign lvm :> pcp_match) }
 
 lvmatch:
@@ -3293,7 +3282,6 @@ interleave_info:
 
 | PROC REWRITE side=side? pos=codepos SLASHEQ
     { Pprocrewrite (side, pos, `Simpl) }
-<<<<<<< HEAD
 
 | PROC CHANGE CIRCUIT o=codepos PLUS w=word s=brace(stmt)
     { Prwprgm (`Change (o, w, s)) }
@@ -3334,8 +3322,6 @@ bdepeq_out_info:
 
 | BDEP BITSTRING
   { Pcirc }
-=======
->>>>>>> origin/main
 
 bdhoare_split:
 | b1=sform b2=sform b3=sform?

src/ecProofTyping.ml

@@ -175,13 +175,13 @@ let tc1_process_Xhl_formula_xreal tc pf =
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos tc (side, cpos) =
-  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
+  let me, _ = EcLowPhlGoal.tc1_get_stmt_with_memory side tc in
   let env = FApi.tc1_env tc in
   let env = EcEnv.Memory.push_active 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 me, _ = EcLowPhlGoal.tc1_get_stmt_with_memory side tc in
   let env = FApi.tc1_env tc in
   let env = EcEnv.Memory.push_active me env in
   EcTyping.trans_codepos1 env cpos

src/phl/ecPhlCodeTx.ml

@@ -178,11 +178,7 @@ let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) =
     with EcProofTerm.FindOccFailure _ ->
       tc_error pe "cannot find an occurrence of the pattern"
 
-<<<<<<< HEAD
-let t_set_match_r (side : oside) (cpos : EcMatching.Position.codepos) (id : symbol) pattern tc =
-=======
 let t_set_match_r (side : oside) (cpos : Position.codepos) (id : symbol) pattern tc =
->>>>>>> origin/main
   let tr = fun side -> `SetMatch (side, cpos) in
   t_code_transform side ~bdhoare:true cpos tr
     (t_zip (set_match_stmt id pattern)) tc
@@ -363,7 +359,7 @@ let process_set (side, cpos, fresh, id, e) tc =
 
 let process_set_match (side, cpos, id, pattern) tc =
   let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
-  let me, _ = tc1_get_stmt side tc in
+  let me, _ = tc1_get_stmt_with_memory side tc in
   let hyps = LDecl.push_active me (FApi.tc1_hyps tc) in
   let ue  = EcProofTyping.unienv_of_hyps hyps in
   let ptnmap = ref Mid.empty in
@@ -472,115 +468,9 @@ let process_case ((side, pos) : side option * pcodepos) (tc : tcenv1) =
   if not (EcLowPhlGoal.is_program_logic concl kinds) then
     assert false;
 
-  let _, s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let s = EcLowPhlGoal.tc1_get_stmt side tc in
   let pos = EcProofTyping.tc1_process_codepos tc (side, pos) in
   let goals, s = EcMatching.Zipper.map env pos change s in
   let concl = EcLowPhlGoal.hl_set_stmt side concl s in
 
   FApi.xmutate1 tc `ProcCase (goals @ [concl])
-
-(* -------------------------------------------------------------------- *)
-(*             Start of Code Cryogenic Vault:                           *)
-(* -------------------------------------------------------------------- *)
-let subst_array env (me: memenv) (insts) : memenv * instr list =
-  let cache : (prog_var, prog_var array * ty) Map.t = Map.empty in
-
-  let size_of_array (arr_e: expr) = match arr_e.e_ty.ty_node with
-  | Tconstr (p, _) -> begin match (EcPath.toqsymbol p) with
-    | ["Top"; "Array256"; _], _ -> Some 256
-    | ["Top"; "Array32"; _], _ -> Some 32
-    | _, "ipoly" -> Some 256
-    | h,t -> Format.eprintf "Unknown array type %s@." (List.fold_right (fun a b -> a ^ "." ^ b) h t);
-      assert false
-    end
-  | _ -> None
-  in
-  let is_arr_read (e: expr) : bool =
-  match e.e_node with
-  | Eop (p, _) -> begin 
-    match (EcPath.toqsymbol p) with
-    | _, "_.[_]" -> true
-    | _ -> Format.eprintf "Unknown arr read %a@." (EcPrinting.pp_expr (EcPrinting.PPEnv.ofenv env)) e; false
-  end 
-  | _ -> false 
-  in
-  let is_arr_write (e: expr) : bool =
-  match e.e_node with
-  | Eop (p, _) -> begin 
-    match (EcPath.toqsymbol p) with
-    | _, "_.[_<-_]" -> true
-    | _ -> Format.eprintf "Unknown arr write %a@." (EcPrinting.pp_expr (EcPrinting.PPEnv.ofenv env)) e; false
-  end 
-  | _ -> false 
-  in
-  
-  let vars_of_array (arr_e : expr) : prog_var array option =
-    let name_from_array (arr_e : expr) : string = 
-      match arr_e.e_node with
-      | Evar (PVloc v) -> v
-      | _ -> assert false
-    in
-    let name = name_from_array arr_e in
-    match size_of_array arr_e with
-    | None -> assert false
-    | Some size -> Some ( 
-      Array.init size (fun i -> 
-        pv_loc @@ name ^ "_" ^ (string_of_int i)))
-  in
-  let array_of_vars (ty:ty) (vars: prog_var array) : expr =
-    let vars = Array.map (fun v -> e_var v ty) vars in
-    let vars = Array.map (form_of_expr (fst me)) vars in
-    let arr = Array.fold_left 
-      (fun acc v -> EcTypesafeFol.f_app_safe env EcCoreLib.CI_List.p_cons [v; acc]) 
-      (fop_empty ty)
-      (Array.rev vars)
-    in 
-    let () = Format.eprintf "type of list :%a @." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) arr.f_ty in
-    let p_of_list, o_of_list = EcEnv.Op.lookup (["Array" ^ (string_of_int @@ Array.length vars)], "of_list") env in
-    let arr = EcTypesafeFol.f_app_safe env p_of_list [Array.get vars 0; arr] in
-    let () = Format.eprintf "type of arr :%a @." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) arr.f_ty in
-    expr_of_form (fst me) arr
-
-  in
-  let rec subst_expr cache (e: expr) =
-  match e.e_node with
-  | Eapp (op, [{e_node=Evar arr_v} as arr_e; {e_node=Eint idx}]) when is_arr_read op -> 
-    begin match Map.find_opt arr_v cache with
-    | Some (vars, ty) -> (cache, e_var (Array.get vars (BI.to_int idx)) e.e_ty) 
-    | None -> let vars = vars_of_array arr_e |> Option.get in
-      (Map.add arr_v (vars, e.e_ty) cache, e_var (Array.get vars (BI.to_int idx)) e.e_ty)
-    end
-  | Eapp (op, args) -> let cache, args = List.fold_left_map (fun cache e -> subst_expr cache e) cache args in
-    (cache, e_app op args e.e_ty)
-  | _ -> (cache, e)
-  in
-
-  let subst_instr cache (i: instr) = 
-  match i.i_node with
-  | Sasgn (lv, e) -> begin match e.e_node with
-    | Eapp (op, [{e_node=Evar arr_v} as arr_e; {e_node = Eint idx}; v]) 
-      when is_arr_write op -> let cache, v = subst_expr cache v in
-      let cache, var = match Map.find_opt arr_v cache with
-      | Some (vars, ty) -> (cache, Array.get vars (BI.to_int idx))
-      | None -> let vars = vars_of_array arr_e |> Option.get in
-        (Map.add arr_v (vars, v.e_ty) cache, Array.get vars (BI.to_int idx)) in
-      (cache, i_asgn (LvVar (var, v.e_ty), v))
-    | Eapp _ -> let cache, e = subst_expr cache e in 
-      (cache, i_asgn (lv, e))
-    | _ -> (cache, i)
-    end
-  | _ -> (cache, i)
-  in
-  let cache, insts = List.fold_left_map subst_instr cache insts in
-  let arr_defs = Map.to_seq cache 
-    |> List.of_seq 
-    |> List.map (fun (arr, (vars, ty)) -> i_asgn (LvVar (arr, ty), array_of_vars ty vars))
-  in 
-  let me = Map.fold (fun (vars, ty) me -> 
-    let vars = Array.map (fun v -> match v with | PVloc v -> {ov_name = Some v; ov_type=ty} | _ -> assert false ) vars in
-    EcMemory.bindall (Array.to_list vars) me) cache me in
-  (me, insts @ arr_defs)
-  
-(* -------------------------------------------------------------------- *)
-(*               End of Code Cryogenic Vault:                           *)
-(* -------------------------------------------------------------------- *)

src/phl/ecPhlEqobs.ml

@@ -454,8 +454,6 @@ let t_eqobs_inS_ (info : sim_info) (tc : tcenv1) =
         (FApi.t_try (FApi.t_seq EcPhlSkip.t_skip t_trivial))
         (t_eqobs_inS sim eqo tc)
     | Some(p1,p2) ->
-      let p1 = EcProofTyping.tc1_process_codepos1 tc (Some `Left , p1) in
-      let p2 = EcProofTyping.tc1_process_codepos1 tc (Some `Right, p2) in
       let _,sl2 = s_split env p1 es.es_sl in
       let _,sr2 = s_split env p2 es.es_sr in
       let _, eqi =

src/phl/ecPhlRewrite.ml

@@ -41,7 +41,7 @@ let t_change
       "conclusion should be a program logic \
       (hoare | ehoare | phoare | equiv)";
 
-  let m, s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let m, s = EcLowPhlGoal.tc1_get_stmt_with_memory side tc in
   let (data, goals), s =
     EcMatching.Zipper.map (FApi.tc1_env tc) pos (change m) s in
   let concl = EcLowPhlGoal.hl_set_stmt side concl s in

src/phl/ecPhlRwEquiv.mli

@@ -9,7 +9,7 @@ open EcMatching.Position
 val t_rewrite_equiv :
   side ->
   [`LtoR | `RtoL ] ->
-  pcodepos1 ->
+  codepos1 ->
   equivF ->
   proofterm ->
   (expr list * lvalue option) option ->