104 val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9); |
104 val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9); |
105 val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true); |
105 val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true); |
106 val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false); |
106 val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false); |
107 |
107 |
108 |
108 |
109 structure LA_Data = |
109 structure LA_Data: LIN_ARITH_DATA = |
110 struct |
110 struct |
111 |
111 |
112 val neq_limit = neq_limit; |
112 val neq_limit = neq_limit; |
113 val verbose = verbose; |
113 val verbose = verbose; |
114 val trace = trace; |
114 val trace = trace; |
164 val (ot',p) = demult (t, Rat.one) |
164 val (ot',p) = demult (t, Rat.one) |
165 in (case (os',ot') of |
165 in (case (os',ot') of |
166 (SOME s', SOME t') => SOME (mC $ s' $ t') |
166 (SOME s', SOME t') => SOME (mC $ s' $ t') |
167 | (SOME s', NONE) => SOME s' |
167 | (SOME s', NONE) => SOME s' |
168 | (NONE, SOME t') => |
168 | (NONE, SOME t') => |
169 let val Const(_,T) = mC |
169 SOME (mC $ Const (@{const_name Groups.one}, domain_type (snd (dest_Const mC))) $ t') |
170 in SOME (mC $ Const (@{const_name Groups.one}, domain_type T) $ t') end |
|
171 | (NONE, NONE) => NONE, |
170 | (NONE, NONE) => NONE, |
172 Rat.mult m' (Rat.inv p)) |
171 Rat.mult m' (Rat.inv p)) |
173 end |
172 end |
174 (* terms that evaluate to numeric constants *) |
173 (* terms that evaluate to numeric constants *) |
175 | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m) |
174 | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m) |