1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Fri Oct 25 20:52:08 2013 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri Oct 25 20:58:28 2013 +0100
1.3 @@ -308,7 +308,7 @@
1.4 crls : rls, (*for check_elementwise, ie. formulae in calc.*)
1.5 nrls : rls, (*canonical simplifier specific for this met *)
1.6 errpats : errpat list,(*error patterns expected in this method *)
1.7 - calc : calc list, (*040207: <--- calclist' in fun prep_met *)
1.8 + calc : calc list, (*Theory_Data in fun prep_met *)
1.9 (*branch : TransitiveB set in append_problem at generation ob pblobj
1.10 FIXXXME.0308: set branch from met in Apply_Method ? *)
1.11 ppc : pat list, (*.items in given, find, relate;
2.1 --- a/src/Tools/isac/KEStore.thy Fri Oct 25 20:52:08 2013 +0100
2.2 +++ b/src/Tools/isac/KEStore.thy Fri Oct 25 20:58:28 2013 +0100
2.3 @@ -71,20 +71,6 @@
2.4 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
2.5 "TODO exception hierarchy needs to be established.")
2.6
2.7 -(* fun assoc_calc calID = let
2.8 - fun ass ([], key) =
2.9 - error ("assoc_calc: '"^ key ^"' not found")
2.10 - | ass ((calc, (keyi, _)) :: pairs, key) =
2.11 - if key = keyi then calc else ass (pairs, key);
2.12 - in ass (!calclist', calID) end;
2.13 -
2.14 -fun assoc_calc' key' = let
2.15 - fun ass ([], key) =
2.16 - error ("assoc_calc': '" ^ key ^ "' not found")
2.17 - | ass ((all as (keyi, _)) :: pairs, key) =
2.18 - if key = keyi then all else ass (pairs, key);
2.19 - in ass (!calclist', key') end; *)
2.20 -
2.21 fun assoc_calc thy calID = let
2.22 fun ass ([], key) =
2.23 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Fri Oct 25 20:52:08 2013 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Fri Oct 25 20:58:28 2013 +0100
3.3 @@ -670,25 +670,6 @@
3.4 }:rls);
3.5 *)
3.6 "******* Atools.ML end *******";
3.7 -
3.8 -calclist':= overwritel (!calclist',
3.9 - [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
3.10 - ("some_occur_in",
3.11 - ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
3.12 - ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
3.13 - ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
3.14 - ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
3.15 - ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
3.16 - ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
3.17 - ("ident" ,("Atools.ident",eval_ident "#ident_")),
3.18 - ("equal" ,("HOL.eq",eval_equal "#equal_")),
3.19 - ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
3.20 - ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
3.21 - ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
3.22 - ("DIVIDE" ,("Fields.inverse_class.divide" ,eval_cancel "#divide_e")),
3.23 - ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
3.24 - ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
3.25 - ]);
3.26 *}
3.27 setup {* KEStore_Elems.add_calcs
3.28 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
4.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Oct 25 20:52:08 2013 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Oct 25 20:58:28 2013 +0100
4.3 @@ -9,7 +9,7 @@
4.4 text {* This theory collects data of theorems and axioms defined and used in ISAC *}
4.5
4.6 ML {*
4.7 - writeln ("======= length (KEStore_Elems = " ^
4.8 + (*writeln ("======= length (KEStore_Elems = " ^
4.9 string_of_int (length (KEStore_Elems.get_calcs @{theory})));
4.10 writeln ("======= length (! calclist') = " ^
4.11 string_of_int (length (! calclist')));
4.12 @@ -30,7 +30,7 @@
4.13 writeln "======= ! calclist' ordered =======";
4.14 ! calclist' |> rev (*!!!!!*)
4.15 |> map string_of_calc |> enumerate_strings |> sort string_ord |> map writeln;
4.16 - writeln "======= end ! calclist' =======";
4.17 + writeln "======= end ! calclist' =======";*)
4.18 *}
4.19
4.20 ML {*
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri Oct 25 20:52:08 2013 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Oct 25 20:58:28 2013 +0100
5.3 @@ -107,10 +107,6 @@
5.4 SOME ((term2str p) ^ " = " ^ term2str (primed t),
5.5 Trueprop $ (mk_equality (p, primed t)))
5.6 | eval_primed _ _ _ _ = NONE;
5.7 -
5.8 -calclist':= overwritel (!calclist',
5.9 - [("primed", ("Diff.primed", eval_primed "#primed"))
5.10 - ]);
5.11 *}
5.12 setup {* KEStore_Elems.add_calcs
5.13 [("primed", ("Diff.primed", eval_primed "#primed"))] *}
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Oct 25 20:52:08 2013 +0100
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Oct 25 20:58:28 2013 +0100
6.3 @@ -82,14 +82,6 @@
6.4 else SOME ((term2str p) ^ " = False",
6.5 Trueprop $ (mk_equality (p, @{term False})))
6.6 | eval_occur_exactly_in _ _ _ _ = NONE;
6.7 -
6.8 -calclist':=
6.9 -overwritel (!calclist',
6.10 - [("occur_exactly_in",
6.11 - ("EqSystem.occur'_exactly'_in",
6.12 - eval_occur_exactly_in "#eval_occur_exactly_in_"))
6.13 - ]);
6.14 -
6.15 *}
6.16 setup {* KEStore_Elems.add_calcs
6.17 [("occur_exactly_in",
7.1 --- a/src/Tools/isac/Knowledge/Equation.thy Fri Oct 25 20:52:08 2013 +0100
7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Fri Oct 25 20:58:28 2013 +0100
7.3 @@ -48,8 +48,6 @@
7.4 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
7.5 (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}
7.6 ML {*
7.7 -
7.8 -
7.9 store_pbt
7.10 (prep_pbt thy "pbl_equ" [] e_pblID
7.11 (["equation"],
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Oct 25 20:52:08 2013 +0100
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Oct 25 20:58:28 2013 +0100
8.3 @@ -107,12 +107,6 @@
8.4 else SOME ((term2str p) ^ " = False",
8.5 Trueprop $ (mk_equality (p, @{term False})))
8.6 | eval_is_f_x _ _ _ _ = NONE;
8.7 -
8.8 -calclist':= overwritel (!calclist',
8.9 - [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
8.10 - ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
8.11 - ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
8.12 - ]);
8.13 *}
8.14 setup {* KEStore_Elems.add_calcs
8.15 [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
9.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Oct 25 20:52:08 2013 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Oct 25 20:58:28 2013 +0100
9.3 @@ -86,11 +86,6 @@
9.4 *}
9.5
9.6 text {* store eval_ functions for calls from Scripts *}
9.7 -ML {*
9.8 -calclist':= overwritel (!calclist',
9.9 - [("drop_questionmarks", ("Partial_Fractions.drop'_questionmarks", eval_drop_questionmarks ""))
9.10 - ]);
9.11 -*}
9.12 setup {* KEStore_Elems.add_calcs
9.13 [("drop_questionmarks", ("Partial_Fractions.drop'_questionmarks", eval_drop_questionmarks ""))] *}
9.14
10.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Oct 25 20:52:08 2013 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Oct 25 20:58:28 2013 +0100
10.3 @@ -1582,18 +1582,6 @@
10.4 ("order_add_rls_", (Context.theory_name @{theory}, prep_rls order_add_rls_)),
10.5 ("make_rat_poly_with_parentheses",
10.6 (Context.theory_name @{theory}, prep_rls make_rat_poly_with_parentheses))] *}
10.7 -ML {*
10.8 -calclist':= overwritel (!calclist',
10.9 - [("is_polyrat_in", ("Poly.is'_polyrat'_in",
10.10 - eval_is_polyrat_in "#eval_is_polyrat_in")),
10.11 - ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
10.12 - ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
10.13 - ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
10.14 - ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
10.15 - ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
10.16 - ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
10.17 - ]);
10.18 -*}
10.19 setup {* KEStore_Elems.add_calcs
10.20 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
10.21 eval_is_polyrat_in "#eval_is_polyrat_in")),
11.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Fri Oct 25 20:52:08 2013 +0100
11.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Fri Oct 25 20:58:28 2013 +0100
11.3 @@ -230,12 +230,6 @@
11.4 ));
11.5 *}
11.6
11.7 -ML {*
11.8 -calclist':= overwritel (!calclist',
11.9 - [("is_ratequation_in", ("RatEq.is_ratequation_in",
11.10 - eval_is_ratequation_in ""))
11.11 - ]);
11.12 -*}
11.13 setup {* KEStore_Elems.add_calcs
11.14 [("is_ratequation_in", ("RatEq.is_ratequation_in", eval_is_ratequation_in ""))] *}
11.15
12.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Oct 25 20:52:08 2013 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Oct 25 20:58:28 2013 +0100
12.3 @@ -459,10 +459,7 @@
12.4 Trueprop $ (mk_equality (t, @{term True})))
12.5 else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
12.6 Trueprop $ (mk_equality (t, @{term False})))
12.7 - | eval_is_expanded _ _ _ _ = NONE;
12.8 -
12.9 -calclist':= overwritel (!calclist',
12.10 - [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))]);
12.11 + | eval_is_expanded _ _ _ _ = NONE;
12.12 *}
12.13 setup {* KEStore_Elems.add_calcs
12.14 [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))] *}
13.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri Oct 25 20:52:08 2013 +0100
13.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Oct 25 20:58:28 2013 +0100
13.3 @@ -80,11 +80,6 @@
13.4 > val Free (n1,t1) = arg;
13.5 > val SOME ni = int_of_str n1;
13.6 *)
13.7 -
13.8 -calclist':= overwritel (!calclist',
13.9 - [("SQRT" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_"))
13.10 - (*different types for 'sqrt 4' --- 'Calculate SQRT'*)
13.11 - ]);
13.12 *}
13.13 setup {* KEStore_Elems.add_calcs
13.14 [("SQRT", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))
14.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri Oct 25 20:52:08 2013 +0100
14.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri Oct 25 20:58:28 2013 +0100
14.3 @@ -642,15 +642,6 @@
14.4 " [no_met]) [BOOL e_e, REAL v_v])))"
14.5 ));
14.6 val --------------------------------------------------++++ = "44444";
14.7 -
14.8 -calclist':= overwritel (!calclist',
14.9 - [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
14.10 - eval_is_rootTerm_in"")),
14.11 - ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in",
14.12 - eval_is_sqrtTerm_in"")),
14.13 - ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in",
14.14 - eval_is_normSqrtTerm_in""))
14.15 - ]);(*("", ("", "")),*)
14.16 *}
14.17 setup {* KEStore_Elems.add_calcs
14.18 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),
15.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Fri Oct 25 20:52:08 2013 +0100
15.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Fri Oct 25 20:58:28 2013 +0100
15.3 @@ -184,10 +184,6 @@
15.4 " in (SubProblem (RootEq',[univariate,equation], " ^
15.5 " [no_met]) [BOOL e_e, REAL v_v]))"
15.6 ));
15.7 -calclist':= overwritel (!calclist',
15.8 - [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",
15.9 - eval_is_rootRatAddTerm_in""))
15.10 - ]);
15.11 *}
15.12 setup {* KEStore_Elems.add_calcs
15.13 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))] *}
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri Oct 25 20:52:08 2013 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Oct 25 20:58:28 2013 +0100
16.3 @@ -206,18 +206,7 @@
16.4 fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
16.5 SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
16.6 Trueprop $ (mk_equality (t, @{term True})))
16.7 - | eval_precond_rootpbl _ _ _ _ = NONE;
16.8 -
16.9 -calclist':= overwritel (!calclist',
16.10 - [("is_root_free", ("Test.is'_root'_free",
16.11 - eval_root_free"#is_root_free_e")),
16.12 - ("contains_root", ("Test.contains'_root",
16.13 - eval_contains_root"#contains_root_")),
16.14 - ("Test.precond'_rootmet", ("Test.precond'_rootmet",
16.15 - eval_precond_rootmet"#Test.precond_rootmet_")),
16.16 - ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
16.17 - eval_precond_rootpbl"#Test.precond_rootpbl_"))
16.18 - ]);
16.19 + | eval_precond_rootpbl _ _ _ _ = NONE;
16.20 *}
16.21 setup {* KEStore_Elems.add_calcs
16.22 [("is_root_free", ("Test.is'_root'_free", eval_root_free"#is_root_free_e")),
17.1 --- a/src/Tools/isac/ProgLang/Tools.thy Fri Oct 25 20:52:08 2013 +0100
17.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Fri Oct 25 20:58:28 2013 +0100
17.3 @@ -221,15 +221,6 @@
17.4 val list_rls = append_rls "list_rls" list_rls [Calc ("Tools.rhs", eval_rhs "")];
17.5 *}
17.6 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
17.7 -ML {*
17.8 -calclist':= overwritel (!calclist',
17.9 - [("matches",("Tools.matches",eval_matches "#matches_")),
17.10 - ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")),
17.11 - ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")),
17.12 - ("lhs" ,("Tools.lhs" ,eval_lhs "")),
17.13 - ("rhs" ,("Tools.rhs" ,eval_rhs ""))
17.14 - ]);
17.15 -*}
17.16 setup {* KEStore_Elems.add_calcs
17.17 [("matches", ("Tools.matches", eval_matches "#matches_")),
17.18 ("matchsub", ("Tools.matchsub", eval_matchsub "#matchsub_")),
18.1 --- a/src/Tools/isac/calcelems.sml Fri Oct 25 20:52:08 2013 +0100
18.2 +++ b/src/Tools/isac/calcelems.sml Fri Oct 25 20:58:28 2013 +0100
18.3 @@ -420,9 +420,6 @@
18.4 ("dummy_ord", dummy_ord)]);
18.5
18.6
18.7 -(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
18.8 -val calclist' = Unsynchronized.ref ([]: calc list);
18.9 -
18.10 (* A tree for storing data defined in different theories
18.11 for access from the Interpreter and from dialogue authoring
18.12 using a string list as key.