Adding a proper interface to Newring.

The ring ASTs were put in a separate interface, and only the
extension-related code was put in a dedicated G_newring file.

5 files changed, 233 insertions, 133 deletions

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
new file mode 100644
index 000000000..856ec0db5
--- /dev/null
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -0,0 +1,90 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+open Pp
+open Util
+open Libnames
+open Printer
+open Newring_ast
+open Newring
+
+DECLARE PLUGIN "newring_plugin"
+
+TACTIC EXTEND protect_fv
+  [ "protect_fv" string(map) "in" ident(id) ] ->
+    [ Proofview.V82.tactic (protect_tac_in map id) ]
+| [ "protect_fv" string(map) ] ->
+    [ Proofview.V82.tactic (protect_tac map) ]
+END
+
+TACTIC EXTEND closed_term
+  [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
+    [ Proofview.V82.tactic (closed_term t l) ]
+END
+
+VERNAC ARGUMENT EXTEND ring_mod
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
+  | [ "abstract" ] -> [ Ring_kind Abstract ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
+  | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
+  | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
+  | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
+  | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ]
+  | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ]
+  | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ]
+  | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
+           [ Pow_spec (Closed l, pow_spec) ]
+  | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
+           [ Pow_spec (CstTac cst_tac, pow_spec) ]
+  | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ]
+END
+
+VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
+  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
+    [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
+      add_theory id (ic t) set k cst (pre,post) power sign div]
+  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
+    msg_notice (strbrk "The following ring structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.ring_req))
+    ) !from_name ]
+END
+
+TACTIC EXTEND ring_lookup
+| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
+    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t]
+END
+
+VERNAC ARGUMENT EXTEND field_mod
+  | [ ring_mod(m) ] -> [ Ring_mod m ]
+  | [ "completeness" constr(inj) ] -> [ Inject inj ]
+END
+
+VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
+| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
+  [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
+    add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
+| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
+    msg_notice (strbrk "The following field structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.field_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.field_req))
+    ) !field_from_name ]
+END
+
+TACTIC EXTEND field_lookup
+| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
+      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
+END
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml
index 72ebfae48..7844a36c1 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml
@@ -30,8 +30,7 @@ open Declare
 open Decl_kinds
 open Entries
 open Misctypes
-
-DECLARE PLUGIN "newring_plugin"
+open Newring_ast
 
 (****************************************************************************)
 (* controlled reduction *)
@@ -105,13 +104,6 @@ let protect_tac_in map id =
   Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));;
 
 
-TACTIC EXTEND protect_fv
-  [ "protect_fv" string(map) "in" ident(id) ] ->
-    [ Proofview.V82.tactic (protect_tac_in map id) ]
-| [ "protect_fv" string(map) ] ->
-    [ Proofview.V82.tactic (protect_tac map) ]
-END;;
-
 (****************************************************************************)
 
 let closed_term t l =
@@ -120,12 +112,6 @@ let closed_term t l =
   if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
 ;;
 
-TACTIC EXTEND closed_term
-  [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ Proofview.V82.tactic (closed_term t l) ]
-END
-;;
-
 (* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
   [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
@@ -354,20 +340,6 @@ let _ = add_map "ring"
 (****************************************************************************)
 (* Ring database *)
 
-type ring_info =
-    { ring_carrier : types;
-      ring_req : constr;
-      ring_setoid : constr;
-      ring_ext : constr;
-      ring_morph : constr;
-      ring_th : constr;
-      ring_cst_tac : glob_tactic_expr;
-      ring_pow_tac : glob_tactic_expr;
-      ring_lemma1 : constr;
-      ring_lemma2 : constr;
-      ring_pre_tac : glob_tactic_expr;
-      ring_post_tac : glob_tactic_expr }
-
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -599,13 +571,6 @@ let dest_morph env sigma m_spec =
         (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
     | _ -> error "bad morphism structure"
 
-
-type 'constr coeff_spec =
-    Computational of 'constr (* equality test *)
-  | Abstract (* coeffs = Z *)
-  | Morphism of 'constr (* general morphism *)
-
-
 let reflect_coeff rkind =
   (* We build an ill-typed terms on purpose... *)
   match rkind with
@@ -613,10 +578,6 @@ let reflect_coeff rkind =
     | Computational c -> lapp coq_comp [|c|]
     | Morphism m -> lapp coq_morph [|m|]
 
-type cst_tac_spec =
-    CstTac of raw_tactic_expr
-  | Closed of reference list
-
 let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
       Some (CstTac t) -> Tacintern.glob_tactic t
@@ -720,41 +681,12 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
           ring_post_tac = posttac }) in
   ()
 
-type 'constr ring_mod =
-    Ring_kind of 'constr coeff_spec
-  | Const_tac of cst_tac_spec
-  | Pre_tac of raw_tactic_expr
-  | Post_tac of raw_tactic_expr
-  | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr
-  | Pow_spec of cst_tac_spec * Constrexpr.constr_expr
-           (* Syntaxification tactic , correctness lemma *)
-  | Sign_spec of Constrexpr.constr_expr
-  | Div_spec of Constrexpr.constr_expr
-
-
 let ic_coeff_spec = function
   | Computational t -> Computational (ic_unsafe t)
   | Morphism t -> Morphism (ic_unsafe t)
   | Abstract -> Abstract
 
 
-VERNAC ARGUMENT EXTEND ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
-  | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
-  | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
-  | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
-  | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
-  | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ]
-  | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ]
-  | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ]
-  | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] ->
-           [ Pow_spec (Closed l, pow_spec) ]
-  | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] ->
-           [ Pow_spec (CstTac cst_tac, pow_spec) ]
-  | [ "div" constr(div_spec) ] -> [ Div_spec div_spec ]
-END
-
 let set_once s r v =
   if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
 
@@ -779,20 +711,6 @@ let process_ring_mods l =
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
-  | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
-    [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
-      add_theory id (ic t) set k cst (pre,post) power sign div]
-  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
-    msg_notice (strbrk "The following ring structures have been declared:");
-    Spmap.iter (fun fn fi ->
-      msg_notice (hov 2
-        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.ring_req))
-    ) !from_name ]
-END
-
 (*****************************************************************************)
 (* The tactics consist then only in a lookup in the ring database and
    call the appropriate ltac. *)
@@ -838,13 +756,6 @@ let ring_lookup (f:glob_tactic_expr) lH rl t =
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
-TACTIC EXTEND ring_lookup
-| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t]
-END
-
-
-
 (***********************************************************************)
 
 let new_field_path =
@@ -918,19 +829,6 @@ let dest_field env evd th_spec =
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
     | _ -> error "bad field structure"
 
-type field_info =
-    { field_carrier : types;
-      field_req : constr;
-      field_cst_tac : glob_tactic_expr;
-      field_pow_tac : glob_tactic_expr;
-      field_ok : constr;
-      field_simpl_eq_ok : constr;
-      field_simpl_ok : constr;
-      field_simpl_eq_in_ok : constr;
-      field_cond : constr;
-      field_pre_tac : glob_tactic_expr;
-      field_post_tac : glob_tactic_expr }
-
 let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
 let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
@@ -1077,15 +975,6 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
           field_pre_tac = pretac;
           field_post_tac = posttac }) in  ()
 
-type 'constr field_mod =
-    Ring_mod of 'constr ring_mod
-  | Inject of Constrexpr.constr_expr
-
-VERNAC ARGUMENT EXTEND field_mod
-  | [ ring_mod(m) ] -> [ Ring_mod m ]
-  | [ "completeness" constr(inj) ] -> [ Inject inj ]
-END
-
 let process_field_mods l =
   let kind = ref None in
   let set = ref None in
@@ -1110,21 +999,6 @@ let process_field_mods l =
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
-| [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
-  [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
-    add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
-| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
-    msg_notice (strbrk "The following field structures have been declared:");
-    Spmap.iter (fun fn fi ->
-      msg_notice (hov 2
-        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.field_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.field_req))
-    ) !field_from_name ]
-END
-
-
 let ltac_field_structure e =
   let req = carg e.field_req in
   let cst_tac = Tacexp e.field_cst_tac in
@@ -1153,9 +1027,3 @@ let field_lookup (f:glob_tactic_expr) lH rl t =
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
-
-
-TACTIC EXTEND field_lookup
-| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
-END
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
new file mode 100644
index 000000000..4bd3383d6
--- /dev/null
+++ b/plugins/setoid_ring/newring.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Constr
+open Libnames
+open Globnames
+open Constrexpr
+open Tacexpr
+open Proof_type
+open Newring_ast
+
+val protect_tac_in : string -> Id.t -> tactic
+
+val protect_tac : string -> tactic
+
+val closed_term : constr -> global_reference list -> tactic
+
+val process_ring_mods :
+  constr_expr ring_mod list ->
+  constr coeff_spec * (constr * constr) option *
+  cst_tac_spec option * raw_tactic_expr option *
+  raw_tactic_expr option *
+  (cst_tac_spec * constr_expr) option *
+  constr_expr option * constr_expr option
+
+val add_theory :
+  Id.t ->
+  Evd.evar_map * constr ->
+  (constr * constr) option ->
+  constr coeff_spec ->
+  cst_tac_spec option ->
+  raw_tactic_expr option * raw_tactic_expr option ->
+  (cst_tac_spec * constr_expr) option ->
+  constr_expr option ->
+  constr_expr option -> unit
+
+val ic : constr_expr -> Evd.evar_map * constr
+
+val from_name : ring_info Spmap.t ref
+
+val ring_lookup :
+  glob_tactic_expr ->
+  constr list ->
+  constr list -> constr -> unit Proofview.tactic
+
+val process_field_mods :
+  constr_expr field_mod list ->
+  constr coeff_spec *
+  (constr * constr) option * constr option *
+  cst_tac_spec option * raw_tactic_expr option *
+  raw_tactic_expr option *
+  (cst_tac_spec * constr_expr) option *
+  constr_expr option * constr_expr option
+
+val add_field_theory :
+  Id.t ->
+  Evd.evar_map * constr ->
+  (constr * constr) option ->
+  constr coeff_spec ->
+  cst_tac_spec option ->
+  constr option ->
+  raw_tactic_expr option * raw_tactic_expr option ->
+  (cst_tac_spec * constr_expr) option ->
+  constr_expr option ->
+  constr_expr option -> unit
+
+val field_from_name : field_info Spmap.t ref
+
+val field_lookup :
+  glob_tactic_expr ->
+  constr list ->
+  constr list -> constr -> unit Proofview.tactic
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
new file mode 100644
index 000000000..c26fcc8d1
--- /dev/null
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Constr
+open Libnames
+open Constrexpr
+open Tacexpr
+
+type 'constr coeff_spec =
+    Computational of 'constr (* equality test *)
+  | Abstract (* coeffs = Z *)
+  | Morphism of 'constr (* general morphism *)
+
+type cst_tac_spec =
+    CstTac of raw_tactic_expr
+  | Closed of reference list
+
+type 'constr ring_mod =
+    Ring_kind of 'constr coeff_spec
+  | Const_tac of cst_tac_spec
+  | Pre_tac of raw_tactic_expr
+  | Post_tac of raw_tactic_expr
+  | Setoid of constr_expr * constr_expr
+  | Pow_spec of cst_tac_spec * constr_expr
+           (* Syntaxification tactic , correctness lemma *)
+  | Sign_spec of constr_expr
+  | Div_spec of constr_expr
+
+type 'constr field_mod =
+    Ring_mod of 'constr ring_mod
+  | Inject of constr_expr
+
+type ring_info =
+    { ring_carrier : types;
+      ring_req : constr;
+      ring_setoid : constr;
+      ring_ext : constr;
+      ring_morph : constr;
+      ring_th : constr;
+      ring_cst_tac : glob_tactic_expr;
+      ring_pow_tac : glob_tactic_expr;
+      ring_lemma1 : constr;
+      ring_lemma2 : constr;
+      ring_pre_tac : glob_tactic_expr;
+      ring_post_tac : glob_tactic_expr }
+
+type field_info =
+    { field_carrier : types;
+      field_req : constr;
+      field_cst_tac : glob_tactic_expr;
+      field_pow_tac : glob_tactic_expr;
+      field_ok : constr;
+      field_simpl_eq_ok : constr;
+      field_simpl_ok : constr;
+      field_simpl_eq_in_ok : constr;
+      field_cond : constr;
+      field_pre_tac : glob_tactic_expr;
+      field_post_tac : glob_tactic_expr }
diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib
index a98392f1e..7d6c49588 100644
--- a/plugins/setoid_ring/newring_plugin.mllib
+++ b/plugins/setoid_ring/newring_plugin.mllib
@@ -1,2 +1,3 @@
 Newring
 Newring_plugin_mod
+G_newring