(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-C-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
open EcParsetree
open EcUtils
open EcTypes
open EcModules
open EcMemory
open EcFol
open EcEnv
open EcPV
open EcCoreGoal

module Zpr = EcMatching.Zipper

(* -------------------------------------------------------------------- *)
type lv_subst_t = (lpattern * form) * (prog_var * memory * form) list

(* -------------------------------------------------------------------- *)
type hlform = [`Any | `Pred | `Stmt]

type hlkind = [
  | `Hoare  of hlform
  | `CHoare of hlform
  | `PHoare of hlform
  | `Equiv  of hlform
  | `Eager
]

and hlkinds = hlkind list

let hlkinds_Xhl_r (form : hlform) : hlkinds =
  [`Hoare form; `PHoare form; `Equiv form]

let hlkinds_Xhl = hlkinds_Xhl_r `Any

let hlkinds_all : hlkinds =
  [`Hoare `Any; `PHoare `Any; `Equiv `Any; `Eager]

(* -------------------------------------------------------------------- *)
let tc_error_noXhl ?(kinds : hlkinds option) pf =
  let string_of_form =
    function `Pred -> "[F]" | `Stmt -> "[S]" | `Any -> "" in

  let string_of_kind kind =
    let kind, fm =
      match kind with
      | `Hoare  fm -> ("hoare" , fm)
      | `CHoare fm -> ("choare", fm)
      | `PHoare fm -> ("phoare", fm)
      | `Equiv  fm -> ("equiv" , fm)
      | `Eager     -> ("eager" , `Any)
    in
      Printf.sprintf "%s%s" kind (fm |> string_of_form)
  in

  tc_error_lazy pf (fun fmt ->
    Format.fprintf fmt "expecting a goal of the form: %s"
      (String.concat ", " (List.map string_of_kind (odfl [] kinds))))

(* -------------------------------------------------------------------- *)
let as_phl (kind : hlkind) (dx : unit -> 'a) (pe : proofenv) =
  try dx () with DestrError _ -> tc_error_noXhl ~kinds:[kind] pe

(* -------------------------------------------------------------------- *)
let s_first proj s =
  match s.s_node with
  | []     -> None
  | i :: r ->
      try  let i = proj i in Some (i, stmt r)
      with Not_found -> None

let s_last proj s =
  match List.rev s.s_node with
  | []     -> None
  | i :: r ->
      try  let i = proj i in Some (i, stmt (List.rev r))
      with Not_found -> None

(* -------------------------------------------------------------------- *)
let pf_first_gen _kind proj pe s =
  match s_first proj s with
  | None   -> tc_error pe "invalid first instruction"
  | Some x -> x

let pf_last_gen _kind proj pe s =
  match s_last proj s with
  | None   -> tc_error pe "invalid last instruction"
  | Some x -> x

(* -------------------------------------------------------------------- *)
let pf_first_asgn   pe st = pf_first_gen  "asgn"   destr_asgn   pe st
let pf_first_rnd    pe st = pf_first_gen  "rnd"    destr_rnd    pe st
let pf_first_call   pe st = pf_first_gen  "call"   destr_call   pe st
let pf_first_if     pe st = pf_first_gen  "if"     destr_if     pe st
let pf_first_match  pe st = pf_first_gen  "match"  destr_match  pe st
let pf_first_while  pe st = pf_first_gen  "while"  destr_while  pe st
let pf_first_assert pe st = pf_first_gen  "assert" destr_assert pe st

(* -------------------------------------------------------------------- *)
let pf_last_asgn   pe st = pf_last_gen  "asgn"   destr_asgn   pe st
let pf_last_rnd    pe st = pf_last_gen  "rnd"    destr_rnd    pe st
let pf_last_call   pe st = pf_last_gen  "call"   destr_call   pe st
let pf_last_if     pe st = pf_last_gen  "if"     destr_if     pe st
let pf_last_match  pe st = pf_last_gen  "match"  destr_match  pe st
let pf_last_while  pe st = pf_last_gen  "while"  destr_while  pe st
let pf_last_assert pe st = pf_last_gen  "assert" destr_assert pe st

(* -------------------------------------------------------------------- *)
let tc1_first_asgn   tc st = pf_first_asgn   !!tc st
let tc1_first_rnd    tc st = pf_first_rnd    !!tc st
let tc1_first_call   tc st = pf_first_call   !!tc st
let tc1_first_if     tc st = pf_first_if     !!tc st
let tc1_first_match  tc st = pf_first_match  !!tc st
let tc1_first_while  tc st = pf_first_while  !!tc st
let tc1_first_assert tc st = pf_first_assert !!tc st

(* -------------------------------------------------------------------- *)
let tc1_last_asgn   tc st = pf_last_asgn   !!tc st
let tc1_last_rnd    tc st = pf_last_rnd    !!tc st
let tc1_last_call   tc st = pf_last_call   !!tc st
let tc1_last_if     tc st = pf_last_if     !!tc st
let tc1_last_match  tc st = pf_last_match  !!tc st
let tc1_last_while  tc st = pf_last_while  !!tc st
let tc1_last_assert tc st = pf_last_assert !!tc st

(* -------------------------------------------------------------------- *)
(* TODO: use in change pos *)

let pf_pos_last_gen msg test pe s =
  match List.orindex test s.s_node with
  | None -> tc_error pe "can not find the last %s instruction" msg
  | Some i -> i

let pf_pos_last_asgn   pe s = pf_pos_last_gen "asgn"   is_asgn   pe s
let pf_pos_last_rnd    pe s = pf_pos_last_gen "rnd"    is_rnd    pe s
let pf_pos_last_call   pe s = pf_pos_last_gen "call"   is_call   pe s
let pf_pos_last_if     pe s = pf_pos_last_gen "if"     is_if     pe s
let pf_pos_last_match  pe s = pf_pos_last_gen "match"  is_match  pe s
let pf_pos_last_while  pe s = pf_pos_last_gen "while"  is_while  pe s
let pf_pos_last_assert pe s = pf_pos_last_gen "assert" is_assert pe s


let tc1_pos_last_asgn   tc s = pf_pos_last_asgn   !!tc s
let tc1_pos_last_rnd    tc s = pf_pos_last_rnd    !!tc s
let tc1_pos_last_call   tc s = pf_pos_last_call   !!tc s
let tc1_pos_last_if     tc s = pf_pos_last_if     !!tc s
let tc1_pos_last_match  tc s = pf_pos_last_match  !!tc s
let tc1_pos_last_while  tc s = pf_pos_last_while  !!tc s
let tc1_pos_last_assert tc s = pf_pos_last_assert !!tc s

(* -------------------------------------------------------------------- *)
let pf_as_hoareF   pe c = as_phl (`Hoare  `Pred) (fun () -> destr_hoareF   c) pe
let pf_as_hoareS   pe c = as_phl (`Hoare  `Stmt) (fun () -> destr_hoareS   c) pe
let pf_as_choareF  pe c = as_phl (`CHoare `Pred) (fun () -> destr_cHoareF  c) pe
let pf_as_choareS  pe c = as_phl (`CHoare `Stmt) (fun () -> destr_cHoareS  c) pe
let pf_as_bdhoareF pe c = as_phl (`PHoare `Pred) (fun () -> destr_bdHoareF c) pe
let pf_as_bdhoareS pe c = as_phl (`PHoare `Stmt) (fun () -> destr_bdHoareS c) pe
let pf_as_equivF   pe c = as_phl (`Equiv  `Pred) (fun () -> destr_equivF   c) pe
let pf_as_equivS   pe c = as_phl (`Equiv  `Stmt) (fun () -> destr_equivS   c) pe
let pf_as_eagerF   pe c = as_phl `Eager          (fun () -> destr_eagerF   c) pe

(* -------------------------------------------------------------------- *)
let tc1_as_hoareF   tc = pf_as_hoareF   !!tc (FApi.tc1_goal tc)
let tc1_as_hoareS   tc = pf_as_hoareS   !!tc (FApi.tc1_goal tc)
let tc1_as_choareF  tc = pf_as_choareF  !!tc (FApi.tc1_goal tc)
let tc1_as_choareS  tc = pf_as_choareS  !!tc (FApi.tc1_goal tc)
let tc1_as_bdhoareF tc = pf_as_bdhoareF !!tc (FApi.tc1_goal tc)
let tc1_as_bdhoareS tc = pf_as_bdhoareS !!tc (FApi.tc1_goal tc)
let tc1_as_equivF   tc = pf_as_equivF   !!tc (FApi.tc1_goal tc)
let tc1_as_equivS   tc = pf_as_equivS   !!tc (FApi.tc1_goal tc)
let tc1_as_eagerF   tc = pf_as_eagerF   !!tc (FApi.tc1_goal tc)

(* -------------------------------------------------------------------- *)
let tc1_get_stmt side tc =
  let concl = FApi.tc1_goal tc in
  match side, concl.f_node with
  | None, FhoareS hs -> hs.hs_s
  | None, FcHoareS hs -> hs.chs_s
  | None, FbdHoareS hs -> hs.bhs_s
  | Some _ , (FhoareS _ | FcHoareS _ | FbdHoareS _) ->
      tc_error_noXhl ~kinds:[`Hoare `Stmt; `PHoare `Stmt] !!tc
  | Some `Left, FequivS es   -> es.es_sl
  | Some `Right, FequivS es  -> es.es_sr
  | None, FequivS _ ->
      tc_error_noXhl ~kinds:[`Equiv `Stmt] !!tc
  | _            ->
      tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc

(* -------------------------------------------------------------------- *)
let get_pre f =
  match f.f_node with
  | FhoareF hf  -> Some (hf.hf_pr)
  | FhoareS hs  -> Some (hs.hs_pr)
  | FcHoareF hf  -> Some (hf.chf_pr)
  | FcHoareS hs  -> Some (hs.chs_pr)
  | FbdHoareF hf -> Some (hf.bhf_pr)
  | FbdHoareS hs -> Some (hs.bhs_pr)
  | FequivF ef   -> Some (ef.ef_pr )
  | FequivS es   -> Some (es.es_pr )
  | _            -> None

let tc1_get_pre tc =
  match get_pre (FApi.tc1_goal tc) with
  | None   -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
  | Some f -> f

(* -------------------------------------------------------------------- *)
let get_post f =
  match f.f_node with
  | FhoareF hf  -> Some (hf.hf_po )
  | FhoareS hs  -> Some (hs.hs_po )
  | FcHoareF hf  -> Some (hf.chf_po )
  | FcHoareS hs  -> Some (hs.chs_po )
  | FbdHoareF hf -> Some (hf.bhf_po)
  | FbdHoareS hs -> Some (hs.bhs_po)
  | FequivF ef   -> Some (ef.ef_po )
  | FequivS es   -> Some (es.es_po )
  | _            -> None

let tc1_get_post tc =
  match get_post (FApi.tc1_goal tc) with
  | None   -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
  | Some f -> f

(* -------------------------------------------------------------------- *)
let set_pre ~pre f =
  match f.f_node with
 | FhoareF hf  -> f_hoareF pre hf.hf_f hf.hf_po
 | FhoareS hs  -> f_hoareS_r { hs with hs_pr = pre }
 | FcHoareF hf  -> f_cHoareF pre hf.chf_f hf.chf_po hf.chf_co
 | FcHoareS hs  -> f_cHoareS_r { hs with chs_pr = pre }
 | FbdHoareF hf -> f_bdHoareF pre hf.bhf_f hf.bhf_po hf.bhf_cmp hf.bhf_bd
 | FbdHoareS hs -> f_bdHoareS_r { hs with bhs_pr = pre }
 | FequivF ef   -> f_equivF pre ef.ef_fl ef.ef_fr ef.ef_po
 | FequivS es   -> f_equivS_r { es with es_pr = pre }
 | _            -> assert false

(* -------------------------------------------------------------------- *)
exception InvalidSplit of codepos1

let s_split i s =
  let module Zpr = EcMatching.Zipper in
  try  Zpr.split_at_cpos1 i s
  with Zpr.InvalidCPos -> raise (InvalidSplit i)

let s_split_i i s =
  let module Zpr = EcMatching.Zipper in
  try  Zpr.find_by_cpos1 ~rev:false i s
  with Zpr.InvalidCPos -> raise (InvalidSplit i)

let o_split ?rev i s =
  let module Zpr = EcMatching.Zipper in
  try  Zpr.may_split_at_cpos1 ?rev i s
  with Zpr.InvalidCPos -> raise (InvalidSplit (oget i))

(* -------------------------------------------------------------------- *)
let t_hS_or_chS_or_bhS_or_eS ?th ?tch ?tbh ?te tc =
  match (FApi.tc1_goal tc).f_node with
  | FhoareS  _ when EcUtils.is_some th  -> (oget th ) tc
  | FcHoareS  _ when EcUtils.is_some tch -> (oget tch) tc
  | FbdHoareS _ when EcUtils.is_some tbh -> (oget tbh) tc
  | FequivS   _ when EcUtils.is_some te  -> (oget te ) tc

  | _ ->
    let kinds = List.flatten [
         if EcUtils.is_some th  then [`Hoare  `Stmt] else [];
         if EcUtils.is_some tch then [`CHoare `Stmt] else [];
         if EcUtils.is_some tbh then [`PHoare `Stmt] else [];
         if EcUtils.is_some te  then [`Equiv  `Stmt] else []]

    in tc_error_noXhl ~kinds !!tc

let t_hF_or_chF_or_bhF_or_eF ?th ?tch ?tbh ?te ?teg tc =
  match (FApi.tc1_goal tc).f_node with
  | FhoareF  _ when EcUtils.is_some th  -> (oget th ) tc
  | FcHoareF  _ when EcUtils.is_some tch -> (oget tch) tc
  | FbdHoareF _ when EcUtils.is_some tbh -> (oget tbh) tc
  | FequivF   _ when EcUtils.is_some te  -> (oget te ) tc
  | FeagerF   _ when EcUtils.is_some teg -> (oget teg) tc

  | _ ->
    let kinds = List.flatten [
         if EcUtils.is_some th  then [`Hoare  `Pred] else [];
         if EcUtils.is_some tch then [`CHoare `Pred] else [];
         if EcUtils.is_some tbh then [`PHoare `Pred] else [];
         if EcUtils.is_some te  then [`Equiv  `Pred] else [];
         if EcUtils.is_some teg then [`Eager       ] else []]

    in tc_error_noXhl ~kinds !!tc

(* -------------------------------------------------------------------- *)
let tag_sym_with_side name m =
  if      EcIdent.id_equal m EcFol.mleft  then (name ^ "_L")
  else if EcIdent.id_equal m EcFol.mright then (name ^ "_R")
  else    name

(* -------------------------------------------------------------------- *)
let id_of_pv pv m =
  let id = symbol_of_pv pv in
  let id = tag_sym_with_side id m in
    EcIdent.create id

(* -------------------------------------------------------------------- *)
let id_of_mp mp m =
  let name =
    match mp.EcPath.m_top with
    | `Local id -> EcIdent.name id
    | _ -> assert false
  in
    EcIdent.create (tag_sym_with_side name m)

(* -------------------------------------------------------------------- *)
let lv_subst ?c_pre m lv f = c_pre, lv, m, f

(* -------------------------------------------------------------------- *)
let mk_let_of_lv_substs_nolet env (lets, f) =
  if List.is_empty lets then f
  else
    let ps, s =
      List.fold_left (fun (ps, s) (c_pre, lv,m,f1) ->
        let c_pre = omap (PVM.subst env s) c_pre in
        let f1 = PVM.subst env s f1 in
        let s =
          match lv, f1.f_node with
          | LvVar (pv,_), _ -> PVM.add env pv m f1 s
          | LvTuple vs, Ftuple fs ->
            List.fold_left2 (fun s (pv,_) f -> PVM.add env pv m f s) s vs fs
          | LvTuple vs, _ ->
            List.fold_lefti
              (fun s i (pv,ty) -> PVM.add env pv m (f_proj f i ty) s)
              s vs in
        let ps =
          match c_pre with None -> ps | Some p -> p::ps in
        ps, s) ([], PVM.empty) lets in
    let f = PVM.subst env s f in
    f_ands_simpl (List.rev ps) f

let add_lv_subst env lv m s =
  match lv with
  | LvVar (pv,t) ->
    let id = id_of_pv pv m in
    let s = PVM.add env pv m (f_local id t) s in
    LSymbol(id, t), s

  | LvTuple pvs ->
    let s, ids =
      List.map_fold (fun s (pv,t) ->
        let id = id_of_pv pv m in
        let s = PVM.add env pv m (f_local id t) s in
        s, (id,t)) s pvs in
    LTuple ids, s

let mk_let_of_lv_substs_let env (lets, f) =
  if List.is_empty lets then f
  else
    let accu,s =
      List.fold_left (fun (accu,s) (c_pre, lv,m,f1) ->
        let c_pre = omap (PVM.subst env s) c_pre in
        let f1 = PVM.subst env s f1 in
        let lv, s = add_lv_subst env lv m s in
        (c_pre,lv,f1)::accu, s) ([],PVM.empty) lets in
    (* accu is the sequence of let in reverse order *)
    let f = PVM.subst env s f in
    (* compute the fv *)
    let _, fvlets =
      List.fold_left (fun (fv2,lets) (c_pre, lp,f1 as lpf) ->
        let fv = EcIdent.fv_diff fv2 (lp_fv lp) in
        let fv = EcIdent.fv_union (f_fv f1) fv in
        let fv = omap_dfl (fun c_pre -> EcIdent.fv_union fv (f_fv c_pre)) fv c_pre in
        fv, (lpf,fv2)::lets) (f.f_fv,[]) accu in
    (* fvlets is the sequence of let in the right order *)
    (* build the lets and perform the substitution/simplification *)
    let add_id fv (accu,s) (id,ty) f1 =
      match EcIdent.Mid.find_opt id fv with
      | None   -> (accu, s)
      | Some i ->
        if   i = 1 || can_subst f1
        then accu, Fsubst.f_bind_local s id f1
        else (LSymbol(id,ty), f1)::accu, s in

    let rlets, s =
      List.fold_left (fun (rlets,s) ((c_pre, lp,f1),fv) ->
        let c_pre = omap (Fsubst.f_subst s) c_pre in
        let f1 = Fsubst.f_subst s f1 in
        let rlet, s =
          match lp, f1.f_node with
          | LRecord _, _ -> assert false
          | LSymbol idt, _ -> add_id fv ([], s) idt f1
          | LTuple ids, Ftuple fs -> List.fold_left2 (add_id fv) ([],s) ids fs
          | LTuple ids, _ ->
            let used =
              List.fold_left (fun u (id, _) ->
                  match u, EcIdent.Mid.find_opt id fv with
                  | Some i1, Some i2 -> Some (i1+i2)
                  | None, i | i, None -> i) None ids in
            match used with
            | None -> [], s
            | Some i ->
              let (rlet,s), fx =
                if i = 1 || can_subst f1 then ([],s), f1
                else
                  let x = EcIdent.create "tpl" in
                  let ty = ttuple (List.map snd ids) in
                  let lpx = LSymbol(x,ty) in
                  let fx = f_local x ty in
                  ([lpx,f1],s), fx in
              List.fold_lefti (fun accus i (_,ty as idt) ->
                add_id fv accus idt (f_proj fx i ty)) (rlet, s) ids in
        (c_pre, rlet) :: rlets, s)
        ([],Fsubst.f_subst_id) fvlets in
    List.fold_left (fun f2 (c_pre, lpf) ->
      let f2 = List.fold_left (fun f2 (lp,f1) -> f_let lp f1 f2) f2 lpf in
      let c_pre = odfl f_true c_pre in
      f_and_simpl c_pre f2) (Fsubst.f_subst s f) rlets


let mk_let_of_lv_substs ?(uselet=true) env letsf =
  if uselet then mk_let_of_lv_substs_let env letsf
  else mk_let_of_lv_substs_nolet env letsf

(* -------------------------------------------------------------------- *)
let subst_form_lv env m lv t f =
  let lets = lv_subst m lv t in
  mk_let_of_lv_substs env ([lets], f)

(* -------------------------------------------------------------------- *)
(* Remark: m is only used to create fresh name, id_of_pv *)
let generalize_subst_ env m uelts uglob =
  let create (pv, ty) = id_of_pv pv m, GTty ty in
  let b = List.map create uelts in
  let s =
    List.fold_left2
      (fun s (pv, ty) (id, _) ->
        Mpv.add env pv (f_local id ty) s)
      Mpv.empty uelts b
  in
  let create mp = id_of_mp mp m, GTty (tglob mp) in
  let b' = List.map create uglob in
  let s  =
    List.fold_left2
      (fun s mp (id, _) ->
        Mpv.add_glob env mp (f_local id (tglob mp)) s)
      s uglob b'
  in
    (b', b, s)

let generalize_mod_ env m modi f =
  let (melts, mglob) = PV.ntr_elements modi in

  (* 1. Compute the prog-vars and the globals used in [f] *)
  let fv = PV.fv env m f in
  let felts, fglob = PV.ntr_elements fv in

  (* 2. Split [modi] into two parts:
   *    the one used in the free-vars and the others *)
  let (uelts, nelts) = List.partition (fun (pv, _) -> PV.mem_pv env pv modi) felts in
  let (uglob, nglob) = List.partition (fun mp -> PV.mem_glob env mp modi) fglob in

  (* 3. We build the related substitution *)

  (* 3.a. Add the global variables *)

  let (bd', bd, s ) = generalize_subst_ env m uelts uglob in
   (* 3.b. Check that the modify variables does not clash with
           the variables not generalized *)
  let restrs =
    List.fold_left (fun r mp ->
      let restr = NormMp.get_restr_use env mp in
      EcPath.Mm.add mp restr r) EcPath.Mm.empty mglob in
  List.iter (fun (npv,_) ->
    if is_glob npv then
      let check1 mp restr =  Mpv.check_npv_mp env (get_glob npv) mp restr in
      EcPath.Mm.iter check1 restrs) nelts;
  List.iter (fun mp ->
    let restr = NormMp.get_restr_use env mp in
    let check (npv,_) =
      if is_glob npv then
        Mpv.check_npv_mp env (get_glob npv) mp restr in
    List.iter check melts;
    let check mp' restr' = Mpv.check_mp_mp env mp restr mp' restr' in
    EcPath.Mm.iter check restrs) nglob;

  (* 3.c. Perform the substitution *)
  let s = PVM.of_mpv s m in
  let f = PVM.subst env s f in
  f_forall_simpl (bd'@bd) f, (bd', uglob), (bd, uelts)

let generalize_subst env m uelts uglob =
  let (b',b,f) = generalize_subst_ env m uelts uglob in
  b'@b, f

let generalize_mod env m modi f =
  let res, _, _ = generalize_mod_ env m modi f in
  res

(* -------------------------------------------------------------------- *)
let abstract_info env f1 =
  let f   = EcEnv.NormMp.norm_xfun env f1 in
  let top = EcPath.m_functor f.EcPath.x_top in
  let def = EcEnv.Fun.by_xpath f env in

  let oi  =
    match def.f_def with
    | FBabs oi -> oi
    | _ ->
      let ppe = EcPrinting.PPEnv.ofenv env in
        if EcPath.x_equal f1 f then
          EcCoreGoal.tacuerror
            "The function %a should be abstract"
            (EcPrinting.pp_funname ppe) f1
        else
          EcCoreGoal.tacuerror
            "The function %a, which reduces to %a, should be abstract"
            (EcPrinting.pp_funname ppe) f1
            (EcPrinting.pp_funname ppe) f
  in
    (top, f, oi, def.f_sig)

(* -------------------------------------------------------------------- *)
let abstract_info2 env fl' fr' =
  let (topl, fl, oil, sigl) = abstract_info env fl' in
  let (topr, fr, oir, sigr) = abstract_info env fr' in
  let fl1 = EcPath.xpath topl fl.EcPath.x_sub in
  let fr1 = EcPath.xpath topr fr.EcPath.x_sub in
    if not (EcPath.x_equal fl1 fr1) then begin
      let ppe = EcPrinting.PPEnv.ofenv env in
        EcCoreGoal.tacuerror
          "function %a reduces to %a and %a reduces to %a, %a and %a should be equal"
          (EcPrinting.pp_funname ppe) fl'
          (EcPrinting.pp_funname ppe) fl1
          (EcPrinting.pp_funname ppe) fr'
          (EcPrinting.pp_funname ppe) fr1
          (EcPrinting.pp_funname ppe) fl1
          (EcPrinting.pp_funname ppe) fr1
    end;
    ((topl, fl, oil, sigl), (topr, fr, oir, sigr))

(* -------------------------------------------------------------------- *)
type code_txenv = proofenv * LDecl.hyps

type 'a code_tx =
     code_txenv -> 'a -> form pair -> memenv * stmt
   -> memenv * stmt * form list

type 'a zip_t =
     code_txenv -> form pair -> memenv -> Zpr.zipper
  -> memenv * Zpr.zipper * form list

let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
  try
    let (me, f) = Zpr.fold cenv cpos f state s in
      ((me, f, []) : memenv * _ * form list)
  with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"

let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) =
  try
    let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos cpos s) in
      ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
  with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"

(* Does not apply to cost statements if [choare] is None.
   If [choare] is [Some c], then [c] is the cost that must be **removed** in
   the premise to compensate for the difference in cost due to the inlining. *)
let t_code_transform
    (side : oside) ?(bdhoare = false) ?(choare = None) cpos tr tx tc =
  let pf = FApi.tc1_penv tc in

  match side with
  | None -> begin
      let (hyps, concl) = FApi.tc1_flat tc in

      match concl.f_node, choare with
      | FhoareS hoare, _ ->
          let pr, po = hoare.hs_pr, hoare.hs_po in
          let (me, stmt, cs) =
            tx (pf, hyps) cpos (pr, po) (hoare.hs_m, hoare.hs_s) in
          let concl = f_hoareS_r { hoare with hs_m = me; hs_s = stmt; } in
          FApi.xmutate1 tc (tr None) (cs @ [concl])

      | FcHoareS chs, Some c ->
        let pr, po = chs.chs_pr, chs.chs_po in
        let (me, stmt, cs) =
          tx (pf, hyps) cpos (pr, po) (chs.chs_m, chs.chs_s) in
        let cond, cost = EcCHoare.cost_sub_self chs.chs_co c in
        let concl = f_cHoareS_r { chs with chs_m = me;
                                           chs_s = stmt;
                                           chs_co = cost; } in
        FApi.xmutate1 tc (tr None) (cs @ [concl; cond])

      | FbdHoareS bhs, _ when bdhoare ->
          let pr, po = bhs.bhs_pr, bhs.bhs_po in
          let (me, stmt, cs) =
            tx (pf, hyps) cpos (pr, po) (bhs.bhs_m, bhs.bhs_s) in
          let concl = f_bdHoareS_r { bhs with bhs_m = me; bhs_s = stmt; } in
          FApi.xmutate1 tc (tr None) (cs @ [concl])

      | _ ->
        let kinds =
            (if bdhoare        then [`PHoare `Stmt] else [])
          @ (if choare <> None then [`CHoare `Stmt] else [])
          @ [`Hoare `Stmt] in

        tc_error_noXhl ~kinds:kinds pf
  end

  | Some side ->
      let hyps      = FApi.tc1_hyps tc in
      let es        = tc1_as_equivS tc in
      let pre, post = es.es_pr, es.es_po in
      let me, stmt     =
        match side with
        | `Left  -> (es.es_ml, es.es_sl)
        | `Right -> (es.es_mr, es.es_sr) in
      let me, stmt, cs = tx (pf, hyps) cpos (pre, post) (me, stmt) in
      let concl =
        match side with
        | `Left  -> f_equivS_r { es with es_ml = me; es_sl = stmt; }
        | `Right -> f_equivS_r { es with es_mr = me; es_sr = stmt; }
      in

      FApi.xmutate1 tc (tr (Some side)) (cs @ [concl])