https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
ecFol.ml
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
 * Distributed under the terms of the CeCILL-B license *)

(* -------------------------------------------------------------------- *)
open EcUtils
open EcIdent
open EcTypes

open EcModules

type memory = EcMemory.memory

module Mp = EcPath.Mp

(* -------------------------------------------------------------------- *)
type gty =
  | GTty    of EcTypes.ty
  | GTmodty of module_type * mod_restr
  | GTmem   of EcMemory.memtype

type quantif =
  | Lforall
  | Lexists
  | Llambda

type binding = (EcIdent.t * gty) list

let mhr    = EcIdent.create "&hr"
let mleft  = EcIdent.create "&1"
let mright = EcIdent.create "&2"

type hoarecmp = FHle | FHeq | FHge

type form = {
  f_node : f_node;
  f_ty   : ty;
  f_fv   : int EcIdent.Mid.t; (* local, memory, module ident *)
  f_tag  : int;
}

and f_node =
  | Fquant  of quantif * binding * form
  | Fif     of form * form * form
  | Flet    of lpattern * form * form
  | Fint    of int (* Change this *)
  | Flocal  of EcIdent.t
  | Fpvar   of EcTypes.prog_var * memory
  | Fglob   of EcPath.mpath     * memory
  | Fop     of EcPath.path * ty list
  | Fapp    of form * form list
  | Ftuple  of form list
  | Fproj   of form * int
  | FhoareF of hoareF (* $hr / $hr *)
  | FhoareS of hoareS

  | FbdHoareF of bdHoareF (* $hr / $hr *)
  | FbdHoareS of bdHoareS

  | FequivF of equivF (* $left,$right / $left,$right *)
  | FequivS of equivS

  | FeagerF of eagerF

  | Fpr of pr (* hr *)

and eagerF = {
  eg_pr : form;
  eg_sl : stmt;  (* No local program variables *)
  eg_fl : EcPath.xpath;
  eg_fr : EcPath.xpath;
  eg_sr : stmt;  (* No local program variables *)
  eg_po : form
}

and equivF = {
  ef_pr : form;
  ef_fl : EcPath.xpath;
  ef_fr : EcPath.xpath;
  ef_po : form;
}

and equivS = {
  es_ml  : EcMemory.memenv;
  es_mr  : EcMemory.memenv;
  es_pr  : form;
  es_sl  : stmt;
  es_sr  : stmt;
  es_po  : form; }

and hoareF = {
  hf_pr : form;
  hf_f  : EcPath.xpath;
  hf_po : form;
}
and hoareS = {
  hs_m  : EcMemory.memenv;
  hs_pr : form;
  hs_s  : stmt;
  hs_po : form; }

and bdHoareF = {
  bhf_pr  : form;
  bhf_f   : EcPath.xpath;
  bhf_po  : form;
  bhf_cmp : hoarecmp;
  bhf_bd  : form;
}
and bdHoareS = {
  bhs_m   : EcMemory.memenv;
  bhs_pr  : form;
  bhs_s   : stmt;
  bhs_po  : form;
  bhs_cmp : hoarecmp;
  bhs_bd  : form;
}

and pr = memory * EcPath.xpath * form * form

type app_bd_info =
| AppNone
| AppSingle of form
| AppMult   of (form * form * form * form * form)

(*-------------------------------------------------------------------- *)
let qt_equal : quantif -> quantif -> bool = (==)
let qt_hash  : quantif -> int = Hashtbl.hash

(*-------------------------------------------------------------------- *)
let gty_equal ty1 ty2 =
  match ty1, ty2 with
  | GTty ty1, GTty ty2 ->
      EcTypes.ty_equal ty1 ty2

  | GTmodty (p1, r1), GTmodty (p2, r2)  ->
    EcModules.mty_equal p1 p2 && mr_equal r1 r2

  | GTmem mt1, GTmem mt2 ->
      EcMemory.mt_equal mt1 mt2

  | _ , _ -> false

let gty_hash = function
  | GTty ty -> EcTypes.ty_hash ty
  | GTmodty (p, _)  ->  EcModules.mty_hash p
  | GTmem _ -> 1

let gty_fv = function
  | GTty ty -> ty.ty_fv
  | GTmodty(_, (rx,r)) ->
    let fv =
      EcPath.Sm.fold (fun mp fv -> EcPath.m_fv fv mp) r EcIdent.Mid.empty in
    EcPath.Sx.fold (fun xp fv -> EcPath.x_fv fv xp) rx fv
  | GTmem mt -> EcMemory.mt_fv mt

(*-------------------------------------------------------------------- *)
let b_equal (b1 : binding) (b2 : binding) =
  let b1_equal (x1, ty1) (x2, ty2) =
    EcIdent.id_equal x1 x2 && gty_equal ty1 ty2
  in
    List.all2 b1_equal b1 b2

let b_hash (bs : binding) =
  let b1_hash (x, ty) =
    Why3.Hashcons.combine (EcIdent.tag x) (gty_hash ty)
  in
    Why3.Hashcons.combine_list b1_hash 0 bs

(* -------------------------------------------------------------------- *)
let hcmp_hash : hoarecmp -> int = Hashtbl.hash

(*-------------------------------------------------------------------- *)
let f_equal : form -> form -> bool = (==)
let f_compare f1 f2 = f2.f_tag - f1.f_tag
let f_hash f = f.f_tag
let f_fv f = f.f_fv
let f_ty f = f.f_ty

module MSHf = EcMaps.MakeMSH(struct
  type t = form
  let tag f = f.f_tag
end)

module Mf = MSHf.M
module Sf = MSHf.S
module Hf = MSHf.H

let hf_equal hf1 hf2 =
     f_equal hf1.hf_pr hf2.hf_pr
  && f_equal hf1.hf_po hf2.hf_po
  && EcPath.x_equal hf1.hf_f hf2.hf_f

let hs_equal hs1 hs2 =
     f_equal hs1.hs_pr hs2.hs_pr
  && f_equal hs1.hs_po hs2.hs_po
  && s_equal hs1.hs_s hs2.hs_s
  && EcMemory.me_equal hs1.hs_m hs2.hs_m

let bhf_equal bhf1 bhf2 =
     f_equal bhf1.bhf_pr bhf2.bhf_pr
  && f_equal bhf1.bhf_po bhf2.bhf_po
  && EcPath.x_equal bhf1.bhf_f bhf2.bhf_f
  && bhf1.bhf_cmp = bhf2.bhf_cmp
  && f_equal bhf1.bhf_bd bhf2.bhf_bd

let bhs_equal bhs1 bhs2 =
     f_equal bhs1.bhs_pr bhs2.bhs_pr
  && f_equal bhs1.bhs_po bhs2.bhs_po
  && s_equal bhs1.bhs_s bhs2.bhs_s
  && EcMemory.me_equal bhs1.bhs_m bhs2.bhs_m
  && bhs1.bhs_cmp = bhs2.bhs_cmp
  && f_equal bhs1.bhs_bd bhs2.bhs_bd

let eqf_equal ef1 ef2 =
     f_equal ef1.ef_pr ef2.ef_pr
  && f_equal ef1.ef_po ef2.ef_po
  && EcPath.x_equal ef1.ef_fl ef2.ef_fl
  && EcPath.x_equal ef1.ef_fr ef2.ef_fr

let eqs_equal es1 es2 =
     f_equal es1.es_pr es2.es_pr
  && f_equal es1.es_po es2.es_po
  && s_equal es1.es_sl es2.es_sl
  && s_equal es1.es_sr es2.es_sr
  && EcMemory.me_equal es1.es_ml es2.es_ml
  && EcMemory.me_equal es1.es_mr es2.es_mr

let egf_equal eg1 eg2 =
     f_equal eg1.eg_pr eg2.eg_pr
  && f_equal eg1.eg_po eg2.eg_po
  && EcModules.s_equal eg1.eg_sl eg2.eg_sl
  && EcPath.x_equal eg1.eg_fl eg2.eg_fl
  && EcPath.x_equal eg1.eg_fr eg2.eg_fr
  && EcModules.s_equal eg1.eg_sr eg2.eg_sr

(* -------------------------------------------------------------------- *)
let hf_hash hf =
  Why3.Hashcons.combine2
    (f_hash hf.hf_pr) (f_hash hf.hf_po) (EcPath.x_hash hf.hf_f)

let hs_hash hs =
  Why3.Hashcons.combine2
    (f_hash hs.hs_pr) (f_hash hs.hs_po) (EcModules.s_hash hs.hs_s)

let bhf_hash bhf =
  Why3.Hashcons.combine_list f_hash
    (Why3.Hashcons.combine (hcmp_hash bhf.bhf_cmp) (EcPath.x_hash bhf.bhf_f))
    [bhf.bhf_pr;bhf.bhf_po;bhf.bhf_bd]

let bhs_hash bhs =
  Why3.Hashcons.combine_list f_hash
    (Why3.Hashcons.combine (hcmp_hash bhs.bhs_cmp) (EcModules.s_hash bhs.bhs_s))
    [bhs.bhs_pr;bhs.bhs_po;bhs.bhs_bd]

let ef_hash ef =
  Why3.Hashcons.combine3
    (f_hash ef.ef_pr) (f_hash ef.ef_po)
    (EcPath.x_hash ef.ef_fl) (EcPath.x_hash ef.ef_fr)

let es_hash es =
  Why3.Hashcons.combine3
    (f_hash es.es_pr) (f_hash es.es_po)
    (EcModules.s_hash es.es_sl) (EcModules.s_hash es.es_sr)

let eg_hash eg =
  Why3.Hashcons.combine3
    (f_hash eg.eg_pr) (f_hash eg.eg_po)
    (Why3.Hashcons.combine (EcModules.s_hash eg.eg_sl) (EcPath.x_hash eg.eg_fl))
    (Why3.Hashcons.combine (EcModules.s_hash eg.eg_sr) (EcPath.x_hash eg.eg_fr))

(* -------------------------------------------------------------------- *)
module Hsform = Why3.Hashcons.Make (struct
  type t = form

  let equal_node f1 f2 =
    match f1, f2 with
    | Fquant(q1,b1,f1), Fquant(q2,b2,f2) ->
        qt_equal q1 q2 && b_equal b1 b2 && f_equal f1 f2

    | Fif(b1,t1,f1), Fif(b2,t2,f2) ->
        f_equal b1 b2 && f_equal t1 t2 && f_equal f1 f2

    | Flet(lp1,e1,f1), Flet(lp2,e2,f2) ->
        lp_equal lp1 lp2 && f_equal e1 e2 && f_equal f1 f2

    | Fint i1, Fint i2 ->
        i1 = i2

    | Flocal id1, Flocal id2 ->
        EcIdent.id_equal id1 id2

    | Fpvar(pv1,s1), Fpvar(pv2,s2) ->
        EcIdent.id_equal s1 s2 && EcTypes.pv_equal pv1 pv2

    | Fglob(mp1,m1), Fglob(mp2,m2) ->
      EcPath.m_equal mp1 mp2 && EcIdent.id_equal m1 m2

    | Fop(p1,lty1), Fop(p2,lty2) ->
        EcPath.p_equal p1 p2 && List.all2 ty_equal lty1 lty2

    | Fapp(f1,args1), Fapp(f2,args2) ->
        f_equal f1 f2 && List.all2 f_equal args1 args2

    | Ftuple args1, Ftuple args2 ->
        List.all2 f_equal args1 args2

    | Fproj(f1,i1), Fproj(f2,i2) ->
      i1 = i2 && f_equal f1 f2

    | FhoareF hf1, FhoareF hf2 -> hf_equal hf1 hf2
    | FhoareS hs1, FhoareS hs2 -> hs_equal hs1 hs2

    | FbdHoareF bhf1, FbdHoareF bhf2 -> bhf_equal bhf1 bhf2
    | FbdHoareS bhs1, FbdHoareS bhs2 -> bhs_equal bhs1 bhs2

    | FequivF eqf1, FequivF eqf2 -> eqf_equal eqf1 eqf2
    | FequivS eqs1, FequivS eqs2 -> eqs_equal eqs1 eqs2

    | FeagerF eg1, FeagerF eg2   -> egf_equal eg1 eg2

    | Fpr (m1, mp1, args1, ev1), Fpr (m2, mp2, args2, ev2) ->
           EcIdent.id_equal m1  m2
        && EcPath.x_equal   mp1 mp2
        && f_equal          ev1 ev2
        && f_equal args1 args2

    | _, _ -> false

  let equal f1 f2 =
       ty_equal f1.f_ty f2.f_ty
    && equal_node f1.f_node f2.f_node

  let hash f =
    match f.f_node with
    | Fquant(q, b, f) ->
        Why3.Hashcons.combine2 (f_hash f) (b_hash b) (qt_hash q)

    | Fif(b, t, f) ->
        Why3.Hashcons.combine2 (f_hash b) (f_hash t) (f_hash f)

    | Flet(lp, e, f) ->
        Why3.Hashcons.combine2 (lp_hash lp) (f_hash e) (f_hash f)

    | Fint i -> Hashtbl.hash i

    | Flocal id -> EcIdent.tag id

    | Fpvar(pv, m) ->
        Why3.Hashcons.combine (EcTypes.pv_hash pv) (EcIdent.id_hash m)

    | Fglob(mp, m) ->
        Why3.Hashcons.combine (EcPath.m_hash mp) (EcIdent.id_hash m)

    | Fop(p, lty) ->
        Why3.Hashcons.combine_list ty_hash (EcPath.p_hash p) lty

    | Fapp(f, args) ->
        Why3.Hashcons.combine_list f_hash (f_hash f) args

    | Ftuple args ->
        Why3.Hashcons.combine_list f_hash 0 args
    | Fproj(f,i) ->
        Why3.Hashcons.combine (f_hash f) i

    | FhoareF hf -> hf_hash hf
    | FhoareS hs -> hs_hash hs

    | FbdHoareF bhf -> bhf_hash bhf
    | FbdHoareS bhs -> bhs_hash bhs

    | FequivF ef -> ef_hash ef
    | FequivS es -> es_hash es

    | FeagerF eg  -> eg_hash eg

    | Fpr (m, mp, args, ev) ->
      Why3.Hashcons.combine3
        (EcIdent.id_hash m)
        (EcPath.x_hash   mp)
        (f_hash          args)
        (f_hash          ev)

  let fv_mlr = Sid.add mleft (Sid.singleton mright)

  let fv_node f =
    let union ex nodes =
      List.fold_left (fun s a -> fv_union s (ex a)) Mid.empty nodes
    in

    match f with
    | Fint _           -> Mid.empty
    | Fop (_, tys)     -> union (fun a -> a.ty_fv) tys
    | Fpvar (pv,m)     -> EcPath.x_fv (fv_add m Mid.empty) pv.pv_name
    | Fglob (mp,m)     -> EcPath.m_fv (fv_add m Mid.empty) mp
    | Flocal id        -> fv_singleton id
    | Fapp (f, args)   -> union f_fv (f :: args)
    | Ftuple args      -> union f_fv args
    | Fproj(e,_)       -> f_fv e
    | Fif (f1, f2, f3) -> union f_fv [f1; f2; f3]

    | Fquant(_, b, f) ->
      let do1 (id, ty) fv = fv_union (gty_fv ty) (Mid.remove id fv) in
      List.fold_right do1 b (f_fv f)

    | Flet(lp, f1, f2) ->
      let fv2 = fv_diff (f_fv f2) (lp_fv lp) in
      fv_union (f_fv f1) fv2

    | FhoareF hf ->
      let fv = fv_union (f_fv hf.hf_pr) (f_fv hf.hf_po) in
      EcPath.x_fv (Mid.remove mhr fv) hf.hf_f

    | FhoareS hs ->
      let fv = fv_union (f_fv hs.hs_pr) (f_fv hs.hs_po) in
      fv_union (EcModules.s_fv hs.hs_s) (Mid.remove (fst hs.hs_m) fv)

    | FbdHoareF bhf ->
      let fv =
        fv_union (f_fv bhf.bhf_pr)
          (fv_union (f_fv bhf.bhf_po) (f_fv bhf.bhf_bd)) in
      EcPath.x_fv (Mid.remove mhr fv) bhf.bhf_f

    | FbdHoareS bhs ->
      let fv =
        fv_union (f_fv bhs.bhs_pr)
          (fv_union (f_fv bhs.bhs_po) (f_fv bhs.bhs_bd)) in
      fv_union (EcModules.s_fv bhs.bhs_s) (Mid.remove (fst bhs.bhs_m) fv)

    | FequivF ef ->
        let fv = fv_union (f_fv ef.ef_pr) (f_fv ef.ef_po) in
        let fv = fv_diff fv fv_mlr in
        EcPath.x_fv (EcPath.x_fv fv ef.ef_fl) ef.ef_fr

    | FequivS es ->
        let fv = fv_union (f_fv es.es_pr) (f_fv es.es_po) in
        let ml, mr = fst es.es_ml, fst es.es_mr in
        let fv = fv_diff fv (Sid.add ml (Sid.singleton mr)) in
        fv_union fv
          (fv_union (EcModules.s_fv es.es_sl) (EcModules.s_fv es.es_sr))

    | FeagerF eg ->
        let fv = fv_union (f_fv eg.eg_pr) (f_fv eg.eg_po) in
        let fv = fv_diff fv fv_mlr in
        let fv = EcPath.x_fv (EcPath.x_fv fv eg.eg_fl) eg.eg_fr in
        fv_union fv
          (fv_union (EcModules.s_fv eg.eg_sl) (EcModules.s_fv eg.eg_sr))

    | Fpr (m,mp,args,event) ->
        let fve = Mid.remove mhr (f_fv event) in
        let fv  = EcPath.x_fv fve mp in
        fv_union (f_fv args) (fv_add m fv)

  let tag n f =
    let fv = fv_union (fv_node f.f_node) f.f_ty.ty_fv in
      { f with f_tag = n; f_fv = fv; }
end)

(* -------------------------------------------------------------------- *)
let mk_form node ty =  Hsform.hashcons
    { f_node = node;
      f_ty   = ty;
      f_fv   = Mid.empty;
      f_tag  = -1; }

let f_node { f_node = form } = form

let ty_bool = tbool
let ty_int  = tint
let ty_unit = tunit
let ty_real = treal

(* -------------------------------------------------------------------- *)
let f_op x tys ty = mk_form (Fop (x, tys)) ty

let f_app f args ty =
  if args = [] then f
  else match f.f_node with
  | Fapp(f',args') -> mk_form (Fapp(f', args'@args)) ty
  | _ -> mk_form (Fapp(f,args)) ty

(* -------------------------------------------------------------------- *)
let f_local x ty = mk_form (Flocal x) ty

let f_pvar x ty m = mk_form (Fpvar(x, m)) ty

let f_pvarg f ty m = f_pvar (pv_arg f) ty m

let f_pvloc f v m =
  f_pvar (EcTypes.pv_loc f v.v_name) v.v_type m

let f_pvlocs f vs m =
  List.map (fun v -> f_pvloc f v m) vs

let f_glob mp m =
  mk_form (Fglob (mp, m)) (tglob mp)

(* -------------------------------------------------------------------- *)
let f_tt    = f_op EcCoreLib.p_tt [] tunit
let f_tuple args =
  match args with
  | []  -> f_tt
  | [x] -> x
  | _   -> mk_form (Ftuple args) (ttuple (List.map f_ty args))

let f_proj f i ty = mk_form (Fproj(f, i)) ty

let f_if f1 f2 f3 =
  mk_form (Fif (f1, f2, f3)) f2.f_ty

let f_let q f1 f2 =
  mk_form (Flet (q, f1, f2)) f2.f_ty (* FIXME rename binding *)

let f_let1 x f1 f2 = f_let (LSymbol (x, f1.f_ty)) f1 f2

let destr_gty = function
  | GTty ty -> ty
  | _ -> assert false

let f_quant q b f =
  if b = [] then f
  else
    let q, b, f =
      match f.f_node with
      | Fquant(q',b',f') when q = q' -> q, b@b', f'
      | _ -> q, b , f in
    let ty =
      if q = Llambda then
        let dom = List.map (fun (_,gty) -> destr_gty gty) b in
        toarrow dom f.f_ty
      else ty_bool in
    mk_form (Fquant(q,b,f)) ty

let f_exists b f = f_quant Lexists b f
let f_forall b f = f_quant Lforall b f
let f_lambda b f = f_quant Llambda b f

let f_forall_mems bds f =
  let bds = List.map (fun (m, mt) -> (m, GTmem mt)) bds in
    f_forall bds f

(* -------------------------------------------------------------------- *)
let f_tt     = f_op EcCoreLib.p_tt [] ty_unit
let f_true   = f_op EcCoreLib.p_true [] ty_bool
let f_false  = f_op EcCoreLib.p_false [] ty_bool
let f_bool   = fun b -> if b then f_true else f_false

let fop_int_opp  = f_op EcCoreLib.p_int_opp [] (tfun tint tint)
let f_int_opp f = f_app fop_int_opp [f] tint

let rec f_int n  =
  if 0 <= n then mk_form (Fint n) ty_int
  else f_int_opp (f_int (-n))

let f_i0     = f_int 0
let f_i1     = f_int 1

let f_op_real_of_int = f_op EcCoreLib.p_real_of_int [] (tfun ty_int ty_real)
let f_real_of_int f  = f_app f_op_real_of_int [f] ty_real
let f_rint n         = f_real_of_int (f_int n)
let f_r0             = f_rint 0
let f_r1             = f_rint 1

(* -------------------------------------------------------------------- *)
let ty_fbool1 = toarrow (List.create 1 ty_bool) ty_bool
let ty_fbool2 = toarrow (List.create 2 ty_bool) ty_bool

let fop_not  = f_op EcCoreLib.p_not  [] ty_fbool1
let fop_and  = f_op EcCoreLib.p_and  [] ty_fbool2
let fop_anda = f_op EcCoreLib.p_anda [] ty_fbool2
let fop_or   = f_op EcCoreLib.p_or   [] ty_fbool2
let fop_ora  = f_op EcCoreLib.p_ora  [] ty_fbool2
let fop_imp  = f_op EcCoreLib.p_imp  [] ty_fbool2
let fop_iff  = f_op EcCoreLib.p_iff  [] ty_fbool2

let f_not  f     = f_app fop_not  [f]      ty_bool
let f_and  f1 f2 = f_app fop_and  [f1; f2] ty_bool
let f_anda f1 f2 = f_app fop_anda [f1; f2] ty_bool
let f_or   f1 f2 = f_app fop_or   [f1; f2] ty_bool
let f_ora  f1 f2 = f_app fop_ora  [f1; f2] ty_bool
let f_imp  f1 f2 = f_app fop_imp  [f1; f2] ty_bool
let f_iff  f1 f2 = f_app fop_iff  [f1; f2] ty_bool

let f_ands fs =
  match List.rev fs with
  | [] -> f_true
  | f::fs -> List.fold_left ((^~) f_and) f fs

let f_andas fs =
  match List.rev fs with
  | [] -> f_true
  | f::fs -> List.fold_left ((^~) f_anda) f fs

let f_ors fs =
  match List.rev fs with
  | [] -> f_false
  | f::fs -> List.fold_left ((^~) f_or) f fs

let f_oras fs =
  match List.rev fs with
  | [] -> f_false
  | f::fs -> List.fold_left ((^~) f_ora) f fs

let f_imps = List.fold_right f_imp

(* -------------------------------------------------------------------- *)
let fop_eq = fun ty -> f_op EcCoreLib.p_eq [ty] (toarrow [ty; ty] tbool)

let f_eq f1 f2 = f_app (fop_eq f1.f_ty) [f1; f2] ty_bool

let f_eqs fs1 fs2 =
  assert (List.length fs1 = List.length fs2);
  f_ands (List.map2 f_eq fs1 fs2)

let f_eqparams f1 ty1 vs1 m1 f2 ty2 vs2 m2 =
  let f_pvlocs f ty vs m =
    let arg = f_pvarg f ty m in
    if List.length vs = 1 then [arg]
    else
      let t = Array.of_list vs in
      let t = Array.mapi (fun i vd -> f_proj arg i vd.v_type) t in
      Array.to_list t in
  match vs1, vs2 with
  | Some vs1, Some vs2 ->
    if List.length vs1 = List.length vs1 then
      f_eqs (f_pvlocs f1 ty1 vs1 m1) (f_pvlocs f2 ty2 vs2 m2)
    else
      f_eq (f_tuple (f_pvlocs f1 ty1 vs1 m1))
        (f_tuple (f_pvlocs f2 ty2 vs2 m2))
  | Some vs1, None ->
    f_eq (f_tuple (f_pvlocs f1 ty1 vs1 m1)) (f_pvarg f2 ty2 m2)
  | None, Some vs2 ->
    f_eq (f_pvarg f1 ty1 m1) (f_tuple (f_pvlocs f2 ty2 vs2 m2))
  | None, None ->
    f_eq (f_pvarg f1 ty1 m1) (f_pvarg f2 ty2 m2)


let f_eqres f1 ty1 m1 f2 ty2 m2 =
  f_eq (f_pvar (pv_res f1) ty1 m1)  (f_pvar (pv_res f2) ty2 m2)

let f_eqglob mp1 m1 mp2 m2 =
  f_eq (f_glob mp1 m1) (f_glob mp2 m2)

(* -------------------------------------------------------------------- *)
let f_hoareS_r hs = mk_form (FhoareS hs) ty_bool

let f_hoareS hs_m hs_pr hs_s hs_po =
  f_hoareS_r { hs_m; hs_pr; hs_s; hs_po; }

let f_hoareF_r hf = mk_form (FhoareF hf) ty_bool

let f_hoareF pre f post =
  f_hoareF_r { hf_pr = pre; hf_f = f; hf_po = post }

(* -------------------------------------------------------------------- *)
let hoarecmp_opp cmp =
  match cmp with
  | FHle -> FHge
  | FHeq -> FHeq
  | FHge -> FHle

let f_bdHoareS_r bhs = mk_form (FbdHoareS bhs) ty_bool

let f_bdHoareS mem pre s post hcmp bd =
  f_bdHoareS_r { bhs_m = mem; bhs_pr = pre; bhs_s = s; bhs_po = post;
                 bhs_cmp = hcmp; bhs_bd = bd }

let f_bdHoareF_r bhf = mk_form (FbdHoareF bhf) ty_bool

let f_bdHoareF bhf_pr bhf_f bhf_po bhf_cmp bhf_bd =
  f_bdHoareF_r { bhf_pr; bhf_f; bhf_po; bhf_cmp; bhf_bd; }

let f_losslessF f = f_bdHoareF f_true f f_true FHeq f_r1

(* -------------------------------------------------------------------- *)
let f_equivS_r es = mk_form (FequivS es) ty_bool

let f_equivS es_ml es_mr es_pr es_sl es_sr es_po =
   f_equivS_r { es_ml; es_mr; es_pr; es_sl; es_sr; es_po; }

let f_equivF_r ef = mk_form (FequivF ef) ty_bool

let f_equivF pre fl fr post =
  f_equivF_r{ ef_pr = pre; ef_fl = fl; ef_fr = fr; ef_po = post }

(* -------------------------------------------------------------------- *)
let f_eagerF pre sl fl fr sr post =
  let eg = { eg_pr = pre; eg_sl = sl;eg_fl = fl;
             eg_fr = fr; eg_sr = sr; eg_po = post; } in
  mk_form (FeagerF eg) ty_bool

(* -------------------------------------------------------------------- *)
let f_pr m f args e = mk_form (Fpr (m, f, args, e)) ty_real

(* -------------------------------------------------------------------- *)
let fop_int_le    = f_op EcCoreLib.p_int_le    [] (tfun tint  (tfun tint ty_bool))
let fop_int_lt    = f_op EcCoreLib.p_int_lt    [] (tfun tint  (tfun tint ty_bool))
let fop_int_mul   = f_op EcCoreLib.p_int_mul   [] (tfun tint  (tfun tint ty_int))
let fop_int_add   = f_op EcCoreLib.p_int_add   [] (tfun tint  (tfun tint ty_int))
let fop_int_sub   = f_op EcCoreLib.p_int_sub   [] (tfun tint  (tfun tint ty_int))
let fop_int_pow   = f_op EcCoreLib.p_int_pow   [] (tfun tint  (tfun tint ty_int))
let fop_real_le   = f_op EcCoreLib.p_real_le   [] (tfun treal (tfun treal ty_bool))
let fop_real_lt   = f_op EcCoreLib.p_real_lt   [] (tfun treal (tfun treal ty_bool))
let fop_real_add  = f_op EcCoreLib.p_real_add  [] (tfun treal (tfun treal treal))
let fop_real_sub  = f_op EcCoreLib.p_real_sub  [] (tfun treal (tfun treal treal))
let fop_real_mul  = f_op EcCoreLib.p_real_mul  [] (tfun treal (tfun treal treal))
let fop_real_div  = f_op EcCoreLib.p_real_div  [] (tfun treal (tfun treal treal))

let f_int_binop op f1 f2 =
  f_app op [f1;f2] ty_bool

let f_int_le = f_int_binop fop_int_le
let f_int_lt = f_int_binop fop_int_lt

let f_int_binop op f1 f2 =
  f_app op [f1; f2] ty_int

let f_int_add = f_int_binop fop_int_add
let f_int_sub = f_int_binop fop_int_sub
let f_int_mul = f_int_binop fop_int_mul
let f_int_pow = f_int_binop fop_int_pow

let fop_int_intval = f_op EcCoreLib.p_int_intval [] (tfun tint (tfun tint (tfset tint)))

let f_int_intval k1 k2 =
  f_app fop_int_intval [k1;k2] (tfset tint)

let fop_int_sum = f_op EcCoreLib.p_int_sum [] (tfun (tfun tint treal) (tfun (tfset tint) treal))

let f_int_sum op intval ty =
  f_app fop_int_sum [op;intval] ty

(* -------------------------------------------------------------------- *)
let f_real_cmp cmp f1 f2 =
  f_app cmp [f1; f2] ty_bool

let f_real_le = f_real_cmp fop_real_le
let f_real_lt = f_real_cmp fop_real_lt

let f_real_binop op f1 f2 =
  f_app op [f1; f2] ty_real

let f_real_add = f_real_binop fop_real_add
let f_real_sub = f_real_binop fop_real_sub
let f_real_mul = f_real_binop fop_real_mul
let f_real_div = f_real_binop fop_real_div

(* -------------------------------------------------------------------- *)
let fop_in_supp ty = f_op EcCoreLib.p_in_supp [ty] (toarrow [ty; tdistr ty] tbool)
let fop_mu_x    ty = f_op EcCoreLib.p_mu_x    [ty] (toarrow [tdistr ty; ty] ty_real)
let fop_mu      ty = f_op EcCoreLib.p_mu      [ty] (toarrow [tdistr ty; tcpred ty] ty_real)

let f_in_supp f1 f2 = f_app (fop_in_supp f1.f_ty) [f1; f2] ty_bool
let f_mu_x    f1 f2 = f_app (fop_mu_x f2.f_ty) [f1; f2] ty_real
let f_mu      f1 f2 = f_app (fop_mu (proj_distr_ty f1.f_ty)) [f1; f2] ty_real

let fop_weight ty = f_op EcCoreLib.p_weight [ty] (tfun (tdistr ty) treal)
let f_weight ty d = f_app (fop_weight ty) [d] treal

(* -------------------------------------------------------------------- *)
let f_identity ?(name = "x") ty =
  let name  = EcIdent.create name in
    f_lambda [name, GTty ty] (f_local name ty)

(* -------------------------------------------------------------------- *)
exception DestrError of string

let destr_error e = raise (DestrError e)

let is_op_and p =
  EcPath.p_equal p EcCoreLib.p_and || EcPath.p_equal p EcCoreLib.p_anda

let is_op_or p =
  EcPath.p_equal p EcCoreLib.p_or || EcPath.p_equal p EcCoreLib.p_ora

let destr_app f =
  match f.f_node with
  | Fapp (f, fs) -> (f, fs)
  | _ -> (f, [])

let destr_tuple f =
  match f.f_node with
  | Ftuple fs -> fs
  | _ -> destr_error "tuple"

let destr_local f =
  match f.f_node with
  | Flocal id -> id
  | _ -> destr_error "local"

let destr_and f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when is_op_and p -> f1,f2
  | _ -> destr_error "and"

let destr_or f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when is_op_or p -> f1,f2
  | _ -> destr_error "or"

let destr_or_kind f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when is_op_or p ->
    EcPath.p_equal p EcCoreLib.p_ora, f1,f2
  | _ -> destr_error "or"

let destr_imp f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when EcPath.p_equal p EcCoreLib.p_imp ->
      f1,f2
  | _ -> destr_error "imp"

let destr_iff f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when EcPath.p_equal p EcCoreLib.p_iff ->
      f1,f2
  | _ -> destr_error "iff"

let destr_eq f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when EcPath.p_equal p EcCoreLib.p_eq ->
      f1,f2
  | _ -> destr_error "eq"

let destr_eq_or_iff f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1;f2]) when
      EcPath.p_equal p EcCoreLib.p_iff || EcPath.p_equal p EcCoreLib.p_eq ->
      f1,f2
  | _ -> destr_error "eq_or_iff"

let destr_not f =
  match f.f_node with
  | Fapp({f_node = Fop(p,_)},[f1]) when EcPath.p_equal p EcCoreLib.p_not ->
      f1
  | _ -> destr_error "not"

let destr_forall1 f =
  match f.f_node with
  | Fquant(Lforall,(x,t)::bd,p) -> x,t,f_forall bd p
  | _ -> destr_error "forall"

let destr_forall f =
  match f.f_node with
  | Fquant(Lforall,bd,p) -> bd, p
  | _ -> destr_error "forall"

let decompose_forall f =
  match f.f_node with
  | Fquant(Lforall,bd,p) -> bd, p
  | _ -> [], f

let destr_exists1 f =
  match f.f_node with
  | Fquant(Lexists,(x,t)::bd,p) -> x,t,f_exists bd p
  | _ -> destr_error "exists"

let destr_exists f =
  match f.f_node with
  | Fquant(Lexists,bd,p) -> bd, p
  | _ -> destr_error "exists"

let destr_let1 f =
  match f.f_node with
  | Flet(LSymbol(x,ty), e1,e2) -> x,ty,e1,e2
  | _ -> destr_error "let1"

let destr_equivS f =
  match f.f_node with
  | FequivS es -> es
  | _ -> destr_error "equivS"

let destr_equivF f =
  match f.f_node with
  | FequivF es -> es
  | _ -> destr_error "equivF"

let destr_eagerF f =
  match f.f_node with
  | FeagerF eg -> eg
  | _ -> destr_error "eagerF"

let destr_hoareS f =
  match f.f_node with
  | FhoareS es -> es
  | _ -> destr_error "hoareS"

let destr_hoareF f =
  match f.f_node with
  | FhoareF es -> es
  | _ -> destr_error "hoareF"

let destr_bdHoareS f =
  match f.f_node with
  | FbdHoareS es -> es
  | _ -> destr_error "bdHoareS"

let destr_bdHoareF f =
  match f.f_node with
  | FbdHoareF es -> es
  | _ -> destr_error "bdHoareF"

let destr_pr f =
  match f.f_node with
  | Fpr (m,f,a,ev) -> (m,f,a,ev)
  | _ -> destr_error "pr"

let destr_programS side f =
  match side, f.f_node with
  | None  , FhoareS   hs  -> (hs.hs_m, hs.hs_s)
  | None  , FbdHoareS bhs -> (bhs.bhs_m, bhs.bhs_s)
  | Some b, FequivS   es  -> begin
      match b with
      | true  -> (es.es_ml, es.es_sl)
      | false -> (es.es_mr, es.es_sr)
  end
  | _, _ -> destr_error "programS"

let destr_int f =
  match f.f_node with
  | Fint n -> n
  | Fapp(op,[{f_node = Fint n}]) when f_equal op fop_int_opp -> -n
  | _ -> destr_error "destr_int"

let destr_rint f =
  match f.f_node with
  | Fapp (op,[f1]) when f_equal f_op_real_of_int op ->
    begin try destr_int f1 with DestrError _ -> destr_error "destr_rint" end
  | _ -> destr_error "destr_rint"


(* -------------------------------------------------------------------- *)
let is_from_destr dt f =
  try ignore (dt f); true with DestrError _ -> false

let is_true  f = f_equal f f_true
let is_false f = f_equal f f_false

let is_tuple    f = is_from_destr destr_tuple     f
let is_local    f = is_from_destr destr_local     f
let is_and      f = is_from_destr destr_and       f
let is_or       f = is_from_destr destr_or        f
let is_not      f = is_from_destr destr_not       f
let is_imp      f = is_from_destr destr_imp       f
let is_iff      f = is_from_destr destr_iff       f
let is_eq       f = is_from_destr destr_eq        f
let is_forall   f = is_from_destr destr_forall1   f
let is_exists   f = is_from_destr destr_exists1   f
let is_let      f = is_from_destr destr_let1      f
let is_equivF   f = is_from_destr destr_equivF    f
let is_equivS   f = is_from_destr destr_equivS    f
let is_eagerF   f = is_from_destr destr_eagerF    f
let is_hoareS   f = is_from_destr destr_hoareS    f
let is_hoareF   f = is_from_destr destr_hoareF    f
let is_bdHoareS f = is_from_destr destr_bdHoareS  f
let is_bdHoareF f = is_from_destr destr_bdHoareF  f
let is_pr       f = is_from_destr destr_pr        f

let is_eq_or_iff f = (is_eq f) || (is_iff f)

(* -------------------------------------------------------------------- *)
module FSmart = struct
  type a_local = EcIdent.t * ty
  type a_pvar  = prog_var * ty * memory
  type a_quant = quantif * binding * form
  type a_if    = form tuple3
  type a_let   = lpattern * form * form
  type a_op    = EcPath.path * ty list * ty
  type a_tuple = form list
  type a_app   = form * form list * ty
  type a_proj  = form * ty

  let f_local (fp, (x, ty)) (x', ty') =
    if   x == x' && ty == ty'
    then fp
    else f_local x' ty'

  let f_pvar (fp, (pv, ty, m)) (pv', ty', m') =
    if   pv == pv' && ty == ty' && m == m'
    then fp
    else f_pvar pv' ty' m'

  let f_quant (fp, (q, b, f)) (q', b', f') =
    if   q == q' && b == b' && f == f'
    then fp
    else f_quant q' b' f'

  let f_glob (fp, (mp, m)) (mp', m') =
    if   mp == mp' && m == m'
    then fp
    else f_glob mp' m'

  let f_if (fp, (c, f1, f2)) (c', f1', f2') =
    if   c == c' && f1 == f1' && f2 == f2'
    then fp
    else f_if c' f1' f2'

  let f_let (fp, (lp, f1, f2)) (lp', f1', f2') =
    if   lp == lp' && f1 == f1' && f2 == f2'
    then fp
    else f_let lp' f1' f2'

  let f_op (fp, (op, tys, ty)) (op', tys', ty') =
    if   op == op' && tys == tys' && ty == ty'
    then fp
    else f_op op' tys' ty'

  let f_app (fp, (f, fs, ty)) (f', fs', ty') =
    if   f == f' && fs == fs' && ty == ty'
    then fp
    else f_app f' fs' ty'

  let f_tuple (fp, fs) fs' =
    if fs == fs' then fp else f_tuple fs'

  let f_proj (fp, (f, ty)) (f', ty') i =
    if   f == f' && ty == ty'
    then fp
    else f_proj f' i ty'

  let f_equivF (fp, ef) ef' =
    if eqf_equal ef ef' then fp else mk_form (FequivF ef') fp.f_ty

  let f_equivS (fp, es) es' =
    if eqs_equal es es' then fp else f_equivS_r es'

  let f_eagerF (fp, eg) eg' =
    if egf_equal eg eg' then fp else mk_form (FeagerF eg') fp.f_ty

  let f_hoareF (fp, hf) hf' =
    if hf_equal hf hf' then fp else mk_form (FhoareF hf') fp.f_ty

  let f_hoareS (fp, hs) hs' =
    if hs_equal hs hs' then fp else f_hoareS_r hs'

  let f_bdHoareF (fp, bhf) bhf' =
    if bhf_equal bhf bhf' then fp else mk_form (FbdHoareF bhf') fp.f_ty

  let f_bdHoareS (fp, bhs) bhs' =
    if bhs_equal bhs bhs' then fp else f_bdHoareS_r bhs'

  let f_pr (fp, (m, mp, args, ev)) (m', mp', args', ev') =
    if   m == m' && mp == mp' && args == args' && ev == ev'
    then fp
    else f_pr m' mp' args' ev'
end

(* -------------------------------------------------------------------- *)
let f_map gt g fp =
  match fp.f_node with
  | Fquant(q, b, f) ->
      let map_gty ((x, gty) as b1) =
        let gty' =
          match gty with
          | GTty ty ->
              let ty' = gt ty in
                if ty == ty' then gty else GTty ty'
          | _ -> gty
        in
          if gty == gty' then b1 else (x, gty')
      in

      let b' = List.Smart.map map_gty b in
      let f' = g f in
        FSmart.f_quant (fp, (q, b, f)) (q, b', f')

  | Fint  _ -> fp
  | Fglob _ -> fp

  | Fif (f1, f2, f3) ->
      FSmart.f_if (fp, (f1, f2, f3)) (g f1, g f2, g f3)

  | Flet (lp, f1, f2) ->
      FSmart.f_let (fp, (lp, f1, f2)) (lp, g f1, g f2)

  | Flocal id ->
      let ty' = gt fp.f_ty in
        FSmart.f_local (fp, (id, fp.f_ty)) (id, ty')

  | Fpvar (id, s) ->
      let ty' = gt fp.f_ty in
        FSmart.f_pvar (fp, (id, fp.f_ty, s)) (id, ty', s)

  | Fop (p, tys) ->
      let tys' = List.Smart.map gt tys in
      let ty'  = gt fp.f_ty in
        FSmart.f_op (fp, (p, tys, fp.f_ty)) (p, tys', ty')

  | Fapp (f, fs) ->
      let f'  = g f in
      let fs' = List.Smart.map g fs in
      let ty' = gt fp.f_ty in
        FSmart.f_app (fp, (f, fs, fp.f_ty)) (f', fs', ty')

  | Ftuple fs ->
      let fs' = List.Smart.map g fs in
        FSmart.f_tuple (fp, fs) fs'

  | Fproj (f, i) ->
      let f'  = g f in
      let ty' = gt fp.f_ty in
        FSmart.f_proj (fp, (f, fp.f_ty)) (f', ty') i

  | FhoareF hf ->
      let pr' = g hf.hf_pr in
      let po' = g hf.hf_po in
        FSmart.f_hoareF (fp, hf)
          { hf with hf_pr = pr'; hf_po = po'; }

  | FhoareS hs ->
      let pr' = g hs.hs_pr in
      let po' = g hs.hs_po in
        FSmart.f_hoareS (fp, hs)
          { hs with hs_pr = pr'; hs_po = po'; }

  | FbdHoareF bhf ->
      let pr' = g bhf.bhf_pr in
      let po' = g bhf.bhf_po in
      let bd' = g bhf.bhf_bd in
        FSmart.f_bdHoareF (fp, bhf)
          { bhf with bhf_pr = pr'; bhf_po = po'; bhf_bd = bd'; }

  | FbdHoareS bhs ->
      let pr' = g bhs.bhs_pr in
      let po' = g bhs.bhs_po in
      let bd' = g bhs.bhs_bd in
        FSmart.f_bdHoareS (fp, bhs)
          { bhs with bhs_pr = pr'; bhs_po = po'; bhs_bd = bd'; }

  | FequivF ef ->
      let pr' = g ef.ef_pr in
      let po' = g ef.ef_po in
        FSmart.f_equivF (fp, ef)
          { ef with ef_pr = pr'; ef_po = po'; }

  | FequivS es ->
      let pr' = g es.es_pr in
      let po' = g es.es_po in
        FSmart.f_equivS (fp, es)
          { es with es_pr = pr'; es_po = po'; }

  | FeagerF eg ->
      let pr' = g eg.eg_pr in
      let po' = g eg.eg_po in
        FSmart.f_eagerF (fp, eg)
          { eg with eg_pr = pr'; eg_po = po'; }

  | Fpr (m, mp, args, ev) ->
      let args' = g args in
      let ev'   = g ev in
        FSmart.f_pr (fp, (m, mp, args, ev)) (m, mp, args', ev')

(* -------------------------------------------------------------------- *)
let f_iter g f =
  match f.f_node with
  | Fquant(_,_,f1) -> g f1
  | Fif(f1,f2,f3) -> g f1;g f2; g f3
  | Flet(_,f1,f2) -> g f1;g f2
  | Fint _  | Flocal _ | Fpvar _ | Fglob _ | Fop _ -> ()
  | Fapp(e, es) -> g e; List.iter g es
  | Ftuple es -> List.iter g es
  | Fproj(e,_) -> g e
  | FhoareF hf -> g hf.hf_pr; g hf.hf_po
  | FhoareS hs -> g hs.hs_pr; g hs.hs_po
  | FbdHoareF bhf -> g bhf.bhf_pr; g bhf.bhf_po
  | FbdHoareS bhs -> g bhs.bhs_pr; g bhs.bhs_po
  | FequivF ef -> g ef.ef_pr; g ef.ef_po
  | FequivS es -> g es.es_pr; g es.es_po
  | FeagerF eg -> g eg.eg_pr; g eg.eg_po
  | Fpr(_,_,args,ev) -> g args; g ev

(* -------------------------------------------------------------------- *)
let rec form_of_expr mem (e: expr) =
  match e.e_node with
  | Eint n -> f_int n
  | Elocal id -> f_local id e.e_ty
  | Evar pv -> f_pvar pv e.e_ty mem
  | Eop (op,tys) -> f_op op tys e.e_ty
  | Eapp (ef,es) -> f_app (form_of_expr mem ef) (List.map (form_of_expr mem) es) e.e_ty
  | Elet (lpt,e1,e2) -> f_let lpt (form_of_expr mem e1) (form_of_expr mem e2)
  | Etuple es -> f_tuple (List.map (form_of_expr mem) es)
  | Eproj(e1,i) -> f_proj (form_of_expr mem e1) i e.e_ty
  | Eif (e1,e2,e3) ->
      f_if (form_of_expr mem e1) (form_of_expr mem e2) (form_of_expr mem e3)
  | Elam(b,e) ->
    f_lambda (List.map (fun (x,ty) -> (x,GTty ty)) b) (form_of_expr mem e)

(* -------------------------------------------------------------------- *)
type f_subst = {
  fs_freshen : bool; (* true means freshen locals *)
  fs_mp      : EcPath.mpath Mid.t;
  fs_loc     : form Mid.t;
  fs_mem     : EcIdent.t Mid.t;
  fs_sty     : ty_subst;
  fs_ty      : ty -> ty;
  fs_opdef   : (EcIdent.t list * expr) Mp.t;
}

module Fsubst = struct
  (* ------------------------------------------------------------------ *)
  let f_subst_id = {
    fs_freshen = false;
    fs_mp      = Mid.empty;
    fs_loc     = Mid.empty;
    fs_mem     = Mid.empty;
    fs_sty     = ty_subst_id;
    fs_ty      = ty_subst ty_subst_id;
    fs_opdef   = Mp.empty;
  }

  let is_subst_id s =
       s.fs_freshen = false
    && is_ty_subst_id s.fs_sty
    && Mid.is_empty s.fs_loc
    && Mid.is_empty s.fs_mem

  let f_subst_init freshen smp sty ops =
    { f_subst_id
        with fs_freshen = freshen;
             fs_mp    = smp;
             fs_sty   = sty;
             fs_ty    = ty_subst sty;
             fs_opdef = ops; }

  (* ------------------------------------------------------------------ *)
  let f_bind_local s x t =
    let merger o = assert (o = None); Some t in
      { s with fs_loc = Mid.change merger x s.fs_loc }

  let f_bind_mem s m1 m2 =
    let merger o = assert (o = None); Some m2 in
      { s with fs_mem = Mid.change merger m1 s.fs_mem }

  let f_bind_mod s x mp =
    let merger o = assert (o = None); Some mp in
    let smp = Mid.change merger x s.fs_mp in
    let sty = s.fs_sty in
    let sty = { sty with ts_mp = EcPath.m_subst sty.ts_p smp } in
      { s with fs_mp = smp; fs_sty = sty; fs_ty = ty_subst sty }

  (* ------------------------------------------------------------------ *)
  let f_rem_local s x =
    { s with fs_loc = Mid.remove x s.fs_loc }

  let f_rem_mem s m =
    { s with fs_mem = Mid.remove m s.fs_mem }

  let f_rem_mod s m =
    let smp = Mid.remove m s.fs_mp in
    let sty = s.fs_sty in
    let sty = { sty with ts_mp = EcPath.m_subst sty.ts_p smp } in

    { s with fs_mp = smp; fs_sty = sty; fs_ty = ty_subst sty }

  (* ------------------------------------------------------------------ *)
  let add_local s (x,t as xt) =
    let x' = if s.fs_freshen then EcIdent.fresh x else x in
    let t' = s.fs_ty t in
      if   x == x' && t == t'
      then (s, xt)
      else f_bind_local s x (f_local x' t'), (x',t')

  let add_locals = List.Smart.map_fold add_local

  let subst_lpattern (s: f_subst) (lp:lpattern) =
    match lp with
    | LSymbol x ->
        let (s, x') = add_local s x in
          if x == x' then (s, lp) else (s, LSymbol x')

    | LTuple xs ->
        let (s, xs') = add_locals s xs in
          if xs == xs' then (s, lp) else (s, LTuple xs')

    | LRecord (p, xs) ->
        let (s, xs') =
          List.Smart.map_fold
            (fun s ((x, t) as xt) ->
              match x with
              | None ->
                  let t' = s.fs_ty t in
                    if t == t' then (s, xt) else (s, (x, t'))
              | Some x ->
                  let (s, (x', t')) = add_local s (x, t) in
                    if   x == x' && t == t'
                    then (s, xt)
                    else (s, (Some x', t')))
            s xs
        in
          if xs == xs' then (s, lp) else (s, LRecord (p, xs'))

  let gty_subst s gty =
    if is_subst_id s then gty
    else match gty with
    | GTty ty ->
      let ty' = s.fs_ty ty in
        if ty == ty' then gty else GTty ty'

    | GTmodty(p, (rx, r)) ->
      let sub = s.fs_sty.ts_mp in
      let p'  = mty_subst s.fs_sty.ts_p sub p in
      let xsub = EcPath.x_substm s.fs_sty.ts_p s.fs_mp in
      let rx' =
        EcPath.Sx.fold
          (fun m rx' -> EcPath.Sx.add (xsub m) rx') rx
          EcPath.Sx.empty in
      let r'  =
        EcPath.Sm.fold
          (fun m r' -> EcPath.Sm.add (sub m) r') r
          EcPath.Sm.empty
      in
        if p == p' && EcPath.Sx.equal rx rx' && EcPath.Sm.equal r r' then gty
        else GTmodty(p', (rx', r'))

    | GTmem mt ->
      let mt' = EcMemory.mt_substm s.fs_sty.ts_p s.fs_mp s.fs_ty mt in
        if mt == mt' then gty else GTmem mt'

  (* ------------------------------------------------------------------ *)
  let add_binding s (x, gty as xt) =
    let gty' = gty_subst s gty in
    let x'   = if s.fs_freshen then EcIdent.fresh x else x in

    if   x == x' && gty == gty'
    then
      let s = match gty with
        | GTty    _ -> f_rem_local s x
        | GTmodty _ -> f_rem_mod   s x
        | GTmem   _ -> f_rem_mem   s x
      in
        (s, xt)
    else
      let s = match gty' with
        | GTty   ty -> f_bind_local s x (f_local x' ty)
        | GTmodty _ -> f_bind_mod s x (EcPath.mident x')
        | GTmem   _ -> f_bind_mem s x x'
      in
        (s, (x', gty'))

  let add_bindings = List.map_fold add_binding

  (* ------------------------------------------------------------------ *)
  let rec f_subst s fp =
    match fp.f_node with
    | Fquant (q, b, f) ->
        let s, b' = add_bindings s b in
        let f'    = f_subst s f in
          FSmart.f_quant (fp, (q, b, f)) (q, b', f')

    | Flet (lp, f1, f2) ->
        let f1'    = f_subst s f1 in
        let s, lp' = subst_lpattern s lp in
        let f2'    = f_subst s f2 in
          FSmart.f_let (fp, (lp, f1, f2)) (lp', f1', f2')

    | Flocal id -> begin
      match Mid.find_opt id s.fs_loc with
      | Some f -> f
      | None ->
          let ty' = s.fs_ty fp.f_ty in
            FSmart.f_local (fp, (id, fp.f_ty)) (id, ty')
    end

    | Fop (p, tys) when Mp.mem p s.fs_opdef ->
        let ty   = s.fs_ty fp.f_ty in
        let tys  = List.Smart.map s.fs_ty tys in
        let body = oget (Mp.find_opt p s.fs_opdef) in
          f_subst_op ty tys [] body

    | Fapp ({ f_node = Fop (p, tys) }, args) when Mp.mem p s.fs_opdef ->
        let ty   = s.fs_ty fp.f_ty in
        let tys  = List.Smart.map s.fs_ty tys in
        let body = oget (Mp.find_opt p s.fs_opdef) in
          f_subst_op ty tys (List.map (f_subst s) args) body

    | Fop (p, tys) ->
        let ty'  = s.fs_ty fp.f_ty in
        let tys' = List.Smart.map s.fs_ty tys in
        let p'   = s.fs_sty.ts_p p in
          FSmart.f_op (fp, (p, tys, fp.f_ty)) (p', tys', ty')

    | Fpvar (pv, m) ->
        let pv' = pv_subst (EcPath.x_substm s.fs_sty.ts_p s.fs_mp) pv in
        let m'  = Mid.find_def m m s.fs_mem in
        let ty' = s.fs_ty fp.f_ty in
          FSmart.f_pvar (fp, (pv, fp.f_ty, m)) (pv', ty', m')

    | Fglob (mp, m) ->
        let m'  = Mid.find_def m m s.fs_mem in
        let mp' = s.fs_sty.ts_mp mp in
          FSmart.f_glob (fp, (mp, m)) (mp', m')

    | FhoareF hf ->
        assert (not (Mid.mem mhr s.fs_mem) && not (Mid.mem mhr s.fs_mem));
        let pr' = f_subst s hf.hf_pr in
        let po' = f_subst s hf.hf_po in
        let mp' = EcPath.x_substm s.fs_sty.ts_p s.fs_mp hf.hf_f in
          FSmart.f_hoareF (fp, hf)
            { hf_pr = pr'; hf_po = po'; hf_f = mp'; }

    | FhoareS hs ->
        assert (not (Mid.mem (fst hs.hs_m) s.fs_mem));
        let es  = e_subst_init s.fs_freshen s.fs_sty.ts_p s.fs_ty s.fs_opdef s.fs_mp in
        let pr' = f_subst s hs.hs_pr in
        let po' = f_subst s hs.hs_po in
        let st' = EcModules.s_subst es hs.hs_s in
        let me' =
          EcMemory.me_substm s.fs_sty.ts_p s.fs_mp s.fs_mem s.fs_ty hs.hs_m in
        FSmart.f_hoareS (fp, hs)
          { hs_pr = pr'; hs_po = po'; hs_s = st'; hs_m = me'; }

    | FbdHoareF bhf ->
      assert (not (Mid.mem mhr s.fs_mem) && not (Mid.mem mhr s.fs_mem));
      let pr' = f_subst s bhf.bhf_pr in
      let po' = f_subst s bhf.bhf_po in
      let mp' = EcPath.x_substm s.fs_sty.ts_p s.fs_mp bhf.bhf_f in
      let bd' = f_subst s bhf.bhf_bd in
      FSmart.f_bdHoareF (fp, bhf)
        { bhf with bhf_pr = pr'; bhf_po = po'; bhf_f = mp'; bhf_bd = bd'; }

    | FbdHoareS bhs ->
      assert (not (Mid.mem (fst bhs.bhs_m) s.fs_mem));
      let es  = e_subst_init s.fs_freshen s.fs_sty.ts_p s.fs_ty s.fs_opdef s.fs_mp in
      let pr' = f_subst s bhs.bhs_pr in
      let po' = f_subst s bhs.bhs_po in
      let st' = EcModules.s_subst es bhs.bhs_s in
      let me' =
        EcMemory.me_substm s.fs_sty.ts_p s.fs_mp s.fs_mem s.fs_ty bhs.bhs_m in
      let bd' = f_subst s bhs.bhs_bd in
      FSmart.f_bdHoareS (fp, bhs)
        { bhs with bhs_pr = pr'; bhs_po = po'; bhs_s = st';
          bhs_bd = bd'; bhs_m  = me'; }

    | FequivF ef ->
      assert (not (Mid.mem mleft s.fs_mem) && not (Mid.mem mright s.fs_mem));
      let m_subst = EcPath.x_substm s.fs_sty.ts_p s.fs_mp in
      let pr' = f_subst s ef.ef_pr in
      let po' = f_subst s ef.ef_po in
      let fl' = m_subst ef.ef_fl in
      let fr' = m_subst ef.ef_fr in
      FSmart.f_equivF (fp, ef)
        { ef_pr = pr'; ef_po = po'; ef_fl = fl'; ef_fr = fr'; }

    | FequivS eqs ->
      assert (not (Mid.mem (fst eqs.es_ml) s.fs_mem) &&
                not (Mid.mem (fst eqs.es_mr) s.fs_mem));
      let es = e_subst_init s.fs_freshen s.fs_sty.ts_p s.fs_ty s.fs_opdef s.fs_mp in
      let s_subst = EcModules.s_subst es in

      let pr' = f_subst s eqs.es_pr in
      let po' = f_subst s eqs.es_po in
      let sl' = s_subst eqs.es_sl in
      let sr' = s_subst eqs.es_sr in
      let ml' =
        EcMemory.me_substm s.fs_sty.ts_p s.fs_mp s.fs_mem s.fs_ty eqs.es_ml in
      let mr' =
        EcMemory.me_substm s.fs_sty.ts_p s.fs_mp s.fs_mem s.fs_ty eqs.es_mr in

      FSmart.f_equivS (fp, eqs)
        { es_ml = ml'; es_mr = mr';
          es_pr = pr'; es_po = po';
          es_sl = sl'; es_sr = sr'; }

    | FeagerF eg ->
      assert (not (Mid.mem mleft s.fs_mem) && not (Mid.mem mright s.fs_mem));
      let m_subst = EcPath.x_substm s.fs_sty.ts_p s.fs_mp in
      let pr' = f_subst s eg.eg_pr in
      let po' = f_subst s eg.eg_po in
      let fl' = m_subst eg.eg_fl in
      let fr' = m_subst eg.eg_fr in

      let es = e_subst_init s.fs_freshen s.fs_sty.ts_p s.fs_ty s.fs_opdef s.fs_mp in
      let s_subst = EcModules.s_subst es in
      let sl' = s_subst eg.eg_sl in
      let sr' = s_subst eg.eg_sr in

      FSmart.f_eagerF (fp, eg)
        { eg_pr = pr'; eg_sl = sl';eg_fl = fl';
          eg_fr = fr'; eg_sr = sr'; eg_po = po'; }

    | Fpr (m, mp, args, e) ->
      assert (not (Mid.mem mhr s.fs_mem));
      let m'    = Mid.find_def m m s.fs_mem in
      let mp'   = EcPath.x_substm s.fs_sty.ts_p s.fs_mp mp in
      let args' = f_subst s args in
      let e'    = f_subst s e in

      FSmart.f_pr (fp, (m, mp, args, e)) (m', mp', args', e')

    | _ -> f_map s.fs_ty (f_subst s) fp

  and f_subst_op fty tys args (tyids, e) =
    (* FIXME: factor this out *)
    (* FIXME: is es_freshen value correct? *)
    (* FIXME: is [mhr] good as a default? *)

    let e =
      let sty = Tvar.init tyids tys in
      let sty = ty_subst { ty_subst_id with ts_v = Mid.find_opt^~ sty; } in
      let sty = { e_subst_id with
                    es_freshen = true;
                    es_ty      = sty ; } in
        e_subst sty e
    in

    let (sag, args, e) =
      match e.e_node with
      | Elam (largs, lbody) when args <> [] ->
          let largs1, largs2 = List.take_n (List.length args  ) largs in
          let  args1,  args2 = List.take_n (List.length largs1)  args in
            (Mid.of_list (List.combine (List.map fst largs1) args1),
             args2, e_lam largs2 lbody)

      | _ -> (Mid.of_list [], args, e)
    in

    let sag = { f_subst_id with fs_loc = sag } in
      f_app (f_subst sag (form_of_expr mhr e)) args fty

  (* ------------------------------------------------------------------ *)
  let f_subst_local x t =
    let s = f_bind_local f_subst_id x t in
    fun f -> if Mid.mem x f.f_fv then f_subst s f else f

  let f_subst_mem m1 m2 =
    let s = f_bind_mem f_subst_id m1 m2 in
    fun f -> if Mid.mem m1 f.f_fv then f_subst s f else f

  let f_subst_mod x mp =
    let s = f_bind_mod f_subst_id x mp in
    fun f -> if Mid.mem x f.f_fv then f_subst s f else f

  let f_subst s =
    if is_subst_id s then identity
    else f_subst s

  (* ------------------------------------------------------------------ *)
  let mapty sty =
    f_subst { f_subst_id with fs_sty = sty; fs_ty = ty_subst sty }

  let uni uidmap =
    mapty { ty_subst_id with ts_u = uidmap }

  (* ------------------------------------------------------------------ *)
  let subst_locals s =
    Hf.memo_rec 107 (fun aux f ->
      match f.f_node with
      | Flocal id ->
          (try Mid.find id s with Not_found -> f)
      | _ -> f_map (fun ty -> ty) aux f)

  let subst_local id f1 f2 =
    subst_locals (Mid.singleton id f1) f2

  (* ------------------------------------------------------------------ *)
  let init_subst_tvar s =
    let sty = { ty_subst_id with ts_v = Mid.find_opt^~ s } in
    { f_subst_id with fs_freshen = true; fs_sty = sty; fs_ty = ty_subst sty }

  let subst_tvar s =
    f_subst (init_subst_tvar s)
end

let can_subst f =
  match f.f_node with
  | Fint _ | Flocal _ | Fpvar _ | Fop _ -> true
  | _ -> false

(* -------------------------------------------------------------------- *)
let rec gcd a b = if b = 0 then a else gcd b (a mod b)

let f_int_opp_simpl f =
  match f.f_node with
  | Fapp(op,[f]) when f_equal op fop_int_opp -> f
  | _ ->
    if f_equal f_i0 f then f_i0 else f_int_opp f

let f_int_add_simpl f1 f2 =
  try f_int (destr_int f1 + destr_int f2)
  with DestrError _ ->
    if f_equal f_i0 f1 then f2
    else if f_equal f_i0 f2 then f1
    else f_int_add f1 f2

let f_int_sub_simpl f1 f2 =
  if f_equal f1 f2 then f_i0
  else
    try f_int (destr_int f1 - destr_int f2)
    with DestrError _ ->
      if f_equal f_i0 f1 then f_int_opp_simpl f2
      else if f_equal f_i0 f2 then f1
      else f_int_sub f1 f2

let f_int_mul_simpl f1 f2 =
  try f_int (destr_int f1 * destr_int f2)
  with DestrError _ ->
    if f_equal f_i0 f1 || f_equal f_i0 f2 then f_i0
    else if f_equal f_i1 f1 then f2
    else if f_equal f_i1 f2 then f1
    else f_int_mul f1 f2

let destr_rdivint f =
  match f.f_node with
  | Fapp(op,[f1;f2]) when f_equal op fop_real_div ->
    begin
      try destr_rint f1, destr_rint f2
      with DestrError _ -> destr_error "rdivint"
    end
  | _ -> destr_error "rdivint"

let norm_real_int_div n1 n2 =
  if n2 = 0 then f_real_div (f_rint n1) (f_rint n2)
  else
    let n = gcd n1 n2 in
    let n1, n2 = if n <> 1 then n1/n, n2/n else n1, n2 in
    if n1 = 0 then f_r0
    else if n2 = 1 then f_rint n1
    else if n2 < 0 then f_real_div (f_rint (-n1)) (f_rint (-n2))
    else f_real_div (f_rint n1) (f_rint n2)

let f_real_add_simpl f1 f2 =
  try f_rint (destr_rint f1 + destr_rint f2)
  with DestrError _ ->
    try
      let (n1,d1), (n2,d2) = destr_rdivint f1, destr_rdivint f2 in
      if d1 = 0 || d2 = 0 then destr_error "";
      norm_real_int_div (n1*d2 + n2*d1) (d1*d2)
    with DestrError _ ->
      if f_equal f_r0 f1 then f2
      else if f_equal f_r0 f2 then f1
      else f_real_add f1 f2

let f_real_sub_simpl f1 f2 =
  try f_rint (destr_rint f1 - destr_rint f2)
  with DestrError _ ->
    try
      let (n1,d1), (n2,d2) = destr_rdivint f1, destr_rdivint f2 in
      if d1 = 0 || d2 = 0 then destr_error "";
      norm_real_int_div (n1*d2 - n2*d1) (d1*d2)
    with DestrError _ ->
      if f_equal f_r0 f2 then f1
      else f_real_sub f1 f2

let rec f_real_mul_simpl f1 f2 =
  match f1.f_node, f2.f_node with
  | Fapp (op1,[f1_1;f1_2]), Fapp (op2,[f2_1;f2_2])
    when f_equal op1 fop_real_div && f_equal op2 fop_real_div ->
    f_real_div_simpl (f_real_mul_simpl f1_1 f2_1) (f_real_mul_simpl f1_2 f2_2)
  | _, Fapp (op2,[f2_1;f2_2]) when f_equal op2 fop_real_div ->
    f_real_div_simpl (f_real_mul_simpl f1 f2_1) f2_2
  | Fapp (op1,[f1_1;f1_2]), _ when f_equal op1 fop_real_div ->
    f_real_div_simpl (f_real_mul_simpl f1_1 f2) f1_2
  | _ ->
    try f_rint (destr_rint f1 * destr_rint f2)
    with DestrError _ ->
      if f_equal f_r0 f1 || f_equal f_r0 f2 then f_r0
      else if f_equal f_r1 f1 then f2
      else if f_equal f_r1 f2 then f1
      else f_real_mul f1 f2

and f_real_div_simpl f1 f2 =
  match f1.f_node, f2.f_node with
  | Fapp (op1,[f1_1;f1_2]), Fapp (op2,[f2_1;f2_2])
    when f_equal op1 fop_real_div && f_equal op2 fop_real_div ->
    f_real_div_simpl (f_real_mul_simpl f1_1 f2_2) (f_real_mul_simpl f1_2 f2_1)
  | _, Fapp (op2,[f2_1;f2_2])
    when f_equal op2 fop_real_div ->
    f_real_div_simpl (f_real_mul_simpl f1 f2_2) f2_1
  | Fapp (op,[f1_1;f1_2]), _
    when f_equal op fop_real_div ->
    f_real_div_simpl f1_1 (f_real_mul_simpl f1_2 f2)
  | _ ->
    try norm_real_int_div (destr_rint f1) (destr_rint f2)
    with DestrError _ ->
      if f_equal f2 f_r1 then f1
      else f_real_div f1 f2

(* -------------------------------------------------------------------- *)
let rec f_let_simpl lp f1 f2 =
  match lp with
  | LSymbol (id, _) -> begin
      match Mid.find_opt id (f_fv f2) with
      | None   -> f2
      | Some i ->
          if   i = 1 || can_subst f1
          then Fsubst.subst_local id f1 f2
          else f_let lp f1 f2
    end

  | LTuple ids -> begin
      match f1.f_node with
      | Ftuple fs ->
          let (d, s) =
            List.fold_left2 (fun (d, s) (id, ty) f1 ->
              match Mid.find_opt id (f_fv f2) with
              | None   -> (d, s)
              | Some i ->
                  if   i = 1 || can_subst f1
                  then (d, Mid.add id f1 s)
                  else (((id, ty), f1) :: d, s))
              ([], Mid.empty) ids fs
          in
            List.fold_left
              (fun f2 (id, f1) -> f_let (LSymbol id) f1 f2)
              (Fsubst.subst_locals s f2) d
      | _ ->
        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
        let tu = f_tuple (List.mapi (fun i (_,ty') -> f_proj fx i ty') ids) in
        f_let_simpl lpx f1 (f_let_simpl lp tu f2)
(*
        let check (id, _) = Mid.find_opt id (f_fv f2) = None in
          if List.for_all check ids then f2 else f_let lp f1 f2 *)
    end

  | LRecord (_, ids) ->
      (* TODO B : PY this should be simplified if possible *)
      let check (id, _) =
        match id with
        | None -> true
        | Some id -> Mid.find_opt id (f_fv f2) = None
      in
        if List.for_all check ids then f2 else f_let lp f1 f2

let f_lets_simpl =
  (* FIXME : optimize this *)
  List.fold_right (fun (lp,f1) f2 -> f_let_simpl lp f1 f2)

let rec f_app_simpl f args ty =
  if args = [] then f
  else match f.f_node,args with
    | Fquant (Llambda, bds,f), args ->
      f_betared_simpl Fsubst.f_subst_id bds f args ty
    | Fapp(f',args'),_ -> mk_form (Fapp(f', args'@args)) ty
    | _ -> mk_form (Fapp(f,args)) ty

and f_betared_simpl subst bds f args ty =
  match bds, args with
  | (x,GTty _)::bds, arg :: args ->
    f_betared_simpl (Fsubst.f_bind_local subst x arg) bds f args ty
  | (_,_)::_, _ :: _ -> assert false
  | _, [] -> f_lambda bds (Fsubst.f_subst subst f)
  | [], _ -> f_app_simpl (Fsubst.f_subst subst f) args ty

let f_betared_simpl bds f args ty =
  f_betared_simpl Fsubst.f_subst_id bds f args ty

let f_forall_simpl b f =
  let b = List.filter (fun (id,_) -> Mid.mem id (f_fv f)) b in
  f_forall b f

let f_exists_simpl b f =
  let b = List.filter (fun (id,_) -> Mid.mem id (f_fv f)) b in
  f_exists b f

let f_quant_simpl q b f =
  if q = Lforall then f_forall_simpl b f else f_exists b f

let f_not_simpl f =
  if is_not f then destr_not f
  else if is_true f then f_false
  else if is_false f then f_true
  else f_not f

let f_and_simpl f1 f2 =
  if is_true f1 then f2
  else if is_false f1 then f_false
  else if is_true f2 then f1
  else if is_false f2 then f_false
  else f_and f1 f2

let f_ands_simpl = List.fold_right f_and_simpl

let f_anda_simpl f1 f2 =
  if is_true f1 then f2
  else if is_false f1 then f_false
  else if is_true f2 then f1
  else if is_false f2 then f_false
  else f_anda f1 f2

let f_andas_simpl = List.fold_right f_anda_simpl

let f_or_simpl f1 f2 =
  if is_true f1 then f_true
  else if is_false f1 then f2
  else if is_true f2 then f_true
  else if is_false f2 then f1
  else f_or f1 f2

let f_ora_simpl f1 f2 =
  if is_true f1 then f_true
  else if is_false f1 then f2
  else if is_true f2 then f_true
  else if is_false f2 then f1
  else f_ora f1 f2

let f_imp_simpl f1 f2 =
  if is_true f1 then f2
  else if is_false f1 || is_true f2 then f_true
  else if is_false f2 then f_not_simpl f1
  else
    if f_equal f1 f2 then f_true
    else f_imp f1 f2
    (* FIXME : simplify x = f1 => f2 into x = f1 => f2{x<-f2} *)

let bool_val f =
  if is_true f then Some true
  else if is_false f then Some false
  else None

let f_proj_simpl f i ty =
  match f.f_node with
  | Ftuple args -> List.nth args i
  | _ -> f_proj f i ty

let f_if_simpl f1 f2 f3 =
  if f_equal f2 f3 then f2
  else match bool_val f1, bool_val f2, bool_val f3 with
  | Some true, _, _  -> f2
  | Some false, _, _ -> f3
  | _, Some true, _  -> f_imp_simpl (f_not_simpl f1) f3
  | _, Some false, _ -> f_anda_simpl (f_not_simpl f1) f3
  | _, _, Some true  -> f_imp_simpl f1 f2
  | _, _, Some false -> f_anda_simpl f1 f2
  | _, _, _          -> f_if f1 f2 f3

let f_imps_simpl = List.fold_right f_imp_simpl

let f_iff_simpl f1 f2 =
  if f_equal f1 f2 then f_true
  else if is_true f1 then f2
  else if is_false f1 then f_not_simpl f2
  else if is_true f2 then f1
  else if is_false f2 then f_not_simpl f1
  else f_iff f1 f2

let rec f_eq_simpl f1 f2 =
  if f_equal f1 f2 then f_true
  else match f1.f_node, f2.f_node with
  | Fint _ , Fint _ -> f_false
  | Fapp(op1, [{f_node = Fint _}]), Fapp(op2,[{f_node = Fint _}])
    when f_equal op1 f_op_real_of_int &&
      f_equal op2 f_op_real_of_int ->
    f_false
  | Fop(op1, []) ,Fop (op2, []) when
    (EcPath.p_equal op1 EcCoreLib.p_true &&
     EcPath.p_equal op2 EcCoreLib.p_false) ||
     (EcPath.p_equal op2 EcCoreLib.p_true &&
     EcPath.p_equal op1 EcCoreLib.p_false) -> f_false
  | Ftuple fs1, Ftuple fs2 when List.length fs1 = List.length fs2 ->
    f_andas_simpl (List.map2 f_eq_simpl fs1 fs2) f_true
  | _ -> f_eq f1 f2

let f_int_le_simpl f1 f2 =
  if f_equal f1 f2 then f_true
  else match f1.f_node, f2.f_node with
  | Fint x1 , Fint x2 -> f_bool (x1 <= x2)
  | _, _ -> f_int_le f1 f2

let f_int_lt_simpl f1 f2 =
  if f_equal f1 f2 then f_false
  else match f1.f_node, f2.f_node with
  | Fint x1 , Fint x2 -> f_bool (x1 < x2)
  | _, _ -> f_int_lt f1 f2

let f_real_le_simpl f1 f2 =
  if f_equal f1 f2 then f_true
  else match f1.f_node, f2.f_node with
  | Fapp(op1, [{f_node = Fint x1}]), Fapp(op2, [{f_node = Fint x2}])
    when f_equal op1 f_op_real_of_int && f_equal op2 f_op_real_of_int ->
    f_bool (x1 <= x2)
  | _, _ -> f_real_le f1 f2

let f_real_lt_simpl f1 f2 =
  if f_equal f1 f2 then f_false
  else match f1.f_node, f2.f_node with
  | Fapp(op1, [{f_node = Fint x1}]), Fapp(op2, [{f_node = Fint x2}])
    when f_equal op1 f_op_real_of_int && f_equal op2 f_op_real_of_int ->
    f_bool (x1 < x2)
  | _, _ -> f_real_lt f1 f2

(* -------------------------------------------------------------------- *)
type op_kind =
  | OK_true
  | OK_false
  | OK_not
  | OK_and   of bool
  | OK_or    of bool
  | OK_imp
  | OK_iff
  | OK_eq
  | OK_int_le
  | OK_int_lt
  | OK_real_le
  | OK_real_lt
  | OK_int_add
  | OK_int_sub
  | OK_int_mul
  | OK_int_exp
  | OK_int_opp
  | OK_real_add
  | OK_real_sub
  | OK_real_mul
  | OK_real_div
  | OK_other

let operators =
  let operators =
    [EcCoreLib.p_true    , OK_true;
     EcCoreLib.p_false   , OK_false;
     EcCoreLib.p_not     , OK_not;
     EcCoreLib.p_anda    , OK_and true;
     EcCoreLib.p_and     , OK_and false;
     EcCoreLib.p_ora     , OK_or  true;
     EcCoreLib.p_or      , OK_or  false;
     EcCoreLib.p_imp     , OK_imp;
     EcCoreLib.p_iff     , OK_iff;
     EcCoreLib.p_eq      , OK_eq;
     EcCoreLib.p_int_le  , OK_int_le;
     EcCoreLib.p_int_lt  , OK_int_lt;
     EcCoreLib.p_real_le , OK_real_le;
     EcCoreLib.p_real_lt , OK_real_lt;
     EcCoreLib.p_int_add , OK_int_add;
     EcCoreLib.p_int_sub , OK_int_sub;
     EcCoreLib.p_int_mul , OK_int_mul;
     EcCoreLib.p_int_opp , OK_int_opp;
     EcCoreLib.p_int_pow , OK_int_exp;
     EcCoreLib.p_real_add, OK_real_add;
     EcCoreLib.p_real_sub, OK_real_sub;
     EcCoreLib.p_real_mul, OK_real_mul;
     EcCoreLib.p_real_div, OK_real_div
    ]
  in

  let tbl = EcPath.Hp.create 11 in
    List.iter (fun (p, k) -> EcPath.Hp.add tbl p k) operators;
    tbl

let op_kind (p : EcPath.path) =
  try EcPath.Hp.find operators p with Not_found -> OK_other

let is_logical_op op =
  match op_kind op with
  | OK_not | OK_and _ | OK_or _ | OK_imp | OK_iff | OK_eq
  | OK_int_le| OK_int_lt | OK_real_le | OK_real_lt
  | OK_int_add | OK_int_sub | OK_int_mul
  | OK_real_add | OK_real_sub| OK_real_mul | OK_real_div -> true
  | _ -> false

(* -------------------------------------------------------------------- *)
type sform =
  | SFint   of int
  | SFlocal of EcIdent.t
  | SFpvar  of EcTypes.prog_var * memory
  | SFglob  of EcPath.mpath * memory

  | SFif    of form * form * form
  | SFlet   of lpattern * form * form
  | SFtuple of form list
  | SFproj  of form * int
  | SFquant of quantif * (EcIdent.t * gty) * form Lazy.t
  | SFtrue
  | SFfalse
  | SFnot   of form
  | SFand   of bool * (form * form)
  | SFor    of bool * (form * form)
  | SFimp   of form * form
  | SFiff   of form * form
  | SFeq    of form * form
  | SFop    of (EcPath.path * ty list) * (form list)

  | SFhoareF   of hoareF
  | SFhoareS   of hoareS
  | SFbdHoareF of bdHoareF
  | SFbdHoareS of bdHoareS
  | SFequivF   of equivF
  | SFequivS   of equivS
  | SFpr       of pr

  | SFother of form

let sform_of_op (op, ty) args =
  match op_kind op, args with
  | OK_true , [] -> SFtrue
  | OK_false, [] -> SFfalse
  | OK_not  , [f] -> SFnot f
  | OK_and b, [f1; f2] -> SFand (b, (f1, f2))
  | OK_or  b, [f1; f2] -> SFor  (b, (f1, f2))
  | OK_imp  , [f1; f2] -> SFimp (f1, f2)
  | OK_iff  , [f1; f2] -> SFiff (f1, f2)
  | OK_eq   , [f1; f2] -> SFeq  (f1, f2)
  | _ -> SFop ((op, ty), args)

let rec sform_of_form fp =
  match fp.f_node with
  | Fint   i      -> SFint   i
  | Flocal x      -> SFlocal x
  | Fpvar (x, me) -> SFpvar  (x, me)
  | Fglob (m, me) -> SFglob  (m, me)

  | Fif    (c, f1, f2)  -> SFif    (c, f1, f2)
  | Flet   (lv, f1, f2) -> SFlet   (lv, f1, f2)
  | Ftuple fs           -> SFtuple fs
  | Fproj (f, i)        -> SFproj  (f,i)

  | Fquant (_, [ ]  , f) -> sform_of_form f
  | Fquant (q, [b]  , f) -> SFquant (q, b, lazy f)
  | Fquant (q, b::bs, f) -> SFquant (q, b, lazy (f_quant q bs f))

  | FhoareF   hf -> SFhoareF   hf
  | FhoareS   hs -> SFhoareS   hs
  | FbdHoareF hf -> SFbdHoareF hf
  | FbdHoareS hs -> SFbdHoareS hs
  | FequivF   ef -> SFequivF   ef
  | FequivS   es -> SFequivS   es
  | Fpr       pr -> SFpr       pr

  | Fop (op, ty) ->
      sform_of_op (op, ty) []

  | Fapp ({ f_node = Fop (op, ty) }, args) ->
      sform_of_op (op, ty) args

  | _ -> SFother fp

(* destr_exists_prenex destructs recursively existentials in a formula
 *  whenever possible.
 * For instance:
 * - E x p1 /\ E y p2 -> [x,y] (p1 /\ p2)
 * - E x p1 /\ E x p2 -> [] (E x p1 /\ E x p2)
 * - p1 => E x p2 -> [x] (p1 => p2)
 * - E x p1 => p2 -> [] (E x p1 => p2)
 *)
let destr_exists_prenex f =
  let disjoint bds1 bds2 =
    List.for_all
      (fun (id1, _) -> List.for_all (fun (id2, _) -> id1 <> id2) bds2)
      bds1
  in

  let rec prenex_exists bds p =
    match sform_of_form p with
    | SFand (false, (f1, f2)) ->
        let (bds1, f1) = prenex_exists [] f1 in
        let (bds2, f2) = prenex_exists [] f2 in
          if   disjoint bds1 bds2
          then (bds1@bds2@bds, f_and f1 f2)
          else (bds, p)

    | SFor (false, (f1, f2)) ->
        let (bds1, f1) = prenex_exists [] f1 in
        let (bds2, f2) = prenex_exists [] f2 in
          if   disjoint bds1 bds2
          then (bds1@bds2@bds, f_or f1 f2)
          else (bds, p)

    | SFimp (f1, f2) ->
        let (bds2, f2) = prenex_exists bds f2 in
          (bds2@bds, f_imp f1 f2)

    | SFquant (Lexists, bd, lazy p) ->
        let (bds, p) = prenex_exists bds p in
          (bd::bds, p)

    | SFif (f, ft, fe) ->
        let (bds1, f1) = prenex_exists [] ft in
        let (bds2, f2) = prenex_exists [] fe in
          if   disjoint bds1 bds2
          then (bds1@bds2@bds, f_if f f1 f2)
          else (bds, p)

    | _ -> (bds, p)
  in
    (* Make it fail as with destr_exists *)
    match prenex_exists [] f with
    | [] , _ -> destr_error "exists"
    | bds, f -> (bds, f)

(* -------------------------------------------------------------------- *)
let f_check_uni f =
  let rec aux f =
    ty_check_uni f.f_ty;
    match f.f_node with
    | Fquant(_,b,f) ->
      let check_gty = function
        | (_,GTty ty) -> ty_check_uni ty
        | _ -> () in
      List.iter check_gty b;
      aux f
    | Fop(_,tys) -> List.iter ty_check_uni tys
    | _ -> f_iter aux f in
  try aux f;true with EcTypes.FoundUnivar -> false
back to top