<commit_before>
(* $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 sp id = 
  Declare.global_sp_reference (path_of_string sp) (id_of_string id)

(* Ring_theory *)

let coq_Ring_Theory = 
  lazy (constant "#Ring_theory#Ring_Theory.cci" "Ring_Theory")
let coq_Semi_Ring_Theory = 
  lazy (constant "#Ring_theory#Semi_Ring_Theory.cci" "Semi_Ring_Theory")

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

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

(* Logic *)
let coq_f_equal2 = lazy (constant "#Logic#f_equal2.cci" "f_equal2")
let coq_eq = lazy (constant "#Logic#eq.cci" "eq")
let coq_eqT = lazy (constant "#Logic_Type#eqT.cci" "eqT")

(*********** 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) }

(* 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 spec_th x = x in
  declare_object ("tactic-ring-theory",
		  { load_function = (fun _ -> ());
		    open_function = (fun _ -> ());
                    cache_function = cache_th;
		    specification_function = spec_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 =<commit_msg>Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'<commit_after>
(* $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 sp id = 
  Declare.global_sp_reference (path_of_string sp) (id_of_string id)

(* Ring_theory *)

let coq_Ring_Theory = 
  lazy (constant "#Ring_theory#Ring_Theory.cci" "Ring_Theory")
let coq_Semi_Ring_Theory = 
  lazy (constant "#Ring_theory#Semi_Ring_Theory.cci" "Semi_Ring_Theory")

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

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

(* Logic *)
let coq_f_equal2 = lazy (constant "#Logic#f_equal2.cci" "f_equal2")
let coq_eq = lazy (constant "#Logic#eq.cci" "eq")
let coq_eqT = lazy (constant "#Logic_Type#eqT.cci" "eqT")

(*********** 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) }

(* 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 spec_th x = x in
  declare_object ("tactic-ring-theory",
		  { load_function = cache_th;
		    open_function = (fun _ -> ());
                    cache_function = cache_th;
		    specification_function = spec_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 =
{'fraction_non_alphanumeric': 0.11095609355765285, 'fraction_numerical': 0.0018054985638079606, 'mean_word_length': 4.526530612244898, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 16, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5274445', 'n_tokens_mistral': 4602, 'n_tokens_neox': 4340, 'n_words': 1030}