1.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Jun 30 17:27:34 2013 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Jul 11 16:58:31 2013 +0200
1.3 @@ -35,7 +35,9 @@
1.4 "--------- build fun check_err_patt ?bdv -------------------------";
1.5 "--------- build fun check_error_patterns ------------------------";
1.6 "--------- embed fun check_error_patterns ------------------------";
1.7 +"--------- build fun get_fillpats --------------------------------";
1.8 "--------- embed fun find_fillpatterns ---------------------------";
1.9 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
1.10 "-----------------------------------------------------------------";
1.11 "-----------------------------------------------------------------";
1.12 "-----------------------------------------------------------------";
1.13 @@ -44,7 +46,6 @@
1.14 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.15 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.16 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.17 -
1.18 val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
1.19 (writeln o term2str) sc;
1.20 val Prog sc = (#scr o get_met) ["Test","solve_linear"];
1.21 @@ -62,15 +63,17 @@
1.22 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.23 val ((pt,_),_) = get_calc 1;
1.24 val str = pr_ptree pr_short pt;
1.25 -
1.26 - writeln str;
1.27 -(*============ inhibit exn AK110726 ==============================================
1.28 -(* 2nd string should be the same as 1st one *)
1.29 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. 1 + x + -1 * 2 = 0\n2.3. 1 + (x + -1 * 2) = 0\n2.4. 1 + (x + -2) = 0\n2.5. 1 + (x + -2 * 1) = 0\n2.6. 1 + x + -2 * 1 = 0\n";
1.30 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n";
1.31 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then ()
1.32 - else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
1.33 -============ inhibit exn AK110726 ==============================================*)
1.34 +if str =
1.35 +(". ----- pblobj -----\n" ^
1.36 +"1. x + 1 = 2\n" ^
1.37 +"2. x + 1 + -1 * 2 = 0\n" ^
1.38 +"2.1. x + 1 + -1 * 2 = 0\n" ^
1.39 +"2.2. 1 + x + -1 * 2 = 0\n" ^
1.40 +"2.3. 1 + (x + -1 * 2) = 0\n" ^
1.41 +"2.4. 1 + (x + -2) = 0\n" ^
1.42 +"2.5. 1 + (x + -2 * 1) = 0\n" ^
1.43 +"2.6. 1 + x + -2 * 1 = 0\n" ) then ()
1.44 +else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
1.45
1.46 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
1.47 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
1.48 @@ -88,13 +91,12 @@
1.49 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
1.50
1.51 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.52 -
1.53 -(*============ inhibit exn AK110725 ==============================================
1.54 -(* ERROR: exception Bind raised *)
1.55 +(* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
1.56 +(*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
1.57 val (_,(tac,_,_)::_) = get_calc 1;
1.58 if tac = Rewrite_Set "Test_simplify" then ()
1.59 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
1.60 -============ inhibit exn AK110725 ==============================================*)
1.61 +============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
1.62
1.63 autoCalculate 1 CompleteCalc;
1.64 val ((pt,_),_) = get_calc 1;
1.65 @@ -267,21 +269,34 @@
1.66 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.67 val ((pt,_),_) = get_calc 1;
1.68 val str = pr_ptree pr_short pt;
1.69 - writeln str;
1.70
1.71 -(*============ inhibit exn AK110725 ==============================================
1.72 -(* 2nd string should be the same as 1st one *)
1.73 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. 1 + x + -1 * 2 = 0\n2.3. 1 + (x + -1 * 2) = 0\n2.4. 1 + (x + -2) = 0\n2.5. 1 + (x + -2 * 1) = 0\n2.6. 1 + x + -2 * 1 = 0\n";
1.74 -". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n";
1.75 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then()
1.76 - else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.77 -============ inhibit exn AK110725 ==============================================*)
1.78 +(* before AK110725 this was
1.79 +". ----- pblobj -----\n
1.80 +1. x + 1 = 2\n
1.81 +2. x + 1 + -1 * 2 = 0\n
1.82 +2.1. x + 1 + -1 * 2 = 0\n
1.83 +2.2. 1 + x + -1 * 2 = 0\n
1.84 +2.3. 1 + (x + -1 * 2) = 0\n
1.85 +2.4. 1 + (x + -2) = 0\n
1.86 +2.5. 1 + (x + -2 * 1) = 0\n
1.87 +2.6. 1 + x + -2 * 1 = 0\n";
1.88 +*)
1.89 +if str =
1.90 +". ----- pblobj -----\n"^
1.91 +"1. x + 1 = 2\n"^
1.92 +"2. x + 1 + -1 * 2 = 0\n"^
1.93 +"2.1. x + 1 + -1 * 2 = 0\n"^
1.94 +"2.2. 1 + x + -1 * 2 = 0\n"^
1.95 +"2.3. 1 + (x + -1 * 2) = 0\n"^
1.96 +"2.4. 1 + (x + -2) = 0\n"^
1.97 +"2.5. 1 + (x + -2 * 1) = 0\n"^
1.98 +"2.6. 1 + x + -2 * 1 = 0\n" then()
1.99 +else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.100
1.101 autoCalculate 1 CompleteCalc;
1.102 val ((pt,pos as (p,_)),_) = get_calc 1;
1.103 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
1.104 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.105 -
1.106
1.107 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.108 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
1.109 @@ -532,14 +547,7 @@
1.110 spec;
1.111 writeln (itms2str_ ctxt probl);
1.112 writeln (itms2str_ ctxt meth);
1.113 -
1.114 -(*============ inhibit exn AK110725 ==============================================
1.115 -(* ERROR: Argument: istate : istate * Proof.context Reason:
1.116 - Can't unify istate to istate * Proof.context *)
1.117 -writeln (istate2str istate);
1.118 -============ inhibit exn AK110725 ==============================================*)
1.119 -
1.120 -print_depth 3;
1.121 +writeln (istate2str (fst istate));
1.122
1.123 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
1.124 (*081016 NOT necessary (but leave it in Java):*)
1.125 @@ -552,10 +560,7 @@
1.126 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.127 val NONE = env;
1.128 val (SOME istate, NONE) = loc;
1.129 -(*============ inhibit exn AK110725 ==============================================
1.130 -(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
1.131 -print_depth 5; writeln (istate2str istate); print_depth 3;
1.132 -============ inhibit exn AK110725 ==============================================*)
1.133 +print_depth 5; writeln (istate2str (fst istate)); print_depth 3;
1.134 (*ScrState ([],
1.135 [], NONE,
1.136 ??.empty, Sundef, false)*)
1.137 @@ -583,7 +588,6 @@
1.138 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
1.139 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
1.140
1.141 -
1.142 "--------- Take as 1st tac, start from exp -----------------------";
1.143 "--------- Take as 1st tac, start from exp -----------------------";
1.144 "--------- Take as 1st tac, start from exp -----------------------";
1.145 @@ -599,10 +603,7 @@
1.146 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.147 val NONE = env;
1.148 val (SOME istate, NONE) = loc;
1.149 -(*============ inhibit exn AK110725 ==============================================
1.150 -(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
1.151 -print_depth 5; writeln (istate2str istate); print_depth 3;
1.152 -============ inhibit exn AK110725 ==============================================*)
1.153 +print_depth 5; writeln (istate2str (fst istate)); print_depth 3;
1.154 (*ScrState ([],
1.155 [], NONE,
1.156 ??.empty, Sundef, false)*)
1.157 @@ -628,7 +629,6 @@
1.158 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
1.159 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
1.160
1.161 -
1.162 "--------- init_form, start with <NEW> (CAS input) ---------------";
1.163 "--------- init_form, start with <NEW> (CAS input) ---------------";
1.164 "--------- init_form, start with <NEW> (CAS input) ---------------";
1.165 @@ -887,14 +887,11 @@
1.166 parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.167 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
1.168 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
1.169 -
1.170 case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
1.171 | NONE => error "check_error_patterns broken";
1.172
1.173 -
1.174 "--------- embed fun check_error_patterns ------------------------";
1.175 "--------- embed fun check_error_patterns ------------------------";
1.176 -(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1.177 "--------- embed fun check_error_patterns ------------------------";
1.178 states:=[];
1.179 CalcTree
1.180 @@ -954,6 +951,65 @@
1.181 ("error pattern #chain-rule-diff-both#", calcstate') => ()
1.182 | _ => error "inform with (positive) check_error_patterns broken"
1.183
1.184 +"--------- build fun get_fillpats --------------------------------";
1.185 +"--------- build fun get_fillpats --------------------------------";
1.186 +"--------- build fun get_fillpats --------------------------------";
1.187 +(*cause for this test was: wrong thy in Build_Thydata.thy in
1.188 + insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)
1.189 +val f_curr = str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
1.190 +val errpatID = "chain-rule-diff-both"
1.191 + val {errpats, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
1.192 +val env =
1.193 + [(str2term "f_f", str2term "x ^^^ 2 + sin (x ^^^ 4)"),
1.194 + (str2term "v_v", str2term "x"),
1.195 + (str2term "f_f'", str2term "d_d x (x ^^^ 2 + sin (x ^^^ 4))")]
1.196 + val subst = get_bdv_subst prog env
1.197 + val errpatthms = errpats
1.198 + |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
1.199 + |> map (#3: errpat -> thm list)
1.200 + |> flat;
1.201 +"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
1.202 + (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
1.203 + val thmDeriv = Thm.get_name_hint thm
1.204 + val (part, thyID) = thy_containing_thm thmDeriv
1.205 + val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
1.206 + val Hthm {fillpats, ...} = get_the theID
1.207 + val some = map (get_fillform subst (thm, form) errpatID) fillpats;
1.208 +"~~~~~ fun get_fillform, args:";
1.209 + val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
1.210 + (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
1.211 + val (form', _, _, rewritten) =
1.212 + rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
1.213 +"~~~~~ fun rew_sub, args:"; val (thy, i, bdv, tless, rls, put_asm, lrd:lrd list, r, t) =
1.214 + ((Isac()), 1, subst, e_rew_ord, e_rls, false, [], (Trueprop $ pat), form);
1.215 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
1.216 + o Logic.strip_imp_concl) r;
1.217 +(*/-------------catch the planned exception*)
1.218 +(let
1.219 + val r' = Envir.subst_term (Pattern.match thy (lhs, t)
1.220 + (Vartab.empty, Vartab.empty)) r;
1.221 +in 111 end
1.222 +) handle PATTERN (*because only a subterm matches*) => 111;
1.223 +case t of t1 $ t2 =>
1.224 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
1.225 + in
1.226 + if rew2 then (t1 $ t2', asm2, lrd, true) else
1.227 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
1.228 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
1.229 + end;
1.230 +(*catch the planned exception-------------/*)
1.231 +
1.232 +val t1 $ t2 = t;
1.233 +val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2;
1.234 +"~~~~~ fun rew_sub, args:"; val (thy, i, bdv, tless, rls, put_asm, lrd:lrd list, r, t) =
1.235 + (thy, i, bdv, tless, rls, put_asm, (lrd@[R]), r, t2);
1.236 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
1.237 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
1.238 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
1.239 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r';
1.240 +if term2str t' = "cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
1.241 + else error "get_fillpats changed 1"
1.242 +
1.243 "--------- embed fun find_fillpatterns ---------------------------";
1.244 "--------- embed fun find_fillpatterns ---------------------------";
1.245 "--------- embed fun find_fillpatterns ---------------------------";
1.246 @@ -977,7 +1033,7 @@
1.247 "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
1.248 val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
1.249 val pp = par_pblobj pt p
1.250 - val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
1.251 + val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
1.252 val ScrState (env, _, _, _, _, _) = get_istate pt pos
1.253 val subst = get_bdv_subst prog env
1.254 val errpatthms = errpats
1.255 @@ -1036,7 +1092,6 @@
1.256 ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
1.257 then () else error "find_fillpatterns changed 4b";
1.258
1.259 -
1.260 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.261 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.262 "--------- build fun is_exactly_equal, inputFillFormula ----------";
1.263 @@ -1117,5 +1172,6 @@
1.264 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1.265 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
1.266 then () else error "inputFillFormula changed 11";
1.267 +(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1.268 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1.269