Revision 4388214acf75d0162f5a29c2c42230f44f6c8187 authored by Pierre-Yves Strub on 12 December 2015, 19:59:46 UTC, committed by Pierre-Yves Strub on 12 December 2015, 20:03:33 UTC
Syntax is `[~*]`. The full syntax of this i-p is now: `move=> [int?~?/?*]`
1 parent c09a98a
ecRing.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcBigInt
open EcMaps
(* -------------------------------------------------------------------- *)
type pexpr =
| PEc of zint
| PEX of int
| PEadd of pexpr * pexpr
| PEsub of pexpr * pexpr
| PEmul of pexpr * pexpr
| PEopp of pexpr
| PEpow of pexpr * zint
val pexpr_eq : pexpr -> pexpr -> bool
val pp_pe : Format.formatter -> pexpr -> unit
val fv_pe : pexpr -> Sint.t
(* -------------------------------------------------------------------- *)
type 'a cmp_sub = [`Eq | `Lt | `Gt of 'a]
(* -------------------------------------------------------------------- *)
exception Overflow
(* -------------------------------------------------------------------- *)
module type Coef = sig
(* ------------------------------------------------------------------ *)
type c
val cofint : zint -> c
val ctoint : c -> zint
val c0 : c
val c1 : c
val cadd : c -> c -> c
val csub : c -> c -> c
val cmul : c -> c -> c
val copp : c -> c
val ceq : c -> c -> bool
val cdiv : c -> c -> c * c
(* ------------------------------------------------------------------ *)
type p
val pofint : zint -> p
val ptoint : p -> zint
val padd : p -> p -> p
val peq : p -> p -> bool
val pcmp : p -> p -> int
val pcmp_sub : p -> p -> p cmp_sub
end
(* -------------------------------------------------------------------- *)
module Cint : Coef
module Cbool : Coef
module type ModVal = sig
val c : zint option
val p : zint option
end
module Cmod(M : ModVal) : Coef
(* -------------------------------------------------------------------- *)
module type Rnorm = sig
module C : Coef
val norm_pe : pexpr -> (pexpr * pexpr) list -> pexpr
end
module Iring : Rnorm
module Bring : Rnorm
module Make(C : Coef) : Rnorm
(* -------------------------------------------------------------------- *)
type c = zint
val c0 : c
val c1 : c
val cadd : c -> c -> c
val csub : c -> c -> c
val cmul : c -> c -> c
val copp : c -> c
val ceq : c -> c -> bool
val cdiv : c -> c -> c*c
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...