1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Apr 09 14:41:41 2012 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Apr 10 09:31:31 2012 +0200
1.3 @@ -72,4 +72,5 @@
1.4 ML {* check_guhs_unique := false; *}
1.5 ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
1.6 ML {* @{theory "Isac"} *}
1.7 +ML {* ! isab_thm_thy *}
1.8 end
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Apr 09 14:41:41 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Apr 10 09:31:31 2012 +0200
2.3 @@ -459,53 +459,47 @@
2.4 end;
2.5
2.6
2.7 -(*.which theory below thy' contains a ruleset;
2.8 -get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
2.9 -(* val (thy', rls') = ("PolyEq", "separate_bdv");
2.10 - *)
2.11 +(* which theory in ancestors of thy' contains a ruleset;
2.12 + i.e. get the occurence _after_ in the _list_ (is up to asking TUM) theory' *)
2.13 local infix mem; (*from Isabelle2002*)
2.14 fun x mem [] = false
2.15 | x mem (y :: ys) = x = y orelse x mem ys;
2.16 in
2.17 fun thy_containing_rls (thy':theory') (rls':rls') =
2.18 - let val rls' = strip_thy rls'
2.19 - val thy' = thyID2theory' thy'
2.20 - (*take thys between "Isac" and thy' not to search #1#*)
2.21 - val dropthys = takewhile [] (not o (curry op= thy') o
2.22 - (#1:theory' * theory -> theory'))
2.23 - (rev (!theory'))
2.24 - val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
2.25 - dropthys
2.26 - (*drop those rulesets which are generated in a theory found in #1#*)
2.27 - val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
2.28 - ((#1 o #2) : rls' * (theory' * rls)
2.29 - -> theory'))
2.30 - (rev (!ruleset'))
2.31 - in case assoc (startsearch, rls') of
2.32 - SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
2.33 - | _ => error ("thy_containing_rls : rls '"^rls'^
2.34 - "' not in !rulset' above thy '"^thy'^"'")
2.35 - end;
2.36 -(* val (thy', termop) = (thyID, termop);
2.37 - *)
2.38 + let
2.39 + val rls' = strip_thy rls'
2.40 + val thy' = thyID2theory' thy'
2.41 + (*take thys between "Isac" and thy' excluding search for #1#--see calcelems.sml*)
2.42 + val dropthys =
2.43 + takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
2.44 + (rev (!theory'))
2.45 + val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
2.46 + (*drop those rulesets which are generated in a theory found in #1#*)
2.47 + val ancestors_rls =
2.48 + filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
2.49 + (rev (!ruleset'))
2.50 + in case assoc (ancestors_rls, rls') of
2.51 + SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
2.52 + | _ => error ("thy_containing_rls : rls '" ^ rls' ^
2.53 + "' not in !rulset' of ancestors of thy '" ^ thy' ^ "'")
2.54 + end;
2.55 +
2.56 fun thy_containing_cal (thy':theory') termop =
2.57 - let val thy' = thyID2theory' thy'
2.58 - val dropthys = takewhile [] (not o (curry op= thy') o
2.59 - (#1:theory' * theory -> theory'))
2.60 - (rev (!theory'))
2.61 - val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
2.62 - dropthys
2.63 - val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
2.64 - (#1 : calc -> string)) (rev (!calclist'))
2.65 - in case assoc (startsearch, strip_thy termop) of
2.66 - SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
2.67 - | _ => error ("thy_containing_rls : rls '"^termop^
2.68 - "' not in !calclist' above thy '"^thy'^"'")
2.69 - end
2.70 -end;
2.71 -
2.72 -(* print_depth 99; map #1 startsearch; print_depth 3;
2.73 - *)
2.74 + let
2.75 + val thy' = thyID2theory' thy'
2.76 + val dropthys =
2.77 + takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
2.78 + (rev (!theory'))
2.79 + val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
2.80 + val ancestors_cal =
2.81 + filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
2.82 + (rev (!calclist'))
2.83 + in case assoc (ancestors_cal, strip_thy termop) of
2.84 + SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
2.85 + | _ => error ("thy_containing_cal : rls '" ^ termop ^
2.86 + "' not in ! calclist' of ancestors of thy '" ^ thy' ^ "'")
2.87 + end
2.88 +end; (*local*)
2.89
2.90 (*.packing return-values to matchTheory, contextToThy for xml-generation.*)
2.91 datatype contthy = (*also an item from KEStore on Browser ......#*)
3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Apr 09 14:41:41 2012 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Tue Apr 10 09:31:31 2012 +0200
3.3 @@ -14,13 +14,15 @@
3.4 (*local*)
3.5 val first_ProgLang_thy = @{theory ListC}
3.6 val first_Knowledge_thy = @{theory Delete} (*see WN120321.TODO rearrange theories*)
3.7 - val allthys = Theory.ancestors_of @{theory}; (* with Isac.thy on top *)
3.8 + val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};
3.9 val isabthys' =
3.10 drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
3.11 + val isacthys' =
3.12 + take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
3.13 val knowthys' =
3.14 - take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
3.15 - val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
3.16 - drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) knowthys') + 1 +3, knowthys');
3.17 + take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');
3.18 + val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
3.19 + drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');
3.20
3.21 val isacrlsthms = ! ruleset'
3.22 |> map (thms_of_rls o #2 o #2)
3.23 @@ -31,14 +33,13 @@
3.24 |> map (apfst Thm.get_name_hint)
3.25 |> map (apsnd prop_of) (*this adapts to Theory.axioms_of*)
3.26 : (thmDeriv * term) list;
3.27 - val isacthys = union Theory.eq_thy knowthys' progthys'
3.28 val isacthms =
3.29 - (flat o (map Theory.axioms_of)) isacthys: (thmDeriv * term) list;
3.30 + (flat o (map Theory.axioms_of)) isacthys': (thmDeriv * term) list;
3.31 (*in*)
3.32 isabthys := isabthys';
3.33 knowthys := knowthys';
3.34 progthys := progthys';
3.35 - theory' := (map Context.theory_name isacthys) ~~ isacthys; (*WN120320 easy to remove*)
3.36 + theory' := rev ((map Context.theory_name isacthys') ~~ isacthys'); (*WN120320 easy to remove*)
3.37 val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
3.38 (*end;*)
3.39 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:
4.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Apr 09 14:41:41 2012 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Apr 10 09:31:31 2012 +0200
4.3 @@ -58,12 +58,14 @@
4.4 (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
4.5 store_pbt
4.6 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
4.7 - (["inverse", "Z_Transform", "SignalProcessing"],
4.8 + (["Inverse", "Z_Transform", "SignalProcessing"],
4.9 + (*^ capital letter breaks coding standard
4.10 + because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
4.11 [("#Given" ,["filterExpression (X_eq::bool)"]),
4.12 ("#Find" ,["stepResponse (n_eq::bool)"])
4.13 ],
4.14 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
4.15 - [["SignalProcessing","Z_Transform","inverse"]]));
4.16 + [["SignalProcessing","Z_Transform","Inverse"]]));
4.17 *}
4.18
4.19 subsection {*Define Name and Signature for the Method*}
4.20 @@ -86,7 +88,7 @@
4.21 val thy = @{theory}; (*latest version of thy required*)
4.22 store_met
4.23 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
4.24 - (["SignalProcessing", "Z_Transform", "inverse"],
4.25 + (["SignalProcessing", "Z_Transform", "Inverse"],
4.26 [("#Given" ,["filterExpression (X_eq::bool)"]),
4.27 ("#Find" ,["stepResponse (n_eq::bool)"])
4.28 ],
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Apr 09 14:41:41 2012 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Apr 10 09:31:31 2012 +0200
5.3 @@ -509,50 +509,47 @@
5.4 ^^^*)
5.5
5.6 val discard_minus =
5.7 - Rls{id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
5.8 + Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
5.9 erls = e_rls, srls = Erls, calc = [],
5.10 - (*asm_thm = [],*)
5.11 - rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
5.12 - (*"a - b = a + -1 * b"*)
5.13 - Thm ("sym_real_mult_minus1",
5.14 - num_str (@{thm real_mult_minus1} RS @{thm sym}))
5.15 - (*- ?z = "-1 * ?z"*)
5.16 - ], scr = EmptyScr}:rls;
5.17 + rules =
5.18 + [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),
5.19 + (*"a - b = a + -1 * b"*)
5.20 + Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym}))
5.21 + (*- ?z = "-1 * ?z"*)],
5.22 + scr = EmptyScr}:rls;
5.23
5.24 val expand_poly_ =
5.25 Rls{id = "expand_poly_", preconds = [],
5.26 rew_ord = ("dummy_ord", dummy_ord),
5.27 erls = e_rls,srls = Erls,
5.28 calc = [],
5.29 - (*asm_thm = [],*)
5.30 - rules = [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),
5.31 - (*"(a + b)^^^4 = ... "*)
5.32 - Thm ("real_plus_binom_pow5",num_str @{thm real_plus_binom_pow5}),
5.33 - (*"(a + b)^^^5 = ... "*)
5.34 - Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
5.35 - (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
5.36 - (*WN071229 changed/removed for Schaerding -----vvv*)
5.37 - (*Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),*)
5.38 - (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
5.39 - Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
5.40 - (*"(a + b)^^^2 = (a + b) * (a + b)"*)
5.41 - (*Thm ("real_plus_minus_binom1_p_p",
5.42 - num_str @{thm real_plus_minus_binom1_p_p}),*)
5.43 - (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
5.44 - (*Thm ("real_plus_minus_binom2_p_p",
5.45 - num_str @{thm real_plus_minus_binom2_p_p}),*)
5.46 - (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
5.47 - (*WN071229 changed/removed for Schaerding -----^^^*)
5.48 + rules =
5.49 + [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),
5.50 + (*"(a + b)^^^4 = ... "*)
5.51 + Thm ("real_plus_binom_pow5",num_str @{thm real_plus_binom_pow5}),
5.52 + (*"(a + b)^^^5 = ... "*)
5.53 + Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
5.54 + (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
5.55 + (*WN071229 changed/removed for Schaerding -----vvv*)
5.56 + (*Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),*)
5.57 + (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
5.58 + Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
5.59 + (*"(a + b)^^^2 = (a + b) * (a + b)"*)
5.60 + (*Thm ("real_plus_minus_binom1_p_p", num_str @{thm real_plus_minus_binom1_p_p}),*)
5.61 + (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
5.62 + (*Thm ("real_plus_minus_binom2_p_p", num_str @{thm real_plus_minus_binom2_p_p}),*)
5.63 + (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
5.64 + (*WN071229 changed/removed for Schaerding -----^^^*)
5.65
5.66 - Thm ("left_distrib" ,num_str @{thm left_distrib}),
5.67 - (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
5.68 - Thm ("right_distrib",num_str @{thm right_distrib}),
5.69 - (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
5.70 + Thm ("left_distrib" ,num_str @{thm left_distrib}),
5.71 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
5.72 + Thm ("right_distrib",num_str @{thm right_distrib}),
5.73 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
5.74
5.75 - Thm ("realpow_multI", num_str @{thm realpow_multI}),
5.76 - (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
5.77 - Thm ("realpow_pow",num_str @{thm realpow_pow})
5.78 - (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
5.79 + Thm ("realpow_multI", num_str @{thm realpow_multI}),
5.80 + (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
5.81 + Thm ("realpow_pow",num_str @{thm realpow_pow})
5.82 + (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
5.83 ], scr = EmptyScr}:rls;
5.84
5.85 (*.the expression contains + - * ^ only ?
5.86 @@ -1513,7 +1510,7 @@
5.87 (*.a minimal ruleset for reverse rewriting of factions [2];
5.88 compare expand_binoms.*)
5.89 val rev_rew_p =
5.90 -Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
5.91 +Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
5.92 erls = Atools_erls, srls = Erls,
5.93 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
5.94 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
5.95 @@ -1602,8 +1599,7 @@
5.96 ("discard_parentheses1",prep_rls discard_parentheses1),
5.97 ("order_mult_rls_", prep_rls order_mult_rls_),
5.98 ("order_add_rls_", prep_rls order_add_rls_),
5.99 - ("make_rat_poly_with_parentheses",
5.100 - prep_rls make_rat_poly_with_parentheses)
5.101 + ("make_rat_poly_with_parentheses", prep_rls make_rat_poly_with_parentheses)
5.102 ]);
5.103
5.104 calclist':= overwritel (!calclist',
6.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Apr 09 14:41:41 2012 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Apr 10 09:31:31 2012 +0200
6.3 @@ -3477,15 +3477,14 @@
6.4 discard binary minus, shift unary minus into -1*;
6.5 unary minus before numerals are put into the numeral by parsing;
6.6 contains absolute minimum of thms for context in norm_Rational
6.7 -val discard_minus = prep_rls(
6.8 +*** val discard_minus = prep_rls(
6.9 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
6.10 erls = e_rls, srls = Erls, calc = [],
6.11 - rules = [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),
6.12 - (*"a - b = a + -1 * b"*)
6.13 - Thm ("sym_real_mult_minus1",
6.14 - num_str (@{thm real_mult_minus1} RS @{thm sym}))
6.15 - (*- ?z = "-1 * ?z"*)
6.16 - ],
6.17 + rules =
6.18 + [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),
6.19 + (*"a - b = a + -1 * b"*)
6.20 + Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym}))
6.21 + (*- ?z = "-1 * ?z"*)],
6.22 scr = EmptyScr
6.23 }):rls;
6.24 *)
6.25 @@ -3788,7 +3787,7 @@
6.26 ("common_nominator_p", common_nominator_p),
6.27 ("common_nominator_p_rls", common_nominator_p_rls),
6.28 ("common_nominator" , common_nominator),
6.29 - ("discard_minus", discard_minus),
6.30 + (*WN120410 ("discard_minus", discard_minus), is defined in Poly.thy*)
6.31 ("powers_erls", powers_erls),
6.32 ("powers", powers),
6.33 ("rat_mult_divide", rat_mult_divide),
7.1 --- a/src/Tools/isac/TODO.txt Mon Apr 09 14:41:41 2012 +0200
7.2 +++ b/src/Tools/isac/TODO.txt Tue Apr 10 09:31:31 2012 +0200
7.3 @@ -16,6 +16,12 @@
7.4 This list is started to record TODOs wich can NOT be done
7.5 before all tests are RUNNING.
7.6
7.7 +WN120314
7.8 +Now ctxt seems settled, and tests are made running in reverse order,
7.9 +from last (except isac.sml) to previous in Test.Isac.thy.
7.10 +TODOs arise from the necessity to produce an ISAC kernel which can be
7.11 +connected with the Java-Frontend asap (for gdaroczy, jrocnik).
7.12 +
7.13 ############## WNxxxxxx.TODO can be found in sources ##############
7.14
7.15 --------------------------------------------------------------------------------
7.16 @@ -123,7 +129,7 @@
7.17 ["diff","integration"]
7.18 ["diff","integration","named"]
7.19 Inverse_Z_Transform
7.20 - ["SignalProcessing", "Z_Transform", "inverse"]
7.21 + ["SignalProcessing", "Z_Transform", "Inverse"]
7.22 Isac //
7.23 LinEq //
7.24 LogExp //
7.25 @@ -198,7 +204,12 @@
7.26 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
7.27 test --- the_hier (! thehier) (collect_thydata ())---
7.28 --------------------------------------------------------------------------------
7.29 +WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
7.30 +!!add mutual crossreferences to ?fun headline??? where the same has to be done:
7.31 +!!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
7.32 --------------------------------------------------------------------------------
7.33 +WN120409.TODO replace "op mem" (2002) with member (2011) ...
7.34 +... an exercise interesting exercise !
7.35 --------------------------------------------------------------------------------
7.36 --------------------------------------------------------------------------------
7.37
8.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Mon Apr 09 14:41:41 2012 +0200
8.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Tue Apr 10 09:31:31 2012 +0200
8.3 @@ -172,20 +172,14 @@
8.4 (*.for creating a href for a rule within an rls's rule list;
8.5 the guh points to the thy of definition of the rule, NOT of use in rls.*)
8.6 fun rule2xml j (thyID:thyID) Erule =
8.7 - error "rule2xml called with 'Erule'"
8.8 -(* val (j, thyID, Thm (thmID, thm)) = (j+i, thyID, nth 1 rules);
8.9 - val (j, thyID, Thm (thmID, thm)) = (j, thyID,r);
8.10 - *)
8.11 + error "rule2xml called with 'Erule'"
8.12 | rule2xml j thyID (Thm (thmDeriv, thm)) =
8.13 - indt j ^ "<RULE>\n" ^
8.14 - indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
8.15 - indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
8.16 - indt (j+i) ^ "<GUH> " ^
8.17 - thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
8.18 - indt j ^ "</RULE>\n" : xml
8.19 -(* val (j, thyID, Calc (termop, _)) = (j+i, thyID, nth 42 rules);
8.20 - val (j, thyID, Calc (termop, _)) = (j+i, thyID, nth 43 rules);
8.21 - *)
8.22 + indt j ^ "<RULE>\n" ^
8.23 + indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
8.24 + indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
8.25 + indt (j+i) ^ "<GUH> " ^
8.26 + thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
8.27 + indt j ^ "</RULE>\n" : xml
8.28 | rule2xml j thyID (Calc (termop, _)) = ""
8.29 (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
8.30 see smltest/../datatypes.sml !
8.31 @@ -197,16 +191,15 @@
8.32 *)
8.33 | rule2xml j thyID (Cal1 (termop, _)) = ""
8.34 | rule2xml j thyID (Rls_ rls) =
8.35 - let val rls' = (#id o rep_rls) rls
8.36 - in indt j ^ "<RULE>\n" ^
8.37 - indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
8.38 - indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
8.39 - indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls')
8.40 - rls' ^ " </GUH>\n" ^
8.41 - indt j ^ "</RULE>\n"
8.42 - end;
8.43 -(* val (j, thyID, r::rs) = (2, "Test", rules);
8.44 - *)
8.45 + let val rls' = (#id o rep_rls) rls
8.46 + in
8.47 + indt j ^ "<RULE>\n" ^
8.48 + indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
8.49 + indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
8.50 + indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
8.51 + indt j ^ "</RULE>\n"
8.52 + end;
8.53 +
8.54 fun rules2xml j thyID [] = ("":xml)
8.55 | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
8.56
9.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Apr 09 14:41:41 2012 +0200
9.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Apr 10 09:31:31 2012 +0200
9.3 @@ -104,10 +104,8 @@
9.4
9.5 val i = indentation;
9.6
9.7 -fun pbl2term thy (pblRD:pblRD) =
9.8 - str2term ("Problem (" ^
9.9 - (get_thy o theory2domID) thy ^ "_, " ^
9.10 - (strs2str' o rev) pblRD ^ ")");
9.11 +fun pbl2term thy (pblRD:pblRD) = (*WN120405.TODO.txt*)
9.12 + str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
9.13 (* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]);
9.14 val it = "Problem (Isac, [normalize, univariate, equations])" : string
9.15 *)
9.16 @@ -302,14 +300,16 @@
9.17 ((str2file (path ^ guh2filename guh)) o (met2xml id)) met);
9.18
9.19
9.20 -(*.scan the mtree Ptyp and and print the nodes using wfn.*)
9.21 +(*.scan the mtree Ptyp and print the nodes using wfn.*)
9.22 fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
9.23 let val po' = lev_on po
9.24 - in wfn pa po' (ids@[id]) n;
9.25 - nodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
9.26 + in
9.27 + wfn pa po' (ids@[id]) n;
9.28 + nodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns
9.29 + end
9.30 and nodes _ _ _ _ [] = ()
9.31 - | nodes pa ids po wfn (n::ns) = (node pa ids po wfn n;
9.32 - nodes pa ids (lev_on po) wfn ns);
9.33 + | nodes pa ids po wfn (n::ns) =
9.34 + (node pa ids po wfn n; nodes pa ids (lev_on po) wfn ns);
9.35
9.36
9.37 fun pbls2file (p:path) = nodes p [] [0] pbl2file (!ptyps);
10.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Apr 09 14:41:41 2012 +0200
10.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Tue Apr 10 09:31:31 2012 +0200
10.3 @@ -181,27 +181,28 @@
10.4 val thydatafilename = "thy_datafile.xml"; (*for "Theorems"|...*)
10.5 fun partfilename str = "thy_" ^ str ^ ".xml"; (*for "Isabelle"|...*)*)
10.6
10.7 -(*.create an xml-hierarchy where the filname is created from the guh.*)
10.8 +(* create an xml-hierarchy where the filname is created from the guh *)
10.9 (*ad DTD: a NODE contains an ID and zero or more NODEs*)
10.10 fun hierarchy_guh h =
10.11 - let val i = indentation
10.12 - val j = indentation
10.13 - fun node i p theID (Ptyp (id,_,ns)) =
10.14 - let val p' = lev_on p
10.15 - val theID' = theID @ [id]
10.16 - in (indt i) ^ "<NODE>\n" ^
10.17 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
10.18 - (indt (i+j)) ^ "<NO> " (*on this level*) ^
10.19 - (string_of_int o last_elem) p' ^ " </NO>\n" ^
10.20 - (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^
10.21 - " </CONTENTREF>\n" ^
10.22 - (nodes (i+j) (lev_dn p') theID' ns) ^
10.23 - (indt i) ^ "</NODE>\n"
10.24 - end
10.25 - and nodes _ _ _ [] = ""
10.26 - | nodes i p theID (n::ns) = (node i p theID n)
10.27 - ^ (nodes i (lev_on p) theID ns);
10.28 - in nodes j [0] [] h end;
10.29 + let
10.30 + val i = indentation
10.31 + val j = indentation
10.32 + fun node i p theID (Ptyp (id,_,ns)) =
10.33 + let
10.34 + val p' = lev_on p
10.35 + val theID' = theID @ [id]
10.36 + in
10.37 + (indt i) ^ "<NODE>\n" ^
10.38 + (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
10.39 + (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
10.40 + (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^ " </CONTENTREF>\n" ^
10.41 + (nodes (i+j) (lev_dn p') theID' ns) ^
10.42 + (indt i) ^ "</NODE>\n"
10.43 + end
10.44 + and nodes _ _ _ [] = ""
10.45 + | nodes i p theID (n::ns) =
10.46 + (node i p theID n) ^ (nodes i (lev_on p) theID ns);
10.47 + in nodes j [0] [] h end;
10.48
10.49 fun thy_hierarchy2file (path:path) =
10.50 str2file (path ^ "thy_hierarchy.xml")
10.51 @@ -213,84 +214,67 @@
10.52 "</NODE>");
10.53
10.54
10.55 -(**.create the xml-files for the theory-data from the hierarchy.**)
10.56 +(** create the xml-files for the theory-data from the hierarchy **)
10.57
10.58 val i = indentation;
10.59 -(*.analoguous to 'fun met2xml'.*)
10.60 +(* analoguous to 'fun met2xml' *)
10.61 fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =
10.62 - "<HTMLDATA>\n" ^
10.63 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.64 - id2xml i theID ^
10.65 - indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
10.66 - authors2xml i "MATHAUTHORS" mathauthors ^
10.67 + "<HTMLDATA>\n" ^
10.68 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.69 + id2xml i theID ^
10.70 + indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
10.71 + authors2xml i "MATHAUTHORS" mathauthors ^
10.72 + authors2xml i "COURSEDESIGNS" coursedesign ^
10.73 + "</HTMLDATA>\n" : xml
10.74 + | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) =
10.75 + "<THEOREMDATA>\n" ^
10.76 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.77 + id2xml i theID ^
10.78 + term2xml i thm ^
10.79 + indt i ^ "<PROOF>\n" ^
10.80 + extref2xml (i+i) "Proof of the theorem"
10.81 + ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
10.82 + nth 2 theID ^ ".html") ^
10.83 + indt i ^ "</PROOF>\n" ^
10.84 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.85 + authors2xml i "MATHAUTHORS" mathauthors ^
10.86 + authors2xml i "COURSEDESIGNS" coursedesign ^
10.87 + "</THEOREMDATA>\n"
10.88 + | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
10.89 + "<RULESETDATA>\n" ^
10.90 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.91 + id2xml i theID ^
10.92 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.93 + authors2xml i "MATHAUTHORS" mathauthors ^
10.94 authors2xml i "COURSEDESIGNS" coursedesign ^
10.95 - "</HTMLDATA>\n" : xml
10.96 - | thydata2xml (theID:theID, Hthm {guh, coursedesign, mathauthors, thm}) =
10.97 - "<THEOREMDATA>\n" ^
10.98 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.99 - id2xml i theID ^
10.100 - term2xml i thm ^
10.101 - indt i ^ "<PROOF>\n" ^
10.102 - extref2xml (i+i) "Proof of the theorem"
10.103 - ("http://www.ist.tugraz.at/projects/isac/www/\
10.104 - \kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
10.105 - nth 2 theID ^ ".html") ^
10.106 - indt i ^ "</PROOF>\n" ^
10.107 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.108 - authors2xml i "MATHAUTHORS" mathauthors ^
10.109 - authors2xml i "COURSEDESIGNS" coursedesign ^
10.110 - "</THEOREMDATA>\n"
10.111 -(* val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
10.112 - (theID, thydata);
10.113 - *)
10.114 - | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
10.115 - "<RULESETDATA>\n" ^
10.116 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.117 - id2xml i theID ^
10.118 - rls2xml i thy_rls ^
10.119 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.120 - authors2xml i "MATHAUTHORS" mathauthors ^
10.121 - authors2xml i "COURSEDESIGNS" coursedesign ^
10.122 - "</RULESETDATA>\n"
10.123 -(* val (theID:theID, Hcal {guh, coursedesign, mathauthors, calc}) =
10.124 - (theID, rlsdata);
10.125 - *)
10.126 + "</RULESETDATA>\n"
10.127 | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) =
10.128 - "<RULESETDATA>\n" ^
10.129 - indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.130 - id2xml i theID ^
10.131 - calc2xml i (theID2thyID theID, calc) ^
10.132 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.133 - authors2xml i "MATHAUTHORS" mathauthors ^
10.134 - authors2xml i "COURSEDESIGNS" coursedesign ^
10.135 - "</RULESETDATA>\n"
10.136 + "<RULESETDATA>\n" ^
10.137 + indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
10.138 + id2xml i theID ^
10.139 + calc2xml i (theID2thyID theID, calc) ^
10.140 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.141 + authors2xml i "MATHAUTHORS" mathauthors ^
10.142 + authors2xml i "COURSEDESIGNS" coursedesign ^
10.143 + "</RULESETDATA>\n"
10.144 | thydata2xml (theID, _) =
10.145 - error ("thydata2xml: not implemented for "^ strs2str' theID);
10.146 + error ("thydata2xml: not implemented for "^ strs2str' theID);
10.147
10.148 -(*.analoguous to 'fun met2file'.*)
10.149 +(* analoguous to 'fun met2file' *)
10.150 fun thydata2file (xmldata:path) (pos:pos) (theID:theID) thydata =
10.151 - (writeln ("### thes2file: id = " ^ strs2str theID);
10.152 - str2file (xmldata ^ theID2filename theID)
10.153 - (thydata2xml (theID:theID, thydata)));
10.154 + (writeln ("### thes2file: id = " ^ strs2str theID);
10.155 + str2file (xmldata ^ theID2filename theID) (thydata2xml (theID:theID, thydata)));
10.156
10.157 -(*.analoguous to 'fun node'; here we scan ??????????.*)
10.158 -(* val (pa, ids, po, wfn, (Ptyp (id,[n],ns))) =
10.159 - (pa, ids, po, wfn, n);
10.160 - *)
10.161 -fun thenode (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
10.162 +(* analoguous to 'fun node' *)
10.163 +fun thenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) =
10.164 let val po' = lev_on po
10.165 - in wfn pa po' (ids@[id]) n;
10.166 - thenodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns end
10.167 -(* val (pa, ids, po, wfn, (n::ns)) =
10.168 - (path, []:string list, [0], thydata2file, (! thehier));
10.169 - *)
10.170 + in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns end
10.171 and thenodes _ _ _ _ [] = ()
10.172 - | thenodes pa ids po wfn (n::ns) = (thenode pa ids po wfn n;
10.173 - thenodes pa ids (lev_on po) wfn ns);
10.174 + | thenodes pa ids po wfn (n::ns) =
10.175 + (thenode pa ids po wfn n; thenodes pa ids (lev_on po) wfn ns);
10.176
10.177 -(*..analoguous to 'fun mets2file'*)
10.178 -fun thes2file (p : path) =
10.179 - thenodes p [] [0] thydata2file (! thehier);
10.180 +(* analoguous to 'fun mets2file' *)
10.181 +fun thes2file (p : path) = thenodes p [] [0] thydata2file (! thehier);
10.182
10.183
10.184 (***.store a single theory element in the hierarchy.***)
11.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Apr 09 14:41:41 2012 +0200
11.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Apr 10 09:31:31 2012 +0200
11.3 @@ -523,7 +523,7 @@
11.4 \begin{verbatim}
11.5 val {srls,...} = get_met ["SignalProcessing",
11.6 "Z_Transform",
11.7 - "inverse"];
11.8 + "Inverse"];
11.9 \end{verbatim}
11.10
11.11 \par \noindent Create 2 good example terms:
11.12 @@ -905,15 +905,15 @@
11.13 ML {*
11.14 store_pbt
11.15 (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
11.16 - (["inverse", "Z_Transform", "SignalProcessing"],
11.17 + (["Inverse", "Z_Transform", "SignalProcessing"],
11.18 [("#Given" ,["filterExpression X_eq"]),
11.19 ("#Find" ,["stepResponse n_eq"])
11.20 ],
11.21 append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
11.22 - [["SignalProcessing","Z_Transform","inverse"]]));
11.23 + [["SignalProcessing","Z_Transform","Inverse"]]));
11.24
11.25 show_ptyps();
11.26 - get_pbt ["inverse","Z_Transform","SignalProcessing"];
11.27 + get_pbt ["Inverse","Z_Transform","SignalProcessing"];
11.28 *}
11.29
11.30 subsection {*Define Name and Signature for the Method*}
11.31 @@ -954,7 +954,7 @@
11.32 ML {*
11.33 store_met
11.34 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.35 - (["SignalProcessing", "Z_Transform", "inverse"],
11.36 + (["SignalProcessing", "Z_Transform", "Inverse"],
11.37 [("#Given" ,["filterExpression X_eq"]),
11.38 ("#Find" ,["stepResponse n_eq"])
11.39 ],
11.40 @@ -970,7 +970,7 @@
11.41 ML {*
11.42 store_met
11.43 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.44 - (["SignalProcessing", "Z_Transform", "inverse"],
11.45 + (["SignalProcessing", "Z_Transform", "Inverse"],
11.46 [("#Given" ,["filterExpression X_eq"]),
11.47 ("#Find" ,["stepResponse n_eq"])
11.48 ],
11.49 @@ -993,7 +993,7 @@
11.50 the hierarchy.*}
11.51
11.52 ML {*
11.53 - get_met ["SignalProcessing","Z_Transform","inverse"];
11.54 + get_met ["SignalProcessing","Z_Transform","Inverse"];
11.55 *}
11.56
11.57 section {*Program in TP-based language \label{prog-steps}*}
11.58 @@ -1150,7 +1150,7 @@
11.59 prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.60 (["SignalProcessing",
11.61 "Z_Transform",
11.62 - "inverse"],
11.63 + "Inverse"],
11.64 [
11.65 ("#Given" ,["filterExpression X_eq"]),
11.66 ("#Find" ,["stepResponse n_eq"])
11.67 @@ -1245,8 +1245,8 @@
11.68 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
11.69 "stepResponse (x[n::real]::bool)"];
11.70 val (dI,pI,mI) =
11.71 - ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
11.72 - ["SignalProcessing","Z_Transform","inverse"]);
11.73 + ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
11.74 + ["SignalProcessing","Z_Transform","Inverse"]);
11.75
11.76 val ([
11.77 (
11.78 @@ -1269,7 +1269,7 @@
11.79 val Script sc
11.80 = (#scr o get_met) ["SignalProcessing",
11.81 "Z_Transform",
11.82 - "inverse"];
11.83 + "Inverse"];
11.84 atomty sc;
11.85 *}
11.86
11.87 @@ -1287,8 +1287,8 @@
11.88 "stepResponse (x[n::real]::bool)"];
11.89
11.90 val (dI,pI,mI) =
11.91 - ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
11.92 - ["SignalProcessing","Z_Transform","inverse"]);
11.93 + ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
11.94 + ["SignalProcessing","Z_Transform","Inverse"]);
11.95
11.96 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
11.97 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
11.98 @@ -1344,7 +1344,7 @@
11.99 val Script s =
11.100 (#scr o get_met) ["SignalProcessing",
11.101 "Z_Transform",
11.102 - "inverse"];
11.103 + "Inverse"];
11.104 writeln (term2str s);
11.105 \end{verbatim}
11.106 \ldots shows the right script. Difference in the arguments.
12.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Apr 09 14:41:41 2012 +0200
12.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue Apr 10 09:31:31 2012 +0200
12.3 @@ -1004,7 +1004,7 @@
12.4 \begin{verbatim}
12.5 val {srls,...} = get_met ["SignalProcessing",
12.6 "Z_Transform",
12.7 - "inverse"];
12.8 + "Inverse"];
12.9 \end{verbatim}
12.10
12.11 \par \noindent Create 2 good example terms:
12.12 @@ -2393,7 +2393,7 @@
12.13 val Script s =
12.14 (#scr o get_met) ["SignalProcessing",
12.15 "Z_Transform",
12.16 - "inverse"];
12.17 + "Inverse"];
12.18 writeln (term2str s);
12.19 \end{verbatim}
12.20 \ldots shows the right script. Difference in the arguments.
13.1 --- a/test/Tools/isac/CLEANUP Mon Apr 09 14:41:41 2012 +0200
13.2 +++ b/test/Tools/isac/CLEANUP Tue Apr 10 09:31:31 2012 +0200
13.3 @@ -100,4 +100,11 @@
13.4 rm .#*
13.5 rm *.tar*
13.6 rm *.orig*
13.7 + cd Inverse_Z_Transform
13.8 + rm *~
13.9 + rm #*
13.10 + rm .#*
13.11 + rm *.tar*
13.12 + rm *.orig*
13.13 + cd ..
13.14 cd ..
14.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Apr 09 14:41:41 2012 +0200
14.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Tue Apr 10 09:31:31 2012 +0200
14.3 @@ -481,8 +481,8 @@
14.4
14.5 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
14.6 "stepResponse (x[n::real]::bool)"];
14.7 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
14.8 - ["SignalProcessing","Z_Transform","inverse"]);
14.9 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
14.10 + ["SignalProcessing","Z_Transform","Inverse"]);
14.11
14.12 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
14.13 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
15.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Apr 09 14:41:41 2012 +0200
15.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Apr 10 09:31:31 2012 +0200
15.3 @@ -2,15 +2,17 @@
15.4 authors: Walther Neuper 2000, 2006
15.5 *)
15.6
15.7 -(*============ inhibit exn WN120321 ==============================================
15.8 "--------------------------------------------------------";
15.9 "--------------------------------------------------------";
15.10 "table of contents --------------------------------------";
15.11 "--------------------------------------------------------";
15.12 +(*============ inhibit exn WN120321 ==============================================
15.13 "----------- fun make_isab ------------------------------";
15.14 "----------- fun collect_isab_thys ----------------------";
15.15 +============ inhibit exn WN120321 ==============================================*)
15.16 "----------- fun thy_containing_rls ---------------------";
15.17 "----------- fun thy_containing_cal ---------------------";
15.18 +(*============ inhibit exn WN120321 ==============================================
15.19 "----------- initContext Thy_ Integration-demo ----------";
15.20 "----------- initContext..Thy_, fun context_thm ---------";
15.21 "----------- initContext..Thy_, fun context_rls ---------";
15.22 @@ -25,11 +27,13 @@
15.23 "--------------------------------------------------------";
15.24 "----------- fun filter_appl_rews -----------------------";
15.25 "----------- fun is_contained_in ------------------------";
15.26 +============ inhibit exn WN120321 ==============================================*)
15.27 "--------------------------------------------------------";
15.28 "--------------------------------------------------------";
15.29
15.30 "----------- fun make_isab ------------------------------";
15.31 "----------- fun make_isab ------------------------------";
15.32 +(*============ inhibit exn WN120321 ==============================================
15.33 "----------- fun make_isab ------------------------------";
15.34 (* rlsthmsNOTisac: contains thms in rls requested from Isabelle ---" *)
15.35 map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)
15.36 @@ -119,68 +123,107 @@
15.37 print_depth 99; isab_thm_thy; print_depth 3;
15.38 *)
15.39 === inhibit exn AK110725 =============================================================*)
15.40 +============ inhibit exn WN120321 ==============================================*)
15.41
15.42
15.43
15.44 "----------- fun thy_containing_rls ---------------------";
15.45 "----------- fun thy_containing_rls ---------------------";
15.46 "----------- fun thy_containing_rls ---------------------";
15.47 +infix mem; (*from Isabelle2002*)
15.48 +fun x mem [] = false
15.49 + | x mem (y :: ys) = x = y orelse x mem ys;
15.50 +
15.51 val thy' = "Biegelinie";
15.52 -val dropthys = takewhile [] (not o (curry op= thy') o
15.53 - (#1:theory' * theory -> theory'))
15.54 - (rev (!theory'));
15.55 + val dropthys =
15.56 + takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
15.57 + (rev (!theory'));
15.58 +
15.59 if length (!theory') <> length dropthys then ()
15.60 -else error "rewtools.sml: diff.behav. in thy_containing_rls 1";
15.61 -val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
15.62 - dropthys;
15.63 -print_depth 99; dropthy's; print_depth 3;
15.64 +else error "thy_containing_rls changed 1";
15.65
15.66 -(*WN100819=======================================================
15.67 -WN100819 THIS DATE MUST BE WRONG: at this date changeset 37934:56f10b13005e
15.68 -finished update ME/calchead.sml + pushed updates over all sml+test
15.69 + val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;
15.70
15.71 -"Isac" mem dropthy's;
15.72 -op mem ("Isac", dropthy's);
15.73 +if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"](*, "Biegelinie",..,"Test",.*)
15.74 +then () else error "thy_containing_rls changed ancestors_rls";
15.75 +
15.76 +"Isac" mem dropthys';
15.77 +op mem ("Isac", dropthys');
15.78 (op mem) o swap;
15.79 -((op mem) o swap) (dropthy's, "Isac");
15.80 +((op mem) o swap) (dropthys', "Isac");
15.81 curry ((op mem) o swap);
15.82 -curry ((op mem) o swap) dropthy's "Isac";
15.83 -val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
15.84 - ((#1 o #2) : rls' * (theory' * rls) -> theory'))
15.85 - (rev (!ruleset'));
15.86 -print_depth 99; map (#1 o #2) startsearch; print_depth 3;
15.87 -if length (!ruleset') <> length startsearch then ()
15.88 -else error "rewtools.sml: diff.behav. in thy_containing_rls 2";
15.89 +curry ((op mem) o swap) dropthys' "Isac";
15.90 + val ancestors_rls =
15.91 + filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
15.92 + (rev (!ruleset'));
15.93
15.94 +take (10, map #1 ancestors_rls) =
15.95 + ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation",
15.96 + "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*)
15.97 +
15.98 +if length (!ruleset') <> length ancestors_rls then ()
15.99 +else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?";
15.100
15.101 val rls' = "norm_Poly";
15.102 -case assoc (startsearch, rls') of
15.103 +case assoc (ancestors_rls, rls') of
15.104 SOME (thy', _) => thyID2theory' thy'
15.105 - | _ => error ("thy_containing_rls : rls '"^str^
15.106 - "' not in !rulset' und thy '"^thy'^"'");
15.107 + | _ => error ("thy_containing_rls : rls '" ^ rls' ^
15.108 + "' not in !rulset' und thy '" ^ thy' ^ "'");
15.109
15.110 if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly") then ()
15.111 -else error "rewtools.sml: diff.behav. in thy_containing_rls 3";
15.112 +else error "thy_containing_rls 3: changed with (Biegelinie, norm_Poly)";
15.113 +
15.114 +"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie" ,"norm_Poly");
15.115 + val rls' = strip_thy rls'
15.116 + val thy' = thyID2theory' thy'
15.117 + val dropthys =
15.118 + takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
15.119 + (rev (!theory'));
15.120 +
15.121 +map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*)
15.122 +
15.123 + val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
15.124 + val ancestors_rls =
15.125 + filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
15.126 + (rev (!ruleset'));
15.127 +
15.128 +case assoc (ancestors_rls, rls') of
15.129 + SOME ("Poly", Seq {id = "norm_Poly", ...}) => ()
15.130 +| _ => error "thy_containing_rls changed 2";
15.131
15.132
15.133 "----------- fun thy_containing_cal ---------------------";
15.134 "----------- fun thy_containing_cal ---------------------";
15.135 "----------- fun thy_containing_cal ---------------------";
15.136 val thy' = "Atools";
15.137 -val dropthys = takewhile [] (not o (curry op= thy') o
15.138 - (#1:theory' * theory -> theory'))
15.139 - (rev (!theory'));
15.140 + val dropthys =
15.141 + takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
15.142 + (rev (!theory'));
15.143 +
15.144 length dropthys <> length (!theory');
15.145 -val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
15.146 - dropthys;
15.147 +
15.148 + val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys;
15.149 +
15.150 +if dropthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",
15.151 + "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",
15.152 + "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",
15.153 + "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*)
15.154 +then () else error "thy_containing_cal changed ancestors_rls for Atools";
15.155
15.156 (rev (!calclist'));
15.157 map #1 (rev (!calclist'));
15.158 map (#1 : calc -> string) (rev (!calclist'));
15.159 -val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
15.160 - (#1 : calc -> string)) (rev (!calclist'));
15.161 -WN100819 =====================================================*)
15.162
15.163 + val ancestors_cal =
15.164 + filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
15.165 + (rev (!calclist'));
15.166 +
15.167 +case ancestors_cal of
15.168 + ("Test.precond'_rootpbl", ("Test.precond'_rootpbl", _)) ::
15.169 + ("Test.precond'_rootmet", ("Test.precond'_rootmet", _)) :: _ => ()
15.170 +| _ => error "thy_containing_cal changed in Test.precond'_rootpbl, ...";
15.171 +
15.172 +(*============ inhibit exn WN120321 ==============================================
15.173 "----------- initContext Thy_ Integration-demo ----------";
15.174 "----------- initContext Thy_ Integration-demo ----------";
15.175 "----------- initContext Thy_ Integration-demo ----------";
16.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Apr 09 14:41:41 2012 +0200
16.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Tue Apr 10 09:31:31 2012 +0200
16.3 @@ -16,16 +16,16 @@
16.4 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
16.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
16.6 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
16.7 -get_pbt ["inverse","Z_Transform","SignalProcessing"];
16.8 -get_met ["SignalProcessing","Z_Transform","inverse"];
16.9 +get_pbt ["Inverse","Z_Transform","SignalProcessing"];
16.10 +get_met ["SignalProcessing","Z_Transform","Inverse"];
16.11
16.12 "----------- test [SignalProcessing,Z_Transform,inverse] ---";
16.13 "----------- test [SignalProcessing,Z_Transform,inverse] ---";
16.14 "----------- test [SignalProcessing,Z_Transform,inverse] ---";
16.15 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
16.16 "stepResponse x[(n::real)]"];
16.17 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
16.18 - ["SignalProcessing","Z_Transform","inverse"]);
16.19 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
16.20 + ["SignalProcessing","Z_Transform","Inverse"]);
16.21 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
16.22 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
16.23
17.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Mon Apr 09 14:41:41 2012 +0200
17.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Tue Apr 10 09:31:31 2012 +0200
17.3 @@ -23,7 +23,8 @@
17.4 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
17.5 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
17.6 "-------- OLD compute rlsthmsNOTisac by eq_thmID --------";
17.7 -(* view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada
17.8 +(* WN1204xx:
17.9 + view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada
17.10 date Thu Jul 22 10:45:18 2010 +0200
17.11
17.12 local
17.13 @@ -106,22 +107,30 @@
17.14 "-------- retrieve isa-b/c theories from Isabelle -------";
17.15 val first_ProgLang_thy = @{theory ListC}
17.16 val first_Knowledge_thy = @{theory Delete} (*see WN120321.TODO rearrange theories*)
17.17 - val allthys = (*!!! @{theory} ::*) Theory.ancestors_of @{theory};
17.18 + val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};
17.19 val isabthys' =
17.20 drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
17.21 + val isacthys' =
17.22 + take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
17.23 val knowthys' =
17.24 - take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
17.25 - val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
17.26 - drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) knowthys') + 1 +3, knowthys');
17.27 + take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');
17.28 + val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
17.29 + drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');
17.30
17.31 map Context.theory_name allthys;
17.32 -map Context.theory_name knowthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate", "Diff", "LogExp",
17.33 - "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript", "Delete", "xmlsrc", "Interpret", "ProgLang",
17.34 - "Script", "Tools", "ListC"]; (*WN120201 true*)
17.35 +map Context.theory_name isabthys';
17.36 +map Context.theory_name isacthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin",
17.37 + "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",
17.38 + "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq",
17.39 + "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript",
17.40 + "Delete", "xmlsrc", "Interpret", "ProgLang", "Script", "Tools", "ListC"]; (*WN120201 true*)
17.41 (*see WN120321.TODO rearrange theories: ATTENTION with ProgLang.thy etc*)
17.42 +map Context.theory_name knowthys' = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin",
17.43 + "Biegelinie", "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem",
17.44 + "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq",
17.45 + "RootEq", "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify", "Atools", "Descript",
17.46 + "Delete"]; (*WN120201 true*)
17.47 map Context.theory_name progthys' = ["Script", "Tools", "ListC"]; (*WN120201 true*)
17.48 -map Context.theory_name isabthys';
17.49 -
17.50
17.51 "-------- prop_of thm .. Theory.axioms_of ---------------";
17.52 "-------- prop_of thm .. Theory.axioms_of ---------------";
18.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Apr 09 14:41:41 2012 +0200
18.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Apr 10 09:31:31 2012 +0200
18.3 @@ -593,7 +593,7 @@
18.4 (*============ inhibit exn WN120314 ==============================================
18.5 (*??? WN111205: this check succeeds erratically : asyncronous Isar/jEdit ???*)
18.6 if existpt' ([1,1,5], Res) pt then ()
18.7 -else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
18.8 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 2 ERRATICAL???";
18.9 ============ inhibit exn WN120314 ==============================================*)
18.10
18.11
19.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Mon Apr 09 14:41:41 2012 +0200
19.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Tue Apr 10 09:31:31 2012 +0200
19.3 @@ -24,8 +24,8 @@
19.4 "----------- why helpless here ? ------------------------";
19.5 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
19.6 "stepResponse (x[n::real]::bool)"];
19.7 -val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
19.8 - ["SignalProcessing","Z_Transform","inverse"]);
19.9 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
19.10 + ["SignalProcessing","Z_Transform","Inverse"]);
19.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
19.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
19.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
19.14 @@ -43,7 +43,7 @@
19.15 val pIopt = get_pblID (pt,ip);
19.16 ip = ([],Res); "false";
19.17 tacis; " = []";
19.18 -pIopt; (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*)
19.19 +pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
19.20 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
19.21 (*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
19.22 THIS MEANS: replace no_meth by [no_meth] in Script.*)
19.23 @@ -62,7 +62,7 @@
19.24 val pIopt = get_pblID (pt,ip);
19.25 ip = ([],Res); " = false";
19.26 tacis; " = []";
19.27 -pIopt (* = SOME ["inverse", "Z_Transform", "SignalProcessing"]*);
19.28 +pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
19.29 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
19.30 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
19.31 nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
20.1 --- a/test/Tools/isac/Test_Isac.thy Mon Apr 09 14:41:41 2012 +0200
20.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Apr 10 09:31:31 2012 +0200
20.3 @@ -95,6 +95,7 @@
20.4 ("Knowledge/algein.sml")
20.5 ("Knowledge/diophanteq.sml")
20.6 ("Knowledge/isac.sml")
20.7 + ("Knowledge/build_thydata.sml")
20.8
20.9 begin
20.10
20.11 @@ -127,7 +128,7 @@
20.12 use "Interpret/generate.sml"
20.13 use "Interpret/calchead.sml" (*part.*)
20.14 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
20.15 - use "Interpret/rewtools.sml" (*TODO*)
20.16 + use "Interpret/rewtools.sml" (*TODO/part.WN120406*)
20.17 use "Interpret/script.sml" (*!TODO/part.*)
20.18 use "Interpret/solve.sml" (*part.*)
20.19 use "Interpret/inform.sml" (*part.*)
20.20 @@ -136,15 +137,15 @@
20.21 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
20.22 use "xmlsrc/mathml.sml" (*part.*)
20.23 use "xmlsrc/datatypes.sml" (*TODO/part.*)
20.24 - use "xmlsrc/pbl-met-hierarchy.sml" (*TODO/part.*)
20.25 - use "xmlsrc/thy-hierarchy.sml" (*TODO after 2009-2/part.*)
20.26 + use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
20.27 + use "xmlsrc/thy-hierarchy.sml" (*TODO after 2009-2/part.*)
20.28 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
20.29 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
20.30 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
20.31 use "Frontend/messages.sml"
20.32 use "Frontend/states.sml"
20.33 use "Frontend/interface.sml"
20.34 - use "print_exn_G.sml"
20.35 + use "print_exn_G.sml"
20.36 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
20.37 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
20.38 use "Knowledge/delete.sml"
21.1 --- a/test/Tools/isac/Test_Some.thy Mon Apr 09 14:41:41 2012 +0200
21.2 +++ b/test/Tools/isac/Test_Some.thy Tue Apr 10 09:31:31 2012 +0200
21.3 @@ -1,12 +1,38 @@
21.4
21.5 theory Test_Some imports Isac begin
21.6
21.7 -use"../../../test/Tools/isac/Knowledge/simplify.sml"
21.8 +use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"
21.9
21.10 ML {*
21.11 val thy = @{theory "Isac"};
21.12 val ctxt = ProofContext.init_global thy;
21.13 -print_depth 5;
21.14 +print_depth 9;
21.15 +*}
21.16 +ML {* (*==================*)
21.17 +*}
21.18 +ML {*
21.19 +val path = "/home/neuper/tmp/xmldata/";
21.20 +
21.21 +pbl_hierarchy2file (path ^ "pbl/");
21.22 +pbls2file (path ^ "pbl/");
21.23 +
21.24 +met_hierarchy2file (path ^ "met/");
21.25 +mets2file (path ^ "met/");
21.26 +
21.27 +thy_hierarchy2file (path ^ "thy/");
21.28 +*}
21.29 +ML {*
21.30 +thes2file (path ^ "thy/");
21.31 +*}
21.32 +text {*
21.33 +"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
21.34 +thy_containing_rls : rls 'discard_minus' not in !rulset' of ancestors of thy 'Poly'
21.35 +*}
21.36 +ML {* (*==================*)
21.37 +*}
21.38 +ML {*
21.39 +*}
21.40 +ML {*
21.41 *}
21.42 ML {*
21.43 *}
21.44 @@ -22,17 +48,7 @@
21.45 *}
21.46 ML {*
21.47 *}
21.48 -ML {*
21.49 -*}
21.50 ML {* (*==================*)
21.51 -*}
21.52 -ML {*
21.53 -*}
21.54 -ML {*
21.55 -*}
21.56 -ML {*
21.57 -*}
21.58 -ML {*
21.59 "~~~~~ fun , args:"; val () = ();
21.60 "~~~~~ to return val:"; val () = ();
21.61
21.62 @@ -43,8 +59,8 @@
21.63 *}
21.64 end
21.65
21.66 -(*============ inhibit exn WN120321 ==============================================
21.67 -============ inhibit exn WN120321 ==============================================*)
21.68 +(*============ inhibit exn WN120406 ==============================================
21.69 +============ inhibit exn WN120406 ==============================================*)
21.70
21.71 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
21.72 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
22.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Apr 09 14:41:41 2012 +0200
22.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Apr 10 09:31:31 2012 +0200
22.3 @@ -13,16 +13,18 @@
22.4 "-----------------------------------------------------------------";
22.5 "table of contents -----------------------------------------------";
22.6 "-----------------------------------------------------------------";
22.7 -"----------- pbl2xml ---------------------------------------------";
22.8 +"----- pbl2xml ---------------------------------------------------";
22.9 +"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
22.10 +"----- fun pbl2term ----------------------------------------------";
22.11 "-----------------------------------------------------------------";
22.12 "-----------------------------------------------------------------";
22.13 "-----------------------------------------------------------------";
22.14
22.15
22.16
22.17 -"----------- pbl2xml ---------------------------------------------";
22.18 -"----------- pbl2xml ---------------------------------------------";
22.19 -"----------- pbl2xml ---------------------------------------------";
22.20 +"----- pbl2xml ---------------------------------------------------";
22.21 +"----- pbl2xml ---------------------------------------------------";
22.22 +"----- pbl2xml ---------------------------------------------------";
22.23 (*what to do if from 'pbls2file "../../xmldata/pbl/";' you get the error
22.24
22.25 ### pbl2file: id = ["Biegelinie"]
22.26 @@ -36,9 +38,55 @@
22.27 Exception- OPTION raised
22.28 *)
22.29
22.30 -
22.31 -(*========== inhibit exn AK110725 ================================================
22.32 - pbl2xml ["Biegelinien"] (get_pbt ["Biegelinien"]);
22.33 +if pbl2xml ["Biegelinien"] (get_pbt ["Biegelinien"]) =
22.34 + "<NODECONTENT>\n"^
22.35 + " <GUH> pbl_bieg </GUH>\n"^
22.36 + " <STRINGLIST>\n"^
22.37 + " <STRING> Biegelinien </STRING>\n"^
22.38 + " </STRINGLIST>\n <META> </META>\n"^
22.39 + " <HEADLINE>\n"^
22.40 + " <MATHML>\n"^
22.41 + " <ISA> Problem (Biegelinie', [Biegelinien]) </ISA>\n"^
22.42 + " </MATHML>\n"^
22.43 + " </HEADLINE>\n"^
22.44 + " <GIVEN>\n"^
22.45 + " <MATHML>\n"^
22.46 + " <ISA> Traegerlaenge l_l </ISA>\n"^
22.47 + " </MATHML>\n"^
22.48 + " <MATHML>\n"^
22.49 + " <ISA> Streckenlast q_q </ISA>\n"^
22.50 + " </MATHML> </GIVEN>\n <WHERE> </WHERE>\n"^
22.51 + " <FIND>\n"^
22.52 + " <MATHML>\n"^
22.53 + " <ISA> Biegelinie b_b </ISA>\n"^
22.54 + " </MATHML> </FIND>\n"^
22.55 + " <RELATE>\n"^
22.56 + " <MATHML>\n"^
22.57 + " <ISA> Randbedingungen r_b </ISA>\n"^
22.58 + " </MATHML> </RELATE>\n"^
22.59 + " <EXPLANATIONS> </EXPLANATIONS>\n"^
22.60 + " <THEORY>\n"^
22.61 + " <KESTOREREF>\n"^
22.62 + " <TAG> Theorem </TAG>\n"^
22.63 + " <ID> </ID>\n"^
22.64 + " <GUH> thy_isac_Biegelinie-thm- </GUH>\n"^
22.65 + " </KESTOREREF>\n"^
22.66 + " </THEORY>\n"^
22.67 + " <METHODS>\n"^
22.68 + " <KESTOREREF>\n"^
22.69 + " <TAG> Method</TAG>\n"^
22.70 + " <ID> [IntegrierenUndKonstanteBestimmen2] </ID>\n"^
22.71 + " <GUH> met_biege_2 </GUH>\n"^
22.72 + " </KESTOREREF>\n"^
22.73 + " </METHODS>\n"^
22.74 + " <EVALPRECOND> e_rls </EVALPRECOND>\n"^
22.75 + " <MATHAUTHORS>\n"^
22.76 + " </MATHAUTHORS>\n"^
22.77 + " <COURSEDESIGNS>\n"^
22.78 + " <STRING> isac team 2006 </STRING>\n"^
22.79 + " </COURSEDESIGNS>\n"^
22.80 + "</NODECONTENT>"
22.81 +then () else error "fun pbl2xml 'Biegelinien' changed";
22.82
22.83 (* val id = ["Biegelinie"];
22.84 val {(*guh,*)cas,met,ppc,prls,thy,where_} = get_pbt ["Biegelinie"];
22.85 @@ -62,19 +110,36 @@
22.86 "(RealDef.real => RealDef.real) => Tools.una") : Term.term
22.87 ..I.E. THE "Script.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)
22.88
22.89 -(*
22.90 -val path = "/home/neuper/proto2/isac/xmldata/";
22.91 -val path = "/home/neuper/tmp/";
22.92
22.93 -pbl_hierarchy2file (path ^ "pbl/");
22.94 -pbls2file (path ^ "pbl/");
22.95 +"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
22.96 +"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
22.97 +"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
22.98 +val path = "/tmp/";
22.99 +"~~~~~ fun pbls2file, args:"; val (p:path) = (path ^ "pbl/");
22.100 +!ptyps; (*not = []*)
22.101 +"~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
22.102 + (p, []: string list, [0], pbl2file, (!ptyps));
22.103 +"~~~~~ fun node, args:"; val (pa:path, ids, po, wfn, Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
22.104 +val po' = lev_on po;
22.105 +wfn (*= pbl2file*)
22.106 +"~~~~~ fun pbl2file, args:"; val ((path:path), (pos:pos), (id:metID), (pbl as {guh,...})) =
22.107 + (pa, po', (ids@[id]), n);
22.108 +strs2str id = "[\"e_pblID\"]"; (*true*)
22.109 +pos2str pos = "[1]"; (*true*)
22.110 +path ^ guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
22.111 +"~~~~~ fun pbl2xml, args:"; val (id: pblID, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
22.112 + (id, pbl);
22.113 +"~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id);
22.114 +if ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
22.115 + "Problem (Pure', [e_pblID])"
22.116 +then () else error "fun pbl2term changed";
22.117
22.118 -met_hierarchy2file (path ^ "met/");
22.119 -mets2file (path ^ "met/");
22.120
22.121 -thy_hierarchy2file (path ^ "thy/");
22.122 -thes2file (path ^ "thy/");
22.123 -*)
22.124 +"----- fun pbl2term ----------------------------------------------";
22.125 +"----- fun pbl2term ----------------------------------------------";
22.126 +"----- fun pbl2term ----------------------------------------------";
22.127 +(*see WN120405a.TODO.txt*)
22.128 +if term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]) =
22.129 + "Problem (Isac', [normalize, univariate, equations])"
22.130 +then () else error "fun pbl2term changed";
22.131
22.132 -
22.133 -============ inhibit exn AK110725 ==============================================*)
23.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Apr 09 14:41:41 2012 +0200
23.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Tue Apr 10 09:31:31 2012 +0200
23.3 @@ -2,9 +2,6 @@
23.4 Authors: Walther Neuper 060113
23.5 (c) due to copyright terms
23.6
23.7 -use"../smltest/xmlsrc/thy-hierarchy.sml";
23.8 -use"thy-hierarchy.sml";
23.9 -
23.10 CAUTION with testing *2file functions -- they are actually writing to ~/tmp
23.11 *)
23.12
23.13 @@ -19,6 +16,7 @@
23.14 "----------- write xml to tmp ------------------------------------";
23.15 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
23.16 "----------- ### thes2file ... Exception- Match raised -----------";
23.17 +"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
23.18 "-----------------------------------------------------------------";
23.19 "-----------------------------------------------------------------";
23.20 "-----------------------------------------------------------------";
23.21 @@ -37,7 +35,10 @@
23.22 overwrite (al, b);
23.23 overwritelthy thy (al, bl);
23.24
23.25 -assoc' (!ruleset',"e_rls");
23.26 +case assoc' (! ruleset',"e_rls") of
23.27 + SOME ("Tools", Rls _) => ()
23.28 +| _ => error "e_rls not in ! ruleset'"
23.29 +
23.30 assoc_rls "e_rls";
23.31
23.32
23.33 @@ -49,8 +50,14 @@
23.34
23.35 val thy' = "Integrate";
23.36 val thy = assoc_thy (thyID2theory' thy');
23.37 +
23.38 +"WN120406.GOON --- restarted with 'isolate response' below, because it was very slow ?!?" ^
23.39 +"slow probably only because of print_depth 999 and large output";
23.40 +
23.41 val thm = prop_of @{thm integral_var};
23.42
23.43 +(*-.-.-.-.-.-WN120406 isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
23.44 +
23.45 "collect_thms thy'------------------------------------------------";
23.46 (apfst single) ("Integrate.integral_var", thm);
23.47 (strip_thy o #1) ("Integrate.integral_var", thm);
23.48 @@ -181,6 +188,7 @@
23.49 mathauthors = _,coursedesign = _} => ()
23.50 | _ => error "thy-hierarchy.sml: [IsacKnowledge,Test,Rulesets]";
23.51 *)
23.52 +-.-.-.-.-.-.-WN120406 isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
23.53
23.54
23.55 "----------- fun thydata2xml -------------------------------------";
23.56 @@ -315,3 +323,72 @@
23.57 (j, (thyID, "Seq", data));
23.58 rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
23.59 ============ inhibit exn AK110725 ==============================================*)
23.60 +
23.61 +"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
23.62 +"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
23.63 +"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
23.64 +val TESTdump = Unsynchronized.ref
23.65 + ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
23.66 +
23.67 +fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids =
23.68 + let val po' = lev_on po
23.69 + in
23.70 + if (ids@[id]) = TESTids
23.71 + then
23.72 + (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns)));
23.73 + error "stopped before error, created TESTdump") (* this exn creates right signature*)
23.74 + else
23.75 + wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
23.76 + end
23.77 +and TESTthenodes _ _ _ _ [] _ = ()
23.78 + | TESTthenodes pa ids po wfn (n::ns) TESTids =
23.79 + (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);
23.80 +
23.81 +(* /--- side effects from previous test files ---\*)
23.82 + val i = indentation;
23.83 + val j = indentation;
23.84 +(* \--- side effects from previous test files ---/*)
23.85 +"~~~~~ fun thes2file, args:"; val (p : path) = ("/home/neuper/tmp/xmldata/");
23.86 +(* recursively descend into thehier just before the error: *)
23.87 +(TESTthenodes p [] [0] thydata2file (! thehier)
23.88 + ["IsacKnowledge","Poly","Rulesets","norm_Poly"]
23.89 +handle _(* "stopped before error, created TESTdump" *) => ());
23.90 +val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump;
23.91 +
23.92 +"~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) =
23.93 + (pa, po', (ids@[id]), n);
23.94 +"~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
23.95 + (theID:theID, thydata);
23.96 +"~~~~~ fun rls2xml, args:"; val (j, (thyID, Seq data)) = (i, thy_rls);
23.97 +"~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
23.98 + srls, calc, rules, scr})) = (j, (thyID, "Seq", data));
23.99 +"~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);
23.100 +"~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);
23.101 +val rls' = (#id o rep_rls) rls;
23.102 +"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = (thyID, rls');
23.103 +infix mem; (*from Isabelle2002*)
23.104 +fun x mem [] = false
23.105 + | x mem (y :: ys) = x = y orelse x mem ys;
23.106 +
23.107 + val rls' = strip_thy rls'
23.108 + val thy' = thyID2theory' thy'
23.109 + val dropthys =
23.110 + takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))
23.111 + (rev (!theory'));
23.112 +
23.113 +if map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",
23.114 + "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",
23.115 + "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",
23.116 + "LinEq", "Root", "Equation", "Rational"]
23.117 +then () else error "thy_containing_rls changed ancestors_rls for (Poly, discard_minus)";
23.118 +
23.119 + val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;
23.120 + val ancestors_rls =
23.121 + filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
23.122 + (rev (!ruleset'));
23.123 +
23.124 +case assoc (ancestors_rls, rls') of
23.125 + SOME ("Poly", Rls {id = "discard_minus", ...}) => ()
23.126 +| _ => error "thy_containing_rls changed 2";
23.127 +
23.128 +