1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
{
open Ltac_plugin
open Pp
open Util
open Ring_ast
open Ring
open Stdarg
open Tacarg
open Pcoq.Constr
open Pltac
}
DECLARE PLUGIN "coq-core.plugins.ring"
TACTIC EXTEND protect_fv
| [ "protect_fv" string(map) "in" ident(id) ] ->
{ protect_tac_in map id }
| [ "protect_fv" string(map) ] ->
{ protect_tac map }
END
{
open Pptactic
open Ppconstr
let pr_ring_mod env sigma = function
| Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg (pr_constr_expr env sigma) eq_test
| Ring_kind Abstract -> str "abstract"
| Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg (pr_constr_expr env sigma) morph
| Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
| Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
| Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
| Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic env sigma t ++ str "]"
| Setoid(sth,ext) -> str "setoid" ++ pr_arg (pr_constr_expr env sigma) sth ++ pr_arg (pr_constr_expr env sigma) ext
| Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
| Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg (pr_constr_expr env sigma) spec ++ spc () ++ str "[" ++ pr_raw_tactic env sigma cst_tac ++ str "]"
| Sign_spec t -> str "sign" ++ pr_arg (pr_constr_expr env sigma) t
| Div_spec t -> str "div" ++ pr_arg (pr_constr_expr env sigma) t
}
VERNAC ARGUMENT EXTEND ring_mod
PRINTED BY { pr_ring_mod env sigma }
| [ "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 pr_ring_mods env sigma l = surround (prlist_with_sep pr_comma (pr_ring_mod env sigma) l)
}
VERNAC ARGUMENT EXTEND ring_mods
PRINTED BY { pr_ring_mods env sigma }
| [ "(" ne_ring_mod_list_sep(mods, ",") ")" ] -> { mods }
END
VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
| [ "Add" "Ring" identref(id) ":" constr(t) ring_mods_opt(l) ] ->
{ add_theory id.CAst.v t (Option.default [] l) }
| [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
print_rings ()
}
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 pr_field_mod env sigma = function
| Ring_mod m -> pr_ring_mod env sigma m
| Inject inj -> str "completeness" ++ pr_arg (pr_constr_expr env sigma) inj
}
VERNAC ARGUMENT EXTEND field_mod
PRINTED BY { pr_field_mod env sigma }
| [ ring_mod(m) ] -> { Ring_mod m }
| [ "completeness" constr(inj) ] -> { Inject inj }
END
{
let pr_field_mods env sigma l = surround (prlist_with_sep pr_comma (pr_field_mod env sigma) l)
}
VERNAC ARGUMENT EXTEND field_mods
PRINTED BY { pr_field_mods env sigma }
| [ "(" ne_field_mod_list_sep(mods, ",") ")" ] -> { mods }
END
VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
| [ "Add" "Field" identref(id) ":" constr(t) field_mods_opt(l) ] ->
{ let l = match l with None -> [] | Some l -> l in add_field_theory id.CAst.v t l }
| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
print_fields ()
}
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
|
