ecFol.mli

(* -------------------------------------------------------------------- *)
open EcBigInt
open EcPath
open EcAst

(* -------------------------------------------------------------------- *)
include module type of struct include EcCoreFol end

include module type of struct include EcCoreSubst end

(* -------------------------------------------------------------------- *)
val f_bind_mod : f_subst -> EcIdent.t -> EcPath.mpath -> EcEnv.env -> f_subst

(* -------------------------------------------------------------------- *)
val f_losslessF: xpath -> form

val f_eqparams:
     EcTypes.ty -> ovariable list -> memory
  -> EcTypes.ty -> ovariable list -> memory
  -> form

val ts_inv_eqparams:
     EcTypes.ty -> ovariable list -> memory
  -> EcTypes.ty -> ovariable list -> memory
  -> ts_inv

val f_eqres:
     EcTypes.ty -> memory
  -> EcTypes.ty -> memory
  -> form

val ts_inv_eqres:
     EcTypes.ty -> memory
  -> EcTypes.ty -> memory
  -> ts_inv

val f_eqglob:
     mpath -> memory
  -> mpath -> memory
  -> form

val ts_inv_eqglob:
     mpath -> memory
  -> mpath -> memory
  -> ts_inv

(* soft-constructors - ordering *)
val f_int_le  : form -> form -> form
val f_int_lt  : form -> form -> form

(* soft-constructors - reals *)
val f_rint : zint -> form
val f_real_of_int : form -> form

val f_r0 : form
val f_r1 : form

(* soft-constructor - numbers *)
val f_real_le : form -> form -> form
val f_real_lt : form -> form -> form

val f_real_add : form -> form -> form
val f_real_opp : form -> form
val f_real_sub : form -> form -> form
val f_real_mul : form -> form -> form
val f_real_inv : form -> form
val f_real_div : form -> form -> form
val f_real_abs : form -> form
val f_decimal  : zint * (int * zint) -> form

(* soft-constructor - xreal *)
val f_xreal_le : form -> form -> form
val fop_interp_ehoare_form : form
val f_interp_ehoare_form : form -> form -> form
val f_Ep : EcTypes.ty -> form -> form -> form
val f_concave_incr : form -> form

val f_rp2xr : form -> form
val f_r2rp  : form -> form
val f_r2xr  : form -> form
val f_b2r   : form -> form
val f_b2xr  : form -> form
val f_xreal_inf : form

(* soft-constructor - map *)
val f_map_cst : EcTypes.ty -> form -> form
val f_map_get : form -> form -> EcTypes.ty -> form
val f_map_set : form -> form -> form -> form

(* soft constructors - distributions *)
val fop_support : EcTypes.ty -> form

val f_predT   : EcTypes.ty -> form
val f_support : form -> form -> form
val f_in_supp : form -> form -> form
val f_mu      : EcEnv.env -> form -> form -> form
val f_mu_x    : form -> form -> form
val f_weight   : EcTypes.ty -> form -> form
val f_lossless : EcTypes.ty -> form -> form
val f_dunit    : form -> form

(* f_dlet tya tyb (d : tya distr) (f : tya -> tyb distr) = dlet d f *)
val f_dlet : ty -> ty -> form -> form -> form
val f_dlet_simpl : ty -> ty -> form -> form -> form
val f_dmap : ty -> ty -> form -> form -> form

(* common functions *)
val f_identity : ?name:EcSymbols.symbol -> EcTypes.ty -> form

val split_sided : memory -> ts_inv -> ss_inv option
val one_sided_vs : memory -> form -> form list

(* -------------------------------------------------------------------- *)
(* "typed" soft-constructors                                            *)
val f_ty_app : EcEnv.env -> form -> form list -> form

(* -------------------------------------------------------------------- *)
(* WARNING : this function should be use only in a context ensuring
 * that the quantified variables can be instantiated *)

val f_betared : form -> form

val f_proj_simpl : form -> int -> EcTypes.ty -> form
val f_if_simpl   : form -> form -> form -> form
val f_let_simpl  : EcTypes.lpattern -> form -> form -> form
val f_lets_simpl : (EcTypes.lpattern * form) list -> form -> form

val f_forall_simpl : bindings -> form -> form
val f_exists_simpl : bindings -> form -> form
val f_quant_simpl  : quantif -> bindings -> form -> form
val f_app_simpl    : form -> form list -> EcTypes.ty -> form

val f_not_simpl   : form -> form
val f_and_simpl   : form -> form -> form
val f_ands_simpl  : form list -> form -> form
val f_ands0_simpl : form list -> form
val f_anda_simpl  : form -> form -> form
val f_or_simpl    : form -> form -> form
val f_ora_simpl   : form -> form -> form
val f_imp_simpl   : form -> form -> form
val f_imps        : form list -> form -> form
val f_imps_simpl  : form list -> form -> form
val f_iff_simpl   : form -> form -> form
val f_eq_simpl    : form -> form -> form

val f_int_le_simpl  : form -> form -> form
val f_int_lt_simpl  : form -> form -> form

val f_real_le_simpl : form -> form -> form
val f_real_lt_simpl : form -> form -> form

val f_int_add_simpl   : form -> form -> form
val f_int_opp_simpl   : form -> form
val f_int_sub_simpl   : form -> form -> form
val f_int_mul_simpl   : form -> form -> form
val f_int_edivz_simpl : form -> form -> form

val f_real_add_simpl : form -> form -> form
val f_real_opp_simpl : form -> form
val f_real_sub_simpl : form -> form -> form
val f_real_mul_simpl : form -> form -> form
val f_real_div_simpl : form -> form -> form
val f_real_inv_simpl : form -> form

(* -------------------------------------------------------------------- *)
val destr_exists_prenex : ?bound:int -> form -> bindings * form
val destr_ands : deep:bool -> form -> form list

(* -------------------------------------------------------------------- *)
(* projects 'a Distr type into 'a *)
val proj_distr_ty : EcEnv.env -> ty -> ty

(* -------------------------------------------------------------------- *)
type op_kind = [
  | `True
  | `False
  | `Not
  | `And   of [`Asym | `Sym]
  | `Or    of [`Asym | `Sym]
  | `Imp
  | `Iff
  | `Eq
  | `Int_le
  | `Int_lt
  | `Real_le
  | `Real_lt
  | `Int_add
  | `Int_mul
  | `Int_pow
  | `Int_opp
  | `Int_edivz
  | `Real_add
  | `Real_opp
  | `Real_mul
  | `Real_inv
  | `Map_get
  | `Map_set
  | `Map_cst
]

val op_kind       : path -> op_kind option
val is_logical_op : path -> bool

(* -------------------------------------------------------------------- *)
(* Structured formulas - allows to get more information on the top-level
 * structure of a formula via direct pattern matching *)

type sform =
  | SFint   of zint
  | SFlocal of EcIdent.t
  | SFpvar  of EcTypes.prog_var * memory
  | SFglob  of EcIdent.t * memory

  | SFif    of form * form * form
  | SFmatch of form * form list * ty
  | 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 [`Asym | `Sym] * (form * form)
  | SFor    of [`Asym | `Sym] * (form * form)
  | SFimp   of form * form
  | SFiff   of form * form
  | SFeq    of form * form
  | SFop    of (path * ty list) * (form list)

  | SFhoareF  of sHoareF
  | SFhoareS  of sHoareS
  | SFbdHoareF of bdHoareF
  | SFbdHoareS of bdHoareS
  | SFequivF   of equivF
  | SFequivS   of equivS
  | SFpr       of pr

  | SFother of form

val sform_of_form : form -> sform

(* -------------------------------------------------------------------- *)
module type DestrRing = sig
  val le  : form -> form * form
  val lt  : form -> form * form
  val add : form -> form * form
  val opp : form -> form
  val sub : form -> form * form
  val mul : form -> form * form
end

module DestrInt : DestrRing

module DestrReal : sig
  include DestrRing

  val inv : form -> form
  val div : form -> form * form
  val abs : form -> form
end

(* -------------------------------------------------------------------- *)
val dump_f : form -> string