1.1 --- a/src/Tools/isac/Frontend/Frontend.thy Fri Sep 27 17:42:16 2013 +0200
1.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Sun Sep 29 18:27:37 2013 +0200
1.3 @@ -3,17 +3,18 @@
1.4 (c) due to copyright terms
1.5 *)
1.6
1.7 -theory Frontend imports
1.8 - "~~/src/Tools/isac/xmlsrc/xmlsrc"
1.9 -uses
1.10 - ("~~/src/Tools/isac/Frontend/messages.sml")
1.11 - ("~~/src/Tools/isac/Frontend/states.sml")
1.12 - ("~~/src/Tools/isac/Frontend/interface.sml")
1.13 - ("~~/src/Tools/isac/print_exn_G.sml")
1.14 +theory Frontend imports "~~/src/Tools/isac/xmlsrc/xmlsrc"
1.15 begin
1.16 +ML {* val Rls {rules = rrr, ...} = assoc_rls "list_rls" *}
1.17 +ML {* length rrr = 53 *}
1.18 +ML {* AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *}
1.19 +ML {* val SOME (_, (Rls {rules = kkk, ...})) =
1.20 + AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *}
1.21 +ML {* length kkk = 42 *}
1.22 +
1.23 ML_file "~~/src/Tools/isac/Frontend/messages.sml"
1.24 ML_file "~~/src/Tools/isac/Frontend/states.sml"
1.25 ML_file "~~/src/Tools/isac/Frontend/interface.sml"
1.26
1.27 - ML_file "~~/src/Tools/isac/print_exn_G.sml"
1.28 + use "~~/src/Tools/isac/print_exn_G.sml"
1.29 end
1.30 \ No newline at end of file
2.1 --- a/src/Tools/isac/KEStore.thy Fri Sep 27 17:42:16 2013 +0200
2.2 +++ b/src/Tools/isac/KEStore.thy Sun Sep 29 18:27:37 2013 +0200
2.3 @@ -6,12 +6,16 @@
2.4
2.5 section {* Knowledge elements for problems and methods *}
2.6 ML {*
2.7 -(* Knowledge and Exercises are held by "KEStore" in Isac's Java front-end.
2.8 +(* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end.
2.9 In the front-end Knowledge comprises theories, problems and methods.
2.10 Elements of problems and methods are defined in theories alongside
2.11 the development of respective language elements.
2.12 However, the structure of methods and problems is independent from theories'
2.13 deductive structure. Thus respective structures are built in Build_Thydata.thy.
2.14 +
2.15 + Most elements of problems and methods are implemented in "Knowledge/", but some
2.16 + of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this
2.17 + location in the directory structure.
2.18 *)
2.19 signature KESTORE_ELEMS =
2.20 sig
2.21 @@ -24,6 +28,7 @@
2.22
2.23 structure KEStore_Elems: KESTORE_ELEMS =
2.24 struct
2.25 + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
2.26
2.27 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
2.28 structure Data = Theory_Data (
2.29 @@ -33,7 +38,7 @@
2.30 val merge = merge rls_eq;
2.31 );
2.32 fun get_rlss thy = Data.get thy
2.33 - fun add_rlss rlss = Data.map (union rls_eq rlss)
2.34 + fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)
2.35
2.36 val calc_eq = rls_eq
2.37 structure Data = Theory_Data (
2.38 @@ -43,7 +48,7 @@
2.39 val merge = merge calc_eq;
2.40 );
2.41 fun get_calcs thy = Data.get thy
2.42 - fun add_calcs calcs = Data.map (union calc_eq calcs)
2.43 + fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)
2.44
2.45 (*etc*)
2.46 end;
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Fri Sep 27 17:42:16 2013 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Sun Sep 29 18:27:37 2013 +0200
3.3 @@ -528,9 +528,8 @@
3.4 (** rule set, for evaluating list-expressions in scripts 8.01.02 **)
3.5
3.6
3.7 -val list_rls =
3.8 - append_rls "list_rls" list_rls
3.9 - [Calc ("Groups.times_class.times",eval_binop "#mult_"),
3.10 +val list_rls = append_rls "list_rls" list_rls
3.11 + [Calc ("Groups.times_class.times",eval_binop "#mult_"),
3.12 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
3.13 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
3.14 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
3.15 @@ -542,12 +541,7 @@
3.16 Thm ("if_True",num_str @{thm if_True}),
3.17 Thm ("if_False",num_str @{thm if_False})
3.18 ];
3.19 -
3.20 -ruleset' := overwritelthy thy (!ruleset',
3.21 - [("list_rls",list_rls)
3.22 - ]);
3.23 *}
3.24 -setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
3.25 ML {*
3.26
3.27 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
3.28 @@ -696,30 +690,27 @@
3.29 ("boollist2sum",("Atools.boollist2sum",eval_boollist2sum ""))
3.30 ]);
3.31
3.32 -val list_rls = prep_rls(
3.33 - merge_rls "list_erls"
3.34 - (Rls {id="replaced",preconds = [],
3.35 - rew_ord = ("termlessI", termlessI),
3.36 - erls = Rls {id="list_elrs", preconds = [],
3.37 - rew_ord = ("termlessI",termlessI),
3.38 - erls = e_rls,
3.39 - srls = Erls, calc = [], errpatts = [],
3.40 - rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
3.41 - Calc ("Orderings.ord_class.less",eval_equ "#less_")
3.42 - (* ~~~~~~ for nth_Cons_*)
3.43 - ],
3.44 - scr = EmptyScr},
3.45 - srls = Erls, calc = [], errpatts = [],
3.46 - rules = [], scr = EmptyScr})
3.47 - list_rls);
3.48 +val list_rls = prep_rls (merge_rls "list_erls"
3.49 + (Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
3.50 + erls = Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
3.51 + erls = e_rls, srls = Erls, calc = [], errpatts = [],
3.52 + rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
3.53 + Calc ("Orderings.ord_class.less", eval_equ "#less_")
3.54 + (* ~~~~~~ for nth_Cons_*)],
3.55 + scr = EmptyScr},
3.56 + srls = Erls, calc = [], errpatts = [],
3.57 + rules = [], scr = EmptyScr})
3.58 + list_rls);
3.59 +
3.60 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
3.61 *}
3.62 -setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
3.63 +setup {* KEStore_Elems.add_rlss
3.64 + [("list_rls", (Context.theory_name @{theory}, prep_rls list_rls))] *}
3.65
3.66 -ML {*
3.67 -(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
3.68 - AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
3.69 - HERE IS ME_Isa: 'eval_rls' not in system ...*)
3.70 -assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
3.71 -*}
3.72 +ML {* val Rls {rules = rrr, ...} = assoc_rls "list_rls" *}
3.73 +ML {* length rrr = 51 *}
3.74 +ML {* AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *}
3.75 +ML {* val SOME (_, (Rls {rules = kkk, ...})) =
3.76 + AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *}
3.77 +ML {* length kkk = 51 *}
3.78 end
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Fri Sep 27 17:42:16 2013 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sun Sep 29 18:27:37 2013 +0200
4.3 @@ -48,49 +48,35 @@
4.4 *}
4.5
4.6 ML {*
4.7 -*} ML {*
4.8 -(* BEFORE EVALUATING val eval_rls = BELOW, HERE IS ME_Isa: 'eval_rls' not in system *)
4.9 -assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
4.10 -*} ML {*
4.11 -AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "eval_rls" (* = NONE*)
4.12 -*} ML {*
4.13 -*} ML {*
4.14 -KEStore_Elems.get_rlss @{theory};
4.15 -*} ML {*
4.16 -*}
4.17 -
4.18 -ML {*
4.19 val thy = @{theory};
4.20
4.21 -val eval_rls = prep_rls(
4.22 - Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
4.23 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
4.24 - rules = [Thm ("refl",num_str @{thm refl}),
4.25 - Thm ("order_refl",num_str @{thm order_refl}),
4.26 - Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
4.27 - Thm ("not_true",num_str @{thm not_true}),
4.28 - Thm ("not_false",num_str @{thm not_false}),
4.29 - Thm ("and_true",num_str @{thm and_true}),
4.30 - Thm ("and_false",num_str @{thm and_false}),
4.31 - Thm ("or_true",num_str @{thm or_true}),
4.32 - Thm ("or_false",num_str @{thm or_false}),
4.33 - Thm ("and_commute",num_str @{thm and_commute}),
4.34 - Thm ("or_commute",num_str @{thm or_commute}),
4.35 -
4.36 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.37 - Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.38 -
4.39 - Calc ("Atools.ident",eval_ident "#ident_"),
4.40 - Calc ("Atools.is'_const",eval_const "#is_const_"),
4.41 - Calc ("Atools.occurs'_in",eval_occurs_in ""),
4.42 - Calc ("Tools.matches",eval_matches "")
4.43 - ],
4.44 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
4.45 - }:rls);
4.46 -ruleset' := overwritelthy @{theory}
4.47 - (!ruleset',
4.48 - [("eval_rls", eval_rls)(*FIXXXME:del with rls.rls'*)
4.49 - ]);
4.50 +val eval_rls = prep_rls (
4.51 + Rls {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
4.52 + erls = e_rls, srls = Erls, calc = [], errpatts = [],
4.53 + rules = [Thm ("refl", num_str @{thm refl}),
4.54 + Thm ("order_refl", num_str @{thm order_refl}),
4.55 + Thm ("radd_left_cancel_le", num_str @{thm radd_left_cancel_le}),
4.56 + Thm ("not_true", num_str @{thm not_true}),
4.57 + Thm ("not_false", num_str @{thm not_false}),
4.58 + Thm ("and_true", num_str @{thm and_true}),
4.59 + Thm ("and_false", num_str @{thm and_false}),
4.60 + Thm ("or_true", num_str @{thm or_true}),
4.61 + Thm ("or_false", num_str @{thm or_false}),
4.62 + Thm ("and_commute", num_str @{thm and_commute}),
4.63 + Thm ("or_commute", num_str @{thm or_commute}),
4.64 +
4.65 + Calc ("Orderings.ord_class.less", eval_equ "#less_"),
4.66 + Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
4.67 +
4.68 + Calc ("Atools.ident", eval_ident "#ident_"),
4.69 + Calc ("Atools.is'_const", eval_const "#is_const_"),
4.70 + Calc ("Atools.occurs'_in", eval_occurs_in ""),
4.71 + Calc ("Tools.matches", eval_matches "")],
4.72 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
4.73 + }:rls);
4.74 +
4.75 +ruleset' := overwritelthy @{theory} (!ruleset',
4.76 + [("eval_rls", eval_rls)(*FIXXXME:del with rls.rls'*)]);
4.77 *}
4.78 setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
4.79 ML{*
4.80 @@ -268,9 +254,9 @@
4.81 "empty_script"));
4.82
4.83 val list_rls = append_rls "list_rls" list_rls
4.84 - [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
4.85 - Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})
4.86 - ];
4.87 + [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
4.88 + Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})];
4.89 +
4.90 ruleset' := overwritelthy @{theory} (!ruleset',
4.91 [("list_rls",list_rls)
4.92 ]);
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Sep 27 17:42:16 2013 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Sep 29 18:27:37 2013 +0200
5.3 @@ -396,23 +396,20 @@
5.4
5.5 (*.for evaluation of conditions in rewrite rules.*)
5.6 val Poly_erls = append_rls "Poly_erls" Atools_erls
5.7 - [ Calc ("HOL.eq",eval_equal "#equal_"),
5.8 - Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
5.9 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
5.10 - Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
5.11 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
5.12 - Calc ("Atools.pow" ,eval_binop "#power_")
5.13 - ];
5.14 + [Calc ("HOL.eq", eval_equal "#equal_"),
5.15 + Thm ("real_unari_minus", num_str @{thm real_unari_minus}),
5.16 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.17 + Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
5.18 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
5.19 + Calc ("Atools.pow", eval_binop "#power_")];
5.20
5.21 -val poly_crls =
5.22 - append_rls "poly_crls" Atools_crls
5.23 - [ Calc ("HOL.eq",eval_equal "#equal_"),
5.24 - Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
5.25 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
5.26 - Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
5.27 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
5.28 - Calc ("Atools.pow" ,eval_binop "#power_")
5.29 - ];
5.30 +val poly_crls = append_rls "poly_crls" Atools_crls
5.31 + [Calc ("HOL.eq", eval_equal "#equal_"),
5.32 + Thm ("real_unari_minus", num_str @{thm real_unari_minus}),
5.33 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
5.34 + Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
5.35 + Calc ("Groups.times_class.times", eval_binop "#mult_"),
5.36 + Calc ("Atools.pow" ,eval_binop "#power_")];
5.37
5.38 local (*. for make_polynomial .*)
5.39
5.40 @@ -721,7 +718,6 @@
5.41 (*"0 / ?x = 0"*)
5.42 ], scr = EmptyScr}:rls;
5.43
5.44 -(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
5.45 val discard_parentheses1 =
5.46 append_rls "discard_parentheses1" e_rls
5.47 [Thm ("sym_mult_assoc",
5.48 @@ -911,7 +907,7 @@
5.49 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
5.50 (*"z1 + (z1 + k) = 2 * z1 + k"*)
5.51 ], scr = EmptyScr}:rls;
5.52 -(*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
5.53 +
5.54 val discard_parentheses =
5.55 append_rls "discard_parentheses" e_rls
5.56 [Thm ("sym_mult_assoc",
5.57 @@ -1590,7 +1586,7 @@
5.58 *}
5.59 setup {* KEStore_Elems.add_rlss
5.60 [("norm_Poly", (Context.theory_name @{theory}, prep_rls norm_Poly)),
5.61 - ("Poly_erls", (Context.theory_name @{theory}, prep_rls Poly_erls)),
5.62 + ("Poly_erls", (Context.theory_name @{theory}, prep_rls Poly_erls)),(*FIXXXME:del with rls.rls'*)
5.63 ("expand", (Context.theory_name @{theory}, prep_rls expand)),
5.64 ("expand_poly", (Context.theory_name @{theory}, prep_rls expand_poly)),
5.65 ("simplify_power", (Context.theory_name @{theory}, prep_rls simplify_power)),
6.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri Sep 27 17:42:16 2013 +0200
6.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Sep 29 18:27:37 2013 +0200
6.3 @@ -1397,7 +1397,7 @@
6.4 val order_add_mult_in = prep_rls(
6.5 Rls{id = "order_add_mult_in", preconds = [],
6.6 rew_ord = ("ord_make_polynomial_in",
6.7 - ord_make_polynomial_in false (Thy_Info.get_theory "Poly")),
6.8 + ord_make_polynomial_in false @{theory "Poly"}),
6.9 erls = e_rls,srls = Erls,
6.10 calc = [], errpatts = [],
6.11 rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
7.1 --- a/src/Tools/isac/ProgLang/ListC.thy Fri Sep 27 17:42:16 2013 +0200
7.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Sun Sep 29 18:27:37 2013 +0200
7.3 @@ -141,10 +141,9 @@
7.4 ML{* (*the former ListC.ML*)
7.5 (** rule set for evaluating listexpr in scripts **)
7.6 val list_rls =
7.7 - Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
7.8 - erls = Erls, srls = Erls, calc = [], errpatts = [],
7.9 - rules = (*8.01: copied from*)
7.10 - [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
7.11 + Rls{id = "list_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
7.12 + erls = Erls, srls = Erls, calc = [], errpatts = [],
7.13 + rules = [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
7.14 Thm ("o_apply", num_str @{thm o_apply}),
7.15
7.16 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
7.17 @@ -186,22 +185,13 @@
7.18 Thm ("tl_Cons",num_str @{thm tl_Cons}),
7.19 Thm ("tl_Nil",num_str @{thm tl_Nil}),
7.20 Thm ("zip_Cons",num_str @{thm zip_Cons}),
7.21 - Thm ("zip_Nil",num_str @{thm zip_Nil})
7.22 - ], scr = EmptyScr}:rls;
7.23 + Thm ("zip_Nil",num_str @{thm zip_Nil})],
7.24 + scr = EmptyScr}:rls;
7.25 *}
7.26
7.27 ML{*
7.28 -ruleset' := overwritelthy @{theory} (!ruleset',
7.29 - [("list_rls",list_rls)
7.30 - ]);
7.31 +ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
7.32 *}
7.33 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
7.34
7.35 -ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF Theory_Data*)*}
7.36 -ML {*
7.37 -(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
7.38 - AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
7.39 - HERE IS ME_Isa: 'eval_rls' not in system ...*)
7.40 -assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
7.41 -*}
7.42 end
8.1 --- a/src/Tools/isac/ProgLang/Script.thy Fri Sep 27 17:42:16 2013 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Script.thy Sun Sep 29 18:27:37 2013 +0200
8.3 @@ -178,7 +178,6 @@
8.4 val tacpbl = Unsynchronized.ref
8.5 (distinct (remove op = "" (!tacs (*@ !subpbls*))));
8.6 (*--^^^----- SHIFT? or delete ?*)
8.7 -
8.8 *}
8.9
8.10 end
9.1 --- a/src/Tools/isac/ProgLang/Tools.thy Fri Sep 27 17:42:16 2013 +0200
9.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Sun Sep 29 18:27:37 2013 +0200
9.3 @@ -218,11 +218,9 @@
9.4
9.5 (*for evaluating scripts*)
9.6
9.7 -val list_rls = append_rls "list_rls" list_rls
9.8 - [Calc ("Tools.rhs",eval_rhs "")];
9.9 -ruleset' := overwritelthy @{theory} (!ruleset',
9.10 - [("list_rls",list_rls)
9.11 - ]);
9.12 +val list_rls = append_rls "list_rls" list_rls [Calc ("Tools.rhs", eval_rhs "")];
9.13 +
9.14 +ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
9.15 *}
9.16 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
9.17 ML {*
9.18 @@ -233,6 +231,6 @@
9.19 ("lhs" ,("Tools.lhs" ,eval_lhs "")),
9.20 ("rhs" ,("Tools.rhs" ,eval_rhs ""))
9.21 ]);
9.22 +*}
9.23
9.24 -*}
9.25 end
10.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Fri Sep 27 17:42:16 2013 +0200
10.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sun Sep 29 18:27:37 2013 +0200
10.3 @@ -440,23 +440,9 @@
10.4 | SOME (t, ts) => SOME (term2str t, terms2str ts)
10.5 end;
10.6
10.7 -(*evaluate list-expressions
10.8 - should work on term, and stand in Isa99/rewrite-parse.sml,
10.9 - but there list_rls <- eval_binop is not yet defined*)
10.10 -(*fun eval_listexpr' ct =
10.11 - let val rew = rewrite_set "ListC" false "list_rls" ct;
10.12 - in case rew of
10.13 - SOME (res,_) => res
10.14 - | NONE => ct end;-----------------30.9.02---*)
10.15 fun eval_listexpr_ thy srls t =
10.16 -(* val (thy, srls, t) =
10.17 - ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
10.18 - *)
10.19 - let val rew = rewrite_set_ thy false srls t;
10.20 - in case rew of
10.21 - SOME (res,_) => res
10.22 - | NONE => t end;
10.23 -
10.24 + let val rew = rewrite_set_ thy false srls t;
10.25 + in case rew of SOME (res,_) => res | NONE => t end;
10.26
10.27 fun get_calculation' (thy:theory') op_ (ct:cterm') =
10.28 case get_calculation_ (assoc_thy thy) op_
11.1 --- a/src/Tools/isac/ROOT Fri Sep 27 17:42:16 2013 +0200
11.2 +++ b/src/Tools/isac/ROOT Sun Sep 29 18:27:37 2013 +0200
11.3 @@ -4,6 +4,12 @@
11.4
11.5 $ cd /usr/local/isabisac/
11.6 $ ./bin/isabelle build -d src/Tools/isac/ -v -b Isac
11.7 +
11.8 +see ~~/etc/settings
11.9 + ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
11.10 +before out-outcommenting (*, browser_info = true*) below and ...
11.11 +$ ./bin/isabelle build -o browser_info -v -c HOL
11.12 +$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v -b Isac
11.13 *)
11.14
11.15 session Isac in "~~/src/Tools/isac" = HOL +
11.16 @@ -15,5 +21,5 @@
11.17 the PolyML math-engine and Isabelle knowledge at RISC Linz.
11.18 See http://www.ist.tugraz.at/isac/.
11.19 *}
11.20 - options [document = false]
11.21 + options [document = false (*, browser_info = true*)]
11.22 theories Build_Isac
12.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Fri Sep 27 17:42:16 2013 +0200
12.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Sun Sep 29 18:27:37 2013 +0200
12.3 @@ -3,20 +3,14 @@
12.4 (c) due to copyright terms
12.5 *)
12.6
12.7 -theory xmlsrc imports
12.8 - "~~/src/Tools/isac/Interpret/Interpret"
12.9 -uses
12.10 - ("~~/src/Tools/isac/xmlsrc/mathml.sml")
12.11 - ("~~/src/Tools/isac/xmlsrc/datatypes.sml")
12.12 - ("~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml")
12.13 - ("~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml")
12.14 - ("~~/src/Tools/isac/xmlsrc/interface-xml.sml")
12.15 +theory xmlsrc imports "~~/src/Tools/isac/Interpret/Interpret"
12.16 +
12.17 begin
12.18
12.19 - use "~~/src/Tools/isac/xmlsrc/mathml.sml"
12.20 - use "~~/src/Tools/isac/xmlsrc/datatypes.sml"
12.21 - use "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml"
12.22 - use "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml"
12.23 - use "~~/src/Tools/isac/xmlsrc/interface-xml.sml"
12.24 + ML_file "~~/src/Tools/isac/xmlsrc/mathml.sml"
12.25 + ML_file "~~/src/Tools/isac/xmlsrc/datatypes.sml"
12.26 + ML_file "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml"
12.27 + ML_file "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml"
12.28 + ML_file "~~/src/Tools/isac/xmlsrc/interface-xml.sml"
12.29
12.30 end
12.31 \ No newline at end of file
13.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Fri Sep 27 17:42:16 2013 +0200
13.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Sun Sep 29 18:27:37 2013 +0200
13.3 @@ -6,13 +6,13 @@
13.4 (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset')
13.5 AT THE BOTTOM OF A THEORY:*)
13.6 length (KEStore_Elems.get_rlss @{theory}) = 0;
13.7 - length (! test_ruleset') = 1
13.8 + length (! test_ruleset') = 1 (* if you have clicked somewhere below *)
13.9 *}
13.10 -setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, Erls))] *}
13.11 +setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
13.12 ML {*
13.13 - test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("list_rls", Erls)])
13.14 + test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
13.15 ;
13.16 - if length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset') then ()
13.17 + if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
13.18 else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*}
13.19
13.20 setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
14.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Fri Sep 27 17:42:16 2013 +0200
14.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy Sun Sep 29 18:27:37 2013 +0200
14.3 @@ -2,9 +2,14 @@
14.4 imports Thy_1
14.5 begin
14.6
14.7 +ML {* val test_list_rls =
14.8 + append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})] *}
14.9 +
14.10 setup {* KEStore_Elems.add_rlss
14.11 - [("list_rls", (Context.theory_name @{theory}, (*already stored in Thy_1.thy*)
14.12 - Erls))] *}
14.13 -ML {* test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("list_rls", Erls)]) *}
14.14 + [("test_list_rls", (Context.theory_name @{theory}, (*already stored in Thy_1.thy*)
14.15 + test_list_rls))] *}
14.16 +
14.17 +ML {* test_ruleset' := overwritelthy @{theory} (! test_ruleset',
14.18 + [("test_list_rls", test_list_rls)]) *}
14.19
14.20 end
15.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Fri Sep 27 17:42:16 2013 +0200
15.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Sun Sep 29 18:27:37 2013 +0200
15.3 @@ -2,19 +2,30 @@
15.4 imports Thy_2
15.5 begin
15.6
15.7 -setup {* KEStore_Elems.add_rlss
15.8 - [("list_rls", (Context.theory_name @{theory}, (*already stored in Thy_1.thy and Thy_2.thy*)
15.9 - append_rls "list_rls" list_rls [Calc ("test_function", e_evalfn)]))] *}
15.10 +ML {* val test_list_rls =
15.11 + append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *}
15.12 +
15.13 +setup {* KEStore_Elems.add_rlss (*already stored in Thy_1.thy and Thy_2.thy*)
15.14 + [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *}
15.15 +
15.16 ML {*
15.17 if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*)
15.18 then () else error "rls identified by string-identifier, not by theory: changed"
15.19 -*}
15.20 -ML {*
15.21 - test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("list_rls",
15.22 - append_rls "list_rls" list_rls [Calc ("test_function", e_evalfn)])])
15.23 +
15.24 + test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls",
15.25 + append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])
15.26 ;
15.27 if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
15.28 then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"
15.29 + ;
15.30 + val SOME (_, Rls {rules, ...}) =
15.31 + AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls"
15.32 + ;
15.33 + case rules of
15.34 + [Thm ("not_def", _)] => ()
15.35 + | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
15.36 + (* merge rules of rls with the same identifier rls' must be done one level higher:
15.37 + KEStore_Elems.add_rlss does *add* or *overwrite* *)
15.38 *}
15.39
15.40 end
16.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy Fri Sep 27 17:42:16 2013 +0200
16.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy Sun Sep 29 18:27:37 2013 +0200
16.3 @@ -6,10 +6,23 @@
16.4 *}
16.5
16.6 ML {*
16.7 +*} ML {*
16.8 +KEStore_Elems.get_rlss @{theory}
16.9 +(*|> map check_kestore_rls
16.10 + |> enumerate_strings
16.11 + |> map writeln*)
16.12 +(*
16.13 +(rls, (Thy_5, Erls))--3
16.14 +(rls1, (Thy_4, Erls))--2
16.15 +(rls2, (Thy_4, Erls))--1
16.16 +(test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4
16.17 +*)
16.18 +*} ML {*
16.19 case KEStore_Elems.get_rlss @{theory} of
16.20 - ("rls", ("Thy_5", Erls)) :: ("rls2", ("Thy_4", Erls)) :: _ => ()
16.21 + ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => ()
16.22 | _ => raise error "KEStore_Elems.get_rlss changed"
16.23 ;
16.24 +*} ML {*
16.25 case KEStore_Elems.get_calcs @{theory} of
16.26 [("calc", ("Thy_1", _))] => ()
16.27 | _ => raise error "KEStore_Elems.get_calcs changed"
17.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Fri Sep 27 17:42:16 2013 +0200
17.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sun Sep 29 18:27:37 2013 +0200
17.3 @@ -16,6 +16,7 @@
17.4
17.5 structure KEStore_Elems: KESTORE_ELEMS =
17.6 struct
17.7 + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
17.8
17.9 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
17.10 structure Data = Theory_Data (
17.11 @@ -25,7 +26,7 @@
17.12 val merge = merge rls_eq;
17.13 );
17.14 fun get_rlss thy = Data.get thy
17.15 - fun add_rlss rlss = Data.map (union rls_eq rlss)
17.16 + fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss)
17.17
17.18 val calc_eq = rls_eq
17.19 structure Data = Theory_Data (
17.20 @@ -35,7 +36,7 @@
17.21 val merge = merge calc_eq;
17.22 );
17.23 fun get_calcs thy = Data.get thy
17.24 - fun add_calcs calcs = Data.map (union calc_eq calcs)
17.25 + fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs)
17.26
17.27 (*etc*)
17.28 end;
18.1 --- a/test/Tools/isac/Frontend/interface.sml Fri Sep 27 17:42:16 2013 +0200
18.2 +++ b/test/Tools/isac/Frontend/interface.sml Sun Sep 29 18:27:37 2013 +0200
18.3 @@ -11,10 +11,6 @@
18.4 "-----------------------------------------------------------------------------";
18.5 "-----------------------------------------------------------------------------";
18.6
18.7 -"within struct ---------------------------------------------------";
18.8 -"within struct ---------------------------------------------------";
18.9 -"within struct ---------------------------------------------------";
18.10 -(*==================================================================*)
18.11
18.12 "-------- TODO ---------------------------------------------------------------";
18.13 "-------- TODO ---------------------------------------------------------------";
19.1 --- a/test/Tools/isac/Test_Isac.thy Fri Sep 27 17:42:16 2013 +0200
19.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Sep 29 18:27:37 2013 +0200
19.3 @@ -13,7 +13,8 @@
19.4 *)
19.5
19.6 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
19.7 -(* !!!!! wait a minute until session Isac and the theories below are loaded !!!!! *)
19.8 +(* !!!!! say "OK" to the popup asking for theories to be loaded and !!!!!!!!!!!!! *)
19.9 +(* !!!!! watch the <Theories> window for errors in the "imports" below !!!!!!!!!! *)
19.10 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
19.11
19.12 theory Test_Isac imports Isac
19.13 @@ -152,7 +153,7 @@
19.14 section {* history of tests *}
19.15 text {*
19.16 Systematic regression tests have been introduced to isac development in 2003.
19.17 - Sanity of the regression test suffered from updates following Isabelle development,
19.18 + Sanity of the regression tests suffers from updates following Isabelle development,
19.19 which mostly exceeded the resources available in isac's development.
19.20
19.21 The survey below shall support to efficiently use the tests for isac
20.1 --- a/test/Tools/isac/kestore.sml Fri Sep 27 17:42:16 2013 +0200
20.2 +++ b/test/Tools/isac/kestore.sml Sun Sep 29 18:27:37 2013 +0200
20.3 @@ -8,6 +8,7 @@
20.4 "table of contents -----------------------------------------------------------";
20.5 "-----------------------------------------------------------------------------";
20.6 "-------- fun check_kestore_rls ----------------------------------------------";
20.7 +"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
20.8 "-----------------------------------------------------------------------------";
20.9 "-----------------------------------------------------------------------------";
20.10
20.11 @@ -24,3 +25,31 @@
20.12 |> sort string_ord
20.13 (*|> map writeln*)
20.14 ;
20.15 +
20.16 +"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
20.17 +"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
20.18 +"-------- fun KEStore_Elems.add_rlss overwrites earlier data -----------------";
20.19 + fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
20.20 + fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
20.21 +
20.22 +val data1 = [("test", ("theory-1", Erls)),
20.23 + ("test_rls", ("theory-1",
20.24 + append_rls "test_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]
20.25 +val data2 =
20.26 + [("test_rls", ("theory-2",
20.27 + append_rls "test_rls" e_rls [Thm ("not_def", @{thm not_def})]))]
20.28 +val data_3a = union rls_eq data1 data2
20.29 +val data_3b = union_overwrite rls_eq data1 data2
20.30 +
20.31 +val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3a "test_rls";
20.32 +case rules of
20.33 + [Thm ("not_def", _)] => ()
20.34 +| _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
20.35 +;
20.36 +val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3b "test_rls";
20.37 +case rules of
20.38 + [Thm ("refl", _), Thm ("subst", _)] => ()
20.39 +| _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"
20.40 +
20.41 +(* add_rlss will take union_overwrite due to argument sequence *)
20.42 +