https://github.com/EasyCrypt/easycrypt
Revision 9f6a2f9c698e6c47fa841a0b040bc45d82a601c5 authored by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC, committed by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC
1 parent 776af38
Tip revision: 9f6a2f9c698e6c47fa841a0b040bc45d82a601c5 authored by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC
add make
add make
Tip revision: 9f6a2f9
ecFol.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcBigInt
open EcPath
open EcTypes
open EcModules
(* -------------------------------------------------------------------- *)
include module type of struct include EcCoreFol end
(* -------------------------------------------------------------------- *)
val f_losslessF: xpath -> form
val f_eqparams:
xpath -> EcTypes.ty -> variable list option -> form
-> xpath -> EcTypes.ty -> variable list option -> form
-> form
val f_eqres:
xpath -> EcTypes.ty -> form
-> xpath -> EcTypes.ty -> form
-> form
val f_eqglob:
mpath -> form
-> mpath -> form
-> 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_div : form -> form -> form
val f_real_abs : form -> form
(* soft constructors - distributions *)
val fop_in_supp : EcTypes.ty -> form
val fop_mu_x : EcTypes.ty -> 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 : ty -> form -> form
val f_real_of_bool : form -> form
val f_muf_ty : ty -> form -> form -> form
val f_muf : EcEnv.env -> form -> form -> form
val f_integr : EcEnv.env -> form -> EcIdent.t -> form
val f_muf_b2r : EcIdent.t * ty -> form -> EcIdent.t -> form
val f_square : EcIdent.t * ty -> form -> EcIdent.t -> form
val f_mulossless : EcEnv.env -> form -> form
(* common functions *)
val f_identity : ?name:EcSymbols.symbol -> EcTypes.ty -> 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_pred2forall : EcEnv.env -> 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_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 destr_exists_prenex : form -> bindings * form
(* -------------------------------------------------------------------- *)
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
| `Real_add
| `Real_opp
| `Real_mul
| `Real_div
]
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 * form
| SFglob of mpath * form
| 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
(* ---------------------------------------------------------------------- *)
val get_lambda1 : EcEnv.env -> form -> EcIdent.t * ty * form
val open_mu_binding : EcEnv.env -> form -> (EcIdent.t * memtype) * form
val close_mu_binding : EcIdent.t * memtype -> form -> form
val is_muf_b2r_not : EcEnv.env -> form -> bool
val destr_muf_b2r_not : EcEnv.env -> form -> form * form
(* -------------------------------------------------------------------- *)
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
Computing file changes ...