1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -9,12 +9,6 @@
1.4 ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
1.5 ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
1.6 ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
1.7 -ML {*
1.8 -Rewrite'; (*thm' vvv*)
1.9 -fun thm'_to_thm'' ((thmID, str) : thm') = (thmID, str2term str) : thm'' (*TODO: id + remove*)
1.10 -fun thm''_to_thm' ((thmID, trm) : thm'') = (thmID, term2str trm) : thm' (*TODO: id + remove*);
1.11 -Rewrite; (*thm'' ^^^*)
1.12 -*}
1.13 ML_file "~~/src/Tools/isac/Interpret/generate.sml"
1.14 ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
1.15 ML_file "~~/src/Tools/isac/Interpret/appl.sml"
2.1 --- a/src/Tools/isac/Interpret/appl.sml Tue Oct 18 12:05:03 2016 +0200
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Oct 20 10:26:29 2016 +0200
2.3 @@ -374,9 +374,9 @@
2.4 let
2.5 val subst = subs2subst thy subs;
2.6 val subs' = subst2subs' subst;
2.7 - in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm'' thy thm'') f of
2.8 + in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of
2.9 SOME (f',asm) =>
2.10 - Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm''_to_thm' thm'', f, (f', asm)))
2.11 + Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
2.12 | NONE => Notappl ((fst thm'')^" not applicable")
2.13 end
2.14 handle _ => Notappl ("syntax error in "^(subs2str subs))
2.15 @@ -395,8 +395,8 @@
2.16 (pos'2str (p,p_)));
2.17 in if msg = "OK"
2.18 then
2.19 - case rewrite_ thy (assoc_rew_ord ro) rls' false (assoc_thm'' thy thm'') f of
2.20 - SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm''_to_thm' thm'', f, (f', asm)))
2.21 + case rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of
2.22 + SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
2.23 | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
2.24 else Notappl msg
2.25 end
2.26 @@ -417,9 +417,9 @@
2.27 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
2.28 | _ => error ("applicable_in: call by "^
2.29 (pos'2str (p,p_)));
2.30 - in case rewrite_ thy (assoc_rew_ord ro') erls false (assoc_thm'' thy thm'') f of
2.31 + in case rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of
2.32 SOME (f',asm) => Appl (
2.33 - Rewrite' (thy', ro', erls, false, thm''_to_thm' thm'', f, (f', asm)))
2.34 + Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
2.35 | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
2.36
2.37 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
3.1 --- a/src/Tools/isac/Interpret/ctree.sml Tue Oct 18 12:05:03 2016 +0200
3.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Oct 20 10:26:29 2016 +0200
3.3 @@ -326,6 +326,10 @@
3.4 | Check_Postcond of pblID
3.5 | Free_Solve
3.6
3.7 +(* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
3.8 + because there all the thms are present with both (thmID, thm)
3.9 + (where user-views can show both or only one of (thmID, thm)),
3.10 + and thm is created from ThmID by assoc_thm'' when entering isabisac *)
3.11 | Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
3.12 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
3.13 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
3.14 @@ -378,10 +382,10 @@
3.15 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
3.16 | Free_Solve => "Free_Solve"
3.17
3.18 - | Rewrite_Inst (subs, (id, term)) =>
3.19 - "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, term2str term)))
3.20 - | Rewrite (id, term) => "Rewrite " ^ spair2str (id, term2str term)
3.21 - | Rewrite_Asm (id, term) => "Rewrite_Asm " ^ spair2str (id, term2str term)
3.22 + | Rewrite_Inst (subs, (id, thm)) =>
3.23 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))
3.24 + | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
3.25 + | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)
3.26 | Rewrite_Set_Inst (subs, rls) =>
3.27 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
3.28 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
3.29 @@ -415,6 +419,15 @@
3.30 | End_Proof' => "tac End_Proof'"
3.31 | _ => "tac2str not impl. for ?!";
3.32
3.33 +fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false
3.34 +
3.35 +fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
3.36 + | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
3.37 + | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
3.38 + | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
3.39 + | eq_tac (Calculate id1, Calculate id2) = id1 = id2
3.40 + | eq_tac _ = false
3.41 +
3.42 fun is_rewset (Rewrite_Set_Inst _) = true
3.43 | is_rewset (Rewrite_Set _) = true
3.44 | is_rewset _ = false;
3.45 @@ -487,9 +500,9 @@
3.46 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst));
3.47
3.48 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
3.49 - | rule2tac _ [] (Thm (thmID, thm)) = Rewrite (thmID, Thm.prop_of thm)
3.50 - | rule2tac _ subst (Thm (thmID, thm)) =
3.51 - Rewrite_Inst (subst2subs subst, (thmID, Thm.prop_of thm))
3.52 + | rule2tac _ [] (Thm thm'') = Rewrite thm''
3.53 + | rule2tac _ subst (Thm thm'') =
3.54 + Rewrite_Inst (subst2subs subst, thm'')
3.55 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
3.56 | rule2tac _ subst (Rls_ rls) =
3.57 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
3.58 @@ -558,9 +571,9 @@
3.59 butlast tac is Check_elementwise: take only these asms*)
3.60 | Free_Solve'
3.61 (* context_thy would be simpler if instead thm' woudl be thm *)
3.62 - | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm' * term * (term * term list)
3.63 - | Rewrite' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
3.64 - | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
3.65 + | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
3.66 + | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
3.67 + | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
3.68 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
3.69 | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
3.70 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
3.71 @@ -1909,7 +1922,7 @@
3.72
3.73 fun append_atomic p l f r f' s pt =
3.74 let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**)
3.75 - val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
3.76 + val (iss, f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
3.77 then (*after Take*)
3.78 ((fst (get_obj g_loc pt p), SOME l),
3.79 get_obj g_form pt p)
3.80 @@ -1938,7 +1951,7 @@
3.81 );
3.82 (*TODO.WN050305 redesign the handling of istates*)
3.83 fun cappend_atomic pt p ist_res f r f' s =
3.84 - if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
3.85 + if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
3.86 then (*after Take: transfer Frm and respective istate*)
3.87 let
3.88 val (ist_form, f) =
3.89 @@ -1991,7 +2004,7 @@
3.90 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
3.91 fun append_parent p l f r b pt =
3.92 let (*val _= tracing("###append_parent: pos ="^pos2str p);*)
3.93 - val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
3.94 + val (ll,f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
3.95 then ((fst (get_obj g_loc pt p), SOME l),
3.96 get_obj g_form pt p)
3.97 else ((SOME l, NONE), f)
4.1 --- a/src/Tools/isac/Interpret/generate.sml Tue Oct 18 12:05:03 2016 +0200
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Oct 20 10:26:29 2016 +0200
4.3 @@ -334,14 +334,14 @@
4.4 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =
4.5 let
4.6 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.7 - (Rewrite_Inst (subst2subs subs', thm'_to_thm'' thm')) (f',asm) Complete;
4.8 + (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
4.9 val pt = update_branch pt p TransitiveB
4.10 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.11
4.12 | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
4.13 let
4.14 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
4.15 - (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete
4.16 + (Rewrite thm') (f',asm) Complete
4.17 val pt = update_branch pt p TransitiveB
4.18 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
4.19
5.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Oct 18 12:05:03 2016 +0200
5.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Oct 20 10:26:29 2016 +0200
5.3 @@ -523,13 +523,14 @@
5.4 fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
5.5
5.6 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
5.7 - (Rewrite (id, Thm.prop_of thm),
5.8 - Rewrite' ("Isac", fst ro, erls, false, rule2thm' r, t, (t', a)),
5.9 + (Rewrite (id, thm),
5.10 + Rewrite' ("Isac", fst ro, erls, false, rule2thm'' r, t, (t', a)),
5.11 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
5.12 - | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
5.13 + | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
5.14 (Rewrite_Set (rule2rls' r),
5.15 Rewrite_Set' ("Isac", false, rls, t, (t', a)),
5.16 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)));
5.17 + (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
5.18 + | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t);
5.19
5.20 (*fo = ifo excluded already in inform*)
5.21 fun concat_deriv rew_ord erls rules fo ifo =
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Oct 18 12:05:03 2016 +0200
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 20 10:26:29 2016 +0200
6.3 @@ -542,35 +542,31 @@
6.4 SOME (f',_) =>[rule2tac thy subst thm']
6.5 | NONE => []
6.6 else (case rewrite_ thy ro erls false thm f of
6.7 - SOME (f',_) => [rule2tac thy [] thm']
6.8 + SOME (f',_) => [rule2tac thy [] thm']
6.9 | NONE => [])
6.10 | try_rew thy _ _ _ f (cal as Calc c) =
6.11 (case get_calculation_ thy c f of
6.12 - SOME (str, _) => [rule2tac thy [] cal]
6.13 + SOME (str, _) => [rule2tac thy [] cal]
6.14 | NONE => [])
6.15 | try_rew thy _ _ _ f (cal as Cal1 c) =
6.16 (case get_calculation_ thy c f of
6.17 - SOME (str, _) => [rule2tac thy [] cal]
6.18 + SOME (str, _) => [rule2tac thy [] cal]
6.19 | NONE => [])
6.20 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
6.21 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
6.22 - distinct (flat (map (try_rew thy ro erls subst f) rules))
6.23 + gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
6.24 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
6.25 - distinct (flat (map (try_rew thy ro erls subst f) rules))
6.26 + gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
6.27 | filter_appl_rews thy subst f (Rrls _) = [];
6.28
6.29 (*. decide if a tactic is applicable to a given formula;
6.30 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
6.31 -(* val
6.32 - *)
6.33 fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
6.34 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
6.35 - | atomic_appl_tacs thy ro erls f (Rewrite (thm'' as (thmID, _))) =
6.36 - try_rew thy (ro, assoc_rew_ord ro) erls [] f
6.37 - (Thm (thmID, assoc_thm'' thy thm''))
6.38 - | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'' as (thmID, _))) =
6.39 - try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f
6.40 - (Thm (thmID, assoc_thm'' thy thm''))
6.41 + | atomic_appl_tacs thy ro erls f (Rewrite thm'') =
6.42 + try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')
6.43 + | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'')) =
6.44 + try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f (Thm thm'')
6.45
6.46 | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
6.47 filter_appl_rews thy [] f (assoc_rls rls')
6.48 @@ -637,7 +633,7 @@
6.49 fun guh2rewtac (guh:guh) ([] : subs) =
6.50 let val [isa, thy, sect, xstr] = guh2theID guh
6.51 in case sect of
6.52 - "Theorems" => Rewrite (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term))
6.53 + "Theorems" => Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
6.54 | "Rulesets" => Rewrite_Set xstr
6.55 | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
6.56 end
6.57 @@ -645,7 +641,7 @@
6.58 let val [isa, thy, sect, xstr] = guh2theID guh
6.59 in case sect of
6.60 "Theorems" =>
6.61 - Rewrite_Inst (subs, (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term)))
6.62 + Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
6.63 | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
6.64 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
6.65 end;
7.1 --- a/src/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
7.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Oct 20 10:26:29 2016 +0200
7.3 @@ -58,8 +58,8 @@
7.4 * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
7.5 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
7.6
7.7 -fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
7.8 - | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
7.9 +fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
7.10 + | rule2thm'' r = error ("rule2thm': not defined for "^(rule2str r));
7.11 fun rule2rls' (Rls_ rls) = id_rls rls
7.12 | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
7.13
7.14 @@ -69,7 +69,7 @@
7.15 let
7.16 val thy = assoc_thy thy'
7.17 val ctxt = get_ctxt pt p |> insert_assumptions am
7.18 - val m = Rewrite' (thy', ro, er, pa, rule2thm' r, f, (f', am))
7.19 + val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
7.20 val is = RrlsState (f', f'', rss, rts)
7.21 val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
7.22 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
7.23 @@ -78,7 +78,7 @@
7.24 let
7.25 val thy = assoc_thy thy'
7.26 val ctxt = get_ctxt pt p |> insert_assumptions am
7.27 - val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
7.28 + val m = Rewrite' (thy',ro,er,pa, rule2thm'' r, f, (f', am))
7.29 val is = RrlsState (f',f'',rss,rts)
7.30 val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
7.31 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
7.32 @@ -340,20 +340,19 @@
7.33 (*.convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac,
7.34 then convert to a 'tac_' (as required in appy).
7.35 arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)
7.36 -fun stac2tac_ pt thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =
7.37 +fun stac2tac_ _ thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ _) =
7.38 let
7.39 val tid = (de_esc_underscore o strip_thy) thmID
7.40 - in (Rewrite (tid, (Thm.prop_of o (assoc_thm'' thy)) (tid, e_term)), Empty_Tac_)
7.41 + in (Rewrite (tid, assoc_thm'' thy tid), Empty_Tac_)
7.42 end
7.43
7.44 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) =
7.45 + | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ _) =
7.46 let
7.47 val subML = ((map isapair2pair) o isalist2list) sub
7.48 val subStr = subst2subs subML
7.49 val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
7.50 - in (Rewrite_Inst (subStr, (tid, (Thm.prop_of o (assoc_thm'' thy)) (tid, e_term))), Empty_Tac_)
7.51 - end
7.52 -
7.53 + in (Rewrite_Inst (subStr, (tid, assoc_thm'' thy tid)), Empty_Tac_) end
7.54 +
7.55 | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
7.56 (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
7.57
7.58 @@ -462,7 +461,7 @@
7.59 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
7.60 NotAss : e.g. thmID in stac/=/thmID in m (not =)
7.61 *)
7.62 -fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', asm))) stac =
7.63 +fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm'' as (thmID, _), f, (f', asm))) stac =
7.64 (case stac of
7.65 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
7.66 if thmID = thmID_
7.67 @@ -472,12 +471,12 @@
7.68 else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
7.69 else ((*tracing"3### assod ..NotAss";*)NotAss)
7.70 | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) =>
7.71 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
7.72 + if contains_rule (Thm thm'') (assoc_rls rls_)
7.73 then
7.74 if f = f_ then Ass (m,f') else AssWeak (m,f')
7.75 else NotAss
7.76 | _ => NotAss)
7.77 - | assod pt d (m as Rewrite' (thy, rod, rls, put, (thmID, _), f, (f', asm))) stac =
7.78 + | assod pt d (m as Rewrite' (thy, rod, rls, put, thm'' as (thmID, _), f, (f', asm))) stac =
7.79 (case stac of
7.80 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
7.81 ((*tracing ("3### assod: stac = " ^ ter2str t);
7.82 @@ -493,7 +492,7 @@
7.83 AssWeak (m,f'))
7.84 else ((*tracing"3### assod ..NotAss";*)NotAss))
7.85 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
7.86 - if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)
7.87 + if contains_rule (Thm thm'') (assoc_rls rls_)
7.88 then
7.89 if f = f_ then Ass (m,f') else AssWeak (m,f')
7.90 else NotAss
7.91 @@ -642,10 +641,8 @@
7.92 | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
7.93 | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
7.94
7.95 - | tac_2tac (Rewrite' (thy,rod,erls,put, thm',f,(f',asm))) = Rewrite (thm'_to_thm'' thm')
7.96 -
7.97 - | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm', _, _))=
7.98 - Rewrite_Inst (subst2subs sub, thm'_to_thm'' thm')
7.99 + | tac_2tac (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
7.100 + | tac_2tac (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (subst2subs sub, thm)
7.101
7.102 | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
7.103 | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
7.104 @@ -1177,9 +1174,9 @@
7.105 NOT IMPL. -- "error: do other step before"
7.106 NotLocatable: thus generate_hard
7.107 *)
7.108 -fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, (thmID, str), f, _)) (pt, p)
7.109 +fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
7.110 (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
7.111 - (case lo rss f (Thm (thmID, mk_thm (assoc_thy thy') str)) of
7.112 + (case lo rss f (Thm thm) of
7.113 [] => NotLocatable
7.114 | rts' =>
7.115 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
7.116 @@ -1459,10 +1456,9 @@
7.117 else
7.118 (case next_rule rss f of
7.119 NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
7.120 - | SOME (Thm (id, thm))(*8.6.03: muss auch f' liefern ?!!*) =>
7.121 - (Rewrite' (thy, "e_rew_ord", e_rls, false,
7.122 - (id, thm |> Thm.prop_of |> term2str), f, (e_term, [(*!?!8.6.03*)])),
7.123 - (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
7.124 + | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
7.125 + (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
7.126 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
7.127
7.128 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
7.129 (ScrState (E,l,a,v,s,b), ctxt) =
7.130 @@ -1630,7 +1626,7 @@
7.131 Frm => get_obj g_form pt p
7.132 | Res => (fst o (get_obj g_result pt)) p
7.133 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
7.134 - in (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
7.135 + in ((gen_distinct eq_tac) o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
7.136
7.137
7.138 (*
8.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy Tue Oct 18 12:05:03 2016 +0200
8.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Thu Oct 20 10:26:29 2016 +0200
8.3 @@ -8,4 +8,8 @@
8.4
8.5 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
8.6
8.7 +ML {*
8.8 +*} ML {*
8.9 +eval_true
8.10 +*}
8.11 end
8.12 \ No newline at end of file
9.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Tue Oct 18 12:05:03 2016 +0200
9.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 20 10:26:29 2016 +0200
9.3 @@ -415,18 +415,12 @@
9.4 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
9.5 identifiers starting with "#" come from Calc and
9.6 get a hand-made theorem (containing numerals only).*)
9.7 -fun assoc_thm'' (thy : theory) ((thmid, term) : thm'') =
9.8 - (case Symbol.explode thmid of
9.9 - "s"::"y"::"m"::"_"::id =>
9.10 - if hd id = "#"
9.11 - then mk_thm'' thy term
9.12 - else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
9.13 - | id =>
9.14 - if hd id = "#"
9.15 - then mk_thm'' thy term
9.16 - else thmid |> convert_metaview_to_thmid thy |> num_str
9.17 - ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) =>
9.18 - error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
9.19 +fun assoc_thm'' (thy : theory) (thmid : thmID) =
9.20 + case Symbol.explode thmid of
9.21 + "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
9.22 + | "s"::"y"::"m"::"_"::id => ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
9.23 + | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
9.24 + | _ => thmid |> convert_metaview_to_thmid thy |> num_str
9.25 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
9.26 (case Symbol.explode thmid of
9.27 "s"::"y"::"m"::"_"::id =>
10.1 --- a/src/Tools/isac/calcelems.sml Tue Oct 18 12:05:03 2016 +0200
10.2 +++ b/src/Tools/isac/calcelems.sml Thu Oct 20 10:26:29 2016 +0200
10.3 @@ -44,7 +44,7 @@
10.4 * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
10.5 from applicable_in..Calculate: opstr --calculate_/get_calculation_--> (thmID, thm)
10.6 *)
10.7 -type thm'' = thmID * term; (* only for transport via libisabelle isac-java <--- ME *)
10.8 +type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
10.9 type rls' = string;
10.10
10.11 (*.a 'guh'='globally unique handle' is a string unique for each element
10.12 @@ -293,7 +293,7 @@
10.13 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
10.14 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
10.15 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
10.16 -fun thm''_of_thm thm = (thmID_of_derivation_name' thm, Thm.prop_of thm) : thm''
10.17 +fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
10.18
10.19 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
10.20 (strip_thy thmid1) = (strip_thy thmid2);
11.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Tue Oct 18 12:05:03 2016 +0200
11.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Thu Oct 20 10:26:29 2016 +0200
11.3 @@ -478,7 +478,7 @@
11.4 XML.Elem (("FORMULA", []), [
11.5 XML.Text form])]) (* repair for MathML: use term instead String *)
11.6 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
11.7 -fun xml_of_thm'' ((ID, term) : thm'') =
11.8 +fun xml_of_thm'' ((ID, thm) : thm'') =
11.9 (*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
11.10 XML.Elem (("THEOREM", []), [
11.11 XML.Elem (("ID", []), [XML.Text ID]),
11.12 @@ -487,7 +487,7 @@
11.13 XML.Elem (("THEOREM", []), [
11.14 XML.Elem (("ID", []), [XML.Text ID]),
11.15 XML.Elem (("FORMULA", []), [
11.16 - XML.Text (term2str term)])]) (* repair for MathML: use term instead String *)
11.17 + XML.Text ((term2str o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
11.18
11.19 fun xml_to_thm'
11.20 (XML.Elem (("THEOREM", []), [
11.21 @@ -506,8 +506,8 @@
11.22 -----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
11.23 (XML.Elem (("THEOREM", []), [
11.24 XML.Elem (("ID", []), [XML.Text ID]),
11.25 - XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
11.26 - XML.Text term])])) = ((ID, str2term term) : thm'')
11.27 + XML.Elem (("FORMULA", []), [
11.28 + XML.Text term])])) = (ID, assoc_thm'' (Isac ()) ID) : thm''
11.29 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
11.30
11.31 fun xml_of_src EmptyScr =
12.1 --- a/test/Tools/isac/Frontend/use-cases.sml Tue Oct 18 12:05:03 2016 +0200
12.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Oct 20 10:26:29 2016 +0200
12.3 @@ -81,7 +81,7 @@
12.4
12.5
12.6 (*------------ set at startup of the Kernel ----------------------*)
12.7 -reset_states (); (*resets all state information in Kernel *)
12.8 +reset_states (); (*resets all state information in Kernel *)
12.9 (*----------------------------------------------------------------*)
12.10
12.11 "--------- empty rootpbl --------------------------------";
12.12 @@ -207,7 +207,6 @@
12.13 "--------- miniscript with mini-subpbl ------------------";
12.14 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
12.15 "=== this sequence of fun-calls resembles fun me ===";
12.16 - reset_states (); (*start of calculation, return No.1*)
12.17 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
12.18 ("Test", ["sqroot-test","univariate","equation","test"],
12.19 ["Test","squ-equ-test-subpbl1"]))];
12.20 @@ -451,7 +450,7 @@
12.21 val (Form f, tac, asms) = pt_extract (pt, p);
12.22 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
12.23 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
12.24 -DEconstrCalcTree 1;
12.25 + DEconstrCalcTree 1;
12.26
12.27 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
12.28 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
12.29 @@ -512,12 +511,11 @@
12.30 val (Form f, tac, asms) = pt_extract (pt, p);
12.31 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
12.32 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
12.33 -DEconstrCalcTree 1;
12.34 + DEconstrCalcTree 1;
12.35
12.36 "--------- setContext..Thy ------------------------------";
12.37 "--------- setContext..Thy ------------------------------";
12.38 "--------- setContext..Thy ------------------------------";
12.39 - reset_states ();
12.40 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
12.41 ("Test", ["sqroot-test","univariate","equation","test"],
12.42 ["Test","squ-equ-test-subpbl1"]))];
12.43 @@ -577,7 +575,7 @@
12.44 val (Form f, tac, asms) = pt_extract (pt, p);
12.45 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
12.46 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
12.47 -DEconstrCalcTree 1;
12.48 + DEconstrCalcTree 1;
12.49
12.50 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
12.51 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
12.52 @@ -621,7 +619,7 @@
12.53 autoCalculate 1 (Step 1); fetchProposedTactic 1;
12.54 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
12.55 autoCalculate 1 (Step 1); fetchProposedTactic 1;
12.56 - setNextTactic 1 (Rewrite ("all_left", Thm.prop_of @{thm all_left}));
12.57 + setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
12.58 autoCalculate 1 (Step 1); fetchProposedTactic 1;
12.59 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
12.60 autoCalculate 1 (Step 1); fetchProposedTactic 1;
12.61 @@ -661,7 +659,7 @@
12.62 val (Form t,_,_) = pt_extract ptp;
12.63 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
12.64 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
12.65 -DEconstrCalcTree 1;
12.66 + DEconstrCalcTree 1;
12.67
12.68 "--------- tryMatchProblem, tryRefineProblem ------------";
12.69 "--------- tryMatchProblem, tryRefineProblem ------------";
12.70 @@ -781,8 +779,7 @@
12.71 val (Form f, tac, asms) = pt_extract (pt, p);
12.72 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
12.73 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
12.74 -
12.75 -DEconstrCalcTree 1;
12.76 + DEconstrCalcTree 1;
12.77
12.78 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
12.79 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
12.80 @@ -1356,7 +1353,6 @@
12.81 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
12.82 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
12.83 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
12.84 -reset_states ();
12.85 CalcTree
12.86 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
12.87 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
12.88 @@ -1374,10 +1370,12 @@
12.89 val p = get_pos 1 1;
12.90 val (Form f, _, asms) = pt_extract (pt, p);
12.91
12.92 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
12.93 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
12.94 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.95 - then () else error "embed fun get_fillform changed 1";
12.96 + if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
12.97 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
12.98 + ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
12.99 + | _ => error "embed fun get_fillform changed 1"
12.100 +else error "embed fun get_fillform changed 2";
12.101 +============ inhibit exn WN161019 TODO ========================================================*)
12.102
12.103 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
12.104 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
12.105 @@ -1433,13 +1431,13 @@
12.106 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
12.107 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
12.108 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
12.109 +DEconstrCalcTree 1;
12.110
12.111 "--------- UC errpat add-fraction, fillpat by input --------------";
12.112 "--------- UC errpat add-fraction, fillpat by input --------------";
12.113 "--------- UC errpat add-fraction, fillpat by input --------------";
12.114 (*cp from BridgeLog Java <=> SML*)
12.115 -reset_states ();
12.116 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
12.117 +=CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
12.118 Iterator 1;
12.119 moveActiveRoot 1;
12.120 moveActiveFormula 1 ([],Pbl);
12.121 @@ -1450,13 +1448,13 @@
12.122 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
12.123 --- but in BridgeLog Java <=> SML:
12.124 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
12.125 +DEconstrCalcTree 1;
12.126
12.127 "--------- UC errpat, fillpat step to Rewrite --------------------";
12.128 "--------- UC errpat, fillpat step to Rewrite --------------------";
12.129 "--------- UC errpat, fillpat step to Rewrite --------------------";
12.130 (*TODO*)
12.131 -reset_states ();
12.132 -CalcTree
12.133 +=CalcTree
12.134 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
12.135 "differentiateFor x", "derivative f_f'"],
12.136 ("Isac", ["derivative_of","function"],
12.137 @@ -1465,11 +1463,11 @@
12.138 moveActiveRoot 1;
12.139 autoCalculate 1 CompleteCalc;
12.140 val ((pt,p),_) = get_calc 1; show_pt pt;
12.141 +DEconstrCalcTree 1;
12.142
12.143 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
12.144 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
12.145 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
12.146 -reset_states ();
12.147 CalcTree
12.148 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
12.149 "differentiateFor x", "derivative f_f'"],
12.150 @@ -1517,4 +1515,5 @@
12.151 autoCalculate 1 CompleteCalc;
12.152 val ((pt,p),_) = get_calc 1; show_pt pt;
12.153 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
12.154 +DEconstrCalcTree 1;
12.155
13.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue Oct 18 12:05:03 2016 +0200
13.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Oct 20 10:26:29 2016 +0200
13.3 @@ -230,8 +230,8 @@
13.4 val nxt = tac2tac_ pt p nxt;
13.5 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
13.6 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
13.7 -if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
13.8 -then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
13.9 +case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => ()
13.10 +| _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus";
13.11
13.12
13.13 "--------- maximum example with 'specify', fmz = [] --------------";
13.14 @@ -733,8 +733,8 @@
13.15 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
13.16 []) : ptree*)
13.17 "----- WN101007 worked until here (checked same as isac2002) ---";
13.18 -if nxt = ("Model_Problem", Model_Problem) then ()
13.19 -else error "clchead.sml: check specify phase step 1";
13.20 +case nxt of ("Model_Problem", Model_Problem) => ()
13.21 +| _ => error "clchead.sml: check specify phase step 1";
13.22 "--- step 2 --";
13.23 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
13.24 (*val it = "--- step 2 --" : string
13.25 @@ -806,13 +806,13 @@
13.26 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
13.27 []) : ptree*)
13.28 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
13.29 -if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then ()
13.30 -else error "clchead.sml: check specify phase step 2";
13.31 +case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => ()
13.32 +| _ => error "clchead.sml: check specify phase step 2";
13.33 "--- step 3 --";
13.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.35 "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
13.36 -if nxt = ("Add_Given", Add_Given "integrateBy x") then ()
13.37 -else error "clchead.sml: check specify phase step 2";
13.38 +case nxt of ("Add_Given", Add_Given "integrateBy x") => ()
13.39 +| _ => error "clchead.sml: check specify phase step 2";
13.40
13.41 "--------- check: fmz matches pbt -----------------------";
13.42 "--------- check: fmz matches pbt -----------------------";
14.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Oct 18 12:05:03 2016 +0200
14.2 +++ b/test/Tools/isac/Interpret/ctree.sml Thu Oct 20 10:26:29 2016 +0200
14.3 @@ -132,8 +132,10 @@
14.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
14.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
14.6 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
14.7 -if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
14.8 -else error "new behaviour in test: miniscript with mini-subpbl";
14.9 +if res = "[x = 1]"
14.10 +then case nxt of ("End_Proof'", End_Proof') => ()
14.11 + | _ => error "new behaviour in test: miniscript with mini-subpbl 1"
14.12 +else error "new behaviour in test: miniscript with mini-subpbl 2"
14.13
14.14 show_pt pt;
14.15
15.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Oct 18 12:05:03 2016 +0200
15.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Oct 20 10:26:29 2016 +0200
15.3 @@ -160,8 +160,8 @@
15.4
15.5 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
15.6 val (_,(tac,_,_)::_) = get_calc 1;
15.7 - if tac = Rewrite_Set "norm_equation" then ()
15.8 - else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
15.9 + case tac of Rewrite_Set "norm_equation" => ()
15.10 + | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
15.11 autoCalculate 1 CompleteCalc;
15.12 val ((pt,_),_) = get_calc 1;
15.13 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
15.14 @@ -190,8 +190,8 @@
15.15
15.16 fetchProposedTactic 1;
15.17 val (_,(tac,_,_)::_) = get_calc 1;
15.18 - if tac = Rewrite_Set "Test_simplify" then ()
15.19 - else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
15.20 + case tac of Rewrite_Set "Test_simplify" => ()
15.21 + | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
15.22 autoCalculate 1 CompleteCalc;
15.23 val ((pt,_),_) = get_calc 1;
15.24 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
15.25 @@ -220,8 +220,8 @@
15.26
15.27 fetchProposedTactic 1;
15.28 val (_,(tac,_,_)::_) = get_calc 1;
15.29 - if tac = Check_Postcond ["LINEAR", "univariate", "equation", "test"] then ()
15.30 - else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
15.31 + case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
15.32 + | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
15.33 autoCalculate 1 CompleteCalc;
15.34 val ((pt,_),_) = get_calc 1;
15.35 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
15.36 @@ -1217,10 +1217,13 @@
15.37 val p = get_pos 1 1;
15.38 val (Form f, _, asms) = pt_extract (pt, p);
15.39
15.40 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
15.41 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
15.42 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
15.43 - then () else error "embed fun get_fillform changed 1";
15.44 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
15.45 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
15.46 + ("diff_sum", thm)) =>
15.47 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
15.48 + else error "embed fun get_fillform changed 11"
15.49 + | _ => error "embed fun get_fillform changed 12"
15.50 + else error "embed fun get_fillform changed 13";
15.51
15.52 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
15.53 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
15.54 @@ -1229,21 +1232,27 @@
15.55 val p = get_pos 1 1;
15.56
15.57 val (Form f, _, asms) = pt_extract (pt, p);
15.58 - if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
15.59 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
15.60 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
15.61 - then () else error "embed fun get_fillform changed 2";
15.62 + if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" then
15.63 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
15.64 + ("diff_sum", thm)) =>
15.65 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
15.66 + else error "embed fun get_fillform changed 21"
15.67 + | _ => error "embed fun get_fillform changed 22"
15.68 + else error "embed fun get_fillform changed 23";
15.69
15.70 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
15.71 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
15.72 val ((pt,pos),_) = get_calc 1;
15.73 val p = get_pos 1 1;
15.74 val (Form f, _, asms) = pt_extract (pt, p);
15.75 - if p = ([1], Res) andalso existpt [2] pt andalso
15.76 - term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
15.77 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
15.78 - ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
15.79 - then () else error "embed fun get_fillform changed 3";
15.80 + if p = ([1], Res) andalso existpt [2] pt
15.81 + andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
15.82 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
15.83 + ("diff_sum", thm)) =>
15.84 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
15.85 + else error "embed fun get_fillform changed 31"
15.86 + | _ => error "embed fun get_fillform changed 32"
15.87 + else error "embed fun get_fillform changed 33";
15.88
15.89 (* input a formula which exactly fills the gaps in a "fillformula"
15.90 presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
15.91 @@ -1260,7 +1269,7 @@
15.92 val p' = lev_on p;
15.93 val tac = get_obj g_tac pt p';
15.94 val Rewrite_Inst ([bbb as "(bdv, x)"], ("diff_sin_chain", ttt)) = tac;
15.95 -if term2str ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
15.96 +if (term2str o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
15.97 else error "inputFillFormula changed 10";
15.98 val Appl rew = applicable_in pos pt tac;
15.99 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
15.100 @@ -1275,9 +1284,11 @@
15.101 val ((pt, _),_) = get_calc 1;
15.102 val p = get_pos 1 1;
15.103 val (Form f, _, asms) = pt_extract (pt, p);
15.104 -if p = ([2], Res) andalso
15.105 - term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
15.106 - get_obj g_tac pt (fst p) =
15.107 - Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
15.108 -then () else error "inputFillFormula changed 11";
15.109 + if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)"
15.110 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
15.111 + ("diff_sin_chain", thm)) =>
15.112 + if (term2str o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
15.113 + else error "inputFillFormula changed 111"
15.114 + | _ => error "inputFillFormula changed 112"
15.115 + else error "inputFillFormula changed 113";
15.116
16.1 --- a/test/Tools/isac/Interpret/mathengine.sml Tue Oct 18 12:05:03 2016 +0200
16.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Oct 20 10:26:29 2016 +0200
16.3 @@ -643,12 +643,12 @@
16.4 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
16.5 (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
16.6 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
16.7 - (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete;
16.8 + (Rewrite thm') (f',asm) Complete;
16.9 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
16.10 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
16.11 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
16.12 - (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite (thm'_to_thm'' thm')), (f',asm), Complete);
16.13 -existpt p pt andalso get_obj g_tac pt p=Empty_Tac = false;
16.14 + (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
16.15 +existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
16.16 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
16.17 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
16.18 (append_atomic p ist_res f r f' s) : ptree -> ptree;
16.19 @@ -664,7 +664,7 @@
16.20 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
16.21 ID = "rnorm_equation_add";
16.22 @{thm rnorm_equation_add};
16.23 -term2str form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
16.24 +(term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
16.25 (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
16.26 (*thmstr2xml (j+i) form;
16.27 ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
17.1 --- a/test/Tools/isac/Interpret/ptyps.sml Tue Oct 18 12:05:03 2016 +0200
17.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Thu Oct 20 10:26:29 2016 +0200
17.3 @@ -328,15 +328,15 @@
17.4 val nxt = ("Specify_Problem", Specify_Problem ["LINEAR","univariate","equation","test"]);
17.5 (*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
17.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.7 -if f = Form' (PpcKF (0, EdUndef, 0, Nundef, (Problem [],
17.8 - {Find = [Incompl "solutions"], With = [],
17.9 - Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
17.10 - Where = [False ("matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
17.11 - "matches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
17.12 - "matches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\n" ^
17.13 - "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)")],
17.14 - Relate = []}))) then ()
17.15 -else error "--- Refine_Problem broken 1";
17.16 +val www =
17.17 +case f of Form' (PpcKF (0, EdUndef, 0, Nundef, (Problem [],
17.18 + {Find = [Incompl "solutions"], With = [],
17.19 + Given = [Correct "equality ((x + 1) * (x + 2) = x ^^^ 2 + 8)", Correct "solveFor x"],
17.20 + Where = [False www],
17.21 + Relate = [],...}))) => www
17.22 +| _ => error "--- Refine_Problem broken 1";
17.23 +if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) |\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"
17.24 +then () else error "--- Refine_Problem broken 2";
17.25 (*ML> f;
17.26 val it = Form' (PpcKF (0,EdUndef,0,Nundef,
17.27 (Problem ["LINEAR","univariate","equation","test"], <<<<<===== diff.to above WN120313
17.28 @@ -404,8 +404,10 @@
17.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.30 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;
17.31
17.32 -if (snd nxt) = End_Proof' andalso res = "[x = 2]" then ()
17.33 -else error "new behaviour in test:refine.sml:miniscript with mini-subpb";
17.34 +if res = "[x = 2]"
17.35 +then case nxt of ("End_Proof'", End_Proof') => ()
17.36 + | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
17.37 +else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
17.38
17.39 "----------- fun coll_guhs ---------------------------------------";
17.40 "----------- fun coll_guhs ---------------------------------------";
18.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Oct 18 12:05:03 2016 +0200
18.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Oct 20 10:26:29 2016 +0200
18.3 @@ -180,7 +180,7 @@
18.4 "----------- checkContext..Thy_, fun context_thy --------";
18.5 (*using pt from above*)
18.6 val p = ([2,4], Res);
18.7 -val tac = Rewrite ("radd_left_commute", e_term);
18.8 +val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
18.9 checkContext 1 p "thy_Test-thm-radd_left_commute";
18.10 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
18.11 --- in checkContext..Thy_ ---*)
18.12 @@ -190,13 +190,13 @@
18.13 else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
18.14
18.15 val p = ([3,1,1], Frm);
18.16 -val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add", e_term));
18.17 +val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
18.18 checkContext 1 p "thy_Test-thm-risolate_bdv_add";
18.19 (* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
18.20 --- in checkContext..Thy_ ---*)
18.21 val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
18.22 if thm = "thy_isac_Test-thm-risolate_bdv_add"
18.23 - andalso term2str result = "x = 0 + -1 * -1" then ()
18.24 + andalso term2str result = "x = 0 + - 1 * -1" then ()
18.25 else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
18.26
18.27 val p = ([2,5], Res);
18.28 @@ -452,5 +452,3 @@
18.29 | _ => error "get_bdv_subst changed 3";
18.30
18.31 val (SOME subs, _) = get_bdv_subst prog env;
18.32 -Rewrite_Inst (subs, ("diff_sin_chain", e_term)) (*<<<----- this is the intended usage*)
18.33 -
19.1 --- a/test/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
19.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Oct 20 10:26:29 2016 +0200
19.3 @@ -176,8 +176,10 @@
19.4 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
19.5
19.6 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
19.7 -if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", str2term "- qq ?x = Q' ?x"))
19.8 -then () else error "--- WN0509 Substitute 2nd part --- changed";
19.9 +val thm = case nxt of ("Rewrite", Rewrite ("Belastung_Querkraft", thm)) => thm
19.10 +| _ => error "--- WN0509 Substitute 2nd part --- changed 1";
19.11 +if (term2str o Thm.prop_of) thm = "- qq ?x = Q' ?x" then ()
19.12 +else error "--- WN0509 Substitute 2nd part --- changed 2";
19.13
19.14
19.15 "----------- fun sel_appl_atomic_tacs ----------------------------";
19.16 @@ -198,8 +200,8 @@
19.17 case appltacs of
19.18 [Rewrite ("radd_commute", radd_commute),
19.19 Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
19.20 - => if term2str radd_commute = "?m + ?n = ?n + ?m" andalso
19.21 - term2str add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
19.22 + => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
19.23 + (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
19.24 else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
19.25 | _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
19.26
19.27 @@ -395,7 +397,7 @@
19.28
19.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
19.30 val (p'''', pt'''') = (p, pt);
19.31 -f2str f = "x + 1 = 2"; snd nxt = Rewrite_Set "norm_equation";
19.32 +f2str f = "x + 1 = 2"; case snd nxt of Rewrite_Set "norm_equation" => () | _ => error "CHANGED";
19.33 val (p, p_) = p(* = ([1], Frm)*);
19.34 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
19.35 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
19.36 @@ -407,7 +409,8 @@
19.37
19.38 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
19.39 val (p'''', pt'''') = (p, pt);
19.40 -f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify";
19.41 +f2str f = "x + 1 + -1 * 2 = 0";
19.42 +case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
19.43 val (p, p_) = p(* = ([1], Res)*);
19.44 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
19.45 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
19.46 @@ -419,7 +422,9 @@
19.47
19.48 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
19.49 val (p'''', pt'''') = (p, pt);
19.50 -f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]);
19.51 +f2str f = "-1 + x = 0";
19.52 +case snd nxt of Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) => ()
19.53 +| _ => error "CHANGED";
19.54 val (p, p_) = p(* = ([2], Res)*);
19.55 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
19.56 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
19.57 @@ -448,7 +453,8 @@
19.58
19.59 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
19.60 val (p'''', pt'''') = (p, pt);
19.61 -f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv");
19.62 +f2str f = "-1 + x = 0";
19.63 +case snd nxt of Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") => () | _ => error "CHANGED";
19.64 val (p, p_) = p(* = ([3, 1], Frm)*);
19.65 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
19.66 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
19.67 @@ -460,7 +466,8 @@
19.68
19.69 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
19.70 val (p'''', pt'''') = (p, pt);
19.71 -f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify";
19.72 +f2str f = "x = 0 + -1 * -1";
19.73 +case snd nxt of Rewrite_Set "Test_simplify" => () | _ => error "CHANGED";
19.74 val (p, p_) = p(* = ([3, 1], Res)*);
19.75 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
19.76 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
19.77 @@ -488,33 +495,32 @@
19.78
19.79 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
19.80 val tacs = sel_rules pt ([],Pbl);
19.81 - if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
19.82 - else error "script.sml: diff.behav. in sel_rules ([],Pbl)";
19.83 + case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
19.84 + | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
19.85
19.86 val tacs = sel_rules pt ([1],Res);
19.87 - if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.88 + case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.89 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
19.90 - Check_elementwise "Assumptions"] then ()
19.91 - else error "script.sml: diff.behav. in sel_rules ([1],Res)";
19.92 + Check_elementwise "Assumptions"] => ()
19.93 + | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
19.94
19.95 val tacs = sel_rules pt ([3],Pbl);
19.96 - if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
19.97 - else error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
19.98 + case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
19.99 + | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
19.100
19.101 val tacs = sel_rules pt ([3,1],Res);
19.102 - if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
19.103 - Rewrite_Set "Test_simplify"] then ()
19.104 - else error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
19.105 + case tacs of [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
19.106 + | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
19.107
19.108 val tacs = sel_rules pt ([3],Res);
19.109 - if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.110 + case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.111 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
19.112 - Check_elementwise "Assumptions"] then ()
19.113 - else error "script.sml: diff.behav. in sel_rules ([3],Res)";
19.114 + Check_elementwise "Assumptions"] => ()
19.115 + | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
19.116
19.117 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
19.118 - if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
19.119 - else error "script.sml: diff.behav. in sel_rules ([],Res)";
19.120 + case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
19.121 + | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
19.122
19.123 "----------- fun sel_appl_atomic_tacs ----------------------------";
19.124 "----------- fun sel_appl_atomic_tacs ----------------------------";
19.125 @@ -534,10 +540,10 @@
19.126 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
19.127 val ((pt, _), _) = get_calc cI;
19.128 (*version 1:*)
19.129 -if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.130 +case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.131 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
19.132 - Check_elementwise "Assumptions"] then ()
19.133 -else error "fetchApplicableTactics ([1],Res) changed";
19.134 + Check_elementwise "Assumptions"] => ()
19.135 +| _ => error "fetchApplicableTactics ([1],Res) changed";
19.136 (*version 2:*)
19.137 (*WAS:
19.138 sel_appl_atomic_tacs pt p;
20.1 --- a/test/Tools/isac/Knowledge/algein.sml Tue Oct 18 12:05:03 2016 +0200
20.2 +++ b/test/Tools/isac/Knowledge/algein.sml Thu Oct 20 10:26:29 2016 +0200
20.3 @@ -73,9 +73,11 @@
20.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
20.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
20.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.7 -if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
20.8 -else error "algein.sml diff.behav. in erstSymbolisch 99";
20.9 - DEconstrCalcTree 1;
20.10 +if f2str f = "L = 104"
20.11 +then case nxt of ("End_Proof'", End_Proof') => ()
20.12 + | _ => error "algein.sml diff.behav. in erstSymbolisch 99 1"
20.13 +else error "algein.sml diff.behav. in erstSymbolisch 99 2";
20.14 +DEconstrCalcTree 1;
20.15
20.16 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
20.17 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
21.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Tue Oct 18 12:05:03 2016 +0200
21.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Thu Oct 20 10:26:29 2016 +0200
21.3 @@ -429,8 +429,8 @@
21.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.7 -if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
21.8 -then () else error "biegelinie.sml met2 b";
21.9 +case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
21.10 +| _ => error "biegelinie.sml met2 b";
21.11
21.12 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
21.13 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
21.14 @@ -487,9 +487,11 @@
21.15 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
21.16 "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
21.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.18 -if nxt = ("End_Proof'", End_Proof') andalso f2str f =
21.19 - "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]" then ()
21.20 -else error "biegelinie.sml met2 e";
21.21 +if f2str f =
21.22 + "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"
21.23 +then case nxt of ("End_Proof'", End_Proof') => ()
21.24 + | _ => error "biegelinie.sml met2 e 1"
21.25 +else error "biegelinie.sml met2 e 2";
21.26
21.27 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
21.28 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
21.29 @@ -514,11 +516,11 @@
21.30 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
21.31 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
21.32 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
21.33 -if nxt = ("End_Proof'", End_Proof') andalso
21.34 -(* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2"
21.35 -CHANGE NOT considered, already on leave*)
21.36 +if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
21.37 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
21.38 -then () else error "biegelinie.sml: SubProblem (_,[setzeRandbed";
21.39 +then case nxt of ("End_Proof'", End_Proof') => ()
21.40 + | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
21.41 +else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
21.42
21.43
21.44 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
22.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Oct 18 12:05:03 2016 +0200
22.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Oct 20 10:26:29 2016 +0200
22.3 @@ -215,8 +215,10 @@
22.4 "--- 9 ---";
22.5 (*val nxt = ("End_Proof'",End_Proof');*)
22.6 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
22.7 -if nxt = ("End_Proof'",End_Proof') andalso f2str f = "3 + 2 * x" then ()
22.8 -else error "diff.sml: new.behav. in me (*+ tacs input*)";
22.9 +if f2str f = "3 + 2 * x"
22.10 + then case nxt of ("End_Proof'", End_Proof') => ()
22.11 + | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"
22.12 +else error "diff.sml: new.behav. in me (*+ tacs input*) 2";
22.13 (*if f = EmptyMout then () else error "new behaviour in + tacs input";
22.14 meNEW extracts Form once more*)
22.15
22.16 @@ -251,8 +253,8 @@
22.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.20 -if nxt = ("End_Proof'",End_Proof') then ()
22.21 -else error "new behaviour in tests/differentiate, 1.5.02 me from script";
22.22 +case nxt of ("End_Proof'",End_Proof') => ()
22.23 +| _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";
22.24
22.25 "----------- primed id ----------------------------------";
22.26 "----------- primed id ----------------------------------";
23.1 --- a/test/Tools/isac/Knowledge/inssort.sml Tue Oct 18 12:05:03 2016 +0200
23.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Thu Oct 20 10:26:29 2016 +0200
23.3 @@ -109,8 +109,10 @@
23.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.7 -if nxt = ("End_Proof'", End_Proof') andalso f2str f = "{|| 1, 2, 3 ||}" then ()
23.8 -else error "--- insertion sort with MathEngine CHANGED"
23.9 +if f2str f = "{|| 1, 2, 3 ||}"
23.10 +then case nxt of ("End_Proof'", End_Proof') => ()
23.11 + | _ => error "--- insertion sort with MathEngine CHANGED 1"
23.12 +else error "--- insertion sort with MathEngine CHANGED 2";
23.13
23.14 "----------- insertion sort: CAS-command -------------------------------------";
23.15 "----------- insertion sort: CAS-command -------------------------------------";
23.16 @@ -141,8 +143,10 @@
23.17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.18 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("Check_Postcond",..*)
23.19 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("End_Proof'",..*)
23.20 -if nxt = ("End_Proof'", End_Proof') andalso f2str f = "{|| 1, 2, 3 ||}" then ()
23.21 -else error "--- insertion sort: CAS-command CHANGED"
23.22 +if f2str f = "{|| 1, 2, 3 ||}"
23.23 +then case nxt of ("End_Proof'", End_Proof') => ()
23.24 + | _ => error "--- insertion sort: CAS-command CHANGED 1"
23.25 +else error "--- insertion sort: CAS-command CHANGED 2";
23.26
23.27 "----------- insertion sort: met_Prog_sort_ins_steps -------------------------";
23.28 "----------- insertion sort: met_Prog_sort_ins_steps -------------------------";
24.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Tue Oct 18 12:05:03 2016 +0200
24.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Oct 20 10:26:29 2016 +0200
24.3 @@ -244,7 +244,6 @@
24.4
24.5 val (Form f, tac, asms) = pt_extract (pt, p);
24.6 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
24.7 - tac = NONE andalso
24.8 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^
24.9 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^
24.10 "B is_polyexp,A is_polyexp," ^
24.11 @@ -252,8 +251,9 @@
24.12 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^
24.13 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
24.14 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
24.15 -then ()
24.16 - else error "autoCalculate for met_partial_fraction changed: final result"
24.17 +then case tac of NONE => ()
24.18 + | _ => error "autoCalculate for met_partial_fraction changed: final result 1"
24.19 +else error "autoCalculate for met_partial_fraction changed: final result 2"
24.20
24.21 show_pt pt;
24.22 (*[
25.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Tue Oct 18 12:05:03 2016 +0200
25.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Thu Oct 20 10:26:29 2016 +0200
25.3 @@ -251,7 +251,7 @@
25.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
25.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
25.6 val asm = get_assumptions_ pt p;
25.7 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso
25.8 +if f2str f = "[]" andalso
25.9 terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
25.10 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
25.11 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
26.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue Oct 18 12:05:03 2016 +0200
26.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Oct 20 10:26:29 2016 +0200
26.3 @@ -60,7 +60,7 @@
26.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.6
26.7 -nxt = ("Rewrite_Set", Rewrite_Set "RatEq_eliminate");
26.8 +case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
26.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.10 (*
26.11 WN120317.TODO dropped rateq: here "x ~= 0 should go to ctxt, but it does not:
26.12 @@ -91,7 +91,7 @@
26.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.14 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
26.15 f2str f = "[x = 1 / 5]";
26.16 -nxt = ("Check_elementwise", Check_elementwise "Assumptions");
26.17 +case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
26.18 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
26.19 val (pt, p) = case locatetac tac (pt,p) of
26.20 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac";
26.21 @@ -131,7 +131,7 @@
26.22 term2str stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
26.23 "~~~~~ to appy return val:"; val ((a', STac stac)) = ((a', STac stac'));
26.24 val (m,m') = stac2tac_ pt (assoc_thy th) stac;
26.25 -m = Check_elementwise "Assumptions"; (*m' = Empty_Tac_ ???!??? *);
26.26 +case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
26.27 val (p''''', pt''''', m''''') = (p, pt, m);
26.28 "~~~~~ fun applicable_in, args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
26.29 member op = [Pbl,Met] p_; (* = false*)
26.30 @@ -170,8 +170,10 @@
26.31 else error "rateq.sml: new behaviour: [x = 1 / 5]";
26.32 (*WN120317.TODO dropped rateq*)
26.33 ============ inhibit exn WN120316 ==============================================*)
26.34 -if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[]" then ()
26.35 -else error "rateq.sml: new behaviour: [x = 1 / 5]";
26.36 +if p = ([], Res) andalso f2str f = "[]"
26.37 +then case nxt of ("End_Proof'", End_Proof') => ()
26.38 + | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"
26.39 +else error "rateq.sml: new behaviour: [x = 1 / 5] 2"
26.40
26.41 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
26.42 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
26.43 @@ -228,8 +230,8 @@
26.44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.47 -if nxt = ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) then ()
26.48 -else error "55b root specification broken";
26.49 +case nxt of ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) => ()
26.50 +| _ => error "55b root specification broken";
26.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.53 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.54 @@ -237,26 +239,26 @@
26.55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.58 -if nxt = ("Apply_Method", Apply_Method ["PolyEq", "normalize_poly"]) then ()
26.59 -else error "55b normalize_poly specification broken";
26.60 +case nxt of ("Apply_Method", Apply_Method ["PolyEq", "normalize_poly"]) => ()
26.61 +| _ => error "55b normalize_poly specification broken";
26.62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.65 -if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0")) then()
26.66 -else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
26.67 +case f of Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0")) => ()
26.68 +| _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
26.69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.73 -if nxt = ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) then ()
26.74 -else error "55b normalize_poly specification broken";
26.75 +case nxt of ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) => ()
26.76 +| _ => error "55b normalize_poly specification broken";
26.77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.81
26.82 -f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
26.83 -snd nxt = Check_elementwise "Assumptions"; (*= GUI*)
26.84 +f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
26.85 +case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*)
26.86 if terms2str (get_assumptions_ pt p) =
26.87 ("[\"~ matches (?a = 0)\n" ^
26.88 " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^
26.89 @@ -328,6 +330,8 @@
26.90 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
26.91 (*WN120317.TODO dropped rateq*)
26.92 ============ inhibit exn WN120316 ==============================================*)
26.93 -if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[]" then ()
26.94 -else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
26.95 + if p = ([], Res) andalso f2str f = "[]"
26.96 + then case nxt of ("End_Proof'", End_Proof') => ()
26.97 + | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 1"
26.98 + else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 2";
26.99
27.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Oct 18 12:05:03 2016 +0200
27.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Oct 20 10:26:29 2016 +0200
27.3 @@ -79,6 +79,6 @@
27.4 (*----------------------------------------############### changed*)
27.5
27.6 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
27.7 -if nxt = ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"])
27.8 -then () else error "450-nxt-Check_Postcond broken"
27.9 +case nxt of ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
27.10 +| _ => error "450-nxt-Check_Postcond broken"
27.11
28.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Tue Oct 18 12:05:03 2016 +0200
28.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Thu Oct 20 10:26:29 2016 +0200
28.3 @@ -37,6 +37,6 @@
28.4 (*WN110521 worked without testing*)
28.5
28.6 val (p,_,f,nxt,_,pt) = me nxt p''' [] pt'''; (*nxt = Check_elementwise "Assumptions"*)
28.7 -if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()
28.8 -else error "Check_elementwise changed; after switch sub-->root-method";
28.9 +case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()
28.10 +| _ => error "Check_elementwise changed; after switch sub-->root-method";
28.11
29.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Oct 18 12:05:03 2016 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Oct 20 10:26:29 2016 +0200
29.3 @@ -83,5 +83,5 @@
29.4 (*2011 changed ^^^^^ *)
29.5
29.6 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*WAS nxt = ("Empty_Tac", Empty_Tac)*)
29.7 -if nxt = ("Check_elementwise", Check_elementwise "Assumptions") then ()
29.8 -else error "Check_elementwise changed; after switch sub-->root-method";
29.9 +case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => ()
29.10 +| _ => error "Check_elementwise changed; after switch sub-->root-method";
30.1 --- a/test/Tools/isac/Minisubpbl/600-postcond.sml Tue Oct 18 12:05:03 2016 +0200
30.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond.sml Thu Oct 20 10:26:29 2016 +0200
30.3 @@ -32,6 +32,7 @@
30.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30.7 -if nxt = ("End_Proof'", End_Proof') andalso p = ([], Res)
30.8 -andalso get_obj g_res pt (fst p) = str2term "[x=1]" then ()
30.9 -else error "calculation not finished correctly";
30.10 +if p = ([], Res)
30.11 +then case nxt of ("End_Proof'", End_Proof') => ()
30.12 + | _ => error "calculation not finished correctly 1"
30.13 +else error "calculation not finished correctly 2"
31.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Oct 18 12:05:03 2016 +0200
31.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Oct 20 10:26:29 2016 +0200
31.3 @@ -16,7 +16,7 @@
31.4 "----------- fun calculate_ -----------------------------";
31.5 "----------- calculate from script --requires 'setup'----";
31.6 "----------- calculate check test-root-equ --------------";
31.7 -"----------- check calculate bottom up ------------------";
31.8 +"----------- check calcul,ate bottom up -----------------";
31.9 "----------- Atools.pow Power.power_class.power ---------";
31.10 " ================= calculate.sml: calculate_ 2002 ======";
31.11 "----------- get_pair with 3 args -----------------------";
31.12 @@ -102,8 +102,8 @@
31.13 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
31.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
31.15 (*nxt = ("End_Proof'",End_Proof')*)
31.16 -if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
31.17 -else error "calculate.sml: script test_calculate changed behaviour";
31.18 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"16")) => () | _ =>
31.19 +error "calculate.sml: script test_calculate changed behaviour";
31.20
31.21
31.22 "----------- calculate check test-root-equ --------------";
32.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml Tue Oct 18 12:05:03 2016 +0200
32.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Thu Oct 20 10:26:29 2016 +0200
32.3 @@ -113,7 +113,7 @@
32.4 import isac.util.tactics.Tactic
32.5 *)
32.6 Rewrite: thm'' -> tac;
32.7 -val tac = Rewrite("refl", str2term "a = a");
32.8 +val tac = Rewrite("refl", @{thm refl});
32.9 if xmlstr 0 (xml_of_tac tac) =
32.10 (*---xml_of_tac------------------------------------------thm'_to_thm''--------------
32.11 "(REWRITETACTIC name=Rewrite)\n" ^
32.12 @@ -126,7 +126,7 @@
32.13 ". . . . a = a\n" ^
32.14 ". . . (/ISA)\n" ^
32.15 ". . . (TERM)\n" ^
32.16 -". . . . a = a\n" ^
32.17 +". . . . ?t = ?t\n" ^
32.18 ". . . (/TERM)\n" ^
32.19 ". . (/FORMULA)\n" ^
32.20 ". (/THEOREM)\n" ^
32.21 @@ -137,13 +137,13 @@
32.22 ". . . refl\n" ^
32.23 ". . (/ID)\n" ^
32.24 ". . (FORMULA)\n" ^
32.25 -". . . a = a\n" ^
32.26 +". . . ?t = ?t\n" ^
32.27 ". . (/FORMULA)\n" ^
32.28 ". (/THEOREM)\n" ^
32.29 "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
32.30
32.31 Rewrite_Inst: subs * thm'' -> tac;
32.32 -val tac = Rewrite_Inst(["(bdv, x)"], ("refl", str2term "a = a"));
32.33 +val tac = Rewrite_Inst(["(bdv, x)"], ("refl", @{thm refl}));
32.34 if xmlstr 0 (xml_of_tac tac) =
32.35 "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^
32.36 ". (SUBSTITUTION)\n" ^
32.37 @@ -174,7 +174,7 @@
32.38 ". . . . a = a\n" ^
32.39 ". . . (/ISA)\n" ^
32.40 ". . . (TERM)\n" ^
32.41 -". . . . a = a\n" ^
32.42 +". . . ?t = ?t\n" ^
32.43 ". . . (/TERM)\n" ^
32.44 ". . (/FORMULA)\n" ^
32.45 ". (/THEOREM)\n" ^
32.46 @@ -184,7 +184,7 @@
32.47 ". . . refl\n" ^
32.48 ". . (/ID)\n" ^
32.49 ". . (FORMULA)\n" ^
32.50 -". . . a = a\n" ^
32.51 +". . . ?t = ?t\n" ^
32.52 ". . (/FORMULA)\n" ^
32.53 ". (/THEOREM)\n" ^
32.54 "(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";
32.55 @@ -322,14 +322,14 @@
32.56 </VALUE>
32.57 </PAIR>
32.58 </SUBSTITUTION>:*)
32.59 -val tac = Rewrite_Inst (subs, ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"));
32.60 +val tac = Rewrite_Inst (subs, ("diff_sin_chain", @{thm diff_sin_chain}));
32.61 val xml = xml_of_tac tac;
32.62
32.63 if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"
32.64 then () else error "xml_of_tac Rewrite_Inst CHANGED";
32.65
32.66 val Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;
32.67 -if term2str term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
32.68 +if (term2str o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
32.69 then () else error "xml_to_tac Rewrite_Inst CHANGED";
32.70
32.71 val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
32.72 @@ -367,5 +367,5 @@
32.73
32.74 if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"
32.75 then () else error "xml_of_tac Substitute CHANGED";
32.76 -if xml_to_tac xml = Substitute ["bdv_1 = xxx", "bdv_2 = yyy"]
32.77 -then () else error "xml_to_tac Substitute CHANGED";
32.78 \ No newline at end of file
32.79 +case xml_to_tac xml of Substitute ["bdv_1 = xxx", "bdv_2 = yyy"] => ()
32.80 +| _ => error "xml_to_tac Substitute CHANGED";
32.81 \ No newline at end of file
33.1 --- a/test/Tools/isac/xmlsrc/interface-xml.sml Tue Oct 18 12:05:03 2016 +0200
33.2 +++ b/test/Tools/isac/xmlsrc/interface-xml.sml Thu Oct 20 10:26:29 2016 +0200
33.3 @@ -16,7 +16,7 @@
33.4 "----------- fun fetchproposedtacticOK2xml -----------------------";
33.5 "----------- fun fetchproposedtacticOK2xml -----------------------";
33.6 "----------- fun fetchproposedtacticOK2xml -----------------------";
33.7 -fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", str2term "?m *?n =?n *?m"));
33.8 +fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", @{thm "rmult_commute"}));
33.9 (*
33.10 @@@@@begin@@@@@
33.11 11