diff options
Diffstat (limited to 'plugins/ring/g_ring.ml4')
| -rw-r--r-- | plugins/ring/g_ring.ml4 | 136 |
1 files changed, 136 insertions, 0 deletions
diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 new file mode 100644 index 00000000..d766e344 --- /dev/null +++ b/plugins/ring/g_ring.ml4 @@ -0,0 +1,136 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Quote +open Ring +open Tacticals + +TACTIC EXTEND ring +| [ "legacy" "ring" constr_list(l) ] -> [ polynom l ] +END + +(* The vernac commands "Add Ring" and co *) + +let cset_of_constrarg_list l = + List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty + +VERNAC COMMAND EXTEND AddRing + [ "Add" "Legacy" "Ring" + constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) + constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] + -> [ add_theory true false false + (constr_of a) + None + None + None + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (Some (constr_of aopp)) + (constr_of aeq) + (constr_of t) + (cset_of_constrarg_list l) ] + +| [ "Add" "Legacy" "Semi" "Ring" + constr(a) constr(aplus) constr(amult) constr(aone) constr(azero) + constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] + -> [ add_theory false false false + (constr_of a) + None + None + None + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + None + (constr_of aeq) + (constr_of t) + (cset_of_constrarg_list l) ] + +| [ "Add" "Legacy" "Abstract" "Ring" + constr(a) constr(aplus) constr(amult) constr(aone) + constr(azero) constr(aopp) constr(aeq) constr(t) ] + -> [ add_theory true true false + (constr_of a) + None + None + None + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (Some (constr_of aopp)) + (constr_of aeq) + (constr_of t) + ConstrSet.empty ] + +| [ "Add" "Legacy" "Abstract" "Semi" "Ring" + constr(a) constr(aplus) constr(amult) constr(aone) + constr(azero) constr(aeq) constr(t) ] + -> [ add_theory false true false + (constr_of a) + None + None + None + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + None + (constr_of aeq) + (constr_of t) + ConstrSet.empty ] + +| [ "Add" "Legacy" "Setoid" "Ring" + constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) + constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm) + constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] + -> [ add_theory true false true + (constr_of a) + (Some (constr_of aequiv)) + (Some (constr_of asetth)) + (Some { + plusm = (constr_of pm); + multm = (constr_of mm); + oppm = Some (constr_of om) }) + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + (Some (constr_of aopp)) + (constr_of aeq) + (constr_of t) + (cset_of_constrarg_list l) ] + +| [ "Add" "Legacy" "Semi" "Setoid" "Ring" + constr(a) constr(aequiv) constr(asetth) constr(aplus) + constr(amult) constr(aone) constr(azero) constr(aeq) + constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] + -> [ add_theory false false true + (constr_of a) + (Some (constr_of aequiv)) + (Some (constr_of asetth)) + (Some { + plusm = (constr_of pm); + multm = (constr_of mm); + oppm = None }) + (constr_of aplus) + (constr_of amult) + (constr_of aone) + (constr_of azero) + None + (constr_of aeq) + (constr_of t) + (cset_of_constrarg_list l) ] +END |