1.1 --- a/test/Tools/isac/Interpret/calchead.sml Wed Oct 06 15:12:41 2010 +0200
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Fri Oct 08 18:51:23 2010 +0200
1.3 @@ -16,6 +16,7 @@
1.4 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.5 "--------- regression test fun is_copy_named ------------";
1.6 "--------- regr.test fun cpy_nam ------------------------";
1.7 +"--------- check specify phase --------------------------";
1.8 "--------------------------------------------------------";
1.9 "--------------------------------------------------------";
1.10 "--------------------------------------------------------";
1.11 @@ -326,6 +327,8 @@
1.12
1.13 ============ inhibit exn =====================================================*)
1.14
1.15 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.16 +
1.17 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.18 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.19 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
1.20 @@ -393,32 +396,32 @@
1.21 val ags = isalist2list ags';
1.22 val pI = ["linear","system"];
1.23 val pats = (#ppc o get_pbt) pI;
1.24 -(*===inhibit exn provided by this testcase==========================
1.25 -val xxx = match_ags (theory "EqSystem") pats ags;
1.26 -===================================================================*)
1.27 +(*---inhibit exn provided by this testcase--------------------------
1.28 +val xxx - match_ags (theory "EqSystem") pats ags;
1.29 +-------------------------------------------------------------------*)
1.30 "-c1-----------------------------------------------------";
1.31 "--------------------------step through code match_ags---";
1.32 val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags);
1.33 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.34 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
1.35 val cy = filter is_copy_named pbt; (*=solution*)
1.36 -(*===inhibit exn provided by this testcase==========================
1.37 - val oris' = matc thy pbt' ags [];
1.38 -===================================================================*)
1.39 +(*---inhibit exn provided by this testcase--------------------------
1.40 + val oris' - matc thy pbt' ags [];
1.41 +-------------------------------------------------------------------*)
1.42 "-------------------------------step through code matc---";
1.43 val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);
1.44 (is_copy_named_idstr o free2str) t;
1.45 "---if False:...";
1.46 -(*===inhibit exn provided by this testcase==========================
1.47 -val opt = mtc thy p a;
1.48 -===================================================================*)
1.49 +(*---inhibit exn provided by this testcase--------------------------
1.50 +val opt - mtc thy p a;
1.51 +-------------------------------------------------------------------*)
1.52 "--------------------------------step through code mtc---";
1.53 -val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
1.54 +val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a);
1.55 cterm_of;
1.56 -val ttt = (dsc $ var);
1.57 -(*===inhibit exn provided by this testcase==========================
1.58 +val ttt - (dsc $ var);
1.59 +(*---inhibit exn provided by this testcase--------------------------
1.60 cterm_of thy (dsc $ var);
1.61 -===================================================================*)
1.62 +-------------------------------------------------------------------*)
1.63 "-------------------------------------step through end---";
1.64
1.65 case ((match_ags (theory "EqSystem") pats ags)
1.66 @@ -568,3 +571,152 @@
1.67 case cpy_nam pbt oris (hd cy) of
1.68 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => ()
1.69 | _ => error "calchead.sml regr.test cpy_nam-2-";
1.70 +
1.71 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.72 +
1.73 +
1.74 +"--------- check specify phase --------------------------";
1.75 +"--------- check specify phase --------------------------";
1.76 +"--------- check specify phase --------------------------";
1.77 +(*val fmz = ["functionTerm (x^^^2 + 1)",*)
1.78 +val fmz = ["functionTerm (x + 1)",
1.79 + "integrateBy x","antiDerivative FF"];
1.80 +val (dI',pI',mI') =
1.81 + ("Integrate",["integrate","function"],
1.82 + ["diff","integration"]);
1.83 +val p = e_pos'; val c = [];
1.84 +"--- step 1 --";
1.85 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.86 +(*> val it = "--- step 1 --" : string
1.87 +val f =
1.88 + Form'
1.89 + (PpcKF
1.90 + (0, EdUndef, 0, Nundef,
1.91 + (Problem [],
1.92 + {Find = [], With = [], Given = [], Where = [], Relate = []})))
1.93 +: mout
1.94 +val nxt = ("Model_Problem", Model_Problem) : string * tac
1.95 +val p = ([], Pbl) : pos'
1.96 +val pt =
1.97 + Nd (PblObj
1.98 + {env = None, fmz =
1.99 + (["functionTerm (x^^^2 + 1)", "integrateBy x",
1.100 + "antiDerivative FF"],
1.101 + ("Integrate.thy", ["integrate", "function"],
1.102 + ["diff", "integration"])),
1.103 + loc =
1.104 + (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
1.105 + None),
1.106 + cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
1.107 + probl = [], branch = TransitiveB,
1.108 + origin =
1.109 + ([(1, [1], "#Given",
1.110 + Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
1.111 + [Const ("op +",
1.112 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.113 + (Const ("Atools.pow",
1.114 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.115 + Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.116 + Free ("1", "RealDef.real")]),
1.117 + (2, [1], "#Given",
1.118 + Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
1.119 + [Free ("x", "RealDef.real")]),
1.120 + (3, [1], "#Find",
1.121 + Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
1.122 + [Free ("FF", "RealDef.real")])],
1.123 + ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
1.124 + Const ("Integrate.Integrate",
1.125 + "(RealDef.real, RealDef.real) * => RealDef.real") $
1.126 + (Const ("Pair",
1.127 + "[RealDef.real, RealDef.real]
1.128 + => (RealDef.real, RealDef.real) *") $
1.129 + (Const ("op +",
1.130 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.131 + (Const ("Atools.pow",
1.132 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.133 + Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.134 + Free ("1", "RealDef.real")) $
1.135 + Free ("x", "RealDef.real"))),
1.136 + ostate = Incomplete, result = (Const ("empty", "'a"), [])},
1.137 + []) : ptree*)
1.138 +"----- WN101007 worked until here (checked same as isac2002) ---";
1.139 +"--- step 2 --";
1.140 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*)
1.141 +(*val it = "--- step 2 --" : string
1.142 +val p = ([], Pbl) : pos'
1.143 +val f =
1.144 + Form'
1.145 + (PpcKF
1.146 + (0, EdUndef, 0, Nundef,
1.147 + (Problem [],
1.148 + {Find = [Incompl "Integrate.antiDerivative"],
1.149 + With = [],
1.150 + Given = [Incompl "functionTerm", Incompl "integrateBy"],
1.151 + Where = [],
1.152 + Relate = []}))) : mout
1.153 +val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_
1.154 +val pt =
1.155 + Nd (PblObj
1.156 + {env = None, fmz =
1.157 + (["functionTerm (x^^^2 + 1)", "integrateBy x",
1.158 + "antiDerivative FF"],
1.159 + ("Integrate.thy", ["integrate", "function"],
1.160 + ["diff", "integration"])),
1.161 + loc =
1.162 + (Some
1.163 + (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
1.164 + None),
1.165 + cell = None, meth = [], spec =
1.166 + ("e_domID", ["e_pblID"], ["e_metID"]), probl =
1.167 + [(0, [], false, "#Given",
1.168 + Inc ((Const ("Descript.functionTerm",
1.169 + "RealDef.real => Tools.una"),[]),
1.170 + (Const ("empty", "'a"), []))),
1.171 + (0, [], false, "#Given",
1.172 + Inc ((Const ("Integrate.integrateBy",
1.173 + "RealDef.real => Tools.una"),[]),
1.174 + (Const ("empty", "'a"), []))),
1.175 + (0, [], false, "#Find",
1.176 + Inc ((Const ("Integrate.antiDerivative",
1.177 + "RealDef.real => Tools.una"),[]),
1.178 + (Const ("empty", "'a"), [])))],
1.179 + branch = TransitiveB, origin =
1.180 + ([(1, [1], "#Given",
1.181 + Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
1.182 + [Const ("op +",
1.183 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.184 + (Const ("Atools.pow",
1.185 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.186 + Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.187 + Free ("1", "RealDef.real")]),
1.188 + (2, [1], "#Given",
1.189 + Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
1.190 + [Free ("x", "RealDef.real")]),
1.191 + (3, [1], "#Find",
1.192 + Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
1.193 + [Free ("FF", "RealDef.real")])],
1.194 + ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
1.195 + Const ("Integrate.Integrate",
1.196 + "(RealDef.real, RealDef.real) * => RealDef.real") $
1.197 + (Const ("Pair",
1.198 + "[RealDef.real, RealDef.real]
1.199 + => (RealDef.real, RealDef.real) *") $
1.200 + (Const ("op +",
1.201 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.202 + (Const ("Atools.pow",
1.203 + "[RealDef.real, RealDef.real] => RealDef.real") $
1.204 + Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.205 + Free ("1", "RealDef.real")) $
1.206 + Free ("x", "RealDef.real"))),
1.207 + ostate = Incomplete, result = (Const ("empty", "'a"), [])},
1.208 + []) : ptree*)
1.209 +"----- WN101007 ptree checked same as isac2002, diff. in nxt ---";
1.210 +
1.211 +
1.212 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.213 +nxt_specif_additem "#Given" ;
1.214 +
1.215 +
1.216 +"--- step 3 --";
1.217 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.218 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)