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
ecAlgebra.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 EcUtils
open EcFol
open EcRing
open EcField
open EcDecl
open EcEnv
module RState : sig
type rstate
val empty : rstate
val add : LDecl.hyps -> form -> rstate -> int * rstate
val get : int -> rstate -> form option
val update : rstate -> int list -> form list -> rstate
end
(* -------------------------------------------------------------------- *)
val rapp : ring -> EcPath.path -> form list -> form
val rzero : ring -> form
val rone : ring -> form
val radd : ring -> form -> form -> form
val ropp : ring -> form -> form
val rmul : ring -> form -> form -> form
val rexp : ring -> form -> EcRing.c -> form
val rsub : ring -> form -> form -> form
val rofint : ring -> EcRing.c -> form
(* -------------------------------------------------------------------- *)
val fzero : field -> form
val fone : field -> form
val fadd : field -> form -> form -> form
val fopp : field -> form -> form
val fmul : field -> form -> form -> form
val fexp : field -> form -> EcRing.c -> form
val fsub : field -> form -> form -> form
val finv : field -> form -> form
val fdiv : field -> form -> form -> form
val fofint : field -> EcRing.c -> form
(* -------------------------------------------------------------------- *)
val emb_rzero : ring -> form
val emb_fzero : field -> form
val emb_rone : ring -> form
val emb_fone : field -> form
(* -------------------------------------------------------------------- *)
type eq = form * form
(* -------------------------------------------------------------------- *)
type cring
type cfield
val cring_of_ring : ring -> cring
val cfield_of_field : field -> cfield
val ring_of_cring : cring -> ring
val field_of_cfield : cfield-> field
(* -------------------------------------------------------------------- *)
val toring:
LDecl.hyps
-> cring (* ring structure *)
-> RState.rstate (* reification state *)
-> form (* formula to reify *)
-> pexpr * RState.rstate (* (reification, mutated state) *)
val ofring:
ring (* ring structure *)
-> RState.rstate (* reification state *)
-> pexpr -> form
val ring_simplify_pe:
cring (* ring structure *)
-> pexpr pair list (* hypotheses (equations) *)
-> pexpr (* expression to simplify *)
-> pexpr (* simplified formula *)
val ring_simplify:
LDecl.hyps
-> cring (* ring structure *)
-> eq list (* hypotheses (equations) *)
-> form (* formula to simplify *)
-> form (* simplified formula *)
val ring_eq:
LDecl.hyps
-> cring (* ring structure *)
-> eq list (* hypotheses (equations) *)
-> form (* LHS *)
-> form (* RHS *)
-> form
(* -------------------------------------------------------------------- *)
val tofield:
EcEnv.LDecl.hyps
-> cfield (* field structure *)
-> RState.rstate (* reification state *)
-> form (* formula to reify *)
-> fexpr * RState.rstate (* (reification, mutated state) *)
val offield:
field (* field structure *)
-> RState.rstate (* reification state *)
-> fexpr -> form
val field_simplify_pe:
cfield (* field structure *)
-> pexpr pair list (* hypotheses (equations) *)
-> fexpr (* formula to simplify *)
-> pexpr list * pexpr pair (* (!=0 conditions, (num, den)) *)
val field_simplify:
LDecl.hyps
-> cfield (* field structure *)
-> eq list (* hypotheses (equations) *)
-> form (* formula to simplify *)
-> form list * form pair (* (!=0 conditions, (num, den)) *)
val field_eq:
LDecl.hyps
-> cfield (* field structure *)
-> eq list (* hypotheses (equations) *)
-> form (* LHS *)
-> form (* RHS *)
-> form list * form pair pair (* (!=0 conditions, (num, den) pair) *)