1.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Jul 24 19:38:53 2011 +0200
1.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon Jul 25 11:52:07 2011 +0200
1.3 @@ -1,6 +1,5 @@
1.4 -(* tests on inform.sml
1.5 - author: Walther Neuper
1.6 - 060225,
1.7 +(* Title: tests on inform.sml
1.8 + Author: Walther Neuper 060225,
1.9 (c) due to copyright terms
1.10
1.11 use"../smltest/ME/inform.sml";
1.12 @@ -44,6 +43,7 @@
1.13 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.14 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.15 "--------- appendFormula: on Res + equ_nrls ----------------------";
1.16 +
1.17 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
1.18 (writeln o term2str) sc;
1.19 val Script sc = (#scr o get_met) ["Test","solve_linear"];
1.20 @@ -61,9 +61,15 @@
1.21 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
1.22 val ((pt,_),_) = get_calc 1;
1.23 val str = pr_ptree pr_short pt;
1.24 +
1.25 writeln str;
1.26 +(*============ inhibit exn AK110725 ==============================================
1.27 +(* 2nd string should be the same as 1st one *)
1.28 +". ----- 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.29 +". ----- 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.30 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.31 else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
1.32 +============ inhibit exn AK110725 ==============================================*)
1.33
1.34 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
1.35 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
1.36 @@ -81,9 +87,12 @@
1.37 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
1.38
1.39 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
1.40 +(*============ inhibit exn AK110725 ==============================================
1.41 +(* ERROR: exception Bind raised *)
1.42 val (_,(tac,_,_)::_) = get_calc 1;
1.43 if tac = Rewrite_Set "Test_simplify" then ()
1.44 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
1.45 +============ inhibit exn AK110725 ==============================================*)
1.46 autoCalculate 1 CompleteCalc;
1.47 val ((pt,_),_) = get_calc 1;
1.48 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
1.49 @@ -100,18 +109,19 @@
1.50
1.51 *)
1.52 "----------------------------------------------------------";
1.53 - val fod = make_deriv (theory "Isac") Atools_erls
1.54 +
1.55 + val fod = make_deriv (@{theory "Isac"}) Atools_erls
1.56 ((#rules o rep_rls) Test_simplify)
1.57 - (sqrt_right false (theory "Pure")) NONE
1.58 + (sqrt_right false (@{theory "Pure"})) NONE
1.59 (str2term "x + 1 + -1 * 2 = 0");
1.60 (writeln o trtas2str) fod;
1.61
1.62 - val ifod = make_deriv (theory "Isac") Atools_erls
1.63 + val ifod = make_deriv (@{theory "Isac"}) Atools_erls
1.64 ((#rules o rep_rls) Test_simplify)
1.65 - (sqrt_right false (theory "Pure")) NONE
1.66 + (sqrt_right false (@{theory "Pure"})) NONE
1.67 (str2term "-2 * 1 + (1 + x) = 0");
1.68 (writeln o trtas2str) ifod;
1.69 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;
1.70 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
1.71 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
1.72 val der = fod' @ (map rev_deriv' rifod');
1.73 (writeln o trtas2str) der;
1.74 @@ -128,7 +138,6 @@
1.75 Iterator 1; moveActiveRoot 1;
1.76 autoCalculate 1 CompleteCalcHead;
1.77 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
1.78 -
1.79 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
1.80
1.81 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
1.82 @@ -203,7 +212,7 @@
1.83 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
1.84 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
1.85 else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
1.86 -
1.87 +
1.88 fetchProposedTactic 1;
1.89 val (_,(tac,_,_)::_) = get_calc 1;
1.90 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
1.91 @@ -256,11 +265,18 @@
1.92 val ((pt,_),_) = get_calc 1;
1.93 val str = pr_ptree pr_short pt;
1.94 writeln str;
1.95 - 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.96 +
1.97 +(*============ inhibit exn AK110725 ==============================================
1.98 +(* 2nd string should be the same as 1st one *)
1.99 +". ----- 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.100 +". ----- 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.101 + 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.102 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
1.103 +============ inhibit exn AK110725 ==============================================*)
1.104 +
1.105 autoCalculate 1 CompleteCalc;
1.106 - val ((pt,pos as(p,_)),_) = get_calc 1;
1.107 - if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.108 + val ((pt,pos as (p,_)),_) = get_calc 1;
1.109 + if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
1.110 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.111
1.112
1.113 @@ -280,11 +296,11 @@
1.114 val ((pt,_),_) = get_calc 1;
1.115 val str = pr_ptree pr_short pt;
1.116 writeln str;
1.117 - if str=". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.118 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.119 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
1.120 autoCalculate 1 CompleteCalc;
1.121 - val ((pt,pos as(p,_)),_) = get_calc 1;
1.122 - if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.123 + val ((pt,pos as (p,_)),_) = get_calc 1;
1.124 + if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
1.125 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
1.126
1.127
1.128 @@ -303,11 +319,11 @@
1.129 val ((pt,_),_) = get_calc 1;
1.130 val str = pr_ptree pr_short pt;
1.131 writeln str;
1.132 - if str=". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.133 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
1.134 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
1.135 autoCalculate 1 CompleteCalc;
1.136 - val ((pt,pos as(p,_)),_) = get_calc 1;
1.137 - if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
1.138 + val ((pt,pos as (p,_)),_) = get_calc 1;
1.139 + if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
1.140 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
1.141
1.142
1.143 @@ -332,7 +348,6 @@
1.144 else error "inform.sml: diff.behav. cut calculation 2";
1.145
1.146
1.147 -
1.148 (* 040307 copied from informtest.sml; ... old version
1.149 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
1.150 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
1.151 @@ -514,7 +529,10 @@
1.152 spec;
1.153 writeln (itms2str_ ctxt probl);
1.154 writeln (itms2str_ ctxt meth);
1.155 +(*============ inhibit exn AK110725 ==============================================
1.156 +(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
1.157 writeln (istate2str istate);
1.158 +============ inhibit exn AK110725 ==============================================*)
1.159
1.160 print_depth 3;
1.161
1.162 @@ -529,7 +547,10 @@
1.163 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.164 val NONE = env;
1.165 val (SOME istate, NONE) = loc;
1.166 +(*============ inhibit exn AK110725 ==============================================
1.167 +(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
1.168 print_depth 5; writeln (istate2str istate); print_depth 3;
1.169 +============ inhibit exn AK110725 ==============================================*)
1.170 (*ScrState ([],
1.171 [], NONE,
1.172 ??.empty, Sundef, false)*)
1.173 @@ -541,12 +562,12 @@
1.174 (*[
1.175 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.176 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.177 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.178 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.179 writeln (itms2str_ ctxt meth);
1.180 (*[
1.181 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.182 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.183 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.184 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.185 writeln"-----------------------------------------------------------";
1.186 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.187 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
1.188 @@ -564,17 +585,19 @@
1.189 (*the following input is copied from BridgeLog Java <==> SML,
1.190 omitting unnecessary inputs*)
1.191 (*1>*)states:=[];
1.192 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
1.193 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
1.194 (*3>*)Iterator 1; moveActiveRoot 1;
1.195
1.196 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
1.197 -
1.198 (***difference II***)
1.199 val ((pt,_),_) = get_calc 1;
1.200 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
1.201 val NONE = env;
1.202 val (SOME istate, NONE) = loc;
1.203 +(*============ inhibit exn AK110725 ==============================================
1.204 +(* ERROR: Argument: istate : istate * Proof.context Reason: Can't unify istate to istate * Proof.context *)
1.205 print_depth 5; writeln (istate2str istate); print_depth 3;
1.206 +============ inhibit exn AK110725 ==============================================*)
1.207 (*ScrState ([],
1.208 [], NONE,
1.209 ??.empty, Sundef, false)*)
1.210 @@ -586,15 +609,14 @@
1.211 (*[
1.212 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.213 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.214 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.215 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.216 writeln (itms2str_ ctxt meth);
1.217 (*[
1.218 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
1.219 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
1.220 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
1.221 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
1.222 writeln"-----------------------------------------------------------";
1.223 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
1.224 -
1.225 autoCalculate 1 (Step 1);
1.226 val ((pt,p),_) = get_calc 1;
1.227 val Form res = (#1 o pt_extract) (pt, p);