1.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Nov 21 17:31:20 2013 +0100
1.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Nov 21 18:12:17 2013 +0100
1.3 @@ -329,11 +329,11 @@
1.4 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.5 (*...copied from stac2tac_*)
1.6 str2term (
1.7 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.8 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
1.9 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.10 " REAL_LIST [c, c_2]]");
1.11 val ags = isalist2list ags';
1.12 -val pI = ["linear","system"];
1.13 +val pI = ["LINEAR","system"];
1.14 val pats = (#ppc o get_pbt) pI;
1.15 "-a1-----------------------------------------------------";
1.16 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
1.17 @@ -354,11 +354,11 @@
1.18 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.19 (*...copied from stac2tac_*)
1.20 str2term (
1.21 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.22 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
1.23 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.24 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
1.25 val ags = isalist2list ags';
1.26 -val pI = ["linear","system"];
1.27 +val pI = ["LINEAR","system"];
1.28 val pats = (#ppc o get_pbt) pI;
1.29 "-b1-----------------------------------------------------";
1.30 val xxx = match_ags @{theory "Isac"} pats ags;
1.31 @@ -380,10 +380,10 @@
1.32 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.33 (*...copied from stac2tac_*)
1.34 str2term (
1.35 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.36 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
1.37 " [REAL_LIST [c, c_2]]");
1.38 val ags = isalist2list ags';
1.39 -val pI = ["linear","system"];
1.40 +val pI = ["LINEAR","system"];
1.41 val pats = (#ppc o get_pbt) pI;
1.42 (*============ inhibit exn AK110726 ==============================================
1.43 val xxx - match_ags (theory "EqSystem") pats ags;
1.44 @@ -420,11 +420,11 @@
1.45 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.46 (*...copied from stac2tac_*)
1.47 str2term (
1.48 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.49 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
1.50 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.51 " REAL_LIST [c, c_2]]");
1.52 val ags = isalist2list ags';
1.53 -val pI = ["linear","system"];
1.54 +val pI = ["LINEAR","system"];
1.55 val pats = (#ppc o get_pbt) pI;
1.56 "-a1-----------------------------------------------------";
1.57 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
1.58 @@ -445,11 +445,11 @@
1.59 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.60 (*...copied from stac2tac_*)
1.61 str2term (
1.62 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.63 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
1.64 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
1.65 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
1.66 val ags = isalist2list ags';
1.67 -val pI = ["linear","system"];
1.68 +val pI = ["LINEAR","system"];
1.69 val pats = (#ppc o get_pbt) pI;
1.70 "-b1-----------------------------------------------------";
1.71 val xxx = match_ags @{theory "Isac"} pats ags;
1.72 @@ -471,10 +471,10 @@
1.73 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
1.74 (*...copied from stac2tac_*)
1.75 str2term (
1.76 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
1.77 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
1.78 " [REAL_LIST [c, c_2]]");
1.79 val ags = isalist2list ags';
1.80 -val pI = ["linear","system"];
1.81 +val pI = ["LINEAR","system"];
1.82 val pats = (#ppc o get_pbt) pI;
1.83 (*============ inhibit exn AK110726 ==============================================
1.84 val xxx - match_ags (theory "EqSystem") pats ags;
1.85 @@ -600,7 +600,7 @@
1.86 vars' ~~ vals;
1.87 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
1.88 (assoc (vars'~~vals, cy'));
1.89 -(*SOME (Free ("x", "RealDef.real")) : term option*)
1.90 +(*SOME (Free ("x", "Real.real")) : term option*)
1.91 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
1.92 (*x_i*)
1.93 "-----------------continue step through code match_ags---";
1.94 @@ -655,7 +655,7 @@
1.95 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
1.96 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
1.97 @{term "solution"}; type_of @{term "ss''' :: bool list"};
1.98 -(*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
1.99 +(*the model-pattern for ["LINEAR", "system"], is_copy_named are filter_out*)
1.100 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
1.101 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
1.102 (*the model specific for an example*)
1.103 @@ -704,32 +704,32 @@
1.104 probl = [], branch = TransitiveB,
1.105 origin =
1.106 ([(1, [1], "#Given",
1.107 - Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
1.108 + Const ("Descript.functionTerm", "Real.real => Tools.una"),
1.109 [Const ("op +",
1.110 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.111 + "["Real.real, "Real.real] => "Real.real") $
1.112 (Const ("Atools.pow",
1.113 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.114 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.115 - Free ("1", "RealDef.real")]),
1.116 + "["Real.real, "Real.real] => "Real.real") $
1.117 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
1.118 + Free ("1", "Real.real")]),
1.119 (2, [1], "#Given",
1.120 - Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
1.121 - [Free ("x", "RealDef.real")]),
1.122 + Const ("Integrate.integrateBy", "Real.real => Tools.una"),
1.123 + [Free ("x", "Real.real")]),
1.124 (3, [1], "#Find",
1.125 - Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
1.126 - [Free ("FF", "RealDef.real")])],
1.127 + Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
1.128 + [Free ("FF", "Real.real")])],
1.129 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
1.130 Const ("Integrate.Integrate",
1.131 - "(RealDef.real, RealDef.real) * => RealDef.real") $
1.132 + "("Real.real, "Real.real) * => "Real.real") $
1.133 (Const ("Product_Type.Pair",
1.134 - "[RealDef.real, RealDef.real]
1.135 - => (RealDef.real, RealDef.real) *") $
1.136 + "["Real.real, "Real.real]
1.137 + => ("Real.real, "Real.real) *") $
1.138 (Const ("op +",
1.139 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.140 + "["Real.real, "Real.real] => "Real.real") $
1.141 (Const ("Atools.pow",
1.142 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.143 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.144 - Free ("1", "RealDef.real")) $
1.145 - Free ("x", "RealDef.real"))),
1.146 + "["Real.real, "Real.real] => "Real.real") $
1.147 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
1.148 + Free ("1", "Real.real")) $
1.149 + Free ("x", "Real.real"))),
1.150 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
1.151 []) : ptree*)
1.152 "----- WN101007 worked until here (checked same as isac2002) ---";
1.153 @@ -765,44 +765,44 @@
1.154 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
1.155 [(0, [], false, "#Given",
1.156 Inc ((Const ("Descript.functionTerm",
1.157 - "RealDef.real => Tools.una"),[]),
1.158 + "Real.real => Tools.una"),[]),
1.159 (Const ("empty", "'a"), []))),
1.160 (0, [], false, "#Given",
1.161 Inc ((Const ("Integrate.integrateBy",
1.162 - "RealDef.real => Tools.una"),[]),
1.163 + "Real.real => Tools.una"),[]),
1.164 (Const ("empty", "'a"), []))),
1.165 (0, [], false, "#Find",
1.166 Inc ((Const ("Integrate.antiDerivative",
1.167 - "RealDef.real => Tools.una"),[]),
1.168 + "Real.real => Tools.una"),[]),
1.169 (Const ("empty", "'a"), [])))],
1.170 branch = TransitiveB, origin =
1.171 ([(1, [1], "#Given",
1.172 - Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
1.173 + Const ("Descript.functionTerm", "Real.real => Tools.una"),
1.174 [Const ("op +",
1.175 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.176 + "["Real.real, "Real.real] => "Real.real") $
1.177 (Const ("Atools.pow",
1.178 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.179 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.180 - Free ("1", "RealDef.real")]),
1.181 + "["Real.real, "Real.real] => "Real.real") $
1.182 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
1.183 + Free ("1", "Real.real")]),
1.184 (2, [1], "#Given",
1.185 - Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
1.186 - [Free ("x", "RealDef.real")]),
1.187 + Const ("Integrate.integrateBy", "Real.real => Tools.una"),
1.188 + [Free ("x", "Real.real")]),
1.189 (3, [1], "#Find",
1.190 - Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
1.191 - [Free ("FF", "RealDef.real")])],
1.192 + Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
1.193 + [Free ("FF", "Real.real")])],
1.194 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
1.195 Const ("Integrate.Integrate",
1.196 - "(RealDef.real, RealDef.real) * => RealDef.real") $
1.197 + "("Real.real, "Real.real) * => "Real.real") $
1.198 (Const ("Product_Type.Pair",
1.199 - "[RealDef.real, RealDef.real]
1.200 - => (RealDef.real, RealDef.real) *") $
1.201 + "["Real.real, "Real.real]
1.202 + => ("Real.real, "Real.real) *") $
1.203 (Const ("op +",
1.204 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.205 + "["Real.real, "Real.real] => "Real.real") $
1.206 (Const ("Atools.pow",
1.207 - "[RealDef.real, RealDef.real] => RealDef.real") $
1.208 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
1.209 - Free ("1", "RealDef.real")) $
1.210 - Free ("x", "RealDef.real"))),
1.211 + "["Real.real, "Real.real] => "Real.real") $
1.212 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
1.213 + Free ("1", "Real.real")) $
1.214 + Free ("x", "Real.real"))),
1.215 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
1.216 []) : ptree*)
1.217 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
1.218 @@ -825,8 +825,8 @@
1.219 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
1.220 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
1.221 (*#############################^^^^^^^^^ defined by Isabelle*)
1.222 - (2, [1], "#Find", Const ("Simplify.normalform", _ (*"RealDef.real \<Rightarrow> Tools.una"*)),
1.223 - [Free ("N", _ (*"RealDef.real"*))])],
1.224 + (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
1.225 + [Free ("N", _ (*"Real.real"*))])],
1.226 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
1.227 "#undef means: the element with description TERM in fmz did not match ";
1.228 "with any element of pbl (fetched by pI), because there we have Simplify.Term";