1.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 09:07:36 2020 +0200
1.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 13:33:23 2020 +0200
1.3 @@ -6,7 +6,7 @@
1.4 "table of contents -----------------------------------------------------------------------------";
1.5 "-----------------------------------------------------------------------------------------------";
1.6 "----------- go through Model_Problem until nxt_tac --------------------------------------------";
1.7 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
1.8 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
1.9 "----------- type penv -------------------------------------------------------------------------";
1.10 "----------- fun untouched ---------------------------------------------------------------------";
1.11 "----------- fun pbl_ids -----------------------------------------------------------------------";
1.12 @@ -79,8 +79,8 @@
1.13 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
1.14 val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
1.15 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
1.16 -val (d, ts) = split_dts t;
1.17 -"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
1.18 +val (d, ts) = I_Model.split_dts t;
1.19 +"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
1.20 (*if is_dsc d then () else error "TODO";*)
1.21 if is_dsc d then () else error "TODO";
1.22 "----- these were the errors (call hierarchy from bottom up)";
1.23 @@ -96,60 +96,60 @@
1.24 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
1.25 ========== inhibit exn AK110725 ================================================*)
1.26
1.27 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
1.28 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
1.29 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
1.30 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
1.31 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
1.32 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
1.33 (*val t = str2term "maximum A";
1.34 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.35 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.36 val it = "maximum A" : cterm
1.37 > val t = str2term "fixedValues [r=Arbfix]";
1.38 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.39 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.40 "fixedValues [r = Arbfix]"
1.41 > val t = str2term "valuesFor [a]";
1.42 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.43 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.44 "valuesFor [a]"
1.45 > val t = str2term "valuesFor [a,b]";
1.46 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.47 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.48 "valuesFor [a, b]"
1.49 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
1.50 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.51 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.52 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
1.53 > val t = str2term "boundVariable a";
1.54 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.55 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.56 "boundVariable a"
1.57 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
1.58 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.59 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.60 "interval {x. 0 <= x & x <= 2 * r}"
1.61
1.62 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
1.63 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.64 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.65 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
1.66 > val t = str2term "solveFor x";
1.67 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.68 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.69 "solveFor x"
1.70 > val t = str2term "errorBound (eps=0)";
1.71 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.72 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.73 "errorBound (eps = 0)"
1.74 > val t = str2term "solutions L";
1.75 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
1.76 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
1.77 "solutions L"
1.78
1.79 before 6.5.03:
1.80 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
1.81 -> val (d,ts) = split_dts t;
1.82 +> val (d,ts) = I_Model.split_dts t;
1.83 > comp_dts thy (d,ts);
1.84 val it = "testdscforlist [#1]" : cterm
1.85
1.86 > val t = (Thm.term_of o the o (parse thy)) "(A::real)";
1.87 -> val (d,ts) = split_dts t;
1.88 +> val (d,ts) = I_Model.split_dts t;
1.89 val d = Const ("empty","empty") : term
1.90 val ts = [Free ("A","RealDef.real")] : term list
1.91 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";
1.92 -> val (d,ts) = split_dts t;
1.93 +> val (d,ts) = I_Model.split_dts t;
1.94 val d = Const ("empty","empty") : term
1.95 val ts = [Const # $ Free # $ Free (#,#)] : term list
1.96 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";
1.97 -> val (d,ts) = split_dts t;
1.98 +> val (d,ts) = I_Model.split_dts t;
1.99 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
1.100 *)
1.101 "----------- type penv -------------------------------------------------------------------------";
1.102 @@ -189,7 +189,7 @@
1.103
1.104 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
1.105 val (d,argl) = strip_comb t;
1.106 - is_dsc d; (*see split_dts*)
1.107 + is_dsc d; (*see I_Model.split_dts*)
1.108 dest_list (d,argl);
1.109 val (_ $ v) = t;
1.110 is_list v;
1.111 @@ -197,7 +197,7 @@
1.112 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
1.113 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
1.114
1.115 - val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
1.116 + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
1.117 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term
1.118 val vl = Free ("x","RealDef.real") : term
1.119
1.120 @@ -205,7 +205,7 @@
1.121 pbl_ids ctxt dsc vl;
1.122 val it = [Free ("x","RealDef.real")] : term list
1.123
1.124 - val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy))
1.125 + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy))
1.126 "errorBound (eps=#0)";
1.127 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";
1.128 pbl_ids ctxt dsc vl;