23252
|
1 |
(* Title: HOL/Tools/Groebner_Basis/normalizer_data.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Amine Chaieb, TU Muenchen
|
|
4 |
|
|
5 |
Ring normalization data.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature NORMALIZER_DATA =
|
|
9 |
sig
|
|
10 |
type entry
|
|
11 |
val get: Proof.context -> (thm * entry) list
|
|
12 |
val match: Proof.context -> cterm -> entry option
|
|
13 |
val del: attribute
|
|
14 |
val add: {semiring: cterm list * thm list, ring: cterm list * thm list, idom: thm list}
|
|
15 |
-> attribute
|
|
16 |
val funs: thm -> {is_const: morphism -> cterm -> bool,
|
|
17 |
dest_const: morphism -> cterm -> Rat.rat,
|
|
18 |
mk_const: morphism -> ctyp -> Rat.rat -> cterm,
|
|
19 |
conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
|
|
20 |
val setup: theory -> theory
|
|
21 |
end;
|
|
22 |
|
|
23 |
structure NormalizerData: NORMALIZER_DATA =
|
|
24 |
struct
|
|
25 |
|
|
26 |
(* data *)
|
|
27 |
|
|
28 |
type entry =
|
|
29 |
{vars: cterm list,
|
|
30 |
semiring: cterm list * thm list,
|
|
31 |
ring: cterm list * thm list,
|
|
32 |
idom: thm list} *
|
|
33 |
{is_const: cterm -> bool,
|
|
34 |
dest_const: cterm -> Rat.rat,
|
|
35 |
mk_const: ctyp -> Rat.rat -> cterm,
|
|
36 |
conv: cterm -> thm};
|
|
37 |
|
|
38 |
val eq_key = Thm.eq_thm;
|
|
39 |
fun eq_data arg = eq_fst eq_key arg;
|
|
40 |
|
|
41 |
structure Data = GenericDataFun
|
|
42 |
(
|
|
43 |
val name = "HOL/norm";
|
|
44 |
type T = (thm * entry) list;
|
|
45 |
val empty = [];
|
|
46 |
val extend = I;
|
|
47 |
fun merge _ = AList.merge eq_key (K true);
|
|
48 |
fun print _ _ = ();
|
|
49 |
);
|
|
50 |
|
|
51 |
val get = Data.get o Context.Proof;
|
|
52 |
|
|
53 |
|
|
54 |
(* match data *)
|
|
55 |
|
|
56 |
fun match ctxt tm =
|
|
57 |
let
|
|
58 |
fun match_inst
|
|
59 |
({vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom},
|
|
60 |
fns as {is_const, dest_const, mk_const, conv}) pat =
|
|
61 |
let
|
|
62 |
fun h instT =
|
|
63 |
let
|
|
64 |
val substT = Thm.instantiate (instT, []);
|
|
65 |
val substT_cterm = Drule.cterm_rule substT;
|
|
66 |
|
|
67 |
val vars' = map substT_cterm vars;
|
|
68 |
val semiring' = (map substT_cterm sr_ops, map substT sr_rules);
|
|
69 |
val ring' = (map substT_cterm r_ops, map substT r_rules);
|
|
70 |
val idom' = map substT idom;
|
|
71 |
|
|
72 |
val result = ({vars = vars', semiring = semiring', ring = ring', idom = idom'}, fns);
|
|
73 |
in SOME result end
|
|
74 |
in (case try Thm.match (pat, tm) of
|
|
75 |
NONE => NONE
|
|
76 |
| SOME (instT, _) => h instT)
|
|
77 |
end;
|
|
78 |
|
|
79 |
fun match_struct (_,
|
|
80 |
entry as ({semiring = (sr_ops, _), ring = (r_ops, _), ...}, _): entry) =
|
|
81 |
get_first (match_inst entry) (sr_ops @ r_ops);
|
|
82 |
in get_first match_struct (get ctxt) end;
|
|
83 |
|
|
84 |
|
|
85 |
(* logical content *)
|
|
86 |
|
|
87 |
val semiringN = "semiring";
|
|
88 |
val ringN = "ring";
|
|
89 |
val idomN = "idom";
|
|
90 |
|
|
91 |
fun undefined _ = raise Match;
|
|
92 |
|
|
93 |
fun del_data key = remove eq_data (key, []);
|
|
94 |
|
|
95 |
val del = Thm.declaration_attribute (Data.map o del_data);
|
|
96 |
|
|
97 |
fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), idom} =
|
|
98 |
Thm.declaration_attribute (fn key => fn context => context |> Data.map
|
|
99 |
let
|
|
100 |
val ctxt = Context.proof_of context;
|
|
101 |
|
|
102 |
fun check kind name xs n =
|
|
103 |
null xs orelse length xs = n orelse
|
|
104 |
error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name);
|
|
105 |
val check_ops = check "operations";
|
|
106 |
val check_rules = check "rules";
|
|
107 |
|
|
108 |
val _ =
|
|
109 |
check_ops semiringN sr_ops 5 andalso
|
|
110 |
check_rules semiringN sr_rules 37 andalso
|
|
111 |
check_ops ringN r_ops 2 andalso
|
|
112 |
check_rules ringN r_rules 2 andalso
|
|
113 |
check_rules idomN idom 2;
|
|
114 |
|
|
115 |
val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
|
|
116 |
val sr_rules' = map mk_meta sr_rules;
|
|
117 |
val r_rules' = map mk_meta r_rules;
|
|
118 |
|
|
119 |
fun rule i = nth sr_rules' (i - 1);
|
|
120 |
|
|
121 |
val (cx, cy) = Thm.dest_binop (hd sr_ops);
|
|
122 |
val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
|
|
123 |
val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
|
|
124 |
val ((clx, crx), (cly, cry)) =
|
|
125 |
rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
|
|
126 |
val ((ca, cb), (cc, cd)) =
|
|
127 |
rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
|
|
128 |
val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
|
|
129 |
val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
|
|
130 |
|
|
131 |
val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
|
|
132 |
val _ = map print_thm sr_rules';
|
|
133 |
val semiring = (sr_ops, sr_rules');
|
|
134 |
val ring = (r_ops, r_rules');
|
|
135 |
in
|
|
136 |
del_data key #>
|
|
137 |
cons (key, ({vars = vars, semiring = semiring, ring = ring, idom = idom},
|
|
138 |
{is_const = undefined, dest_const = undefined, mk_const = undefined,
|
|
139 |
conv = undefined}))
|
|
140 |
end);
|
|
141 |
|
|
142 |
|
|
143 |
(* extra-logical functions *)
|
|
144 |
|
|
145 |
fun funs raw_key {is_const, dest_const, mk_const, conv} phi = Data.map (fn data =>
|
|
146 |
let
|
|
147 |
val key = Morphism.thm phi raw_key;
|
|
148 |
val _ = AList.defined eq_key data key orelse
|
|
149 |
raise THM ("No data entry for structure key", 0, [key]);
|
|
150 |
val fns = {is_const = is_const phi, dest_const = dest_const phi,
|
|
151 |
mk_const = mk_const phi, conv = conv phi};
|
|
152 |
in AList.map_entry eq_key key (apsnd (K fns)) data end);
|
|
153 |
|
|
154 |
|
|
155 |
(* concrete syntax *)
|
|
156 |
|
|
157 |
local
|
|
158 |
|
|
159 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
|
|
160 |
fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
|
|
161 |
fun keyword3 k1 k2 k3 =
|
|
162 |
Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
|
|
163 |
|
|
164 |
val opsN = "ops";
|
|
165 |
val rulesN = "rules";
|
|
166 |
|
|
167 |
val normN = "norm";
|
|
168 |
val constN = "const";
|
|
169 |
val delN = "del";
|
|
170 |
|
|
171 |
val any_keyword =
|
|
172 |
keyword2 semiringN opsN || keyword2 semiringN rulesN ||
|
|
173 |
keyword2 ringN opsN || keyword2 ringN rulesN ||
|
|
174 |
keyword2 idomN rulesN;
|
|
175 |
|
|
176 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
|
|
177 |
val terms = thms >> map Drule.dest_term;
|
|
178 |
|
|
179 |
fun optional scan = Scan.optional scan [];
|
|
180 |
|
|
181 |
in
|
|
182 |
|
|
183 |
fun att_syntax src = src |> Attrib.syntax
|
|
184 |
(Scan.lift (Args.$$$ delN >> K del) ||
|
|
185 |
((keyword2 semiringN opsN |-- terms) --
|
|
186 |
(keyword2 semiringN rulesN |-- thms)) --
|
|
187 |
(optional (keyword2 ringN opsN |-- terms) --
|
|
188 |
optional (keyword2 ringN rulesN |-- thms)) --
|
|
189 |
optional (keyword2 idomN rulesN |-- thms)
|
|
190 |
>> (fn ((sr, r), id) => add {semiring = sr, ring = r, idom = id}));
|
|
191 |
|
|
192 |
end;
|
|
193 |
|
|
194 |
|
|
195 |
(* theory setup *)
|
|
196 |
|
|
197 |
val setup =
|
|
198 |
Attrib.add_attributes [("normalizer", att_syntax, "semiring normalizer data")];
|
|
199 |
|
|
200 |
end;
|