(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

(* ML part of the Ring tactic *)

open Pp;;
open Util;;
open Term;;
open Names;;
open Reduction;;
open Tacmach;;
open Proof_type;;
open Proof_trees;;
open Printer;;
open Equality;;
open Vernacinterp;;
open Libobject;;
open Closure;;
open Tacred;;
open Tactics;;
open Pattern ;;
open Hiddentac;;
open Quote;;

let mt_evd = Evd.empty
let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com

let constant dir s =
  let dir = "Coq"::"ring"::dir in
  let id = id_of_string s in
  try 
    Declare.global_reference_in_absolute_module dir id
  with Not_found ->
    anomaly ("Ring: cannot find "^
	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))

(* Ring_theory *)

let coq_Ring_Theory = lazy (constant ["Ring_theory"] "Ring_Theory")
let coq_Semi_Ring_Theory = lazy (constant ["Ring_theory"] "Semi_Ring_Theory")

(* Ring_normalize *)
let coq_SPplus = lazy (constant ["Ring_normalize"] "SPplus")
let coq_SPmult = lazy (constant ["Ring_normalize"] "SPmult")
let coq_SPvar = lazy (constant ["Ring_normalize"] "SPvar")
let coq_SPconst = lazy (constant ["Ring_normalize"] "SPconst")
let coq_Pplus = lazy (constant ["Ring_normalize"] "Pplus")
let coq_Pmult = lazy (constant ["Ring_normalize"] "Pmult")
let coq_Pvar = lazy (constant ["Ring_normalize"] "Pvar")
let coq_Pconst = lazy (constant ["Ring_normalize"] "Pconst")
let coq_Popp = lazy (constant ["Ring_normalize"] "Popp")
let coq_interp_sp = lazy (constant ["Ring_normalize"] "interp_sp")
let coq_interp_p = lazy (constant ["Ring_normalize"] "interp_p")
let coq_interp_cs = lazy (constant ["Ring_normalize"] "interp_cs")
let coq_spolynomial_simplify = 
  lazy (constant ["Ring_normalize"] "spolynomial_simplify")
let coq_polynomial_simplify = 
  lazy (constant ["Ring_normalize"] "polynomial_simplify")
let coq_spolynomial_simplify_ok = 
  lazy (constant ["Ring_normalize"] "spolynomial_simplify_ok")
let coq_polynomial_simplify_ok = 
  lazy (constant ["Ring_normalize"] "polynomial_simplify_ok")

(* Ring_abstract *)
let coq_ASPplus = lazy (constant ["Ring_abstract"] "ASPplus")
let coq_ASPmult = lazy (constant ["Ring_abstract"] "ASPmult")
let coq_ASPvar = lazy (constant ["Ring_abstract"] "ASPvar")
let coq_ASP0 = lazy (constant ["Ring_abstract"] "ASP0")
let coq_ASP1 = lazy (constant ["Ring_abstract"] "ASP1")
let coq_APplus = lazy (constant ["Ring_abstract"] "APplus")
let coq_APmult = lazy (constant ["Ring_abstract"] "APmult")
let coq_APvar = lazy (constant ["Ring_abstract"] "APvar")
let coq_AP0 = lazy (constant ["Ring_abstract"] "AP0")
let coq_AP1 = lazy (constant ["Ring_abstract"] "AP1")
let coq_APopp = lazy (constant ["Ring_abstract"] "APopp")
let coq_interp_asp = 
  lazy (constant ["Ring_abstract"] "interp_asp")
let coq_interp_ap = 
  lazy (constant ["Ring_abstract"] "interp_ap")
 let coq_interp_acs = 
  lazy (constant ["Ring_abstract"] "interp_acs")
let coq_interp_sacs = 
  lazy (constant ["Ring_abstract"] "interp_sacs")
let coq_aspolynomial_normalize = 
  lazy (constant ["Ring_abstract"] "aspolynomial_normalize")
let coq_apolynomial_normalize = 
  lazy (constant ["Ring_abstract"] "apolynomial_normalize")
let coq_aspolynomial_normalize_ok = 
  lazy (constant ["Ring_abstract"] "aspolynomial_normalize_ok")
let coq_apolynomial_normalize_ok = 
  lazy (constant ["Ring_abstract"] "apolynomial_normalize_ok")

(* Logic --> to be found in Coqlib *)
open Coqlib
(*
val build_coq_f_equal2 : constr delayed
val build_coq_eqT : constr delayed
val build_coq_sym_eqT : constr delayed
*)


(*********** Useful types and functions ************)

module OperSet = 
  Set.Make (struct 
	      type t = global_reference
	      let compare = (Pervasives.compare : t->t->int)
	    end)	

type theory =
    { th_ring : bool;                  (* false for a semi-ring *)
      th_abstract : bool;
      th_a : constr;                   (* e.g. nat *)
      th_plus : constr;
      th_mult : constr;
      th_one : constr;
      th_zero : constr;
      th_opp : constr;                 (* Not used if semi-ring *)
      th_eq : constr;
      th_t : constr;                   (* e.g. NatTheory *)
      th_closed : ConstrSet.t;         (* e.g. [S; O] *)
                                       (* Must be empty for an abstract ring *)
    }

(* Theories are stored in a table which is synchronised with the Reset 
   mechanism. *)

module Cmap = Map.Make(struct type t = constr let compare = compare end)

let theories_map = ref Cmap.empty

let theories_map_add (c,t) = theories_map := Cmap.add c t !theories_map
let theories_map_find c = Cmap.find c !theories_map
let theories_map_mem c = Cmap.mem c !theories_map

let _ = 
  Summary.declare_summary "tactic-ring-table"
    { Summary.freeze_function = (fun () -> !theories_map);
      Summary.unfreeze_function = (fun t -> theories_map := t);
      Summary.init_function = (fun () -> theories_map := Cmap.empty);
      Summary.survive_section = false }

(* declare a new type of object in the environment, "tactic-ring-theory"
   The functions theory_to_obj and obj_to_theory do the conversions
   between theories and environement objects. *)

let (theory_to_obj, obj_to_theory) = 
  let cache_th (_,(c, th)) = theories_map_add (c,th)
  and export_th x = Some x in
  declare_object ("tactic-ring-theory",
		  { load_function = (fun _ -> ());
		    open_function = cache_th;
                    cache_function = cache_th;
		    export_function = export_th })

(* from the set A, guess the associated theory *)
(* With this simple solution, the theory to use is automatically guessed *)
(* But only one theory can be declared for a given Set *)

let guess_theory a =
  try 
    theories_map_find a
  with Not_found -> 
    errorlabstrm "Ring" 
      [< 'sTR "No Declared Ring Theory for ";
	 prterm a; 'fNL;
	 'sTR "Use Add [Semi] Ring to declare it">]

(* Add a Ring or a Semi-Ring to the database after a type verification *)

let add_theory want_ring want_abstract a aplus amult aone azero aopp aeq t cset = 
  if theories_map_mem a then errorlabstrm "Add Semi Ring" 
    [< 'sTR "A (Semi-)Ring Structure is already declared for "; prterm a >];
  let env = Global.env () in
  if (want_ring & 
      not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
	     (mkApp (Lazy.force coq_Ring_Theory, [| a; aplus; amult;
			aone; azero; aopp; aeq |])))) then
    errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
  if (not want_ring &
      not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
	     (mkApp (Lazy.force coq_Semi_Ring_Theory, [| a; 
			aplus; amult; aone; azero; aeq |])))) then 
    errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
  Lib.add_anonymous_leaf
    (theory_to_obj 
       (a, { th_ring = want_ring;
	     th_abstract = want_abstract;
	     th_a = a;
	     th_plus = aplus;
	     th_mult = amult;
	     th_one = aone;
	     th_zero = azero;
	     th_opp = aopp;
	     th_eq = aeq;
	     th_t = t;
	     th_closed = cset }))

(* The vernac commands "Add Ring" and "Add Semi Ring" *)
(* see file Ring.v for examples of this command *)

let constr_of_comarg = function 
  | VARG_CONSTR c -> constr_of c
  | _ -> anomaly "Add (Semi) Ring"
  
let cset_of_comarg_list l = 
  List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty

let _ = 
  vinterp_add "AddSemiRing"
    (function
       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq)
	 ::(VARG_CONSTR t)::l -> 
	   (fun () -> (add_theory false false
			 (constr_of a)
			 (constr_of aplus)
			 (constr_of amult)
			 (constr_of aone)
			 (constr_of azero)
			 mkImplicit
			 (constr_of aeq)
			 (constr_of t)
			 (cset_of_comarg_list l)))
       | _ -> anomaly "AddSemiRing")

let _ = 
  vinterp_add "AddRing"
    (function 
       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
	 ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> 
	   (fun () -> (add_theory true false
			 (constr_of a)
			 (constr_of aplus)
			 (constr_of amult)
			 (constr_of aone)
			 (constr_of azero)
			 (constr_of aopp)
			 (constr_of aeq)
			 (constr_of t)
			 (cset_of_comarg_list l)))
       | _ -> anomaly "AddRing")
    
let _ = 
  vinterp_add "AddAbstractSemiRing"
    (function 
       | [VARG_CONSTR a; VARG_CONSTR aplus; 
	  VARG_CONSTR amult; VARG_CONSTR aone;
	  VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> 
	   (fun () -> (add_theory false false
			 (constr_of a)
			 (constr_of aplus)
			 (constr_of amult)
			 (constr_of aone)
			 (constr_of azero)
			 mkImplicit
			 (constr_of aeq)
			 (constr_of t)
			 ConstrSet.empty))
       | _ -> anomaly "AddAbstractSemiRing")
    
let _ = 
  vinterp_add "AddAbstractRing"
    (function 
       | [ VARG_CONSTR a; VARG_CONSTR aplus; 
	   VARG_CONSTR amult; VARG_CONSTR aone;
	   VARG_CONSTR azero; VARG_CONSTR aopp; 
	   VARG_CONSTR aeq; VARG_CONSTR t ] -> 
	   (fun () -> (add_theory true true
			 (constr_of a)
			 (constr_of aplus)
			 (constr_of amult)
			 (constr_of aone)
			 (constr_of azero)
			 (constr_of aopp)
			 (constr_of aeq)
			 (constr_of t)
			 ConstrSet.empty))
       | _ -> anomaly "AddAbstractRing")
    
(******** The tactic itself *********)

(*
   gl : goal sigma
   th : semi-ring theory (concrete)
   cl : constr list [c1; c2; ...]
 
Builds 
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_spolynom gl th lc =
  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  (* aux creates the spolynom p by a recursive destructuration of c 
     and builds the varmap with side-effects *)
  let rec aux c = 
    match (kind_of_term (strip_outer_cast c)) with 
      | IsApp (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
	  mkAppA [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |]
      | IsApp (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
	  mkAppA [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |]
      | _ when closed_under th.th_closed c ->
	  mkAppA [| Lazy.force coq_SPconst; th.th_a; c |]
      | _ -> 
	  try Hashtbl.find varhash c 
	  with Not_found -> 
	    let newvar = mkAppA [| Lazy.force coq_SPvar; th.th_a; 
				   (path_of_int !counter) |] in
	    begin 
	      incr counter;
	      varlist := c :: !varlist;
	      Hashtbl.add varhash c newvar;
	      newvar
	    end
  in 
  let lp = List.map aux lc in
  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
  List.map 
    (fun p -> 
       (mkAppA [| Lazy.force coq_interp_sp; th.th_a; th.th_plus; th.th_mult; 
		  th.th_zero; v; p |],
	mkAppA [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; 
		  th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl 
		    (mkAppA [| Lazy.force coq_spolynomial_simplify; 
			       th.th_a; th.th_plus; th.th_mult; 
			       th.th_one; th.th_zero; 
			       th.th_eq; p|]) |],
	mkAppA [| Lazy.force coq_spolynomial_simplify_ok;
		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
		  th.th_eq; v; th.th_t; p |]))
    lp

(*
   gl : goal sigma
   th : ring theory (concrete)
   cl : constr list [c1; c2; ...]
 
Builds 
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_polynom gl th lc =
  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  let rec aux c = 
    match (kind_of_term (strip_outer_cast c)) with 
      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
	  mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |]
      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
	  mkAppA [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |]
      (* The special case of Zminus *)
      | IsApp (binop, [|c1; c2|])
	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
	                                 mkAppA [| th.th_opp; c2 |] |]) ->
	    mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1;
	              mkAppA [| Lazy.force coq_Popp; th.th_a; aux c2 |] |]
      | IsApp (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
	  mkAppA [| Lazy.force coq_Popp; th.th_a; aux c1 |]
      | _ when closed_under th.th_closed c ->
	  mkAppA [| Lazy.force coq_Pconst; th.th_a; c |]
      | _ -> 
	  try Hashtbl.find varhash c 
	  with Not_found -> 
	    let newvar = mkAppA [| Lazy.force coq_Pvar; th.th_a; 
				   (path_of_int !counter) |] in
	    begin 
	      incr counter;
	      varlist := c :: !varlist;
	      Hashtbl.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
  List.map 
    (fun p -> 
       (mkAppA [| Lazy.force coq_interp_p;
		  th.th_a; th.th_plus; th.th_mult; th.th_zero; th.th_opp;
		  v; p |],
	mkAppA [| Lazy.force coq_interp_cs;
		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl 
		    (mkAppA [| Lazy.force coq_polynomial_simplify; 
			       th.th_a; th.th_plus; th.th_mult; 
			       th.th_one; th.th_zero; 
			       th.th_opp; th.th_eq; p |]) |],
	mkAppA [| Lazy.force coq_polynomial_simplify_ok;
		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
		  th.th_opp; th.th_eq; v; th.th_t; p |]))
    lp

(*
   gl : goal sigma
   th : semi-ring theory (abstract)
   cl : constr list [c1; c2; ...]
 
Builds 
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_aspolynom gl th lc =
  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  (* aux creates the aspolynom p by a recursive destructuration of c 
     and builds the varmap with side-effects *)
  let rec aux c = 
    match (kind_of_term (strip_outer_cast c)) with 
      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
	  mkAppA [| Lazy.force coq_ASPplus; aux c1; aux c2 |]
      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
	  mkAppA [| Lazy.force coq_ASPmult; aux c1; aux c2 |]
      | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
      | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
      | _ -> 
	  try Hashtbl.find varhash c 
	  with Not_found -> 
	    let newvar = mkAppA [| Lazy.force coq_ASPvar; 
				   (path_of_int !counter) |] in
	    begin 
	      incr counter;
	      varlist := c :: !varlist;
	      Hashtbl.add varhash c newvar;
	      newvar
	    end
  in 
  let lp = List.map aux lc in
  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
  List.map 
    (fun p -> 
       (mkAppA [| Lazy.force coq_interp_asp; th.th_a; th.th_plus; th.th_mult; 
		  th.th_one; th.th_zero; v; p |],
	mkAppA [| Lazy.force coq_interp_acs; th.th_a; th.th_plus; th.th_mult; 
		  th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl 
		    (mkAppA [| Lazy.force coq_aspolynomial_normalize; p|]) |],
	mkAppA [| Lazy.force coq_spolynomial_simplify_ok;
		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
		  th.th_eq; v; th.th_t; p |]))
    lp

(*
   gl : goal sigma
   th : ring theory (abstract)
   cl : constr list [c1; c2; ...]
 
Builds 
   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
  where c'i is convertible with ci and
  c'i_eq_c''i is a proof of equality of c'i and c''i

*)

let build_apolynom gl th lc =
  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
  let varlist = ref ([] : constr list) in (* list of variables *)
  let counter = ref 1 in (* number of variables created + 1 *)
  let rec aux c = 
    match (kind_of_term (strip_outer_cast c)) with 
      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
	  mkAppA [| Lazy.force coq_APplus; aux c1; aux c2 |]
      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
	  mkAppA [| Lazy.force coq_APmult; aux c1; aux c2 |]
      (* The special case of Zminus *)
      | IsApp (binop, [|c1; c2|]) 
	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
	                                 mkAppA [| th.th_opp; c2 |] |]) ->
	    mkAppA [| Lazy.force coq_APplus; aux c1;
	              mkAppA [| Lazy.force coq_APopp; aux c2 |] |]
      | IsApp (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
	  mkAppA [| Lazy.force coq_APopp; aux c1 |]
      | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
      | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
      | _ -> 
	  try Hashtbl.find varhash c 
	  with Not_found -> 
	    let newvar = mkAppA [| Lazy.force coq_APvar; 
				   (path_of_int !counter) |] in
	    begin 
	      incr counter;
	      varlist := c :: !varlist;
	      Hashtbl.add varhash c newvar;
	      newvar
	    end
  in
  let lp = List.map aux lc in
  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
  List.map 
    (fun p -> 
       (mkAppA [| Lazy.force coq_interp_ap;
		  th.th_a; th.th_plus; th.th_mult; th.th_one; 
		  th.th_zero; th.th_opp; v; p |],
	mkAppA [| Lazy.force coq_interp_sacs;
		  th.th_a; th.th_plus; th.th_mult; 
		  th.th_one; th.th_zero; th.th_opp; v; 
		  pf_reduce cbv_betadeltaiota gl 
		    (mkAppA [| Lazy.force coq_apolynomial_normalize; p |]) |],
	mkAppA [| Lazy.force coq_apolynomial_normalize_ok;
		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
		  th.th_opp; th.th_eq; v; th.th_t; p |]))
    lp
    
module SectionPathSet = 
  Set.Make(struct
	     type t = section_path
	     let compare = Pervasives.compare
	   end)

(* Avec l'uniformisation des red_kind, on perd ici sur la structure
   SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
let constants_to_unfold = 
(*  List.fold_right SectionPathSet.add *)
    [ path_of_string "Coq.ring.Ring_normalize.interp_cs";
      path_of_string "Coq.ring.Ring_normalize.interp_var";
      path_of_string "Coq.ring.Ring_normalize.interp_vl";
      path_of_string "Coq.ring.Ring_abstract.interp_acs";
      path_of_string "Coq.ring.Ring_abstract.interp_sacs";
      path_of_string "Coq.ring.Quote.varmap_find" ]
(*    SectionPathSet.empty *)

(* Unfolds the functions interp and find_btree in the term c of goal gl *)
let polynom_unfold_tac =
  let flags = (UNIFORM, red_add betaiota_red (CONST constants_to_unfold)) in
  reduct_in_concl (cbv_norm_flags flags)
      
(* lc : constr list *)
(* th : theory associated to t *)
(* op : clause (None for conclusion or Some id for hypothesis id) *)
(* gl : goal  *)
(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i)) 
   where the ring R, the Ring theory RC, the varmap v and the polynomials p_i
   are guessed and such that c_i = (interp R RC v p_i) *)
let raw_polynom th op lc gl =
  (* first we sort the terms : if t' is a subterm of t it must appear
     after t in the list. This is to avoid that the normalization of t'
     modifies t in a non-desired way *)
  let lc = sort_subterm gl lc in
  let ltriplets = 
    if th.th_abstract then 
      if th.th_ring
      then build_apolynom gl th lc
      else build_aspolynom gl th lc
    else
      if th.th_ring 
      then build_polynom gl th lc
      else build_spolynom gl th lc in 
  let polynom_tac = 
    List.fold_right2
      (fun ci (c'i, c''i, c'i_eq_c''i) tac ->
        let c'''i = pf_nf gl c''i in
          if pf_conv_x gl c'''i ci then tac (* convertible terms *)
          else
           (tclORELSE
             (tclORELSE
               (h_exact c'i_eq_c''i)
               (h_exact (mkAppA
                 [| build_coq_sym_eqT (); th.th_a; c'''i; ci; c'i_eq_c''i |]))
             ) 
	     (tclTHENS 
	       (elim_type (mkAppA [| build_coq_eqT (); th.th_a; c'''i; ci |]))
               [ tac ;
                 h_exact c'i_eq_c''i
               ]
             )
           )
      ) lc ltriplets polynom_unfold_tac 
  in
  polynom_tac gl

let guess_eq_tac th = 
  (tclORELSE reflexivity
     (tclTHEN 
	polynom_unfold_tac
	(tclREPEAT 
	   (tclORELSE 
	      (apply (mkAppA [| build_coq_f_equal2 ();
				th.th_a; th.th_a; th.th_a;
				th.th_plus |])) 
	      (apply (mkAppA [| build_coq_f_equal2 ();
				th.th_a; th.th_a; th.th_a; 
				th.th_mult |]))))))

let polynom lc gl =
  match lc with 
   (* If no argument is given, try to recognize either an equality or
      a declared relation with arguments c1 ... cn, 
      do "Ring c1 c2 ... cn" and then try to apply the simplification
      theorems declared for the relation *)
    | [] ->
	(match Hipattern.match_with_equation (pf_concl gl) with
	   | Some (eq,t::args) ->
	       let th = guess_theory t in
	       if List.exists 
		 (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) args
	       then 
		 errorlabstrm "Ring :"
		   [< 'sTR" All terms must have the same type" >];
	       (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl
	   | _ -> 
	       errorlabstrm "polynom :" 
		 [< 'sTR" This goal is not an equality" >])
    (* Elsewhere, guess the theory, check that all terms have the same type
       and apply raw_polynom *)
    | c :: lc' -> 
	let t = pf_type_of gl c in 
	let th = guess_theory t in 
	if List.exists 
	  (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) lc'
	then 
	  errorlabstrm "Ring :"
	    [< 'sTR" All terms must have the same type" >];
	(tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl

let dyn_polynom ltacargs gl =  
  polynom (List.map 
	     (function 
		| Command c -> pf_interp_constr gl c 
		| Constr c -> c 
		| _ -> anomaly "dyn_polynom")
	     ltacargs) gl

let v_polynom = add_tactic "Ring" dyn_polynom