diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 15 | ||||
| -rw-r--r-- | plugins/nsatz/ideal.ml | 143 | ||||
| -rw-r--r-- | plugins/nsatz/ideal.mli | 47 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.mli | 9 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 4 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 5 |
6 files changed, 105 insertions, 118 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 312c2eab3d..a980a43f53 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -371,8 +371,7 @@ and extract_really_ind env kn mib = let packets = Array.mapi (fun i mip -> - let (ind,u), ctx = - Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in @@ -591,10 +590,10 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const (kn,u) -> - extract_cst_app env mle mlt kn u args - | Construct (cp,u) -> - extract_cons_app env mle mlt cp u args + | Const (kn,_) -> + extract_cst_app env mle mlt kn args + | Construct (cp,_) -> + extract_cons_app env mle mlt cp args | Proj (p, c) -> let term = Retyping.expand_projection env (Evd.from_env env) p c [] in extract_term env mle mlt term args @@ -645,7 +644,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn u args = +and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -718,7 +717,7 @@ and extract_cst_app env mle mlt kn u args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 482ce50538..48bdad8264 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -19,75 +19,6 @@ open Utile exception NotInIdeal -module type S = sig - -(* Monomials *) -type mon = int array - -val mult_mon : mon -> mon -> mon -val deg : mon -> int -val compare_mon : mon -> mon -> int -val div_mon : mon -> mon -> mon -val div_mon_test : mon -> mon -> bool -val ppcm_mon : mon -> mon -> mon - -(* Polynomials *) - -type deg = int -type coef -type poly -type polynom - -val repr : poly -> (coef * mon) list -val polconst : coef -> poly -val zeroP : poly -val gen : int -> poly - -val equal : poly -> poly -> bool -val name_var : string list ref -val getvar : string list -> int -> string -val lstringP : poly list -> string -val printP : poly -> unit -val lprintP : poly list -> unit - -val div_pol_coef : poly -> coef -> poly -val plusP : poly -> poly -> poly -val mult_t_pol : coef -> mon -> poly -> poly -val selectdiv : mon -> poly list -> poly -val oppP : poly -> poly -val emultP : coef -> poly -> poly -val multP : poly -> poly -> poly -val puisP : poly -> int -> poly -val contentP : poly -> coef -val contentPlist : poly list -> coef -val pgcdpos : coef -> coef -> coef -val div_pol : poly -> poly -> coef -> coef -> mon -> poly -val reduce2 : poly -> poly list -> coef * poly - -val poldepcontent : coef list ref -val coefpoldep_find : poly -> poly -> poly -val coefpoldep_set : poly -> poly -> poly -> unit -val initcoefpoldep : poly list -> unit -val reduce2_trace : poly -> poly list -> poly list -> poly list * poly -val spol : poly -> poly -> poly -val etrangers : poly -> poly -> bool -val div_ppcm : poly -> poly -> poly -> bool - -val genPcPf : poly -> poly list -> poly list -> poly list -val genOCPf : poly list -> poly list - -val is_homogeneous : poly -> bool - -type certificate = - { coef : coef; power : int; - gb_comb : poly list list; last_comb : poly list } - -val test_dans_ideal : poly -> poly list -> poly list -> - poly list * poly * certificate -val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate - -end - (*********************************************************************** Global options *) @@ -127,11 +58,11 @@ type polynom = num : int; sugar : int} -let nvar m = Array.length m - 1 +let nvar (m : mon) = Array.length m - 1 -let deg m = m.(0) +let deg (m : mon) = m.(0) -let mult_mon m m' = +let mult_mon (m : mon) (m' : mon) = let d = nvar m in let m'' = Array.make (d+1) 0 in for i=0 to d do @@ -140,7 +71,7 @@ let mult_mon m m' = m'' -let compare_mon m m' = +let compare_mon (m : mon) (m' : mon) = let d = nvar m in if !lexico then ( @@ -148,18 +79,18 @@ let compare_mon m m' = let res=ref 0 in let i=ref 1 in (* 1 si lexico pur 0 si degre*) while (!res=0) && (!i<=d) do - res:= (compare m.(!i) m'.(!i)); + res:= (Int.compare m.(!i) m'.(!i)); i:=!i+1; done; !res) else ( (* degre lexicographique inverse *) - match compare m.(0) m'.(0) with + match Int.compare m.(0) m'.(0) with | 0 -> (* meme degre total *) let res=ref 0 in let i=ref d in while (!res=0) && (!i>=1) do - res:= - (compare m.(!i) m'.(!i)); + res:= - (Int.compare m.(!i) m'.(!i)); i:=!i-1; done; !res @@ -402,29 +333,25 @@ let polconst d c = [(c,m)] let plusP p q = - let rec plusP p q = - match p with - [] -> q - |t::p' -> - match q with - [] -> p - |t'::q' -> - match compare_mon (snd t) (snd t') with - 1 -> t::(plusP p' q) - |(-1) -> t'::(plusP p q') - |_ -> let c=P.plusP (fst t) (fst t') in - match P.equal c coef0 with - true -> (plusP p' q') - |false -> (c,(snd t))::(plusP p' q') - in plusP p q + let rec plusP p q accu = match p, q with + | [], [] -> List.rev accu + | [], _ -> List.rev_append accu q + | _, [] -> List.rev_append accu p + | t :: p', t' :: q' -> + let c = compare_mon (snd t) (snd t') in + if c > 0 then plusP p' q (t :: accu) + else if c < 0 then plusP p q' (t' :: accu) + else + let c = P.plusP (fst t) (fst t') in + if P.equal c coef0 then plusP p' q' accu + else plusP p' q' ((c, (snd t)) :: accu) + in + plusP p q [] (* multiplication by (a,monomial) *) let mult_t_pol a m p = - let rec mult_t_pol p = - match p with - [] -> [] - |(b,m')::p -> ((P.multP a b),(mult_mon m m'))::(mult_t_pol p) - in mult_t_pol p + let map (b, m') = (P.multP a b, mult_mon m m') in + CList.map map p let coef_of_int x = P.of_num (Num.Int x) @@ -451,23 +378,27 @@ let emultP a p = in emultP p let multP p q = - let rec aux p = + let rec aux p accu = match p with - [] -> [] - |(a,m)::p' -> plusP (mult_t_pol a m q) (aux p') - in aux p + [] -> accu + |(a,m)::p' -> aux p' (plusP (mult_t_pol a m q) accu) + in aux p [] let puisP p n= match p with [] -> [] |_ -> + if n = 0 then let d = nvar (snd (List.hd p)) in - let rec puisP n = - match n with - 0 -> [coef1, Array.make (d+1) 0] - | 1 -> p - |_ -> multP p (puisP (n-1)) - in puisP n + [coef1, Array.make (d+1) 0] + else + let rec puisP p n = + if n = 1 then p + else + let q = puisP p (n / 2) in + let q = multP q q in + if n mod 2 = 0 then q else multP p q + in puisP p n let rec contentP p = match p with diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli new file mode 100644 index 0000000000..d1a2a0a7d1 --- /dev/null +++ b/plugins/nsatz/ideal.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +module Make (P : Polynom.S) : +sig +(* Polynomials *) + +type deg = int +type coef = P.t +type poly + +val repr : poly -> (coef * int array) list +val polconst : int -> coef -> poly +val zeroP : poly +val gen : int -> int -> poly + +val equal : poly -> poly -> bool +val name_var : string list ref + +val plusP : poly -> poly -> poly +val oppP : poly -> poly +val multP : poly -> poly -> poly +val puisP : poly -> int -> poly + +val poldepcontent : coef list ref + +type certificate = + { coef : coef; power : int; + gb_comb : poly list list; last_comb : poly list } + +val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate + +module Hashpol : Hashtbl.S with type key = poly + +val sugar_flag : bool ref +val divide_rem_with_critical_pair : bool ref + +end + +exception NotInIdeal + +val lexico : bool ref diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli new file mode 100644 index 0000000000..e876ccfa5d --- /dev/null +++ b/plugins/nsatz/nsatz.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val nsatz_compute : Constr.t -> unit Proofview.tactic diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 96885d2f7a..20022c00ec 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -18,7 +18,6 @@ Require Import BinInt. Require Import Setoid. Require Export Ncring. Require Export Ncring_polynom. -Import List. Set Implicit Arguments. @@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Notation "[ x ]" := (gen_phiZ x). + Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Local Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 7fcd6c08a7..f7757a18da 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -238,7 +238,6 @@ Section ALMOST_RING. Variable req : R -> R -> Prop. Notation "0" := rO. Notation "1" := rI. Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. - Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Equivalence (@eq R). @@ -263,7 +262,7 @@ Section ALMOST_RING. -x = x and x - y = x + y *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). - Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + Definition SRsub x y := x + -y. Infix "-" := SRsub. Lemma SRopp_ext : forall x y, x == y -> -x == -y. Proof. intros x y H; exact H. Qed. @@ -320,6 +319,8 @@ Section ALMOST_RING. Qed. End SEMI_RING. + Infix "-" := rsub. + Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. |