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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo" i*)
(* $Id$ *)
open Names
open Proof_type
open Tacinterp
open Tacmach
open Term
open Util
open Vernacinterp
(* Interpretation of constr's *)
let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
(* Construction of constants *)
let constant dir s =
let dir = make_dirpath (List.map id_of_string ("Coq"::"field"::dir)) in
let id = id_of_string s in
try
Declare.global_reference_in_absolute_module dir id
with Not_found ->
anomaly ("Field: cannot find "^
(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
(* To deal with the optional arguments *)
let constr_of_opt a opt =
let ac = constr_of a in
match opt with
| None -> mkApp ((constant ["Field_Compl"] "None"),[|ac|])
| Some f -> mkApp ((constant ["Field_Compl"] "Some"),[|ac;constr_of f|])
(* Table of theories *)
let th_tab = ref ((Hashtbl.create 53) : (constr,constr) Hashtbl.t)
let lookup typ = Hashtbl.find !th_tab typ
let _ =
let init () = th_tab := (Hashtbl.create 53) in
let freeze () = !th_tab in
let unfreeze fs = th_tab := fs in
Summary.declare_summary "field"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
Summary.survive_section = false }
let load_addfield _ = ()
let cache_addfield (_,(typ,th)) = Hashtbl.add !th_tab typ th
let export_addfield x = Some x
(* Declaration of the Add Field library object *)
let (in_addfield,out_addfield)=
Libobject.declare_object
("ADD_FIELD",
{ Libobject.load_function = load_addfield;
Libobject.open_function = cache_addfield;
Libobject.cache_function = cache_addfield;
Libobject.export_function = export_addfield })
(* Adds a theory to the table *)
let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
ainv_l =
begin
(try
Ring.add_theory true true false a None None None aplus amult aone azero
(Some aopp) aeq rth Quote.ConstrSet.empty
with | UserError("Add Semi Ring",_) -> ());
let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"),
[|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
Lib.add_anonymous_leaf (in_addfield (a,th))
end
(* Vernac command declaration *)
let _ =
let rec opt_arg (aminus_o,adiv_o) = function
| (VARG_STRING "minus")::(VARG_CONSTR aminus)::l ->
(match aminus_o with
| None -> opt_arg ((Some aminus),adiv_o) l
| _ -> anomaly "AddField")
| (VARG_STRING "div")::(VARG_CONSTR adiv)::l ->
(match adiv_o with
| None -> opt_arg (aminus_o,(Some adiv)) l
| _ -> anomaly "AddField")
| _ -> (aminus_o,adiv_o) in
vinterp_add "AddField"
(function
| (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
::(VARG_CONSTR aeq)::(VARG_CONSTR ainv)::(VARG_CONSTR rth)
::(VARG_CONSTR ainv_l)::l ->
(fun () ->
let (aminus_o,adiv_o) = opt_arg (None,None) l in
add_field (constr_of a) (constr_of aplus) (constr_of amult)
(constr_of aone) (constr_of azero) (constr_of aopp)
(constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
(constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l))
| _ -> anomaly "AddField")
(* Guesses the type and calls Field_Gen with the right theory *)
let field g =
let evc = project g
and env = pf_env g in
let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
goalopt=Some g; debug=get_debug () } in
let typ = constr_of_Constr (interp_tacarg ist
<:tactic<
Match Context With
| [|- (eq ?1 ? ?)] -> ?1
| [|- (eqT ?1 ? ?)] -> ?1>>) in
let th = VArg (Constr (lookup typ)) in
(tac_interp [(id_of_string "FT",th)] [] (get_debug ())
<:tactic<
Match Context With
| [|- (eq ?1 ?2 ?3)] ->
Let t = (eqT ?1 ?2 ?3) In
Cut t;[Intro;
(Match Context With
| [id:t |- ?] -> Rewrite id;Reflexivity)|Field_Gen FT]
| [|- (eqT ? ? ?)] -> Field_Gen FT>>) g
(* Declaration of Field *)
let _ = hide_tactic "Field" (function _ -> field)
|
