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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Libnames
open Printer
open Newring_ast
open Newring
open Stdarg
open Tacarg
open Pcoq.Constr
open Pltac
}
DECLARE PLUGIN "newring_plugin"
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" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
{ let l = match l with None -> [] | Some l -> l in add_theory id t l }
| ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
fun ~pstate ->
Feedback.msg_notice (strbrk "The following ring structures have been declared:");
Spmap.iter (fun fn fi ->
(* We should use the global env here as this shouldn't contain proof
data, however preserving behavior as requested in review. *)
let sigma, env = Option.cata Pfedit.get_current_context
(let e = Global.env () in Evd.from_env e, e) pstate in
Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
) !from_name;
pstate }
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" ident(id) ":" constr(t) field_mods_opt(l) ] ->
{ let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
fun ~pstate ->
Feedback.msg_notice (strbrk "The following field structures have been declared:");
Spmap.iter (fun fn fi ->
(* We should use the global env here as this shouldn't
contain proof data. *)
let sigma, env = Option.cata Pfedit.get_current_context
(let e = Global.env () in Evd.from_env e, e) pstate in
Feedback.msg_notice (hov 2
(Ppconstr.pr_id (Libnames.basename fn)++spc()++
str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
) !field_from_name;
pstate }
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
|
