summaryrefslogtreecommitdiff
path: root/plugins/nsatz/nsatz.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/nsatz/nsatz.ml4')
-rw-r--r--plugins/nsatz/nsatz.ml488
1 files changed, 48 insertions, 40 deletions
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index da0ee898..e48643b4 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -16,7 +16,7 @@ open Closure
open Environ
open Libnames
open Tactics
-open Rawterm
+open Glob_term
open Tacticals
open Tacexpr
open Pcoq
@@ -180,21 +180,24 @@ let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul")
let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp")
let ttpow = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEpow")
-let tlist = lazy (gen_constant "CC" ["Lists";"List"] "list")
-let lnil = lazy (gen_constant "CC" ["Lists";"List"] "nil")
-let lcons = lazy (gen_constant "CC" ["Lists";"List"] "cons")
+let datatypes = ["Init";"Datatypes"]
+let binnums = ["Numbers";"BinNums"]
-let tz = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z")
-let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0")
-let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos")
-let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg")
+let tlist = lazy (gen_constant "CC" datatypes "list")
+let lnil = lazy (gen_constant "CC" datatypes "nil")
+let lcons = lazy (gen_constant "CC" datatypes "cons")
-let pxI = lazy(gen_constant "CC" ["NArith";"BinPos"] "xI")
-let pxO = lazy(gen_constant "CC" ["NArith";"BinPos"] "xO")
-let pxH = lazy(gen_constant "CC" ["NArith";"BinPos"] "xH")
+let tz = lazy (gen_constant "CC" binnums "Z")
+let z0 = lazy (gen_constant "CC" binnums "Z0")
+let zpos = lazy (gen_constant "CC" binnums "Zpos")
+let zneg = lazy(gen_constant "CC" binnums "Zneg")
-let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0")
-let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos")
+let pxI = lazy(gen_constant "CC" binnums "xI")
+let pxO = lazy(gen_constant "CC" binnums "xO")
+let pxH = lazy(gen_constant "CC" binnums "xH")
+
+let nN0 = lazy (gen_constant "CC" binnums "N0")
+let nNpos = lazy(gen_constant "CC" binnums "Npos")
let mkt_app name l = mkApp (Lazy.force name, Array.of_list l)
@@ -237,14 +240,14 @@ else
let rec parse_pos p =
match kind_of_term p with
| App (a,[|p2|]) ->
- if a = Lazy.force pxO then num_2 */ (parse_pos p2)
+ if eq_constr a (Lazy.force pxO) then num_2 */ (parse_pos p2)
else num_1 +/ (num_2 */ (parse_pos p2))
| _ -> num_1
let parse_z z =
match kind_of_term z with
| App (a,[|p2|]) ->
- if a = Lazy.force zpos then parse_pos p2 else (num_0 -/ (parse_pos p2))
+ if eq_constr a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2))
| _ -> num_0
let parse_n z =
@@ -256,15 +259,15 @@ let parse_n z =
let rec parse_term p =
match kind_of_term p with
| App (a,[|_;p2|]) ->
- if a = Lazy.force ttvar then Var (string_of_num (parse_pos p2))
- else if a = Lazy.force ttconst then Const (parse_z p2)
- else if a = Lazy.force ttopp then Opp (parse_term p2)
+ if eq_constr a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2))
+ else if eq_constr a (Lazy.force ttconst) then Const (parse_z p2)
+ else if eq_constr a (Lazy.force ttopp) then Opp (parse_term p2)
else Zero
| App (a,[|_;p2;p3|]) ->
- if a = Lazy.force ttadd then Add (parse_term p2, parse_term p3)
- else if a = Lazy.force ttsub then Sub (parse_term p2, parse_term p3)
- else if a = Lazy.force ttmul then Mul (parse_term p2, parse_term p3)
- else if a = Lazy.force ttpow then
+ if eq_constr a (Lazy.force ttadd) then Add (parse_term p2, parse_term p3)
+ else if eq_constr a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3)
+ else if eq_constr a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3)
+ else if eq_constr a (Lazy.force ttpow) then
Pow (parse_term p2, int_of_num (parse_n p3))
else Zero
| _ -> Zero
@@ -323,6 +326,8 @@ open PIdeal
let term_pol_sparse np t=
let d = !nvars in
let rec aux t =
+(* info ("conversion de: "^(string_of_term t)^"\n");*)
+ let res =
match t with
| Zero -> zeroP
| Const r ->
@@ -339,9 +344,11 @@ let term_pol_sparse np t=
| Sub (t1,t2) -> plusP (aux t1) (oppP (aux t2))
| Mul (t1,t2) -> multP (aux t1) (aux t2)
| Pow (t1,n) -> puisP (aux t1) n
- in (*info ("conversion de: "^(string_of_term t)^"\n");*)
+ in
+(* info ("donne: "^(stringP res)^"\n");*)
+ res
+ in
let res= aux t in
- (*info ("donne: "^(stringP res)^"\n");*)
res
(* sparse polynomial to term *)
@@ -364,7 +371,7 @@ let polrec_to_term p =
(* approximation of the Horner form used in the tactic ring *)
let pol_sparse_to_term n2 p =
- info "pol_sparse_to_term ->\n";
+ (* info "pol_sparse_to_term ->\n";*)
let p = PIdeal.repr p in
let rec aux p =
match p with
@@ -408,7 +415,7 @@ let pol_sparse_to_term n2 p =
then Var (string_of_int (i0))
else pow (Var (string_of_int (i0)),e0) in
add(mul(vm, aux (List.rev (!p1))), aux (List.rev (!p2))))
- in info "-> pol_sparse_to_term\n";
+ in (*info "-> pol_sparse_to_term\n";*)
aux p
@@ -467,7 +474,7 @@ let remove_zeros zero lci =
done;
!lcr)
lr in
- info ("useless spolynomials: "
+ info ("unuseful spolynomials: "
^string_of_int (m-List.length lr)^"\n");
info ("useful spolynomials: "
^string_of_int (List.length lr)^"\n");
@@ -489,35 +496,35 @@ let theoremedeszeros_termes lp =
match lp with
| Const (Int sugarparam)::Const (Int nparam)::lp ->
((match sugarparam with
- |0 -> info "calcul sans sugar\n";
+ |0 -> info "computation without sugar\n";
lexico:=false;
sugar_flag := false;
divide_rem_with_critical_pair := false
- |1 -> info "calcul avec sugar\n";
+ |1 -> info "computation with sugar\n";
lexico:=false;
sugar_flag := true;
divide_rem_with_critical_pair := false
- |2 -> info "ordre lexico calcul sans sugar\n";
+ |2 -> info "ordre lexico computation without sugar\n";
lexico:=true;
sugar_flag := false;
divide_rem_with_critical_pair := false
- |3 -> info "ordre lexico calcul avec sugar\n";
+ |3 -> info "ordre lexico computation with sugar\n";
lexico:=true;
sugar_flag := true;
divide_rem_with_critical_pair := false
- |4 -> info "calcul sans sugar, division par les paires\n";
+ |4 -> info "computation without sugar, division by pairs\n";
lexico:=false;
sugar_flag := false;
divide_rem_with_critical_pair := true
- |5 -> info "calcul avec sugar, division par les paires\n";
+ |5 -> info "computation with sugar, division by pairs\n";
lexico:=false;
sugar_flag := true;
divide_rem_with_critical_pair := true
- |6 -> info "ordre lexico calcul sans sugar, division par les paires\n";
+ |6 -> info "ordre lexico computation without sugar, division by pairs\n";
lexico:=true;
sugar_flag := false;
divide_rem_with_critical_pair := true
- |7 -> info "ordre lexico calcul avec sugar, division par les paires\n";
+ |7 -> info "ordre lexico computation with sugar, division by pairs\n";
lexico:=true;
sugar_flag := true;
divide_rem_with_critical_pair := true
@@ -534,6 +541,7 @@ let theoremedeszeros_termes lp =
| p::lp1 ->
let lpol = List.rev lp1 in
let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
+ info "cert ok\n";
let lc = cert.last_comb::List.rev cert.gb_comb in
match remove_zeros (fun x -> x=zeroP) lc with
| [] -> assert false
@@ -545,8 +553,8 @@ let theoremedeszeros_termes lp =
let lci = List.rev lci in
let lci = List.map (List.map (pol_sparse_to_term m)) lci in
let lq = List.map (pol_sparse_to_term m) lq in
- info ("nombre de parametres: "^string_of_int nparam^"\n");
- info "terme calcule\n";
+ info ("number of parametres: "^string_of_int nparam^"\n");
+ info "term computed\n";
(c,r,lci,lq)
)
|_ -> assert false
@@ -565,7 +573,7 @@ let nsatz lpol =
let certif = hash_certif certif in
let certif = certif_term certif in
let c = mkt_term c in
- info "constr calcule\n";
+ info "constr computed\n";
(c, certif)
*)
@@ -586,7 +594,7 @@ let nsatz lpol =
mkt_app lcons [tlp ();ltterm;r])
res
(mkt_app lnil [tlp ()]) in
- info "terme calcule\n";
+ info "term computed\n";
res
let return_term t =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 12:27:32 +0000