diff options
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 90 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml (renamed from plugins/setoid_ring/newring.ml4) | 134 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.mli | 78 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_ast.mli | 63 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_plugin.mllib | 1 |
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 |