1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 10:13:30 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 10:53:04 2020 +0200
1.3 @@ -67,8 +67,8 @@
1.4 val add_cas: CAS_Def.cas_elem list -> theory -> theory
1.5 val get_ptyps: theory -> Probl_Def.store
1.6 val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
1.7 - val get_mets: theory -> Meth_Def.mets
1.8 - val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
1.9 + val get_mets: theory -> Meth_Def.store
1.10 + val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
1.11 val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
1.12 val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.13 val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.14 @@ -122,15 +122,15 @@
1.15 in Data.map (fold add_pbt pbts) thy end;
1.16
1.17 structure Data = Theory_Data (
1.18 - type T = Meth_Def.mets;
1.19 - val empty = [Meth_Def.e_Mets];
1.20 + type T = Meth_Def.store;
1.21 + val empty = [Meth_Def.empty_store];
1.22 val extend = I;
1.23 val merge = Store.merge_ptyps;
1.24 );
1.25 val get_mets = Data.get;
1.26 fun add_mets mets thy = let
1.27 fun add_met (met as {guh,...}, metID) =
1.28 - (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_metguh_unique guh (Data.get thy) else ();
1.29 + (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
1.30 Store.insrt metID met metID);
1.31 in Data.map (fold add_met mets) thy end;
1.32
1.33 @@ -250,10 +250,10 @@
1.34 :: sort_kestore_ptyp' ordfun ps');
1.35 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.36
1.37 -fun metguh2str ({guh,...} : Meth_Def.met) = guh : string;
1.38 -fun check_kestore_met (mp: Meth_Def.met Store.ptyp) =
1.39 +fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
1.40 +fun check_kestore_met (mp: Meth_Def.T Store.ptyp) =
1.41 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.42 -fun met_ord ({guh = guh'1, ...} : Meth_Def.met, {guh = guh'2, ...} : Meth_Def.met) = string_ord (guh'1, guh'2);
1.43 +fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
1.44 val sort_kestore_met = sort_kestore_ptyp' met_ord;
1.45
1.46 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 10:13:30 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 10:53:04 2020 +0200
2.3 @@ -71,8 +71,8 @@
2.4 (*\------- to Celem8 -------/*)
2.5
2.6 (*/------- to Celem6 -------\*)
2.7 - type met = Meth_Def.met
2.8 - type mets = Meth_Def.mets
2.9 + type met = Meth_Def.T
2.10 + type mets = Meth_Def.store
2.11 val e_Mets: met Store.ptyp
2.12 (*\------- to Celem6 -------/*)
2.13
2.14 @@ -288,9 +288,9 @@
2.15 (*\------- to Celem5 -------/*)
2.16
2.17 (*/------- to Celem6 -------\*)
2.18 -type met = Meth_Def.met;
2.19 -val e_met = Meth_Def.e_met;
2.20 -val e_Mets = Meth_Def.e_Mets;
2.21 +type met = Meth_Def.T;
2.22 +val e_met = Meth_Def.empty;
2.23 +val e_Mets = Meth_Def.empty_store;
2.24 type mets = (met Store.ptyp) list;
2.25 (*\------- to Celem6 -------/*)
2.26
2.27 @@ -298,8 +298,8 @@
2.28 val check_guhs_unique = Check_Unique.check_guhs_unique;
2.29 val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh);
2.30 val check_pblguh_unique = Probl_Def.check_unique;
2.31 -val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh);
2.32 -val check_metguh_unique = Meth_Def.check_metguh_unique;
2.33 +val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh);
2.34 +val check_metguh_unique = Meth_Def.check_unique;
2.35 (*\------- to Celem91 -------/*)
2.36
2.37 (*/------- to Celem8 -------\*)
3.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 21 10:13:30 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 21 10:53:04 2020 +0200
3.3 @@ -6,12 +6,16 @@
3.4 *)
3.5 signature METHOD_DEFINITION =
3.6 sig
3.7 - type met
3.8 - val e_met: met
3.9 - type mets
3.10 - val e_Mets: met Store.ptyp
3.11 -(*vvv check_unique*)
3.12 - val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit
3.13 + type T
3.14 +(*type met*)
3.15 + val empty: T
3.16 +(*val e_met: T*)
3.17 + type store
3.18 +(*type mets*)
3.19 + val empty_store: T Store.ptyp
3.20 +(*val e_Mets: T Store.ptyp*)
3.21 + val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit
3.22 +(*val check_metguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*)
3.23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.24 (*NONE*)
3.25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.26 @@ -24,9 +28,8 @@
3.27 struct
3.28 (**)
3.29
3.30 -(*/------- to Celem6 -------\*)
3.31 (* data for methods stored in 'methods'-database*)
3.32 -type met =
3.33 +type T =
3.34 {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
3.35 mathauthors: string list, (* copyright *)
3.36 init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
3.37 @@ -50,15 +53,15 @@
3.38 see ME/calchead.sml 'fun is_copy_named'. *)
3.39 pre : term list (* preconditions in where *)
3.40 };
3.41 -val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
3.42 +val empty = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
3.43 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
3.44 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
3.45 -val e_Mets = Store.Ptyp ("e_metID", [e_met],[]);
3.46 +val empty_store = Store.Ptyp ("e_metID", [empty],[]);
3.47
3.48 -type mets = (met Store.ptyp) list;
3.49 +type store = (T Store.ptyp) list;
3.50 (*\------- to Celem6 -------/*)
3.51
3.52 -val check_metguh_unique =
3.53 - Check_Unique.message (Check_Unique.collect (#guh: met -> Check_Unique.guh));
3.54 +val check_unique =
3.55 + Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.guh));
3.56
3.57 (**)end(**)
4.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 10:13:30 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 10:53:04 2020 +0200
4.3 @@ -66,7 +66,7 @@
4.4 in nds j [0] h : Celem.xml end;
4.5 fun hierarchy_met h =
4.6 let val j = indentation
4.7 - fun nd i p (Store.Ptyp (id,[n as {guh,...} : Celem.met],ns)) =
4.8 + fun nd i p (Store.Ptyp (id,[n as {guh,...} : Method.T],ns)) =
4.9 let val p' = Pos.lev_on p
4.10 in (indt i) ^ "<NODE>\n" ^
4.11 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
4.12 @@ -192,7 +192,7 @@
4.13 requires elements (rls, calc, ...) to be reorganized.*)
4.14 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
4.15 fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
4.16 - crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) =
4.17 + crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) =
4.18 let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*)
4.19 val crls' = (#id o Rule_Set.rep) crls
4.20 val erls' = (#id o Rule_Set.rep) erls
4.21 @@ -230,7 +230,7 @@
4.22 (*.format a method in xml for presentation on the method browser;
4.23 old version with 'dead' strings for rls, calc, ....*)
4.24 fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
4.25 - crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) =
4.26 + crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) =
4.27 "<NODECONTENT>\n" ^
4.28 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
4.29 id2xml i id ^
4.30 @@ -291,11 +291,11 @@
4.31 *)
4.32
4.33 fun update_metdata
4.34 - ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: Celem.met)
4.35 + ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: Method.T)
4.36 errpats' =
4.37 {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls,
4.38 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc,
4.39 - ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: Celem.met
4.40 + ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: Method.T
4.41
4.42 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
4.43 fun update_metpair thy metID errpats = let
5.1 --- a/src/Tools/isac/MathEngBasic/method.sml Tue Apr 21 10:13:30 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Apr 21 10:53:04 2020 +0200
5.3 @@ -5,9 +5,12 @@
5.4
5.5 signature METHOD =
5.6 sig
5.7 + type T = Meth_Def.T
5.8
5.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.10 + (*NONE*)
5.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.12 + (*NONE*)
5.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.14 end
5.15
5.16 @@ -16,5 +19,6 @@
5.17 struct
5.18 (**)
5.19
5.20 +type T = Meth_Def.T;
5.21
5.22 (**)end(**)
6.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 10:13:30 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 10:53:04 2020 +0200
6.3 @@ -26,8 +26,8 @@
6.4 val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *)
6.5
6.6 val get_pbt : Celem.pblID -> Problem.T
6.7 - val get_met : Celem.metID -> Celem.met (* for generate.sml *)
6.8 - val get_met' : theory -> Celem.metID -> Celem.met (* for pbl-met-hierarchy.sml *)
6.9 + val get_met : Celem.metID -> Method.T (* for generate.sml *)
6.10 + val get_met' : theory -> Celem.metID -> Method.T (* for pbl-met-hierarchy.sml *)
6.11 val get_the : Celem.theID -> Celem.thydata (* for inform.sml *)
6.12
6.13 type pblRD = string list (* for pbl-met-hierarchy.sml *)
6.14 @@ -48,7 +48,7 @@
6.15 string list * (string * string list) list *
6.16 {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
6.17 rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
6.18 - Celem.met * Celem.metID
6.19 + Method.T * Celem.metID
6.20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.21 val show_ptyps : unit -> unit
6.22 val show_mets : unit -> unit
6.23 @@ -110,7 +110,7 @@
6.24
6.25 open Model
6.26
6.27 -fun fun_id_of ({scr = prog, ...} : Celem.met) =
6.28 +fun fun_id_of ({scr = prog, ...} : Method.T) =
6.29 case prog of
6.30 Rule.Empty_Prog => NONE
6.31 | Rule.Prog t =>