intermed. ctxt ..: cleanup before start with Add_Given
uncommenting in src/../calchead.sm 2x "update_env" after "prep_ori"
marked with GOON.WN110506
causes errors in most test/../*, all with CalcTreeTEST; me; ..
1.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu May 05 14:21:54 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri May 06 11:18:07 2011 +0200
1.3 @@ -1094,9 +1094,10 @@
1.4 val (oris, ctxt) =
1.5 if dI' = e_domID orelse pI' = e_pblID
1.6 then ([], e_ctxt)
1.7 - else pI' |> #ppc o get_pbt |> prep_ori fmz thy;
1.8 + else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1.9 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.10 - (oris, (dI',pI',mI'),e_term);
1.11 + (oris, (dI',pI',mI'),e_term)
1.12 + (*val pt = update_env pt [] (SOME (e_istate, ctxt)) GOON.WN110506*)
1.13 val {ppc, prls, where_, ...} = get_pbt pI'
1.14 val (pbl, pre, pb) = ([], [], false)
1.15 in
1.16 @@ -1576,6 +1577,7 @@
1.17 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1.18 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1.19 (pors, (dI, pI, mI), hdl)
1.20 + (* val pt = update_env pt [] (SOME (e_istate, pctxt)) GOON.WN110506*)
1.21 in ((pt, ([], Pbl)),
1.22 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.23 end;
2.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu May 05 14:21:54 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/ctree.sml Fri May 06 11:18:07 2011 +0200
2.3 @@ -732,8 +732,13 @@
2.4 (*^^^FIXME.WN0607 rename this field*)
2.5 form : term, (* where tac is applied to *)
2.6 tac : tac, (* also in istate *)
2.7 - loc : (istate * Proof.context) option * (istate * Proof.context) option,
2.8 - (*for form, result 13.8.02: (NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
2.9 + loc : (istate * (* script interpreter state *)
2.10 + Proof.context) (* context for provers, type inference *)
2.11 + option * (* both for interpreter location on Frm, Pbl, Met *)
2.12 + (istate * (* script interpreter state *)
2.13 + Proof.context) (* context for provers, type inference *)
2.14 + option, (* both for interpreter location on Res *)
2.15 + (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
2.16 branch: branch, (* only rudimentary *)
2.17 result: term * term list, (* result and assumptions *)
2.18 ostate: ostate} (* Complete <=> result is OK *)
2.19 @@ -742,18 +747,19 @@
2.20 fmz : fmz, (* from init:FIXME never use this spec;-drop *)
2.21 origin: (ori list) * (* representation from fmz+pbt
2.22 for efficiently adding items in probl, meth *)
2.23 - spec * (* updated by Refine_Tacitly *)
2.24 - term, (* headline of calc-head, as calculated initially(!)*)
2.25 + spec * (* updated by Refine_Tacitly *)
2.26 + term, (* headline of calc-head, as calculated initially(!)*)
2.27 spec : spec, (* explicitly input *)
2.28 probl : itm list, (* itms explicitly input *)
2.29 meth : itm list, (* itms automatically added to copy of probl *)
2.30 env : (istate * Proof.context) option,
2.31 - (* for problem with initac in script*)
2.32 + (* istate only for initac in script
2.33 + context for specify phase on this node *)
2.34 loc : (istate * Proof.context) option * (istate * Proof.context) option,
2.35 - (* for pbl+met * result *)
2.36 - branch: branch, (* only rudimentary *)
2.37 - result: term * term list, (* result and assumptions *)
2.38 - ostate: ostate}; (* Complete <=> result is _proven_ OK *)
2.39 + (* like PrfObj *)
2.40 + branch: branch, (* like PrfObj *)
2.41 + result: term * term list, (* like PrfObj *)
2.42 + ostate: ostate}; (* like PrfObj *)
2.43
2.44 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
2.45 the structure has been copied from an early version of Theorema(c);
3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu May 05 14:21:54 2011 +0200
3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri May 06 11:18:07 2011 +0200
3.3 @@ -695,7 +695,7 @@
3.4 Thm ("tl_Nil",num_str @{thm tl_Nil})
3.5 ],
3.6 prls = Erls, crls = Erls, nrls = Erls},
3.7 -(*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.8 +(*STOPPED.WN06? met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
3.9 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
3.10 " (let e__s = " ^
3.11 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
4.1 --- a/test/Tools/isac/CLEANUP Thu May 05 14:21:54 2011 +0200
4.2 +++ b/test/Tools/isac/CLEANUP Fri May 06 11:18:07 2011 +0200
4.3 @@ -9,6 +9,13 @@
4.4 rm .#*
4.5 rm *.tar*
4.6 rm *.orig
4.7 + cd file-depend
4.8 + rm *~
4.9 + rm #*
4.10 + rm .#*
4.11 + rm *.tar*
4.12 + rm *.orig
4.13 + cd ..
4.14 cd ..
4.15 cd ProgLang
4.16 rm *~
5.1 --- a/test/Tools/isac/Interpret/appl.sml Thu May 05 14:21:54 2011 +0200
5.2 +++ b/test/Tools/isac/Interpret/appl.sml Fri May 06 11:18:07 2011 +0200
5.3 @@ -21,6 +21,7 @@
5.4 ("Test",["sqroot-test","univariate","equation","test"],
5.5 ["Test","squ-equ-test-subpbl1"]);
5.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.7 +(*========== inhibit exn 110415 -> 110506 ======================================
5.8 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.10 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.11 @@ -40,7 +41,6 @@
5.12 val ctxt = assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres;
5.13 (*TODO.WN110416 read pres from ctxt and check*)
5.14
5.15 -(*========== inhibit exn 110415 ================================================
5.16 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.17 show_pt pt;
5.18 ============ inhibit exn 110415 ==============================================*)
5.19 @@ -81,5 +81,5 @@
5.20 if t = parseNEW "-1 + x = (0::real)" then ()
5.21 else error "TODO"
5.22 is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
5.23 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) use "Interpret/mstools.sml" (*empty*)
5.24 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
5.25
6.1 --- a/test/Tools/isac/Interpret/mstools.sml Thu May 05 14:21:54 2011 +0200
6.2 +++ b/test/Tools/isac/Interpret/mstools.sml Fri May 06 11:18:07 2011 +0200
6.3 @@ -11,7 +11,7 @@
6.4 "----------- fun declare_constraints --------------------";
6.5 "----------- fun get_assumptions, fun get_environments --";
6.6 "----------- fun transfer_from_subproblem ---------------";
6.7 -"----------- all handling ctxt in minimsubpbl x+1=2 ----";
6.8 +"----------- all handling ctxt in minimsubpbl x+1=2 -----";
6.9 "--------------------------------------------------------";
6.10 "--------------------------------------------------------";
6.11 "--------------------------------------------------------";
6.12 @@ -63,5 +63,37 @@
6.13 "----------- all handling ctxt in minimsubpbl x+1=2 ----";
6.14 "----------- all handling ctxt in minimsubpbl x+1=2 ----";
6.15 "----------- all handling ctxt in minimsubpbl x+1=2 ----";
6.16 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.17 +val (dI',pI',mI') =
6.18 + ("Test", ["sqroot-test","univariate","equation","test"],
6.19 + ["Test","squ-equ-test-subpbl1"]);
6.20 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.21 +print_depth 999; pt; (*see tmp/del.sml*)
6.22 +(*GOON ---------------------------
6.23 +val SOME (_, ctxt) = get_obj g_env pt (fst p);
6.24 +if parseNEW ctxt "x+y+z" = parseNEW ctxt "x+y+(z::real)" andalso
6.25 + parseNEW ctxt "a+b+c" <> parseNEW ctxt "a+b+(c::real)" then ()
6.26 +else error "mstools.sml: ctxt initialisation broken in rootproblem";
6.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.32 +(*nxt = Specify_Problem*)
6.33 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.34 +(* check precond_root_1, precond_root_2 in root-ctxt TODO *)
6.35 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.36 +(*nxt = Apply_Method*)
6.37 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.38 +(* check precond_root_1, precond_root_2 in sub-ctxt TODO *)
6.39 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.40 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.41 +(*nxt = Subproblem*)
6.42 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.43 +(* check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a in subproblem*)
6.44 +print_depth 999; pt; (*see tmp/del.sml*)
6.45 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
6.46 +(*nxt = Tac..ERROR*)
6.47 +---------------------------GOON *)
6.48
6.49
7.1 --- a/test/Tools/isac/Knowledge/algein.sml Thu May 05 14:21:54 2011 +0200
7.2 +++ b/test/Tools/isac/Knowledge/algein.sml Fri May 06 11:18:07 2011 +0200
7.3 @@ -150,7 +150,7 @@
7.4 (********"0 = 3 * 0"*)
7.5
7.6 val thm = assoc_thm' thy ("sym","");
7.7 -(*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
7.8 +(*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
7.9 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
7.10 *)
7.11
8.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu May 05 14:21:54 2011 +0200
8.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri May 06 11:18:07 2011 +0200
8.3 @@ -245,7 +245,7 @@
8.4 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
8.5 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
8.6 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
8.7 -(*GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
8.8 +(*STOPPED.WN06?: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
8.9 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
8.10 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
8.11 \c + c_2 + c_3 + c_4 = 0,\
8.12 @@ -1087,7 +1087,7 @@
8.13 c |
8.14 c c_2 |1:c -> 2:c_2
8.15 c_3 |
8.16 - c_4 | GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
8.17 + c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
8.18
8.19 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
8.20 val t = str2term"[L * q_0 = c, \
8.21 @@ -1395,7 +1395,7 @@
8.22 "----------- 4x4 systems from Biegelinie -------------------------";
8.23 "----------- 4x4 systems from Biegelinie -------------------------";
8.24 "----------- 4x4 systems from Biegelinie -------------------------";
8.25 -(*GOON replace this test with 7.70 *)
8.26 +(*STOPPED.WN08?? replace this test with 7.70 *)
8.27 "----- Bsp 7.27";
8.28 val fmz = ["equalities \
8.29 \[0 = c_4, \
9.1 --- a/test/Tools/isac/Knowledge/poly.sml Thu May 05 14:21:54 2011 +0200
9.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri May 06 11:18:07 2011 +0200
9.3 @@ -437,7 +437,7 @@
9.4 "normalform N"];
9.5 "-----0 ---";
9.6 (*===== inhibit exn ============================================================
9.7 -GOON
9.8 +STOPPED.WN10xx
9.9
9.10 case refine fmz ["polynomial","simplification"]of
9.11 [Matches (["polynomial", "simplification"], _)] => ()
10.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu May 05 14:21:54 2011 +0200
10.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Fri May 06 11:18:07 2011 +0200
10.3 @@ -530,7 +530,7 @@
10.4 (*TODO: make is_monom more general, a*a=a^2, ...*)
10.5 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;
10.6 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";
10.7 -(*GOON.WN080104
10.8 +(*STOPPED.WN080104
10.9 val rls = fasse_zusammen;
10.10 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;
10.11 val rls = verschoenere;
11.1 --- a/test/Tools/isac/Test_Isac.thy Thu May 05 14:21:54 2011 +0200
11.2 +++ b/test/Tools/isac/Test_Isac.thy Fri May 06 11:18:07 2011 +0200
11.3 @@ -82,108 +82,6 @@
11.4 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
11.5 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
11.6 ML {*
11.7 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11.8 -val (dI',pI',mI') =
11.9 - ("Test", ["sqroot-test","univariate","equation","test"],
11.10 - ["Test","squ-equ-test-subpbl1"]);
11.11 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
11.12 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.13 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.14 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.15 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.16 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.17 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.18 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.19 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.20 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.21 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.22 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.23 -(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS:
11.24 - Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
11.25 -(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: applicable_in (p,Pbl) pt (Tac id): not at Pbl*)
11.26 -show_pt pt; (*WAS ...(([3], Pbl), solve (-1 + x = 0, x))] OK*)
11.27 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
11.28 -val (pt, p) = case locatetac tac (pt,p) of
11.29 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
11.30 -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
11.31 -val pIopt = get_pblID (pt,ip);
11.32 -tacis; (*= []*)
11.33 -pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
11.34 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
11.35 -"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
11.36 -val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
11.37 - probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
11.38 -just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
11.39 -val cpI = if pI = e_pblID then pI' else pI;
11.40 - val cmI = if mI = e_metID then mI' else mI;
11.41 - val {ppc, prls, where_, ...} = get_pbt cpI;
11.42 - val pre = check_preconds "thy 100820" prls where_ probl;
11.43 - val pb = foldl and_ (true, map fst pre);
11.44 -val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
11.45 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
11.46 -"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
11.47 -"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
11.48 -val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
11.49 - probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
11.50 -val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
11.51 -val cpI = if pI = e_pblID then pI' else pI;
11.52 -val ctxt = get_ctxt pt (p, Pbl);
11.53 -oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)
11.54 -"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
11.55 - (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
11.56 -*}
11.57 -ML {*
11.58 -val t = parseNEW ctxt str;
11.59 -str;
11.60 -t;
11.61 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
11.62 -if t = parseNEW ctxt "-1 + x = (0::real)" then ()
11.63 -else error "TODO"
11.64 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
11.65 -
11.66 -*}
11.67 -ML {*
11.68 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
11.69 -print_depth 999; applicable_in p pt m;
11.70 -Model_Problem';
11.71 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
11.72 -*}
11.73 -ML {*
11.74 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11.75 -val (dI',pI',mI') =
11.76 - ("Test", ["sqroot-test","univariate","equation","test"],
11.77 - ["Test","squ-equ-test-subpbl1"]);
11.78 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
11.79 -(*nxt = Model_Problem*)
11.80 -print_depth 999; pt;
11.81 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.82 -(*check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a *)
11.83 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.84 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.85 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.86 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.87 -(*nxt = Specify_Problem*)
11.88 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.89 -(* check precond_root_1, precond_root_2 in root-ctxt *)
11.90 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.91 -(*nxt = Apply_Method*)
11.92 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.93 -(*check precond_root_1, precond_root_2 in sub-ctxt *)
11.94 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.95 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.96 -*}
11.97 -ML {*
11.98 -(*nxt = Subproblem*)
11.99 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.100 -*}
11.101 -ML {*
11.102 -(*nxt = Model_Problem*)
11.103 -print_depth 999; pt;
11.104 -*}
11.105 -ML {*
11.106 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.107 -(*check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a *)
11.108 -(*nxt = ERROR*)
11.109 *}
11.110
11.111 use "Interpret/mstools.sml" (*new 2010*)