1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 16:43:53 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Apr 20 15:54:19 2020 +0200
1.3 @@ -29,15 +29,14 @@
1.4 ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
1.5 ML_file "rule-set.sml"
1.6
1.7 -ML_file "celem-0.sml" (*survey Celem.*)
1.8 ML_file "store.sml"
1.9 +ML_file "check-unique.sml"
1.10 ML_file "specification.sml"
1.11 ML_file "celem-4.sml" (*pat*)
1.12 ML_file "celem-5.sml" (*ptyps*)
1.13 ML_file "celem-6.sml" (*mets*)
1.14 ML_file "celem-7.sml" (*cas_elem*)
1.15 ML_file "celem-8.sml" (*thydata*)
1.16 -ML_file "celem-91.sml" (*check_guhs_unique*)
1.17
1.18 ML_file tracing.sml
1.19 ML \<open>
1.20 @@ -119,7 +118,7 @@
1.21 fun add_pbts pbts thy = let
1.22 fun add_pbt (pbt as {guh,...}, pblID) =
1.23 (* the pblID has the leaf-element as first; better readability achieved *)
1.24 - (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
1.25 + (if (!Check_Unique.check_guhs_unique) then Celem5.check_pblguh_unique guh (Data.get thy) else ();
1.26 rev pblID |> Store.insrt pblID pbt);
1.27 in Data.map (fold add_pbt pbts) thy end;
1.28
1.29 @@ -132,7 +131,7 @@
1.30 val get_mets = Data.get;
1.31 fun add_mets mets thy = let
1.32 fun add_met (met as {guh,...}, metID) =
1.33 - (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
1.34 + (if (!Check_Unique.check_guhs_unique) then Celem6.check_metguh_unique guh (Data.get thy) else ();
1.35 Store.insrt metID met metID);
1.36 in Data.map (fold add_met mets) thy end;
1.37
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 16:43:53 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Mon Apr 20 15:54:19 2020 +0200
2.3 @@ -136,7 +136,7 @@
2.4 type calcID = int;
2.5
2.6 (*/------- to Celem2 -------\*)
2.7 -type guh = Spec.guh;
2.8 +type guh = Check_Unique.guh;
2.9 (*\------- to Celem2 -------/*)
2.10 type xml = string; (* rm together with old code replaced by XML.tree *)
2.11
2.12 @@ -295,11 +295,11 @@
2.13 (*\------- to Celem6 -------/*)
2.14
2.15 (*/------- to Celem91 -------\*)
2.16 -val check_guhs_unique = Celem91.check_guhs_unique;
2.17 -val coll_pblguhs = Celem91.coll_pblguhs;
2.18 -val check_pblguh_unique = Celem91.check_pblguh_unique;
2.19 -val coll_metguhs = Celem91.coll_metguhs;
2.20 -val check_metguh_unique = Celem91.check_metguh_unique;
2.21 +val check_guhs_unique = Check_Unique.check_guhs_unique;
2.22 +val coll_pblguhs = Check_Unique.collect (#guh : Celem5.pbt -> Check_Unique.guh);
2.23 +val check_pblguh_unique = Celem5.check_pblguh_unique;
2.24 +val coll_metguhs = Check_Unique.collect (#guh : Celem6.met -> Check_Unique.guh);
2.25 +val check_metguh_unique = Celem6.check_metguh_unique;
2.26 (*\------- to Celem91 -------/*)
2.27
2.28 (*/------- to Celem8 -------\*)
3.1 --- a/src/Tools/isac/BaseDefinitions/celem-0.sml Sun Apr 19 16:43:53 2020 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,72 +0,0 @@
3.4 -(* Title: BaseDefinitions/celem-0.sml
3.5 - Author: Walther Neuper
3.6 - (c) due to copyright terms
3.7 -
3.8 - *)
3.9 -signature CALCELEMENT_0 =
3.10 -(*/------- to Celem0 -------\*)
3.11 -(*\------- to Celem0 -------/*)
3.12 -sig
3.13 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.14 - (*NONE*)
3.15 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.16 - (*NONE*)
3.17 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.18 -end
3.19 -
3.20 -(**)
3.21 -structure Celem0(**): CALCELEMENT_0(**) =
3.22 -struct
3.23 -(**)
3.24 -(*
3.25 -val get_cas: theory -> Celem7.cas_elem list
3.26 - val add_cas: Celem7.cas_elem list -> theory -> theory
3.27 - val get_ptyps: theory -> Celem5.ptyps
3.28 - val add_pbts: (Celem5.pbt * Spec.pblID) list -> theory -> theory
3.29 - val get_mets: theory -> Celem6.mets
3.30 - val add_mets: (Celem6.met * Spec.metID) list -> theory -> theory
3.31 - val get_thes: theory -> (Celem8.thydata Store.ptyp) list
3.32 - val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
3.33 - val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
3.34 - type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
3.35 - val merge = merge Celem7.cas_eq;
3.36 - fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
3.37 - type T = Celem5.ptyps;
3.38 - val empty = [Celem5.e_Ptyp];
3.39 - val merge = Store.merge_ptyps;
3.40 - (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
3.41 - rev pblID |> Store.insrt pblID pbt);
3.42 - type T = Celem6.mets;
3.43 - val empty = [Celem6.e_Mets];
3.44 - val merge = Store.merge_ptyps;
3.45 - (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
3.46 - Store.insrt metID met metID);
3.47 - type T = (Celem8.thydata Store.ptyp) list;
3.48 - val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
3.49 - fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
3.50 - val hthm = Store.get_py (Data.get thy) theID theID
3.51 - val hthm' = Celem8.update_hthm hthm fillpats
3.52 - in Store.update_ptyps theID theID hthm' end
3.53 - [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
3.54 - (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
3.55 - (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
3.56 -fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
3.57 - (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
3.58 - | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
3.59 -fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
3.60 - (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
3.61 -val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
3.62 -fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
3.63 -fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
3.64 - | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
3.65 - ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
3.66 -fun metguh2str ({guh,...} : Celem6.met) = guh : string;
3.67 -fun check_kestore_met (mp: Celem6.met Store.ptyp) =
3.68 -fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
3.69 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
3.70 - |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))
3.71 -*)
3.72 -(*/------- to Celem0 -------\*)
3.73 -(*\------- to Celem0 -------/*)
3.74 -
3.75 -(**)end(**)
4.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 16:43:53 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml Mon Apr 20 15:54:19 2020 +0200
4.3 @@ -1,18 +1,17 @@
4.4 -(* Title: BaseDefinitions/celem-5.sml
4.5 +(* Title: BaseDefinitions/problem-def.sml
4.6 Author: Walther Neuper
4.7 (c) due to copyright terms
4.8
4.9 - *)
4.10 +Will be enhanced by Problem later.
4.11 +*)
4.12 signature CALCELEMENT_5 =
4.13 -(*/------- to Celem5 -------\*)
4.14 -(*\------- to Celem5 -------/*)
4.15 sig
4.16 -(*/------- to Celem5 -------\*)
4.17 type pbt
4.18 type ptyps
4.19 val pbts2str: pbt list -> string
4.20 val e_Ptyp: pbt Store.ptyp
4.21 -(*\------- to Celem5 -------/*)
4.22 +(*vvv check_unique*)
4.23 + val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit
4.24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.25 val e_pbt: pbt
4.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.27 @@ -27,7 +26,7 @@
4.28
4.29 (*/------- to Celem5 -------\*)
4.30 type pbt =
4.31 - {guh : Spec.guh, (* unique within this isac-knowledge *)
4.32 + {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
4.33 mathauthors : string list, (* copyright *)
4.34 init : Spec.pblID, (* to start refinement with *)
4.35 thy : theory, (* which allows to compile that pbt
4.36 @@ -60,4 +59,7 @@
4.37 type ptyps = (pbt Store.ptyp) list
4.38 (*\------- to Celem5 -------/*)
4.39
4.40 +val check_pblguh_unique =
4.41 + Check_Unique.messsage (Check_Unique.collect (#guh : pbt -> Check_Unique.guh));
4.42 +
4.43 (**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 16:43:53 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/celem-6.sml Mon Apr 20 15:54:19 2020 +0200
5.3 @@ -1,18 +1,17 @@
5.4 -(* Title: BaseDefinitions/celem-6.sml
5.5 +(* Title: BaseDefinitions/method-def.sml
5.6 Author: Walther Neuper
5.7 (c) due to copyright terms
5.8
5.9 - *)
5.10 +Will be enhanced by Method later.
5.11 +*)
5.12 signature CALCELEMENT_6 =
5.13 -(*/------- to Celem6 -------\*)
5.14 -(*\------- to Celem6 -------/*)
5.15 sig
5.16 -(*/------- to Celem6 -------\*)
5.17 type met
5.18 val e_met: met
5.19 type mets
5.20 val e_Mets: met Store.ptyp
5.21 -(*\------- to Celem6 -------/*)
5.22 +(*vvv check_unique*)
5.23 + val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit
5.24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.25 (*NONE*)
5.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.27 @@ -28,7 +27,7 @@
5.28 (*/------- to Celem6 -------\*)
5.29 (* data for methods stored in 'methods'-database*)
5.30 type met =
5.31 - {guh : Spec.guh, (* unique within this isac-knowledge *)
5.32 + {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
5.33 mathauthors: string list, (* copyright *)
5.34 init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
5.35 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
5.36 @@ -59,4 +58,7 @@
5.37 type mets = (met Store.ptyp) list;
5.38 (*\------- to Celem6 -------/*)
5.39
5.40 +val check_metguh_unique =
5.41 + Check_Unique.messsage (Check_Unique.collect (#guh: met -> Check_Unique.guh));
5.42 +
5.43 (**)end(**)
6.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 16:43:53 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Mon Apr 20 15:54:19 2020 +0200
6.3 @@ -10,25 +10,25 @@
6.4 (*/------- to Celem8 -------\*)
6.5 type authors
6.6 datatype thydata
6.7 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Spec.guh, mathauthors: authors}
6.8 - | Hord of {coursedesign: authors, guh: Spec.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
6.9 - | Hrls of {coursedesign: authors, guh: Spec.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
6.10 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Spec.guh, mathauthors: authors, thm: thm}
6.11 - | Html of {coursedesign: authors, guh: Spec.guh, html: string, mathauthors: authors}
6.12 + = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors}
6.13 + | Hord of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
6.14 + | Hrls of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
6.15 + | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.guh, mathauthors: authors, thm: thm}
6.16 + | Html of {coursedesign: authors, guh: Check_Unique.guh, html: string, mathauthors: authors}
6.17 type theID
6.18 val theID2str: string list -> string
6.19 val the2str: thydata -> string
6.20 val thes2str: thydata list -> string
6.21 val theID2thyID: theID -> ThyC.id
6.22
6.23 - val part2guh: theID -> Spec.guh
6.24 - val thy2guh: theID -> Spec.guh
6.25 - val thypart2guh: theID -> Spec.guh
6.26 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Spec.guh
6.27 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Spec.guh
6.28 - val cal2guh: string * ThyC.id -> string -> Spec.guh
6.29 - val ord2guh: string * ThyC.id -> string -> Spec.guh
6.30 - val theID2guh: theID -> Spec.guh
6.31 + val part2guh: theID -> Check_Unique.guh
6.32 + val thy2guh: theID -> Check_Unique.guh
6.33 + val thypart2guh: theID -> Check_Unique.guh
6.34 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh
6.35 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh
6.36 + val cal2guh: string * ThyC.id -> string -> Check_Unique.guh
6.37 + val ord2guh: string * ThyC.id -> string -> Check_Unique.guh
6.38 + val theID2guh: theID -> Check_Unique.guh
6.39
6.40 val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
6.41 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
6.42 @@ -56,12 +56,12 @@
6.43 (* datatype for collecting thydata for hierarchy *)
6.44 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
6.45 datatype thydata =
6.46 - Html of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, html: string}
6.47 -| Hthm of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
6.48 + Html of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, html: string}
6.49 +| Hthm of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
6.50 thm: thm} (* here no sym_thm, thus no thmID required *)
6.51 -| Hrls of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
6.52 -| Hcal of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
6.53 -| Hord of {guh: Spec.guh, coursedesign: authors, mathauthors: authors,
6.54 +| Hrls of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
6.55 +| Hcal of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
6.56 +| Hord of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors,
6.57 ord: (UnparseC.subst -> (term * term) -> bool)};
6.58 fun the2str (Html {guh, ...}) = guh
6.59 | the2str (Hthm {guh, ...}) = guh
6.60 @@ -86,7 +86,7 @@
6.61 type thehier = (thydata Store.ptyp) list;
6.62 (* required to determine sequence of main nodes of thehier in Know_Store.thy *)
6.63 fun part2guh [str] = (case str of
6.64 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Spec.guh
6.65 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.guh
6.66 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
6.67 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
6.68 | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
6.69 @@ -100,7 +100,7 @@
6.70 | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
6.71
6.72 fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
6.73 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Spec.guh
6.74 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.guh
6.75 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
6.76 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
6.77 | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
6.78 @@ -110,28 +110,28 @@
6.79 (* convert the data got via contextToThy to a globally unique handle.
6.80 there is another way to get the guh: get out of the 'theID' in the hierarchy *)
6.81 fun thm2guh (isa, thyID) thmID = case isa of
6.82 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Spec.guh
6.83 + "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.guh
6.84 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
6.85 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
6.86 | _ => raise ERROR
6.87 ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
6.88
6.89 fun rls2guh (isa, thyID) rls' = case isa of
6.90 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Spec.guh
6.91 + "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.guh
6.92 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
6.93 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
6.94 | _ => raise ERROR
6.95 ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
6.96
6.97 fun cal2guh (isa, thyID) calID = case isa of
6.98 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Spec.guh
6.99 + "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.guh
6.100 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
6.101 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
6.102 | _ => raise ERROR
6.103 ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
6.104
6.105 fun ord2guh (isa, thyID) rew_ord' = case isa of
6.106 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Spec.guh
6.107 + "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.guh
6.108 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
6.109 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
6.110 | _ => raise ERROR
7.1 --- a/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 16:43:53 2020 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,63 +0,0 @@
7.4 -(* Title: BaseDefinitions/celem-91.sml
7.5 - Author: Walther Neuper
7.6 - (c) due to copyright terms
7.7 -
7.8 - *)
7.9 -signature CALCELEMENT_91 =
7.10 -(*/------- to Celem91 -------\*)
7.11 -(*\------- to Celem91 -------/*)
7.12 -sig
7.13 -(*/------- to Celem91 -------\*)
7.14 - val check_guhs_unique: bool Unsynchronized.ref
7.15 - val check_pblguh_unique: Spec.guh -> Celem5.pbt Store.ptyp list -> unit
7.16 - val check_metguh_unique: Spec.guh -> Celem6.met Store.ptyp list -> unit
7.17 - val coll_pblguhs: Celem5.pbt Store.ptyp list -> Spec.guh list
7.18 - val coll_metguhs: Celem6.met Store.ptyp list -> Spec.guh list
7.19 -(*\------- to Celem91 -------/*)
7.20 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.21 - (*NONE*)
7.22 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.23 - (*NONE*)
7.24 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.25 -end
7.26 -
7.27 -(**)
7.28 -structure Celem91(**): CALCELEMENT_91(**) =
7.29 -struct
7.30 -(**)
7.31 -
7.32 -(*/------- to Celem91 -------\*)
7.33 -(* switch for checking guhs unique before storing a pbl or met;
7.34 - set true at startup (done at begin of ROOT.ML)
7.35 - set false for editing IsacKnowledge (done at end of ROOT.ML) *)
7.36 -val check_guhs_unique = Unsynchronized.ref true;
7.37 -
7.38 -fun coll_pblguhs pbls =
7.39 - let
7.40 - fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Spec.guh) n] @ (nodes coll ns)
7.41 - | node _ _ = raise ERROR "coll_pblguhs - node"
7.42 - and nodes coll [] = coll
7.43 - | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
7.44 - in nodes [] pbls end;
7.45 -fun check_pblguh_unique guh pbls =
7.46 - if member op = (coll_pblguhs pbls) guh
7.47 - then error ("check_guh_unique failed with \""^ guh ^"\";\n"^
7.48 - "use \"sort_pblguhs()\" for a list of guhs;\n"^
7.49 - "consider setting \"check_guhs_unique := false\"")
7.50 - else ();
7.51 -fun coll_metguhs mets =
7.52 - let
7.53 - fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Spec.guh) n] @ (nodes coll ns)
7.54 - | node _ _ = raise ERROR "coll_pblguhs - node"
7.55 - and nodes coll [] = coll
7.56 - | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
7.57 - in nodes [] mets end;
7.58 -fun check_metguh_unique (guh: Spec.guh) (mets: (Celem6.met Store.ptyp) list) =
7.59 - if member op = (coll_metguhs mets) guh
7.60 - then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
7.61 - (*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
7.62 - "consider setting \"check_guhs_unique := false\"")
7.63 - else ();
7.64 -(*\------- to Celem91 -------/*)
7.65 -
7.66 -(**)end(**)
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 15:54:19 2020 +0200
8.3 @@ -0,0 +1,55 @@
8.4 +(* Title: BaseDefinitions/celem-91.sml
8.5 + Author: Walther Neuper
8.6 + (c) due to copyright terms
8.7 +
8.8 +Check entries to Know_Store unique.
8.9 +This is legacy code; check runs on #guh.
8.10 +*)
8.11 +signature CHECK_UNIQUE =
8.12 +sig
8.13 +(*type switch *)
8.14 + type guh
8.15 +(*val on *)
8.16 + val check_guhs_unique: bool Unsynchronized.ref
8.17 +(*val collect *)
8.18 + val collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
8.19 + val messsage: ('a -> guh list) -> guh -> 'a -> unit;
8.20 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.21 + (*NONE*)
8.22 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.23 + (*NONE*)
8.24 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.25 +end
8.26 +
8.27 +(**)
8.28 +structure Check_Unique(**): CHECK_UNIQUE(**) =
8.29 +struct
8.30 +(**)
8.31 +
8.32 +(*
8.33 + the last remaining code from Klaus Schmaranz's Dinopolis Project:
8.34 + guh stands for "globally unique handle" -- over all of the internet.
8.35 +*)
8.36 +type guh = string;
8.37 +
8.38 +(* switch for checking guhs unique before storing a pbl or met;
8.39 + set true at startup (done at begin of ROOT.ML)
8.40 + set false for editing Isac_Knowledge (done at end of ROOT.ML) *)
8.41 +val check_guhs_unique = Unsynchronized.ref true;
8.42 +
8.43 +fun collect select_guh pbls =
8.44 + let
8.45 + fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
8.46 + | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
8.47 + and nodes coll [] = coll
8.48 + | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
8.49 + in nodes [] pbls end;
8.50 +
8.51 +fun messsage select guh store =
8.52 + if member op = (select store) guh
8.53 + then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
8.54 + "use \"sort_guhs()\" for a list of guhs;\n" ^
8.55 + "consider setting \"Check_Unique.on := false\"")
8.56 + else ();
8.57 +
8.58 +(**)end(**)
9.1 --- a/src/Tools/isac/BaseDefinitions/specification.sml Sun Apr 19 16:43:53 2020 +0200
9.2 +++ b/src/Tools/isac/BaseDefinitions/specification.sml Mon Apr 20 15:54:19 2020 +0200
9.3 @@ -1,4 +1,4 @@
9.4 -(* Title: BaseDefinitions/celem-3.sml
9.5 +(* Title: BaseDefinitions/specification.sml
9.6 Author: Walther Neuper
9.7 (c) due to copyright terms
9.8
9.9 @@ -6,7 +6,6 @@
9.10 *)
9.11 signature SPECIFICATION =
9.12 sig
9.13 - type guh
9.14 type metID
9.15 type pblID
9.16 type spec
9.17 @@ -28,12 +27,6 @@
9.18 struct
9.19 (**)
9.20
9.21 -(*
9.22 -The last remainder from Klaus Schmaranz' Dinopolis Project, which used "globally unique handles"
9.23 -abbreviated "guh". These are used for files names; can be dropped with switch to Isabelle/PIDE.
9.24 -*)
9.25 -type guh = string;
9.26 -
9.27 (*/------- to Spec -------\*)
9.28 (*the key into the hierarchy ob problems*)
9.29 type pblID = string list; (* domID :: ...*)
10.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Sun Apr 19 16:43:53 2020 +0200
10.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Mon Apr 20 15:54:19 2020 +0200
10.3 @@ -6,12 +6,18 @@
10.4 *)
10.5 signature STORE_TREE =
10.6 sig
10.7 + type key
10.8 datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
10.9 +(*vvv merge *)
10.10 val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
10.11 - val insrt: (*pblID*)string list -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
10.12 - val get_py: 'a ptyp list -> (*pblID*)string list -> string list -> 'a
10.13 - val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
10.14 - val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> (*pblID*)string list -> string list -> 'b
10.15 +(*vvv insert *)
10.16 + val insrt: key -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
10.17 +(*vvv get *)
10.18 + val get_py: 'a ptyp list -> key -> (*rev*)key -> 'a
10.19 +(*vvv update *)
10.20 + val update_ptyps: key -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
10.21 +(*vvv apply *)
10.22 + val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> key -> (*rev*)key -> 'b
10.23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.24 (*NONE*)
10.25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.26 @@ -24,6 +30,7 @@
10.27 struct
10.28 (**)
10.29
10.30 +type key = string list; (*will become pblID, methID, theID*)
10.31 (*/------- to Store -------\*)
10.32 (* A tree for storing data defined in different theories
10.33 for access from the Interpreter and from dialogue authoring
11.1 --- a/src/Tools/isac/Build_Isac.thy Sun Apr 19 16:43:53 2020 +0200
11.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Apr 20 15:54:19 2020 +0200
11.3 @@ -134,7 +134,7 @@
11.4 ML \<open>@{thm last_thmI}\<close>
11.5 ML \<open>@{thm Querkraft_Belastung}\<close>
11.6
11.7 -ML \<open>Celem.check_guhs_unique := false;\<close>
11.8 +ML \<open>Check_Unique.check_guhs_unique := false;\<close>
11.9 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
11.10 ML \<open>@{theory "Isac_Knowledge"}\<close>
11.11 ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
12.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Apr 19 16:43:53 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Apr 20 15:54:19 2020 +0200
12.3 @@ -145,7 +145,7 @@
12.4 decomposedFunction :: "real => una"
12.5
12.6 ML \<open>
12.7 -Celem.check_guhs_unique := false; (*WN120307 REMOVE after editing*)
12.8 +Check_Unique.check_guhs_unique := false; (*WN120307 REMOVE after editing*)
12.9 \<close>
12.10 setup \<open>KEStore_Elems.add_pbts
12.11 [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] Celem.e_pblID
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 15:54:19 2020 +0200
13.3 @@ -0,0 +1,64 @@
13.4 +(* Title: "BaseDefinitions/check-unique.sml"
13.5 + Author: Walther Neuper
13.6 + (c) due to copyright terms
13.7 +*)
13.8 +
13.9 +"-----------------------------------------------------------------------------------------------";
13.10 +"table of contents -----------------------------------------------------------------------------";
13.11 +"-----------------------------------------------------------------------------------------------";
13.12 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
13.13 +"-----------------------------------------------------------------------------------------------";
13.14 +"-----------------------------------------------------------------------------------------------";
13.15 +"-----------------------------------------------------------------------------------------------";
13.16 +
13.17 +
13.18 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
13.19 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
13.20 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
13.21 +(*------- auxiliary format for fn*)
13.22 +fun pbl_select_guh pbt =
13.23 + let
13.24 + val {guh, ...} = (**)(pbt: pbt)(** )(pbt: met)( **)
13.25 + in guh end;
13.26 +pbl_select_guh: pbt -> guh;(**)
13.27 +
13.28 +fun met_select_guh pbt =
13.29 + let
13.30 + val {guh, ...} = (pbt: met)
13.31 + in guh end;
13.32 +met_select_guh: met -> guh;(**)
13.33 +
13.34 +(*------- hint: build higher order functions be replacing the selector by a variable argument *)
13.35 +(* collect*)
13.36 +fun collect select_guh pbls =
13.37 + let
13.38 + fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
13.39 + | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
13.40 + and nodes coll [] = coll
13.41 + | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
13.42 + in nodes [] pbls end;
13.43 +
13.44 +collect: ('a -> 'b) -> 'a ptyp list -> 'b list;
13.45 +collect pbl_select_guh: pbt ptyp list -> guh list;
13.46 +collect met_select_guh: met ptyp list -> guh list;
13.47 +
13.48 +fun message select store guh =
13.49 + if member op = (select store) guh
13.50 + then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
13.51 + "use \"sort_guhs()\" for a list of guhs;\n" ^
13.52 + "consider setting \"Check_Unique.on := false\"")
13.53 + else ();
13.54 +
13.55 + message: ('a -> guh list ) -> 'a -> guh -> unit;
13.56 +(message (collect pbl_select_guh)): pbt ptyp list -> guh -> unit;
13.57 +(message (collect met_select_guh)): met ptyp list -> guh -> unit;
13.58 +
13.59 +(Check_Unique.collect (#guh : Celem5.pbt -> Check_Unique.guh)): pbt ptyp list -> guh list;
13.60 +(Check_Unique.collect (#guh : Celem6.met -> Check_Unique.guh)): met ptyp list -> guh list;
13.61 +
13.62 +val check_pblguh_unique = messsage (Check_Unique.collect (#guh : Celem5.pbt -> Check_Unique.guh));
13.63 +check_pblguh_unique: pbt ptyp list -> guh -> unit
13.64 +;
13.65 +val check_metguh_unique = messsage (Check_Unique.collect (#guh : Celem6.met -> Check_Unique.guh));
13.66 +check_metguh_unique: met ptyp list -> guh -> unit
13.67 +;
13.68 \ No newline at end of file
14.1 --- a/test/Tools/isac/Test_Isac.thy Sun Apr 19 16:43:53 2020 +0200
14.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Apr 20 15:54:19 2020 +0200
14.3 @@ -123,12 +123,12 @@
14.4 open ContextC; transfer_asms_from_to;
14.5 open Tactic; (* NONE *)
14.6 open Model; (* NONE *)
14.7 - open Rewrite; mk_thm;
14.8 + open Rewrite;
14.9 open Eval; get_pair;
14.10 open TermC; atomt;
14.11 open Celem; e_pbt;
14.12 open Rule;
14.13 - open Rule_Set
14.14 + open Rule_Set; Sequence;
14.15 open Exec_Def
14.16 open ThyC
14.17 open ThmC_Def
14.18 @@ -187,6 +187,7 @@
14.19 ML_file "BaseDefinitions/thmC-def.sml"
14.20 ML_file "BaseDefinitions/error-fill-def.sml"
14.21 ML_file "BaseDefinitions/rule-set.sml"
14.22 + ML_file "BaseDefinitions/check-unique.sml"
14.23 ML_file "BaseDefinitions/calcelems.sml"
14.24 ML_file "BaseDefinitions/termC.sml"
14.25 ML_file "BaseDefinitions/contextC.sml"
14.26 @@ -248,7 +249,7 @@
14.27 ML_file "Interpret/istate.sml"
14.28 ML_file "Interpret/sub-problem.sml"
14.29 ML_file "Interpret/rewtools.sml"
14.30 - ML_file "Interpret/error-pattern.sml"
14.31 + ML_file "Interpret/error-fill-pattern.sml"
14.32 ML_file "Interpret/li-tool.sml"
14.33 ML_file "Interpret/lucas-interpreter.sml"
14.34 ML_file "Interpret/step-solve.sml"
15.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Apr 19 16:43:53 2020 +0200
15.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Apr 20 15:54:19 2020 +0200
15.3 @@ -152,8 +152,8 @@
15.4 \<close> ML \<open>
15.5 \<close> ML \<open>
15.6 \<close> ML \<open>
15.7 -\<close> ML \<open>`
15.8 -\<close> ML \<open>`
15.9 +\<close> ML \<open>
15.10 +\<close> ML \<open>
15.11 \<close> ML \<open>
15.12 \<close> ML \<open>
15.13 \<close> ML \<open>
15.14 @@ -187,6 +187,7 @@
15.15 ML_file "BaseDefinitions/thmC-def.sml"
15.16 ML_file "BaseDefinitions/error-fill-def.sml"
15.17 ML_file "BaseDefinitions/rule-set.sml"
15.18 + ML_file "BaseDefinitions/check-unique.sml"
15.19 ML_file "BaseDefinitions/calcelems.sml"
15.20 ML_file "BaseDefinitions/termC.sml"
15.21 ML_file "BaseDefinitions/contextC.sml"
16.1 --- a/test/Tools/isac/Test_Some.thy Sun Apr 19 16:43:53 2020 +0200
16.2 +++ b/test/Tools/isac/Test_Some.thy Mon Apr 20 15:54:19 2020 +0200
16.3 @@ -96,9 +96,7 @@
16.4 section \<open>===================================================================================\<close>
16.5 ML \<open>
16.6 \<close> ML \<open>
16.7 -val (Const ("HOL.Not", _) $ xxx) = @{term "Not (a = b)"}
16.8 \<close> ML \<open>
16.9 -@{thm all_left}
16.10 \<close> ML \<open>
16.11 \<close>
16.12