1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Jun 11 16:11:26 2014 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Jun 15 18:27:23 2014 +0200
1.3 @@ -77,7 +77,8 @@
1.4 ML {* check_guhs_unique := false; *}
1.5 ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
1.6 ML {* @{theory "Isac"} *}
1.7 -ML {* ! isab_thm_thy *}
1.8 +ML {* CHECK_FILLPATS "at end of Build_Isac";
1.9 +(*"CHECK_FILLPATS: diff_sin_chain exists, fillpat --> NOT empty !!!"*)*}
1.10
1.11 section {* State of approaching Isabelle by Isac *}
1.12 text {*
2.1 --- a/src/Tools/isac/Frontend/Frontend.thy Wed Jun 11 16:11:26 2014 +0200
2.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Sun Jun 15 18:27:23 2014 +0200
2.3 @@ -3,14 +3,9 @@
2.4 (c) due to copyright terms
2.5 *)
2.6
2.7 -theory Frontend imports "~~/src/Tools/isac/xmlsrc/xmlsrc"
2.8 +theory Frontend
2.9 +imports "~~/src/Tools/isac/xmlsrc/xmlsrc"
2.10 begin
2.11 -ML {* val Rls {rules = rrr, ...} = assoc_rls' @{theory} "list_rls" *}
2.12 -ML {* length rrr = 53 *}
2.13 -ML {* AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *}
2.14 -ML {* val SOME (_, (Rls {rules = kkk, ...})) =
2.15 - AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *}
2.16 -ML {* length kkk = 42 *}
2.17
2.18 ML_file "~~/src/Tools/isac/Frontend/messages.sml"
2.19 ML_file "~~/src/Tools/isac/Frontend/states.sml"
3.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed Jun 11 16:11:26 2014 +0200
3.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sun Jun 15 18:27:23 2014 +0200
3.3 @@ -294,21 +294,6 @@
3.4 ["normalize","univariate","equations"] is the related pblID
3.5 WN.24.4.03: also used for metID*)
3.6
3.7 -fun app_py p f (d:pblID) (k:pblRD) = let
3.8 - fun py_err _ =
3.9 - error ("app_py: not found: " ^ (strs2str d));
3.10 - fun app_py' _ [] = py_err ()
3.11 - | app_py' [] _ = py_err ()
3.12 - | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) =
3.13 - if k0 = k' then f p' else app_py' [k0] ps
3.14 - | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =
3.15 - if k0 = k'' then app_py' ks ps else app_py' k' ps';
3.16 - in app_py' k p end;
3.17 -
3.18 -fun get_py p = let
3.19 - fun extract_py (Ptyp (_, [py], _)) = py
3.20 - | extract_py _ = error ("extract_py: Ptyp has wrong format.");
3.21 - in app_py p extract_py end;
3.22
3.23 (*> ptyps:=
3.24 [Ptyp ("1",[("ptyp 1",([],[]))],
4.1 --- a/src/Tools/isac/KEStore.thy Wed Jun 11 16:11:26 2014 +0200
4.2 +++ b/src/Tools/isac/KEStore.thy Sun Jun 15 18:27:23 2014 +0200
4.3 @@ -34,7 +34,9 @@
4.4 val get_mets: theory -> mets
4.5 val add_mets: (met * metID) list -> theory -> theory
4.6 val get_thes: theory -> (thydata ptyp) list
4.7 - val add_thes: (thydata * theID) list -> theory -> theory
4.8 + val add_thes: (thydata * theID) list -> theory -> theory (* thydata dropped at existing elems *)
4.9 + val insert_fillpats: (theID * fillpat list) list -> theory -> theory
4.10 + (* fillpat update !existing elems *)
4.11 end;
4.12
4.13 structure KEStore_Elems: KESTORE_ELEMS =
4.14 @@ -103,9 +105,33 @@
4.15 );
4.16 fun get_thes thy = Data.get thy
4.17 fun add_thes thes thy = let
4.18 - fun add_the (the, theID) = insrt theID the theID
4.19 - (*needs no (!check_guhs_unique) because guh is generated automatically*)
4.20 + fun add_the (thydata, theID) =
4.21 + if can_insert theID (Data.get thy)
4.22 + then
4.23 + if exist_the theID (Data.get thy)
4.24 + then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
4.25 + else insrt theID thydata theID
4.26 + else
4.27 + let
4.28 + val th' = fill_parents (Data.get thy) theID theID (*..*** insert: not found*)
4.29 + val th' = insrt theID thydata theID th'
4.30 + in merge_ptyps' th' end; (*...TODO improve efficiency:
4.31 + val ((exist, notexist) branch) = fill_parents ([], theID) (Data.get thy)
4.32 + (* fill_parents: can_insert (hd theID), then insert the branch built from there;
4.33 + fill_parents probably could generalise to the then-branch above *)
4.34 + in insrt_branch exist branch end (*notexist is in branch*)*)
4.35 in Data.map (fold add_the thes) thy end;
4.36 + fun insert_fillpats fis thy =
4.37 + let
4.38 + fun update_elem (theID, fillpats) =
4.39 + let
4.40 + val hthm = get_py (Data.get thy) theID theID
4.41 + val hthm' = update_hthm hthm fillpats
4.42 + handle ERROR _ =>
4.43 + error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
4.44 + in update_ptyps theID theID hthm' end
4.45 + in Data.map (fold update_elem fis) thy end
4.46 +
4.47 end;
4.48 *}
4.49
4.50 @@ -147,26 +173,15 @@
4.51 ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_ptyps;
4.52 fun get_mets () =
4.53 ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_mets;
4.54 -fun get_thes () =
4.55 +fun get_thes () =
4.56 ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_thes;
4.57 *}
4.58 setup {* KEStore_Elems.add_rlss
4.59 [("e_rls", (Context.theory_name @{theory}, e_rls)),
4.60 ("e_rrls", (Context.theory_name @{theory}, e_rrls))] *}
4.61
4.62 -ML {*
4.63 -(* determine sequence of main parts*)
4.64 -val (theID1, thydata1) =
4.65 - (["IsacKnowledge"] : theID, Html {guh = part2guh ["IsacKnowledge"], html = "",
4.66 - mathauthors = ["Isac team"], coursedesign = []})
4.67 -val (theID2, thydata2) =
4.68 - (["Isabelle"] : theID, Html {guh = part2guh ["Isabelle"], html = "",
4.69 - mathauthors = ["Isabelle team, TU Munich"], coursedesign = []})
4.70 -val (theID3, thydata3) =
4.71 - (["IsacScripts"] : theID, Html {guh = part2guh ["IsacScripts"], html = "",
4.72 - mathauthors = ["Isac team"], coursedesign = []})
4.73 -*}
4.74 -setup {* (* determine sequence of main parts in thehier *)
4.75 +section {* determine sequence of main parts in thehier *}
4.76 +setup {*
4.77 KEStore_Elems.add_thes
4.78 [(Html {guh = part2guh ["IsacKnowledge"], html = "",
4.79 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
5.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Jun 11 16:11:26 2014 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Jun 15 18:27:23 2014 +0200
5.3 @@ -90,15 +90,14 @@
5.4 collect_part "IsacScripts" proglang_parent progthys'
5.5 : (theID * thydata) list
5.6 *}
5.7 -(*setup {* KEStore_Elems.add_thes (map swap thydata_list) *}
5.8 -insert: not found ["IsacKnowledge","Test_Build_Thydata","Theorems","thm111"]*)
5.9 +setup {* KEStore_Elems.add_thes (map swap thydata_list) *}
5.10
5.11 section {* interface for dialog-authoring *}
5.12 -
5.13 (*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)
5.14 setup {*
5.15 KEStore_Elems.add_thes
5.16 - [make_thy @{theory "Diff"} ["Isabelle2011-->12"],
5.17 + [
5.18 +(*make_thy @{theory "Diff"} ["Isabelle2011-->12"],
5.19 make_isa @{theory "Diff"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
5.20 make_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
5.21 ["Isabelle2011-->12"],
5.22 @@ -113,7 +112,7 @@
5.23
5.24 make_isa @{theory "Diff"} ("IsacKnowledge", "Rulesets") ["Isabelle2011-->12"],
5.25 make_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"],
5.26 -
5.27 +*)
5.28 make_thy @{theory "Test"} ["Isabelle2011-->12"],
5.29 make_isa @{theory "Test"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
5.30 make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
5.31 @@ -137,8 +136,8 @@
5.32 *}
5.33
5.34 setup {*
5.35 -KEStore_Elems.add_thes
5.36 - [insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
5.37 +KEStore_Elems.insert_fillpats
5.38 + [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
5.39 ([("fill-d_d-arg",
5.40 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
5.41 ("fill-both-args",
5.42 @@ -148,7 +147,7 @@
5.43 ("fill-inner-deriv",
5.44 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
5.45 ("fill-all",
5.46 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list)
5.47 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list))
5.48 ]
5.49 *}
5.50
5.51 @@ -225,8 +224,9 @@
5.52 ]: fillpat list;
5.53 *)
5.54
5.55 -(* still ununsed; planned for stepToErrorpattern: this is just a reminder... *)
5.56 -
5.57 +(* still ununsed; planned for stepToErrorpattern: this is just a reminder:
5.58 + adapt analogously to KEStore_Elems.add_thes [insert_fillpats ...
5.59 + ---9c19751b2ad1---> KEStore_Elems.insert_fillpats *)
5.60 insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
5.61 (["chain-rule-diff-both", "cancel"]: errpatID list);
5.62
5.63 @@ -250,8 +250,4 @@
5.64 Adjust ''val path'' (for details see wiki) and copy line for line
5.65 into the ML-block below:
5.66 *}
5.67 -ML {*
5.68 -
5.69 -*}
5.70 -
5.71 end
6.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Jun 11 16:11:26 2014 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sun Jun 15 18:27:23 2014 +0200
6.3 @@ -405,4 +405,47 @@
6.4 setup {* KEStore_Elems.add_cas
6.5 [((term_of o the o (parse thy)) "Differentiate",
6.6 (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))] *}
6.7 +
6.8 +(* trying to find the reasons, why insert_fillpats are empty in test/../inform.sml
6.9 + after uncommenting setup KEStore_Elems.add_thes (map swap thydata_list)
6.10 + in Build_Thydata.thy;
6.11 + trial: *shift* all KEStore_Elems.add_thes from Build_Thydata.thy to here... *)
6.12 +(*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)
6.13 +ML {*
6.14 +fun CHECK_FILLPATS location =
6.15 + (get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"];
6.16 + let val Hthm {fillpats, ...} = get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
6.17 + in case fillpats of
6.18 + [] => "CHECK_FILLPATS at: " ^ location ^ ": diff_sin_chain exists, fillpat --> []"
6.19 + | _ => "CHECK_FILLPATS at: " ^ location ^ ": diff_sin_chain exists, fillpat --> NOT empty !!!"
6.20 + end)
6.21 + handle _ =>
6.22 + ("CHECK_FILLPATS at: " ^ location ^ ": diff_sin_chain does NOT exist");
6.23 +*}
6.24 +setup {*
6.25 +KEStore_Elems.add_thes
6.26 + [make_thy @{theory} ["Isabelle2011-->12"],
6.27 + make_isa @{theory} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
6.28 + make_thm @{theory} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
6.29 + ["Isabelle2011-->12"],
6.30 + make_thm @{theory} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})
6.31 + ["Isabelle2011-->12"],
6.32 + make_thm @{theory} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
6.33 + ["Isabelle2011-->12"],
6.34 + make_thm @{theory} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
6.35 + ["Isabelle2011-->12"],
6.36 + make_thm @{theory} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
6.37 + ["Isabelle2011-->12"],
6.38 +
6.39 + make_isa @{theory} ("IsacKnowledge", "Rulesets") ["Isabelle2011-->12"],
6.40 + make_rls @{theory} norm_diff ["Isabelle2011-->12"]
6.41 +(*,
6.42 + make_thy @{theory "Test"} ["Isabelle2011-->12"],
6.43 + make_isa @{theory "Test"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
6.44 + make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
6.45 + ["Isabelle2011-->12"]
6.46 +*)
6.47 + ]
6.48 +*}
6.49 +(*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
6.50 end
7.1 --- a/src/Tools/isac/calcelems.sml Wed Jun 11 16:11:26 2014 +0200
7.2 +++ b/src/Tools/isac/calcelems.sml Sun Jun 15 18:27:23 2014 +0200
7.3 @@ -897,6 +897,20 @@
7.4 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
7.5 );
7.6
7.7 +fun update_ptyps ID _ _ [] =
7.8 + error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
7.9 + | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
7.10 + if i = key
7.11 + then
7.12 + if length pys = 0
7.13 + then ((Ptyp (key, [data], [])) :: pyss)
7.14 + else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
7.15 + else py :: update_ptyps ID [i] data pyss
7.16 + | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
7.17 + if i = key
7.18 + then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
7.19 + else (py :: (update_ptyps ID (i :: is) data pyss))
7.20 +
7.21 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
7.22 function for trees / ptyps *)
7.23 fun merge_ptyps ([], pt) = pt
7.24 @@ -905,7 +919,7 @@
7.25 if k = k'
7.26 then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
7.27 else x' :: merge_ptyps (xs, xs');
7.28 -
7.29 +fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2)
7.30
7.31 (* data for methods stored in 'methods'-database*)
7.32 type met =
7.33 @@ -1006,22 +1020,75 @@
7.34 parents of thydata in list, missing in thehier, are inserted
7.35 (causing msgs '*** insert: not found');
7.36 (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
7.37 -fun the_hier th ([]: (theID * thydata) list) = th
7.38 - | the_hier th ((theID, thydata)::ths) =
7.39 - if can_insert theID th
7.40 - then
7.41 +fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)
7.42 + let
7.43 + fun add_the th ((thydata, theID)) =
7.44 + if can_insert theID th
7.45 + then
7.46 + if exist_the theID th
7.47 + then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
7.48 + else insrt theID thydata theID
7.49 + else
7.50 + let
7.51 + val th' = fill_parents th theID theID (*..*** insert: not found*)
7.52 + val th' = insrt theID thydata theID th'
7.53 + in merge_ptyps' th' end;
7.54 +in fold (add_the th) thes end
7.55 +
7.56 +
7.57 +fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
7.58 + Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
7.59 + fillpats = fillpats', thm = thm}
7.60 + | update_hthm _ _ = raise ERROR "wrong data";
7.61 +
7.62 +(* for interface for dialog-authoring *)
7.63 +fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
7.64 + let
7.65 + val rls' =
7.66 + case rls of
7.67 + Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
7.68 + Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
7.69 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
7.70 + | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
7.71 + Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
7.72 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
7.73 + | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>
7.74 + Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
7.75 + scr = scr, errpatts = errpatIDs}
7.76 + | Erls => Erls
7.77 + in
7.78 + Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
7.79 + thy_rls = (thyID, rls')}
7.80 + end
7.81 + | update_hrls _ _ = raise ERROR "wrong data";
7.82 +
7.83 +fun app_py p f (d:pblID) (k(*:pblRD*)) = let
7.84 + fun py_err _ =
7.85 + error ("app_py: not found: " ^ (strs2str d));
7.86 + fun app_py' _ [] = py_err ()
7.87 + | app_py' [] _ = py_err ()
7.88 + | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) =
7.89 + if k0 = k' then f p' else app_py' [k0] ps
7.90 + | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =
7.91 + if k0 = k'' then app_py' ks ps else app_py' k' ps';
7.92 + in app_py' k p end;
7.93 +
7.94 +fun get_py p = let
7.95 + fun extract_py (Ptyp (_, [py], _)) = py
7.96 + | extract_py _ = error ("extract_py: Ptyp has wrong format.");
7.97 + in app_py p extract_py end;
7.98 +
7.99 +(*
7.100 +fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)
7.101 + let
7.102 + fun update_elem th (theID, fillpats) =
7.103 let
7.104 - val th' =
7.105 - if exist_the theID th
7.106 - then (writeln ("*** insert: preserved " ^ strs2str theID); th)
7.107 - else insrt theID thydata theID th
7.108 - in the_hier th' ths end
7.109 - else
7.110 - let
7.111 - val th' = fill_parents th theID theID (*..*** insert: not found*)
7.112 - val th' = insrt theID thydata theID th'
7.113 - in the_hier th' ths end;
7.114 -
7.115 + val hthm = get_py th theID theID
7.116 + val hthm' = update_hthm hthm fillpats
7.117 + handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
7.118 + in update_ptyps theID theID hthm' end
7.119 + in fold (update_elem th) fis end
7.120 + *)
7.121 (*
7.122 end (*struct*)
7.123 *)
8.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Jun 11 16:11:26 2014 +0200
8.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Jun 15 18:27:23 2014 +0200
8.3 @@ -51,19 +51,11 @@
8.4 |> map (fn a => (string_of_thm a, prop_of a))
8.5 : (thmID * term) list
8.6
8.7 -fun collect_thms' (part, thy') = (*delete*)
8.8 - let val thy = assoc_thy (thyID2theory' thy')
8.9 - in map (makeHthm (part, thy')) (Theory.axioms_of thy) end;
8.10 -fun collect_thms'' part thy =
8.11 +fun collect_thms part thy =
8.12 map (makeHthm (part, Context.theory_name thy)) (Theory.axioms_of thy);
8.13
8.14 (*.collect all rulesets defined in in a theory and insert the guh.*)
8.15 -fun collect_rlss (part, thy') = (*delete*)
8.16 - let val rlss = filter ((curry op= thy') o
8.17 - ((#1 o #2):(rls' * (theory' * rls)) -> theory'))
8.18 - (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
8.19 - in map (makeHrls part) rlss end;
8.20 -fun collect_rlss' part rlss thys = (rlss : (rls' * (thyID * rls)) list)
8.21 +fun collect_rlss part rlss thys = (rlss : (rls' * (thyID * rls)) list)
8.22 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
8.23 |> map (makeHrls part)
8.24
8.25 @@ -79,15 +71,9 @@
8.26 in [(*TODO.WN060120 rew_ord, Calc*)]:(theID * thydata) list end;
8.27
8.28 (*.collect all data for a thy TODO.WN060120 rew_ord, Calc.*)
8.29 -(* val thy' = nth 1 scri_thys;
8.30 - *)
8.31 -fun collect_thy part(*IsacScripts|IsacKnowledge*) (thy': theory') = (*delete*)
8.32 - ((collect_thms' (part, thy')) @ (collect_rlss (part, thy')) @
8.33 - (collect_cals (part, thy')) @ (collect_ords (part, thy')))
8.34 - : (theID * thydata) list;
8.35 fun collect_part part parent thys =
8.36 - (flat (map (collect_thms'' part) thys)) @
8.37 - (collect_rlss' part (KEStore_Elems.get_rlss parent) thys) @
8.38 + (flat (map (collect_thms part) thys)) @
8.39 + (collect_rlss part (KEStore_Elems.get_rlss parent) thys) @
8.40 [(*TODO: collect_cals, collect_ords*)]
8.41
8.42 (*.collect theorems defined in Isabelle (before Isac is evaluated above).*)
8.43 @@ -106,14 +92,16 @@
8.44 mathauthors = ["Isabelle team, TU Munich"],
8.45 coursedesign = []});
8.46
8.47 +(* TODO Deleted called funs ---------------------------------------------------------
8.48 (*.create a list with all thydata=thyelements=the;
8.49 - this list is used by 'fun the_hier' to create the hierarchy .*)
8.50 + this list is used by KEStore_Elems.add_thes to create the hierarchy .*)
8.51 fun collect_thydata knowthys' progthys' rlsthmsNOTisac = (*delete*)
8.52 [isabelle_page] @
8.53 (map (collect_isab "Isabelle") rlsthmsNOTisac) @
8.54 ((flat o (map (collect_thy "IsacScripts"))) (map Context.theory_name progthys')) @
8.55 ((flat o (map (collect_thy "IsacKnowledge"))) (map Context.theory_name knowthys')):
8.56 (theID * thydata) list;
8.57 +------------------------------------------------------------------------------------*)
8.58
8.59 fun show_thes () = (writeln o format_pblIDl o (scan [])) (get_thes ());
8.60
8.61 @@ -304,32 +292,6 @@
8.62 ord = ord}
8.63 in (the, theID) end
8.64
8.65 -fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
8.66 - Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
8.67 - fillpats = fillpats', thm = thm}
8.68 - | update_hthm _ _ = raise ERROR "wrong data";
8.69 -
8.70 -(* for interface for dialog-authoring *)
8.71 -fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
8.72 - let
8.73 - val rls' =
8.74 - case rls of
8.75 - Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
8.76 - Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
8.77 - calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
8.78 - | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
8.79 - Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
8.80 - calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
8.81 - | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>
8.82 - Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
8.83 - scr = scr, errpatts = errpatIDs}
8.84 - | Erls => Erls
8.85 - in
8.86 - Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
8.87 - thy_rls = (thyID, rls')}
8.88 - end
8.89 - | update_hrls _ _ = raise ERROR "wrong data";
8.90 -
8.91 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
8.92 fun insert_fillpats theID fillpats =
8.93 let
9.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Wed Jun 11 16:11:26 2014 +0200
9.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Sun Jun 15 18:27:23 2014 +0200
9.3 @@ -17,6 +17,7 @@
9.4 "-------- hard-coded val rlsthmsNOTisac -----------------";
9.5 "-------- the_hier (get_thes ()) thydata_list -------------";
9.6 "-------- retrieve errpats ------------------------------";
9.7 +"-------- ERROR insert: not found [... ------------------";
9.8 "--------------------------------------------------------";
9.9 "--------------------------------------------------------";
9.10 "--------------------------------------------------------";
9.11 @@ -1024,3 +1025,10 @@
9.12 case errpats of [("chain-rule-diff-both", _, _)] => ()
9.13 | _ => error "errpats chain-rule-diff-both changed"
9.14
9.15 +"-------- ERROR insert: not found [... ------------------";
9.16 +"-------- ERROR insert: not found [... ------------------";
9.17 +"-------- ERROR insert: not found [... ------------------";
9.18 +(* in Build_Thydata.thy:
9.19 +setup {* KEStore_Elems.add_thes (map swap thydata_list) *}
9.20 +insert: not found ["IsacKnowledge","Test_Build_Thydata","Theorems","thm111"]*)
9.21 +
10.1 --- a/test/Tools/isac/calcelems.sml Wed Jun 11 16:11:26 2014 +0200
10.2 +++ b/test/Tools/isac/calcelems.sml Sun Jun 15 18:27:23 2014 +0200
10.3 @@ -11,6 +11,7 @@
10.4 "-------- fun term2str ----------------------------------";
10.5 "-------- fun thmID_of_derivation_name 000---------------";
10.6 "-------- fun merge_rlss -----------------------------------------------------";
10.7 +"-------- fun update_ptyps --------------------------------------------------";
10.8 "--------------------------------------------------------";
10.9 "--------------------------------------------------------";
10.10 "--------------------------------------------------------";
10.11 @@ -113,3 +114,45 @@
10.12 [Thm ("subst", _), Thm ("refl", _), Thm ("False_def", _)] => ()
10.13 | _ => error "merge_rlss changed"
10.14
10.15 +"-------- fun update_ptyps --------------------------------------------------";
10.16 +"-------- fun update_ptyps --------------------------------------------------";
10.17 +"-------- fun update_ptyps --------------------------------------------------";
10.18 +val pty = [
10.19 + Ptyp ("aaa", [1], [
10.20 + Ptyp ("aaa-1", [11], [])]),
10.21 + Ptyp ("bbb", [2], [
10.22 + Ptyp ("bbb-1", [21], []),
10.23 + Ptyp ("bbb-2", [22], [
10.24 + Ptyp ("bbb-21", [221], []),
10.25 + Ptyp ("bbb-22", [222], [])])]),
10.26 + Ptyp ("ccc", [3], [])] : int ptyp list
10.27 +
10.28 +val ID = ["ddd"];
10.29 +(*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)
10.30 +
10.31 +val ID = ["ccc"];
10.32 +if update_ptyps ID ID 99999 pty =
10.33 + [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
10.34 + Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []),
10.35 + Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [222], [])])]),
10.36 + Ptyp ("ccc", [99999], [])]
10.37 + then () else error "update_ptyps has changed 1";
10.38 +
10.39 +val ID = ["aaa"];
10.40 +(*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] has descendants*)
10.41 +
10.42 +val ID = ["bbb", "bbb-2", "bbb-21"];
10.43 +if update_ptyps ID ID 99999 pty =
10.44 + [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
10.45 + Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []), Ptyp ("bbb-2", [22],
10.46 + [Ptyp ("bbb-21", [99999], []), Ptyp ("bbb-22", [222], [])])]),
10.47 + Ptyp ("ccc", [3], [])]
10.48 +then () else error "update_ptyps has changed 2";
10.49 +
10.50 +val ID = ["bbb", "bbb-2", "bbb-22"];
10.51 +if update_ptyps ID ID 99999 pty =
10.52 + [Ptyp ("aaa", [1], [Ptyp ("aaa-1", [11], [])]),
10.53 + Ptyp ("bbb", [2], [Ptyp ("bbb-1", [21], []),
10.54 + Ptyp ("bbb-2", [22], [Ptyp ("bbb-21", [221], []), Ptyp ("bbb-22", [99999], [])])]),
10.55 + Ptyp ("ccc", [3], [])]
10.56 +then () else error "update_ptyps has changed 3";
11.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Jun 11 16:11:26 2014 +0200
11.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Jun 15 18:27:23 2014 +0200
11.3 @@ -15,7 +15,6 @@
11.4 "table of contents -----------------------------------------------";
11.5 "-----------------------------------------------------------------";
11.6 "----------- thm_hier --------------------------------------------";
11.7 -"----------- fun thydata2xml -------------------------------------";
11.8 "----------- write xml to tmp ------------------------------------";
11.9 "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
11.10 "----------- ### thes2file ... Exception- Match raised -----------";
11.11 @@ -25,7 +24,6 @@
11.12 "----------- fun insert_errpatIDs --------------------------------";
11.13 "--------- (*collect_part: data too large for buffers*) ----------";
11.14 "----------- collect thydata from Test_Build_Thydata.thy ---------";
11.15 -"----------- the_hier from Test_Build_Thydata.thy ----------------";
11.16 "----------- correct theIDs for e_rls ----------------------------";
11.17 "----------- correct theIDs for list_rls -------------------------";
11.18 "-----------------------------------------------------------------";
11.19 @@ -51,7 +49,7 @@
11.20 makeHthm ("IsacKnowledge", thy') ("Integrate.integral_var", thm);
11.21 (makeHthm ("IsacKnowledge", thy')) ("Integrate.integral_var", thm);
11.22 map (makeHthm ("IsacKnowledge", thy')) (Theory.axioms_of thy);
11.23 -collect_thms' ("IsacKnowledge", thy');
11.24 +collect_thms "IsacKnowledge" thy;
11.25
11.26 "collect_rlss thy'------------------------------------------------";
11.27 makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules));
11.28 @@ -60,38 +58,7 @@
11.29 val rlss = filter ((curry op= thy') o
11.30 ((#1 o #2):(rls' * (theory' * rls)) -> theory'))
11.31 (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));
11.32 -collect_rlss ("IsacKnowledge",thy');
11.33 -
11.34 -(* collect_thy and others below changed in 2014 *)
11.35 -
11.36 -
11.37 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ WN140313
11.38 -"----------- fun thydata2xml -------------------------------------";
11.39 -"----------- fun thydata2xml -------------------------------------";
11.40 -"----------- fun thydata2xml -------------------------------------";
11.41 -(*========== inhibit exn AK110725 ================================================
11.42 -val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"];
11.43 -val thmdata = get_the theID;
11.44 -writeln(thydata2xml (theID, thmdata));
11.45 -
11.46 -val theID = ["IsacKnowledge", "Poly", "Rulesets", "norm_Poly"];
11.47 -val rlsdata = get_the theID;
11.48 -writeln(thydata2xml (theID, rlsdata));
11.49 -========== inhibit exn AK110725 ================================================*)
11.50 -
11.51 -(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
11.52 - see sml/../datatypes.sml !
11.53 -val (thy', rls') = ("DiffApp", "Tools.rhs");
11.54 -thy_containing_rls thy' rls';
11.55 -print_depth 99; map #1 startsearch; print_depth 3;
11.56 -*)
11.57 -
11.58 -(*
11.59 -val path = "../../tmp/";
11.60 -thes2file path;
11.61 -*)
11.62 -@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ WN140313 @@@*)
11.63 -
11.64 +collect_rlss "IsacKnowledge" rlss [thy];
11.65
11.66 "----------- write xml to tmp ------------------------------------";
11.67 "----------- write xml to tmp ------------------------------------";
11.68 @@ -371,17 +338,6 @@
11.69 mathauthors = ["isac-team"], thm = _})] => ()
11.70 | _ => error "collect thydata from Test_Build_Thydata changed";
11.71
11.72 -"----------- the_hier from Test_Build_Thydata.thy ----------------";
11.73 -"----------- the_hier from Test_Build_Thydata.thy ----------------";
11.74 -"----------- the_hier from Test_Build_Thydata.thy ----------------";
11.75 -(*WE CIRCUMVENT TO STORE TO KEStore_Elems.*)
11.76 -val thehierTEST = [];
11.77 -insrt theID1 thydata1 theID1 thehierTEST; (*se KEStore.thy*)
11.78 -insrt theID1 thydata2 theID2 thehierTEST;
11.79 -insrt theID1 thydata3 theID3 thehierTEST;
11.80 -;
11.81 -val thehierTEST = the_hier thehierTEST(*NO store_thm ETC*) thydata_list;
11.82 -
11.83 "----------- xml from Test_Build_Thydata.thy ---------------------";
11.84 "----------- xml from Test_Build_Thydata.thy ---------------------";
11.85 "----------- xml from Test_Build_Thydata.thy ---------------------";