189 |
189 |
190 fun optional scan = Scan.optional scan []; |
190 fun optional scan = Scan.optional scan []; |
191 |
191 |
192 in |
192 in |
193 |
193 |
194 val att_syntax = Attrib.syntax |
194 val attribute = |
195 (Scan.lift (Args.$$$ delN >> K del) || |
195 Scan.lift (Args.$$$ delN >> K del) || |
196 ((keyword2 semiringN opsN |-- terms) -- |
196 ((keyword2 semiringN opsN |-- terms) -- |
197 (keyword2 semiringN rulesN |-- thms)) -- |
197 (keyword2 semiringN rulesN |-- thms)) -- |
198 (optional (keyword2 ringN opsN |-- terms) -- |
198 (optional (keyword2 ringN opsN |-- terms) -- |
199 optional (keyword2 ringN rulesN |-- thms)) -- |
199 optional (keyword2 ringN rulesN |-- thms)) -- |
200 optional (keyword2 idomN rulesN |-- thms) -- |
200 optional (keyword2 idomN rulesN |-- thms) -- |
201 optional (keyword2 idealN rulesN |-- thms) |
201 optional (keyword2 idealN rulesN |-- thms) |
202 >> (fn (((sr, r), id), idl) => |
202 >> (fn (((sr, r), id), idl) => |
203 add {semiring = sr, ring = r, idom = id, ideal = idl})); |
203 add {semiring = sr, ring = r, idom = id, ideal = idl}); |
204 |
204 |
205 end; |
205 end; |
206 |
206 |
207 |
207 |
208 (* theory setup *) |
208 (* theory setup *) |
209 |
209 |
210 val setup = |
210 val setup = |
211 Attrib.add_attributes |
211 Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #> |
212 [("normalizer", att_syntax, "semiring normalizer data"), |
212 Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra"; |
213 ("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")]; |
|
214 |
213 |
215 end; |
214 end; |