1.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Jul 18 15:48:54 2011 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Jul 18 16:37:30 2011 +0200
1.3 @@ -22,6 +22,9 @@
1.4 val ctxt = get_ctxt pt p;
1.5 val SOME known_x = parseNEW ctxt "x + y + z";
1.6 val SOME unknown = parseNEW ctxt "a + b + c";
1.7 + if type_of known_x = HOLogic.realT andalso
1.8 + type_of unknown = TFree ("'a",["Groups.plus"])
1.9 + then () else error "All_Ctx: type constraints beginning specification of root-problem ";
1.10 *}
1.11
1.12 ML {*
1.13 @@ -39,7 +42,8 @@
1.14 text {* preconditions are known at start of interpretation of (root-)method *}
1.15
1.16 ML {*
1.17 - get_assumptions_ pt p |> terms2strs;
1.18 + if terms2strs (get_assumptions_ pt p) = ["precond_rootmet x"]
1.19 + then () else error "All_Ctx: asms after start interpretation of root-method";
1.20 *}
1.21
1.22 ML {*
1.23 @@ -57,6 +61,9 @@
1.24 val ctxt = get_ctxt pt p;
1.25 val SOME known_x = parseNEW ctxt "x+y+z";
1.26 val SOME unknown = parseNEW ctxt "a+b+c";
1.27 + if type_of known_x = HOLogic.realT andalso
1.28 + type_of unknown = TFree ("'a",["Groups.plus"])
1.29 + then () else error "All_Ctx: type constraints beginning specification of SubProblem ";
1.30 *}
1.31
1.32 ML {*
1.33 @@ -75,7 +82,8 @@
1.34 text {* preconds are known at start of interpretation of (sub-)method *}
1.35
1.36 ML {*
1.37 - get_assumptions_ pt p |> terms2strs
1.38 + if terms2strs (get_assumptions_ pt p) = ["matches (?a = ?b) (-1 + x = 0)"]
1.39 + then () else error "All_Ctx: asms after start interpretation of SubProblem";
1.40 *}
1.41
1.42 ML {*
1.43 @@ -102,7 +110,9 @@
1.44 *}
1.45
1.46 ML {*
1.47 - terms2strs (get_assumptions_ pt p);
1.48 + if terms2strs (get_assumptions_ pt p) =
1.49 + ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
1.50 + then () else error "All_Ctx: asms after finishing SubProblem";
1.51 *}
1.52
1.53 ML {*
1.54 @@ -115,7 +125,9 @@
1.55 text {* assumptions collected during lucas-interpretation for proof of postcondition *}
1.56
1.57 ML {*
1.58 - terms2strs (get_assumptions_ pt p);
1.59 + if terms2strs (get_assumptions_ pt p) =
1.60 + ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
1.61 + then () else error "All_Ctx at final result";
1.62 *}
1.63
1.64 ML {*
2.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Jul 18 15:48:54 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon Jul 18 16:37:30 2011 +0200
2.3 @@ -346,5 +346,74 @@
2.4 ("Test", ["sqroot-test","univariate","equation","test"],
2.5 ["Test","squ-equ-test-subpbl1"]))];
2.6 Iterator 1;
2.7 - moveActiveRoot 1;
2.8 + moveActiveRoot 1;
2.9 +(*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
2.10 +"~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
2.11 +val pold = get_pos cI 1;
2.12 +(*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
2.13 + Type error in application: incompatible operand type
2.14 + Operator: solveFor :: real \<Rightarrow> una
2.15 + Operand: x :: 'a *)*)
2.16 +"~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
2.17 + = ([] : pos' list, pold, (get_calc cI), auto);
2.18 +autoord auto > 3 andalso just_created (pt, pos); (*true*)
2.19 +val ptp = all_modspec (pt, pos);
2.20 +"TODO all_modspec: preconds for rootpbl";
2.21 +(*all_solve auto c ptp; (*WAS Type unification failed...*)*)
2.22 +"~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
2.23 + (auto, c, ptp);
2.24 + val (_,_,mI) = get_obj g_spec pt p
2.25 + val ctxt = get_ctxt pt pos
2.26 + val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
2.27 +(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
2.28 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
2.29 + (auto, (c @ c'), ptp);
2.30 +p = ([], Res) (*false p = ([1], Frm)*);
2.31 +member op = [Pbl,Met] p_ (*false*);
2.32 +val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
2.33 +(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
2.34 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
2.35 + (auto, (c @ c'), ptp');
2.36 +p = ([], Res) (*false p = ([1], Res)*);
2.37 +member op = [Pbl,Met] p_ (*false*);
2.38 +val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
2.39 +(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
2.40 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
2.41 + (auto, (c @ c'), ptp');
2.42 +p = ([], Res) (*false p = ([2], Res)*);
2.43 +member op = [Pbl,Met] p_ (*false*);
2.44 +val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
2.45 +autoord auto < 5 (*false*);
2.46 +(* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
2.47 +"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
2.48 + val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
2.49 + val thy = assoc_thy dI;
2.50 + val {ppc, ...} = get_met mI;
2.51 +(* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
2.52 +val ctxt' = dI |> Thy_Info.get_theory |> ProofContext.init_global;
2.53 +(parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
2.54 + ^^^^^ *)
2.55 +(*vvv from: | assod pt _ (Subproblem'...*)
2.56 + val (fmz_, vals) = oris2fmz_vals pors;
2.57 +(**)
2.58 + val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global
2.59 + |> declare_constraints' vals
2.60 +(**)
2.61 +(*^^^ from: | assod pt _ (Subproblem'...*)
2.62 +val [(1, [1], "#Given", dsc_eq, [equality]),
2.63 + (2, [1], "#Given", dsc_solvefor, [xxx]),
2.64 + (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
2.65 +if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
2.66 +else error "autoCalculate..CompleteCalc: SubProblem broken 1";
2.67 + val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
2.68 + val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
2.69 + val pt = update_spec pt p (dI,pI,mI);
2.70 + val pt = update_ctxt pt p ctxt;
2.71 +"~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
2.72 +val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
2.73 +if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
2.74 +else error "autoCalculate..CompleteCalc: final result";
2.75 +if terms2strs (get_assumptions_ pt p) =
2.76 + ["matches (?a = ?b) (-1 + x = 0)", "x = 1", "precond_rootmet x"]
2.77 +then () else error "autoCalculate..CompleteCalc: ctxt at final result";
2.78
3.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jul 18 15:48:54 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Jul 18 16:37:30 2011 +0200
3.3 @@ -128,97 +128,6 @@
3.4 (*use "Interpret/solve.sml" !TODO*)
3.5 (*use "Interpret/inform.sml" !TODO*)
3.6 use "Interpret/mathengine.sml" (*!part.*)
3.7 -ML {*
3.8 -*}
3.9 -ML {*
3.10 -"----------- fun autoCalculate..CompleteCalc ------------";
3.11 - states:=[];
3.12 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.13 - ("Test", ["sqroot-test","univariate","equation","test"],
3.14 - ["Test","squ-equ-test-subpbl1"]))];
3.15 - Iterator 1;
3.16 - moveActiveRoot 1;
3.17 -(*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
3.18 -"~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
3.19 -val pold = get_pos cI 1;
3.20 -(*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
3.21 - Type error in application: incompatible operand type
3.22 - Operator: solveFor :: real \<Rightarrow> una
3.23 - Operand: x :: 'a *)*)
3.24 -"~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
3.25 - = ([] : pos' list, pold, (get_calc cI), auto);
3.26 -autoord auto > 3 andalso just_created (pt, pos); (*true*)
3.27 -val ptp = all_modspec (pt, pos);
3.28 -(*all_solve auto c ptp; (*WAS Type unification failed...*)*)
3.29 -"~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
3.30 - (auto, c, ptp);
3.31 - val (_,_,mI) = get_obj g_spec pt p
3.32 - val ctxt = get_ctxt pt pos
3.33 - val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
3.34 -(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
3.35 -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
3.36 - (auto, (c @ c'), ptp);
3.37 -p = ([], Res) (*false p = ([1], Frm)*);
3.38 -member op = [Pbl,Met] p_ (*false*);
3.39 -val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
3.40 -(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
3.41 -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
3.42 - (auto, (c @ c'), ptp');
3.43 -p = ([], Res) (*false p = ([1], Res)*);
3.44 -member op = [Pbl,Met] p_ (*false*);
3.45 -val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
3.46 -(* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
3.47 -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
3.48 - (auto, (c @ c'), ptp');
3.49 -p = ([], Res) (*false p = ([2], Res)*);
3.50 -member op = [Pbl,Met] p_ (*false*);
3.51 -val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
3.52 -autoord auto < 5 (*false*);
3.53 -(* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
3.54 -"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
3.55 - val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
3.56 - val thy = assoc_thy dI;
3.57 - val {ppc, ...} = get_met mI;
3.58 -(* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
3.59 -val ctxt' = dI |> Thy_Info.get_theory |> ProofContext.init_global;
3.60 -(parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]); *)
3.61 -(*vvv from: | assod pt _ (Subproblem'...*)
3.62 - val (fmz_, vals) = oris2fmz_vals pors;
3.63 - (*
3.64 - val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global
3.65 - |> declare_constraints' vals
3.66 -*)
3.67 -(*^^^ from: | assod pt _ (Subproblem'...*)
3.68 -val [(1, [1], "#Given", dsc_eq, [equality]),
3.69 - (2, [1], "#Given", dsc_solvefor, [xxx]),
3.70 - (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
3.71 -if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
3.72 -else error "autoCalculate..CompleteCalc: SubProblem broken 1";
3.73 - val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
3.74 - val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
3.75 - val pt = update_spec pt p (dI,pI,mI);
3.76 -*}
3.77 -ML {*
3.78 -p;
3.79 -pos;
3.80 - get_assumptions_ pt pos |> terms2strs;
3.81 -tac_;
3.82 -*}
3.83 -ML {*
3.84 -print_depth 999; Subproblem'; print_depth 999;
3.85 -*}
3.86 -ML {*
3.87 -print_depth 999; tac_; print_depth 999;
3.88 -*}
3.89 -ML {*
3.90 - val pt = update_ctxt pt p ctxt;
3.91 -"~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
3.92 -case complete_solve auto (c @ c') ptp of
3.93 - ("end-of-calculation",[],(_,([], Res))) => ()
3.94 -| _ => error "autoCalculate..CompleteCalc: SubProblem broken 2";
3.95 -*}
3.96 -
3.97 -
3.98 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
3.99 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
3.100 (*use "xmlsrc/mathml.sml" TODO*)