1.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Sun Oct 09 06:53:03 2022 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Sun Oct 09 07:44:22 2022 +0200
1.3 @@ -103,7 +103,7 @@
1.4 "ctree.sml-------------- cut_tree new (from ctree above)----------";
1.5 val (pt', cuts) = cut_tree pt ([1],Frm);
1.6 "ctree.sml-------------- cappend on complete ctree from above ----";
1.7 -val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (TermC.str2term "Inform[1]");
1.8 +val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (TermC.parse_test @{context} "Inform[1]");
1.9 "----------------------------------------------------------------/";
1.10
1.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
1.12 @@ -419,7 +419,7 @@
1.13 "-------------- cappend (from ctree above)------------------------";
1.14 "-------------- cappend (from ctree above)------------------------";
1.15 "-------------- cappend (from ctree above)------------------------";
1.16 -val (pt',cuts) = cappend_form pt [3,2,1] Istate.empty (TermC.str2term "newnew");
1.17 +val (pt',cuts) = cappend_form pt [3,2,1] Istate.empty (TermC.parse_test @{context} "newnew");
1.18 if cuts = [([3, 2, 1], Res),
1.19 ([3, 2, 2], Res),
1.20 ([3, 2], Res),
1.21 @@ -432,8 +432,8 @@
1.22 UnparseC.term (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
1.23 then () else error "ctree.sml: diff:behav. in cappend 1";
1.24
1.25 -val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.str2term "newform")
1.26 - (Tac "test") (TermC.str2term "newresult",[]) Complete;
1.27 +val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.parse_test @{context} "newform")
1.28 + (Tac "test") (TermC.parse_test @{context} "newresult",[]) Complete;
1.29 if cuts = [([3, 2, 1], Res), (*?????????????*)
1.30 ([3, 2, 2], Res),
1.31 ([3, 2], Res),
1.32 @@ -471,7 +471,7 @@
1.33
1.34 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
1.35 val p = ([1], Frm);
1.36 -val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.str2term "x + 1 = 2");
1.37 +val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 = 2");
1.38 val form = get_obj g_form pt (fst p);
1.39 val (res,_) = get_obj g_result pt (fst p);
1.40 if UnparseC.term form = "x + 1 = 2" andalso res = TermC.empty then () else
1.41 @@ -482,8 +482,8 @@
1.42 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
1.43 val p = ([1], Res);
1.44 val (pt,cuts) =
1.45 - cappend_atomic pt (fst p) Istate.empty (TermC.str2term "x + 1 = 2")
1.46 - Empty_Tac (TermC.str2term "x + 1 + - 1 * 2 = 0",[]) Incomplete;
1.47 + cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 = 2")
1.48 + Empty_Tac (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0",[]) Incomplete;
1.49 val form = get_obj g_form pt (fst p);
1.50 val (res,_) = get_obj g_result pt (fst p);
1.51 if UnparseC.term form = "x + 1 = 2" andalso UnparseC.term res = "x + 1 + - 1 * 2 = 0"
1.52 @@ -494,8 +494,8 @@
1.53 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
1.54 val p = ([2], Res);
1.55 val (pt,cuts) =
1.56 - cappend_atomic pt (fst p) Istate.empty (TermC.str2term "x + 1 + - 1 * 2 = 0")
1.57 - Empty_Tac (TermC.str2term "- 1 + x = 0",[]) Incomplete;
1.58 + cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0")
1.59 + Empty_Tac (TermC.parse_test @{context} "- 1 + x = 0",[]) Incomplete;
1.60 val form = get_obj g_form pt (fst p);
1.61 val (res,_) = get_obj g_result pt (fst p);
1.62 if UnparseC.term form = "x + 1 + - 1 * 2 = 0" andalso UnparseC.term res = "- 1 + x = 0"
1.63 @@ -516,7 +516,7 @@
1.64
1.65 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
1.66 val p = ([3, 1], Frm);
1.67 -val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.str2term "- 1 + x = 0");
1.68 +val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.parse_test @{context} "- 1 + x = 0");
1.69 val form = get_obj g_form pt (fst p);
1.70 val (res,_) = get_obj g_result pt (fst p);
1.71 if UnparseC.term form = "- 1 + x = 0" andalso res = TermC.empty then () else
1.72 @@ -527,8 +527,8 @@
1.73 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
1.74 val p = ([3, 1], Res);
1.75 val (pt,cuts) =
1.76 - cappend_atomic pt (fst p) Istate.empty (TermC.str2term "- 1 + x = 0")
1.77 - Empty_Tac (TermC.str2term "x = 0 + - 1 * - 1",[]) Incomplete;
1.78 + cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "- 1 + x = 0")
1.79 + Empty_Tac (TermC.parse_test @{context} "x = 0 + - 1 * - 1",[]) Incomplete;
1.80 val form = get_obj g_form pt (fst p);
1.81 val (res,_) = get_obj g_result pt (fst p);
1.82 if UnparseC.term form = "- 1 + x = 0" andalso UnparseC.term res = "x = 0 + - 1 * - 1" then()
1.83 @@ -1160,8 +1160,8 @@
1.84 "---(2) on S(606)..S(608)--------";
1.85 (*========== inhibit exn AK110726 ==============================================
1.86 (* ERROR: Can't unify istate to istate * Proof.context *)
1.87 -val (pt', cuts) = cappend_atomic pt [1] Istate.empty (TermC.str2term "Inform[1]")
1.88 - (Tac "test") (TermC.str2term "Inres[1]",[]) Complete;
1.89 +val (pt', cuts) = cappend_atomic pt [1] Istate.empty (TermC.parse_test @{context} "Inform[1]")
1.90 + (Tac "test") (TermC.parse_test @{context} "Inres[1]",[]) Complete;
1.91
1.92 (*default_print_depth 99;*)
1.93 cuts;
1.94 @@ -1182,8 +1182,8 @@
1.95 Test_Tool.show_pt pt';
1.96 "---(3) on S(606)..S(608)--------";
1.97 Test_Tool.show_pt pt;
1.98 -val (pt', cuts) = cappend_atomic pt [2] Istate.empty (TermC.str2term "Inform[2]")
1.99 - (Tac "test") (TermC.str2term "Inres[2]",[]) Complete;
1.100 +val (pt', cuts) = cappend_atomic pt [2] Istate.empty (TermC.parse_test @{context} "Inform[2]")
1.101 + (Tac "test") (TermC.parse_test @{context} "Inres[2]",[]) Complete;
1.102 (*default_print_depth 99;*)
1.103 cuts;
1.104 (*default_print_depth 3;*)
1.105 @@ -1220,7 +1220,7 @@
1.106
1.107 "---(4) on S(606)..S(608)--------";
1.108 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],References.empty)
1.109 - ([],References.empty, TermC.str2term "Inhead[3]", ContextC.empty);
1.110 + ([],References.empty, TermC.parse_test @{context} "Inhead[3]", ContextC.empty);
1.111 (*default_print_depth 99;*)
1.112 cuts;
1.113 (*default_print_depth 3;*)
1.114 @@ -1245,8 +1245,8 @@
1.115 *)
1.116
1.117 "---(6- 1) on S(606)..S(608)--------";
1.118 -val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (TermC.str2term "Inform[3,1]")
1.119 - (Tac "test") (TermC.str2term "Inres[3,1]",[]) Complete;
1.120 +val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (TermC.parse_test @{context} "Inform[3,1]")
1.121 + (Tac "test") (TermC.parse_test @{context} "Inres[3,1]",[]) Complete;
1.122 (*default_print_depth 99;*)
1.123 cuts;
1.124 (*default_print_depth 3;*)
1.125 @@ -1271,8 +1271,8 @@
1.126 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1.127
1.128 "---(6) on S(606)..S(608)--------";
1.129 -val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (TermC.str2term "Inform[3,2]")
1.130 - (Tac "test") (TermC.str2term "Inres[3,2]",[]) Complete;
1.131 +val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (TermC.parse_test @{context} "Inform[3,2]")
1.132 + (Tac "test") (TermC.parse_test @{context} "Inres[3,2]",[]) Complete;
1.133 (*default_print_depth 99;*)
1.134 cuts;
1.135 (*default_print_depth 3;*)
1.136 @@ -1296,8 +1296,8 @@
1.137
1.138 "---(6++) on S(606)..S(608)--------";
1.139 (**)
1.140 -val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.str2term "Inform[3,2,1]")
1.141 - (Tac "test") (TermC.str2term "Inres[3,2,1]",[]) Complete;
1.142 +val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.parse_test @{context} "Inform[3,2,1]")
1.143 + (Tac "test") (TermC.parse_test @{context} "Inres[3,2,1]",[]) Complete;
1.144 (*default_print_depth 99;*)
1.145 cuts;
1.146 (*default_print_depth 1;*)