# HG changeset patch # User Walther Neuper # Date 1587459184 -7200 # Node ID 454fad8ab67a7aeaf23e980fa4a0f9141b5ba06d # Parent b9e10434530c909d46ed8ed3298528def4d718ea derive Method.T from Meth_Def.T, drop funs and types used by Know_Store diff -r b9e10434530c -r 454fad8ab67a src/Tools/isac/BaseDefinitions/Know_Store.thy --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 10:13:30 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 10:53:04 2020 +0200 @@ -67,8 +67,8 @@ val add_cas: CAS_Def.cas_elem list -> theory -> theory val get_ptyps: theory -> Probl_Def.store val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory - val get_mets: theory -> Meth_Def.mets - val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory + val get_mets: theory -> Meth_Def.store + val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *) val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory @@ -122,15 +122,15 @@ in Data.map (fold add_pbt pbts) thy end; structure Data = Theory_Data ( - type T = Meth_Def.mets; - val empty = [Meth_Def.e_Mets]; + type T = Meth_Def.store; + val empty = [Meth_Def.empty_store]; val extend = I; val merge = Store.merge_ptyps; ); val get_mets = Data.get; fun add_mets mets thy = let fun add_met (met as {guh,...}, metID) = - (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_metguh_unique guh (Data.get thy) else (); + (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else (); Store.insrt metID met metID); in Data.map (fold add_met mets) thy end; @@ -250,10 +250,10 @@ :: sort_kestore_ptyp' ordfun ps'); val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; -fun metguh2str ({guh,...} : Meth_Def.met) = guh : string; -fun check_kestore_met (mp: Meth_Def.met Store.ptyp) = +fun metguh2str ({guh,...} : Meth_Def.T) = guh : string; +fun check_kestore_met (mp: Meth_Def.T Store.ptyp) = check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; -fun met_ord ({guh = guh'1, ...} : Meth_Def.met, {guh = guh'2, ...} : Meth_Def.met) = string_ord (guh'1, guh'2); +fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2); val sort_kestore_met = sort_kestore_ptyp' met_ord; fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes diff -r b9e10434530c -r 454fad8ab67a src/Tools/isac/BaseDefinitions/calcelems.sml --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 10:13:30 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 10:53:04 2020 +0200 @@ -71,8 +71,8 @@ (*\------- to Celem8 -------/*) (*/------- to Celem6 -------\*) - type met = Meth_Def.met - type mets = Meth_Def.mets + type met = Meth_Def.T + type mets = Meth_Def.store val e_Mets: met Store.ptyp (*\------- to Celem6 -------/*) @@ -288,9 +288,9 @@ (*\------- to Celem5 -------/*) (*/------- to Celem6 -------\*) -type met = Meth_Def.met; -val e_met = Meth_Def.e_met; -val e_Mets = Meth_Def.e_Mets; +type met = Meth_Def.T; +val e_met = Meth_Def.empty; +val e_Mets = Meth_Def.empty_store; type mets = (met Store.ptyp) list; (*\------- to Celem6 -------/*) @@ -298,8 +298,8 @@ val check_guhs_unique = Check_Unique.check_guhs_unique; val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh); val check_pblguh_unique = Probl_Def.check_unique; -val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh); -val check_metguh_unique = Meth_Def.check_metguh_unique; +val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh); +val check_metguh_unique = Meth_Def.check_unique; (*\------- to Celem91 -------/*) (*/------- to Celem8 -------\*) diff -r b9e10434530c -r 454fad8ab67a src/Tools/isac/BaseDefinitions/method-def.sml --- a/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 21 10:13:30 2020 +0200 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 21 10:53:04 2020 +0200 @@ -6,12 +6,16 @@ *) signature METHOD_DEFINITION = sig - type met - val e_met: met - type mets - val e_Mets: met Store.ptyp -(*vvv check_unique*) - val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit + type T +(*type met*) + val empty: T +(*val e_met: T*) + type store +(*type mets*) + val empty_store: T Store.ptyp +(*val e_Mets: T Store.ptyp*) + val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit +(*val check_metguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*) (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) @@ -24,9 +28,8 @@ struct (**) -(*/------- to Celem6 -------\*) (* data for methods stored in 'methods'-database*) -type met = +type T = {guh : Check_Unique.guh, (* unique within this isac-knowledge *) mathauthors: string list, (* copyright *) init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *) @@ -50,15 +53,15 @@ see ME/calchead.sml 'fun is_copy_named'. *) pre : term list (* preconditions in where *) }; -val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord', +val empty = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord', erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog}; -val e_Mets = Store.Ptyp ("e_metID", [e_met],[]); +val empty_store = Store.Ptyp ("e_metID", [empty],[]); -type mets = (met Store.ptyp) list; +type store = (T Store.ptyp) list; (*\------- to Celem6 -------/*) -val check_metguh_unique = - Check_Unique.message (Check_Unique.collect (#guh: met -> Check_Unique.guh)); +val check_unique = + Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.guh)); (**)end(**) diff -r b9e10434530c -r 454fad8ab67a src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 10:13:30 2020 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 10:53:04 2020 +0200 @@ -66,7 +66,7 @@ in nds j [0] h : Celem.xml end; fun hierarchy_met h = let val j = indentation - fun nd i p (Store.Ptyp (id,[n as {guh,...} : Celem.met],ns)) = + fun nd i p (Store.Ptyp (id,[n as {guh,...} : Method.T],ns)) = let val p' = Pos.lev_on p in (indt i) ^ "\n" ^ (indt (i+j)) ^ " " ^ id ^ " \n" ^ @@ -192,7 +192,7 @@ requires elements (rls, calc, ...) to be reorganized.*) (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*) fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc, - crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) = + crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) = let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*) val crls' = (#id o Rule_Set.rep) crls val erls' = (#id o Rule_Set.rep) erls @@ -230,7 +230,7 @@ (*.format a method in xml for presentation on the method browser; old version with 'dead' strings for rls, calc, ....*) fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc, - crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) = + crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) = "\n" ^ indt i ^ " " ^ guh ^ " \n" ^ id2xml i id ^ @@ -291,11 +291,11 @@ *) fun update_metdata - ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: Celem.met) + ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: Method.T) errpats' = {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls, srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc, - ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: Celem.met + ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: Method.T (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *) fun update_metpair thy metID errpats = let diff -r b9e10434530c -r 454fad8ab67a src/Tools/isac/MathEngBasic/method.sml --- a/src/Tools/isac/MathEngBasic/method.sml Tue Apr 21 10:13:30 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Apr 21 10:53:04 2020 +0200 @@ -5,9 +5,12 @@ signature METHOD = sig + type T = Meth_Def.T (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) + (*NONE*) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) + (*NONE*) ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end @@ -16,5 +19,6 @@ struct (**) +type T = Meth_Def.T; (**)end(**) diff -r b9e10434530c -r 454fad8ab67a src/Tools/isac/Specify/ptyps.sml --- a/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 10:13:30 2020 +0200 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 10:53:04 2020 +0200 @@ -26,8 +26,8 @@ val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *) val get_pbt : Celem.pblID -> Problem.T - val get_met : Celem.metID -> Celem.met (* for generate.sml *) - val get_met' : theory -> Celem.metID -> Celem.met (* for pbl-met-hierarchy.sml *) + val get_met : Celem.metID -> Method.T (* for generate.sml *) + val get_met' : theory -> Celem.metID -> Method.T (* for pbl-met-hierarchy.sml *) val get_the : Celem.theID -> Celem.thydata (* for inform.sml *) type pblRD = string list (* for pbl-met-hierarchy.sml *) @@ -48,7 +48,7 @@ string list * (string * string list) list * {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm -> - Celem.met * Celem.metID + Method.T * Celem.metID (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) val show_ptyps : unit -> unit val show_mets : unit -> unit @@ -110,7 +110,7 @@ open Model -fun fun_id_of ({scr = prog, ...} : Celem.met) = +fun fun_id_of ({scr = prog, ...} : Method.T) = case prog of Rule.Empty_Prog => NONE | Rule.Prog t =>