https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecFol.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcBigInt
open EcPath
open EcTypes
open EcModules
open EcMemory
(* -------------------------------------------------------------------- *)
include module type of struct include EcCoreFol end
(* -------------------------------------------------------------------- *)
val f_losslessF: xpath -> form
val f_eqparams:
xpath -> EcTypes.ty -> variable list option -> memory
-> xpath -> EcTypes.ty -> variable list option -> memory
-> form
val f_eqres:
xpath -> EcTypes.ty -> memory
-> xpath -> EcTypes.ty -> memory
-> form
val f_eqglob:
mpath -> memory
-> mpath -> memory
-> form
(* 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
(* 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
(* common functions *)
val f_identity : ?name:EcSymbols.symbol -> EcTypes.ty -> form
(* -------------------------------------------------------------------- *)
(* "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 instanciated *)
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_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 : form -> bindings * form
(* -------------------------------------------------------------------- *)
(* 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
]
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 mpath * 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 hoareF
| SFhoareS of hoareS
| 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