address TODOs from memory softcoding PR (#817)

Author: oskgo

src/ecAst.ml

@@ -466,7 +466,6 @@ type inv =
   | Inv_ss of ss_inv
   | Inv_ts of ts_inv
 
-(* TODO: Get rid of this after refactor *)
 let inv_of_inv (inv: inv) : form =
   match inv with
   | Inv_ss ss -> ss.inv
@@ -502,20 +501,6 @@ let lift_ts_inv2 (f: ts_inv -> ts_inv -> 'a) : inv -> inv -> 'a =
   | _ -> failwith "expected only two sided invariants" in
   f
 
-(* TODO: This should be removed after refactor is done *)
-let lift_inv_adapter (f: form -> 'a) : inv -> 'a =
-  let f inv = match inv with
-  | Inv_ss ss -> f ss.inv
-  | Inv_ts ts -> f ts.inv in
-  f
-
-let lift_inv_adapter2 (f: form -> form -> 'a) : inv -> inv -> 'a =
-  let f inv1 inv2 = match inv1, inv2 with
-  | Inv_ss ss1, Inv_ss ss2 -> f ss1.inv ss2.inv
-  | Inv_ts ts1, Inv_ts ts2 -> f ts1.inv ts2.inv
-  | _ -> failwith "expected compatible invariants" in
-  f
-
 let ss_inv_generalize_left (inv: ss_inv) (m: memory) : ts_inv =
   { ml = m; mr = inv.m; inv = inv.inv }
 

src/ecAst.mli

@@ -373,8 +373,6 @@ val lift_ss_inv2 : (ss_inv -> ss_inv -> 'a) -> inv -> inv -> 'a
 val lift_ss_inv3 : (ss_inv -> ss_inv -> ss_inv -> 'a) -> inv -> inv -> inv -> 'a
 val lift_ts_inv : (ts_inv -> 'a) -> inv -> 'a
 val lift_ts_inv2 : (ts_inv -> ts_inv -> 'a) -> inv -> inv -> 'a
-val lift_inv_adapter : (form -> 'a) -> inv -> 'a
-val lift_inv_adapter2 : (form -> form -> 'a) -> inv -> inv -> 'a
 
 val ss_inv_generalize_left : ss_inv -> memory -> ts_inv
 val ss_inv_generalize_right : ss_inv -> memory -> ts_inv

src/phl/ecPhlConseq.ml

@@ -1024,7 +1024,6 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
     let m,hi,hh, h0 =
       as_seq4 (LDecl.fresh_ids (FApi.tc1_hyps tc) ["&m";"_";"_";"_"]) in
     let pre    = map_ss_inv2 f_and (bhs_pr hs) (hs_pr hs2) in
-    (* TODO: dubious *)
     let mpre   = Fsubst.f_subst_mem pre.m m pre.inv in
     let post1  = (bhs_po hs0) in
     let post   = (bhs_po hs) in

src/phl/ecPhlPr.ml

@@ -89,7 +89,6 @@ let process_ppr info tc =
       let ef   = tc1_as_equivF tc in
       let qenvl = snd (LDecl.hoareF ef.ef_ml ef.ef_fl hyps) in
       let qenvr = snd (LDecl.hoareF ef.ef_mr ef.ef_fr hyps) in
-      (* TODO: These should be one-sided *)
       let phi1 = TTC.pf_process_form_opt !!tc qenvl None phi1 in 
       let phi2 = TTC.pf_process_form_opt !!tc qenvr None phi2 in
       if not (EcReduction.EqTest.for_type (LDecl.toenv hyps) phi1.f_ty phi2.f_ty) then