1.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Nov 30 12:09:24 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Nov 30 13:05:08 2016 +0100
1.3 @@ -62,13 +62,13 @@
1.4
1.5 (*.handle an input as into an algebra system.*)
1.6 fun dtss2itm_ ppc (d, ts) =
1.7 -let
1.8 - val (f, (d, id)) = the (find_first ((curry op= d) o
1.9 - (#1: (term * term) -> term) o
1.10 - (#2: pbt_ -> (term * term))) ppc)
1.11 -in
1.12 - ([1], true, f, Cor ((d, ts), (id, ts)))
1.13 -end
1.14 + let
1.15 + val (f, (d, id)) = the (find_first ((curry op= d) o
1.16 + (#1: (term * term) -> term) o
1.17 + (#2: pbt_ -> (term * term))) ppc)
1.18 + in
1.19 + ([1], true, f, Cor ((d, ts), (id, ts)))
1.20 + end
1.21
1.22 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
1.23
1.24 @@ -234,15 +234,12 @@
1.25 let val itm = appl_add' dI oris ppc pbt selct;
1.26 in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end
1.27
1.28 -fun oris2itms _ _ [] = ([] : itm list)
1.29 +fun oris2itms _ _ [] = ([] : itm list) (* WN161130: similar in ptyps ?!? *)
1.30 | oris2itms pbt vat ((i, v, f, d, ts) :: (os: ori list)) =
1.31 if member op = vat v
1.32 then (i, v, true, f, Cor ((d, ts), (e_term, []))) :: (oris2itms pbt vat os)
1.33 else oris2itms pbt vat os
1.34
1.35 -fun filter_dsc oris itm =
1.36 - filter_out ((curry op= ((d_in o #5) (itm:itm))) o (#4:ori -> term)) oris
1.37 -
1.38 fun par2fstr ((_, _, _, f, Par s) : itm) = (f, s)
1.39 | par2fstr itm = error ("par2fstr: called with " ^ itm2str_ (thy2ctxt' "Isac") itm)
1.40 fun itms2fstr ((_, _, _, f, Cor ((d, ts), _)) : itm) = (f, comp_dts'' (d, ts))
1.41 @@ -263,9 +260,13 @@
1.42 in xxx [] iitems end;
1.43
1.44 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
1.45 -fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
1.46 - let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.47 - spec = sspec as (sdI,spI,smI), probl, meth, ...} = get_obj I pt p;
1.48 +fun input_icalhd pt (((p, _), hdf, imodel, Pbl, spec as (dI, pI, mI)) : icalhd) =
1.49 + let
1.50 + val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case get_obj I pt p of
1.51 + PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.52 + spec = sspec as (sdI, spI, smI), probl, meth, ...}
1.53 + => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
1.54 + | _ => error "input_icalhd: uncovered case of get_obj I pt p"
1.55 in if is_casinput hdf fmz then the (cas_input (str2term hdf))
1.56 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
1.57 let val (pos_, pits, mits) =
1.58 @@ -274,24 +275,25 @@
1.59 val (its, trms) = filter_sep is_Par its;
1.60 val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
1.61 in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.62 - else if pI <> spI
1.63 - then if pI = snd3 ospec then (Pbl, probl, meth)
1.64 - else
1.65 - let val pbt = (#ppc o get_pbt) pI
1.66 - val dI' = #1 (some_spec ospec spec)
1.67 - val oris = if pI = #2 ospec then oris
1.68 - else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.69 - in (Pbl, appl_adds dI' oris probl pbt
1.70 - (map itms2fstr probl), meth) end
1.71 - else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.72 - then let val met = (#ppc o get_met) mI
1.73 - val mits = complete_metitms oris probl meth met
1.74 - in if foldl and_ (true, map #3 mits)
1.75 - then (Pbl, probl, mits) else (Met, probl, mits)
1.76 - end
1.77 - else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
1.78 - ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
1.79 - (imodel2fstr imodel), meth);
1.80 + else
1.81 + if pI <> spI
1.82 + then if pI = snd3 ospec then (Pbl, probl, meth)
1.83 + else
1.84 + let val pbt = (#ppc o get_pbt) pI
1.85 + val dI' = #1 (some_spec ospec spec)
1.86 + val oris = if pI = #2 ospec then oris
1.87 + else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.88 + in (Pbl, appl_adds dI' oris probl pbt
1.89 + (map itms2fstr probl), meth) end
1.90 + else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.91 + then let val met = (#ppc o get_met) mI
1.92 + val mits = complete_metitms oris probl meth met
1.93 + in if foldl and_ (true, map #3 mits)
1.94 + then (Pbl, probl, mits) else (Met, probl, mits)
1.95 + end
1.96 + else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
1.97 + ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
1.98 + (imodel2fstr imodel), meth)
1.99 val pt = update_spec pt p spec;
1.100 in if pos_ = Pbl
1.101 then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.102 @@ -306,120 +308,32 @@
1.103 end
1.104 end
1.105 end
1.106 - | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
1.107 - error "input_icalhd Met not impl.";
1.108 + | input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl."
1.109
1.110
1.111 (***. handle an input formula .***)
1.112 -(*
1.113 -Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
1.114 -Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
1.115 -wenn Abteilungen nur auf gleichem Level gesucht werden ?
1.116 -WN.040216
1.117
1.118 -Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
1.119 -
1.120 -------------------------------------------------------------------------------
1.121 -"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
1.122 -------------------------------------------------------------------------------
1.123 -1. "5 * x / (x - 2) - x / (x + 2) = 4"
1.124 -...
1.125 -4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
1.126 -...
1.127 -4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
1.128 -...
1.129 -4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
1.130 -...
1.131 -"[x = -4 / 3]"
1.132 -------------------------------------------------------------------------------
1.133 -(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
1.134 -
1.135 -(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
1.136 -------------------------------------------------------------------------------
1.137 -
1.138 -
1.139 -------------------------------------------------------------------------------
1.140 -"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
1.141 -------------------------------------------------------------------------------
1.142 -1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
1.143 -...
1.144 -4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
1.145 - Subproblem["normalize", "polynomial", "univariate"..
1.146 -...
1.147 -4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
1.148 -...
1.149 -4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.150 -4.4.5. "[x = 0, x = 6 / 5]"
1.151 -...
1.152 -5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.153 - "[x = 6 / 5]"
1.154 -------------------------------------------------------------------------------
1.155 -(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
1.156 -
1.157 -(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
1.158 -------------------------------------------------------------------------------
1.159 -
1.160 -
1.161 -------------------------------------------------------------------------------
1.162 -"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1.163 -------------------------------------------------------------------------------
1.164 -1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
1.165 -...
1.166 -6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
1.167 - Subproblem["sq", "root'", "univariate", "equation"]
1.168 -...
1.169 -6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
1.170 - Subproblem["normalize", "polynomial", "univariate", "equation"]
1.171 -...
1.172 -6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
1.173 -... Or_to_List
1.174 -6.6.3.2 "UniversalList"
1.175 -------------------------------------------------------------------------------
1.176 -(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
1.177 -
1.178 -(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
1.179 -------------------------------------------------------------------------------
1.180 -*)
1.181 -(*sh. comments auf 498*)
1.182 -
1.183 -fun equal a b = a=b;
1.184 +fun equal a b = a = b
1.185
1.186 (*the lists contain eq-al elem-pairs at the beginning;
1.187 return first list reverted (again) - ie. in order as required subsequently*)
1.188 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
1.189 - if equal f1 i1 then
1.190 - if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is)
1.191 - else (rev (f1::f2::fs), i1::i2::is)
1.192 + if equal f1 i1
1.193 + then
1.194 + if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
1.195 + else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
1.196 else error "dropwhile': did not start with equal elements"
1.197 | dropwhile' equal (f::fs) [i] =
1.198 - if equal f i then (rev (f::fs), [i])
1.199 + if equal f i
1.200 + then (rev (f::fs), [i])
1.201 else error "dropwhile': did not start with equal elements"
1.202 | dropwhile' equal [f] (i::is) =
1.203 - if equal f i then ([f], i::is)
1.204 - else error "dropwhile': did not start with equal elements";
1.205 -(*
1.206 - fun equal a b = a=b;
1.207 - val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
1.208 - val r_foder = rev foder; val r_ifoder = rev ifoder;
1.209 - dropwhile' equal r_foder r_ifoder;
1.210 -> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
1.211 + if equal f i
1.212 + then ([f], i::is)
1.213 + else error "dropwhile': did not start with equal elements"
1.214 + | dropwhile' _ _ _ = error "dropwhile': uncovered case"
1.215
1.216 - val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
1.217 - val r_foder = rev foder; val r_ifoder = rev ifoder;
1.218 - dropwhile' equal r_foder r_ifoder;
1.219 -> val it = ([3], [3, 12, 11]) : int list * int list
1.220 -
1.221 - val foder = [5]; val ifoder = [11,12,3,4,5];
1.222 - val r_foder = rev foder; val r_ifoder = rev ifoder;
1.223 - dropwhile' equal r_foder r_ifoder;
1.224 -> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
1.225 -
1.226 - val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
1.227 - val r_foder = rev foder; val r_ifoder = rev ifoder;
1.228 - dropwhile' equal r_foder r_ifoder;
1.229 -> *** dropwhile': did not start with equal elements*)
1.230 -
1.231 -(*040214: version for concat_deriv*)
1.232 +(* 040214: version for concat_deriv *)
1.233 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
1.234
1.235 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
1.236 @@ -430,9 +344,9 @@
1.237 (Rewrite_Set (Lucin.rule2rls' r),
1.238 Rewrite_Set' ("Isac", false, rls, t, (t', a)),
1.239 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
1.240 - | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t);
1.241 + | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t)
1.242
1.243 -(*fo = ifo excluded already in inform*)
1.244 +(* fo = ifo excluded already in inform *)
1.245 fun concat_deriv rew_ord erls rules fo ifo =
1.246 let
1.247 fun derivat ([]:(term * rule * (term * term list)) list) = e_term
1.248 @@ -452,32 +366,14 @@
1.249 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
1.250 in (true, fod' @ (map rev_deriv' rifod')) end
1.251 else (false, [])
1.252 - end;
1.253 -(*
1.254 - val ({rew_ord, erls, rules,...}, fo, ifo) =
1.255 - (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
1.256 - (tracing o trtas2str) fod';
1.257 -> ["
1.258 -(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
1.259 -(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
1.260 -(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
1.261 -(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
1.262 -val it = () : unit
1.263 - (tracing o trtas2str) (map rev_deriv' rifod');
1.264 -> ["
1.265 -(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
1.266 -(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
1.267 -(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
1.268 -val it = () : unit
1.269 -*)
1.270 -
1.271 + end
1.272
1.273 (* compare inform with ctree.form at current pos by nrls;
1.274 if found, embed the derivation generated during comparison
1.275 if not, let the mat-engine compute the next ctree.form *)
1.276 -(*structure copied from complete_solve
1.277 - CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
1.278 - all_modspec etc. has to be inserted at Subproblem'*)
1.279 +(* structure copied from complete_solve
1.280 + CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
1.281 + all_modspec etc. has to be inserted at Subproblem'*)
1.282 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
1.283 let
1.284 val fo =
1.285 @@ -501,16 +397,15 @@
1.286 else
1.287 let
1.288 val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
1.289 - val cs' as (tacis, c'', ptp) =
1.290 - case tacis of
1.291 - ((Subproblem _, _, _)::_) =>
1.292 - let
1.293 - val ptp as (pt, (p,_)) = all_modspec ptp (*<------------------*)
1.294 - val mI = get_obj g_metID pt p
1.295 - in
1.296 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.297 - end
1.298 - | _ => cs';
1.299 + val (tacis, c'', ptp) = case tacis of
1.300 + ((Subproblem _, _, _)::_) =>
1.301 + let
1.302 + val ptp as (pt, (p,_)) = all_modspec ptp (*<--------------------*)
1.303 + val mI = get_obj g_metID pt p
1.304 + in
1.305 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.306 + end
1.307 + | _ => cs';
1.308 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.309 end;
1.310
1.311 @@ -560,7 +455,7 @@
1.312 collect all the tacs applied by the way;
1.313 if "no derivation found" then check_error_patterns.
1.314 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
1.315 -fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
1.316 +fun inform (cs as (_, _, (pt, pos as (p, _))): calcstate') istr =
1.317 case parse (assoc_thy "Isac") istr of
1.318 SOME f_in =>
1.319 let
1.320 @@ -574,8 +469,7 @@
1.321 SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
1.322 | NONE =>
1.323 let
1.324 - val pos_pred = lev_back' pos
1.325 - (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
1.326 + val pos_pred = lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.327 val f_pred = get_curr_formula (pt, pos_pred)
1.328 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
1.329 (*last step re-calc in compare_step TODO before WN09*)
1.330 @@ -584,8 +478,12 @@
1.331 ("no derivation found", calcstate') =>
1.332 let
1.333 val pp = par_pblobj pt p
1.334 - val {errpats, nrls, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
1.335 - val ScrState (env, _, _, _, _, _) = get_istate pt pos
1.336 + val (errpats, nrls, prog) = case get_met (get_obj g_metID pt pp) of
1.337 + {errpats, nrls, scr = Prog prog, ...} => (errpats, nrls, prog)
1.338 + | _ => error "inform: uncovered case of get_met"
1.339 + val env = case get_istate pt pos of
1.340 + ScrState (env, _, _, _, _, _) => env
1.341 + | _ => error "inform: uncovered case of get_istate"
1.342 in
1.343 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
1.344 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
1.345 @@ -594,7 +492,7 @@
1.346 | _ => msg_calcstate'
1.347 end
1.348 end
1.349 - | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
1.350 + | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate')
1.351
1.352 (* fill-in patterns an forms.
1.353 returns thm required by "fun in_fillform *)
1.354 @@ -604,29 +502,37 @@
1.355 rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
1.356 in (*the fillpat of the thm must be dedicated to errpatID*)
1.357 if errpatID = erpaID andalso rewritten
1.358 - then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) else NONE end;
1.359 + then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
1.360 + else NONE
1.361 + end
1.362
1.363 fun get_fillpats subst form errpatID thm =
1.364 - let
1.365 - val thmDeriv = Thm.get_name_hint thm
1.366 - val (part, thyID) = Rtools.thy_containing_thm thmDeriv
1.367 - val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
1.368 - val Hthm {fillpats, ...} = get_the theID
1.369 - val some = map (get_fillform subst (thm, form) errpatID) fillpats
1.370 - in some |> filter is_some |> map the end;
1.371 + let
1.372 + val thmDeriv = Thm.get_name_hint thm
1.373 + val (part, thyID) = Rtools.thy_containing_thm thmDeriv
1.374 + val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
1.375 + val fillpats = case get_the theID of
1.376 + Hthm {fillpats, ...} => fillpats
1.377 + | _ => error "get_fillpats: uncovered case of get_the"
1.378 + val some = map (get_fillform subst (thm, form) errpatID) fillpats
1.379 + in some |> filter is_some |> map the end
1.380
1.381 fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
1.382 let
1.383 val f_curr = get_curr_formula (pt, pos);
1.384 val pp = par_pblobj pt p
1.385 - val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
1.386 - val ScrState (env, _, _, _, _, _) = get_istate pt pos
1.387 + val (errpats, prog) = case get_met (get_obj g_metID pt pp) of
1.388 + {errpats, scr = Prog prog, ...} => (errpats, prog)
1.389 + | _ => error "find_fillpatterns: uncovered case of get_met"
1.390 + val env = case get_istate pt pos of
1.391 + ScrState (env, _, _, _, _, _) => env
1.392 + | _ => error "inform: uncovered case of get_istate"
1.393 val subst = Rtools.get_bdv_subst prog env
1.394 val errpatthms = errpats
1.395 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
1.396 |> map (#3: errpat -> thm list)
1.397 |> flat
1.398 - in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end;
1.399 + in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
1.400
1.401 (* check if an input formula is exactly equal the rewrite from a rule
1.402 which is stored at the pos where the input is stored of "ok". *)
1.403 @@ -643,8 +549,9 @@
1.404 | Appl rew =>
1.405 let
1.406 val res = case rew of
1.407 - Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
1.408 - | Rewrite' (_, _, _, _, _, _, (res, _)) => res
1.409 + Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
1.410 + | Rewrite' (_, _, _, _, _, _, (res, _)) => res
1.411 + | t => error ("is_exactly_equal: uncovered case for " ^ tac_2str t)
1.412 in
1.413 if not (ifo = res)
1.414 then ("input does not exactly fill the gaps", Tac "")
1.415 @@ -661,13 +568,16 @@
1.416 | Rewrite_Set_Inst (_, rlsID) => rlsID
1.417 | _ => "e_rls"
1.418 val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
1.419 - val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
1.420 + val rls = case get_the [part, thyID, "Rulesets", rlsID] of
1.421 + Hrls {thy_rls = (_, rls), ...} => rls
1.422 + | _ => error "fetchErrorpatterns: uncovered case of get_the"
1.423 in case rls of
1.424 - Rls {errpatts, ...} => errpatts
1.425 - | Seq {errpatts, ...} => errpatts
1.426 - | Rrls {errpatts, ...} => errpatts
1.427 - | Erls => []
1.428 + Rls {errpatts, ...} => errpatts
1.429 + | Seq {errpatts, ...} => errpatts
1.430 + | Rrls {errpatts, ...} => errpatts
1.431 + | Erls => []
1.432 end
1.433 +
1.434 (**)
1.435 end
1.436 (**)
1.437 \ No newline at end of file
2.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Nov 30 12:09:24 2016 +0100
2.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Nov 30 13:05:08 2016 +0100
2.3 @@ -39,6 +39,9 @@
2.4 "--------- embed fun find_fillpatterns ---------------------------";
2.5 "--------- build fun is_exactly_equal, inputFillFormula ----------";
2.6 "--------- fun appl_adds -----------------------------------------";
2.7 +"--------- fun concat_deriv --------------------------------------";
2.8 +"--------- handle an input formula -------------------------------";
2.9 +"--------- fun dropwhile' ----------------------------------------";
2.10 "-----------------------------------------------------------------";
2.11 "-----------------------------------------------------------------";
2.12 "-----------------------------------------------------------------";
2.13 @@ -1322,3 +1325,120 @@
2.14 val itm = appl_add' dI oris ppc pbt selct;
2.15 val ppc = insert_ppc' itm ppc;
2.16 *)
2.17 +"--------- fun concat_deriv --------------------------------------";
2.18 +"--------- fun concat_deriv --------------------------------------";
2.19 +"--------- fun concat_deriv --------------------------------------";
2.20 +(*
2.21 + val ({rew_ord, erls, rules,...}, fo, ifo) =
2.22 + (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
2.23 + (tracing o trtas2str) fod';
2.24 +> ["
2.25 +(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
2.26 +(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
2.27 +(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
2.28 +(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
2.29 +val it = () : unit
2.30 + (tracing o trtas2str) (map rev_deriv' rifod');
2.31 +> ["
2.32 +(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
2.33 +(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
2.34 +(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
2.35 +val it = () : unit
2.36 +*)
2.37 +"--------- handle an input formula -------------------------------";
2.38 +"--------- handle an input formula -------------------------------";
2.39 +"--------- handle an input formula -------------------------------";
2.40 +(*
2.41 +Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
2.42 +Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
2.43 +wenn Abteilungen nur auf gleichem Level gesucht werden ?
2.44 +WN.040216
2.45 +
2.46 +Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
2.47 +
2.48 +------------------------------------------------------------------------------
2.49 +"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
2.50 +------------------------------------------------------------------------------
2.51 +1. "5 * x / (x - 2) - x / (x + 2) = 4"
2.52 +...
2.53 +4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
2.54 +...
2.55 +4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
2.56 +...
2.57 +4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
2.58 +...
2.59 +"[x = -4 / 3]"
2.60 +------------------------------------------------------------------------------
2.61 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
2.62 +
2.63 +(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
2.64 +------------------------------------------------------------------------------
2.65 +
2.66 +
2.67 +------------------------------------------------------------------------------
2.68 +"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
2.69 +------------------------------------------------------------------------------
2.70 +1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
2.71 +...
2.72 +4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
2.73 + Subproblem["normalize", "polynomial", "univariate"..
2.74 +...
2.75 +4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
2.76 +...
2.77 +4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
2.78 +4.4.5. "[x = 0, x = 6 / 5]"
2.79 +...
2.80 +5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
2.81 + "[x = 6 / 5]"
2.82 +------------------------------------------------------------------------------
2.83 +(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
2.84 +
2.85 +(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
2.86 +------------------------------------------------------------------------------
2.87 +
2.88 +
2.89 +------------------------------------------------------------------------------
2.90 +"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
2.91 +------------------------------------------------------------------------------
2.92 +1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
2.93 +...
2.94 +6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
2.95 + Subproblem["sq", "root'", "univariate", "equation"]
2.96 +...
2.97 +6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
2.98 + Subproblem["normalize", "polynomial", "univariate", "equation"]
2.99 +...
2.100 +6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
2.101 +... Or_to_List
2.102 +6.6.3.2 "UniversalList"
2.103 +------------------------------------------------------------------------------
2.104 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
2.105 +
2.106 +(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
2.107 +------------------------------------------------------------------------------
2.108 +*)
2.109 +(*sh. comments auf 498*)
2.110 +"--------- fun dropwhile' ----------------------------------------";
2.111 +"--------- fun dropwhile' ----------------------------------------";
2.112 +"--------- fun dropwhile' ----------------------------------------";
2.113 +(*
2.114 + fun equal a b = a=b;
2.115 + val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
2.116 + val r_foder = rev foder; val r_ifoder = rev ifoder;
2.117 + dropwhile' equal r_foder r_ifoder;
2.118 +> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
2.119 +
2.120 + val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
2.121 + val r_foder = rev foder; val r_ifoder = rev ifoder;
2.122 + dropwhile' equal r_foder r_ifoder;
2.123 +> val it = ([3], [3, 12, 11]) : int list * int list
2.124 +
2.125 + val foder = [5]; val ifoder = [11,12,3,4,5];
2.126 + val r_foder = rev foder; val r_ifoder = rev ifoder;
2.127 + dropwhile' equal r_foder r_ifoder;
2.128 +> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
2.129 +
2.130 + val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
2.131 + val r_foder = rev foder; val r_ifoder = rev ifoder;
2.132 + dropwhile' equal r_foder r_ifoder;
2.133 +> *** dropwhile': did not start with equal elements*)