1.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Sat May 02 10:57:04 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Sat May 02 11:36:13 2020 +0200
1.3 @@ -332,8 +332,7 @@
1.4 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.5 }: string ppc;
1.6 *)
1.7 -val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.8 - specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1.9 +val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
1.10
1.11 val ct = "fixedValues [R=(R::real)]";
1.12 (*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)
1.13 @@ -375,16 +374,14 @@
1.14 *)
1.15 *)
1.16 (* --- tricky case (termlist interleaving variants):
1.17 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.18 - specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
1.19 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
1.20
1.21 > val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";
1.22 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.23 *)
1.24
1.25 (* --- incomplete input ---
1.26 -> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
1.27 - specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
1.28 +> val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = Test_Code.CalcTreeTEST [(cts, (dI',pI',mI'))];
1.29
1.30 > val ct = "[R=(R::real)]";
1.31 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
1.32 @@ -419,6 +416,7 @@
1.33 ("DiffAppl",["DiffAppl","test_maximum"],Method.id_empty);
1.34 val p = e_pos'; val c = [];
1.35
1.36 +(*/------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------\* )
1.37 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
1.38 val (pst as (sc,pt,cl):pstate) = (Rule.Empty_Prog, e_ctree, []);
1.39 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
1.40 @@ -427,3 +425,4 @@
1.41 val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) =
1.42 do_ nxt p c (Rule.Empty_Prog,pt,[]);
1.43 (*val nxt = ("Add_Given",Add_Given "boundVariable a") *)
1.44 +( *\------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------/*)
2.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 10:57:04 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 11:36:13 2020 +0200
2.3 @@ -14,7 +14,6 @@
2.4 | Add_Relation' of TermC.as_string * Model.itm list
2.5 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
2.6 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
2.7 -(*RM*)| Init_Proof' of TermC.as_string list * Spec.T
2.8 | Model_Problem' of Problem.id * Model.itm list * Model.itm list
2.9 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
2.10 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
2.11 @@ -50,7 +49,6 @@
2.12 | Add_Relation of TermC.as_string
2.13 | Apply_Method of Method.id
2.14 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
2.15 - | Init_Proof of TermC.as_string list * Spec.T
2.16 | Model_Problem
2.17 | Refine_Problem of Problem.id
2.18 | Refine_Tacitly of Problem.id
2.19 @@ -118,7 +116,6 @@
2.20 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
2.21 | Apply_Method of Method.id
2.22 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
2.23 - | Init_Proof of TermC.as_string list * Spec.T
2.24 | Model_Problem
2.25 | Refine_Problem of Problem.id
2.26 | Refine_Tacitly of Problem.id
2.27 @@ -148,9 +145,7 @@
2.28 | End_Proof';
2.29
2.30 fun input_to_string ma = case ma of
2.31 - Init_Proof (ppc, spec) =>
2.32 - "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
2.33 - | Model_Problem => "Model_Problem "
2.34 + Model_Problem => "Model_Problem "
2.35 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
2.36 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
2.37 | Add_Given cterm' => "Add_Given " ^ cterm'
2.38 @@ -320,7 +315,6 @@
2.39 Istate_Def.T * (* for starting the Program *)
2.40 Proof.context (* for starting the Program *)
2.41 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
2.42 -(*RM*)| Init_Proof' of TermC.as_string list * Spec.T
2.43 | Model_Problem' of (* first step in specify-phase *)
2.44 Problem.id * (* id in the Know_Store *)
2.45 Model.itm list * (* the model for the Problem *)
2.46 @@ -376,8 +370,7 @@
2.47 | End_Proof''
2.48
2.49 fun string_of ma = case ma of
2.50 - Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
2.51 - | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
2.52 + Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
2.53 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
2.54 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
2.55 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
2.56 @@ -472,8 +465,7 @@
2.57
2.58 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
2.59
2.60 -fun for_specify (Init_Proof _) = true
2.61 - | for_specify Model_Problem = true
2.62 +fun for_specify Model_Problem = true
2.63 | for_specify (Refine_Tacitly _) = true
2.64 | for_specify (Refine_Problem _) = true
2.65 | for_specify (Add_Given _) = true
2.66 @@ -486,8 +478,7 @@
2.67 | for_specify (Specify_Problem _) = true
2.68 | for_specify (Specify_Method _) = true
2.69 | for_specify _ = false
2.70 -fun for_specify' (Init_Proof' _) = true
2.71 - | for_specify' (Model_Problem' _) = true
2.72 +fun for_specify' (Model_Problem' _) = true
2.73 | for_specify' (Refine_Tacitly' _) = true
2.74 | for_specify' (Refine_Problem' _) = true
2.75 | for_specify' (Add_Given' _) = true
3.1 --- a/src/Tools/isac/Specify/specify-step.sml Sat May 02 10:57:04 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/specify-step.sml Sat May 02 11:36:13 2020 +0200
3.3 @@ -71,7 +71,6 @@
3.4 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
3.5 then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.6 else Applicable.Yes (Tactic.Del_Relation' ct')
3.7 - | check (Tactic.Init_Proof (ct', spec)) _ = Applicable.Yes (Tactic.Init_Proof' (ct', spec))
3.8 | check Tactic.Model_Problem (pt, (p, p_)) =
3.9 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
3.10 Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
3.11 @@ -79,7 +78,7 @@
3.12 let
3.13 val pI' = case Ctree.get_obj I pt p of
3.14 Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
3.15 - | _ => error "Specify_Step.check Init_Proof: uncovered case Ctree.get_obj"
3.16 + | _ => error "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
3.17 val {ppc, ...} = Specify.get_pbt pI'
3.18 val pbl = Generate.init_pbl ppc
3.19 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
4.1 --- a/src/Tools/isac/Specify/step-specify.sml Sat May 02 10:57:04 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/step-specify.sml Sat May 02 11:36:13 2020 +0200
4.3 @@ -147,24 +147,7 @@
4.4
4.5
4.6 (* was fun Chead.specify *)
4.7 -fun by_tactic (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ =
4.8 - let (* either """"""""""""""" all empty or complete *)
4.9 - val thy = ThyC.get_theory dI'
4.10 - val (oris, ctxt) =
4.11 - if dI' = ThyC.id_empty orelse pI' = Problem.id_empty (*andalso? WN110511*)
4.12 - then ([], ContextC.empty)
4.13 - else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
4.14 - (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
4.15 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) (fmz, spec')
4.16 - (oris, (dI',pI',mI'), TermC.empty, ctxt)
4.17 - val pt = update_loc' pt [] (SOME (Istate_Def.empty, ctxt), NONE)
4.18 - in
4.19 - case mI' of
4.20 - ["no_met"] => ("Refine_Tacitly", ([], [], (pt, ([], Pbl))))
4.21 - | _ => ("ok", ([], [], (pt, ([], Pbl))))
4.22 - end
4.23 - (* ONLY for STARTING modeling phase *)
4.24 - | by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _)) =
4.25 +fun by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _)) =
4.26 let
4.27 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
4.28 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
5.1 --- a/test/Tools/isac/Knowledge/diff.sml Sat May 02 10:57:04 2020 +0200
5.2 +++ b/test/Tools/isac/Knowledge/diff.sml Sat May 02 11:36:13 2020 +0200
5.3 @@ -190,9 +190,6 @@
5.4 val (dI',pI',mI') =
5.5 ("Diff",["derivative_of","function"],
5.6 ["diff","diff_simpl"]);
5.7 -(*val p = e_pos'; val c = [];
5.8 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
5.9 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
5.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Sat May 02 10:57:04 2020 +0200
6.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Sat May 02 11:36:13 2020 +0200
6.3 @@ -124,15 +124,6 @@
6.4 "-------------------- ctree of {(a,b). is-max ... --------------------------";
6.5 "-------------------- ctree of {(a,b). is-max ... --------------------------";
6.6
6.7 -(* Teil von max-on-surface.sml,
6.8 - der nach Init_Proof -> prep_ori wieder l"auft
6.9 - (f"ur tests mit neuer pos')
6.10 - use"test-max-surf1.sml";
6.11 -
6.12 - Compiler.Control.Print.printDepth:=7; (*4 is default*)
6.13 - Compiler.Control.Print.printDepth:=4; (*4 is default*)
6.14 - *)
6.15 -
6.16 (* --vvv-- ausgeliehen von test-root-equ/sml *)
6.17 val loc = Istate.empty;
6.18 val (dI',pI',mI') =
6.19 @@ -143,7 +134,7 @@
6.20 "solutions L"];
6.21 (*
6.22 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.23 -val ((p,p_),_,_,_,_,(_,pt,_)) = do_ (mI,m) e_pos'[1](e_scr,EmptyPtree,[]);
6.24 +val ((p,p_),_,_,_,_,(_,pt,_)) = CalcTreeTEST [fmz, (dI',pI',mI')))];
6.25 --^^^-- ausgeliehen von test-root-equ/sml *)
6.26 (*-------------- 9.6.03 --- cappend_ ... term -------irreparabler test
6.27 val (pt,_) =
7.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Sat May 02 10:57:04 2020 +0200
7.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sat May 02 11:36:13 2020 +0200
7.3 @@ -390,9 +390,6 @@
7.4 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
7.5 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
7.6 ["PolyEq","solve_d2_polyeq_pq_equation"]);
7.7 -(*val p = e_pos';
7.8 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
7.9 -val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
7.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Sat May 02 10:57:04 2020 +0200
8.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Sat May 02 11:36:13 2020 +0200
8.3 @@ -197,10 +197,6 @@
8.4 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
8.5 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
8.6 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
8.7 -(*val p = e_pos';
8.8 -val c = [];
8.9 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
8.10 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
8.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
8.12
8.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.1 --- a/test/Tools/isac/Knowledge/rlang.sml Sat May 02 10:57:04 2020 +0200
9.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Sat May 02 11:36:13 2020 +0200
9.3 @@ -63,10 +63,6 @@
9.4 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",
9.5 "solveFor x","solutions L"];
9.6 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.7 -(*val p = e_pos';
9.8 -val c = [];
9.9 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.10 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.14 @@ -94,10 +90,6 @@
9.15 val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
9.16 "solveFor x","solutions L"];
9.17 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.18 -(*val p = e_pos';
9.19 -val c = [];
9.20 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.21 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.22 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.25 @@ -124,10 +116,6 @@
9.26 val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",
9.27 "solveFor x","solutions L"];
9.28 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.29 -(*val p = e_pos';
9.30 -val c = [];
9.31 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.32 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.33 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.34 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.35 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.36 @@ -154,10 +142,6 @@
9.37 val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",
9.38 "solveFor x","solutions L"];
9.39 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.40 -(*val p = e_pos';
9.41 -val c = [];
9.42 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.43 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.44 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.47 @@ -184,9 +168,6 @@
9.48 val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
9.49 "solveFor x","solutions L"];
9.50 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.51 -(*val p = e_pos'; val c = [];
9.52 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.53 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.54 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.57 @@ -226,10 +207,6 @@
9.58 val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
9.59 "solveFor x","solutions L"];
9.60 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.61 -(*val p = e_pos';
9.62 -val c = [];
9.63 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.64 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.65 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.68 @@ -266,10 +243,6 @@
9.69 val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
9.70 "solveFor x","solutions L"];
9.71 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.72 -(*val p = e_pos';
9.73 -val c = [];
9.74 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.75 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.76 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.79 @@ -306,10 +279,6 @@
9.80 val fmz = ["equality ((x+3)/(2*x - 4)=3)",
9.81 "solveFor x","solutions L"];
9.82 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.83 -(*val p = e_pos';
9.84 -val c = [];
9.85 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.86 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.87 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.90 @@ -348,10 +317,6 @@
9.91 val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",
9.92 "solveFor x","solutions L"];
9.93 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.94 -(*val p = e_pos';
9.95 -val c = [];
9.96 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.97 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.98 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.99 (*Rewrite.trace_on:=true;
9.100 *)
9.101 @@ -395,9 +360,6 @@
9.102 "solveFor x","solutions L"];
9.103 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.104
9.105 -(*val p = e_pos'; val c = [];
9.106 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.107 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.108 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.111 @@ -435,9 +397,6 @@
9.112 "solveFor m1","solutions L"];
9.113 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.114
9.115 -(*val p = e_pos'; val c = [];
9.116 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.117 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.118 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.121 @@ -464,9 +423,6 @@
9.122 "solveFor v","solutions L"];
9.123 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.124
9.125 -(*val p = e_pos'; val c = [];
9.126 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.127 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.128 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.131 @@ -542,9 +498,6 @@
9.132 val fmz = ["equality (f=((w+u)/(w+v))*v0)",
9.133 "solveFor w","solutions L"];
9.134 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.135 -(*val p = e_pos';val c = [];
9.136 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.137 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.138 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.141 @@ -590,9 +543,6 @@
9.142 val fmz = ["equality (1/R=1/R1+1/R2)",
9.143 "solveFor R1","solutions L"];
9.144 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.145 -(*val p = e_pos'; val c = [];
9.146 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.147 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.148 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.151 @@ -635,9 +585,6 @@
9.152 val fmz = ["equality (y^^^2=2*p*x)",
9.153 "solveFor p","solutions L"];
9.154 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.155 -(*val p = e_pos'; val c = [];
9.156 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.157 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.158 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.161 @@ -668,10 +615,6 @@
9.162 val fmz = ["equality (y^^^2=2*p*x)",
9.163 "solveFor y","solutions L"];
9.164 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.165 -(*val p = e_pos';
9.166 -val c = [];
9.167 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.168 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.169 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.172 @@ -703,10 +646,6 @@
9.173 val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",
9.174 "solveFor x","solutions L"];
9.175 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.176 -(*val p = e_pos';
9.177 -val c = [];
9.178 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.179 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.180 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.183 @@ -753,10 +692,6 @@
9.184 val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
9.185 "solveFor x2","solutions L"];
9.186 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.187 -(*val p = e_pos';
9.188 -val c = [];
9.189 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.190 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.191 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.194 @@ -792,10 +727,6 @@
9.195 val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
9.196 "solveFor x","solutions L"];
9.197 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
9.198 -(*val p = e_pos';
9.199 -val c = [];
9.200 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.201 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.202 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.205 @@ -830,10 +761,6 @@
9.206 val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
9.207 "solveFor x","solutions L"];
9.208 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
9.209 -(*val p = e_pos';
9.210 -val c = [];
9.211 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.212 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.213 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.214 (* val nxt = ("Model_Problem",Model_Problem ["normalise","rootX","univariate","equation"])*)
9.215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.216 @@ -1078,10 +1005,6 @@
9.217 val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
9.218 "solveFor x","solutions L"];
9.219 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
9.220 -(*val p = e_pos';
9.221 -val c = [];
9.222 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.223 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.224 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.225 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.226 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.227 @@ -1150,10 +1073,6 @@
9.228 val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
9.229 "solveFor x","solutions L"];
9.230 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
9.231 -(*val p = e_pos';
9.232 -val c = [];
9.233 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.234 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.235 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.237 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.238 @@ -1192,10 +1111,6 @@
9.239 val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",
9.240 "solveFor x","solutions L"];
9.241 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
9.242 -(*val p = e_pos';
9.243 -val c = [];
9.244 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.245 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.246 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.249 @@ -1286,10 +1201,6 @@
9.250 val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",
9.251 "solveFor a","solutions L"];
9.252 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
9.253 -(*val p = e_pos';
9.254 -val c = [];
9.255 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
9.256 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
9.257 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.259 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Sat May 02 10:57:04 2020 +0200
10.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Sat May 02 11:36:13 2020 +0200
10.3 @@ -146,9 +146,6 @@
10.4 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
10.5 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
10.6 (*val p = e_pos';
10.7 -val c = [];
10.8 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.9 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.13 @@ -269,9 +266,6 @@
10.14 "solveFor x","solutions L"];
10.15 val (dI',pI',mI') = ("RootEq",["sq","rootX","univariate","equation"],
10.16 ["RootEq","solve_sq_root_equation"]);
10.17 -(*val p = e_pos'; val c = [];
10.18 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.19 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.23 @@ -320,9 +314,6 @@
10.24 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
10.25 val (dI',pI',mI') = ("RootEq",["sq","rootX","univariate","equation"],
10.26 ["RootEq","solve_sq_root_equation"]);
10.27 -(*val p = e_pos'; val c = [];
10.28 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.29 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.30 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.33 @@ -488,9 +479,6 @@
10.34 val (dI',pI',mI') =
10.35 ("Test",["sqroot-test","univariate","equation","test"],
10.36 ["Test","square_equation1"]);
10.37 -(*val p = e_pos'; val c = [];
10.38 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.39 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.40 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.43 @@ -563,9 +551,6 @@
10.44 val Prog sc = (#scr o get_met) ["Test","square_equation2"];
10.45 (writeln o UnparseC.term) sc;
10.46
10.47 -(*val p = e_pos'; val c = [];
10.48 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.49 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.51 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.53 @@ -643,9 +628,6 @@
10.54 val (dI',pI',mI') =
10.55 ("Test",["squareroot","univariate","equation","test"],
10.56 ["Test","square_equation"]);
10.57 -(*val p = e_pos'; val c = [];
10.58 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.59 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.60 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.63 @@ -706,9 +688,6 @@
10.64 val Prog sc = (#scr o get_met) ["Test","square_equation"];
10.65 (writeln o UnparseC.term) sc;
10.66
10.67 -(*val p = e_pos'; val c = [];
10.68 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.69 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.70 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
10.73 @@ -762,9 +741,6 @@
10.74 val (dI',pI',mI') =
10.75 ("Test",["univariate","equation","test"],
10.76 ["no_met"]);
10.77 -(*val p = e_pos'; val c = [];
10.78 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
10.79 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
10.80 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.81 (*val nxt = ("Model_Problem",Model_Problem ["normalise","univariate","equati*)
10.82 val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Sat May 02 10:57:04 2020 +0200
11.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Sat May 02 11:36:13 2020 +0200
11.3 @@ -399,10 +399,7 @@
11.4 val (dI',pI',mI') =
11.5 ("Test",["sqroot-test","univariate","equation","test"],
11.6 ("Test","sqrt-equ-test"));
11.7 -val p = e_pos'; val c = [];
11.8 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
11.9 -
11.10 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
11.11 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
11.12 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
11.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.14 (* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
11.15 @@ -504,9 +501,6 @@
11.16 ("Test",["sqroot-test","univariate","equation","test"],
11.17 ["Test","sqrt-equ-test"]);
11.18 "--- s1 ---";
11.19 -(*val p = e_pos'; val c = [];
11.20 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
11.21 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
11.22 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
11.23 "--- s1b ---";
11.24 val nxt = ("Model_Problem",
12.1 --- a/test/Tools/isac/OLDTESTS/script.sml Sat May 02 10:57:04 2020 +0200
12.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Sat May 02 11:36:13 2020 +0200
12.3 @@ -188,9 +188,6 @@
12.4 val (dI',pI',mI') =
12.5 ("Test",["sqroot-test","univariate","equation","test"],
12.6 ["Test","sqrt-equ-test"]);
12.7 -(*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
12.8 -val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)
12.9 -
12.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
12.11 val nxt = ("Model_Problem",
12.12 Model_Problem ["sqroot-test","univariate","equation","test"]);
12.13 @@ -258,9 +255,8 @@
12.14 atomty sc;
12.15 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
12.16 ["Test","sqrt-equ-test"]);
12.17 -val p = e_pos'; val c = [];
12.18 -val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
12.19 -val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
12.20 +val c = [];
12.21 +val (p,_,_,_,_,pt) = CalcTreeTEST [([], (dI',pI',mI')))];
12.22 val nxt = ("Specify_Theory",Specify_Theory "Test");
12.23 val (p,_,_,_,_,pt) = me nxt p c pt;
12.24 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
13.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Sat May 02 10:57:04 2020 +0200
13.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Sat May 02 11:36:13 2020 +0200
13.3 @@ -98,9 +98,7 @@
13.4 val (dI',pI',mI') =
13.5 ("Isac_Knowledge",["approximate","univariate","equation","test"],
13.6 ("Isac_Knowledge","solve_univar_err"));
13.7 -val p = e_pos'; val c = [];
13.8 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
13.9 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
13.10 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
13.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.14 @@ -137,9 +135,7 @@
13.15 val (dI',pI',mI') =
13.16 ("Isac_Knowledge",["approximate","univariate","equation","test"],
13.17 ("Isac_Knowledge","solve_univar_err"));
13.18 -val p = e_pos'; val c = [];
13.19 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
13.20 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
13.21 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
13.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Sat May 02 10:57:04 2020 +0200
14.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Sat May 02 11:36:13 2020 +0200
14.3 @@ -48,9 +48,6 @@
14.4 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];
14.5 val (dI',pI',mI') = ("Test",["met_testterm","tests"],
14.6 ["Test","met_testterm"]);
14.7 -(*val p = e_pos'; val c = [];
14.8 -val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.9 -val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
14.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.13 @@ -123,9 +120,6 @@
14.14 ["Test","testeq1"]);
14.15 val Prog sc = (#scr o get_met) ["Test","testeq1"];
14.16 atomt sc;
14.17 -(*val p = e_pos'; val c = [];
14.18 -val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.19 -val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
14.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.23 @@ -180,9 +174,6 @@
14.24 "boolTestFind v_i_"];
14.25 val (dI',pI',mI') = ("Test",["met_testeq","tests"],
14.26 ["Test","testlet"]);
14.27 -(*val p = e_pos'; val c = [];
14.28 -val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.29 -val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
14.30 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.33 @@ -213,9 +204,6 @@
14.34 writeln(UnparseC.term sc);
14.35
14.36 "--- s1 ---";
14.37 -(*val p = e_pos'; val c = [];
14.38 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.39 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
14.40 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.41 "--- s2 ---";
14.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.43 @@ -316,9 +304,6 @@
14.44 val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];
14.45 (writeln o UnparseC.term) sc;
14.46 "--- s1 ---";
14.47 -(*val p = e_pos'; val c = [];
14.48 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.49 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
14.50 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.51 "--- s2 ---";
14.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.53 @@ -388,9 +373,6 @@
14.54 ("Test",["sqroot-test","univariate","equation","test"],
14.55 ["Test","square_equation"]);
14.56
14.57 -(*val p = e_pos'; val c = [];
14.58 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
14.59 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
14.60 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14.61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.62 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Sat May 02 10:57:04 2020 +0200
15.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Sat May 02 11:36:13 2020 +0200
15.3 @@ -63,10 +63,6 @@
15.4 val (dI',pI',mI') =
15.5 ("Test",["plain_square","univariate","equation","test"],
15.6 ["Test","solve_plain_square"]);
15.7 -(*val p = e_pos'; val c = [];
15.8 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
15.9 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
15.10 -
15.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
15.12 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
15.13
16.1 --- a/test/Tools/isac/Specify/calchead.sml Sat May 02 10:57:04 2020 +0200
16.2 +++ b/test/Tools/isac/Specify/calchead.sml Sat May 02 11:36:13 2020 +0200
16.3 @@ -150,7 +150,6 @@
16.4 ("DiffApp",["maximum_of","function"],
16.5 ["DiffApp","max_by_calculus"]);
16.6 val c = []:cid;
16.7 -(*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
16.8 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
16.9
16.10 val nxt = tac2tac_ pt p nxt;
16.11 @@ -228,7 +227,6 @@
16.12 val (dI',pI',mI') = empty_spec;
16.13 val c = []:cid;
16.14
16.15 -val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)
16.16 (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*)
16.17 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' []
16.18 EmptyPtree;