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
|
(************************************************************************)
(* 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
open Stdarg
open Constrarg
open Pcoq.Constr
open Pcoq.Tactic
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
TACTIC EXTEND closed_term
[ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
[ closed_term t l ]
END
open Pptactic
open Ppconstr
let pr_ring_mod = function
| Ring_kind (Computational eq_test) -> str "decidable" ++ pr_arg pr_constr_expr eq_test
| Ring_kind Abstract -> str "abstract"
| Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph
| Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
| Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]"
| Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
| Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
| Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext
| Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]"
| Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
| Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
| Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
VERNAC ARGUMENT EXTEND ring_mod
PRINTED BY pr_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 pr_ring_mods l = surround (prlist_with_sep pr_comma pr_ring_mod l)
VERNAC ARGUMENT EXTEND ring_mods
PRINTED BY pr_ring_mods
| [ "(" 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
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] -> [
Feedback.msg_notice (strbrk "The following ring structures have been declared:");
Spmap.iter (fun fn fi ->
Feedback.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
let pr_field_mod = function
| Ring_mod m -> pr_ring_mod m
| Inject inj -> str "completeness" ++ pr_arg pr_constr_expr inj
VERNAC ARGUMENT EXTEND field_mod
PRINTED BY pr_field_mod
| [ ring_mod(m) ] -> [ Ring_mod m ]
| [ "completeness" constr(inj) ] -> [ Inject inj ]
END
let pr_field_mods l = surround (prlist_with_sep pr_comma pr_field_mod l)
VERNAC ARGUMENT EXTEND field_mods
PRINTED BY pr_field_mods
| [ "(" 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
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] -> [
Feedback.msg_notice (strbrk "The following field structures have been declared:");
Spmap.iter (fun fn fi ->
Feedback.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
|
