1.1 --- a/src/Tools/isac/ProgLang/Tools.thy Wed Jul 27 13:05:27 2011 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Thu Jul 28 11:27:04 2011 +0200
1.3 @@ -64,9 +64,9 @@
1.4 (tracing"### or2list _ = _";list2isalist bool [t])
1.5 | or2list ors =
1.6 (tracing"### or2list _ | _";
1.7 - let fun get ls (Const ("op |",_) $ o1 $ o2) =
1.8 + let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
1.9 case o2 of
1.10 - Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
1.11 + Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
1.12 | _ => ls @ [o1, o2]
1.13 in (((list2isalist bool) o (get [])) ors)
1.14 handle _ => error ("or2list: no ORs= "^(term2str ors)) end
2.1 --- a/test/Tools/isac/Frontend/interface.sml Wed Jul 27 13:05:27 2011 +0200
2.2 +++ b/test/Tools/isac/Frontend/interface.sml Thu Jul 28 11:27:04 2011 +0200
2.3 @@ -729,11 +729,9 @@
2.4 setNextTactic 1 (Model_Problem );
2.5 (*..this tactic should be done 'tacitly', too !*)
2.6
2.7 -(*
2.8 autoCalculate 1 CompleteCalcHead;
2.9 checkContext 1 ([],Pbl) "pbl_equ_univ";
2.10 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.11 -*)
2.12
2.13 autoCalculate 1 (Step 1);
2.14
2.15 @@ -796,11 +794,8 @@
2.16 show_pt pt;
2.17 val p = get_pos 1 1;
2.18 val (Form f, tac, asms) = pt_extract (pt, p);
2.19 -(*========== inhibit exn 110719 ================================================
2.20 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.21 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.22 -========== inhibit exn 110719 ================================================*)
2.23 -
2.24 (*------------^^^-inserted-----------------------------------------------*)
2.25 (*WN050904 the fetchProposedTactic's below may not have worked like that
2.26 before, too, because there was no check*)
2.27 @@ -820,13 +815,10 @@
2.28 rootthy pt;
2.29 show_pt pt;
2.30 val p = get_pos 1 1;
2.31 -(*============ inhibit exn AK110719 ==============================================
2.32 -(* ERROR: execption Bind raised *)
2.33 val (Form f, tac, asms) = pt_extract (pt, p);
2.34 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.35 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.36 -============ inhibit exn AK110719 ==============================================*)
2.37 -DEconstrCalcTree 1;
2.38 +DEconstrCalcTree 1;
2.39
2.40 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
2.41 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.1 --- a/test/Tools/isac/Interpret/mathengine.sml Wed Jul 27 13:05:27 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Jul 28 11:27:04 2011 +0200
3.3 @@ -16,6 +16,7 @@
3.4 "----------- fun autocalc -------------------------------";
3.5 "----------- fun autoCalculate --------------------------";
3.6 "----------- fun autoCalculate..CompleteCalc ------------";
3.7 +"----------- search for Or_to_List ----------------------";
3.8 "--------------------------------------------------------";
3.9 "--------------------------------------------------------";
3.10 "--------------------------------------------------------";
3.11 @@ -424,5 +425,48 @@
3.12 then () else error "autoCalculate..CompleteCalc: ctxt at final result";
3.13
3.14
3.15 +"----------- search for Or_to_List ----------------------";
3.16 +"----------- search for Or_to_List ----------------------";
3.17 +"--------- search for Or_to_List ------------------------";
3.18 +val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
3.19 +val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
3.20 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
3.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.41 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) =
3.42 + (nxt, p, [], pt);
3.43 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
3.44 +val (pt, p) = ptp;
3.45 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
3.46 + (p, ((pt, e_pos'),[]));
3.47 +val pIopt = get_pblID (pt,ip);
3.48 +ip = ([],Res); (*false*)
3.49 +ip = p; (*false*)
3.50 +member op = [Pbl,Met] p_; (*false*)
3.51 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
3.52 +e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
3.53 +val thy' = get_obj g_domID pt (par_pblobj pt p);
3.54 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.55 +val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
3.56 +case tac_ of Or_to_List' _ => ()
3.57 +| _ => error "Or_to_List broken ?"
3.58
3.59
4.1 --- a/test/Tools/isac/ProgLang/tools.sml Wed Jul 27 13:05:27 2011 +0200
4.2 +++ b/test/Tools/isac/ProgLang/tools.sml Thu Jul 28 11:27:04 2011 +0200
4.3 @@ -8,6 +8,7 @@
4.4 "table of contents -----------------------------------------------";
4.5 "-----------------------------------------------------------------";
4.6 "----------- fun matchsub ----------------------------------------";
4.7 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -22,3 +23,19 @@
4.12 if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
4.13 then () else error "tools.sml matchsub (a + (b + c)) + d";
4.14
4.15 +
4.16 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.17 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.18 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.19 +"see: --------- search for Or_to_List ---";
4.20 +case or2list HOLogic.true_const of Const ("Tools.UniversalList", _) => ()
4.21 + | _ => error "Tools.UniversalList changed";
4.22 +case or2list HOLogic.false_const of Const ("List.list.Nil", _) => ()
4.23 + | _ => error "Tools.UniversalList changed";
4.24 +val t = (str2term "x=3");
4.25 +if term2str (or2list t) = "[x = 3]" then ()
4.26 +else error "or2list changed";
4.27 +val t = (str2term "x=3 | x=-3 | x=0");
4.28 +if term2str (or2list t) = "[x = 3, x = -3, x = 0]" then ()
4.29 +else error "HOL.eq ? HOL.disj ? changed";
4.30 +
5.1 --- a/test/Tools/isac/Test_Isac.thy Wed Jul 27 13:05:27 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jul 28 11:27:04 2011 +0200
5.3 @@ -100,11 +100,11 @@
5.4 use "library.sml"
5.5 use "calcelems.sml"
5.6 use "ProgLang/termC.sml"
5.7 - use "ProgLang/calculate.sml" (*part.*)
5.8 - use "ProgLang/rewrite.sml" (*?complete?*)
5.9 + use "ProgLang/calculate.sml"
5.10 + use "ProgLang/rewrite.sml"
5.11 (*use "ProgLang/listC.sml" 2002*)
5.12 - use "ProgLang/scrtools.sml" (*complete*)
5.13 - use "ProgLang/tools.sml" (*complete*)
5.14 + use "ProgLang/scrtools.sml"
5.15 + use "ProgLang/tools.sml"
5.16 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
5.17 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
5.18 use "Minisubpbl/000-comments.sml"
5.19 @@ -141,7 +141,7 @@
5.20 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
5.21 use "Frontend/messages.sml" (*new 2011*)
5.22 use "Frontend/states.sml" (*new 2011*)
5.23 - use "Frontend/interface.sml" (*complete*)
5.24 + use "Frontend/interface.sml"
5.25 use "print_exn_G.sml" (*new 2011*)
5.26 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
5.27 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
5.28 @@ -161,19 +161,19 @@
5.29 (*use "Knowledge/polyeq.sml" 2002*)
5.30 (*use "Knowledge/rlang.sml" 2002???*)
5.31 use "Knowledge/calculus.sml" (*new 2011*)
5.32 - use "Knowledge/trig.sml" (*complete*)
5.33 + use "Knowledge/trig.sml"
5.34 use "Knowledge/logexp.sml" (*part.*)
5.35 use "Knowledge/diff.sml" (*part.*)
5.36 use "Knowledge/integrate.sml" (*part. was complete 2009-2
5.37 diff.emacs--jedit*)
5.38 use "Knowledge/eqsystem.sml" (*part.*)
5.39 - use "Knowledge/test.sml" (*complete*)
5.40 + use "Knowledge/test.sml"
5.41 use "Knowledge/polyminus.sml" (*part.*)
5.42 - use "Knowledge/vect.sml" (*complete*)
5.43 + use "Knowledge/vect.sml"
5.44 use "Knowledge/diffapp.sml" (*part.*)
5.45 use "Knowledge/biegelinie.sml" (*part.*)
5.46 use "Knowledge/algein.sml" (*part.*)
5.47 - use "Knowledge/diophanteq.sml" (*complete*)
5.48 + use "Knowledge/diophanteq.sml"
5.49 use "Knowledge/isac.sml" (*part.*)
5.50 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
5.51 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
6.1 --- a/test/Tools/isac/Test_Some.thy Wed Jul 27 13:05:27 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 28 11:27:04 2011 +0200
6.3 @@ -5,23 +5,22 @@
6.4
6.5 theory Test_Some imports Isac begin
6.6
6.7 -ML{* writeln "**** run the test ***************************************" *}
6.8 +use"../../../test/Tools/isac/Frontend/interface.sml"
6.9
6.10 -use"../../../test/Tools/isac/Interpret/script.sml"
6.11 +
6.12 +ML{*
6.13 +*}
6.14
6.15 ML {*
6.16
6.17
6.18 +*}
6.19 +ML{*
6.20
6.21 -
6.22 -
6.23 -
6.24 -
6.25 -
6.26 -
6.27 -
6.28 -
6.29 -
6.30 +*}
6.31 +ML{*
6.32 +*}
6.33 +ML{*
6.34 *}
6.35 ML{*
6.36 *}