1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Feb 03 15:21:12 2021 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Feb 03 16:39:44 2021 +0100
1.3 @@ -1,7 +1,7 @@
1.4 (* Title: src/Tools/isac/Know_Store.thy
1.5 Author: Mathias Lehnfeld
1.6
1.7 -Calc work on Problem employing Method; both are collected in a respective Store;
1.8 +Calc work on Problem employing MethodC; both are collected in a respective Store;
1.9 The collections' structure is independent from the dependency graph of Isabelle's theories
1.10 in Knowledge.
1.11 Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
2.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Wed Feb 03 15:21:12 2021 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Wed Feb 03 16:39:44 2021 +0100
2.3 @@ -3,7 +3,7 @@
2.4 (c) due to copyright terms
2.5
2.6 Here is a minimum of code required for Know_Store.thy.
2.7 -For main code see structure Method.
2.8 +For main code see structure MethodC.
2.9 *)
2.10 signature METHOD_DEFINITION =
2.11 sig
2.12 @@ -49,7 +49,7 @@
2.13 nrls : Rule_Set.T, (* for rewriting by Tactic.Rewrite *)
2.14 errpats : Error_Pattern_Def.T list, (* error patterns expected in this method *)
2.15 calc : Rule_Def.calc list,(* ?DEL *)
2.16 - scr : Rule.program, (* filled in Method.prep_input *)
2.17 + scr : Rule.program, (* filled in MethodC.prep_input *)
2.18 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
2.19 ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate"
2.20 for constraints on identifiers see "O_Model.cpy_nam" *)
3.1 --- a/src/Tools/isac/BaseDefinitions/references-def.sml Wed Feb 03 15:21:12 2021 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/references-def.sml Wed Feb 03 16:39:44 2021 +0100
3.3 @@ -6,7 +6,7 @@
3.4 *)
3.5 signature REFERENCES_DEFINITION =
3.6 sig
3.7 - type id (* will be specialised to Problem.id, Method.id *)
3.8 + type id (* will be specialised to Problem.id, MethodC.id *)
3.9 val id_to_string: id -> string
3.10 val empty_probl_id: id
3.11 val empty_meth_id: id
3.12 @@ -37,7 +37,7 @@
3.13 type T = (* 3-dimensional universe of math knowledge: *)
3.14 ThyC.id * (* reference to a theory comprising definitions *)
3.15 id * (* will become Problem.id; a reference into a tree *)
3.16 - id; (* will become Method.id; a reference into a tree *)
3.17 + id; (* will become MethodC.id; a reference into a tree *)
3.18 fun to_string (dom, pbl, met) =
3.19 "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
3.20 val empty = (ThyC.id_empty, empty_probl_id, empty_meth_id);
4.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Wed Feb 03 15:21:12 2021 +0100
4.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Wed Feb 03 16:39:44 2021 +0100
4.3 @@ -2,7 +2,7 @@
4.4 Author: Walther Neuper
4.5 (c) due to copyright terms
4.6
4.7 -A tree for storing collections of Problem, Method and Thy_Write.
4.8 +A tree for storing collections of Problem, MethodC and Thy_Write.
4.9 *)
4.10 signature STORE_TREE =
4.11 sig
5.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Wed Feb 03 15:21:12 2021 +0100
5.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Wed Feb 03 16:39:44 2021 +0100
5.3 @@ -22,7 +22,7 @@
5.4 val tokenize_formalise: Position.T -> string -> Fdl_Lexer.T list * Fdl_Lexer.chars
5.5
5.6 type form_model = TermC.as_string list;
5.7 - type form_refs = (((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string
5.8 + type form_refs = (((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string
5.9 type form_model_refs =
5.10 (((((string * string) * form_model) * string) * form_refs) * string) * string
5.11
5.12 @@ -323,10 +323,10 @@
5.13 type form_model = TermC.as_string list;
5.14 type form_refs = (((((string * string) * string) * string list) * string) * string list) * string
5.15 type form_model_refs = ((((((string * string) * form_model) * string) *
5.16 - ((((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string)) *
5.17 + ((((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string)) *
5.18 string) * string)
5.19 type formalise = (((((string * string) * form_model) * string) *
5.20 - ((((((string * ThyC.id) * string) * Problem.id) * string) * Method.id) * string)) *
5.21 + ((((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string)) *
5.22 string) * string;
5.23
5.24 val parse_string = Fdl_Parser.group "string"
5.25 @@ -372,7 +372,7 @@
5.26 ","),
5.27 probl_id: Problem.id),
5.28 ","),
5.29 - meth_id: Method.id),
5.30 + meth_id: MethodC.id),
5.31 ")")),
5.32 ")"),
5.33 "]") = [(form_model, (thy_id, probl_id, meth_id))]
6.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Wed Feb 03 15:21:12 2021 +0100
6.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Wed Feb 03 16:39:44 2021 +0100
6.3 @@ -601,7 +601,7 @@
6.4 fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =
6.5 if inthy = thy andalso inpbl = pbl
6.6 then ((thy, pbl, met_id) : References.T, o_model)
6.7 - else ((inthy, inpbl, Method.id_empty), [])
6.8 + else ((inthy, inpbl, MethodC.id_empty), [])
6.9
6.10 fun prove_vc (*vc_name*)problem lthy =
6.11 let
7.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Feb 03 15:21:12 2021 +0100
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Feb 03 16:39:44 2021 +0100
7.3 @@ -52,7 +52,7 @@
7.4 val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
7.5 val resetCalcHead : calcID -> XML.tree
7.6 val setContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
7.7 - val setMethod : calcID -> Method.id -> XML.tree
7.8 + val setMethod : calcID -> MethodC.id -> XML.tree
7.9 val setNextTactic : calcID -> Tactic.input -> XML.tree
7.10 val setProblem : calcID -> Problem.id -> XML.tree
7.11 val setTheory : calcID -> ThyC.id -> XML.tree
7.12 @@ -316,7 +316,7 @@
7.13 (* set the UContext determined on a knowledgebrowser to the current calc
7.14 WN0825: not implemented in isac-java.
7.15 Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):
7.16 - Main success was showing UContext from Worksheet to the Example/Method/Problem/TheoryBrowser,
7.17 + Main success was showing UContext from Worksheet to the Example/MethodC/Problem/TheoryBrowser,
7.18 while the buttons on these browsers <To Worksheet> <Try Refine> have no
7.19 code in isac-java (and only partial, untested code in isabisac).
7.20 *)
7.21 @@ -385,7 +385,7 @@
7.22 ) handle _ => sysERROR2xml cI "setContext: met_ ???")
7.23
7.24
7.25 -(* specify the Method at the activeFormula and return a CalcHead containing the Guard.
7.26 +(* specify the MethodC at the activeFormula and return a CalcHead containing the Guard.
7.27 WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
7.28 fun setMethod cI mI =
7.29 (let
8.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Feb 03 15:21:12 2021 +0100
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Feb 03 16:39:44 2021 +0100
8.3 @@ -8,25 +8,25 @@
8.4 eqtype filepath
8.5 val file2str: filepath -> Thy_Present.filename -> string
8.6 val hierarchy: string -> 'a Store.node list -> string
8.7 - val hierarchy_met: Method.T Store.node list -> xml
8.8 + val hierarchy_met: MethodC.T Store.node list -> xml
8.9 val hierarchy_pbl: Problem.T Store.node list -> xml
8.10 val i: int
8.11 val id2filename: string list -> string
8.12 - val met2file: filepath -> Pos.pos -> Method.id -> Method.T -> unit
8.13 - val met2xml: Method.id -> Method.T -> xml
8.14 + val met2file: filepath -> Pos.pos -> MethodC.id -> MethodC.T -> unit
8.15 + val met2xml: MethodC.id -> MethodC.T -> xml
8.16 val met_hierarchy2file: filepath -> unit
8.17 val mets2file: filepath -> unit
8.18 val node: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node -> unit
8.19 val nodes: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node list -> unit
8.20 - val pbl2file: filepath -> Pos.pos -> Method.id -> Problem.T -> unit
8.21 + val pbl2file: filepath -> Pos.pos -> MethodC.id -> Problem.T -> unit
8.22 val pbl2term: theory -> Problem.id -> term
8.23 val pbl2xml: Problem.id -> Problem.T -> xml
8.24 val pbl_hierarchy2file: filepath -> unit
8.25 val pbls2file: filepath -> unit
8.26 val pos2filename: int list -> string
8.27 val str2file: Thy_Present.filename -> string -> unit
8.28 - val update_metdata: Method.T -> Error_Pattern_Def.T list -> Method.T
8.29 - val update_metpair: theory -> Method.id -> Error_Pattern_Def.T list -> Method.T * Method.id
8.30 + val update_metdata: MethodC.T -> Error_Pattern_Def.T list -> MethodC.T
8.31 + val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
8.32 end
8.33
8.34 (**)
8.35 @@ -102,7 +102,7 @@
8.36 in nds j [0] h : xml end;
8.37 fun hierarchy_met h =
8.38 let val j = indentation
8.39 - fun nd i p (Store.Node (id,[n as {guh,...} : Method.T],ns)) =
8.40 + fun nd i p (Store.Node (id,[n as {guh,...} : MethodC.T],ns)) =
8.41 let val p' = Pos.lev_on p
8.42 in (indt i) ^ "<NODE>\n" ^
8.43 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
8.44 @@ -217,7 +217,7 @@
8.45
8.46
8.47 (**. write pbls from hierarchy to files.**)
8.48 -fun pbl2file path (pos: Pos.pos) (id: Method.id) (pbl as {guh, ...}) =
8.49 +fun pbl2file path (pos: Pos.pos) (id: MethodC.id) (pbl as {guh, ...}) =
8.50 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos);
8.51 ((str2file (path ^ Thy_Present.guh2filename guh)) o (pbl2xml id)) pbl
8.52 );
8.53 @@ -227,8 +227,8 @@
8.54 new version with <KESTOREREF>s -- not used because linking
8.55 requires elements (rls, calc, ...) to be reorganized.*)
8.56 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
8.57 -fun met2xml (id: Method.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
8.58 - crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) =
8.59 +fun met2xml (id: MethodC.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
8.60 + crls,erls,errpats,nrls,prls,srls,rew_ord'}: MethodC.T) =
8.61 let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*)
8.62 val crls' = (#id o Rule_Set.rep) crls
8.63 val erls' = (#id o Rule_Set.rep) erls
8.64 @@ -265,8 +265,8 @@
8.65 end;
8.66 (*.format a method in xml for presentation on the method browser;
8.67 old version with 'dead' strings for rls, calc, ....*)
8.68 -fun met2xml (id: Method.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
8.69 - crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) =
8.70 +fun met2xml (id: MethodC.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
8.71 + crls,erls,errpats,nrls,prls,srls,rew_ord'}: MethodC.T) =
8.72 "<NODECONTENT>\n" ^
8.73 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
8.74 id2xml i id ^
8.75 @@ -290,12 +290,12 @@
8.76 *)
8.77
8.78 (*.write the files using an int-key (pos') as filename.*)
8.79 -fun met2file path (pos: Pos.pos) (id: Method.id) met =
8.80 +fun met2file path (pos: Pos.pos) (id: MethodC.id) met =
8.81 (writeln ("### met2file: id = " ^ strs2str id);
8.82 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
8.83
8.84 (*.write the files using the guh as filename.*)
8.85 -fun met2file path (pos: Pos.pos) (id: Method.id) (met as {guh,...}) =
8.86 +fun met2file path (pos: Pos.pos) (id: MethodC.id) (met as {guh,...}) =
8.87 (writeln ("### met2file: id = " ^ strs2str id);
8.88 ((str2file (path ^ Thy_Present.guh2filename guh)) o (met2xml id)) met);
8.89
8.90 @@ -327,15 +327,15 @@
8.91 *)
8.92
8.93 fun update_metdata
8.94 - ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: Method.T)
8.95 + ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: MethodC.T)
8.96 errpats' =
8.97 {guh = guh, mathauthors = mathauthors, init = init, rew_ord' = rew_ord', erls = erls,
8.98 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc,
8.99 - ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: Method.T
8.100 + ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: MethodC.T
8.101
8.102 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
8.103 fun update_metpair thy metID errpats = let
8.104 - val ret = (update_metdata (Method.from_store' thy metID) errpats, metID)
8.105 + val ret = (update_metdata (MethodC.from_store' thy metID) errpats, metID)
8.106 handle ERROR _ => raise ERROR ("update_metpair: " ^ (strs2str metID) ^ " must address a method");
8.107 in ret end;
8.108
9.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Wed Feb 03 15:21:12 2021 +0100
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Wed Feb 03 16:39:44 2021 +0100
9.3 @@ -12,7 +12,7 @@
9.4
9.5 type kestoreID
9.6 val pblID2guh : Problem.id -> Check_Unique.id
9.7 - val metID2guh : Method.id -> Check_Unique.id
9.8 + val metID2guh : MethodC.id -> Check_Unique.id
9.9 val kestoreID2guh : ketype -> kestoreID -> Check_Unique.id
9.10 val guh2kestoreID : Check_Unique.id -> string list (* for interface.sml *)
9.11
9.12 @@ -68,7 +68,7 @@
9.13 fun ketype2str' Exp_ = "Example"
9.14 | ketype2str' Thy_ = "Theory"
9.15 | ketype2str' Pbl_ = "Problem"
9.16 - | ketype2str' Met_ = "Method";
9.17 + | ketype2str' Met_ = "MethodC";
9.18 (* for conversion from XML *)
9.19 fun str2ketype' "exp" = Exp_
9.20 | str2ketype' "thy" = Thy_
9.21 @@ -76,14 +76,14 @@
9.22 | str2ketype' "met" = Met_
9.23 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
9.24
9.25 -(*either ThyC.id or Problem.id or Method.id*)
9.26 +(*either ThyC.id or Problem.id or MethodC.id*)
9.27 type kestoreID = string list;
9.28
9.29 (* make a guh from a reference to an element in the kestore;
9.30 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
9.31 fun pblID2guh pblID = (((#guh o Problem.from_store) pblID)
9.32 handle _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
9.33 -fun metID2guh metID = (((#guh o Method.from_store) metID)
9.34 +fun metID2guh metID = (((#guh o MethodC.from_store) metID)
9.35 handle _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
9.36 fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID
9.37 | kestoreID2guh Met_ kestoreID = metID2guh kestoreID
10.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Feb 03 15:21:12 2021 +0100
10.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Feb 03 16:39:44 2021 +0100
10.3 @@ -61,7 +61,7 @@
10.4 (**)
10.5 open TermC (* allows contains_one_of to be infix *)
10.6
10.7 -fun fun_id_of ({scr = prog, ...} : Method.T) =
10.8 +fun fun_id_of ({scr = prog, ...} : MethodC.T) =
10.9 case prog of
10.10 Rule.Empty_Prog => NONE
10.11 | Rule.Prog t =>
11.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/document/root.bib Wed Feb 03 15:21:12 2021 +0100
11.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.bib Wed Feb 03 16:39:44 2021 +0100
11.3 @@ -165,7 +165,7 @@
11.4 @InCollection{pl:formal-lang-hist,
11.5 author = {Lucas, Peter},
11.6 title = {On the Formalization of Programming Languages: Early History and Main Approaches},
11.7 - booktitle = {The Vienna Development Method: The Meta-Language},
11.8 + booktitle = {The Vienna Development MethodC: The Meta-Language},
11.9 publisher = {Springer},
11.10 year = {1978},
11.11 editor = {D. Bj{\o}rner and C. B. Jones},
12.1 --- a/src/Tools/isac/Interpret/derive.sml Wed Feb 03 15:21:12 2021 +0100
12.2 +++ b/src/Tools/isac/Interpret/derive.sml Wed Feb 03 16:39:44 2021 +0100
12.3 @@ -153,7 +153,7 @@
12.4 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
12.5 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
12.6 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
12.7 - val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
12.8 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
12.9 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
12.10 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
12.11 val pt = Ctree.update_branch pt p Ctree.TransitiveB
12.12 @@ -171,7 +171,7 @@
12.13 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
12.14 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
12.15 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
12.16 - val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
12.17 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
12.18 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
12.19 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
12.20 val pt = Ctree.update_branch pt p Ctree.TransitiveB
13.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Feb 03 15:21:12 2021 +0100
13.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Feb 03 16:39:44 2021 +0100
13.3 @@ -119,7 +119,7 @@
13.4 let
13.5 val f_curr = Ctree.get_curr_formula (pt, pos);
13.6 val pp = Ctree.par_pblobj pt p
13.7 - val (errpats, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
13.8 + val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
13.9 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
13.10 | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
13.11 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
14.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Feb 03 15:21:12 2021 +0100
14.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Feb 03 16:39:44 2021 +0100
14.3 @@ -13,7 +13,7 @@
14.4 | Not_Associated;
14.5 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
14.6
14.7 - val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> Method.id ->
14.8 + val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
14.9 Istate.T * Proof.context * Program.T
14.10 val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
14.11 (Istate.T * Proof.context) * Program.T
14.12 @@ -30,7 +30,7 @@
14.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.14 (*NONE*)
14.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
14.16 - val arguments_from_model : Method.id -> I_Model.T -> term list
14.17 + val arguments_from_model : MethodC.id -> I_Model.T -> term list
14.18 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.19 end
14.20
14.21 @@ -66,7 +66,7 @@
14.22 case find_first (test_dsc d) itms of
14.23 NONE => raise ERROR (error_msg_2 d itms)
14.24 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
14.25 - val pats = (#ppc o Method.from_store) mI
14.26 + val pats = (#ppc o MethodC.from_store) mI
14.27 val _ = if pats = [] then raise ERROR error_msg_1 else ()
14.28 in (flat o (map (itm2arg itms))) pats end;
14.29
14.30 @@ -228,14 +228,14 @@
14.31 val errmsg = "ERROR: found no actual arguments for prog. of "
14.32 fun msg_miss sc metID caller f formals actuals =
14.33 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
14.34 - "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
14.35 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
14.36 "formal arg \"" ^ UnparseC.term f ^ "\" doesn't mach an actual arg.\n" ^
14.37 "with:\n" ^
14.38 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
14.39 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals
14.40 fun msg_miss_type sc metID f formals actuals =
14.41 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
14.42 - "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
14.43 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
14.44 "formal arg \"" ^ UnparseC.term f ^ "\" of type \"" ^ UnparseC.typ (type_of f) ^
14.45 "\" doesn't mach an actual arg.\nwith:\n" ^
14.46 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
14.47 @@ -243,7 +243,7 @@
14.48 " with types: " ^ (strs2str o (map (UnparseC.typ o type_of))) actuals
14.49 fun msg_ambiguous sc metID f aas formals actuals =
14.50 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
14.51 - "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
14.52 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
14.53 "formal arg. \"" ^ UnparseC.term f ^ "\" type-matches with several..." ^
14.54 "actual args. \"" ^ UnparseC.terms aas ^ "\"\n" ^
14.55 "selected \"" ^ UnparseC.term (hd aas) ^ "\"\n" ^
14.56 @@ -259,9 +259,9 @@
14.57 let
14.58 val actuals = arguments_from_model metID itms
14.59 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
14.60 - val (scr, sc) = (case (#scr o Method.from_store) metID of
14.61 + val (scr, sc) = (case (#scr o MethodC.from_store) metID of
14.62 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
14.63 - | _ => raise ERROR ("init_pstate with " ^ Method.id_to_string metID))
14.64 + | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string metID))
14.65 val formals = Program.formal_args sc
14.66 fun assoc_by_type f aa =
14.67 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
14.68 @@ -276,7 +276,7 @@
14.69 else
14.70 let val (f, a) = assoc_by_type f aas
14.71 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
14.72 - val {pre, prls, ...} = Method.from_store metID;
14.73 + val {pre, prls, ...} = MethodC.from_store metID;
14.74 val pres = Pre_Conds.check prls pre itms 0 |> snd |> map snd;
14.75 val ctxt = ctxt |> ContextC.insert_assumptions pres;
14.76 val ist = Istate.e_pstate
14.77 @@ -292,7 +292,7 @@
14.78 let
14.79 val p' = Ctree.par_pblobj pt p
14.80 val metID = Ctree.get_obj Ctree.g_metID pt p'
14.81 - val {srls, ...} = Method.from_store metID
14.82 + val {srls, ...} = MethodC.from_store metID
14.83 in srls end
14.84
14.85 (* resume program interpretation at the beginning of a step *)
14.86 @@ -303,13 +303,13 @@
14.87 if is_problem then
14.88 let
14.89 val metID = get_obj g_metID pt p'
14.90 - val {srls, ...} = Method.from_store metID
14.91 + val {srls, ...} = MethodC.from_store metID
14.92 val (is, ctxt) =
14.93 case get_loc pt (p, p_) of
14.94 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
14.95 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
14.96 in
14.97 - ((is, ctxt), (#scr o Method.from_store) metID)
14.98 + ((is, ctxt), (#scr o MethodC.from_store) metID)
14.99 end
14.100 else
14.101 (get_loc pt (p, p_),
15.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Feb 03 15:21:12 2021 +0100
15.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Feb 03 16:39:44 2021 +0100
15.3 @@ -497,7 +497,7 @@
15.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
15.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
15.6 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
15.7 - val {ppc, ...} = Method.from_store mI;
15.8 + val {ppc, ...} = MethodC.from_store mI;
15.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
15.10 val srls = LItool.get_simplifier (pt, pos)
15.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
15.12 @@ -543,7 +543,7 @@
15.13 | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
15.14 let
15.15 val parent_pos = par_pblobj pt p
15.16 - val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
15.17 + val {scr, ...} = MethodC.from_store (get_obj g_metID pt parent_pos);
15.18 val prog_res =
15.19 case find_next_step scr (pt, pos) sub_ist sub_ctxt of
15.20 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
15.21 @@ -581,7 +581,7 @@
15.22 end
15.23 (*find_next_step from program, by_tactic will update Ctree*)
15.24 and do_next (ptp as (pt, pos as (p, p_))) =
15.25 - if Method.id_empty = get_obj g_metID pt (par_pblobj pt p) then
15.26 + if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) then
15.27 ("helpless", ([], [], (pt, (p, p_))))
15.28 else
15.29 let
15.30 @@ -611,7 +611,7 @@
15.31 fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
15.32 let
15.33 val fo = Calc.current_formula ptp
15.34 - val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
15.35 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
15.36 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
15.37 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
15.38 in
16.1 --- a/src/Tools/isac/Interpret/solve-step.sml Wed Feb 03 15:21:12 2021 +0100
16.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Feb 03 16:39:44 2021 +0100
16.3 @@ -52,7 +52,7 @@
16.4 then
16.5 let
16.6 val thy' = Ctree.get_obj Ctree.g_domID pt p'
16.7 - val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt p')
16.8 + val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
16.9 in ("OK", thy', rew_ord', erls, false) end
16.10 else
16.11 let
16.12 @@ -69,7 +69,7 @@
16.13 then
16.14 let
16.15 val thy' = Ctree.get_obj Ctree.g_domID pt p'
16.16 - val {calc = scr_isa_fns, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt p')
16.17 + val {calc = scr_isa_fns, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
16.18 val opt = assoc (scr_isa_fns, scrop)
16.19 in
16.20 case opt of
16.21 @@ -154,7 +154,7 @@
16.22 val pp = Ctree.par_pblobj pt p;
16.23 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
16.24 val thy = ThyC.get_theory thy';
16.25 - val {rew_ord' = ro', erls = erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp);
16.26 + val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
16.27 val f = Calc.current_formula cs;
16.28 val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
16.29 in
16.30 @@ -188,14 +188,14 @@
16.31 | NONE => Applicable.No (rls ^ " not applicable")
16.32 end
16.33 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
16.34 - Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
16.35 + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [],
16.36 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
16.37 | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
16.38 let
16.39 val pp = Ctree.par_pblobj pt p
16.40 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
16.41 val f = Calc.current_formula cs;
16.42 - val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp)
16.43 + val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
16.44 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
16.45 val subst = Subst.T_from_string_eqs thy sube
16.46 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
17.1 --- a/src/Tools/isac/Interpret/step-solve.sml Wed Feb 03 15:21:12 2021 +0100
17.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Feb 03 16:39:44 2021 +0100
17.3 @@ -24,7 +24,7 @@
17.4 | by_tactic (Tactic.Free_Solve') (pt, po as (p, _)) =
17.5 let
17.6 val p' = lev_dn_ (p, Res);
17.7 - val pt = update_metID pt (par_pblobj pt p) Method.id_empty;
17.8 + val pt = update_metID pt (par_pblobj pt p) MethodC.id_empty;
17.9 in
17.10 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.empty)))], [], (pt,p')))
17.11 end
17.12 @@ -36,7 +36,7 @@
17.13 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
17.14 end
17.15 | by_tactic m (pt, po as (p, p_)) =
17.16 - if Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
17.17 + if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
17.18 then
17.19 let
17.20 val ctxt = get_ctxt pt po
17.21 @@ -109,7 +109,7 @@
17.22 | LI.Not_Derivable =>
17.23 let
17.24 val pp = Ctree.par_pblobj pt p
17.25 - val (errpats, nrls, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
17.26 + val (errpats, nrls, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
17.27 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
17.28 | _ => raise ERROR "inform: uncovered case of get_met"
17.29 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
18.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Wed Feb 03 15:21:12 2021 +0100
18.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed Feb 03 16:39:44 2021 +0100
18.3 @@ -34,12 +34,12 @@
18.4 Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
18.5
18.6 setup \<open>KEStore_Elems.add_mets
18.7 - [Method.prep_input thy "met_algein" [] Method.id_empty
18.8 + [MethodC.prep_input thy "met_algein" [] MethodC.id_empty
18.9 (["Berechnung"], [],
18.10 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
18.11 errpats = [], nrls = Rule_Set.Empty},
18.12 @{thm refl}),
18.13 - Method.prep_input thy "met_algein_numsym" [] Method.id_empty
18.14 + MethodC.prep_input thy "met_algein_numsym" [] MethodC.id_empty
18.15 (["Berechnung", "erstNumerisch"], [],
18.16 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
18.17 errpats = [], nrls = Rule_Set.Empty},
18.18 @@ -69,7 +69,7 @@
18.19 in
18.20 Try (Rewrite_Set ''norm_Poly'') t_t)"
18.21 setup \<open>KEStore_Elems.add_mets
18.22 - [Method.prep_input thy "met_algein_numsym_1num" [] Method.id_empty
18.23 + [MethodC.prep_input thy "met_algein_numsym_1num" [] MethodC.id_empty
18.24 (["Berechnung", "erstNumerisch"],
18.25 [("#Given" ,["KantenLaenge k_k", "Querschnitt q__q", "KantenUnten u_u",
18.26 "KantenSenkrecht s_s", "KantenOben o_o"]),
18.27 @@ -102,7 +102,7 @@
18.28 in
18.29 (Try (Rewrite_Set ''norm_Poly'')) t_t)"
18.30 setup \<open>KEStore_Elems.add_mets
18.31 - [Method.prep_input thy "met_algein_symnum" [] Method.id_empty
18.32 + [MethodC.prep_input thy "met_algein_symnum" [] MethodC.id_empty
18.33 (["Berechnung", "erstSymbolisch"],
18.34 [("#Given" ,["KantenLaenge k_k", "Querschnitt q__q", "KantenUnten u_u",
18.35 "KantenSenkrecht s_s", "KantenOben o_o"]),
19.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Feb 03 15:21:12 2021 +0100
19.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Feb 03 16:39:44 2021 +0100
19.3 @@ -192,7 +192,7 @@
19.4 section \<open>Methods\<close>
19.5 (* setup parent directory *)
19.6 setup \<open>KEStore_Elems.add_mets
19.7 - [Method.prep_input @{theory} "met_biege" [] Method.id_empty
19.8 + [MethodC.prep_input @{theory} "met_biege" [] MethodC.id_empty
19.9 (["IntegrierenUndKonstanteBestimmen"], [],
19.10 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
19.11 errpats = [], nrls = Rule_Set.Empty},
19.12 @@ -205,26 +205,26 @@
19.13 v-- the root Problem calling SubProblems according to indentation
19.14
19.15 Problem ["Biegelinien"]
19.16 - Method ["IntegrierenUndKonstanteBestimmen2"] biegelinie
19.17 + MethodC ["IntegrierenUndKonstanteBestimmen2"] biegelinie
19.18
19.19 Problem ["vonBelastungZu", "Biegelinien"]
19.20 - Method ["Biegelinien", "ausBelastung"] belastung_zu_biegelinie
19.21 + MethodC ["Biegelinien", "ausBelastung"] belastung_zu_biegelinie
19.22
19.23 Problem ["named", "integrate", "function"]
19.24 - Method ["diff", "integration", "named"]
19.25 + MethodC ["diff", "integration", "named"]
19.26
19.27 -"- 4 times
19.28
19.29 Problem ["setzeRandbedingungen", "Biegelinien"]
19.30 - Method ["Biegelinien", "setzeRandbedingungenEin"] setzte_randbedingungen
19.31 + MethodC ["Biegelinien", "setzeRandbedingungenEin"] setzte_randbedingungen
19.32
19.33 Problem ["makeFunctionTo", "equation"]
19.34 - Method ["Equation", "fromFunction"]
19.35 + MethodC ["Equation", "fromFunction"]
19.36
19.37 -"- 4 times
19.38
19.39 Problem ["LINEAR", "system"]
19.40 - Method ["no_met"]
19.41 + MethodC ["no_met"]
19.42 ^^^^^^--- thus automatied refinement to appropriate Problem
19.43 \<close>
19.44
19.45 @@ -248,7 +248,7 @@
19.46 B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', fun_var)] ''make_ratpoly_in'')) B
19.47 in B)"
19.48 setup \<open>KEStore_Elems.add_mets
19.49 - [Method.prep_input @{theory} "met_biege_2" [] Method.id_empty
19.50 + [MethodC.prep_input @{theory} "met_biege_2" [] MethodC.id_empty
19.51 (["IntegrierenUndKonstanteBestimmen2"],
19.52 [("#Given" ,["Traegerlaenge beam", "Streckenlast load",
19.53 "FunktionsVariable fun_var", "GleichungsVariablen vs", "AbleitungBiegelinie id_der"]),
19.54 @@ -271,22 +271,22 @@
19.55 @{thm biegelinie.simps})]
19.56 \<close>
19.57 setup \<open>KEStore_Elems.add_mets
19.58 - [Method.prep_input @{theory} "met_biege_intconst_2" [] Method.id_empty
19.59 + [MethodC.prep_input @{theory} "met_biege_intconst_2" [] MethodC.id_empty
19.60 (["IntegrierenUndKonstanteBestimmen", "2xIntegrieren"], [],
19.61 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
19.62 errpats = [], nrls = Rule_Set.empty},
19.63 @{thm refl}),
19.64 - Method.prep_input @{theory} "met_biege_intconst_4" [] Method.id_empty
19.65 + MethodC.prep_input @{theory} "met_biege_intconst_4" [] MethodC.id_empty
19.66 (["IntegrierenUndKonstanteBestimmen", "4x4System"], [],
19.67 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
19.68 errpats = [], nrls = Rule_Set.empty},
19.69 @{thm refl}),
19.70 - Method.prep_input @{theory} "met_biege_intconst_1" [] Method.id_empty
19.71 + MethodC.prep_input @{theory} "met_biege_intconst_1" [] MethodC.id_empty
19.72 (["IntegrierenUndKonstanteBestimmen", "1xIntegrieren"], [],
19.73 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
19.74 errpats = [], nrls = Rule_Set.empty},
19.75 @{thm refl}),
19.76 - Method.prep_input @{theory} "met_biege2" [] Method.id_empty
19.77 + MethodC.prep_input @{theory} "met_biege2" [] MethodC.id_empty
19.78 (["Biegelinien"], [],
19.79 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
19.80 errpats = [], nrls = Rule_Set.empty},
19.81 @@ -319,7 +319,7 @@
19.82 in
19.83 [Q__Q, M__M, N__N, B__B])" (*..Q is Const Querkraft -------------------------^ *)
19.84 setup \<open>KEStore_Elems.add_mets
19.85 - [Method.prep_input @{theory} "met_biege_ausbelast" [] Method.id_empty
19.86 + [MethodC.prep_input @{theory} "met_biege_ausbelast" [] MethodC.id_empty
19.87 (["Biegelinien", "ausBelastung"],
19.88 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",
19.89 "Biegelinie id_fun", "AbleitungBiegelinie id_der"]),
19.90 @@ -360,7 +360,7 @@
19.91 in
19.92 [e_1, e_2, e_3, e_4])"
19.93 setup \<open>KEStore_Elems.add_mets
19.94 - [Method.prep_input @{theory} "met_biege_setzrand" [] Method.id_empty
19.95 + [MethodC.prep_input @{theory} "met_biege_setzrand" [] MethodC.id_empty
19.96 (["Biegelinien", "setzeRandbedingungenEin"],
19.97 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
19.98 ("#Find" , ["Gleichungen equs'''"])],
19.99 @@ -384,7 +384,7 @@
19.100 in
19.101 (Rewrite_Set ''norm_Rational'') eq_u)"
19.102 setup \<open>KEStore_Elems.add_mets
19.103 - [Method.prep_input @{theory} "met_equ_fromfun" [] Method.id_empty
19.104 + [MethodC.prep_input @{theory} "met_equ_fromfun" [] MethodC.id_empty
19.105 (["Equation", "fromFunction"],
19.106 [("#Given" ,["functionEq fu_n", "substitution su_b"]),
19.107 ("#Find" ,["equality equ'''"])],
20.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Feb 03 15:21:12 2021 +0100
20.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Feb 03 16:39:44 2021 +0100
20.3 @@ -272,7 +272,7 @@
20.4 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
20.5 \<close>
20.6 setup \<open>KEStore_Elems.add_mets
20.7 - [Method.prep_input thy "met_diff" [] Method.id_empty
20.8 + [MethodC.prep_input thy "met_diff" [] MethodC.id_empty
20.9 (["diff"], [],
20.10 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
20.11 crls = Atools_erls, errpats = [], nrls = norm_diff},
20.12 @@ -307,7 +307,7 @@
20.13 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
20.14 ) f_f')"
20.15 setup \<open>KEStore_Elems.add_mets
20.16 - [Method.prep_input thy "met_diff_onR" [] Method.id_empty
20.17 + [MethodC.prep_input thy "met_diff_onR" [] MethodC.id_empty
20.18 (["diff", "differentiate_on_R"],
20.19 [("#Given" ,["functionTerm f_f", "differentiateFor v_v"]),
20.20 ("#Find" ,["derivative f_f'"])],
20.21 @@ -342,7 +342,7 @@
20.22 (Repeat (Rewrite_Set ''make_polynomial'')))
20.23 ) f_f')"
20.24 setup \<open>KEStore_Elems.add_mets
20.25 - [Method.prep_input thy "met_diff_simpl" [] Method.id_empty
20.26 + [MethodC.prep_input thy "met_diff_simpl" [] MethodC.id_empty
20.27 (["diff", "diff_simpl"],
20.28 [("#Given", ["functionTerm f_f", "differentiateFor v_v"]),
20.29 ("#Find" , ["derivative f_f'"])],
20.30 @@ -380,7 +380,7 @@
20.31 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
20.32 ) f_f')"
20.33 setup \<open>KEStore_Elems.add_mets
20.34 - [Method.prep_input thy "met_diff_equ" [] Method.id_empty
20.35 + [MethodC.prep_input thy "met_diff_equ" [] MethodC.id_empty
20.36 (["diff", "differentiate_equality"],
20.37 [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),
20.38 ("#Find" ,["derivativeEq f_f'"])],
20.39 @@ -403,7 +403,7 @@
20.40 ) term')"
20.41
20.42 setup \<open>KEStore_Elems.add_mets
20.43 - [Method.prep_input thy "met_diff_after_simp" [] Method.id_empty
20.44 + [MethodC.prep_input thy "met_diff_after_simp" [] MethodC.id_empty
20.45 (["diff", "after_simplification"],
20.46 [("#Given" ,["functionTerm term", "differentiateFor bound_variable"]),
20.47 ("#Find" ,["derivative term'"])],
21.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Feb 03 15:21:12 2021 +0100
21.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Feb 03 16:39:44 2021 +0100
21.3 @@ -315,7 +315,7 @@
21.4 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
21.5 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
21.6 val (dI',pI',mI')=
21.7 - ("DiffAppl",["Program", "maximum_of", "function"],Method.id_empty);
21.8 + ("DiffAppl",["Program", "maximum_of", "function"],MethodC.id_empty);
21.9 val c = []:cid;
21.10
21.11 (*
21.12 @@ -413,7 +413,7 @@
21.13 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
21.14 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
21.15 val (dI',pI',mI')=
21.16 - ("DiffAppl",["DiffAppl", "test_maximum"],Method.id_empty);
21.17 + ("DiffAppl",["DiffAppl", "test_maximum"],MethodC.id_empty);
21.18 val p = e_pos'; val c = [];
21.19
21.20 (*/------- Init_Proof replaced by Test_Code.CalcTreeTEST ------------------------------------\* )
22.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Feb 03 15:21:12 2021 +0100
22.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Feb 03 16:39:44 2021 +0100
22.3 @@ -103,7 +103,7 @@
22.4
22.5 (** methods, scripts not yet implemented **)
22.6 setup \<open>KEStore_Elems.add_mets
22.7 - [Method.prep_input thy "met_diffapp" [] Method.id_empty
22.8 + [MethodC.prep_input thy "met_diffapp" [] MethodC.id_empty
22.9 (["DiffApp"], [],
22.10 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
22.11 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
22.12 @@ -125,7 +125,7 @@
22.13 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
22.14 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
22.15 setup \<open>KEStore_Elems.add_mets
22.16 - [Method.prep_input thy "met_diffapp_max" [] Method.id_empty
22.17 + [MethodC.prep_input thy "met_diffapp_max" [] MethodC.id_empty
22.18 (["DiffApp", "max_by_calculus"],
22.19 [("#Given" ,["fixedValues f_ix", "maximum m_m", "relations r_s", "boundVariable v_v",
22.20 "interval i_tv", "errorBound e_rr"]),
22.21 @@ -152,7 +152,7 @@
22.22 [BOOL e_2, REAL v_2]
22.23 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
22.24 setup \<open>KEStore_Elems.add_mets
22.25 - [Method.prep_input thy "met_diffapp_funnew" [] Method.id_empty
22.26 + [MethodC.prep_input thy "met_diffapp_funnew" [] MethodC.id_empty
22.27 (["DiffApp", "make_fun_by_new_variable"],
22.28 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
22.29 ("#Find" ,["functionEq f_1"])],
22.30 @@ -172,7 +172,7 @@
22.31 [BOOL e_1, REAL v_1]
22.32 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
22.33 setup \<open>KEStore_Elems.add_mets
22.34 - [Method.prep_input thy "met_diffapp_funexp" [] Method.id_empty
22.35 + [MethodC.prep_input thy "met_diffapp_funexp" [] MethodC.id_empty
22.36 (["DiffApp", "make_fun_by_explicit"],
22.37 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
22.38 ("#Find" ,["functionEq f_1"])],
22.39 @@ -181,14 +181,14 @@
22.40 @{thm make_fun_by_explicit.simps})]
22.41 \<close>
22.42 setup \<open>KEStore_Elems.add_mets
22.43 - [Method.prep_input thy "met_diffapp_max_oninterval" [] Method.id_empty
22.44 + [MethodC.prep_input thy "met_diffapp_max_oninterval" [] MethodC.id_empty
22.45 (["DiffApp", "max_on_interval_by_calculus"],
22.46 [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"(*, "errorBound e_rr"*)]),
22.47 ("#Find" ,["maxArgument v_0"])],
22.48 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
22.49 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
22.50 @{thm refl}),
22.51 - Method.prep_input thy "met_diffapp_findvals" [] Method.id_empty
22.52 + MethodC.prep_input thy "met_diffapp_findvals" [] MethodC.id_empty
22.53 (["DiffApp", "find_values"], [],
22.54 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
22.55 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
23.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed Feb 03 15:21:12 2021 +0100
23.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed Feb 03 16:39:44 2021 +0100
23.3 @@ -33,7 +33,7 @@
23.4 (Try (Calculate ''PLUS'')) #>
23.5 (Try (Calculate ''TIMES''))) e_e)"
23.6 setup \<open>KEStore_Elems.add_mets
23.7 - [Method.prep_input thy "met_test_diophant" [] Method.id_empty
23.8 + [MethodC.prep_input thy "met_test_diophant" [] MethodC.id_empty
23.9 (["Test", "solve_diophant"],
23.10 [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
23.11 (* TODO: drop ^^^^^*)
24.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Feb 03 15:21:12 2021 +0100
24.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Feb 03 16:39:44 2021 +0100
24.3 @@ -513,12 +513,12 @@
24.4 section \<open>Methods\<close>
24.5
24.6 setup \<open>KEStore_Elems.add_mets
24.7 - [Method.prep_input thy "met_eqsys" [] Method.id_empty
24.8 + [MethodC.prep_input thy "met_eqsys" [] MethodC.id_empty
24.9 (["EqSystem"], [],
24.10 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
24.11 errpats = [], nrls = Rule_Set.Empty},
24.12 @{thm refl}),
24.13 - Method.prep_input thy "met_eqsys_topdown" [] Method.id_empty
24.14 + MethodC.prep_input thy "met_eqsys_topdown" [] MethodC.id_empty
24.15 (["EqSystem", "top_down_substitution"], [],
24.16 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
24.17 errpats = [], nrls = Rule_Set.Empty},
24.18 @@ -545,7 +545,7 @@
24.19 in
24.20 Try (Rewrite_Set ''order_system'' ) e__s) "
24.21 setup \<open>KEStore_Elems.add_mets
24.22 - [Method.prep_input thy "met_eqsys_topdown_2x2" [] Method.id_empty
24.23 + [MethodC.prep_input thy "met_eqsys_topdown_2x2" [] MethodC.id_empty
24.24 (["EqSystem", "top_down_substitution", "2x2"],
24.25 [("#Given", ["equalities e_s", "solveForVars v_s"]),
24.26 ("#Where",
24.27 @@ -561,7 +561,7 @@
24.28 @{thm solve_system.simps})]
24.29 \<close>
24.30 setup \<open>KEStore_Elems.add_mets
24.31 - [Method.prep_input thy "met_eqsys_norm" [] Method.id_empty
24.32 + [MethodC.prep_input thy "met_eqsys_norm" [] MethodC.id_empty
24.33 (["EqSystem", "normalise"], [],
24.34 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
24.35 errpats = [], nrls = Rule_Set.Empty},
24.36 @@ -583,7 +583,7 @@
24.37 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
24.38 [BOOL_LIST e__s, REAL_LIST v_s])"
24.39 setup \<open>KEStore_Elems.add_mets
24.40 - [Method.prep_input thy "met_eqsys_norm_2x2" [] Method.id_empty
24.41 + [MethodC.prep_input thy "met_eqsys_norm_2x2" [] MethodC.id_empty
24.42 (["EqSystem", "normalise", "2x2"],
24.43 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
24.44 ("#Find" ,["solution ss'''"])],
24.45 @@ -615,7 +615,7 @@
24.46 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
24.47 [BOOL_LIST e__s, REAL_LIST v_s])"
24.48 setup \<open>KEStore_Elems.add_mets
24.49 - [Method.prep_input thy "met_eqsys_norm_4x4" [] Method.id_empty
24.50 + [MethodC.prep_input thy "met_eqsys_norm_4x4" [] MethodC.id_empty
24.51 (["EqSystem", "normalise", "4x4"],
24.52 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
24.53 ("#Find" ,["solution ss'''"])],
24.54 @@ -647,7 +647,7 @@
24.55 in
24.56 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
24.57 setup \<open>KEStore_Elems.add_mets
24.58 - [Method.prep_input thy "met_eqsys_topdown_4x4" [] Method.id_empty
24.59 + [MethodC.prep_input thy "met_eqsys_topdown_4x4" [] MethodC.id_empty
24.60 (["EqSystem", "top_down_substitution", "4x4"],
24.61 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
24.62 ("#Where" , (*accepts missing variables up to diagonal form*)
25.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Feb 03 15:21:12 2021 +0100
25.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Feb 03 16:39:44 2021 +0100
25.3 @@ -81,7 +81,7 @@
25.4
25.5
25.6 setup \<open>KEStore_Elems.add_mets
25.7 - [Method.prep_input thy "met_equ" [] Method.id_empty
25.8 + [MethodC.prep_input thy "met_equ" [] MethodC.id_empty
25.9 (["Equation"], [],
25.10 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
25.11 errpats = [], nrls = Rule_Set.empty},
26.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Wed Feb 03 15:21:12 2021 +0100
26.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed Feb 03 16:39:44 2021 +0100
26.3 @@ -85,11 +85,11 @@
26.4 section \<open>methods\<close>
26.5 (* TODO: implementation needs extra object-level lists ?!?*)
26.6 setup \<open>KEStore_Elems.add_mets
26.7 - [ Method.prep_input @{theory} "met_Programming" [] Method.id_empty
26.8 + [ MethodC.prep_input @{theory} "met_Programming" [] MethodC.id_empty
26.9 (["Programming"], [],
26.10 {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
26.11 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
26.12 - Method.prep_input @{theory} "met_Prog_sort" [] Method.id_empty
26.13 + MethodC.prep_input @{theory} "met_Prog_sort" [] MethodC.id_empty
26.14 (["Programming", "SORT"], [],
26.15 {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
26.16 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},
26.17 @@ -104,7 +104,7 @@
26.18 in
26.19 (Rewrite_Set ''ins_sort'') uns)"
26.20 setup \<open>KEStore_Elems.add_mets
26.21 - [Method.prep_input @{theory} "met_Prog_sort_ins" [] Method.id_empty
26.22 + [MethodC.prep_input @{theory} "met_Prog_sort_ins" [] MethodC.id_empty
26.23 (["Programming", "SORT", "insertion"],
26.24 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
26.25 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
26.26 @@ -134,7 +134,7 @@
26.27 (Repeat (Rewrite ''if_False'')))
26.28 ) uns)"
26.29 setup \<open>KEStore_Elems.add_mets
26.30 - [Method.prep_input @{theory} "met_Prog_sort_ins_steps" [] Method.id_empty
26.31 + [MethodC.prep_input @{theory} "met_Prog_sort_ins_steps" [] MethodC.id_empty
26.32 (["Programming", "SORT", "insertion_steps"],
26.33 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
26.34 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
27.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 03 15:21:12 2021 +0100
27.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 03 16:39:44 2021 +0100
27.3 @@ -357,7 +357,7 @@
27.4 in
27.5 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
27.6 setup \<open>KEStore_Elems.add_mets
27.7 - [Method.prep_input thy "met_diffint" [] Method.id_empty
27.8 + [MethodC.prep_input thy "met_diffint" [] MethodC.id_empty
27.9 (["diff", "integration"],
27.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
27.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
27.12 @@ -375,7 +375,7 @@
27.13 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
27.14 ) t_t)"
27.15 setup \<open>KEStore_Elems.add_mets
27.16 - [Method.prep_input thy "met_diffint_named" [] Method.id_empty
27.17 + [MethodC.prep_input thy "met_diffint_named" [] MethodC.id_empty
27.18 (["diff", "integration", "named"],
27.19 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
27.20 ("#Find" ,["antiDerivativeName F_F"])],
28.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Feb 03 15:21:12 2021 +0100
28.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Feb 03 16:39:44 2021 +0100
28.3 @@ -56,14 +56,14 @@
28.4 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE,
28.5 [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
28.6
28.7 -subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
28.8 +subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
28.9 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
28.10 setup \<open>KEStore_Elems.add_mets
28.11 - [Method.prep_input thy "met_SP" [] Method.id_empty
28.12 + [MethodC.prep_input thy "met_SP" [] MethodC.id_empty
28.13 (["SignalProcessing"], [],
28.14 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
28.15 errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
28.16 - Method.prep_input thy "met_SP_Ztrans" [] Method.id_empty
28.17 + MethodC.prep_input thy "met_SP_Ztrans" [] MethodC.id_empty
28.18 (["SignalProcessing", "Z_Transform"], [],
28.19 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
28.20 errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
28.21 @@ -87,7 +87,7 @@
28.22 [BOOL equ, REAL X_z]
28.23 in X) "
28.24 setup \<open>KEStore_Elems.add_mets
28.25 - [Method.prep_input thy "met_SP_Ztrans_inv" [] Method.id_empty
28.26 + [MethodC.prep_input thy "met_SP_Ztrans_inv" [] MethodC.id_empty
28.27 (["SignalProcessing", "Z_Transform", "Inverse"],
28.28 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
28.29 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
28.30 @@ -115,7 +115,7 @@
28.31 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
28.32 in n_eq)"
28.33 setup \<open>KEStore_Elems.add_mets
28.34 - [Method.prep_input thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
28.35 + [MethodC.prep_input thy "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
28.36 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
28.37 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
28.38 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
29.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Feb 03 15:21:12 2021 +0100
29.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Feb 03 16:39:44 2021 +0100
29.3 @@ -127,7 +127,7 @@
29.4
29.5 (*-------------- methods------------------------------------------------------*)
29.6 setup \<open>KEStore_Elems.add_mets
29.7 - [Method.prep_input thy "met_eqlin" [] Method.id_empty
29.8 + [MethodC.prep_input thy "met_eqlin" [] MethodC.id_empty
29.9 (["LinEq"], [],
29.10 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
29.11 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
29.12 @@ -151,7 +151,7 @@
29.13 in
29.14 Or_to_List e_e)"
29.15 setup \<open>KEStore_Elems.add_mets
29.16 - [Method.prep_input thy "met_eq_lin" [] Method.id_empty
29.17 + [MethodC.prep_input thy "met_eq_lin" [] MethodC.id_empty
29.18 (["LinEq", "solve_lineq_equation"],
29.19 [("#Given", ["equality e_e", "solveFor v_v"]),
29.20 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]),
29.21 @@ -160,7 +160,7 @@
29.22 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
29.23 @{thm solve_linear_equation.simps})]
29.24 \<close>
29.25 -ML \<open>Method.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
29.26 +ML \<open>MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
29.27
29.28 end
29.29
30.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Feb 03 15:21:12 2021 +0100
30.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Feb 03 16:39:44 2021 +0100
30.3 @@ -44,7 +44,7 @@
30.4 in
30.5 [e_e])"
30.6 setup \<open>KEStore_Elems.add_mets
30.7 - [Method.prep_input thy "met_equ_log" [] Method.id_empty
30.8 + [MethodC.prep_input thy "met_equ_log" [] MethodC.id_empty
30.9 (["Equation", "solve_log"],
30.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
30.11 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
31.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Feb 03 15:21:12 2021 +0100
31.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Feb 03 16:39:44 2021 +0100
31.3 @@ -160,7 +160,7 @@
31.4 NONE,
31.5 [["simplification", "of_rationals", "to_partial_fraction"]]))]\<close>
31.6
31.7 -subsection \<open>Method\<close>
31.8 +subsection \<open>MethodC\<close>
31.9 text \<open>rule set for functions called in the Program\<close>
31.10 ML \<open>
31.11 val srls_partial_fraction = Rule_Def.Repeat {id="srls_partial_fraction",
31.12 @@ -228,7 +228,7 @@
31.13 pbz = Substitute [AA = a, BB = b] pbz \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
31.14 in pbz) "
31.15 setup \<open>KEStore_Elems.add_mets
31.16 - [Method.prep_input @{theory} "met_partial_fraction" [] Method.id_empty
31.17 + [MethodC.prep_input @{theory} "met_partial_fraction" [] MethodC.id_empty
31.18 (["simplification", "of_rationals", "to_partial_fraction"],
31.19 [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
31.20 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
32.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Feb 03 15:21:12 2021 +0100
32.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Feb 03 16:39:44 2021 +0100
32.3 @@ -1450,7 +1450,7 @@
32.4 where
32.5 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
32.6 setup \<open>KEStore_Elems.add_mets
32.7 - [Method.prep_input thy "met_simp_poly" [] Method.id_empty
32.8 + [MethodC.prep_input thy "met_simp_poly" [] MethodC.id_empty
32.9 (["simplification", "for_polynomials"],
32.10 [("#Given" ,["Term t_t"]),
32.11 ("#Where" ,["t_t is_polyexp"]),
33.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Feb 03 15:21:12 2021 +0100
33.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Feb 03 16:39:44 2021 +0100
33.3 @@ -901,7 +901,7 @@
33.4
33.5 text \<open>"-------------------------methods-----------------------"\<close>
33.6 setup \<open>KEStore_Elems.add_mets
33.7 - [Method.prep_input thy "met_polyeq" [] Method.id_empty
33.8 + [MethodC.prep_input thy "met_polyeq" [] MethodC.id_empty
33.9 (["PolyEq"], [],
33.10 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
33.11 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
33.12 @@ -922,7 +922,7 @@
33.13 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
33.14 [BOOL e_e, REAL v_v])"
33.15 setup \<open>KEStore_Elems.add_mets
33.16 - [Method.prep_input thy "met_polyeq_norm" [] Method.id_empty
33.17 + [MethodC.prep_input thy "met_polyeq_norm" [] MethodC.id_empty
33.18 (["PolyEq", "normalise_poly"],
33.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.20 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
33.21 @@ -940,7 +940,7 @@
33.22 in
33.23 Or_to_List e_e)"
33.24 setup \<open>KEStore_Elems.add_mets
33.25 - [Method.prep_input thy "met_polyeq_d0" [] Method.id_empty
33.26 + [MethodC.prep_input thy "met_polyeq_d0" [] MethodC.id_empty
33.27 (["PolyEq", "solve_d0_polyeq_equation"],
33.28 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.29 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
33.30 @@ -963,7 +963,7 @@
33.31 in
33.32 Check_elementwise L_L {(v_v::real). Assumptions})"
33.33 setup \<open>KEStore_Elems.add_mets
33.34 - [Method.prep_input thy "met_polyeq_d1" [] Method.id_empty
33.35 + [MethodC.prep_input thy "met_polyeq_d1" [] MethodC.id_empty
33.36 (["PolyEq", "solve_d1_polyeq_equation"],
33.37 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.38 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
33.39 @@ -988,7 +988,7 @@
33.40 in
33.41 Check_elementwise L_L {(v_v::real). Assumptions})"
33.42 setup \<open>KEStore_Elems.add_mets
33.43 - [Method.prep_input thy "met_polyeq_d22" [] Method.id_empty
33.44 + [MethodC.prep_input thy "met_polyeq_d22" [] MethodC.id_empty
33.45 (["PolyEq", "solve_d2_polyeq_equation"],
33.46 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.47 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
33.48 @@ -1013,7 +1013,7 @@
33.49 in
33.50 Check_elementwise L_L {(v_v::real). Assumptions})"
33.51 setup \<open>KEStore_Elems.add_mets
33.52 - [Method.prep_input thy "met_polyeq_d2_bdvonly" [] Method.id_empty
33.53 + [MethodC.prep_input thy "met_polyeq_d2_bdvonly" [] MethodC.id_empty
33.54 (["PolyEq", "solve_d2_polyeq_bdvonly_equation"],
33.55 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.56 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
33.57 @@ -1036,7 +1036,7 @@
33.58 in
33.59 Check_elementwise L_L {(v_v::real). Assumptions})"
33.60 setup \<open>KEStore_Elems.add_mets
33.61 - [Method.prep_input thy "met_polyeq_d2_sqonly" [] Method.id_empty
33.62 + [MethodC.prep_input thy "met_polyeq_d2_sqonly" [] MethodC.id_empty
33.63 (["PolyEq", "solve_d2_polyeq_sqonly_equation"],
33.64 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.65 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
33.66 @@ -1059,7 +1059,7 @@
33.67 in
33.68 Check_elementwise L_L {(v_v::real). Assumptions})"
33.69 setup \<open>KEStore_Elems.add_mets
33.70 - [Method.prep_input thy "met_polyeq_d2_pq" [] Method.id_empty
33.71 + [MethodC.prep_input thy "met_polyeq_d2_pq" [] MethodC.id_empty
33.72 (["PolyEq", "solve_d2_polyeq_pq_equation"],
33.73 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.74 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
33.75 @@ -1081,7 +1081,7 @@
33.76 L_L = Or_to_List e_e
33.77 in Check_elementwise L_L {(v_v::real). Assumptions})"
33.78 setup \<open>KEStore_Elems.add_mets
33.79 - [Method.prep_input thy "met_polyeq_d2_abc" [] Method.id_empty
33.80 + [MethodC.prep_input thy "met_polyeq_d2_abc" [] MethodC.id_empty
33.81 (["PolyEq", "solve_d2_polyeq_abc_equation"],
33.82 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.83 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
33.84 @@ -1108,7 +1108,7 @@
33.85 in
33.86 Check_elementwise L_L {(v_v::real). Assumptions})"
33.87 setup \<open>KEStore_Elems.add_mets
33.88 - [Method.prep_input thy "met_polyeq_d3" [] Method.id_empty
33.89 + [MethodC.prep_input thy "met_polyeq_d3" [] MethodC.id_empty
33.90 (["PolyEq", "solve_d3_polyeq_equation"],
33.91 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.92 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
33.93 @@ -1138,7 +1138,7 @@
33.94 in
33.95 Or_to_List e_e)"
33.96 setup \<open>KEStore_Elems.add_mets
33.97 - [Method.prep_input thy "met_polyeq_complsq" [] Method.id_empty
33.98 + [MethodC.prep_input thy "met_polyeq_complsq" [] MethodC.id_empty
33.99 (["PolyEq", "complete_square"],
33.100 [("#Given" ,["equality e_e", "solveFor v_v"]),
33.101 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
34.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Feb 03 15:21:12 2021 +0100
34.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Feb 03 16:39:44 2021 +0100
34.3 @@ -480,7 +480,7 @@
34.4 (Try (Rewrite_Set ''verschoenere'')))
34.5 ) t_t)"
34.6 setup \<open>KEStore_Elems.add_mets
34.7 - [Method.prep_input thy "met_simp_poly_minus" [] Method.id_empty
34.8 + [MethodC.prep_input thy "met_simp_poly_minus" [] MethodC.id_empty
34.9 (["simplification", "for_polynomials", "with_minus"],
34.10 [("#Given" ,["Term t_t"]),
34.11 ("#Where" ,["t_t is_polyexp",
34.12 @@ -515,7 +515,7 @@
34.13 (Try (Rewrite_Set ''verschoenere'')))
34.14 ) t_t)"
34.15 setup \<open>KEStore_Elems.add_mets
34.16 - [Method.prep_input thy "met_simp_poly_parenth" [] Method.id_empty
34.17 + [MethodC.prep_input thy "met_simp_poly_parenth" [] MethodC.id_empty
34.18 (["simplification", "for_polynomials", "with_parentheses"],
34.19 [("#Given" ,["Term t_t"]),
34.20 ("#Where" ,["t_t is_polyexp"]),
34.21 @@ -540,7 +540,7 @@
34.22 (Try (Rewrite_Set ''verschoenere'')))
34.23 ) t_t)"
34.24 setup \<open>KEStore_Elems.add_mets
34.25 - [Method.prep_input thy "met_simp_poly_parenth_mult" [] Method.id_empty
34.26 + [MethodC.prep_input thy "met_simp_poly_parenth_mult" [] MethodC.id_empty
34.27 (["simplification", "for_polynomials", "with_parentheses_mult"],
34.28 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
34.29 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
34.30 @@ -550,7 +550,7 @@
34.31 @{thm simplify3.simps})]
34.32 \<close>
34.33 setup \<open>KEStore_Elems.add_mets
34.34 - [Method.prep_input thy "met_probe" [] Method.id_empty
34.35 + [MethodC.prep_input thy "met_probe" [] MethodC.id_empty
34.36 (["probe"], [],
34.37 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
34.38 errpats = [], nrls = Rule_Set.Empty},
34.39 @@ -570,7 +570,7 @@
34.40 (Try (Repeat (Calculate ''MINUS''))))
34.41 ) e_e)"
34.42 setup \<open>KEStore_Elems.add_mets
34.43 - [Method.prep_input thy "met_probe_poly" [] Method.id_empty
34.44 + [MethodC.prep_input thy "met_probe_poly" [] MethodC.id_empty
34.45 (["probe", "fuer_polynom"],
34.46 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
34.47 ("#Where" ,["e_e is_polyexp"]),
34.48 @@ -582,7 +582,7 @@
34.49 @{thm mache_probe.simps})]
34.50 \<close>
34.51 setup \<open>KEStore_Elems.add_mets
34.52 - [Method.prep_input thy "met_probe_bruch" [] Method.id_empty
34.53 + [MethodC.prep_input thy "met_probe_bruch" [] MethodC.id_empty
34.54 (["probe", "fuer_bruch"],
34.55 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
34.56 ("#Where" ,["e_e is_ratpolyexp"]),
35.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Feb 03 15:21:12 2021 +0100
35.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Feb 03 16:39:44 2021 +0100
35.3 @@ -170,7 +170,7 @@
35.4
35.5 subsection \<open>methods\<close>
35.6 setup \<open>KEStore_Elems.add_mets
35.7 - [Method.prep_input thy "met_rateq" [] Method.id_empty
35.8 + [MethodC.prep_input thy "met_rateq" [] MethodC.id_empty
35.9 (["RatEq"], [],
35.10 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
35.11 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>
35.12 @@ -188,7 +188,7 @@
35.13 in
35.14 Check_elementwise L_L {(v_v::real). Assumptions})"
35.15 setup \<open>KEStore_Elems.add_mets
35.16 - [Method.prep_input thy "met_rat_eq" [] Method.id_empty
35.17 + [MethodC.prep_input thy "met_rat_eq" [] MethodC.id_empty
35.18 (["RatEq", "solve_rat_equation"],
35.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
35.20 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
36.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Feb 03 15:21:12 2021 +0100
36.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Feb 03 16:39:44 2021 +0100
36.3 @@ -905,7 +905,7 @@
36.4 Try (Rewrite_Set ''discard_parentheses1''))
36.5 term)"
36.6 setup \<open>KEStore_Elems.add_mets
36.7 - [Method.prep_input thy "met_simp_rat" [] Method.id_empty
36.8 + [MethodC.prep_input thy "met_simp_rat" [] MethodC.id_empty
36.9 (["simplification", "of_rationals"],
36.10 [("#Given" ,["Term t_t"]),
36.11 ("#Where" ,["t_t is_ratpolyexp"]),
37.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Feb 03 15:21:12 2021 +0100
37.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Feb 03 16:39:44 2021 +0100
37.3 @@ -474,7 +474,7 @@
37.4
37.5 subsection \<open>methods\<close>
37.6 setup \<open>KEStore_Elems.add_mets
37.7 - [Method.prep_input thy "met_rooteq" [] Method.id_empty
37.8 + [MethodC.prep_input thy "met_rooteq" [] MethodC.id_empty
37.9 (["RootEq"], [],
37.10 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
37.11 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
37.12 @@ -495,7 +495,7 @@
37.13 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
37.14 [BOOL e_e, REAL v_v])"
37.15 setup \<open>KEStore_Elems.add_mets
37.16 - [Method.prep_input thy "met_rooteq_norm" [] Method.id_empty
37.17 + [MethodC.prep_input thy "met_rooteq_norm" [] MethodC.id_empty
37.18 (["RootEq", "norm_sq_root_equation"],
37.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
37.20 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
37.21 @@ -528,7 +528,7 @@
37.22 [BOOL e_e, REAL v_v])
37.23 in Check_elementwise L_L {(v_v::real). Assumptions})"
37.24 setup \<open>KEStore_Elems.add_mets
37.25 - [Method.prep_input thy "met_rooteq_sq" [] Method.id_empty
37.26 + [MethodC.prep_input thy "met_rooteq_sq" [] MethodC.id_empty
37.27 (["RootEq", "solve_sq_root_equation"],
37.28 [("#Given" ,["equality e_e", "solveFor v_v"]),
37.29 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
37.30 @@ -560,7 +560,7 @@
37.31 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
37.32 [BOOL e_e, REAL v_v])"
37.33 setup \<open>KEStore_Elems.add_mets
37.34 - [Method.prep_input thy "met_rooteq_sq_right" [] Method.id_empty
37.35 + [MethodC.prep_input thy "met_rooteq_sq_right" [] MethodC.id_empty
37.36 (["RootEq", "solve_right_sq_root_equation"],
37.37 [("#Given" ,["equality e_e", "solveFor v_v"]),
37.38 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
37.39 @@ -589,7 +589,7 @@
37.40 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
37.41 [BOOL e_e, REAL v_v])"
37.42 setup \<open>KEStore_Elems.add_mets
37.43 - [Method.prep_input thy "met_rooteq_sq_left" [] Method.id_empty
37.44 + [MethodC.prep_input thy "met_rooteq_sq_left" [] MethodC.id_empty
37.45 (["RootEq", "solve_left_sq_root_equation"],
37.46 [("#Given" ,["equality e_e", "solveFor v_v"]),
37.47 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
38.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Feb 03 15:21:12 2021 +0100
38.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Feb 03 16:39:44 2021 +0100
38.3 @@ -139,7 +139,7 @@
38.4
38.5 subsection \<open>methods\<close>
38.6 setup \<open>KEStore_Elems.add_mets
38.7 - [Method.prep_input @{theory LinEq} "met_rootrateq" [] Method.id_empty
38.8 + [MethodC.prep_input @{theory LinEq} "met_rootrateq" [] MethodC.id_empty
38.9 (["RootRatEq"], [],
38.10 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
38.11 crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]
38.12 @@ -157,7 +157,7 @@
38.13 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
38.14 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
38.15 setup \<open>KEStore_Elems.add_mets
38.16 - [Method.prep_input thy "met_rootrateq_elim" [] Method.id_empty
38.17 + [MethodC.prep_input thy "met_rootrateq_elim" [] MethodC.id_empty
38.18 (["RootRatEq", "elim_rootrat_equation"],
38.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
38.20 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
39.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed Feb 03 15:21:12 2021 +0100
39.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed Feb 03 16:39:44 2021 +0100
39.3 @@ -38,7 +38,7 @@
39.4
39.5 (** methods **)
39.6 setup \<open>KEStore_Elems.add_mets
39.7 - [Method.prep_input thy "met_tsimp" [] Method.id_empty
39.8 + [MethodC.prep_input thy "met_tsimp" [] MethodC.id_empty
39.9 (["simplification"],
39.10 [("#Given" ,["Term t_t"]),
39.11 ("#Find" ,["normalform n_n"])],
40.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Feb 03 15:21:12 2021 +0100
40.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Feb 03 16:39:44 2021 +0100
40.3 @@ -833,7 +833,7 @@
40.4 section \<open>methods\<close>
40.5 subsection \<open>differentiate\<close>
40.6 setup \<open>KEStore_Elems.add_mets
40.7 - [Method.prep_input @{theory "Diff"} "met_test" [] Method.id_empty
40.8 + [MethodC.prep_input @{theory "Diff"} "met_test" [] MethodC.id_empty
40.9 (["Test"], [],
40.10 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
40.11 crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
40.12 @@ -849,7 +849,7 @@
40.13 in
40.14 [e_e])"
40.15 setup \<open>KEStore_Elems.add_mets
40.16 - [Method.prep_input thy "met_test_solvelin" [] Method.id_empty
40.17 + [MethodC.prep_input thy "met_test_solvelin" [] MethodC.id_empty
40.18 (["Test", "solve_linear"],
40.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
40.20 ("#Where" ,["matches (?a = ?b) e_e"]),
40.21 @@ -880,7 +880,7 @@
40.22 in
40.23 [e_e])"
40.24 setup \<open>KEStore_Elems.add_mets
40.25 - [Method.prep_input thy "met_test_sqrt" [] Method.id_empty
40.26 + [MethodC.prep_input thy "met_test_sqrt" [] MethodC.id_empty
40.27 (*root-equation, version for tests before 8.01.01*)
40.28 (["Test", "sqrt-equ-test"],
40.29 [("#Given" ,["equality e_e", "solveFor v_v"]),
40.30 @@ -908,7 +908,7 @@
40.31 in
40.32 Check_elementwise L_L {(v_v::real). Assumptions})"
40.33 setup \<open>KEStore_Elems.add_mets
40.34 - [Method.prep_input thy "met_test_squ_sub" [] Method.id_empty
40.35 + [MethodC.prep_input thy "met_test_squ_sub" [] MethodC.id_empty
40.36 (*tests subproblem fixed linear*)
40.37 (["Test", "squ-equ-test-subpbl1"],
40.38 [("#Given" ,["equality e_e", "solveFor v_v"]),
40.39 @@ -940,7 +940,7 @@
40.40 in
40.41 Check_elementwise L_L {(v_v::real). Assumptions}) "
40.42 setup \<open>KEStore_Elems.add_mets
40.43 - [Method.prep_input thy "met_test_eq1" [] Method.id_empty
40.44 + [MethodC.prep_input thy "met_test_eq1" [] MethodC.id_empty
40.45 (*root-equation1:*)
40.46 (["Test", "square_equation1"],
40.47 [("#Given" ,["equality e_e", "solveFor v_v"]),
40.48 @@ -973,7 +973,7 @@
40.49 in
40.50 Check_elementwise L_L {(v_v::real). Assumptions})"
40.51 setup \<open>KEStore_Elems.add_mets
40.52 - [Method.prep_input thy "met_test_squ2" [] Method.id_empty
40.53 + [MethodC.prep_input thy "met_test_squ2" [] MethodC.id_empty
40.54 (*root-equation2*)
40.55 (["Test", "square_equation2"],
40.56 [("#Given" ,["equality e_e", "solveFor v_v"]),
40.57 @@ -1006,7 +1006,7 @@
40.58 in
40.59 Check_elementwise L_L {(v_v::real). Assumptions})"
40.60 setup \<open>KEStore_Elems.add_mets
40.61 - [Method.prep_input thy "met_test_squeq" [] Method.id_empty
40.62 + [MethodC.prep_input thy "met_test_squeq" [] MethodC.id_empty
40.63 (*root-equation*)
40.64 (["Test", "square_equation"],
40.65 [("#Given" ,["equality e_e", "solveFor v_v"]),
40.66 @@ -1032,7 +1032,7 @@
40.67 in
40.68 Or_to_List e_e)"
40.69 setup \<open>KEStore_Elems.add_mets
40.70 - [Method.prep_input thy "met_test_eq_plain" [] Method.id_empty
40.71 + [MethodC.prep_input thy "met_test_eq_plain" [] MethodC.id_empty
40.72 (*solve_plain_square*)
40.73 (["Test", "solve_plain_square"],
40.74 [("#Given",["equality e_e", "solveFor v_v"]),
40.75 @@ -1059,7 +1059,7 @@
40.76 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
40.77 [''no_met'']) [BOOL e_e, REAL v_v])"
40.78 setup \<open>KEStore_Elems.add_mets
40.79 - [Method.prep_input thy "met_test_norm_univ" [] Method.id_empty
40.80 + [MethodC.prep_input thy "met_test_norm_univ" [] MethodC.id_empty
40.81 (["Test", "norm_univar_equation"],
40.82 [("#Given",["equality e_e", "solveFor v_v"]),
40.83 ("#Where" ,[]),
40.84 @@ -1077,7 +1077,7 @@
40.85 (Try (Calculate ''PLUS'')) #>
40.86 (Try (Calculate ''TIMES''))) t_t)"
40.87 setup \<open>KEStore_Elems.add_mets
40.88 - [Method.prep_input thy "met_test_intsimp" [] Method.id_empty
40.89 + [MethodC.prep_input thy "met_test_intsimp" [] MethodC.id_empty
40.90 (["Test", "intsimp"],
40.91 [("#Given" ,["intTestGiven t_t"]),
40.92 ("#Where" ,[]),
41.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Feb 03 15:21:12 2021 +0100
41.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Feb 03 16:39:44 2021 +0100
41.3 @@ -10,7 +10,7 @@
41.4 val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree
41.5 val update_met : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =vvv= ? *)
41.6 val update_metppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =^^^= ? *)
41.7 - val update_metID : CTbasic.ctree -> Pos.pos -> Method.id -> CTbasic.ctree
41.8 + val update_metID : CTbasic.ctree -> Pos.pos -> MethodC.id -> CTbasic.ctree
41.9 val update_pbl : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =vvv= ? *)
41.10 val update_pblppc : CTbasic.ctree -> Pos.pos -> Model_Def.i_model -> CTbasic.ctree (* =^^^= ? *)
41.11 val update_pblID : CTbasic.ctree -> Pos.pos -> Problem.id -> CTbasic.ctree
42.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Feb 03 15:21:12 2021 +0100
42.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Feb 03 16:39:44 2021 +0100
42.3 @@ -43,7 +43,7 @@
42.4 val g_form : ppobj -> term
42.5 val g_pbl : ppobj -> Model_Def.i_model
42.6 val g_met : ppobj -> Model_Def.i_model
42.7 - val g_metID : ppobj -> Method.id
42.8 + val g_metID : ppobj -> MethodC.id
42.9 val g_result : ppobj -> Celem.result
42.10 val g_tac : ppobj -> Tactic.input
42.11 val g_domID : ppobj -> ThyC.id
42.12 @@ -185,8 +185,8 @@
42.13 term, (* headline of calc-head, as calculated initially(!) *)
42.14 spec : References_Def.T, (* explicitly input *)
42.15 probl : Model_Def.i_model,(* = I_Model.T for interactive input to a Problem *)
42.16 - meth : Model_Def.i_model,(* = I_Model.T for interactive input to a Method *)
42.17 - ctxt : Proof.context, (* used while specifying this (Sub-)Problem and Method *)
42.18 + meth : Model_Def.i_model,(* = I_Model.T for interactive input to a MethodC *)
42.19 + ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *)
42.20 loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *)
42.21 * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
42.22 branch: branch, (* like PrfObj *)
42.23 @@ -470,7 +470,7 @@
42.24 let
42.25 val domID = if dI = ThyC.id_empty then dI' else dI
42.26 val pblID = if pI = Problem.id_empty then pI' else pI
42.27 - val metID = if mI = Method.id_empty then mI' else mI
42.28 + val metID = if mI = MethodC.id_empty then mI' else mI
42.29 in (domID, pblID, metID) end;
42.30
42.31 (**.development for extracting an 'interval' from ptree.**)
43.1 --- a/src/Tools/isac/MathEngBasic/method.sml Wed Feb 03 15:21:12 2021 +0100
43.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Wed Feb 03 16:39:44 2021 +0100
43.3 @@ -28,7 +28,7 @@
43.4 end
43.5
43.6 (**)
43.7 -structure Method(**): METHOD(**) =
43.8 +structure MethodC(**): METHOD(**) =
43.9 struct
43.10 (**)
43.11
43.12 @@ -40,9 +40,9 @@
43.13 val id_to_string = Meth_Def.id_to_string;
43.14
43.15
43.16 -(** prepare Method for Store **)
43.17 +(** prepare MethodC for Store **)
43.18
43.19 -(* a subset of Method.T record's fields *)
43.20 +(* a subset of MethodC.T record's fields *)
43.21 type input =
43.22 {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
43.23 prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
43.24 @@ -92,7 +92,7 @@
43.25 end;
43.26
43.27
43.28 -(** get Method from Store **)
43.29 +(** get MethodC from Store **)
43.30
43.31 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
43.32 fun from_store metID = Store.get (get_mets ()) metID metID;
44.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Feb 03 15:21:12 2021 +0100
44.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Wed Feb 03 16:39:44 2021 +0100
44.3 @@ -34,12 +34,12 @@
44.4 type T = Probl_Def.T;
44.5
44.6 (*
44.7 - elements if the id are in reverse order as compared to Method:
44.8 + elements if the id are in reverse order as compared to MethodC:
44.9 e.g. ["linear", "univariate", "equation"] has "equation" as parent node --
44.10 -- this makes the id readable.
44.11 *)
44.12 type id = Probl_Def.id;
44.13 -(* same order as for Method (used in Store )*)
44.14 +(* same order as for MethodC (used in Store )*)
44.15 type id_reverse = Probl_Def.id;
44.16
44.17 val id_empty = Probl_Def.id_empty;
44.18 @@ -111,7 +111,7 @@
44.19 end;
44.20
44.21
44.22 -(** get Method from Store **)
44.23 +(** get MethodC from Store **)
44.24
44.25 fun from_store id = Store.get (get_ptyps ()) id (rev id);
44.26
45.1 --- a/src/Tools/isac/MathEngBasic/references.sml Wed Feb 03 15:21:12 2021 +0100
45.2 +++ b/src/Tools/isac/MathEngBasic/references.sml Wed Feb 03 16:39:44 2021 +0100
45.3 @@ -40,7 +40,7 @@
45.4 let
45.5 val (dI, pI, mI) = Ctree.get_obj Ctree.g_spec pt p
45.6 in
45.7 - dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
45.8 + dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
45.9 end;
45.10
45.11 (* complete References and save them to the state *)
46.1 --- a/src/Tools/isac/MathEngBasic/specification-def.sml Wed Feb 03 15:21:12 2021 +0100
46.2 +++ b/src/Tools/isac/MathEngBasic/specification-def.sml Wed Feb 03 16:39:44 2021 +0100
46.3 @@ -23,7 +23,7 @@
46.4
46.5 type T =
46.6 bool * (* I_Model.T andalso Pre_Conds.T *)
46.7 - Pos.pos_ * (* model belongs to Problem or Method *)
46.8 + Pos.pos_ * (* model belongs to Problem or MethodC *)
46.9 term * (* the headline shown on Calc.T *)
46.10 Model_Def.i_model * (* used by I_Model.T *)
46.11 Pre_Conds_Def.T * (* used by Pre_Conds.T *)
47.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Feb 03 15:21:12 2021 +0100
47.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Feb 03 16:39:44 2021 +0100
47.3 @@ -15,12 +15,12 @@
47.4 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
47.5 | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
47.6 | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
47.7 - | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model_Def.i_model
47.8 - | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
47.9 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model
47.10 + | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
47.11 | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))
47.12 | Specify_Theory' of ThyC.id
47.13 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
47.14 - | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
47.15 + | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context
47.16 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
47.17 | Check_Postcond' of Problem.id * term
47.18 | Check_elementwise' of term * TermC.as_string * Celem.result
47.19 @@ -49,11 +49,11 @@
47.20 | Model_Problem
47.21 | Refine_Problem of Problem.id
47.22 | Refine_Tacitly of Problem.id
47.23 - | Specify_Method of Method.id
47.24 + | Specify_Method of MethodC.id
47.25 | Specify_Problem of Problem.id
47.26 | Specify_Theory of ThyC.id
47.27 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
47.28 - | Apply_Method of Method.id
47.29 + | Apply_Method of MethodC.id
47.30 | Calculate of string
47.31 | Check_Postcond of Problem.id
47.32 | Check_elementwise of TermC.as_string
47.33 @@ -114,11 +114,11 @@
47.34 | Model_Problem
47.35 | Refine_Problem of Problem.id
47.36 | Refine_Tacitly of Problem.id
47.37 - | Specify_Method of Method.id
47.38 + | Specify_Method of MethodC.id
47.39 | Specify_Problem of Problem.id
47.40 | Specify_Theory of ThyC.id
47.41 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
47.42 - | Apply_Method of Method.id
47.43 + | Apply_Method of MethodC.id
47.44 | Calculate of string
47.45 | Check_Postcond of Problem.id
47.46 | Check_elementwise of TermC.as_string
47.47 @@ -307,9 +307,9 @@
47.48 Problem.id * (* the original id in the Know_Store *)
47.49 Problem.id * (* the id of the refined Problem *)
47.50 ThyC.id * (* the id of the refined theory *)
47.51 - Method.id * (* the id of the refined Method *)
47.52 + MethodC.id * (* the id of the refined MethodC *)
47.53 Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
47.54 - | Specify_Method' of Method.id * Model_Def.o_model * Model_Def.i_model
47.55 + | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
47.56 | Specify_Problem' of Problem.id *
47.57 (bool * (* all preconditions evaluate to True *)
47.58 (Model_Def.i_model * (* the model checked for the input id *)
47.59 @@ -317,7 +317,7 @@
47.60 | Specify_Theory' of ThyC.id
47.61 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
47.62 | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
47.63 - Method.id * (* id in the Know_Store *)
47.64 + MethodC.id * (* id in the Know_Store *)
47.65 term option * (* first formula in the (sub-)Problem TODO: rm option *)
47.66 Istate_Def.T * (* for starting the Program *)
47.67 Proof.context (* for starting the Program *)
47.68 @@ -373,7 +373,7 @@
47.69 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
47.70 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
47.71 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
47.72 - Method.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
47.73 + MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
47.74
47.75 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
47.76 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
48.1 --- a/src/Tools/isac/MathEngine/detail-step.sml Wed Feb 03 15:21:12 2021 +0100
48.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Wed Feb 03 16:39:44 2021 +0100
48.3 @@ -43,7 +43,7 @@
48.4 | _ =>
48.5 let
48.6 val is = Istate.init_detail tac t
48.7 - val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
48.8 + val tac_ = Tactic.Apply_Method' (MethodC.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
48.9 val pos' = ((lev_on o lev_dn) p, Frm)
48.10 val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *)
48.11 val (_,_, (pt'', _)) = Solve.complete_solve Solve.CompleteSubpbl [] (pt', pos')
49.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Feb 03 15:21:12 2021 +0100
49.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Feb 03 16:39:44 2021 +0100
49.3 @@ -30,8 +30,8 @@
49.4 val thy' = get_obj g_domID pt pp;
49.5 val thy = ThyC.get_theory thy';
49.6 val metID = get_obj g_metID pt pp;
49.7 - val metID' = if metID = Method.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
49.8 - val (sc, srls) = (case Method.from_store metID' of
49.9 + val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
49.10 + val (sc, srls) = (case MethodC.from_store metID' of
49.11 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
49.12 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
49.13 val ctxt = get_ctxt pt (p, p_)
49.14 @@ -53,10 +53,10 @@
49.15 val thy = ThyC.get_theory thy'
49.16 val metID = get_obj g_metID pt pp
49.17 val metID' =
49.18 - if metID = Method.id_empty
49.19 + if metID = MethodC.id_empty
49.20 then (thd3 o snd3) (get_obj g_origin pt pp)
49.21 else metID
49.22 - val (sc, srls, erls, ro) = (case Method.from_store metID' of
49.23 + val (sc, srls, erls, ro) = (case MethodC.from_store metID' of
49.24 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
49.25 | _ => raise ERROR "specific_from_prog 1")
49.26 val (env, (a, v)) = (case get_istate_LI pt (p, p_) of
50.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Feb 03 15:21:12 2021 +0100
50.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Feb 03 16:39:44 2021 +0100
50.3 @@ -12,9 +12,9 @@
50.4
50.5 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T * Pre_Conds.T
50.6 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * Pre_Conds.T
50.7 - val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * I_Model.T * Pre_Conds.T
50.8 + val context_met : MethodC.id -> Ctree.ctree -> Pos.pos -> bool * MethodC.id * Program.T * I_Model.T * Pre_Conds.T
50.9 val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
50.10 - val set_method : Method.id -> Calc.T -> Ctree.ctree * SpecificationC.T
50.11 + val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
50.12 val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T
50.13 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
50.14 val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
50.15 @@ -159,10 +159,10 @@
50.16 case Ctree.get_obj I pt p of
50.17 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
50.18 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case"
50.19 - val metID = if mI' = Method.id_empty
50.20 + val metID = if mI' = MethodC.id_empty
50.21 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
50.22 else mI'
50.23 - val {ppc, pre, prls, scr, ...} = Method.from_store metID
50.24 + val {ppc, pre, prls, scr, ...} = MethodC.from_store metID
50.25 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
50.26 in
50.27 (model_ok, metID, scr, pbl, pre)
50.28 @@ -187,7 +187,7 @@
50.29 case Ctree.get_obj I pt p of
50.30 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
50.31 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
50.32 - val {ppc,pre,prls,scr,...} = Method.from_store mI
50.33 + val {ppc,pre,prls,scr,...} = MethodC.from_store mI
50.34 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
50.35 in
50.36 (model_ok, mI, scr, pbl, pre)
51.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Wed Feb 03 15:21:12 2021 +0100
51.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Wed Feb 03 16:39:44 2021 +0100
51.3 @@ -24,10 +24,10 @@
51.4 fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ...}) Pos.Met =
51.5 let
51.6 val (_, _, metID) = Ctree.get_somespec' spec spec'
51.7 - val pre = if metID = Method.id_empty then []
51.8 + val pre = if metID = MethodC.id_empty then []
51.9 else
51.10 let
51.11 - val {prls, pre= where_, ...} = Method.from_store metID
51.12 + val {prls, pre= where_, ...} = MethodC.from_store metID
51.13 val (_, pre) = Pre_Conds.check prls where_ meth 0
51.14 in pre end
51.15 val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 pre))
52.1 --- a/src/Tools/isac/Specify/cas-command.sml Wed Feb 03 15:21:12 2021 +0100
52.2 +++ b/src/Tools/isac/Specify/cas-command.sml Wed Feb 03 16:39:44 2021 +0100
52.3 @@ -14,7 +14,7 @@
52.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
52.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
52.6 val input_: References.T -> (term * term list) list ->
52.7 - Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context
52.8 + Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context
52.9
52.10 val dtss2itm_: Model_Pattern.T -> term * term list ->
52.11 int list * bool * string * I_Model.feedback (*I_Model.single'*)
52.12 @@ -57,7 +57,7 @@
52.13 case Refine.problem thy pI pits of
52.14 SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
52.15 | NONE => (pI, (hd o #met o Problem.from_store) pI)
52.16 - val {ppc, pre, prls, ...} = Method.from_store mI
52.17 + val {ppc, pre, prls, ...} = MethodC.from_store mI
52.18 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
52.19 val its = O_Model.add_id its_
52.20 val mits = map flattup2 its
53.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Feb 03 15:21:12 2021 +0100
53.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Feb 03 16:39:44 2021 +0100
53.3 @@ -309,7 +309,7 @@
53.4 end)
53.5 end
53.6 end
53.7 - (* for Method: #undef completed vvvvv vvvvvv term_as_string *)
53.8 + (* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
53.9 | check_single ctxt m_field o_model i_model m_patt str =
53.10 case TermC.parseNEW ctxt str of
53.11 NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")
54.1 --- a/src/Tools/isac/Specify/o-model.sml Wed Feb 03 15:21:12 2021 +0100
54.2 +++ b/src/Tools/isac/Specify/o-model.sml Wed Feb 03 16:39:44 2021 +0100
54.3 @@ -10,7 +10,7 @@
54.4 \<open>O_Model\<close> serves efficiency of student's interactive modelling via \<open>I_Model\<close>.
54.5
54.6 \<open>O_Model\<close> marks elements with \<open>m_field\<close> \<open>#undef\<close>, which are not required by the \<open>Model_Pattern\<close>
54.7 -of the \<open>Problem\<close> or the \<open>Method\<close> .. TODO redes: \<open>m_field\<close> probably different in root..Subproblem
54.8 +of the \<open>Problem\<close> or the \<open>MethodC\<close> .. TODO redes: \<open>m_field\<close> probably different in root..Subproblem
54.9
54.10 TODO: revise with an example with more than 1 variant.
54.11 + consider: drop m_field ?
55.1 --- a/src/Tools/isac/Specify/p-spec.sml Wed Feb 03 15:21:12 2021 +0100
55.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Feb 03 16:39:44 2021 +0100
55.3 @@ -49,7 +49,7 @@
55.4 type record = {thy_id: ThyC.id, pbl_id: Problem.id, (* headline of Problem *)
55.5 givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T *)
55.6 find: TermC.as_string, relates: TermC.as_string list,
55.7 - rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: Method.id} (* References.T *)
55.8 + rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id} (* References.T *)
55.9
55.10 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
55.11
55.12 @@ -67,7 +67,7 @@
55.13 Pos.pos' * (* the position in Ctree *)
55.14 TermC.as_string * (* the headline shown on Calc.T *)
55.15 imodel * (* the model *)
55.16 - Pos.pos_ * (* model belongs to Problem or Method *)
55.17 + Pos.pos_ * (* model belongs to Problem or MethodC *)
55.18 References.T; (* into Know_Store *)
55.19 val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
55.20
55.21 @@ -228,7 +228,7 @@
55.22 in (Pos.Pbl, appl_adds dI' oris probl pbt
55.23 (map itms2fstr probl), meth) end
55.24 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
55.25 - then let val met = (#ppc o Method.from_store) mI
55.26 + then let val met = (#ppc o MethodC.from_store) mI
55.27 val mits = I_Model.complete oris probl meth met
55.28 in if foldl and_ (true, map #3 mits)
55.29 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
55.30 @@ -243,7 +243,7 @@
55.31 in (Ctree.update_pbl pt p pits,
55.32 (SpecificationC.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)
55.33 end
55.34 - else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
55.35 + else let val {prls,pre,...} = MethodC.from_store (#3 (References.select ospec spec))
55.36 val (_, pre) = Pre_Conds.check prls pre mits 0
55.37 in (Ctree.update_met pt p mits,
55.38 (SpecificationC.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
56.1 --- a/src/Tools/isac/Specify/specification.sml Wed Feb 03 15:21:12 2021 +0100
56.2 +++ b/src/Tools/isac/Specify/specification.sml Wed Feb 03 16:39:44 2021 +0100
56.3 @@ -64,7 +64,7 @@
56.4 I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
56.5 val reset: Calc.T -> Calc.T
56.6
56.7 - val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
56.8 + val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * MethodC.id -> bool
56.9 val is_complete: Calc.T -> bool
56.10
56.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
56.12 @@ -84,7 +84,7 @@
56.13 fun complete its pre (dI, pI, mI) =
56.14 foldl and_ (true, map #3 (its: I_Model.T)) andalso
56.15 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
56.16 - dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
56.17 + dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
56.18
56.19 fun get_data (pt, (p, _)) =
56.20 case Ctree.get_obj I pt p of
56.21 @@ -119,7 +119,7 @@
56.22 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
56.23 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
56.24 | _ => raise ERROR "get Met: uncovered case get_obj"
56.25 - val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
56.26 + val {prls, pre, ...} = MethodC.from_store (#3 (References.select ospec spec))
56.27 val (_, pre) = Pre_Conds.check prls pre meth 0
56.28 in
56.29 (complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
57.1 --- a/src/Tools/isac/Specify/specify-step.sml Wed Feb 03 15:21:12 2021 +0100
57.2 +++ b/src/Tools/isac/Specify/specify-step.sml Wed Feb 03 16:39:44 2021 +0100
57.3 @@ -10,7 +10,7 @@
57.4 val check: Tactic.input -> Calc.T -> Applicable.T
57.5 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
57.6
57.7 - val complete_for: Method.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
57.8 + val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
57.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
57.10 (*NONE*)
57.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
57.12 @@ -28,7 +28,7 @@
57.13 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
57.14 ...} = Calc.specify_data (ctree, pos);
57.15 val (dI, _, _) = References.select o_refs refs;
57.16 - val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
57.17 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
57.18 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
57.19 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
57.20 val thy = ThyC.get_theory dI
57.21 @@ -80,7 +80,7 @@
57.22 in
57.23 case Refine.refine_ori oris pI of
57.24 SOME pblID =>
57.25 - Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [(*filled later*)]))
57.26 + Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, MethodC.id_empty, [(*filled later*)]))
57.27 | NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Tacitly pI) ^ " not applicable")
57.28 end
57.29 | check (Tactic.Specify_Method mID) (ctree, pos) =
58.1 --- a/src/Tools/isac/Specify/specify.sml Wed Feb 03 15:21:12 2021 +0100
58.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Feb 03 16:39:44 2021 +0100
58.3 @@ -79,9 +79,9 @@
58.4 fun for_problem oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
58.5 let
58.6 val cpI = if pI = Problem.id_empty then pI' else pI;
58.7 - val cmI = if mI = Method.id_empty then mI' else mI;
58.8 + val cmI = if mI = MethodC.id_empty then mI' else mI;
58.9 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
58.10 - val {ppc = mpc, ...} = Method.from_store cmI
58.11 + val {ppc = mpc, ...} = MethodC.from_store cmI
58.12 val (preok, _) = Pre_Conds.check prls where_ pbl 0;
58.13 in
58.14 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
58.15 @@ -100,7 +100,7 @@
58.16 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
58.17 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
58.18 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
58.19 - else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
58.20 + else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
58.21 else
58.22 case find_first (I_Model.is_error o #5) met of
58.23 SOME (_, _, _, fd, itm_) =>
58.24 @@ -114,8 +114,8 @@
58.25
58.26 fun for_method oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
58.27 let
58.28 - val cmI = if mI = Method.id_empty then mI' else mI;
58.29 - val {ppc = mpc, prls, pre, ...} = Method.from_store cmI; (*..Method ?*)
58.30 + val cmI = if mI = MethodC.id_empty then mI' else mI;
58.31 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store cmI; (*..MethodC ?*)
58.32 val (preok, _) = Pre_Conds.check prls pre pbl 0;
58.33 in
58.34 (case find_first (I_Model.is_error o #5) met of
58.35 @@ -163,7 +163,7 @@
58.36 val (i_model, m_patt) =
58.37 if p_ = Pos.Met then
58.38 (met,
58.39 - (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
58.40 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
58.41 else
58.42 (pbl,
58.43 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store |> #ppc)
58.44 @@ -192,7 +192,7 @@
58.45 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
58.46 | _ => raise ERROR "finish_phase: unvered case get_obj"
58.47 val (_, pI, mI) = References.select ospec spec
58.48 - val mpc = (#ppc o Method.from_store) mI
58.49 + val mpc = (#ppc o MethodC.from_store) mI
58.50 val ppc = (#ppc o Problem.from_store) pI
58.51 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
58.52 val pt = Ctree.update_pblppc pt p pits
58.53 @@ -209,7 +209,7 @@
58.54 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
58.55 => (pors, dI, pI, mI)
58.56 | _ => raise ERROR "do_all: uncovered case get_obj"
58.57 - val {ppc, ...} = Method.from_store mI
58.58 + val {ppc, ...} = MethodC.from_store mI
58.59 val (_, vals) = O_Model.values' pors
58.60 val ctxt = ContextC.initialise dI vals
58.61 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
59.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Feb 03 15:21:12 2021 +0100
59.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Feb 03 16:39:44 2021 +0100
59.3 @@ -34,7 +34,7 @@
59.4 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
59.5 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
59.6 val (_, pI, mI) = References.select ospec spec
59.7 - val mpc = (#ppc o Method.from_store) mI (* just for reuse I_Model.complete_method *)
59.8 + val mpc = (#ppc o MethodC.from_store) mI (* just for reuse I_Model.complete_method *)
59.9 val {cas, ppc, ...} = Problem.from_store pI
59.10 val pbl = I_Model.init ppc (* fill in descriptions *)
59.11 (*----------------if you think, this should be done by the Dialog
59.12 @@ -52,7 +52,7 @@
59.13 | by_tactic_input (Tactic.Add_Find ct) ptp = Specify.by_Add_ "#Find" ct ptp
59.14 | by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_Add_"#Relate" ct ptp
59.15
59.16 - (* called with Method.id_empty *)
59.17 + (* called with MethodC.id_empty *)
59.18 | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
59.19 let
59.20 val (oris, dI, ctxt) = case get_obj I pt p of
59.21 @@ -65,7 +65,7 @@
59.22 let
59.23 val {met, ...} = Problem.from_store pI'
59.24 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
59.25 - val mI = if length met = 0 then Method.id_empty else hd met
59.26 + val mI = if length met = 0 then MethodC.id_empty else hd met
59.27 val (pos, c, _, pt) =
59.28 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
59.29 in
59.30 @@ -155,7 +155,7 @@
59.31 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
59.32 let
59.33 val {met, thy,...} = Problem.from_store pIre
59.34 - val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)
59.35 + val (domID, metID) = (Context.theory_name thy, if length met = 0 then MethodC.id_empty else hd met)
59.36 val ((p,_), _, _, pt) =
59.37 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
59.38 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
59.39 @@ -294,7 +294,7 @@
59.40 if mI <> []
59.41 then (* from met-browser *)
59.42 let
59.43 - val {ppc, ...} = Method.from_store mI
59.44 + val {ppc, ...} = MethodC.from_store mI
59.45 val dI = if dI = "" then "Isac_Knowledge" else dI
59.46 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
59.47 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
60.1 --- a/src/Tools/isac/Specify/test-out.sml Wed Feb 03 15:21:12 2021 +0100
60.2 +++ b/src/Tools/isac/Specify/test-out.sml Wed Feb 03 16:39:44 2021 +0100
60.3 @@ -7,7 +7,7 @@
60.4
60.5 signature TEST_OUTPUT =
60.6 sig
60.7 - datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
60.8 + datatype pblmet = MethodC of MethodC.id | Problem of Problem.id | Upblmet
60.9 datatype mout =
60.10 EmptyMout
60.11 | Error' of string
60.12 @@ -34,9 +34,9 @@
60.13 datatype pblmet =
60.14 Upblmet
60.15 | Problem of Problem.id
60.16 -| Method of Method.id;
60.17 +| MethodC of MethodC.id;
60.18 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
60.19 - | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)
60.20 + | pblmet2str (MethodC metID) = "MethodC " ^ MethodC.id_to_string metID (*%^%*)
60.21 | pblmet2str x = raise ERROR ("pblmet2str: uncovered definition " ^ pblmet2str x)
60.22
60.23 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
61.1 --- a/src/Tools/isac/Test_Code/test-code.sml Wed Feb 03 15:21:12 2021 +0100
61.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Feb 03 16:39:44 2021 +0100
61.3 @@ -46,7 +46,7 @@
61.4 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
61.5 Test_Out.PpcKF (
61.6 (case p_ of Pos.Pbl => Test_Out.Problem []
61.7 - | Pos.Met => Test_Out.Method []
61.8 + | Pos.Met => Test_Out.MethodC []
61.9 | _ => raise ERROR "TESTg_form: uncovered case",
61.10 P_Model.from (ThyC.get_theory"Isac_Knowledge") gfr pre))
61.11 end
62.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Wed Feb 03 15:21:12 2021 +0100
62.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Wed Feb 03 16:39:44 2021 +0100
62.3 @@ -10,7 +10,7 @@
62.4
62.5 (*----START----Example Function Declaration from Rationals.thy----*)
62.6
62.7 -text\<open>Define Method name and input, output types\<close>
62.8 +text\<open>Define MethodC name and input, output types\<close>
62.9
62.10 consts
62.11 get_denominator :: "real => real"
62.12 @@ -32,7 +32,7 @@
62.13 \<close>
62.14 (*----END----Example Function Decleration from Rationals.thy----*)
62.15
62.16 -text\<open>Apply the Method to an expression.\<close>
62.17 +text\<open>Apply the MethodC to an expression.\<close>
62.18
62.19 ML\<open>
62.20 val input = Thm.term_of (the (TermC.parse thy "get_denominator ((a + b) / c)"));
63.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Feb 03 15:21:12 2021 +0100
63.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Feb 03 16:39:44 2021 +0100
63.3 @@ -513,7 +513,7 @@
63.4 the original \emph{srls}.\\
63.5
63.6 \begin{verbatim}
63.7 - val {srls,...} = Method.from_store ["SignalProcessing",
63.8 + val {srls,...} = MethodC.from_store ["SignalProcessing",
63.9 "Z_Transform",
63.10 "Inverse"];
63.11 \end{verbatim}
63.12 @@ -858,7 +858,7 @@
63.13 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
63.14 \<close>
63.15
63.16 -section \<open>Implement the Specification and the Method \label{spec-meth}\<close>
63.17 +section \<open>Implement the Specification and the MethodC \label{spec-meth}\<close>
63.18
63.19 text\<open>\noindent Now everything we need for solving the problem has been
63.20 tested out. We now start by creating new nodes for our methods and
63.21 @@ -904,7 +904,7 @@
63.22 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
63.23 \<close>
63.24
63.25 -subsection \<open>Define Name and Signature for the Method\<close>
63.26 +subsection \<open>Define Name and Signature for the MethodC\<close>
63.27
63.28 text\<open>\noindent As a next step we store the definition of our new method as a
63.29 constant for the interpreter.\<close>
63.30 @@ -913,7 +913,7 @@
63.31 InverseZTransform :: "[bool, bool] => bool"
63.32 ("((Program InverseZTransform (_ =))// (_))" 9)
63.33
63.34 -subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
63.35 +subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}\<close>
63.36
63.37 text\<open>\noindent Again we have to generate the nodes step by step, first the
63.38 parent node and then the originally \em Z\_Transformation
63.39 @@ -921,12 +921,12 @@
63.40 as content.\<close>
63.41
63.42 setup \<open>KEStore_Elems.add_mets
63.43 - [Method.prep_input thy "met_SP" [] e_metID
63.44 + [MethodC.prep_input thy "met_SP" [] e_metID
63.45 (["SignalProcessing"], [],
63.46 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
63.47 errpats = [], nrls = Rule_Set.empty},
63.48 "empty_script"),
63.49 - Method.prep_input thy "met_SP_Ztrans" [] e_metID
63.50 + MethodC.prep_input thy "met_SP_Ztrans" [] e_metID
63.51 (["SignalProcessing", "Z_Transform"], [],
63.52 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
63.53 errpats = [], nrls = Rule_Set.empty},
63.54 @@ -938,7 +938,7 @@
63.55 of the script in e.g. the in- and output.\<close>
63.56
63.57 setup \<open>KEStore_Elems.add_mets
63.58 - [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
63.59 + [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
63.60 (["SignalProcessing", "Z_Transform", "Inverse"],
63.61 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
63.62 ("#Find", ["stepResponse n_eq"])],
63.63 @@ -952,7 +952,7 @@
63.64 simple operation.\<close>
63.65
63.66 setup \<open>KEStore_Elems.add_mets
63.67 - [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
63.68 + [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
63.69 (["SignalProcessing", "Z_Transform", "Inverse"],
63.70 [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
63.71 ("#Find", ["stepResponse n_eq"])],
63.72 @@ -974,7 +974,7 @@
63.73 the hierarchy.\<close>
63.74
63.75 ML \<open>
63.76 - Method.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
63.77 + MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
63.78 \<close>
63.79
63.80 section \<open>Program in TP-based language \label{prog-steps}\<close>
63.81 @@ -1122,7 +1122,7 @@
63.82 subversion.\<close>
63.83
63.84 setup \<open>KEStore_Elems.add_mets
63.85 - [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
63.86 + [MethodC.prep_input thy "met_SP_Ztrans_inv" [] e_metID
63.87 (["SignalProcessing", "Z_Transform", "Inverse"],
63.88 [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
63.89 ("#Find", ["stepResponse n_eq"])],
63.90 @@ -1231,7 +1231,7 @@
63.91 ) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
63.92
63.93 val Prog sc
63.94 - = (#scr o Method.from_store) ["SignalProcessing",
63.95 + = (#scr o MethodC.from_store) ["SignalProcessing",
63.96 "Z_Transform",
63.97 "Inverse"];
63.98 atomty sc;
63.99 @@ -1307,7 +1307,7 @@
63.100 arguments in the arguments\ldots
63.101 \begin{verbatim}
63.102 val Prog s =
63.103 - (#scr o Method.from_store) ["SignalProcessing",
63.104 + (#scr o MethodC.from_store) ["SignalProcessing",
63.105 "Z_Transform",
63.106 "Inverse"];
63.107 writeln (UnparseC.term s);
63.108 @@ -1591,7 +1591,7 @@
63.109 parse-tree of the program with {\sisac}'s specific debug tools:
63.110 \begin{verbatim}
63.111 val {scr = Prog t,...} =
63.112 - Method.from_store ["simplification",
63.113 + MethodC.from_store ["simplification",
63.114 "of_rationals",
63.115 "to_partial_fraction"];
63.116 atomty_thy @{theory "Inverse_Z_Transform"} t ;
64.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/antiquote_setup.ML Wed Feb 03 15:21:12 2021 +0100
64.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/antiquote_setup.ML Wed Feb 03 16:39:44 2021 +0100
64.3 @@ -179,7 +179,7 @@
64.4 val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command";
64.5 val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword";
64.6 val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element";
64.7 -val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
64.8 +val _ = entity_antiqs (thy_check MethodC.intern MethodC.defined) "" "method";
64.9 val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
64.10 val _ = entity_antiqs no_check "" "fact";
64.11 val _ = entity_antiqs no_check "" "variable";
65.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Feb 03 15:21:12 2021 +0100
65.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Feb 03 16:39:44 2021 +0100
65.3 @@ -1002,7 +1002,7 @@
65.4 the original \emph{srls}.\\
65.5
65.6 \begin{verbatim}
65.7 - val {srls,...} = Method.from_store ["SignalProcessing",
65.8 + val {srls,...} = MethodC.from_store ["SignalProcessing",
65.9 "Z_Transform",
65.10 "Inverse"];
65.11 \end{verbatim}
65.12 @@ -1483,9 +1483,9 @@
65.13 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
65.14 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.15 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.16 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ Specify{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.17 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ Specify{\isaliteral{5F}{\isacharunderscore}}MethodC{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.18 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.19 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.20 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}MethodC{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.21 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.22 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Rewrite\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{2E}{\isachardot}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.23 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.24 @@ -1504,7 +1504,7 @@
65.25 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
65.26 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
65.27 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
65.28 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.29 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}MethodC\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.30 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.31 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set{\isaliteral{5F}{\isacharunderscore}}Inst{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}bdv{\isaliteral{2C}{\isacharcomma}}A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}d{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}simplify{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.32 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}fa{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.33 @@ -1645,7 +1645,7 @@
65.34 %
65.35 \endisadelimML
65.36 %
65.37 -\isamarkupsection{Implement the Specification and the Method \label{spec-meth}%
65.38 +\isamarkupsection{Implement the Specification and the MethodC \label{spec-meth}%
65.39 }
65.40 \isamarkuptrue%
65.41 %
65.42 @@ -1737,7 +1737,7 @@
65.43 %
65.44 \endisadelimML
65.45 %
65.46 -\isamarkupsubsection{Define Name and Signature for the Method%
65.47 +\isamarkupsubsection{Define Name and Signature for the MethodC%
65.48 }
65.49 \isamarkuptrue%
65.50 %
65.51 @@ -1750,7 +1750,7 @@
65.52 \isanewline
65.53 \ \ InverseZTransform\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}bool{\isaliteral{2C}{\isacharcomma}}\ bool{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
65.54 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{9}}{\isaliteral{29}{\isacharparenright}}%
65.55 -\isamarkupsubsection{Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}%
65.56 +\isamarkupsubsection{Setup Parent Nodes in Hierarchy of MethodC\label{sec:cparentnode}%
65.57 }
65.58 \isamarkuptrue%
65.59 %
65.60 @@ -2342,9 +2342,9 @@
65.61 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.62 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.63 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.64 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Specify{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.65 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Specify{\isaliteral{5F}{\isacharunderscore}}MethodC{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.66 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.67 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Apply{\isaliteral{5F}{\isacharunderscore}}Method{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.68 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Apply{\isaliteral{5F}{\isacharunderscore}}MethodC{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.69 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.70 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Rewrite\ {\isaliteral{28}{\isacharparenleft}}ruleZY{\isaliteral{2C}{\isacharcomma}}\ Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{2E}{\isachardot}}ruleZY{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.71 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.72 @@ -2391,7 +2391,7 @@
65.73 arguments in the arguments\ldots
65.74 \begin{verbatim}
65.75 val Prog s =
65.76 - (#scr o Method.from_store) ["SignalProcessing",
65.77 + (#scr o MethodC.from_store) ["SignalProcessing",
65.78 "Z_Transform",
65.79 "Inverse"];
65.80 writeln (UnparseC.term s);
65.81 @@ -2505,9 +2505,9 @@
65.82 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
65.83 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}abcFormula{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.84 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.85 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}PolyEq{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abc{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.86 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}MethodC\ {\isaliteral{5B}{\isacharbrackleft}}PolyEq{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abc{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.87 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
65.88 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}PolyEq{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abc{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.89 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}MethodC\ {\isaliteral{5B}{\isacharbrackleft}}PolyEq{\isaliteral{2C}{\isacharcomma}}solve{\isaliteral{5F}{\isacharunderscore}}d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abc{\isaliteral{5F}{\isacharunderscore}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.90 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.91 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set{\isaliteral{5F}{\isacharunderscore}}Inst\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}bdv{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ d{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}polyeq{\isaliteral{5F}{\isacharunderscore}}abcFormula{\isaliteral{5F}{\isacharunderscore}}simplify{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.92 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.93 @@ -2529,9 +2529,9 @@
65.94 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.95 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Problem\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.96 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.97 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.98 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Specify{\isaliteral{5F}{\isacharunderscore}}MethodC\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.99 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.100 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}Method\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.101 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Apply{\isaliteral{5F}{\isacharunderscore}}MethodC\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}normalise{\isaliteral{5F}{\isacharunderscore}}poly{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.102 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.103 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Rewrite\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}PolyEq{\isaliteral{2E}{\isachardot}}all{\isaliteral{5F}{\isacharunderscore}}left{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
65.104 \ \ val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
65.105 @@ -2698,7 +2698,7 @@
65.106 parse-tree of the program with {\sisac}'s specific debug tools:
65.107 \begin{verbatim}
65.108 val {scr = Prog t,...} =
65.109 - Method.from_store ["simplification",
65.110 + MethodC.from_store ["simplification",
65.111 "of_rationals",
65.112 "to_partial_fraction"];
65.113 atomty_thy @ { theory } t ;
66.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Wed Feb 03 15:21:12 2021 +0100
66.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Wed Feb 03 16:39:44 2021 +0100
66.3 @@ -43,7 +43,7 @@
66.4 \<close>
66.5 ML \<open>
66.6 Test_Tool.show_mets ();
66.7 -Method.from_store ["simplification", "for_polynomials", "with_minus"];
66.8 +MethodC.from_store ["simplification", "for_polynomials", "with_minus"];
66.9 \<close>
66.10 text \<open>For a readable format of the method look up the definition in
66.11 ~~/Tools/isac/Knowledge/PolyMinus.thy or
67.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Wed Feb 03 15:21:12 2021 +0100
67.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Wed Feb 03 16:39:44 2021 +0100
67.3 @@ -24,9 +24,9 @@
67.4
67.5 fun met_select_guh pbt =
67.6 let
67.7 - val {guh, ...} = (pbt: Method.T)
67.8 + val {guh, ...} = (pbt: MethodC.T)
67.9 in guh end;
67.10 -met_select_guh: Method.T -> Check_Unique.id;(**)
67.11 +met_select_guh: MethodC.T -> Check_Unique.id;(**)
67.12
67.13 (*------- hint: build higher order functions be replacing the selector by a variable argument *)
67.14 (* collect*)
67.15 @@ -40,7 +40,7 @@
67.16
67.17 collect: ('a -> 'b) -> 'a Store.T -> 'b list;
67.18 collect pbl_select_guh: Problem.T Store.T -> Check_Unique.id list;
67.19 -collect met_select_guh: Method.T Store.T -> Check_Unique.id list;
67.20 +collect met_select_guh: MethodC.T Store.T -> Check_Unique.id list;
67.21
67.22 fun message select store guh =
67.23 if member op = (select store) guh
67.24 @@ -51,10 +51,10 @@
67.25
67.26 message: ('a -> Check_Unique.id list ) -> 'a -> Check_Unique.id -> unit;
67.27 (message (collect pbl_select_guh)): Problem.T Store.T -> Check_Unique.id -> unit;
67.28 -(message (collect met_select_guh)): Method.T Store.T -> Check_Unique.id -> unit;
67.29 +(message (collect met_select_guh)): MethodC.T Store.T -> Check_Unique.id -> unit;
67.30
67.31 (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)): Problem.T Store.T -> Check_Unique.id list;
67.32 -(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)): Method.T Store.T -> Check_Unique.id list;
67.33 +(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)): MethodC.T Store.T -> Check_Unique.id list;
67.34
67.35 val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id));
67.36 check_pblguh_unique: Problem.T Store.T -> Check_Unique.id -> unit
68.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Wed Feb 03 15:21:12 2021 +0100
68.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Wed Feb 03 16:39:44 2021 +0100
68.3 @@ -230,7 +230,7 @@
68.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
68.5 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
68.6 val parent_pos = par_pblobj pt p
68.7 - val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
68.8 + val {scr, ...} = MethodC.from_store (get_obj g_metID pt parent_pos);
68.9 val prog_res =
68.10 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
68.11 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
69.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Wed Feb 03 15:21:12 2021 +0100
69.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Wed Feb 03 16:39:44 2021 +0100
69.3 @@ -96,7 +96,7 @@
69.4 "-------- build fun for_bdv --------------------------------------------------";
69.5 Subst.program_to_input: Subst.program -> string list;
69.6
69.7 -val {scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"];
69.8 +val {scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"];
69.9 val env = [(str2term "v_v", str2term "x")] : Subst.T;
69.10
69.11 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);
70.1 --- a/test/Tools/isac/BridgeJEdit/parseC.sml Wed Feb 03 15:21:12 2021 +0100
70.2 +++ b/test/Tools/isac/BridgeJEdit/parseC.sml Wed Feb 03 16:39:44 2021 +0100
70.3 @@ -505,7 +505,7 @@
70.4 Parse.$$$ "," --
70.5 (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Problem.id *) --
70.6 Parse.$$$ "," --
70.7 - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Method.id *) --
70.8 + (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* MethodC.id *) --
70.9 Parse.$$$ ")" (* end Formalise.spec *) --
70.10 Parse.$$$ ")";
70.11
71.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Feb 03 15:21:12 2021 +0100
71.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Feb 03 16:39:44 2021 +0100
71.3 @@ -264,14 +264,14 @@
71.4 Model_Problem: Tactic.input;
71.5 Or_to_List: Tactic.input;
71.6
71.7 -Apply_Method: Method.id -> Tactic.input;
71.8 +Apply_Method: MethodC.id -> Tactic.input;
71.9 Refine_Tacitly: Problem.id -> Tactic.input;
71.10 Specify_Problem: Problem.id -> Tactic.input;
71.11 -Specify_Method: Method.id -> Tactic.input;
71.12 +Specify_Method: MethodC.id -> Tactic.input;
71.13 Substitute: Subst.input -> Tactic.input;; (* Substitute: sube -> tac; Subst.string_eqs_empty: TermC.as_string list; UNCLEAR HOW TO INPUT *)
71.14 Check_Postcond: Problem.id -> Tactic.input;
71.15
71.16 -Apply_Method: Method.id -> Tactic.input;
71.17 +Apply_Method: MethodC.id -> Tactic.input;
71.18 val tac = Apply_Method(["test", "equation", "simplify"]);
71.19 xml_of_tac tac;(*
71.20 <STRINGLISTTACTIC name="Apply_Method">
72.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Feb 03 15:21:12 2021 +0100
72.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Feb 03 16:39:44 2021 +0100
72.3 @@ -78,7 +78,7 @@
72.4
72.5 " <METHODS>\n"^
72.6 " <KESTOREREF>\n"^
72.7 - " <TAG> Method</TAG>\n"^
72.8 + " <TAG> MethodC</TAG>\n"^
72.9 " <ID> [IntegrierenUndKonstanteBestimmen2] </ID>\n"^
72.10 " <GUH> met_biege_2 </GUH>\n"^
72.11 " </KESTOREREF>\n"^
72.12 @@ -127,7 +127,7 @@
72.13 "~~~~~ fun node, args:"; val (pa: Pbl_Met_Hierarchy.filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);
72.14 val po' = lev_on po;
72.15 wfn (*= pbl2file*)
72.16 -"~~~~~ fun pbl2file, args:"; val ((path:Pbl_Met_Hierarchy.filepath), (pos:pos), (id: Method.id), (pbl as {guh,...})) =
72.17 +"~~~~~ fun pbl2file, args:"; val ((path:Pbl_Met_Hierarchy.filepath), (pos:pos), (id: MethodC.id), (pbl as {guh,...})) =
72.18 (pa, po', (ids@[id]), n);
72.19 strs2str id = "[\"e_pblID\"]"; (*true*)
72.20 pos2str pos = "[1]"; (*true*)
72.21 @@ -166,7 +166,7 @@
72.22
72.23 insert_errpats ["diff", "differentiate_on_R"] errpatstest;
72.24
72.25 -val {errpats, ...} = Method.from_store ["diff", "differentiate_on_R"];
72.26 +val {errpats, ...} = MethodC.from_store ["diff", "differentiate_on_R"];
72.27 case errpats of
72.28 ("chain-rule-diff-both", _, _) :: _ => ()
72.29 | _ => error "insert_errpats chain-rule-diff-both changed";
73.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Feb 03 15:21:12 2021 +0100
73.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Feb 03 16:39:44 2021 +0100
73.3 @@ -195,7 +195,7 @@
73.4
73.5 Step_Solve.by_tactic m (pt, p);
73.6 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
73.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
73.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
73.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
73.10 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
73.11 val Safe_Step (istate, _, tac) =
74.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Wed Feb 03 15:21:12 2021 +0100
74.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Feb 03 16:39:44 2021 +0100
74.3 @@ -47,9 +47,9 @@
74.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
74.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
74.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
74.7 - val Prog sc = (#scr o Method.from_store) ["Test", "squ-equ-test-subpbl1"];
74.8 + val Prog sc = (#scr o MethodC.from_store) ["Test", "squ-equ-test-subpbl1"];
74.9 (writeln o UnparseC.term) sc;
74.10 - val Prog sc = (#scr o Method.from_store) ["Test", "solve_linear"];
74.11 + val Prog sc = (#scr o MethodC.from_store) ["Test", "solve_linear"];
74.12 (writeln o UnparseC.term) sc;
74.13
74.14 reset_states ();
74.15 @@ -984,7 +984,7 @@
74.16 val (res, inf) =
74.17 (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
74.18 str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
74.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"]
74.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"]
74.21
74.22 val env = [(str2term "v_v", str2term "x")];
74.23 val errpats =
74.24 @@ -1032,16 +1032,16 @@
74.25 (*if*) f_pred = f_in; (*else*)
74.26 val NONE = (*case*) CAS_Cmd.input f_in (*of*);
74.27 (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
74.28 - (*old*)val {scr = prog, ...} = Method.from_store metID
74.29 + (*old*)val {scr = prog, ...} = MethodC.from_store metID
74.30 (*old*)val istate = get_istate_LI pt pos
74.31 (*old*)val ctxt = get_ctxt pt pos
74.32 ( *old*)
74.33 val LI.Not_Derivable =
74.34 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
74.35 val pp = Ctree.par_pblobj pt p
74.36 - val (errpats, nrls, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
74.37 + val (errpats, nrls, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
74.38 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
74.39 - | _ => error "inform: uncovered case of Method.from_store"
74.40 + | _ => error "inform: uncovered case of MethodC.from_store"
74.41 ;
74.42 (*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
74.43 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
74.44 @@ -1084,9 +1084,9 @@
74.45 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
74.46 val f_curr = Ctree.get_curr_formula (pt, pos);
74.47 val pp = Ctree.par_pblobj pt p
74.48 - val (errpats, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
74.49 + val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
74.50 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
74.51 - | _ => error "find_fill_patterns: uncovered case of Method.from_store"
74.52 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store"
74.53 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
74.54 val subst = Subst.for_bdv prog env
74.55 val errpatthms = errpats
75.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Feb 03 15:21:12 2021 +0100
75.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Feb 03 16:39:44 2021 +0100
75.3 @@ -41,7 +41,7 @@
75.4 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
75.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
75.6 = (m, pos);
75.7 -val {srls, ...} = Method.from_store mI;
75.8 +val {srls, ...} = MethodC.from_store mI;
75.9 val PblObj {meth=itms, ...} = get_obj I pt p;
75.10 val thy' = get_obj g_domID pt p;
75.11 val thy = ThyC.get_theory thy';
75.12 @@ -135,10 +135,10 @@
75.13 val thy = ThyC.get_theory thy'
75.14 val metID = get_obj g_metID pt pp
75.15 val metID' =
75.16 - if metID = Method.id_empty
75.17 + if metID = MethodC.id_empty
75.18 then (thd3 o snd3) (get_obj g_origin pt pp)
75.19 else metID
75.20 - val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = Method.from_store metID'
75.21 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = MethodC.from_store metID'
75.22 val Pstate ist = get_istate_LI pt (p,p_)
75.23 val ctxt = get_ctxt pt (p, p_)
75.24 val alltacs = (*we expect at least 1 stac in a script*)
76.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Feb 03 15:21:12 2021 +0100
76.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Feb 03 16:39:44 2021 +0100
76.3 @@ -43,7 +43,7 @@
76.4
76.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
76.6 = (m, (pt, pos));
76.7 - val {srls, ...} = Method.from_store mI;
76.8 + val {srls, ...} = MethodC.from_store mI;
76.9 val itms = case get_obj I pt p of
76.10 PblObj {meth=itms, ...} => itms
76.11 | _ => error "solve Apply_Method: uncovered case get_obj"
76.12 @@ -118,7 +118,7 @@
76.13 Step_Solve.by_tactic m ptp;
76.14 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
76.15 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
76.16 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
76.17 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
76.18 val thy' = get_obj g_domID pt (par_pblobj pt p);
76.19 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
76.20
76.21 @@ -273,7 +273,7 @@
76.22
76.23 Step_Solve.by_tactic m (pt, p);
76.24 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
76.25 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
76.26 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
76.27 val thy' = get_obj g_domID pt (par_pblobj pt p);
76.28 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
76.29
76.30 @@ -388,7 +388,7 @@
76.31 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
76.32 Step_Solve.do_next (pt, ip);
76.33 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
76.34 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
76.35 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
76.36 val thy' = get_obj g_domID pt (par_pblobj pt p);
76.37 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
76.38
76.39 @@ -439,7 +439,7 @@
76.40 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
76.41 Step_Solve.do_next (pt, ip);
76.42 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
76.43 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
76.44 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
76.45 val thy' = get_obj g_domID pt (par_pblobj pt p);
76.46 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
76.47
76.48 @@ -565,7 +565,7 @@
76.49 (*case*) CAS_Cmd.input f_in (*of*);
76.50
76.51 (*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
76.52 -(*old*) val {scr = prog, ...} = Method.from_store metID
76.53 +(*old*) val {scr = prog, ...} = MethodC.from_store metID
76.54 (*old*) val istate = get_istate_LI pt pos
76.55 (*old*) val ctxt = get_ctxt pt pos
76.56 val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
77.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Wed Feb 03 15:21:12 2021 +0100
77.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Wed Feb 03 16:39:44 2021 +0100
77.3 @@ -20,7 +20,7 @@
77.4 "----------- retrieve errpats ------------------------------------";
77.5 "----------- retrieve errpats ------------------------------------";
77.6 "----------- retrieve errpats ------------------------------------";
77.7 -val {errpats, nrls, scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"];
77.8 +val {errpats, nrls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"];
77.9 case errpats of [("chain-rule-diff-both", _, _)] => ()
77.10 | _ => error "errpats chain-rule-diff-both changed"
77.11
78.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Feb 03 15:21:12 2021 +0100
78.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Feb 03 16:39:44 2021 +0100
78.3 @@ -43,7 +43,7 @@
78.4 val chkorg = map (the o (parse thy)) org;
78.5
78.6 Problem.from_store ["derivative_of", "function"];
78.7 -Method.from_store ["diff", "differentiate_on_R"];
78.8 +MethodC.from_store ["diff", "differentiate_on_R"];
78.9
78.10 "----------- for correction of diff_const ---------------";
78.11 "----------- for correction of diff_const ---------------";
79.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Feb 03 15:21:12 2021 +0100
79.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Feb 03 16:39:44 2021 +0100
79.3 @@ -351,7 +351,7 @@
79.4 val {ppc,...} = Problem.from_store ["named", "integrate", "function"];
79.5 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
79.6 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
79.7 -val {scr = Prog sc,... } = Method.from_store ["diff", "integration", "named"];
79.8 +val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
79.9 val [_,_, F2_] = formal_args sc;
79.10 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
79.11
80.1 --- a/test/Tools/isac/Knowledge/integrate.thy Wed Feb 03 15:21:12 2021 +0100
80.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Wed Feb 03 16:39:44 2021 +0100
80.3 @@ -15,7 +15,7 @@
80.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
80.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
80.6 setup \<open>KEStore_Elems.add_mets
80.7 - [Method.prep_input @{theory "Isac_Knowledge"} "met_testint" [] Method.id_empty
80.8 + [MethodC.prep_input @{theory "Isac_Knowledge"} "met_testint" [] MethodC.id_empty
80.9 (["diff", "integration", "test"],
80.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
80.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
81.1 --- a/test/Tools/isac/Knowledge/inverse_z_transform.sml Wed Feb 03 15:21:12 2021 +0100
81.2 +++ b/test/Tools/isac/Knowledge/inverse_z_transform.sml Wed Feb 03 16:39:44 2021 +0100
81.3 @@ -16,7 +16,7 @@
81.4 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
81.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
81.6 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
81.7 -Method.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
81.8 +MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
81.9
81.10 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
81.11 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
82.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Feb 03 15:21:12 2021 +0100
82.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Feb 03 16:39:44 2021 +0100
82.3 @@ -139,7 +139,7 @@
82.4 val thy' = (get_obj g_domID pt pp):theory';
82.5 val thy = ThyC.get_theory thy'
82.6 val metID = (get_obj g_metID pt pp)
82.7 - val {crls,...} = Method.from_store metID
82.8 + val {crls,...} = MethodC.from_store metID
82.9 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
82.10 | Res => get_obj g_result pt p;
82.11 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)
83.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Wed Feb 03 15:21:12 2021 +0100
83.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Feb 03 16:39:44 2021 +0100
83.3 @@ -548,7 +548,7 @@
83.4 val (dI',pI',mI') =
83.5 ("Test",["sqroot-test", "univariate", "equation", "test"],
83.6 ["Test", "square_equation2"]);
83.7 -val Prog sc = (#scr o Method.from_store) ["Test", "square_equation2"];
83.8 +val Prog sc = (#scr o MethodC.from_store) ["Test", "square_equation2"];
83.9 (writeln o UnparseC.term) sc;
83.10
83.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
83.12 @@ -614,7 +614,7 @@
83.13
83.14
83.15
83.16 -val Prog s = (#scr o Method.from_store) ["Test", "square_equation"];
83.17 +val Prog s = (#scr o MethodC.from_store) ["Test", "square_equation"];
83.18 atomt s;
83.19
83.20
83.21 @@ -685,7 +685,7 @@
83.22 val (dI',pI',mI') =
83.23 ("Test",["squareroot", "univariate", "equation", "test"],
83.24 ["Test", "square_equation"]);
83.25 - val Prog sc = (#scr o Method.from_store) ["Test", "square_equation"];
83.26 + val Prog sc = (#scr o MethodC.from_store) ["Test", "square_equation"];
83.27 (writeln o UnparseC.term) sc;
83.28
83.29 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
84.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Wed Feb 03 15:21:12 2021 +0100
84.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Feb 03 16:39:44 2021 +0100
84.3 @@ -336,7 +336,7 @@
84.4
84.5 LI.do_next (pt, input_pos);
84.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
84.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
84.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
84.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
84.10
84.11 val (_, (ist, ctxt), sc) =
85.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Wed Feb 03 15:21:12 2021 +0100
85.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Wed Feb 03 16:39:44 2021 +0100
85.3 @@ -169,7 +169,7 @@
85.4 "----------- fun upds_envv ---------------------------------------------------------------------";
85.5 (* eval test-maximum.sml until Specify_Method ...
85.6 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
85.7 - val met = (#ppc o Method.from_store) mI;
85.8 + val met = (#ppc o MethodC.from_store) mI;
85.9
85.10 val envv = [];
85.11 val eargs = flat eargs;
86.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Feb 03 15:21:12 2021 +0100
86.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Feb 03 16:39:44 2021 +0100
86.3 @@ -117,7 +117,7 @@
86.4 ip = p; (*false*)
86.5 member op = [Pbl,Met] p_; (*false*)
86.6 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
86.7 -Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
86.8 +MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
86.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
86.10 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
86.11
86.12 @@ -206,7 +206,7 @@
86.13 val is = Istate.init_detail tac t
86.14 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
86.15 is wrong for simpl, but working ?!? *)
86.16 - val tac_ = Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
86.17 + val tac_ = Apply_Method' (MethodC.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
86.18 val pos' = ((lev_on o lev_dn) p, Frm)
86.19 val thy = ThyC.get_theory "Isac_Knowledge"
86.20 val (_,_,_,pt') = (*implicit Take*)Step.add tac_ (is, ctxt) (pt, pos');
86.21 @@ -222,7 +222,7 @@
86.22 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
86.23 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
86.24 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
86.25 -Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
86.26 +MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
86.27 val thy' = get_obj g_domID pt (par_pblobj pt p);
86.28 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
86.29 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
86.30 @@ -348,7 +348,7 @@
86.31 Frm => get_obj g_form pt p
86.32 | Res => (fst o (get_obj g_result pt)) p
86.33 | _ => TermC.empty (*on PblObj is fo <> ifo*);
86.34 - val {nrls, ...} = Method.from_store (get_obj g_metID pt (par_pblobj pt p))
86.35 + val {nrls, ...} = MethodC.from_store (get_obj g_metID pt (par_pblobj pt p))
86.36 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
86.37 (*val (found, der) = *)Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
86.38 "~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
87.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Wed Feb 03 15:21:12 2021 +0100
87.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Wed Feb 03 16:39:44 2021 +0100
87.3 @@ -43,7 +43,7 @@
87.4 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
87.5 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
87.6 val cpI = if pI = Problem.id_empty then pI' else pI;
87.7 - val cmI = if mI = Method.id_empty then mI' else mI;
87.8 + val cmI = if mI = MethodC.id_empty then mI' else mI;
87.9 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
87.10
87.11 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
88.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Feb 03 15:21:12 2021 +0100
88.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Feb 03 16:39:44 2021 +0100
88.3 @@ -66,7 +66,7 @@
88.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
88.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
88.6 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
88.7 - val {ppc, ...} = Method.from_store mI;
88.8 + val {ppc, ...} = MethodC.from_store mI;
88.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
88.10 val srls = LItool.get_simplifier (pt, pos)
88.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
88.12 @@ -101,5 +101,5 @@
88.13 (* final test ...*)
88.14 if p'''''_' = ([1], Frm) andalso f2str f'''''_' = "x + 1 = 2"
88.15 then case nxt'''''_' of (Rewrite_Set "norm_equation") => ()
88.16 - | _ => error "minisubpbl: Method not started in root-problem 1"
88.17 -else error "minisubpbl: Method not started in root-problem 2";
88.18 + | _ => error "minisubpbl: MethodC not started in root-problem 1"
88.19 +else error "minisubpbl: MethodC not started in root-problem 2";
89.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Feb 03 15:21:12 2021 +0100
89.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Feb 03 16:39:44 2021 +0100
89.3 @@ -36,7 +36,7 @@
89.4
89.5 Step_Solve.by_tactic m ptp;
89.6 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
89.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);
89.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);
89.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
89.10 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
89.11
89.12 @@ -91,8 +91,8 @@
89.13 (*if*) member op = [Pbl, Met] p_ = false;
89.14
89.15 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
89.16 - Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
89.17 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p)(*else*);
89.18 + MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
89.19 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p)(*else*);
89.20 val thy' = get_obj g_domID pt (par_pblobj pt p);
89.21 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
89.22
89.23 @@ -144,7 +144,7 @@
89.24
89.25 Step_Solve.do_next (pt, ip);
89.26 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
89.27 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
89.28 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
89.29 val thy' = get_obj g_domID pt (par_pblobj pt p);
89.30 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
89.31
90.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Feb 03 15:21:12 2021 +0100
90.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Feb 03 16:39:44 2021 +0100
90.3 @@ -36,7 +36,7 @@
90.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
90.5 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
90.6 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
90.7 - val {ppc, ...} = Method.from_store mI;
90.8 + val {ppc, ...} = MethodC.from_store mI;
90.9 val (itms, oris, probl) = case get_obj I pt p of
90.10 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
90.11 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
91.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Feb 03 15:21:12 2021 +0100
91.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Feb 03 16:39:44 2021 +0100
91.3 @@ -37,7 +37,7 @@
91.4 (*val (msg, cs') =*)
91.5 Step_Solve.by_tactic m (pt, p);
91.6 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
91.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
91.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
91.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
91.10 val (is, sc) = resume_prog thy' (p,p_) pt;
91.11
92.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Feb 03 15:21:12 2021 +0100
92.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Feb 03 16:39:44 2021 +0100
92.3 @@ -52,7 +52,7 @@
92.4
92.5 LI.do_next (pt, ip);
92.6 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
92.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
92.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
92.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
92.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
92.11
93.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Feb 03 15:21:12 2021 +0100
93.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Feb 03 16:39:44 2021 +0100
93.3 @@ -44,7 +44,7 @@
93.4 (*if*) member op = [Pbl,Met] p_; (*= false*)
93.5
93.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
93.7 -(*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
93.8 +(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
93.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
93.10 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
93.11
93.12 @@ -56,7 +56,7 @@
93.13 "~~~~~ fun by_tactic , args:"; val ((Check_Postcond' (pI, _)), (sub_ist, sub_ctxt), (pt, pos as (p,_))) =
93.14 (tac, (ist, ctxt), ptp);
93.15 val parent_pos = par_pblobj pt p
93.16 - val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
93.17 + val {scr, ...} = MethodC.from_store (get_obj g_metID pt parent_pos);
93.18 val prog_res =
93.19 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
93.20 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
94.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Feb 03 15:21:12 2021 +0100
94.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Feb 03 16:39:44 2021 +0100
94.3 @@ -53,7 +53,7 @@
94.4 tacis; (*= []*)
94.5 member op = [Pbl,Met] p_; (*= false*)
94.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
94.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
94.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
94.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
94.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
94.11
95.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Wed Feb 03 15:21:12 2021 +0100
95.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Wed Feb 03 16:39:44 2021 +0100
95.3 @@ -98,7 +98,7 @@
95.4
95.5 Step_Solve.do_next (pt, ip);
95.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
95.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
95.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
95.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
95.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
95.11
96.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Feb 03 15:21:12 2021 +0100
96.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Feb 03 16:39:44 2021 +0100
96.3 @@ -91,7 +91,7 @@
96.4
96.5 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
96.6
96.7 - val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
96.8 + val tac_ = Tactic.Apply_Method' (MethodC.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
96.9 val pos' = ((lev_on o lev_dn) p, Frm)
96.10 val thy = ThyC.get_theory "Isac_Knowledge"
96.11 val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *);
97.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Feb 03 15:21:12 2021 +0100
97.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Feb 03 16:39:44 2021 +0100
97.3 @@ -49,7 +49,7 @@
97.4
97.5 LI.do_next (pt, input_pos);
97.6 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
97.7 - (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
97.8 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
97.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
97.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
97.11
97.12 @@ -112,7 +112,7 @@
97.13 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
97.14 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
97.15 val fo = Calc.current_formula ptp
97.16 - val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
97.17 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
97.18 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
97.19 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
97.20 (*if*) found (*then*);
97.21 @@ -130,7 +130,7 @@
97.22 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
97.23 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
97.24 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
97.25 - val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
97.26 + val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
97.27 val (pt, c, pos as (p, _)) =
97.28
97.29 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
98.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Feb 03 15:21:12 2021 +0100
98.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Feb 03 16:39:44 2021 +0100
98.3 @@ -544,7 +544,7 @@
98.4 (*solve*)
98.5 val pp = par_pblobj pt p;
98.6 val metID = get_obj g_metID pt pp;
98.7 - val sc = (#scr o Method.from_store) metID;
98.8 + val sc = (#scr o MethodC.from_store) metID;
98.9 val is = get_istate_LI pt (p,p_);
98.10 val thy' = get_obj g_domID pt pp;
98.11 val thy = ThyC.get_theory thy';
99.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Wed Feb 03 15:21:12 2021 +0100
99.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Wed Feb 03 16:39:44 2021 +0100
99.3 @@ -78,7 +78,7 @@
99.4
99.5 methods:= overwritel (!methods,
99.6 [
99.7 - Method.prep_input
99.8 + MethodC.prep_input
99.9 (("Isac_Knowledge", "solve_univar_err"):metID,
99.10 [("#Given" ,["equality e_e", "solveFor v_v", "errorBound err_"]),
99.11 ("#Find" ,["solutions v_i_"])
100.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Feb 03 15:21:12 2021 +0100
100.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Feb 03 16:39:44 2021 +0100
100.3 @@ -30,7 +30,7 @@
100.4 thy;
100.5
100.6 store_met
100.7 - (Method.prep_input Test.thy "met_test_simp" [] e_metID
100.8 + (MethodC.prep_input Test.thy "met_test_simp" [] e_metID
100.9 (*test for simplification*)
100.10 (["Test", "met_testterm"]:metID,
100.11 [("#Given" ,["realTestGiven g_"]),
100.12 @@ -95,7 +95,7 @@
100.13 thy;
100.14
100.15 store_met
100.16 - (Method.prep_input Test.thy "met_test_eq1" [] e_metID
100.17 + (MethodC.prep_input Test.thy "met_test_eq1" [] e_metID
100.18 (["Test", "testeq1"]:metID,
100.19 [("#Given",["boolTestGiven e_e"]),
100.20 ("#Where" ,[]),
100.21 @@ -118,7 +118,7 @@
100.22 "boolTestFind v_i_"];
100.23 val (dI',pI',mI') = ("Test",["met_testeq", "tests"],
100.24 ["Test", "testeq1"]);
100.25 -val Prog sc = (#scr o Method.from_store) ["Test", "testeq1"];
100.26 +val Prog sc = (#scr o MethodC.from_store) ["Test", "testeq1"];
100.27 atomt sc;
100.28 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
100.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
100.30 @@ -150,7 +150,7 @@
100.31 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
100.32 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
100.33 store_met
100.34 - (Method.prep_input Test.thy "met_test_let" [] e_metID
100.35 + (MethodC.prep_input Test.thy "met_test_let" [] e_metID
100.36 (["Test", "testlet"]:metID,
100.37 [("#Given",["boolTestGiven e_e"]),
100.38 ("#Where" ,[]),
100.39 @@ -168,7 +168,7 @@
100.40 \ e_e)\
100.41 \in [e_::bool])"
100.42 ));
100.43 -val Prog sc = (#scr o Method.from_store) ["Test", "testlet"];
100.44 +val Prog sc = (#scr o MethodC.from_store) ["Test", "testlet"];
100.45 writeln(UnparseC.term sc);
100.46 val fmz = ["boolTestGiven (sqrt a = 0)",
100.47 "boolTestFind v_i_"];
100.48 @@ -200,7 +200,7 @@
100.49 val (dI',pI',mI') =
100.50 ("Test",["sqroot-test", "univariate", "equation", "test"],
100.51 ["Test", "sqrt-equ-test"]);
100.52 -val Prog sc = (#scr o Method.from_store) ["Test", "sqrt-equ-test"];
100.53 +val Prog sc = (#scr o MethodC.from_store) ["Test", "sqrt-equ-test"];
100.54 writeln(UnparseC.term sc);
100.55
100.56 "--- s1 ---";
100.57 @@ -301,7 +301,7 @@
100.58 val (dI',pI',mI') =
100.59 ("Test",["sqroot-test", "univariate", "equation", "test"],
100.60 ["Test", "sqrt-equ-test"]);
100.61 - val Prog sc = (#scr o Method.from_store) ["Test", "sqrt-equ-test"];
100.62 + val Prog sc = (#scr o MethodC.from_store) ["Test", "sqrt-equ-test"];
100.63 (writeln o UnparseC.term) sc;
100.64 "--- s1 ---";
100.65 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
101.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Wed Feb 03 15:21:12 2021 +0100
101.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Wed Feb 03 16:39:44 2021 +0100
101.3 @@ -275,7 +275,7 @@
101.4 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
101.5 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
101.6 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
101.7 -val {scr, ...} = Method.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
101.8 +val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
101.9 case stacpbls sc of
101.10 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
101.11 Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
102.1 --- a/test/Tools/isac/ProgLang/calculate.thy Wed Feb 03 15:21:12 2021 +0100
102.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed Feb 03 16:39:44 2021 +0100
102.3 @@ -34,7 +34,7 @@
102.4 (Try (Repeat (Calculate ''DIVIDE''))) #>
102.5 (Try (Repeat (Calculate ''POWER''))))) t_t"
102.6 setup \<open>KEStore_Elems.add_mets
102.7 - [Method.prep_input (@{theory "Test"}) "met_testcal" [] Method.id_empty
102.8 + [MethodC.prep_input (@{theory "Test"}) "met_testcal" [] MethodC.id_empty
102.9 (["Test", "test_calculate"],
102.10 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
102.11 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
103.1 --- a/test/Tools/isac/ProgLang/prog_tac.sml Wed Feb 03 15:21:12 2021 +0100
103.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Wed Feb 03 16:39:44 2021 +0100
103.3 @@ -18,7 +18,7 @@
103.4 "-------- fun eval_leaf -------------------------------------------------------------------";
103.5 "-------- fun eval_leaf -------------------------------------------------------------------";
103.6 "-------- fun eval_leaf -------------------------------------------------------------------";
103.7 -val {scr = Prog sc, ...} = Method.from_store ["Test", "sqrt-equ-test"];
103.8 +val {scr = Prog sc, ...} = MethodC.from_store ["Test", "sqrt-equ-test"];
103.9 case eval_leaf [] NONE TermC.empty sc of
103.10 (Expr (Const ("HOL.eq", _) $
103.11 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
104.1 --- a/test/Tools/isac/ProgLang/tactical.sml Wed Feb 03 15:21:12 2021 +0100
104.2 +++ b/test/Tools/isac/ProgLang/tactical.sml Wed Feb 03 16:39:44 2021 +0100
104.3 @@ -17,7 +17,7 @@
104.4 "-------- fun Tactical.is ----------------------------------------------------------------------";
104.5 "-------- fun Tactical.is ----------------------------------------------------------------------";
104.6 "-------- fun Tactical.is ----------------------------------------------------------------------";
104.7 -val {scr = Prog t, ...} = Method.from_store ["simplification", "for_polynomials"];
104.8 +val {scr = Prog t, ...} = MethodC.from_store ["simplification", "for_polynomials"];
104.9
104.10 if Tactical.is (Program.body_of t)
104.11 then error "Tactical.is body_of [simplification,for_polynomials]" else ();
104.12 @@ -25,11 +25,11 @@
104.13 "-------- fun contained_in ---------------------------------------------------------------------";
104.14 "-------- fun contained_in ---------------------------------------------------------------------";
104.15 "-------- fun contained_in ---------------------------------------------------------------------";
104.16 -val {scr = Prog t, ...} = Method.from_store ["simplification", "for_polynomials"];
104.17 +val {scr = Prog t, ...} = MethodC.from_store ["simplification", "for_polynomials"];
104.18 if contained_in t then error "NOT Tactical.contained_in [simplification,for_polynomials]" else ();
104.19
104.20 -val {scr = Prog t, ...} = Method.from_store ["Test", "squ-equ-test-subpbl1"];
104.21 +val {scr = Prog t, ...} = MethodC.from_store ["Test", "squ-equ-test-subpbl1"];
104.22 if contained_in t then () else error "Tactical.contained_in [Test,squ-equ-test-subpbl1]";
104.23
104.24 -val {scr = Prog t, ...} = Method.from_store ["simplification", "of_rationals"];
104.25 +val {scr = Prog t, ...} = MethodC.from_store ["simplification", "of_rationals"];
104.26 if contained_in t then () else error "Tactical.contained_in [simplification,of_rationals]";
105.1 --- a/test/Tools/isac/Specify/i-model.sml Wed Feb 03 15:21:12 2021 +0100
105.2 +++ b/test/Tools/isac/Specify/i-model.sml Wed Feb 03 16:39:44 2021 +0100
105.3 @@ -48,7 +48,7 @@
105.4 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
105.5 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
105.6 val cpI = if pI = Problem.id_empty then pI' else pI
105.7 - val cmI = if mI = Method.id_empty then mI' else mI
105.8 + val cmI = if mI = MethodC.id_empty then mI' else mI
105.9 val {ppc, where_, prls, ...} = Problem.from_store cpI;
105.10
105.11 (*+*)if Model_Pattern.to_string ppc = "[\"" ^
106.1 --- a/test/Tools/isac/Specify/refine.sml Wed Feb 03 15:21:12 2021 +0100
106.2 +++ b/test/Tools/isac/Specify/refine.sml Wed Feb 03 16:39:44 2021 +0100
106.3 @@ -408,9 +408,9 @@
106.4 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
106.5 (oris, (o_refs, refs), (pbl, met));
106.6 val cpI = if pI = Problem.id_empty then pI' else pI;
106.7 - val cmI = if mI = Method.id_empty then mI' else mI;
106.8 + val cmI = if mI = MethodC.id_empty then mI' else mI;
106.9 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
106.10 - val {ppc = mpc, ...} = Method.from_store cmI
106.11 + val {ppc = mpc, ...} = MethodC.from_store cmI
106.12 val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0;
106.13 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
106.14 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
107.1 --- a/test/Tools/isac/Specify/specify.sml Wed Feb 03 15:21:12 2021 +0100
107.2 +++ b/test/Tools/isac/Specify/specify.sml Wed Feb 03 16:39:44 2021 +0100
107.3 @@ -122,7 +122,7 @@
107.4 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
107.5 val mits = get_obj g_met pt (fst p);
107.6 val mits = I_Model.complete oris pits []
107.7 - ((#ppc o Method.from_store) ["DiffApp", "max_by_calculus"]);
107.8 + ((#ppc o MethodC.from_store) ["DiffApp", "max_by_calculus"]);
107.9 writeln (I_Model.to_string ctxt mits);
107.10 (*[
107.11 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
107.12 @@ -241,7 +241,7 @@
107.13 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
107.14 ...} = Calc.specify_data (ctree, pos);
107.15 val (dI, _, _) = References.select o_refs refs;
107.16 - val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
107.17 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
107.18 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
107.19 val (o_model', ctxt') =
107.20
107.21 @@ -317,7 +317,7 @@
107.22 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
107.23 (*NEW*) ...} = Calc.specify_data (pt, pos);
107.24 (*NEW*) val (dI, _, mID) = References.select o_refs refs;
107.25 -(*NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
107.26 +(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
107.27 (*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
107.28 (*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
107.29 (*NEW*) val thy = ThyC.get_theory dI
107.30 @@ -396,16 +396,16 @@
107.31 (*.NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
107.32 (*.NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
107.33 val cpI = if pI = Problem.id_empty then pI' else pI;
107.34 - val cmI = if mI = Method.id_empty then mI' else mI;
107.35 + val cmI = if mI = MethodC.id_empty then mI' else mI;
107.36 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
107.37 val (preok, pre) = Pre_Conds.check prls where_ pbl 0;
107.38 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
107.39 - val mpc = (#ppc o Method.from_store) cmI
107.40 + val mpc = (#ppc o MethodC.from_store) cmI
107.41 val Pos.Met = (*case*) p_ (*of*);
107.42 val NONE = (*case*) find_first (I_Model.is_error o #5) met (*of*);
107.43
107.44 (*/------------------- check within find_next_step -----------------------------------------\*)
107.45 -(*+*)Model_Pattern.to_string (Method.from_store mI' |> #ppc) = "[\"" ^
107.46 +(*+*)Model_Pattern.to_string (MethodC.from_store mI' |> #ppc) = "[\"" ^
107.47 "(#Given, (Traegerlaenge, l))\", \"" ^
107.48 "(#Given, (Streckenlast, q))\", \"" ^
107.49 "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
107.50 @@ -495,7 +495,7 @@
107.51 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
107.52 (*if*) p_ = Pos.Met (*then*);
107.53 val (i_model, m_patt) = (met,
107.54 - (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
107.55 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
107.56
107.57 val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
107.58 (*case*)
107.59 @@ -555,7 +555,7 @@
107.60 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
107.61 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
107.62 (*
107.63 -.. here the O_Model does NOT know, which Method will be chosen,
107.64 +.. here the O_Model does NOT know, which MethodC will be chosen,
107.65 so "belastung_zu_biegelinie q__q v_v id_fun id_abl" is NOT known,
107.66 "id_fun" and "id_abl" are NOT missing.
107.67 *)
107.68 @@ -592,24 +592,24 @@
107.69 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
107.70 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
107.71 (*
107.72 -.. here the Method has been determined by the user,
107.73 +.. here the MethodC has been determined by the user,
107.74 so "belastung_zu_biegelinie q__q v_v id_fun id_abl" IS KNOWN and,
107.75 "id_fun" and "id_abl" WOULD BE missing (added by O_Model.).
107.76 *)
107.77 -then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY Method";
107.78 +then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
107.79 (*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
107.80 "~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
107.81 (tac', ptp);
107.82 (*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
107.83 (*.NEW*) ...} =Calc.specify_data (pt, pos);
107.84 (*.NEW*) val (dI, _, mID) = References.select o_refs refs;
107.85 -(*.NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
107.86 +(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
107.87 (*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
107.88 (*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
107.89
107.90 (*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
107.91 (*+*)if mID = ["Biegelinien", "ausBelastung"]
107.92 -(*+*)then () else error "Method [Biegelinien, ausBelastung] CHANGED";
107.93 +(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
107.94 (*+*)if Model_Pattern.to_string m_patt = "[\"" ^
107.95 "(#Given, (Streckenlast, q__q))\", \"" ^
107.96 "(#Given, (FunktionsVariable, v_v))\", \"" ^
107.97 @@ -621,7 +621,7 @@
107.98 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
107.99 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
107.100 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
107.101 -(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY Method CHANGED";
107.102 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
107.103 (*+*)if O_Model.to_string root_model = "[\n" ^
107.104 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
107.105 "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
107.106 @@ -638,7 +638,7 @@
107.107 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*.. value from O_Model of root-problem*)
107.108 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]" (*.. value from O_Model of root-problem*)
107.109 (* ^^^----- aim at dropping this field *)
107.110 -(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY Method CHANGED";
107.111 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
107.112 (*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
107.113
107.114 O_Model.complete_for m_patt root_model (o_model, ctxt);
107.115 @@ -675,7 +675,7 @@
107.116 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^
107.117 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
107.118 (* ^^^----- aim at dropping this field *)
107.119 -(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY Method CHANGED";
107.120 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
107.121 (*\------------------- check within O_Model.complete_for -------------------------------------------/*)
107.122
107.123 (*.NEW*) val thy = ThyC.get_theory dI
107.124 @@ -742,11 +742,11 @@
107.125
107.126 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
107.127 val cpI = if pI = Problem.id_empty then pI' else pI;
107.128 - val cmI = if mI = Method.id_empty then mI' else mI;
107.129 + val cmI = if mI = MethodC.id_empty then mI' else mI;
107.130 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
107.131 val (preok, pre) = Pre_Conds.check prls where_ pbl 0;
107.132 val preok = foldl and_ (true, map fst pre);
107.133 - val mpc = (#ppc o Method.from_store) cmI
107.134 + val mpc = (#ppc o MethodC.from_store) cmI
107.135 val Pos.Met = (*case*) p_ (*of*);
107.136 val NONE = (*case*) find_first (is_error o #5) met (*of*);
107.137 (*val SOME ("#Given", "Biegelinie y") =*)
107.138 @@ -778,7 +778,7 @@
107.139 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
107.140 (*if*) p_ = Pos.Met (*then*);
107.141 val (i_model, m_patt) = (met,
107.142 - (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
107.143 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
107.144
107.145 val Add (4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
107.146 (*case*)
107.147 @@ -802,7 +802,7 @@
107.148 (*\------------------- check for entry to check_single -------------------------------------/*)
107.149
107.150 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
107.151 - (ctxt, sel, oris, met, ((#ppc o Method.from_store) cmI), ct);
107.152 + (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct);
107.153 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
107.154
107.155 (*+*)val Const ("Biegelinie.Biegelinie", _) $ Free ("y", _) = t;
107.156 @@ -836,7 +836,7 @@
107.157 (*/------------------- check within seek_orits -------------------------------\*)
107.158 (*+*)if sel = "#Given" andalso sel' = "#Given"
107.159 (*+*)then () else error "seek_orits Model_Pattern CHANGED";
107.160 -(*BUT: m_field can change from root-Problem to sub-Method --------------------vvv*)
107.161 +(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
107.162 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
107.163 (*+*)if (Problem.from_store ["vonBelastungZu", "Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
107.164 "(#Given, (Streckenlast, q_q))\", \"" ^
107.165 @@ -851,7 +851,7 @@
107.166 "(#Relate, (Randbedingungen, r_b))\"]"
107.167 (*+*)then () else error "seek_orits Model_Pattern root-problem CHANGED";
107.168 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
107.169 -(*+*)if (Method.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
107.170 +(*+*)if (MethodC.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
107.171 "(#Given, (Streckenlast, q__q))\", \"" ^
107.172 "(#Given, (FunktionsVariable, v_v))\", \"" ^
107.173 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*---------------------------------^^^*)