1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Apr 22 11:23:30 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Apr 22 14:36:27 2020 +0200
1.3 @@ -66,9 +66,9 @@
1.4 val get_cas: theory -> CAS_Def.T list
1.5 val add_cas: CAS_Def.T list -> theory -> theory
1.6 val get_ptyps: theory -> Probl_Def.store
1.7 - val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
1.8 + val add_pbts: (Probl_Def.T * Spec.id) list -> theory -> theory
1.9 val get_mets: theory -> Meth_Def.store
1.10 - val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
1.11 + val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
1.12 val get_thes: theory -> (Thy_Html.thydata Store.node) list
1.13 val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.14 val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.15 @@ -99,7 +99,7 @@
1.16 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
1.17
1.18 structure Data = Theory_Data (
1.19 - type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
1.20 + type T = (term * (Spec.T * (term list -> (term * term list) list))) list;
1.21 val empty = [];
1.22 val extend = I;
1.23 val merge = merge CAS_Def.equal;
2.1 --- a/src/Tools/isac/BaseDefinitions/cas-def.sml Wed Apr 22 11:23:30 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/cas-def.sml Wed Apr 22 14:36:27 2020 +0200
2.3 @@ -31,7 +31,7 @@
2.4 list) (* of elements in the formalization *)
2.5 type T =
2.6 (term * (* cas-command, eg. 'solve' *)
2.7 - (Spec.spec * (* theory, problem, method *)
2.8 + (Spec.T * (* theory, problem, method *)
2.9 generate_fn))
2.10 fun equal ((t1, (_, _)) : T, (t2, (_, _)) : T) = t1 = t2
2.11 (*\------- to Celem7 -------/*)
3.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Wed Apr 22 11:23:30 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Wed Apr 22 14:36:27 2020 +0200
3.3 @@ -6,6 +6,10 @@
3.4 *)
3.5 signature METHOD_DEFINITION =
3.6 sig
3.7 + type id = Spec.id;
3.8 + val id_empty: id
3.9 + val id_to_string: id -> string
3.10 +
3.11 type T
3.12 (*type met*)
3.13 val empty: T
3.14 @@ -28,11 +32,15 @@
3.15 struct
3.16 (**)
3.17
3.18 +type id = Spec.id;
3.19 +val id_empty = Spec.empty_meth_id;
3.20 +val id_to_string = Spec.id_to_string;
3.21 +
3.22 (* data for methods stored in 'methods'-database*)
3.23 type T =
3.24 {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
3.25 mathauthors: string list, (* copyright *)
3.26 - init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
3.27 + init : Spec.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE! *)
3.28 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
3.29 TODO.WN0509 store fun itself, see 'type pbt' *)
3.30 erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
3.31 @@ -53,10 +61,10 @@
3.32 see ME/calchead.sml 'fun is_copy_named'. *)
3.33 pre : term list (* preconditions in where *)
3.34 };
3.35 -val empty = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
3.36 +val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
3.37 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
3.38 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
3.39 -val empty_store = Store.Node ("e_metID", [empty],[]);
3.40 +val empty_store = Store.Node ("empty_meth_id", [empty],[]);
3.41
3.42 type store = (T Store.node) list;
3.43 (*\------- to Celem6 -------/*)
4.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Wed Apr 22 11:23:30 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Wed Apr 22 14:36:27 2020 +0200
4.3 @@ -6,6 +6,9 @@
4.4 *)
4.5 signature PROBLEM_DEFINITION =
4.6 sig
4.7 + type id = Spec.id
4.8 + val id_empty: id
4.9 + val id_to_string: id -> string
4.10 (*type pbt*)
4.11 type T
4.12 (*val e_Ptyp: T Store.node*)
4.13 @@ -30,18 +33,21 @@
4.14 struct
4.15 (**)
4.16
4.17 -(*/------- to Celem5 -------\*)
4.18 +type id = Spec.id;
4.19 +val id_empty = Spec.empty_probl_id;
4.20 +val id_to_string = Spec.id_to_string;
4.21 +
4.22 type T =
4.23 {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
4.24 mathauthors : string list, (* copyright *)
4.25 - init : Spec.pblID, (* to start refinement with *)
4.26 + init : Spec.id, (* to start refinement with *)
4.27 thy : theory, (* which allows to compile that T
4.28 TODO: search generalized for subthy (ref.p.69*)
4.29 (*^^^ WN050912 NOT used during application of the problem,
4.30 because applied terms may be from 'subthy' as well as from super;
4.31 thus we take 'maxthy'; see match_ags ! *)
4.32 cas : term option, (* 'CAS-command' *)
4.33 - met : Spec.metID list, (* methods solving the T *)
4.34 + met : Spec.id list, (* methods solving the T *)
4.35 (*TODO: abstract to ?pre_model?...*)
4.36 prls : Rule_Set.T, (* for preds in where_ *)
4.37 where_ : term list, (* where - predicates *)
4.38 @@ -49,7 +55,7 @@
4.39 it contains "#Given","#Where","#Find","#Relate"-patterns
4.40 for constraints on identifiers see "fun cpy_nam" *)
4.41 }
4.42 -val empty = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
4.43 +val empty = {guh = "pbl_empty", mathauthors = [], init = id_empty, thy = Thy_Info.get_theory "Pure",
4.44 cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : T
4.45 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
4.46 prls = prls', thy = thy', where_ = w'} : T)
4.47 @@ -61,7 +67,7 @@
4.48 fun s_to_string pbts = map pbt2str pbts |> list2str;
4.49 (*\------- to Celem5 -------/*)
4.50 (*/------- to Celem5 -------\*)
4.51 -val empty_store = Store.Node ("e_pblID", [empty], [])
4.52 +val empty_store = Store.Node ("empty_probl_id", [empty], [])
4.53 type store = (T Store.node) list
4.54 (*\------- to Celem5 -------/*)
4.55
5.1 --- a/src/Tools/isac/BaseDefinitions/specification.sml Wed Apr 22 11:23:30 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/specification.sml Wed Apr 22 14:36:27 2020 +0200
5.3 @@ -6,14 +6,15 @@
5.4 *)
5.5 signature SPECIFICATION =
5.6 sig
5.7 - type metID
5.8 - type pblID
5.9 - type spec
5.10 + type id (* will be specialised to Problem.id, Method.id *)
5.11 + val id_to_string: id -> string
5.12 + val empty_probl_id: id
5.13 + val empty_meth_id: id
5.14 +
5.15 + type T
5.16 + val empty: T
5.17 val to_string: string * string list * string list -> string
5.18 - val metID2str: string list -> string
5.19 - val e_pblID: pblID
5.20 - val e_metID: metID
5.21 - val empty: spec
5.22 +
5.23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.24 (*NONE*)
5.25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.26 @@ -26,17 +27,14 @@
5.27 struct
5.28 (**)
5.29
5.30 -(*the key into the hierarchy ob problems*)
5.31 -type pblID = string list; (* domID :: ...*)
5.32 -val e_pblID = ["e_pblID"];
5.33 +type id = string list;
5.34 +val id_to_string = strs2str;
5.35 +val empty_probl_id = ["empty_probl_id"];
5.36 +val empty_meth_id = ["empty_meth_id"];
5.37
5.38 -(*the key into the hierarchy ob methods*)
5.39 -type metID = string list;
5.40 -type spec = ThyC.id * pblID * metID;
5.41 +type T = ThyC.id * id * id;
5.42 fun to_string (dom, pbl, met) =
5.43 "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
5.44 -val e_metID = ["e_metID"];
5.45 -val metID2str = strs2str;
5.46 -val empty = (ThyC.id_empty, e_pblID, e_metID);
5.47 +val empty = (ThyC.id_empty, empty_probl_id, empty_meth_id);
5.48
5.49 (**)end(**)
6.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Apr 22 11:23:30 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Apr 22 14:36:27 2020 +0200
6.3 @@ -33,14 +33,14 @@
6.4
6.5 fun get_thy thyID = Thy_Info.get_theory ("Isac." ^ thyID);
6.6 fun get_theory thy =
6.7 - if thy = "thy_empty_id"
6.8 + if thy = "empty_thy_id"
6.9 then (get_thy "Base_Tools") (*lower bound of Knowledge*)
6.10 else (get_thy thy) handle _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
6.11
6.12 fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');
6.13 fun to_ctxt thy = Proof_Context.init_global thy;
6.14
6.15 -val id_empty = "thy_empty_id";
6.16 +val id_empty = "empty_thy_id";
6.17 fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge");
6.18
6.19 (**)end(**)
7.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 11:23:30 2020 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 14:36:27 2020 +0200
7.3 @@ -41,7 +41,7 @@
7.4 val rule2xml : int -> Check_Unique.guh -> Rule.rule -> Celem.xml
7.5 val rules2xml : int -> Check_Unique.guh -> Rule.rule list -> Celem.xml
7.6 val scr2xml : int -> Program.T -> Celem.xml
7.7 - val spec2xml : int -> Spec.spec -> Celem.xml
7.8 + val spec2xml : int -> Spec.T -> Celem.xml
7.9 val sub2xml : int -> Term.term * Term.term -> Celem.xml
7.10 val subs2xml : int -> Selem.subs -> Celem.xml
7.11 val subst2xml : int -> UnparseC.subst -> Celem.xml
7.12 @@ -641,7 +641,7 @@
7.13 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
7.14
7.15 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
7.16 - ("Problem (" ^ ThyC.id_empty ^ "," ^ strs2str' Spec.e_pblID ^ ")");
7.17 + ("Problem (" ^ ThyC.id_empty ^ "," ^ strs2str' Problem.id_empty ^ ")");
7.18
7.19 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
7.20 fun xml_of_posterm (p, t, _) =
8.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 22 11:23:30 2020 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 22 14:36:27 2020 +0200
8.3 @@ -52,9 +52,9 @@
8.4 val requestFillformula : Celem.calcID -> Error_Fill_Def.errpatID * Error_Fill_Def.fillpatID -> XML.tree
8.5 val resetCalcHead : Celem.calcID -> XML.tree
8.6 val setContext : Celem.calcID -> Pos.pos' -> Check_Unique.guh -> XML.tree
8.7 - val setMethod : Celem.calcID -> Spec.metID -> XML.tree
8.8 + val setMethod : Celem.calcID -> Method.id -> XML.tree
8.9 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
8.10 - val setProblem : Celem.calcID -> Spec.pblID -> XML.tree
8.11 + val setProblem : Celem.calcID -> Problem.id -> XML.tree
8.12 val setTheory : Celem.calcID -> ThyC.id -> XML.tree
8.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.14 (* NONE *)
9.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 22 11:23:30 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 22 14:36:27 2020 +0200
9.3 @@ -115,7 +115,7 @@
9.4 val i = indentation;
9.5
9.6 (* new version with <KESTOREREF>s -- not used *)
9.7 -fun pbl2xml (id:(*pblRD*)Spec.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
9.8 +fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls,
9.9 thy,where_}:Problem.T) =
9.10 let val thy' = Context.theory_name thy
9.11 val prls' = (#id o Rule_Set.rep) prls
9.12 @@ -149,7 +149,7 @@
9.13 "</NODECONTENT>" : Celem.xml
9.14 end;
9.15 (* old version with 'dead' strings for rls, calc, ....* *)
9.16 -fun pbl2xml (id:(*pblRD*)Spec.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
9.17 +fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls,
9.18 thy,where_}:Problem.T) =
9.19 "<NODECONTENT>\n" ^
9.20 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
9.21 @@ -181,7 +181,7 @@
9.22
9.23
9.24 (**. write pbls from hierarchy to files.**)
9.25 -fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Spec.metID) (pbl as {guh,...}) =
9.26 +fun pbl2file (path: Celem.filepath) (pos: Pos.pos) (id:Method.id) (pbl as {guh,...}) =
9.27 (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos);
9.28 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
9.29 );
9.30 @@ -191,7 +191,7 @@
9.31 new version with <KESTOREREF>s -- not used because linking
9.32 requires elements (rls, calc, ...) to be reorganized.*)
9.33 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
9.34 -fun met2xml (id: Spec.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
9.35 +fun met2xml (id: Method.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
9.36 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) =
9.37 let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*)
9.38 val crls' = (#id o Rule_Set.rep) crls
9.39 @@ -229,7 +229,7 @@
9.40 end;
9.41 (*.format a method in xml for presentation on the method browser;
9.42 old version with 'dead' strings for rls, calc, ....*)
9.43 -fun met2xml (id: Spec.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
9.44 +fun met2xml (id: Method.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
9.45 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Method.T) =
9.46 "<NODECONTENT>\n" ^
9.47 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
9.48 @@ -254,12 +254,12 @@
9.49 *)
9.50
9.51 (*.write the files using an int-key (pos') as filename.*)
9.52 -fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Spec.metID) met =
9.53 +fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) met =
9.54 (writeln ("### met2file: id = " ^ strs2str id);
9.55 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
9.56
9.57 (*.write the files using the guh as filename.*)
9.58 -fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Spec.metID) (met as {guh,...}) =
9.59 +fun met2file (path: Celem.filepath) (pos: Pos.pos) (id: Method.id) (met as {guh,...}) =
9.60 (writeln ("### met2file: id = " ^ strs2str id);
9.61 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
9.62
10.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 22 11:23:30 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 22 14:36:27 2020 +0200
10.3 @@ -14,7 +14,7 @@
10.4 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
10.5
10.6 val implicit_take : Program.T -> (term * term) list -> term option
10.7 - val init_pstate : Rule_Set.T -> Proof.context -> Model.itm list -> Spec.metID ->
10.8 + val init_pstate : Rule_Set.T -> Proof.context -> Model.itm list -> Method.id ->
10.9 Istate.T * Proof.context * Program.T
10.10
10.11 val get_simplifier : Calc.T -> Rule_Set.T
10.12 @@ -29,7 +29,7 @@
10.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.14 (*NONE*)
10.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.16 - val arguments_from_model : Spec.metID -> Model.itm list -> term list
10.17 + val arguments_from_model : Method.id -> Model.itm list -> term list
10.18 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.19 end
10.20
10.21 @@ -241,14 +241,14 @@
10.22 val errmsg = "ERROR: found no actual arguments for prog. of "
10.23 fun msg_miss sc metID caller f formals actuals =
10.24 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
10.25 - "and the actual args., ie. items of the guard of \"" ^ Spec.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
10.26 + "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
10.27 "formal arg \"" ^ UnparseC.term f ^ "\" doesn't mach an actual arg.\n" ^
10.28 "with:\n" ^
10.29 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
10.30 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals
10.31 fun msg_miss_type sc metID f formals actuals =
10.32 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
10.33 - "and the actual args., ie. items of the guard of \"" ^ Spec.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
10.34 + "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
10.35 "formal arg \"" ^ UnparseC.term f ^ "\" of type \"" ^ UnparseC.typ (type_of f) ^
10.36 "\" doesn't mach an actual arg.\nwith:\n" ^
10.37 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
10.38 @@ -256,7 +256,7 @@
10.39 " with types: " ^ (strs2str o (map (UnparseC.typ o type_of))) actuals
10.40 fun msg_ambiguous sc metID f aas formals actuals =
10.41 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
10.42 - "and the actual args., ie. items of the guard of \"" ^ Spec.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
10.43 + "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
10.44 "formal arg. \"" ^ UnparseC.term f ^ "\" type-matches with several..." ^
10.45 "actual args. \"" ^ UnparseC.terms aas ^ "\"\n" ^
10.46 "selected \"" ^ UnparseC.term (hd aas) ^ "\"\n" ^
10.47 @@ -275,7 +275,7 @@
10.48 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
10.49 val (scr, sc) = (case (#scr o Specify.get_met) metID of
10.50 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
10.51 - | _ => raise ERROR ("init_pstate with " ^ Spec.metID2str metID))
10.52 + | _ => raise ERROR ("init_pstate with " ^ Method.id_to_string metID))
10.53 val formals = Program.formal_args sc
10.54 fun assoc_by_type f aa =
10.55 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
11.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 22 11:23:30 2020 +0200
11.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 22 14:36:27 2020 +0200
11.3 @@ -588,7 +588,7 @@
11.4 end
11.5 (*find_next_step from program, by_tactic will update Ctree*)
11.6 and do_next (ptp as (pt, pos as (p, p_))) =
11.7 - if Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) then
11.8 + if Method.id_empty = get_obj g_metID pt (par_pblobj pt p) then
11.9 ("helpless", ([], [], (pt, (p, p_))))
11.10 else
11.11 let
12.1 --- a/src/Tools/isac/Interpret/step-solve.sml Wed Apr 22 11:23:30 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Apr 22 14:36:27 2020 +0200
12.3 @@ -24,7 +24,7 @@
12.4 | by_tactic (Tactic.Free_Solve') (pt, po as (p, _)) =
12.5 let
12.6 val p' = lev_dn_ (p, Res);
12.7 - val pt = update_metID pt (par_pblobj pt p) Spec.e_metID;
12.8 + val pt = update_metID pt (par_pblobj pt p) Method.id_empty;
12.9 in
12.10 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.empty)))], [], (pt,p')))
12.11 end
12.12 @@ -36,7 +36,7 @@
12.13 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
12.14 end
12.15 | by_tactic m (pt, po as (p, p_)) =
12.16 - if Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
12.17 + if Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
12.18 then
12.19 let
12.20 val ctxt = get_ctxt pt po
13.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Wed Apr 22 11:23:30 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed Apr 22 14:36:27 2020 +0200
13.3 @@ -24,8 +24,8 @@
13.4 \<close>
13.5 (** problems **)
13.6 setup \<open>KEStore_Elems.add_pbts
13.7 - [(Specify.prep_pbt thy "pbl_algein" [] Spec.e_pblID (["Berechnung"], [], Rule_Set.empty, NONE, [])),
13.8 - (Specify.prep_pbt thy "pbl_algein_numsym" [] Spec.e_pblID
13.9 + [(Specify.prep_pbt thy "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),
13.10 + (Specify.prep_pbt thy "pbl_algein_numsym" [] Problem.id_empty
13.11 (["numerischSymbolische", "Berechnung"],
13.12 [("#Given",
13.13 ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
13.14 @@ -34,12 +34,12 @@
13.15 Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
13.16
13.17 setup \<open>KEStore_Elems.add_mets
13.18 - [Specify.prep_met thy "met_algein" [] Spec.e_metID
13.19 + [Specify.prep_met thy "met_algein" [] Method.id_empty
13.20 (["Berechnung"], [],
13.21 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
13.22 errpats = [], nrls = Rule_Set.Empty},
13.23 @{thm refl}),
13.24 - Specify.prep_met thy "met_algein_numsym" [] Spec.e_metID
13.25 + Specify.prep_met thy "met_algein_numsym" [] Method.id_empty
13.26 (["Berechnung","erstNumerisch"], [],
13.27 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
13.28 errpats = [], nrls = Rule_Set.Empty},
13.29 @@ -69,7 +69,7 @@
13.30 in
13.31 Try (Rewrite_Set ''norm_Poly'') t_t)"
13.32 setup \<open>KEStore_Elems.add_mets
13.33 - [Specify.prep_met thy "met_algein_numsym_1num" [] Spec.e_metID
13.34 + [Specify.prep_met thy "met_algein_numsym_1num" [] Method.id_empty
13.35 (["Berechnung","erstNumerisch"],
13.36 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
13.37 "KantenSenkrecht s_s", "KantenOben o_o"]),
13.38 @@ -102,7 +102,7 @@
13.39 in
13.40 (Try (Rewrite_Set ''norm_Poly'')) t_t)"
13.41 setup \<open>KEStore_Elems.add_mets
13.42 - [Specify.prep_met thy "met_algein_symnum" [] Spec.e_metID
13.43 + [Specify.prep_met thy "met_algein_symnum" [] Method.id_empty
13.44 (["Berechnung","erstSymbolisch"],
13.45 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
13.46 "KantenSenkrecht s_s", "KantenOben o_o"]),
14.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 22 11:23:30 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 22 14:36:27 2020 +0200
14.3 @@ -72,14 +72,14 @@
14.4
14.5 (** problems **)
14.6 setup \<open>KEStore_Elems.add_pbts
14.7 - [(Specify.prep_pbt @{theory} "pbl_bieg" [] Spec.e_pblID
14.8 + [(Specify.prep_pbt @{theory} "pbl_bieg" [] Problem.id_empty
14.9 (["Biegelinien"],
14.10 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
14.11 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
14.12 ("#Find" ,["Biegelinie b_b"]),
14.13 ("#Relate",["Randbedingungen r_b"])],
14.14 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
14.15 - (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Spec.e_pblID
14.16 + (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Problem.id_empty
14.17 (["MomentBestimmte","Biegelinien"],
14.18 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
14.19 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
14.20 @@ -87,26 +87,26 @@
14.21 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
14.22 ],
14.23 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
14.24 - (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Spec.e_pblID
14.25 + (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Problem.id_empty
14.26 (["MomentGegebene","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
14.27 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
14.28 - (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Spec.e_pblID
14.29 + (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Problem.id_empty
14.30 (["einfache","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
14.31 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
14.32 - (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Spec.e_pblID
14.33 + (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Problem.id_empty
14.34 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
14.35 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
14.36 - (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Spec.e_pblID
14.37 + (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Problem.id_empty
14.38 (["vonBelastungZu","Biegelinien"],
14.39 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
14.40 ("#Find" ,["Funktionen funs'''"])],
14.41 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien","ausBelastung"]])),
14.42 - (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Spec.e_pblID
14.43 + (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Problem.id_empty
14.44 (["setzeRandbedingungen","Biegelinien"],
14.45 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
14.46 ("#Find" ,["Gleichungen equs'''"])],
14.47 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
14.48 - (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Spec.e_pblID
14.49 + (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Problem.id_empty
14.50 (["makeFunctionTo","equation"],
14.51 [("#Given" ,["functionEq fu_n","substitution su_b"]),
14.52 ("#Find" ,["equality equ'''"])],
14.53 @@ -163,7 +163,7 @@
14.54 section \<open>Methods\<close>
14.55 (* setup parent directory *)
14.56 setup \<open>KEStore_Elems.add_mets
14.57 - [Specify.prep_met @{theory} "met_biege" [] Spec.e_metID
14.58 + [Specify.prep_met @{theory} "met_biege" [] Method.id_empty
14.59 (["IntegrierenUndKonstanteBestimmen"], [],
14.60 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
14.61 errpats = [], nrls = Rule_Set.Empty},
14.62 @@ -186,7 +186,7 @@
14.63 B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B
14.64 in B)"
14.65 setup \<open>KEStore_Elems.add_mets
14.66 - [Specify.prep_met @{theory} "met_biege_2" [] Spec.e_metID
14.67 + [Specify.prep_met @{theory} "met_biege_2" [] Method.id_empty
14.68 (["IntegrierenUndKonstanteBestimmen2"],
14.69 [("#Given" ,["Traegerlaenge l", "Streckenlast q",
14.70 "FunktionsVariable v", "GleichungsVariablen vs", "AbleitungBiegelinie id_abl"]),
14.71 @@ -209,22 +209,22 @@
14.72 @{thm biegelinie.simps})]
14.73 \<close>
14.74 setup \<open>KEStore_Elems.add_mets
14.75 - [Specify.prep_met @{theory} "met_biege_intconst_2" [] Spec.e_metID
14.76 + [Specify.prep_met @{theory} "met_biege_intconst_2" [] Method.id_empty
14.77 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
14.78 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
14.79 errpats = [], nrls = Rule_Set.empty},
14.80 @{thm refl}),
14.81 - Specify.prep_met @{theory} "met_biege_intconst_4" [] Spec.e_metID
14.82 + Specify.prep_met @{theory} "met_biege_intconst_4" [] Method.id_empty
14.83 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
14.84 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
14.85 errpats = [], nrls = Rule_Set.empty},
14.86 @{thm refl}),
14.87 - Specify.prep_met @{theory} "met_biege_intconst_1" [] Spec.e_metID
14.88 + Specify.prep_met @{theory} "met_biege_intconst_1" [] Method.id_empty
14.89 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
14.90 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
14.91 errpats = [], nrls = Rule_Set.empty},
14.92 @{thm refl}),
14.93 - Specify.prep_met @{theory} "met_biege2" [] Spec.e_metID
14.94 + Specify.prep_met @{theory} "met_biege2" [] Method.id_empty
14.95 (["Biegelinien"], [],
14.96 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
14.97 errpats = [], nrls = Rule_Set.empty},
14.98 @@ -254,7 +254,7 @@
14.99 in
14.100 [Q__Q, M__M, N__N, B__B])"
14.101 setup \<open>KEStore_Elems.add_mets
14.102 - [Specify.prep_met @{theory} "met_biege_ausbelast" [] Spec.e_metID
14.103 + [Specify.prep_met @{theory} "met_biege_ausbelast" [] Method.id_empty
14.104 (["Biegelinien", "ausBelastung"],
14.105 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",
14.106 "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]),
14.107 @@ -295,7 +295,7 @@
14.108 in
14.109 [e_1, e_2, e_3, e_4])"
14.110 setup \<open>KEStore_Elems.add_mets
14.111 - [Specify.prep_met @{theory} "met_biege_setzrand" [] Spec.e_metID
14.112 + [Specify.prep_met @{theory} "met_biege_setzrand" [] Method.id_empty
14.113 (["Biegelinien", "setzeRandbedingungenEin"],
14.114 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
14.115 ("#Find" , ["Gleichungen equs'''"])],
14.116 @@ -319,7 +319,7 @@
14.117 in
14.118 (Rewrite_Set ''norm_Rational'') eq_u)"
14.119 setup \<open>KEStore_Elems.add_mets
14.120 - [Specify.prep_met @{theory} "met_equ_fromfun" [] Spec.e_metID
14.121 + [Specify.prep_met @{theory} "met_equ_fromfun" [] Method.id_empty
14.122 (["Equation","fromFunction"],
14.123 [("#Given" ,["functionEq fu_n","substitution su_b"]),
14.124 ("#Find" ,["equality equ'''"])],
15.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Apr 22 11:23:30 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Apr 22 14:36:27 2020 +0200
15.3 @@ -239,8 +239,8 @@
15.4
15.5 (** problem types **)
15.6 setup \<open>KEStore_Elems.add_pbts
15.7 - [(Specify.prep_pbt thy "pbl_fun" [] Spec.e_pblID (["function"], [], Rule_Set.empty, NONE, [])),
15.8 - (Specify.prep_pbt thy "pbl_fun_deriv" [] Spec.e_pblID
15.9 + [(Specify.prep_pbt thy "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
15.10 + (Specify.prep_pbt thy "pbl_fun_deriv" [] Problem.id_empty
15.11 (["derivative_of","function"],
15.12 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
15.13 ("#Find" ,["derivative f_f'"])],
15.14 @@ -248,7 +248,7 @@
15.15 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
15.16 ["diff","after_simplification"]])),
15.17 (*here "named" is used differently from Integration"*)
15.18 - (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] Spec.e_pblID
15.19 + (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] Problem.id_empty
15.20 (["named","derivative_of","function"],
15.21 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
15.22 ("#Find" ,["derivativeEq f_f'"])],
15.23 @@ -272,7 +272,7 @@
15.24 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
15.25 \<close>
15.26 setup \<open>KEStore_Elems.add_mets
15.27 - [Specify.prep_met thy "met_diff" [] Spec.e_metID
15.28 + [Specify.prep_met thy "met_diff" [] Method.id_empty
15.29 (["diff"], [],
15.30 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
15.31 crls = Atools_erls, errpats = [], nrls = norm_diff},
15.32 @@ -307,7 +307,7 @@
15.33 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
15.34 ) f_f')"
15.35 setup \<open>KEStore_Elems.add_mets
15.36 - [Specify.prep_met thy "met_diff_onR" [] Spec.e_metID
15.37 + [Specify.prep_met thy "met_diff_onR" [] Method.id_empty
15.38 (["diff","differentiate_on_R"],
15.39 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
15.40 ("#Find" ,["derivative f_f'"])],
15.41 @@ -342,7 +342,7 @@
15.42 (Repeat (Rewrite_Set ''make_polynomial'')))
15.43 ) f_f')"
15.44 setup \<open>KEStore_Elems.add_mets
15.45 - [Specify.prep_met thy "met_diff_simpl" [] Spec.e_metID
15.46 + [Specify.prep_met thy "met_diff_simpl" [] Method.id_empty
15.47 (["diff","diff_simpl"],
15.48 [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
15.49 ("#Find" , ["derivative f_f'"])],
15.50 @@ -380,7 +380,7 @@
15.51 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
15.52 ) f_f')"
15.53 setup \<open>KEStore_Elems.add_mets
15.54 - [Specify.prep_met thy "met_diff_equ" [] Spec.e_metID
15.55 + [Specify.prep_met thy "met_diff_equ" [] Method.id_empty
15.56 (["diff","differentiate_equality"],
15.57 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
15.58 ("#Find" ,["derivativeEq f_f'"])],
15.59 @@ -403,7 +403,7 @@
15.60 ) term')"
15.61
15.62 setup \<open>KEStore_Elems.add_mets
15.63 - [Specify.prep_met thy "met_diff_after_simp" [] Spec.e_metID
15.64 + [Specify.prep_met thy "met_diff_after_simp" [] Method.id_empty
15.65 (["diff","after_simplification"],
15.66 [("#Given" ,["functionTerm term","differentiateFor bound_variable"]),
15.67 ("#Find" ,["derivative term'"])],
16.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Apr 22 11:23:30 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Wed Apr 22 14:36:27 2020 +0200
16.3 @@ -315,7 +315,7 @@
16.4 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
16.5 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
16.6 val (dI',pI',mI')=
16.7 - ("DiffAppl",["Program","maximum_of","function"],Spec.e_metID);
16.8 + ("DiffAppl",["Program","maximum_of","function"],Method.id_empty);
16.9 val c = []:cid;
16.10
16.11 (*
16.12 @@ -416,7 +416,7 @@
16.13 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
16.14 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
16.15 val (dI',pI',mI')=
16.16 - ("DiffAppl",["DiffAppl","test_maximum"],Spec.e_metID);
16.17 + ("DiffAppl",["DiffAppl","test_maximum"],Method.id_empty);
16.18 val p = e_pos'; val c = [];
16.19
16.20 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
17.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Apr 22 11:23:30 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Apr 22 14:36:27 2020 +0200
17.3 @@ -63,37 +63,37 @@
17.4
17.5 (** problem types **)
17.6 setup \<open>KEStore_Elems.add_pbts
17.7 - [(Specify.prep_pbt thy "pbl_fun_max" [] Spec.e_pblID
17.8 + [(Specify.prep_pbt thy "pbl_fun_max" [] Problem.id_empty
17.9 (["maximum_of","function"],
17.10 [("#Given" ,["fixedValues f_ix"]),
17.11 ("#Find" ,["maximum m_m","valuesFor v_s"]),
17.12 ("#Relate",["relations r_s"])],
17.13 Rule_Set.empty, NONE, [])),
17.14 - (Specify.prep_pbt thy "pbl_fun_make" [] Spec.e_pblID
17.15 + (Specify.prep_pbt thy "pbl_fun_make" [] Problem.id_empty
17.16 (["make","function"],
17.17 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
17.18 ("#Find" ,["functionEq f_1"])],
17.19 Rule_Set.empty, NONE, [])),
17.20 - (Specify.prep_pbt thy "pbl_fun_max_expl" [] Spec.e_pblID
17.21 + (Specify.prep_pbt thy "pbl_fun_max_expl" [] Problem.id_empty
17.22 (["by_explicit","make","function"],
17.23 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
17.24 ("#Find" ,["functionEq f_1"])],
17.25 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_explicit"]])),
17.26 - (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Spec.e_pblID
17.27 + (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Problem.id_empty
17.28 (["by_new_variable","make","function"],
17.29 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
17.30 (*WN.12.5.03: precond for distinction still missing*)
17.31 ("#Find" ,["functionEq f_1"])],
17.32 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_new_variable"]])),
17.33 - (Specify.prep_pbt thy "pbl_fun_max_interv" [] Spec.e_pblID
17.34 + (Specify.prep_pbt thy "pbl_fun_max_interv" [] Problem.id_empty
17.35 (["on_interval","maximum_of","function"],
17.36 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
17.37 (*WN.12.5.03: precond for distinction still missing*)
17.38 ("#Find" ,["maxArgument v_0"])],
17.39 Rule_Set.empty, NONE, [])),
17.40 - (Specify.prep_pbt thy "pbl_tool" [] Spec.e_pblID
17.41 + (Specify.prep_pbt thy "pbl_tool" [] Problem.id_empty
17.42 (["tool"], [], Rule_Set.empty, NONE, [])),
17.43 - (Specify.prep_pbt thy "pbl_tool_findvals" [] Spec.e_pblID
17.44 + (Specify.prep_pbt thy "pbl_tool_findvals" [] Problem.id_empty
17.45 (["find_values","tool"],
17.46 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
17.47 ("#Find" ,["valuesFor v_ls"]),
17.48 @@ -103,7 +103,7 @@
17.49
17.50 (** methods, scripts not yet implemented **)
17.51 setup \<open>KEStore_Elems.add_mets
17.52 - [Specify.prep_met thy "met_diffapp" [] Spec.e_metID
17.53 + [Specify.prep_met thy "met_diffapp" [] Method.id_empty
17.54 (["DiffApp"], [],
17.55 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
17.56 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
17.57 @@ -125,7 +125,7 @@
17.58 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
17.59 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
17.60 setup \<open>KEStore_Elems.add_mets
17.61 - [Specify.prep_met thy "met_diffapp_max" [] Spec.e_metID
17.62 + [Specify.prep_met thy "met_diffapp_max" [] Method.id_empty
17.63 (["DiffApp","max_by_calculus"],
17.64 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v",
17.65 "interval i_tv","errorBound e_rr"]),
17.66 @@ -152,7 +152,7 @@
17.67 [BOOL e_2, REAL v_2]
17.68 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
17.69 setup \<open>KEStore_Elems.add_mets
17.70 - [Specify.prep_met thy "met_diffapp_funnew" [] Spec.e_metID
17.71 + [Specify.prep_met thy "met_diffapp_funnew" [] Method.id_empty
17.72 (["DiffApp","make_fun_by_new_variable"],
17.73 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
17.74 ("#Find" ,["functionEq f_1"])],
17.75 @@ -172,7 +172,7 @@
17.76 [BOOL e_1, REAL v_1]
17.77 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
17.78 setup \<open>KEStore_Elems.add_mets
17.79 - [Specify.prep_met thy "met_diffapp_funexp" [] Spec.e_metID
17.80 + [Specify.prep_met thy "met_diffapp_funexp" [] Method.id_empty
17.81 (["DiffApp","make_fun_by_explicit"],
17.82 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
17.83 ("#Find" ,["functionEq f_1"])],
17.84 @@ -181,14 +181,14 @@
17.85 @{thm make_fun_by_explicit.simps})]
17.86 \<close>
17.87 setup \<open>KEStore_Elems.add_mets
17.88 - [Specify.prep_met thy "met_diffapp_max_oninterval" [] Spec.e_metID
17.89 + [Specify.prep_met thy "met_diffapp_max_oninterval" [] Method.id_empty
17.90 (["DiffApp","max_on_interval_by_calculus"],
17.91 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]),
17.92 ("#Find" ,["maxArgument v_0"])],
17.93 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
17.94 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
17.95 @{thm refl}),
17.96 - Specify.prep_met thy "met_diffapp_findvals" [] Spec.e_metID
17.97 + Specify.prep_met thy "met_diffapp_findvals" [] Method.id_empty
17.98 (["DiffApp","find_values"], [],
17.99 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
17.100 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
18.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed Apr 22 11:23:30 2020 +0200
18.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed Apr 22 14:36:27 2020 +0200
18.3 @@ -15,7 +15,7 @@
18.4
18.5 text \<open>problemclass for the usecase\<close>
18.6 setup \<open>KEStore_Elems.add_pbts
18.7 - [(Specify.prep_pbt thy "pbl_equ_dio" [] Spec.e_pblID
18.8 + [(Specify.prep_pbt thy "pbl_equ_dio" [] Problem.id_empty
18.9 (["diophantine","equation"],
18.10 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
18.11 (* TODO: drop ^^^^^*)
18.12 @@ -33,7 +33,7 @@
18.13 (Try (Calculate ''PLUS'')) #>
18.14 (Try (Calculate ''TIMES''))) e_e)"
18.15 setup \<open>KEStore_Elems.add_mets
18.16 - [Specify.prep_met thy "met_test_diophant" [] Spec.e_metID
18.17 + [Specify.prep_met thy "met_test_diophant" [] Method.id_empty
18.18 (["Test","solve_diophant"],
18.19 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
18.20 (* TODO: drop ^^^^^*)
19.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 22 11:23:30 2020 +0200
19.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 22 14:36:27 2020 +0200
19.3 @@ -406,18 +406,18 @@
19.4
19.5 (** problems **)
19.6 setup \<open>KEStore_Elems.add_pbts
19.7 - [(Specify.prep_pbt thy "pbl_equsys" [] Spec.e_pblID
19.8 + [(Specify.prep_pbt thy "pbl_equsys" [] Problem.id_empty
19.9 (["system"],
19.10 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.11 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
19.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
19.13 - (Specify.prep_pbt thy "pbl_equsys_lin" [] Spec.e_pblID
19.14 + (Specify.prep_pbt thy "pbl_equsys_lin" [] Problem.id_empty
19.15 (["LINEAR", "system"],
19.16 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.17 (*TODO.WN050929 check linearity*)
19.18 ("#Find" ,["solution ss'''"])],
19.19 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
19.20 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Spec.e_pblID
19.21 + (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Problem.id_empty
19.22 (["2x2", "LINEAR", "system"],
19.23 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
19.24 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.25 @@ -429,7 +429,7 @@
19.26 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.27 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
19.28 SOME "solveSystem e_s v_s", [])),
19.29 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Spec.e_pblID
19.30 + (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
19.31 (["triangular", "2x2", "LINEAR", "system"],
19.32 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.33 ("#Where",
19.34 @@ -437,14 +437,14 @@
19.35 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
19.36 ("#Find" ,["solution ss'''"])],
19.37 prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])),
19.38 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Spec.e_pblID
19.39 + (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
19.40 (["normalise", "2x2", "LINEAR", "system"],
19.41 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.42 ("#Find" ,["solution ss'''"])],
19.43 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
19.44 SOME "solveSystem e_s v_s",
19.45 [["EqSystem","normalise","2x2"]])),
19.46 - (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Spec.e_pblID
19.47 + (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Problem.id_empty
19.48 (["3x3", "LINEAR", "system"],
19.49 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
19.50 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.51 @@ -456,7 +456,7 @@
19.52 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.53 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
19.54 SOME "solveSystem e_s v_s", [])),
19.55 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Spec.e_pblID
19.56 + (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Problem.id_empty
19.57 (["4x4", "LINEAR", "system"],
19.58 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
19.59 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.60 @@ -468,7 +468,7 @@
19.61 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.62 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
19.63 SOME "solveSystem e_s v_s", [])),
19.64 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Spec.e_pblID
19.65 + (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
19.66 (["triangular", "4x4", "LINEAR", "system"],
19.67 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.68 ("#Where" , (*accepts missing variables up to diagional form*)
19.69 @@ -481,7 +481,7 @@
19.70 [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
19.71 SOME "solveSystem e_s v_s",
19.72 [["EqSystem","top_down_substitution","4x4"]])),
19.73 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Spec.e_pblID
19.74 + (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
19.75 (["normalise", "4x4", "LINEAR", "system"],
19.76 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.77 (*LENGTH is checked 1 level above*)
19.78 @@ -510,12 +510,12 @@
19.79
19.80 (**methods**)
19.81 setup \<open>KEStore_Elems.add_mets
19.82 - [Specify.prep_met thy "met_eqsys" [] Spec.e_metID
19.83 + [Specify.prep_met thy "met_eqsys" [] Method.id_empty
19.84 (["EqSystem"], [],
19.85 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
19.86 errpats = [], nrls = Rule_Set.Empty},
19.87 @{thm refl}),
19.88 - Specify.prep_met thy "met_eqsys_topdown" [] Spec.e_metID
19.89 + Specify.prep_met thy "met_eqsys_topdown" [] Method.id_empty
19.90 (["EqSystem","top_down_substitution"], [],
19.91 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
19.92 errpats = [], nrls = Rule_Set.Empty},
19.93 @@ -542,7 +542,7 @@
19.94 in
19.95 Try (Rewrite_Set ''order_system'' ) e__s) "
19.96 setup \<open>KEStore_Elems.add_mets
19.97 - [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Spec.e_metID
19.98 + [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Method.id_empty
19.99 (["EqSystem", "top_down_substitution", "2x2"],
19.100 [("#Given", ["equalities e_s", "solveForVars v_s"]),
19.101 ("#Where",
19.102 @@ -558,7 +558,7 @@
19.103 @{thm solve_system.simps})]
19.104 \<close>
19.105 setup \<open>KEStore_Elems.add_mets
19.106 - [Specify.prep_met thy "met_eqsys_norm" [] Spec.e_metID
19.107 + [Specify.prep_met thy "met_eqsys_norm" [] Method.id_empty
19.108 (["EqSystem", "normalise"], [],
19.109 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
19.110 errpats = [], nrls = Rule_Set.Empty},
19.111 @@ -580,7 +580,7 @@
19.112 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
19.113 [BOOL_LIST e__s, REAL_LIST v_s])"
19.114 setup \<open>KEStore_Elems.add_mets
19.115 - [Specify.prep_met thy "met_eqsys_norm_2x2" [] Spec.e_metID
19.116 + [Specify.prep_met thy "met_eqsys_norm_2x2" [] Method.id_empty
19.117 (["EqSystem","normalise","2x2"],
19.118 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.119 ("#Find" ,["solution ss'''"])],
19.120 @@ -612,7 +612,7 @@
19.121 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
19.122 [BOOL_LIST e__s, REAL_LIST v_s])"
19.123 setup \<open>KEStore_Elems.add_mets
19.124 - [Specify.prep_met thy "met_eqsys_norm_4x4" [] Spec.e_metID
19.125 + [Specify.prep_met thy "met_eqsys_norm_4x4" [] Method.id_empty
19.126 (["EqSystem","normalise","4x4"],
19.127 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.128 ("#Find" ,["solution ss'''"])],
19.129 @@ -644,7 +644,7 @@
19.130 in
19.131 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
19.132 setup \<open>KEStore_Elems.add_mets
19.133 - [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Spec.e_metID
19.134 + [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Method.id_empty
19.135 (["EqSystem","top_down_substitution","4x4"],
19.136 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
19.137 ("#Where" , (*accepts missing variables up to diagonal form*)
20.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Apr 22 11:23:30 2020 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Apr 22 14:36:27 2020 +0200
20.3 @@ -43,14 +43,14 @@
20.4 setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
20.5 (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} univariate_equation_prls))]\<close>
20.6 setup \<open>KEStore_Elems.add_pbts
20.7 - [(Specify.prep_pbt thy "pbl_equ" [] Spec.e_pblID
20.8 + [(Specify.prep_pbt thy "pbl_equ" [] Problem.id_empty
20.9 (["equation"],
20.10 [("#Given" ,["equality e_e","solveFor v_v"]),
20.11 ("#Where" ,["matches (?a = ?b) e_e"]),
20.12 ("#Find" ,["solutions v_v'i'"])],
20.13 Rule_Set.append_rules "equation_prls" Rule_Set.empty [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
20.14 SOME "solve (e_e::bool, v_v)", [])),
20.15 - (Specify.prep_pbt thy "pbl_equ_univ" [] Spec.e_pblID
20.16 + (Specify.prep_pbt thy "pbl_equ_univ" [] Problem.id_empty
20.17 (["univariate","equation"],
20.18 [("#Given" ,["equality e_e","solveFor v_v"]),
20.19 ("#Where" ,["matches (?a = ?b) e_e"]),
20.20 @@ -81,7 +81,7 @@
20.21
20.22
20.23 setup \<open>KEStore_Elems.add_mets
20.24 - [Specify.prep_met thy "met_equ" [] Spec.e_metID
20.25 + [Specify.prep_met thy "met_equ" [] Method.id_empty
20.26 (["Equation"], [],
20.27 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
20.28 errpats = [], nrls = Rule_Set.empty},
21.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Wed Apr 22 11:23:30 2020 +0200
21.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed Apr 22 14:36:27 2020 +0200
21.3 @@ -72,11 +72,11 @@
21.4
21.5 section \<open>problems\<close>
21.6 setup \<open>KEStore_Elems.add_pbts
21.7 - [(Specify.prep_pbt @{theory} "pbl_Programming" [] Spec.e_pblID
21.8 + [(Specify.prep_pbt @{theory} "pbl_Programming" [] Problem.id_empty
21.9 (["Programming"], [], Rule_Set.empty, NONE, [])),
21.10 - (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] Spec.e_pblID
21.11 + (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] Problem.id_empty
21.12 (["SORT","Programming"], [], Rule_Set.empty, NONE, [])),
21.13 - (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] Spec.e_pblID
21.14 + (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] Problem.id_empty
21.15 (["insertion","SORT","Programming"],
21.16 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
21.17 Rule_Set.empty,
21.18 @@ -85,11 +85,11 @@
21.19 section \<open>methods\<close>
21.20 (* TODO: implementation needs extra object-level lists ?!?*)
21.21 setup \<open>KEStore_Elems.add_mets
21.22 - [ Specify.prep_met @{theory} "met_Programming" [] Spec.e_metID
21.23 + [ Specify.prep_met @{theory} "met_Programming" [] Method.id_empty
21.24 (["Programming"], [],
21.25 {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
21.26 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
21.27 - Specify.prep_met @{theory} "met_Prog_sort" [] Spec.e_metID
21.28 + Specify.prep_met @{theory} "met_Prog_sort" [] Method.id_empty
21.29 (["Programming","SORT"], [],
21.30 {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
21.31 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},
21.32 @@ -104,7 +104,7 @@
21.33 in
21.34 (Rewrite_Set ''ins_sort'') uns)"
21.35 setup \<open>KEStore_Elems.add_mets
21.36 - [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Spec.e_metID
21.37 + [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Method.id_empty
21.38 (["Programming","SORT","insertion"],
21.39 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
21.40 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
21.41 @@ -134,7 +134,7 @@
21.42 (Repeat (Rewrite ''if_False'')))
21.43 ) uns)"
21.44 setup \<open>KEStore_Elems.add_mets
21.45 - [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Spec.e_metID
21.46 + [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Method.id_empty
21.47 (["Programming","SORT","insertion_steps"],
21.48 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
21.49 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
22.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 22 11:23:30 2020 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 22 14:36:27 2020 +0200
22.3 @@ -331,7 +331,7 @@
22.4
22.5 (** problems **)
22.6 setup \<open>KEStore_Elems.add_pbts
22.7 - [(Specify.prep_pbt thy "pbl_fun_integ" [] Spec.e_pblID
22.8 + [(Specify.prep_pbt thy "pbl_fun_integ" [] Problem.id_empty
22.9 (["integrate","function"],
22.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
22.11 ("#Find" ,["antiDerivative F_F"])],
22.12 @@ -339,7 +339,7 @@
22.13 SOME "Integrate (f_f, v_v)",
22.14 [["diff","integration"]])),
22.15 (*here "named" is used differently from Differentiation"*)
22.16 - (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Spec.e_pblID
22.17 + (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Problem.id_empty
22.18 (["named","integrate","function"],
22.19 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
22.20 ("#Find" ,["antiDerivativeName F_F"])],
22.21 @@ -357,7 +357,7 @@
22.22 in
22.23 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
22.24 setup \<open>KEStore_Elems.add_mets
22.25 - [Specify.prep_met thy "met_diffint" [] Spec.e_metID
22.26 + [Specify.prep_met thy "met_diffint" [] Method.id_empty
22.27 (["diff","integration"],
22.28 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
22.29 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
22.30 @@ -375,7 +375,7 @@
22.31 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
22.32 ) t_t)"
22.33 setup \<open>KEStore_Elems.add_mets
22.34 - [Specify.prep_met thy "met_diffint_named" [] Spec.e_metID
22.35 + [Specify.prep_met thy "met_diffint_named" [] Method.id_empty
22.36 (["diff","integration","named"],
22.37 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
22.38 ("#Find" ,["antiDerivativeName F_F"])],
23.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Apr 22 11:23:30 2020 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Apr 22 14:36:27 2020 +0200
23.3 @@ -46,10 +46,10 @@
23.4 val thy = @{theory};
23.5 \<close>
23.6 setup \<open>KEStore_Elems.add_pbts
23.7 - [(Specify.prep_pbt thy "pbl_SP" [] Spec.e_pblID (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
23.8 - (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Spec.e_pblID
23.9 + [(Specify.prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
23.10 + (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
23.11 (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])),
23.12 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Spec.e_pblID
23.13 + (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
23.14 (["Inverse", "Z_Transform", "SignalProcessing"],
23.15 [("#Given" , ["filterExpression X_eq"]),
23.16 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
23.17 @@ -59,11 +59,11 @@
23.18 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
23.19 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
23.20 setup \<open>KEStore_Elems.add_mets
23.21 - [Specify.prep_met thy "met_SP" [] Spec.e_metID
23.22 + [Specify.prep_met thy "met_SP" [] Method.id_empty
23.23 (["SignalProcessing"], [],
23.24 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
23.25 errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
23.26 - Specify.prep_met thy "met_SP_Ztrans" [] Spec.e_metID
23.27 + Specify.prep_met thy "met_SP_Ztrans" [] Method.id_empty
23.28 (["SignalProcessing", "Z_Transform"], [],
23.29 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
23.30 errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
23.31 @@ -87,7 +87,7 @@
23.32 [BOOL equ, REAL X_z]
23.33 in X) "
23.34 setup \<open>KEStore_Elems.add_mets
23.35 - [Specify.prep_met thy "met_SP_Ztrans_inv" [] Spec.e_metID
23.36 + [Specify.prep_met thy "met_SP_Ztrans_inv" [] Method.id_empty
23.37 (["SignalProcessing", "Z_Transform", "Inverse"],
23.38 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
23.39 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
23.40 @@ -115,7 +115,7 @@
23.41 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
23.42 in n_eq)"
23.43 setup \<open>KEStore_Elems.add_mets
23.44 - [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Spec.e_metID
23.45 + [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
23.46 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
23.47 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
23.48 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
24.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Apr 22 11:23:30 2020 +0200
24.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Apr 22 14:36:27 2020 +0200
24.3 @@ -114,7 +114,7 @@
24.4 (*----------------------------- problem types --------------------------------*)
24.5 (* ---------linear----------- *)
24.6 setup \<open>KEStore_Elems.add_pbts
24.7 - [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Spec.e_pblID
24.8 + [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Problem.id_empty
24.9 (["LINEAR", "univariate", "equation"],
24.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
24.11 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
24.12 @@ -127,7 +127,7 @@
24.13
24.14 (*-------------- methods------------------------------------------------------*)
24.15 setup \<open>KEStore_Elems.add_mets
24.16 - [Specify.prep_met thy "met_eqlin" [] Spec.e_metID
24.17 + [Specify.prep_met thy "met_eqlin" [] Method.id_empty
24.18 (["LinEq"], [],
24.19 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
24.20 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
24.21 @@ -151,7 +151,7 @@
24.22 in
24.23 Or_to_List e_e)"
24.24 setup \<open>KEStore_Elems.add_mets
24.25 - [Specify.prep_met thy "met_eq_lin" [] Spec.e_metID
24.26 + [Specify.prep_met thy "met_eq_lin" [] Method.id_empty
24.27 (["LinEq","solve_lineq_equation"],
24.28 [("#Given", ["equality e_e", "solveFor v_v"]),
24.29 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]),
25.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Apr 22 11:23:30 2020 +0200
25.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Apr 22 14:36:27 2020 +0200
25.3 @@ -22,7 +22,7 @@
25.4 \<close>
25.5 (** problems **)
25.6 setup \<open>KEStore_Elems.add_pbts
25.7 - [(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] Spec.e_pblID
25.8 + [(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] Problem.id_empty
25.9 (["logarithmic","univariate","equation"],
25.10 [("#Given",["equality e_e","solveFor v_v"]),
25.11 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
25.12 @@ -44,7 +44,7 @@
25.13 in
25.14 [e_e])"
25.15 setup \<open>KEStore_Elems.add_mets
25.16 - [Specify.prep_met thy "met_equ_log" [] Spec.e_metID
25.17 + [Specify.prep_met thy "met_equ_log" [] Method.id_empty
25.18 (["Equation","solve_log"],
25.19 [("#Given" ,["equality e_e","solveFor v_v"]),
25.20 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
26.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Apr 22 11:23:30 2020 +0200
26.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Apr 22 14:36:27 2020 +0200
26.3 @@ -148,7 +148,7 @@
26.4 Check_Unique.check_guhs_unique := false; (*WN120307 REMOVE after editing*)
26.5 \<close>
26.6 setup \<open>KEStore_Elems.add_pbts
26.7 - [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] Spec.e_pblID
26.8 + [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] Problem.id_empty
26.9 (["partial_fraction", "rational", "simplification"],
26.10 [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
26.11 (* TODO: call this sub-problem with appropriate functionTerm:
26.12 @@ -228,7 +228,7 @@
26.13 pbz = Substitute [AA = a, BB = b] pbz \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
26.14 in pbz) "
26.15 setup \<open>KEStore_Elems.add_mets
26.16 - [Specify.prep_met @{theory} "met_partial_fraction" [] Spec.e_metID
26.17 + [Specify.prep_met @{theory} "met_partial_fraction" [] Method.id_empty
26.18 (["simplification","of_rationals","to_partial_fraction"],
26.19 [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
26.20 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
27.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Apr 22 11:23:30 2020 +0200
27.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Apr 22 14:36:27 2020 +0200
27.3 @@ -1434,7 +1434,7 @@
27.4
27.5 subsection \<open>problems\<close>
27.6 setup \<open>KEStore_Elems.add_pbts
27.7 - [(Specify.prep_pbt thy "pbl_simp_poly" [] Spec.e_pblID
27.8 + [(Specify.prep_pbt thy "pbl_simp_poly" [] Problem.id_empty
27.9 (["polynomial","simplification"],
27.10 [("#Given" ,["Term t_t"]),
27.11 ("#Where" ,["t_t is_polyexp"]),
27.12 @@ -1450,7 +1450,7 @@
27.13 where
27.14 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
27.15 setup \<open>KEStore_Elems.add_mets
27.16 - [Specify.prep_met thy "met_simp_poly" [] Spec.e_metID
27.17 + [Specify.prep_met thy "met_simp_poly" [] Method.id_empty
27.18 (["simplification","for_polynomials"],
27.19 [("#Given" ,["Term t_t"]),
27.20 ("#Where" ,["t_t is_polyexp"]),
28.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 22 11:23:30 2020 +0200
28.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 22 14:36:27 2020 +0200
28.3 @@ -778,7 +778,7 @@
28.4 *)
28.5 \<close>
28.6 setup \<open>KEStore_Elems.add_pbts
28.7 - [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] Spec.e_pblID
28.8 + [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] Problem.id_empty
28.9 (["polynomial","univariate","equation"],
28.10 [("#Given" ,["equality e_e","solveFor v_v"]),
28.11 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
28.12 @@ -787,7 +787,7 @@
28.13 ("#Find" ,["solutions v_v'i'"])],
28.14 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
28.15 (*--- d0 ---*)
28.16 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] Spec.e_pblID
28.17 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] Problem.id_empty
28.18 (["degree_0","polynomial","univariate","equation"],
28.19 [("#Given" ,["equality e_e","solveFor v_v"]),
28.20 ("#Where" ,["matches (?a = 0) e_e",
28.21 @@ -796,7 +796,7 @@
28.22 ("#Find" ,["solutions v_v'i'"])],
28.23 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])),
28.24 (*--- d1 ---*)
28.25 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] Spec.e_pblID
28.26 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] Problem.id_empty
28.27 (["degree_1","polynomial","univariate","equation"],
28.28 [("#Given" ,["equality e_e","solveFor v_v"]),
28.29 ("#Where" ,["matches (?a = 0) e_e",
28.30 @@ -805,7 +805,7 @@
28.31 ("#Find" ,["solutions v_v'i'"])],
28.32 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])),
28.33 (*--- d2 ---*)
28.34 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] Spec.e_pblID
28.35 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] Problem.id_empty
28.36 (["degree_2","polynomial","univariate","equation"],
28.37 [("#Given" ,["equality e_e","solveFor v_v"]),
28.38 ("#Where" ,["matches (?a = 0) e_e",
28.39 @@ -813,7 +813,7 @@
28.40 "((lhs e_e) has_degree_in v_v ) = 2"]),
28.41 ("#Find" ,["solutions v_v'i'"])],
28.42 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])),
28.43 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] Spec.e_pblID
28.44 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
28.45 (["sq_only","degree_2","polynomial","univariate","equation"],
28.46 [("#Given" ,["equality e_e","solveFor v_v"]),
28.47 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_e | " ^
28.48 @@ -831,7 +831,7 @@
28.49 ("#Find" ,["solutions v_v'i'"])],
28.50 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
28.51 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),
28.52 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] Spec.e_pblID
28.53 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
28.54 (["bdv_only","degree_2","polynomial","univariate","equation"],
28.55 [("#Given", ["equality e_e","solveFor v_v"]),
28.56 ("#Where", ["matches (?a*?v_ + ?v_^^^2 = 0) e_e | " ^
28.57 @@ -843,14 +843,14 @@
28.58 ("#Find", ["solutions v_v'i'"])],
28.59 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
28.60 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),
28.61 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] Spec.e_pblID
28.62 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
28.63 (["pqFormula","degree_2","polynomial","univariate","equation"],
28.64 [("#Given", ["equality e_e","solveFor v_v"]),
28.65 ("#Where", ["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
28.66 "matches (?a + ?v_^^^2 = 0) e_e"]),
28.67 ("#Find", ["solutions v_v'i'"])],
28.68 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])),
28.69 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] Spec.e_pblID
28.70 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
28.71 (["abcFormula","degree_2","polynomial","univariate","equation"],
28.72 [("#Given", ["equality e_e","solveFor v_v"]),
28.73 ("#Where", ["matches (?a + ?v_^^^2 = 0) e_e | " ^
28.74 @@ -858,7 +858,7 @@
28.75 ("#Find", ["solutions v_v'i'"])],
28.76 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])),
28.77 (*--- d3 ---*)
28.78 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] Spec.e_pblID
28.79 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] Problem.id_empty
28.80 (["degree_3","polynomial","univariate","equation"],
28.81 [("#Given", ["equality e_e","solveFor v_v"]),
28.82 ("#Where", ["matches (?a = 0) e_e",
28.83 @@ -867,7 +867,7 @@
28.84 ("#Find", ["solutions v_v'i'"])],
28.85 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])),
28.86 (*--- d4 ---*)
28.87 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] Spec.e_pblID
28.88 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] Problem.id_empty
28.89 (["degree_4","polynomial","univariate","equation"],
28.90 [("#Given", ["equality e_e","solveFor v_v"]),
28.91 ("#Where", ["matches (?a = 0) e_e",
28.92 @@ -876,7 +876,7 @@
28.93 ("#Find", ["solutions v_v'i'"])],
28.94 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),
28.95 (*--- normalise ---*)
28.96 - (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] Spec.e_pblID
28.97 + (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] Problem.id_empty
28.98 (["normalise","polynomial","univariate","equation"],
28.99 [("#Given", ["equality e_e","solveFor v_v"]),
28.100 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
28.101 @@ -884,7 +884,7 @@
28.102 ("#Find", ["solutions v_v'i'"])],
28.103 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "normalise_poly"]])),
28.104 (*-------------------------expanded-----------------------*)
28.105 - (Specify.prep_pbt thy "pbl_equ_univ_expand" [] Spec.e_pblID
28.106 + (Specify.prep_pbt thy "pbl_equ_univ_expand" [] Problem.id_empty
28.107 (["expanded","univariate","equation"],
28.108 [("#Given", ["equality e_e","solveFor v_v"]),
28.109 ("#Where", ["matches (?a = 0) e_e",
28.110 @@ -892,7 +892,7 @@
28.111 ("#Find", ["solutions v_v'i'"])],
28.112 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
28.113 (*--- d2 ---*)
28.114 - (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] Spec.e_pblID
28.115 + (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] Problem.id_empty
28.116 (["degree_2","expanded","univariate","equation"],
28.117 [("#Given", ["equality e_e","solveFor v_v"]),
28.118 ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
28.119 @@ -901,7 +901,7 @@
28.120
28.121 text \<open>"-------------------------methods-----------------------"\<close>
28.122 setup \<open>KEStore_Elems.add_mets
28.123 - [Specify.prep_met thy "met_polyeq" [] Spec.e_metID
28.124 + [Specify.prep_met thy "met_polyeq" [] Method.id_empty
28.125 (["PolyEq"], [],
28.126 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
28.127 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
28.128 @@ -922,7 +922,7 @@
28.129 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
28.130 [BOOL e_e, REAL v_v])"
28.131 setup \<open>KEStore_Elems.add_mets
28.132 - [Specify.prep_met thy "met_polyeq_norm" [] Spec.e_metID
28.133 + [Specify.prep_met thy "met_polyeq_norm" [] Method.id_empty
28.134 (["PolyEq", "normalise_poly"],
28.135 [("#Given" ,["equality e_e","solveFor v_v"]),
28.136 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
28.137 @@ -940,7 +940,7 @@
28.138 in
28.139 Or_to_List e_e)"
28.140 setup \<open>KEStore_Elems.add_mets
28.141 - [Specify.prep_met thy "met_polyeq_d0" [] Spec.e_metID
28.142 + [Specify.prep_met thy "met_polyeq_d0" [] Method.id_empty
28.143 (["PolyEq","solve_d0_polyeq_equation"],
28.144 [("#Given" ,["equality e_e","solveFor v_v"]),
28.145 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
28.146 @@ -963,7 +963,7 @@
28.147 in
28.148 Check_elementwise L_L {(v_v::real). Assumptions})"
28.149 setup \<open>KEStore_Elems.add_mets
28.150 - [Specify.prep_met thy "met_polyeq_d1" [] Spec.e_metID
28.151 + [Specify.prep_met thy "met_polyeq_d1" [] Method.id_empty
28.152 (["PolyEq","solve_d1_polyeq_equation"],
28.153 [("#Given" ,["equality e_e","solveFor v_v"]),
28.154 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
28.155 @@ -988,7 +988,7 @@
28.156 in
28.157 Check_elementwise L_L {(v_v::real). Assumptions})"
28.158 setup \<open>KEStore_Elems.add_mets
28.159 - [Specify.prep_met thy "met_polyeq_d22" [] Spec.e_metID
28.160 + [Specify.prep_met thy "met_polyeq_d22" [] Method.id_empty
28.161 (["PolyEq","solve_d2_polyeq_equation"],
28.162 [("#Given" ,["equality e_e","solveFor v_v"]),
28.163 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
28.164 @@ -1013,7 +1013,7 @@
28.165 in
28.166 Check_elementwise L_L {(v_v::real). Assumptions})"
28.167 setup \<open>KEStore_Elems.add_mets
28.168 - [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Spec.e_metID
28.169 + [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Method.id_empty
28.170 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
28.171 [("#Given" ,["equality e_e","solveFor v_v"]),
28.172 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
28.173 @@ -1036,7 +1036,7 @@
28.174 in
28.175 Check_elementwise L_L {(v_v::real). Assumptions})"
28.176 setup \<open>KEStore_Elems.add_mets
28.177 - [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Spec.e_metID
28.178 + [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Method.id_empty
28.179 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
28.180 [("#Given" ,["equality e_e","solveFor v_v"]),
28.181 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
28.182 @@ -1059,7 +1059,7 @@
28.183 in
28.184 Check_elementwise L_L {(v_v::real). Assumptions})"
28.185 setup \<open>KEStore_Elems.add_mets
28.186 - [Specify.prep_met thy "met_polyeq_d2_pq" [] Spec.e_metID
28.187 + [Specify.prep_met thy "met_polyeq_d2_pq" [] Method.id_empty
28.188 (["PolyEq","solve_d2_polyeq_pq_equation"],
28.189 [("#Given" ,["equality e_e","solveFor v_v"]),
28.190 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
28.191 @@ -1081,7 +1081,7 @@
28.192 L_L = Or_to_List e_e
28.193 in Check_elementwise L_L {(v_v::real). Assumptions})"
28.194 setup \<open>KEStore_Elems.add_mets
28.195 - [Specify.prep_met thy "met_polyeq_d2_abc" [] Spec.e_metID
28.196 + [Specify.prep_met thy "met_polyeq_d2_abc" [] Method.id_empty
28.197 (["PolyEq","solve_d2_polyeq_abc_equation"],
28.198 [("#Given" ,["equality e_e","solveFor v_v"]),
28.199 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
28.200 @@ -1108,7 +1108,7 @@
28.201 in
28.202 Check_elementwise L_L {(v_v::real). Assumptions})"
28.203 setup \<open>KEStore_Elems.add_mets
28.204 - [Specify.prep_met thy "met_polyeq_d3" [] Spec.e_metID
28.205 + [Specify.prep_met thy "met_polyeq_d3" [] Method.id_empty
28.206 (["PolyEq","solve_d3_polyeq_equation"],
28.207 [("#Given" ,["equality e_e","solveFor v_v"]),
28.208 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
28.209 @@ -1138,7 +1138,7 @@
28.210 in
28.211 Or_to_List e_e)"
28.212 setup \<open>KEStore_Elems.add_mets
28.213 - [Specify.prep_met thy "met_polyeq_complsq" [] Spec.e_metID
28.214 + [Specify.prep_met thy "met_polyeq_complsq" [] Method.id_empty
28.215 (["PolyEq","complete_square"],
28.216 [("#Given" ,["equality e_e","solveFor v_v"]),
28.217 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
29.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Apr 22 11:23:30 2020 +0200
29.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Apr 22 14:36:27 2020 +0200
29.3 @@ -392,9 +392,9 @@
29.4
29.5 (** problems **)
29.6 setup \<open>KEStore_Elems.add_pbts
29.7 - [(Specify.prep_pbt thy "pbl_vereinf_poly" [] Spec.e_pblID
29.8 + [(Specify.prep_pbt thy "pbl_vereinf_poly" [] Problem.id_empty
29.9 (["polynom","vereinfachen"], [], Rule_Set.Empty, NONE, [])),
29.10 - (Specify.prep_pbt thy "pbl_vereinf_poly_minus" [] Spec.e_pblID
29.11 + (Specify.prep_pbt thy "pbl_vereinf_poly_minus" [] Problem.id_empty
29.12 (["plus_minus","polynom","vereinfachen"],
29.13 [("#Given", ["Term t_t"]),
29.14 ("#Where", ["t_t is_polyexp",
29.15 @@ -419,7 +419,7 @@
29.16 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
29.17 (*"(~ False) = True"*)],
29.18 SOME "Vereinfache t_t", [["simplification","for_polynomials","with_minus"]])),
29.19 - (Specify.prep_pbt thy "pbl_vereinf_poly_klammer" [] Spec.e_pblID
29.20 + (Specify.prep_pbt thy "pbl_vereinf_poly_klammer" [] Problem.id_empty
29.21 (["klammer","polynom","vereinfachen"],
29.22 [("#Given" ,["Term t_t"]),
29.23 ("#Where" ,["t_t is_polyexp",
29.24 @@ -441,7 +441,7 @@
29.25 (*"(~ False) = True"*)],
29.26 SOME "Vereinfache t_t",
29.27 [["simplification","for_polynomials","with_parentheses"]])),
29.28 - (Specify.prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] Spec.e_pblID
29.29 + (Specify.prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
29.30 (["binom_klammer","polynom","vereinfachen"],
29.31 [("#Given", ["Term t_t"]),
29.32 ("#Where", ["t_t is_polyexp"]),
29.33 @@ -450,8 +450,8 @@
29.34 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
29.35 SOME "Vereinfache t_t",
29.36 [["simplification","for_polynomials","with_parentheses_mult"]])),
29.37 - (Specify.prep_pbt thy "pbl_probe" [] Spec.e_pblID (["probe"], [], Rule_Set.Empty, NONE, [])),
29.38 - (Specify.prep_pbt thy "pbl_probe_poly" [] Spec.e_pblID
29.39 + (Specify.prep_pbt thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
29.40 + (Specify.prep_pbt thy "pbl_probe_poly" [] Problem.id_empty
29.41 (["polynom","probe"],
29.42 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
29.43 ("#Where", ["e_e is_polyexp"]),
29.44 @@ -460,7 +460,7 @@
29.45 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
29.46 SOME "Probe e_e w_w",
29.47 [["probe","fuer_polynom"]])),
29.48 - (Specify.prep_pbt thy "pbl_probe_bruch" [] Spec.e_pblID
29.49 + (Specify.prep_pbt thy "pbl_probe_bruch" [] Problem.id_empty
29.50 (["bruch","probe"],
29.51 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
29.52 ("#Where" ,["e_e is_ratpolyexp"]),
29.53 @@ -480,7 +480,7 @@
29.54 (Try (Rewrite_Set ''verschoenere'')))
29.55 ) t_t)"
29.56 setup \<open>KEStore_Elems.add_mets
29.57 - [Specify.prep_met thy "met_simp_poly_minus" [] Spec.e_metID
29.58 + [Specify.prep_met thy "met_simp_poly_minus" [] Method.id_empty
29.59 (["simplification","for_polynomials","with_minus"],
29.60 [("#Given" ,["Term t_t"]),
29.61 ("#Where" ,["t_t is_polyexp",
29.62 @@ -515,7 +515,7 @@
29.63 (Try (Rewrite_Set ''verschoenere'')))
29.64 ) t_t)"
29.65 setup \<open>KEStore_Elems.add_mets
29.66 - [Specify.prep_met thy "met_simp_poly_parenth" [] Spec.e_metID
29.67 + [Specify.prep_met thy "met_simp_poly_parenth" [] Method.id_empty
29.68 (["simplification","for_polynomials","with_parentheses"],
29.69 [("#Given" ,["Term t_t"]),
29.70 ("#Where" ,["t_t is_polyexp"]),
29.71 @@ -540,7 +540,7 @@
29.72 (Try (Rewrite_Set ''verschoenere'')))
29.73 ) t_t)"
29.74 setup \<open>KEStore_Elems.add_mets
29.75 - [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Spec.e_metID
29.76 + [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Method.id_empty
29.77 (["simplification","for_polynomials","with_parentheses_mult"],
29.78 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
29.79 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
29.80 @@ -550,7 +550,7 @@
29.81 @{thm simplify3.simps})]
29.82 \<close>
29.83 setup \<open>KEStore_Elems.add_mets
29.84 - [Specify.prep_met thy "met_probe" [] Spec.e_metID
29.85 + [Specify.prep_met thy "met_probe" [] Method.id_empty
29.86 (["probe"], [],
29.87 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
29.88 errpats = [], nrls = Rule_Set.Empty},
29.89 @@ -570,7 +570,7 @@
29.90 (Try (Repeat (Calculate ''MINUS''))))
29.91 ) e_e)"
29.92 setup \<open>KEStore_Elems.add_mets
29.93 - [Specify.prep_met thy "met_probe_poly" [] Spec.e_metID
29.94 + [Specify.prep_met thy "met_probe_poly" [] Method.id_empty
29.95 (["probe","fuer_polynom"],
29.96 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
29.97 ("#Where" ,["e_e is_polyexp"]),
29.98 @@ -582,7 +582,7 @@
29.99 @{thm mache_probe.simps})]
29.100 \<close>
29.101 setup \<open>KEStore_Elems.add_mets
29.102 - [Specify.prep_met thy "met_probe_bruch" [] Spec.e_metID
29.103 + [Specify.prep_met thy "met_probe_bruch" [] Method.id_empty
29.104 (["probe","fuer_bruch"],
29.105 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
29.106 ("#Where" ,["e_e is_ratpolyexp"]),
30.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Apr 22 11:23:30 2020 +0200
30.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Apr 22 14:36:27 2020 +0200
30.3 @@ -161,7 +161,7 @@
30.4
30.5 subsection \<open>problems\<close>
30.6 setup \<open>KEStore_Elems.add_pbts
30.7 - [(Specify.prep_pbt thy "pbl_equ_univ_rat" [] Spec.e_pblID
30.8 + [(Specify.prep_pbt thy "pbl_equ_univ_rat" [] Problem.id_empty
30.9 (["rational","univariate","equation"],
30.10 [("#Given", ["equality e_e","solveFor v_v"]),
30.11 ("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),
30.12 @@ -170,7 +170,7 @@
30.13
30.14 subsection \<open>methods\<close>
30.15 setup \<open>KEStore_Elems.add_mets
30.16 - [Specify.prep_met thy "met_rateq" [] Spec.e_metID
30.17 + [Specify.prep_met thy "met_rateq" [] Method.id_empty
30.18 (["RatEq"], [],
30.19 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
30.20 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>
30.21 @@ -188,7 +188,7 @@
30.22 in
30.23 Check_elementwise L_L {(v_v::real). Assumptions})"
30.24 setup \<open>KEStore_Elems.add_mets
30.25 - [Specify.prep_met thy "met_rat_eq" [] Spec.e_metID
30.26 + [Specify.prep_met thy "met_rat_eq" [] Method.id_empty
30.27 (["RatEq", "solve_rat_equation"],
30.28 [("#Given" ,["equality e_e","solveFor v_v"]),
30.29 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
31.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Apr 22 11:23:30 2020 +0200
31.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Apr 22 14:36:27 2020 +0200
31.3 @@ -877,7 +877,7 @@
31.4
31.5 section \<open>A problem for simplification of rationals\<close>
31.6 setup \<open>KEStore_Elems.add_pbts
31.7 - [(Specify.prep_pbt thy "pbl_simp_rat" [] Spec.e_pblID
31.8 + [(Specify.prep_pbt thy "pbl_simp_rat" [] Problem.id_empty
31.9 (["rational","simplification"],
31.10 [("#Given" ,["Term t_t"]),
31.11 ("#Where" ,["t_t is_ratpolyexp"]),
31.12 @@ -905,7 +905,7 @@
31.13 Try (Rewrite_Set ''discard_parentheses1''))
31.14 term)"
31.15 setup \<open>KEStore_Elems.add_mets
31.16 - [Specify.prep_met thy "met_simp_rat" [] Spec.e_metID
31.17 + [Specify.prep_met thy "met_simp_rat" [] Method.id_empty
31.18 (["simplification","of_rationals"],
31.19 [("#Given" ,["Term t_t"]),
31.20 ("#Where" ,["t_t is_ratpolyexp"]),
32.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Apr 22 11:23:30 2020 +0200
32.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Apr 22 14:36:27 2020 +0200
32.3 @@ -444,7 +444,7 @@
32.4 subsection \<open>problems\<close>
32.5 setup \<open>KEStore_Elems.add_pbts
32.6 (* ---------root----------- *)
32.7 - [(Specify.prep_pbt thy "pbl_equ_univ_root" [] Spec.e_pblID
32.8 + [(Specify.prep_pbt thy "pbl_equ_univ_root" [] Problem.id_empty
32.9 (["rootX","univariate","equation"],
32.10 [("#Given" ,["equality e_e","solveFor v_v"]),
32.11 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
32.12 @@ -452,7 +452,7 @@
32.13 ("#Find" ,["solutions v_v'i'"])],
32.14 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
32.15 (* ---------sqrt----------- *)
32.16 - (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] Spec.e_pblID
32.17 + (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] Problem.id_empty
32.18 (["sq","rootX","univariate","equation"],
32.19 [("#Given" ,["equality e_e","solveFor v_v"]),
32.20 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
32.21 @@ -462,7 +462,7 @@
32.22 ("#Find" ,["solutions v_v'i'"])],
32.23 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
32.24 (* ---------normalise----------- *)
32.25 - (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] Spec.e_pblID
32.26 + (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] Problem.id_empty
32.27 (["normalise","rootX","univariate","equation"],
32.28 [("#Given" ,["equality e_e","solveFor v_v"]),
32.29 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
32.30 @@ -474,7 +474,7 @@
32.31
32.32 subsection \<open>methods\<close>
32.33 setup \<open>KEStore_Elems.add_mets
32.34 - [Specify.prep_met thy "met_rooteq" [] Spec.e_metID
32.35 + [Specify.prep_met thy "met_rooteq" [] Method.id_empty
32.36 (["RootEq"], [],
32.37 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
32.38 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
32.39 @@ -495,7 +495,7 @@
32.40 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
32.41 [BOOL e_e, REAL v_v])"
32.42 setup \<open>KEStore_Elems.add_mets
32.43 - [Specify.prep_met thy "met_rooteq_norm" [] Spec.e_metID
32.44 + [Specify.prep_met thy "met_rooteq_norm" [] Method.id_empty
32.45 (["RootEq","norm_sq_root_equation"],
32.46 [("#Given" ,["equality e_e","solveFor v_v"]),
32.47 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
32.48 @@ -528,7 +528,7 @@
32.49 [BOOL e_e, REAL v_v])
32.50 in Check_elementwise L_L {(v_v::real). Assumptions})"
32.51 setup \<open>KEStore_Elems.add_mets
32.52 - [Specify.prep_met thy "met_rooteq_sq" [] Spec.e_metID
32.53 + [Specify.prep_met thy "met_rooteq_sq" [] Method.id_empty
32.54 (["RootEq", "solve_sq_root_equation"],
32.55 [("#Given" ,["equality e_e", "solveFor v_v"]),
32.56 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
32.57 @@ -560,7 +560,7 @@
32.58 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
32.59 [BOOL e_e, REAL v_v])"
32.60 setup \<open>KEStore_Elems.add_mets
32.61 - [Specify.prep_met thy "met_rooteq_sq_right" [] Spec.e_metID
32.62 + [Specify.prep_met thy "met_rooteq_sq_right" [] Method.id_empty
32.63 (["RootEq","solve_right_sq_root_equation"],
32.64 [("#Given" ,["equality e_e","solveFor v_v"]),
32.65 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
32.66 @@ -589,7 +589,7 @@
32.67 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
32.68 [BOOL e_e, REAL v_v])"
32.69 setup \<open>KEStore_Elems.add_mets
32.70 - [Specify.prep_met thy "met_rooteq_sq_left" [] Spec.e_metID
32.71 + [Specify.prep_met thy "met_rooteq_sq_left" [] Method.id_empty
32.72 (["RootEq","solve_left_sq_root_equation"],
32.73 [("#Given" ,["equality e_e","solveFor v_v"]),
32.74 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
33.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Apr 22 11:23:30 2020 +0200
33.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Apr 22 14:36:27 2020 +0200
33.3 @@ -129,7 +129,7 @@
33.4 *)
33.5 \<close>
33.6 setup \<open>KEStore_Elems.add_pbts
33.7 - [(Specify.prep_pbt thy "pbl_equ_univ_root_sq_rat" [] Spec.e_pblID
33.8 + [(Specify.prep_pbt thy "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
33.9 (["rat","sq","rootX","univariate","equation"],
33.10 [("#Given" ,["equality e_e","solveFor v_v"]),
33.11 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
33.12 @@ -139,7 +139,7 @@
33.13
33.14 subsection \<open>methods\<close>
33.15 setup \<open>KEStore_Elems.add_mets
33.16 - [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Spec.e_metID
33.17 + [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Method.id_empty
33.18 (["RootRatEq"], [],
33.19 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
33.20 crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]
33.21 @@ -157,7 +157,7 @@
33.22 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
33.23 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
33.24 setup \<open>KEStore_Elems.add_mets
33.25 - [Specify.prep_met thy "met_rootrateq_elim" [] Spec.e_metID
33.26 + [Specify.prep_met thy "met_rootrateq_elim" [] Method.id_empty
33.27 (["RootRatEq","elim_rootrat_equation"],
33.28 [("#Given" ,["equality e_e","solveFor v_v"]),
33.29 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
34.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed Apr 22 11:23:30 2020 +0200
34.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed Apr 22 14:36:27 2020 +0200
34.3 @@ -25,12 +25,12 @@
34.4 \<close>
34.5 (** problems **)
34.6 setup \<open>KEStore_Elems.add_pbts
34.7 - [(Specify.prep_pbt thy "pbl_simp" [] Spec.e_pblID
34.8 + [(Specify.prep_pbt thy "pbl_simp" [] Problem.id_empty
34.9 (["simplification"],
34.10 [("#Given" ,["Term t_t"]),
34.11 ("#Find" ,["normalform n_n"])],
34.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])),
34.13 - (Specify.prep_pbt thy "pbl_vereinfache" [] Spec.e_pblID
34.14 + (Specify.prep_pbt thy "pbl_vereinfache" [] Problem.id_empty
34.15 (["vereinfachen"],
34.16 [("#Given", ["Term t_t"]),
34.17 ("#Find", ["normalform n_n"])],
34.18 @@ -38,7 +38,7 @@
34.19
34.20 (** methods **)
34.21 setup \<open>KEStore_Elems.add_mets
34.22 - [Specify.prep_met thy "met_tsimp" [] Spec.e_metID
34.23 + [Specify.prep_met thy "met_tsimp" [] Method.id_empty
34.24 (["simplification"],
34.25 [("#Given" ,["Term t_t"]),
34.26 ("#Find" ,["normalform n_n"])],
35.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Apr 22 11:23:30 2020 +0200
35.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Apr 22 14:36:27 2020 +0200
35.3 @@ -570,20 +570,20 @@
35.4 subsection \<open>problems\<close>
35.5 (** problem types **)
35.6 setup \<open>KEStore_Elems.add_pbts
35.7 - [(Specify.prep_pbt thy "pbl_test" [] Spec.e_pblID (["test"], [], Rule_Set.empty, NONE, [])),
35.8 - (Specify.prep_pbt thy "pbl_test_equ" [] Spec.e_pblID
35.9 + [(Specify.prep_pbt thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
35.10 + (Specify.prep_pbt thy "pbl_test_equ" [] Problem.id_empty
35.11 (["equation","test"],
35.12 [("#Given" ,["equality e_e","solveFor v_v"]),
35.13 ("#Where" ,["matches (?a = ?b) e_e"]),
35.14 ("#Find" ,["solutions v_v'i'"])],
35.15 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
35.16 - (Specify.prep_pbt thy "pbl_test_uni" [] Spec.e_pblID
35.17 + (Specify.prep_pbt thy "pbl_test_uni" [] Problem.id_empty
35.18 (["univariate","equation","test"],
35.19 [("#Given" ,["equality e_e","solveFor v_v"]),
35.20 ("#Where" ,["matches (?a = ?b) e_e"]),
35.21 ("#Find" ,["solutions v_v'i'"])],
35.22 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
35.23 - (Specify.prep_pbt thy "pbl_test_uni_lin" [] Spec.e_pblID
35.24 + (Specify.prep_pbt thy "pbl_test_uni_lin" [] Problem.id_empty
35.25 (["LINEAR","univariate","equation","test"],
35.26 [("#Given" ,["equality e_e","solveFor v_v"]),
35.27 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
35.28 @@ -772,7 +772,7 @@
35.29
35.30 section \<open>problems\<close>
35.31 setup \<open>KEStore_Elems.add_pbts
35.32 - [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Spec.e_pblID
35.33 + [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Problem.id_empty
35.34 (["plain_square","univariate","equation","test"],
35.35 [("#Given" ,["equality e_e","solveFor v_v"]),
35.36 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
35.37 @@ -782,28 +782,28 @@
35.38 ("#Find" ,["solutions v_v'i'"])],
35.39 assoc_rls' @{theory} "matches",
35.40 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])),
35.41 - (Specify.prep_pbt thy "pbl_test_uni_poly" [] Spec.e_pblID
35.42 + (Specify.prep_pbt thy "pbl_test_uni_poly" [] Problem.id_empty
35.43 (["polynomial","univariate","equation","test"],
35.44 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
35.45 ("#Where" ,["HOL.False"]),
35.46 ("#Find" ,["solutions v_v'i'"])],
35.47 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
35.48 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Spec.e_pblID
35.49 + (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Problem.id_empty
35.50 (["degree_two","polynomial","univariate","equation","test"],
35.51 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
35.52 ("#Find" ,["solutions v_v'i'"])],
35.53 Rule_Set.empty, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
35.54 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Spec.e_pblID
35.55 + (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
35.56 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
35.57 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
35.58 ("#Find" ,["solutions v_v'i'"])],
35.59 Rule_Set.empty, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
35.60 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Spec.e_pblID
35.61 + (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
35.62 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
35.63 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
35.64 ("#Find" ,["solutions v_v'i'"])],
35.65 Rule_Set.empty, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
35.66 - (Specify.prep_pbt thy "pbl_test_uni_root" [] Spec.e_pblID
35.67 + (Specify.prep_pbt thy "pbl_test_uni_root" [] Problem.id_empty
35.68 (["squareroot","univariate","equation","test"],
35.69 [("#Given" ,["equality e_e","solveFor v_v"]),
35.70 ("#Where" ,["precond_rootpbl v_v"]),
35.71 @@ -811,19 +811,19 @@
35.72 Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains'_root",
35.73 eval_contains_root "#contains_root_")],
35.74 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
35.75 - (Specify.prep_pbt thy "pbl_test_uni_norm" [] Spec.e_pblID
35.76 + (Specify.prep_pbt thy "pbl_test_uni_norm" [] Problem.id_empty
35.77 (["normalise","univariate","equation","test"],
35.78 [("#Given" ,["equality e_e","solveFor v_v"]),
35.79 ("#Where" ,[]),
35.80 ("#Find" ,["solutions v_v'i'"])],
35.81 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
35.82 - (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Spec.e_pblID
35.83 + (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Problem.id_empty
35.84 (["sqroot-test","univariate","equation","test"],
35.85 [("#Given" ,["equality e_e","solveFor v_v"]),
35.86 ("#Where" ,["precond_rootpbl v_v"]),
35.87 ("#Find" ,["solutions v_v'i'"])],
35.88 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
35.89 - (Specify.prep_pbt thy "pbl_test_intsimp" [] Spec.e_pblID
35.90 + (Specify.prep_pbt thy "pbl_test_intsimp" [] Problem.id_empty
35.91 (["inttype","test"],
35.92 [("#Given" ,["intTestGiven t_t"]),
35.93 ("#Where" ,[]),
35.94 @@ -833,7 +833,7 @@
35.95 section \<open>methods\<close>
35.96 subsection \<open>differentiate\<close>
35.97 setup \<open>KEStore_Elems.add_mets
35.98 - [Specify.prep_met @{theory "Diff"} "met_test" [] Spec.e_metID
35.99 + [Specify.prep_met @{theory "Diff"} "met_test" [] Method.id_empty
35.100 (["Test"], [],
35.101 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
35.102 crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
35.103 @@ -849,7 +849,7 @@
35.104 in
35.105 [e_e])"
35.106 setup \<open>KEStore_Elems.add_mets
35.107 - [Specify.prep_met thy "met_test_solvelin" [] Spec.e_metID
35.108 + [Specify.prep_met thy "met_test_solvelin" [] Method.id_empty
35.109 (["Test","solve_linear"],
35.110 [("#Given" ,["equality e_e","solveFor v_v"]),
35.111 ("#Where" ,["matches (?a = ?b) e_e"]),
35.112 @@ -880,7 +880,7 @@
35.113 in
35.114 [e_e])"
35.115 setup \<open>KEStore_Elems.add_mets
35.116 - [Specify.prep_met thy "met_test_sqrt" [] Spec.e_metID
35.117 + [Specify.prep_met thy "met_test_sqrt" [] Method.id_empty
35.118 (*root-equation, version for tests before 8.01.01*)
35.119 (["Test","sqrt-equ-test"],
35.120 [("#Given" ,["equality e_e","solveFor v_v"]),
35.121 @@ -908,7 +908,7 @@
35.122 in
35.123 Check_elementwise L_L {(v_v::real). Assumptions})"
35.124 setup \<open>KEStore_Elems.add_mets
35.125 - [Specify.prep_met thy "met_test_squ_sub" [] Spec.e_metID
35.126 + [Specify.prep_met thy "met_test_squ_sub" [] Method.id_empty
35.127 (*tests subproblem fixed linear*)
35.128 (["Test","squ-equ-test-subpbl1"],
35.129 [("#Given" ,["equality e_e","solveFor v_v"]),
35.130 @@ -940,7 +940,7 @@
35.131 in
35.132 Check_elementwise L_L {(v_v::real). Assumptions}) "
35.133 setup \<open>KEStore_Elems.add_mets
35.134 - [Specify.prep_met thy "met_test_eq1" [] Spec.e_metID
35.135 + [Specify.prep_met thy "met_test_eq1" [] Method.id_empty
35.136 (*root-equation1:*)
35.137 (["Test","square_equation1"],
35.138 [("#Given" ,["equality e_e","solveFor v_v"]),
35.139 @@ -973,7 +973,7 @@
35.140 in
35.141 Check_elementwise L_L {(v_v::real). Assumptions})"
35.142 setup \<open>KEStore_Elems.add_mets
35.143 - [Specify.prep_met thy "met_test_squ2" [] Spec.e_metID
35.144 + [Specify.prep_met thy "met_test_squ2" [] Method.id_empty
35.145 (*root-equation2*)
35.146 (["Test","square_equation2"],
35.147 [("#Given" ,["equality e_e","solveFor v_v"]),
35.148 @@ -1006,7 +1006,7 @@
35.149 in
35.150 Check_elementwise L_L {(v_v::real). Assumptions})"
35.151 setup \<open>KEStore_Elems.add_mets
35.152 - [Specify.prep_met thy "met_test_squeq" [] Spec.e_metID
35.153 + [Specify.prep_met thy "met_test_squeq" [] Method.id_empty
35.154 (*root-equation*)
35.155 (["Test","square_equation"],
35.156 [("#Given" ,["equality e_e","solveFor v_v"]),
35.157 @@ -1032,7 +1032,7 @@
35.158 in
35.159 Or_to_List e_e)"
35.160 setup \<open>KEStore_Elems.add_mets
35.161 - [Specify.prep_met thy "met_test_eq_plain" [] Spec.e_metID
35.162 + [Specify.prep_met thy "met_test_eq_plain" [] Method.id_empty
35.163 (*solve_plain_square*)
35.164 (["Test","solve_plain_square"],
35.165 [("#Given",["equality e_e","solveFor v_v"]),
35.166 @@ -1059,7 +1059,7 @@
35.167 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
35.168 [''no_met'']) [BOOL e_e, REAL v_v])"
35.169 setup \<open>KEStore_Elems.add_mets
35.170 - [Specify.prep_met thy "met_test_norm_univ" [] Spec.e_metID
35.171 + [Specify.prep_met thy "met_test_norm_univ" [] Method.id_empty
35.172 (["Test","norm_univar_equation"],
35.173 [("#Given",["equality e_e","solveFor v_v"]),
35.174 ("#Where" ,[]),
35.175 @@ -1077,7 +1077,7 @@
35.176 (Try (Calculate ''PLUS'')) #>
35.177 (Try (Calculate ''TIMES''))) t_t)"
35.178 setup \<open>KEStore_Elems.add_mets
35.179 - [Specify.prep_met thy "met_test_intsimp" [] Spec.e_metID
35.180 + [Specify.prep_met thy "met_test_intsimp" [] Method.id_empty
35.181 (["Test","intsimp"],
35.182 [("#Given" ,["intTestGiven t_t"]),
35.183 ("#Where" ,[]),
36.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 22 11:23:30 2020 +0200
36.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 22 14:36:27 2020 +0200
36.3 @@ -10,22 +10,22 @@
36.4 val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree
36.5 val update_met : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
36.6 val update_metppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
36.7 - val update_metID : CTbasic.ctree -> Pos.pos -> Spec.metID -> CTbasic.ctree
36.8 + val update_metID : CTbasic.ctree -> Pos.pos -> Method.id -> CTbasic.ctree
36.9 val update_pbl : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
36.10 val update_pblppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
36.11 - val update_pblID : CTbasic.ctree -> Pos.pos -> Spec.pblID -> CTbasic.ctree
36.12 + val update_pblID : CTbasic.ctree -> Pos.pos -> Problem.id -> CTbasic.ctree
36.13 val update_oris : CTbasic.ctree -> Pos.pos -> Model.ori list -> CTbasic.ctree
36.14 - val update_orispec : CTbasic.ctree -> Pos.pos -> Spec.spec -> CTbasic.ctree
36.15 - val update_spec : CTbasic.ctree -> Pos.pos -> Spec.spec -> CTbasic.ctree
36.16 + val update_orispec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree
36.17 + val update_spec : CTbasic.ctree -> Pos.pos -> Spec.T -> CTbasic.ctree
36.18 val update_tac : CTbasic.ctree -> Pos.pos -> Tactic.input -> CTbasic.ctree
36.19
36.20 (* original write access *)
36.21 val cappend_form : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context -> term ->
36.22 CTbasic.ctree * Pos.pos' list
36.23 val cappend_problem : CTbasic.ctree -> Pos.pos -> Istate_Def.T * Proof.context ->
36.24 - Selem.fmz -> Model.ori list * Spec.spec * term * Proof.context
36.25 + Selem.fmz -> Model.ori list * Spec.T * term * Proof.context
36.26 -> CTbasic.ctree * Pos.pos' list
36.27 - val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.spec * Model.itm list * Model.itm list * Proof.context
36.28 + val cupdate_problem: CTbasic.ctree -> Pos.pos -> Spec.T * Model.itm list * Model.itm list * Proof.context
36.29 -> CTbasic.ctree * Pos.pos' list
36.30 val append_atomic : (* for solve.sml *)
36.31 Pos.pos -> ((Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context)) ->
36.32 @@ -42,8 +42,8 @@
36.33 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
36.34 val append_form: Pos.pos -> Istate_Def.T * Proof.context -> term -> CTbasic.ctree -> CTbasic.ctree
36.35 val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Selem.fmz ->
36.36 - Model.ori list * Spec.spec * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
36.37 - val update_problem: Pos.pos -> Spec.spec * Model.itm list * Model.itm list * Proof.context
36.38 + Model.ori list * Spec.T * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
36.39 + val update_problem: Pos.pos -> Spec.T * Model.itm list * Model.itm list * Proof.context
36.40 -> CTbasic.ctree -> CTbasic.ctree
36.41 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
36.42 end
37.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 22 11:23:30 2020 +0200
37.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 22 14:36:27 2020 +0200
37.3 @@ -24,10 +24,10 @@
37.4 result: Selem.result,
37.5
37.6 fmz: Selem.fmz,
37.7 - origin: Model.ori list * Spec.spec * term,
37.8 + origin: Model.ori list * Spec.T * term,
37.9 probl: Model.itm list,
37.10 meth: Model.itm list,
37.11 - spec: Spec.spec,
37.12 + spec: Spec.T,
37.13 ctxt: Proof.context}
37.14 | PrfObj of
37.15 {branch: branch,
37.16 @@ -49,23 +49,23 @@
37.17 val get_nd : ctree -> Pos.pos -> ctree (* for solve.sml *)
37.18 val just_created_ : ppobj -> bool (* for mathengine.sml *)
37.19 val just_created : state -> bool (* for mathengine.sml *)
37.20 - val e_origin : Model.ori list * Spec.spec * term (* for mathengine.sml *)
37.21 + val e_origin : Model.ori list * Spec.T * term (* for mathengine.sml *)
37.22
37.23 val is_pblobj : ppobj -> bool
37.24 val is_pblobj' : ctree -> Pos.pos -> bool
37.25 val is_pblnd : ctree -> bool
37.26
37.27 - val g_spec : ppobj -> Spec.spec
37.28 + val g_spec : ppobj -> Spec.T
37.29 val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
37.30 val g_form : ppobj -> term
37.31 val g_pbl : ppobj -> Model.itm list
37.32 val g_met : ppobj -> Model.itm list
37.33 - val g_metID : ppobj -> Spec.metID
37.34 + val g_metID : ppobj -> Method.id
37.35 val g_result : ppobj -> Selem.result
37.36 val g_tac : ppobj -> Tactic.input
37.37 val g_domID : ppobj -> ThyC.id (* for appl.sml TODO: replace by thyID *)
37.38
37.39 - val g_origin : ppobj -> Model.ori list * Spec.spec * term (* for script.sml *)
37.40 + val g_origin : ppobj -> Model.ori list * Spec.T * term (* for script.sml *)
37.41 val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context (* for script.sml *)
37.42 val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T (* for script.sml *)
37.43 val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context
37.44 @@ -77,9 +77,9 @@
37.45 val new_val : term -> Istate_Def.T -> Istate_Def.T
37.46 (* for calchead.sml *)
37.47 type cid = cellID list
37.48 - type ocalhd = bool * Pos.pos_ * term * Model.itm list * (bool * term) list * Spec.spec
37.49 + type ocalhd = bool * Pos.pos_ * term * Model.itm list * (bool * term) list * Spec.T
37.50 datatype ptform = Form of term | ModSpec of ocalhd
37.51 - val get_somespec' : Spec.spec -> Spec.spec -> Spec.spec
37.52 + val get_somespec' : Spec.T -> Spec.T -> Spec.T
37.53 exception PTREE of string;
37.54
37.55 val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule_Set.T (* for appl.sml *)
37.56 @@ -206,9 +206,9 @@
37.57 | PblObj of (* a step serving a whole specification-phase *)
37.58 {fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
37.59 origin: (Model.ori list) *(* from fmz+pbt+met for efficiently adding items to probl, meth *)
37.60 - Spec.spec * (* updated by Refine_Tacitly *)
37.61 + Spec.T * (* updated by Refine_Tacitly *)
37.62 term, (* headline of calc-head, as calculated initially(!) *)
37.63 - spec : Spec.spec, (* explicitly input *)
37.64 + spec : Spec.T, (* explicitly input *)
37.65 probl : Model.itm list, (* itms explicitly input *)
37.66 meth : Model.itm list, (* itms automatically added to copy of probl *)
37.67 ctxt : Proof.context, (* used while specifying this SubProblem *)
37.68 @@ -440,7 +440,7 @@
37.69 term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*)
37.70 Model.itm list * (* model: given, find, relate *)
37.71 ((bool * term) list) *(* model: preconds *)
37.72 - Spec.spec; (* specification *)
37.73 + Spec.T; (* specification *)
37.74 val e_ocalhd = (false, Und, TermC.empty, [Model.e_itm], [(false, TermC.empty)], Spec.empty);
37.75
37.76 datatype ptform = Form of term | ModSpec of ocalhd;
37.77 @@ -485,8 +485,8 @@
37.78 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
37.79 let
37.80 val domID = if dI = ThyC.id_empty then dI' else dI
37.81 - val pblID = if pI = Spec.e_pblID then pI' else pI
37.82 - val metID = if mI = Spec.e_metID then mI' else mI
37.83 + val pblID = if pI = Problem.id_empty then pI' else pI
37.84 + val metID = if mI = Method.id_empty then mI' else mI
37.85 in (domID, pblID, metID) end;
37.86
37.87 (**.development for extracting an 'interval' from ptree.**)
38.1 --- a/src/Tools/isac/MathEngBasic/ctree.sml Wed Apr 22 11:23:30 2020 +0200
38.2 +++ b/src/Tools/isac/MathEngBasic/ctree.sml Wed Apr 22 14:36:27 2020 +0200
38.3 @@ -9,7 +9,7 @@
38.4 include CALC_TREE_NAVIGATION
38.5 include CALC_TREE_ACCESS
38.6
38.7 - val get_pblID : state -> Spec.pblID option
38.8 + val get_pblID : state -> Problem.id option
38.9 end
38.10
38.11 structure Ctree : CTREE =
38.12 @@ -23,10 +23,10 @@
38.13 val (_, pI, _) = get_obj g_spec pt p'
38.14 val (_, (_, oI, _), _) = get_obj g_origin pt p'
38.15 in
38.16 - if pI <> Spec.e_pblID
38.17 + if pI <> Problem.id_empty
38.18 then SOME pI
38.19 else
38.20 - if oI <> Spec.e_pblID then SOME oI else NONE end;
38.21 + if oI <> Problem.id_empty then SOME oI else NONE end;
38.22
38.23
38.24 end;
39.1 --- a/src/Tools/isac/MathEngBasic/method.sml Wed Apr 22 11:23:30 2020 +0200
39.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Wed Apr 22 14:36:27 2020 +0200
39.3 @@ -6,6 +6,12 @@
39.4 signature METHOD =
39.5 sig
39.6 type T = Meth_Def.T
39.7 + val empty: T
39.8 +
39.9 + type id = Meth_Def.id
39.10 + val id_empty: id
39.11 + val id_to_string: id -> string
39.12 +(*val metID2str: id -> string*)
39.13
39.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
39.15 (*NONE*)
39.16 @@ -20,5 +26,10 @@
39.17 (**)
39.18
39.19 type T = Meth_Def.T;
39.20 +val empty = Meth_Def.empty;
39.21 +
39.22 +type id = Meth_Def.id;
39.23 +val id_empty = Meth_Def.id_empty;
39.24 +val id_to_string = Meth_Def.id_to_string;
39.25
39.26 (**)end(**)
40.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Wed Apr 22 11:23:30 2020 +0200
40.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Wed Apr 22 14:36:27 2020 +0200
40.3 @@ -12,20 +12,20 @@
40.4 val check_preconds : 'a -> Rule_Set.T -> term list -> Model.itm list -> (bool * term) list
40.5 val check_preconds' : Rule_Set.T -> term list -> Model.itm list -> 'a -> (bool * term) list
40.6
40.7 - datatype match_ = Match_ of Spec.pblID * (Model.itm list * (bool * term) list) | NoMatch_
40.8 + datatype match_ = Match_ of Problem.id * (Model.itm list * (bool * term) list) | NoMatch_
40.9 val refined_ : match_ list -> match_ option
40.10 - datatype match = Matches of Spec.pblID * Model.item Model.ppc | NoMatch of Spec.pblID * Model.item Model.ppc
40.11 + datatype match = Matches of Problem.id * Model.item Model.ppc | NoMatch of Problem.id * Model.item Model.ppc
40.12 val matchs2str : match list -> string
40.13 val common_subthy : theory * theory -> theory
40.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
40.15 val pres2str : (bool * term) list -> string
40.16 - val refined : match list -> Spec.pblID
40.17 + val refined : match list -> Problem.id
40.18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
40.19 (*NONE*)
40.20 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40.21
40.22 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
40.23 - val pblID_of_match : match -> Spec.pblID
40.24 + val pblID_of_match : match -> Problem.id
40.25 val refined_IDitms : match list -> match option
40.26 end
40.27
40.28 @@ -33,8 +33,8 @@
40.29 struct
40.30
40.31 datatype match =
40.32 - Matches of Spec.pblID * Model.item Model.ppc
40.33 -| NoMatch of Spec.pblID * Model.item Model.ppc;
40.34 + Matches of Problem.id * Model.item Model.ppc
40.35 +| NoMatch of Problem.id * Model.item Model.ppc;
40.36 fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")"
40.37 | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")";
40.38 fun matchs2str ms = (strs2str o (map match2str)) ms;
40.39 @@ -43,7 +43,7 @@
40.40
40.41 (* 10.03 for Refine_Problem *)
40.42 datatype match_ =
40.43 - Match_ of Spec.pblID * (( Model.itm list) * ((bool * term) list))
40.44 + Match_ of Problem.id * (( Model.itm list) * ((bool * term) list))
40.45 | NoMatch_;
40.46
40.47 (* the refined pbt is the last_element Matches in the list *)
41.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Apr 22 11:23:30 2020 +0200
41.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Wed Apr 22 14:36:27 2020 +0200
41.3 @@ -7,6 +7,10 @@
41.4 sig
41.5 type T = Probl_Def.T
41.6
41.7 + type id = Probl_Def.id
41.8 + val id_empty: id
41.9 + val id_to_string: id -> string
41.10 +
41.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
41.12 (*NONE*)
41.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
41.14 @@ -21,5 +25,8 @@
41.15
41.16 type T = Probl_Def.T;
41.17
41.18 +type id = Probl_Def.id;
41.19 +val id_empty = Probl_Def.id_empty;
41.20 +val id_to_string = Probl_Def.id_to_string;
41.21
41.22 (**)end(**)
42.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Wed Apr 22 11:23:30 2020 +0200
42.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Wed Apr 22 14:36:27 2020 +0200
42.3 @@ -29,7 +29,7 @@
42.4 val subte2sube : term list -> TermC.as_string list
42.5
42.6 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
42.7 - val e_fmz : fmz_ * Spec.spec (* for datatypes.sml *)
42.8 + val e_fmz : fmz_ * Spec.T (* for datatypes.sml *)
42.9 val e_sube : TermC.as_string list
42.10 val e_subs : string list
42.11 val subte2subst : term list -> (term * term) list
42.12 @@ -53,7 +53,7 @@
42.13 (* a formalization of an example contains data
42.14 sufficient for mechanically finding the solution for the example.
42.15 FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
42.16 -type fmz = fmz_ * Spec.spec;
42.17 +type fmz = fmz_ * Spec.T;
42.18 val e_fmz = ([], Spec.empty);
42.19
42.20 type result = term * term list
43.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 22 11:23:30 2020 +0200
43.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 22 14:36:27 2020 +0200
43.3 @@ -12,7 +12,7 @@
43.4 datatype T =
43.5 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
43.6 | Add_Relation' of TermC.as_string * Model.itm list
43.7 - | Apply_Method' of Spec.metID * term option * Istate_Def.T * Proof.context
43.8 + | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
43.9
43.10 | Begin_Sequ' | Begin_Trans' of term
43.11 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
43.12 @@ -22,7 +22,7 @@
43.13
43.14 | CAScmd' of term
43.15 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
43.16 - | Check_Postcond' of Spec.pblID * term
43.17 + | Check_Postcond' of Problem.id * term
43.18 | Check_elementwise' of term * TermC.as_string * Selem.result
43.19 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
43.20
43.21 @@ -34,22 +34,22 @@
43.22 | Empty_Tac_
43.23 | Free_Solve'
43.24
43.25 - | Init_Proof' of TermC.as_string list * Spec.spec
43.26 - | Model_Problem' of Spec.pblID * Model.itm list * Model.itm list
43.27 + | Init_Proof' of TermC.as_string list * Spec.T
43.28 + | Model_Problem' of Problem.id * Model.itm list * Model.itm list
43.29 | Or_to_List' of term * term
43.30 - | Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
43.31 - | Refine_Tacitly' of Spec.pblID * Spec.pblID * ThyC.id * Spec.metID * Model.itm list
43.32 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
43.33 + | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
43.34
43.35 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
43.36 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
43.37 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
43.38 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
43.39
43.40 - | Specify_Method' of Spec.metID * Model.ori list * Model.itm list
43.41 - | Specify_Problem' of Spec.pblID * (bool * (Model.itm list * (bool * term) list))
43.42 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
43.43 + | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
43.44 | Specify_Theory' of ThyC.id
43.45 | Subproblem' of
43.46 - Spec.spec * Model.ori list *
43.47 + Spec.T * Model.ori list *
43.48 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
43.49 Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
43.50 (*Istate.T * ? *)
43.51 @@ -63,7 +63,7 @@
43.52 datatype input =
43.53 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
43.54 | Apply_Assumption of TermC.as_string list
43.55 - | Apply_Method of Spec.metID
43.56 + | Apply_Method of Method.id
43.57 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
43.58 | Begin_Sequ | Begin_Trans
43.59 | Split_And | Split_Or | Split_Intersect
43.60 @@ -73,7 +73,7 @@
43.61 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
43.62 | CAScmd of TermC.as_string
43.63 | Calculate of string
43.64 - | Check_Postcond of Spec.pblID
43.65 + | Check_Postcond of Problem.id
43.66 | Check_elementwise of TermC.as_string
43.67 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
43.68
43.69 @@ -85,21 +85,21 @@
43.70 | Empty_Tac
43.71 | Free_Solve
43.72
43.73 - | Init_Proof of TermC.as_string list * Spec.spec
43.74 + | Init_Proof of TermC.as_string list * Spec.T
43.75 | Model_Problem
43.76 | Or_to_List
43.77 - | Refine_Problem of Spec.pblID
43.78 - | Refine_Tacitly of Spec.pblID
43.79 + | Refine_Problem of Problem.id
43.80 + | Refine_Tacitly of Problem.id
43.81
43.82 | Rewrite of ThmC.T
43.83 | Rewrite_Inst of Selem.subs * ThmC.T
43.84 | Rewrite_Set of Rule_Set.id
43.85 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
43.86
43.87 - | Specify_Method of Spec.metID
43.88 - | Specify_Problem of Spec.pblID
43.89 + | Specify_Method of Method.id
43.90 + | Specify_Problem of Problem.id
43.91 | Specify_Theory of ThyC.id
43.92 - | Subproblem of ThyC.id * Spec.pblID
43.93 + | Subproblem of ThyC.id * Problem.id
43.94
43.95 | Substitute of Selem.sube
43.96 | Tac of string
43.97 @@ -146,7 +146,7 @@
43.98 datatype input =
43.99 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
43.100 | Apply_Assumption of TermC.as_string list
43.101 - | Apply_Method of Spec.metID
43.102 + | Apply_Method of Method.id
43.103 (* creates an "istate" in PblObj.env; in case of "implicit_take"
43.104 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
43.105 a "SOME istate" at fst of "loc".
43.106 @@ -161,7 +161,7 @@
43.107 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
43.108 | CAScmd of TermC.as_string
43.109 | Calculate of string
43.110 - | Check_Postcond of Spec.pblID
43.111 + | Check_Postcond of Problem.id
43.112 | Check_elementwise of TermC.as_string
43.113 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
43.114
43.115 @@ -173,11 +173,11 @@
43.116 | Empty_Tac
43.117 | Free_Solve
43.118
43.119 - | Init_Proof of TermC.as_string list * Spec.spec
43.120 + | Init_Proof of TermC.as_string list * Spec.T
43.121 | Model_Problem
43.122 | Or_to_List
43.123 - | Refine_Problem of Spec.pblID
43.124 - | Refine_Tacitly of Spec.pblID
43.125 + | Refine_Problem of Problem.id
43.126 + | Refine_Tacitly of Problem.id
43.127
43.128 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
43.129 because there all the thms are present with both (thmID, thm)
43.130 @@ -188,10 +188,10 @@
43.131 | Rewrite_Set of Rule_Set.id
43.132 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
43.133
43.134 - | Specify_Method of Spec.metID
43.135 - | Specify_Problem of Spec.pblID
43.136 + | Specify_Method of Method.id
43.137 + | Specify_Problem of Problem.id
43.138 | Specify_Theory of ThyC.id
43.139 - | Subproblem of ThyC.id * Spec.pblID (* WN0509 drop *)
43.140 + | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
43.141
43.142 | Substitute of Selem.sube
43.143 | Tac of string (* WN0509 drop *)
43.144 @@ -339,7 +339,7 @@
43.145 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
43.146 * tactic Apply_Method metID
43.147 * formula term *)
43.148 - Spec.metID * (* key for Know_Store *)
43.149 + Method.id * (* key for Know_Store *)
43.150 term option * (* the first formula of Calc.T. TODO: rm option *)
43.151 Istate_Def.T * (* for the newly started program *)
43.152 Proof.context (* for the newly started program *)
43.153 @@ -352,7 +352,7 @@
43.154 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
43.155 | CAScmd' of term
43.156 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
43.157 - | Check_Postcond' of Spec.pblID *
43.158 + | Check_Postcond' of Problem.id *
43.159 term (* returnvalue of program in solve *)
43.160 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
43.161 term * (* (1) the current formula: [x=1,x=...] *)
43.162 @@ -368,32 +368,32 @@
43.163 | Empty_Tac_
43.164 | Free_Solve'
43.165
43.166 - | Init_Proof' of TermC.as_string list * Spec.spec
43.167 + | Init_Proof' of TermC.as_string list * Spec.T
43.168 | Model_Problem' of (* first step in specifying *)
43.169 - Spec.pblID * (* key into Know_Store *)
43.170 + Problem.id * (* key into Know_Store *)
43.171 Model.itm list * (* the 'untouched' pbl *)
43.172 Model.itm list (* the casually completed met *)
43.173 | Or_to_List' of term * term
43.174 - | Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
43.175 + | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
43.176 | Refine_Tacitly' of
43.177 - Spec.pblID * (* input *)
43.178 - Spec.pblID * (* the refined from applicable_in *)
43.179 + Problem.id * (* input *)
43.180 + Problem.id * (* the refined from applicable_in *)
43.181 ThyC.id * (* from new pbt?! filled in specify *)
43.182 - Spec.metID * (* from new pbt?! filled in specify *)
43.183 + Method.id * (* from new pbt?! filled in specify *)
43.184 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
43.185 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
43.186 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
43.187 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
43.188 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
43.189
43.190 - | Specify_Method' of Spec.metID * Model.ori list * Model.itm list
43.191 - | Specify_Problem' of Spec.pblID *
43.192 + | Specify_Method' of Method.id * Model.ori list * Model.itm list
43.193 + | Specify_Problem' of Problem.id *
43.194 (bool * (* matches *)
43.195 (Model.itm list * (* ppc *)
43.196 (bool * term) list)) (* preconditions marked true/false *)
43.197 | Specify_Theory' of ThyC.id
43.198 | Subproblem' of
43.199 - Spec.spec *
43.200 + Spec.T *
43.201 (Model.ori list) * (* filled in associate Subproblem' *)
43.202 term * (* filled -"-, headline of calc-head *)
43.203 Selem.fmz_ * (* string list from arguments *)
43.204 @@ -425,7 +425,7 @@
43.205 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
43.206 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
43.207 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
43.208 - Spec.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
43.209 + Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
43.210
43.211 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
43.212 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
44.1 --- a/src/Tools/isac/MathEngine/detail-step.sml Wed Apr 22 11:23:30 2020 +0200
44.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Wed Apr 22 14:36:27 2020 +0200
44.3 @@ -43,7 +43,7 @@
44.4 | _ =>
44.5 let
44.6 val is = Generate.init_istate tac t
44.7 - val tac_ = Tactic.Apply_Method' (Spec.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
44.8 + val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
44.9 val pos' = ((lev_on o lev_dn) p, Frm)
44.10 val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *)
44.11 val (_,_, (pt'', _)) = Solve.complete_solve Solve.CompleteSubpbl [] (pt', pos')
45.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Apr 22 11:23:30 2020 +0200
45.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Apr 22 14:36:27 2020 +0200
45.3 @@ -30,7 +30,7 @@
45.4 val thy' = get_obj g_domID pt pp;
45.5 val thy = ThyC.get_theory thy';
45.6 val metID = get_obj g_metID pt pp;
45.7 - val metID' = if metID = Spec.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
45.8 + val metID' = if metID = Method.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
45.9 val (sc, srls) = (case Specify.get_met metID' of
45.10 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
45.11 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
45.12 @@ -53,7 +53,7 @@
45.13 val thy = ThyC.get_theory thy'
45.14 val metID = get_obj g_metID pt pp
45.15 val metID' =
45.16 - if metID = Spec.e_metID
45.17 + if metID = Method.id_empty
45.18 then (thd3 o snd3) (get_obj g_origin pt pp)
45.19 else metID
45.20 val (sc, srls, erls, ro) = (case Specify.get_met metID' of
46.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 11:23:30 2020 +0200
46.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 14:36:27 2020 +0200
46.3 @@ -12,12 +12,12 @@
46.4
46.5 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
46.6 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list
46.7 - val context_met : Spec.metID -> Ctree.ctree -> Pos.pos -> bool * Spec.metID * Program.T * Model.itm list * (bool * term) list
46.8 - val context_pbl : Spec.pblID -> Ctree.ctree -> Pos.pos -> bool * Spec.pblID * term * Model.itm list * (bool * term) list
46.9 - val set_method : Spec.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
46.10 - val set_problem : Spec.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
46.11 + val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * Model.itm list * (bool * term) list
46.12 + val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * Model.itm list * (bool * term) list
46.13 + val set_method : Method.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
46.14 + val set_problem : Problem.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
46.15 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
46.16 - val tryrefine : Spec.pblID -> Ctree.ctree -> Pos.pos' -> bool * Spec.pblID * term * Model.itm list * (bool * term) list
46.17 + val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * Model.itm list * (bool * term) list
46.18 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
46.19 (*NONE*)
46.20 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
46.21 @@ -144,7 +144,7 @@
46.22 => (probl, os, pI, hdl, pI')
46.23 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
46.24 val pblID =
46.25 - if pI' = Spec.e_pblID
46.26 + if pI' = Problem.id_empty
46.27 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
46.28 else pI'
46.29 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
46.30 @@ -159,7 +159,7 @@
46.31 case Ctree.get_obj I pt p of
46.32 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
46.33 | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
46.34 - val metID = if mI' = Spec.e_metID
46.35 + val metID = if mI' = Method.id_empty
46.36 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
46.37 else mI'
46.38 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
47.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 22 11:23:30 2020 +0200
47.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 22 14:36:27 2020 +0200
47.3 @@ -28,7 +28,7 @@
47.4 val contain_bdv: Rule.rule list -> bool
47.5 val contains_bdv: thm -> bool
47.6 val subst_typs: term -> typ -> typ -> term
47.7 - val pblterm: ThyC.id -> Spec.pblID -> term
47.8 + val pblterm: ThyC.id -> Probl_Def.id -> term
47.9 val subpbl: string -> string list -> term
47.10 val stacpbls: term -> term list
47.11 val op_of_calc: term -> string
48.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 22 11:23:30 2020 +0200
48.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 22 14:36:27 2020 +0200
48.3 @@ -57,7 +57,7 @@
48.4 ML \<open>
48.5 signature PROGAM_TACTIC =
48.6 sig
48.7 - val dest_spec : term -> Spec.spec
48.8 + val dest_spec : term -> Spec.T
48.9 val get_first_argument : term -> term option (*TODO rename get_first_argument*)
48.10 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
48.11 val is: term -> bool
48.12 @@ -76,7 +76,7 @@
48.13 fun dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) $ p $ m)) =
48.14 (d |> HOLogic.dest_string,
48.15 p |> HOLogic.dest_list |> map HOLogic.dest_string,
48.16 - m |> HOLogic.dest_list |> map HOLogic.dest_string) : Spec.spec
48.17 + m |> HOLogic.dest_list |> map HOLogic.dest_string) : Spec.T
48.18 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
48.19
48.20 (* get argument of first Prog_Tac in a progam for implicit_take *)
49.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 22 11:23:30 2020 +0200
49.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 22 14:36:27 2020 +0200
49.3 @@ -148,7 +148,7 @@
49.4 in
49.5 case Specify.refine_ori oris pI of
49.6 SOME pblID =>
49.7 - Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Spec.e_metID, [](*filled in specify*)))
49.8 + Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
49.9 | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
49.10 end
49.11 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
49.12 @@ -210,7 +210,7 @@
49.13 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
49.14 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
49.15 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
49.16 - val pbl = if pI' = Spec.e_pblID andalso pI = Spec.e_pblID
49.17 + val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
49.18 then (false, (Generate.init_pbl ppc, []))
49.19 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
49.20 in
49.21 @@ -422,7 +422,7 @@
49.22 then
49.23 Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
49.24 else (*some fields filled later in LI*)
49.25 - Appl (Tactic.Subproblem' ((domID, pblID, Spec.e_metID), [],
49.26 + Appl (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
49.27 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
49.28 | applicable_in _ _ (Tactic.End_Subproblem) =
49.29 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
50.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 22 11:23:30 2020 +0200
50.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 22 14:36:27 2020 +0200
50.3 @@ -69,12 +69,12 @@
50.4 type calcstate
50.5 type calcstate'
50.6
50.7 - val nxt_spec : Pos.pos_ -> bool -> Model.ori list -> Spec.spec -> Model.itm list * Model.itm list ->
50.8 - (string * (term * 'a)) list * (string * (term * 'b)) list -> Spec.spec -> Pos.pos_ * Tactic.input
50.9 + val nxt_spec : Pos.pos_ -> bool -> Model.ori list -> Spec.T -> Model.itm list * Model.itm list ->
50.10 + (string * (term * 'a)) list * (string * (term * 'b)) list -> Spec.T -> Pos.pos_ * Tactic.input
50.11
50.12 val reset_calchead : Calc.T -> Calc.T
50.13 val get_ocalhd : Calc.T -> Ctree.ocalhd
50.14 - val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.id * Spec.pblID * Spec.metID -> bool
50.15 + val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
50.16 val all_modspec : Calc.T -> Calc.T
50.17
50.18 val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem4.pat list -> Model.itm list
50.19 @@ -84,7 +84,7 @@
50.20 val is_complete_mod : Calc.T -> bool
50.21 val complete_spec : Calc.T -> Calc.T
50.22 val is_complete_spec : Calc.T -> bool
50.23 - val some_spec : Spec.spec -> Spec.spec -> Spec.spec
50.24 + val some_spec : Spec.T -> Spec.T -> Spec.T
50.25 (* these could go to Ctree ..*)
50.26 val show_pt : Ctree.ctree -> unit
50.27 val show_pt_tac : Ctree.ctree -> unit
50.28 @@ -92,7 +92,7 @@
50.29 val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
50.30
50.31 val match_ags : theory -> Celem4.pat list -> term list -> Model.ori list
50.32 - val match_ags_msg : Spec.pblID -> term -> term list -> unit
50.33 + val match_ags_msg : Problem.id -> term -> term list -> unit
50.34 val oris2fmz_vals : Model.ori list -> string list * term list
50.35 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
50.36 val is_known : Proof.context -> string -> Model.ori list -> term -> string * Model.ori * term list
50.37 @@ -185,7 +185,7 @@
50.38 fun ocalhd_complete its pre (dI, pI, mI) =
50.39 foldl and_ (true, map #3 (its: Model.itm list)) andalso
50.40 foldl and_ (true, map #1 (pre: (bool * term) list)) andalso
50.41 - dI <> ThyC.id_empty andalso pI <> Spec.e_pblID andalso mI <> Spec.e_metID
50.42 + dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
50.43
50.44 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
50.45 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
50.46 @@ -360,7 +360,7 @@
50.47 *)
50.48 fun nxt_spec Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
50.49 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')
50.50 - else if pI' = Spec.e_pblID andalso pI = Spec.e_pblID then (Pbl, Tactic.Specify_Problem pI')
50.51 + else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pbl, Tactic.Specify_Problem pI')
50.52 else
50.53 case find_first (is_error o #5) pbl of
50.54 SOME (_, _, _, fd, itm_) =>
50.55 @@ -371,8 +371,8 @@
50.56 | NONE => (*pbl-items complete*)
50.57 if not preok then (Pbl, Tactic.Refine_Problem pI')
50.58 else if dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')
50.59 - else if pI = Spec.e_pblID then (Pbl, Tactic.Specify_Problem pI')
50.60 - else if mI = Spec.e_metID then (Pbl, Tactic.Specify_Method mI')
50.61 + else if pI = Problem.id_empty then (Pbl, Tactic.Specify_Problem pI')
50.62 + else if mI = Method.id_empty then (Pbl, Tactic.Specify_Method mI')
50.63 else
50.64 case find_first (is_error o #5) met of
50.65 SOME (_, _, _, fd, itm_) => (Met, mk_delete (ThyC.get_theory dI) fd itm_)
50.66 @@ -388,7 +388,7 @@
50.67 SOME (fd,ct') => (Met, mk_additem fd ct')
50.68 | NONE =>
50.69 (if dI = ThyC.id_empty then (Met, Tactic.Specify_Theory dI')
50.70 - else if pI = Spec.e_pblID then (Met, Tactic.Specify_Problem pI')
50.71 + else if pI = Problem.id_empty then (Met, Tactic.Specify_Problem pI')
50.72 else if not preok then (Met, Tactic.Specify_Method mI)
50.73 else (Met, Tactic.Apply_Method mI)))
50.74 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
50.75 @@ -675,7 +675,7 @@
50.76
50.77 (* output the headline to a ppc *)
50.78 fun header p_ pI mI =
50.79 - case p_ of Pbl => Generate.Problem (if pI = Spec.e_pblID then [] else pI)
50.80 + case p_ of Pbl => Generate.Problem (if pI = Problem.id_empty then [] else pI)
50.81 | Met => Generate.Method mI
50.82 | pos => error ("header called with "^ pos_2str pos)
50.83
50.84 @@ -686,8 +686,8 @@
50.85 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
50.86 | _ => error "specify_additem: uncovered case of get_obj I pt p"
50.87 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
50.88 - val cpI = if pI = Spec.e_pblID then pI' else pI
50.89 - val cmI = if mI = Spec.e_metID then mI' else mI
50.90 + val cpI = if pI = Problem.id_empty then pI' else pI
50.91 + val cmI = if mI = Method.id_empty then mI' else mI
50.92 val {ppc, pre, prls, ...} = Specify.get_met cmI
50.93 in
50.94 case appl_add ctxt sel oris met ppc ct of
50.95 @@ -728,8 +728,8 @@
50.96 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
50.97 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
50.98 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
50.99 - val cpI = if pI = Spec.e_pblID then pI' else pI
50.100 - val cmI = if mI = Spec.e_metID then mI' else mI
50.101 + val cpI = if pI = Problem.id_empty then pI' else pI
50.102 + val cmI = if mI = Method.id_empty then mI' else mI
50.103 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
50.104 in
50.105 case appl_add ctxt sel oris pbl ppc ct of
50.106 @@ -774,7 +774,7 @@
50.107 (oris, dI', pI', dI, pI, pbl, ctxt)
50.108 | _ => error "specify (Specify_Theory': uncovered case get_obj"
50.109 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
50.110 - val cpI = if pI = Spec.e_pblID then pI' else pI;
50.111 + val cpI = if pI = Problem.id_empty then pI' else pI;
50.112 in
50.113 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
50.114 Add itm (*..union old input *) =>
50.115 @@ -804,7 +804,7 @@
50.116 (oris, dI', mI', dI, mI, met, ctxt)
50.117 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
50.118 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
50.119 - val cmI = if mI = Spec.e_metID then mI' else mI;
50.120 + val cmI = if mI = Method.id_empty then mI' else mI;
50.121 in
50.122 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
50.123 Add itm (*..union old input *) =>
50.124 @@ -874,8 +874,8 @@
50.125
50.126 fun some_spec (odI, opI, omI) (dI, pI, mI) =
50.127 (if dI = ThyC.id_empty then odI else dI,
50.128 - if pI = Spec.e_pblID then opI else pI,
50.129 - if mI = Spec.e_metID then omI else mI)
50.130 + if pI = Problem.id_empty then opI else pI,
50.131 + if mI = Method.id_empty then omI else mI)
50.132
50.133 (* get the values from oris; handle the term list w.r.t. penv *)
50.134 fun vals_of_oris (oris: Model.ori list) =
50.135 @@ -976,7 +976,7 @@
50.136 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
50.137 else
50.138 let val (dI,pI,mI) = get_obj g_spec pt p
50.139 - in dI <> ThyC.id_empty andalso pI <> Spec.e_pblID andalso mI <> Spec.e_metID end
50.140 + in dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty end
50.141
50.142 (* complete empty items in specification from origin (pbl, met ev.refined);
50.143 assumes 'is_complete_mod' *)
50.144 @@ -995,7 +995,7 @@
50.145 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
50.146 let
50.147 val (_, _, metID) = get_somespec' spec spec'
50.148 - val pre = if metID = Spec.e_metID then []
50.149 + val pre = if metID = Method.id_empty then []
50.150 else
50.151 let
50.152 val {prls, pre= where_, ...} = Specify.get_met metID
50.153 @@ -1008,7 +1008,7 @@
50.154 | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
50.155 let
50.156 val (_, pI, _) = get_somespec' spec spec'
50.157 - val pre = if pI = Spec.e_pblID then []
50.158 + val pre = if pI = Problem.id_empty then []
50.159 else
50.160 let
50.161 val {prls, where_, ...} = Specify.get_pbt pI
50.162 @@ -1056,7 +1056,7 @@
50.163 val pI = case get_obj I pt (lev_up p) of
50.164 PblObj{spec = (_, pI, _), ...} => pI
50.165 | _ => error "pt_extract last_onlev: uncovered case get_obj"
50.166 - in if pI = Spec.e_pblID then NONE else SOME (Tactic.Check_Postcond pI) end
50.167 + in if pI = Problem.id_empty then NONE else SOME (Tactic.Check_Postcond pI) end
50.168 else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)
50.169 else
50.170 let val p' = lev_on p
51.1 --- a/src/Tools/isac/Specify/generate.sml Wed Apr 22 11:23:30 2020 +0200
51.2 +++ b/src/Tools/isac/Specify/generate.sml Wed Apr 22 14:36:27 2020 +0200
51.3 @@ -7,13 +7,13 @@
51.4 sig
51.5 type taci
51.6 val e_taci : taci
51.7 - datatype pblmet = Method of Spec.metID | Problem of Spec.pblID | Upblmet
51.8 + datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
51.9 datatype mout =
51.10 EmptyMout
51.11 | Error' of string
51.12 | FormKF of TermC.as_string
51.13 | PpcKF of pblmet * Model.item Model.ppc
51.14 - | RefinedKF of Spec.pblID * (Model.itm list * (bool * term) list)
51.15 + | RefinedKF of Problem.id * (Model.itm list * (bool * term) list)
51.16 val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T
51.17 -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
51.18 val init_istate : Tactic.input -> term -> Istate_Def.T
51.19 @@ -87,10 +87,10 @@
51.20
51.21 datatype pblmet = (*%^%*)
51.22 Upblmet (*undefined*)
51.23 -| Problem of Spec.pblID (*%^%*)
51.24 -| Method of Spec.metID; (*%^%*)
51.25 +| Problem of Problem.id (*%^%*)
51.26 +| Method of Method.id; (*%^%*)
51.27 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
51.28 - | pblmet2str (Method metID) = "Method " ^ Spec.metID2str metID (*%^%*)
51.29 + | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)
51.30 | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
51.31
51.32 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
51.33 @@ -121,7 +121,7 @@
51.34 | FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*)
51.35 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
51.36 | RefineKF of Stool.match list (*<--*)
51.37 -| RefinedKF of (Spec.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*)
51.38 +| RefinedKF of (Problem.id * ((Model.itm list) * ((bool * term) list))) (*<--*)
51.39
51.40 (*
51.41 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
51.42 @@ -129,7 +129,7 @@
51.43 datatype mout =
51.44 FormKF of TermC.as_string
51.45 | PpcKF of (pblmet * Model.item Model.ppc)
51.46 -| RefinedKF of Spec.pblID * (Model.itm list * (bool * term) list)
51.47 +| RefinedKF of Problem.id * (Model.itm list * (bool * term) list)
51.48 | Error' of string
51.49 | EmptyMout
51.50
51.51 @@ -274,7 +274,7 @@
51.52 val (pt, _) = cappend_form pt p (is, ctxt) f
51.53 val pt = update_branch pt p TransitiveB
51.54 val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule_Set.id rls)) f
51.55 - val tac_ = Tactic.Apply_Method' (Spec.e_metID, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
51.56 + val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
51.57 val pos' = ((lev_on o lev_dn) p, Frm)
51.58 in
51.59 generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
51.60 @@ -292,7 +292,7 @@
51.61 val (pt, _) = cappend_form pt p (is, ctxt) f
51.62 val pt = update_branch pt p TransitiveB
51.63 val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id rls)) f
51.64 - val tac_ = Tactic.Apply_Method' (Spec.e_metID, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
51.65 + val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
51.66 val pos' = ((lev_on o lev_dn) p, Frm)
51.67 in
51.68 generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
52.1 --- a/src/Tools/isac/Specify/input-calchead.sml Wed Apr 22 11:23:30 2020 +0200
52.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Wed Apr 22 14:36:27 2020 +0200
52.3 @@ -7,7 +7,7 @@
52.4 sig
52.5 datatype iitem = Find of TermC.as_string list | Given of TermC.as_string list | Relate of TermC.as_string list
52.6 type imodel = iitem list
52.7 - type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * Spec.spec
52.8 + type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * Spec.T
52.9 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
52.10 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
52.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
52.12 @@ -38,7 +38,7 @@
52.13
52.14 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
52.15
52.16 -fun cas_input_ ((dI, pI, mI): Spec.spec) dtss = (*WN110515 reconsider thy..ctxt*)
52.17 +fun cas_input_ ((dI, pI, mI): Spec.T) dtss = (*WN110515 reconsider thy..ctxt*)
52.18 let
52.19 val thy = ThyC.get_theory dI
52.20 val {ppc, ...} = Specify.get_pbt pI
52.21 @@ -100,7 +100,7 @@
52.22 TermC.as_string * (*the headline*)
52.23 imodel * (*the model (without Find) of the calc-head*)
52.24 Pos.pos_ * (*model belongs to Pbl or Met*)
52.25 - Spec.spec; (*specification: domID, pblID, metID*)
52.26 + Spec.T; (*specification: domID, pblID, metID*)
52.27 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty)
52.28
52.29 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Selem.fmz) =
53.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed Apr 22 11:23:30 2020 +0200
53.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed Apr 22 14:36:27 2020 +0200
53.3 @@ -5,8 +5,8 @@
53.4
53.5 signature MODEL_SPECIFY =
53.6 sig
53.7 - val hack_until_review_Specify_1: Spec.metID -> Model.itm list -> Model.itm list
53.8 - val hack_until_review_Specify_2: Spec.metID -> Model.itm list -> Model.itm list
53.9 + val hack_until_review_Specify_1: Method.id -> Model.itm list -> Model.itm list
53.10 + val hack_until_review_Specify_2: Method.id -> Model.itm list -> Model.itm list
53.11
53.12 val get_fun_ids : theory -> (string * typ) list
53.13 type field
53.14 @@ -16,18 +16,18 @@
53.15 val add_field' : theory -> field list -> Model.ori list -> Model.ori list
53.16 val match_itms_oris : theory -> Model.itm list -> field list * term list * Rule_Set.T ->
53.17 Model.ori list -> bool * (Model.itm list * (bool * term) list)
53.18 - val refine_ori : Model.ori list -> Spec.pblID -> Spec.pblID option
53.19 - val refine_ori' : Model.ori list -> Spec.pblID -> Spec.pblID
53.20 - val refine_pbl : theory -> Spec.pblID -> Model.itm list ->
53.21 - (Spec.pblID * (Model.itm list * (bool * term) list)) option
53.22 + val refine_ori : Model.ori list -> Problem.id -> Problem.id option
53.23 + val refine_ori' : Model.ori list -> Problem.id -> Problem.id
53.24 + val refine_pbl : theory -> Problem.id -> Model.itm list ->
53.25 + (Problem.id * (Model.itm list * (bool * term) list)) option
53.26
53.27 val appc : ('a list -> 'b list) -> 'a Model.ppc -> 'b Model.ppc
53.28 val mappc : ('a -> 'b) -> 'a Model.ppc -> 'b Model.ppc
53.29 val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *)
53.30
53.31 - val get_pbt : Spec.pblID -> Problem.T
53.32 - val get_met : Spec.metID -> Method.T (* for generate.sml *)
53.33 - val get_met' : theory -> Spec.metID -> Method.T (* for pbl-met-hierarchy.sml *)
53.34 + val get_pbt : Problem.id -> Problem.T
53.35 + val get_met : Method.id -> Method.T (* for generate.sml *)
53.36 + val get_met' : theory -> Method.id -> Method.T (* for pbl-met-hierarchy.sml *)
53.37 val get_the : Thy_Html.theID -> Thy_Html.thydata (* for inform.sml *)
53.38
53.39 type pblRD = string list (* for pbl-met-hierarchy.sml *)
53.40 @@ -36,25 +36,25 @@
53.41 val itm_out : theory -> Model.itm_ -> string
53.42 val dsc_unknown : term
53.43
53.44 - val pblID2guh : Spec.pblID -> Check_Unique.guh (* for datatypes.sml *)
53.45 - val metID2guh : Spec.metID -> Check_Unique.guh (* for datatypes.sml *)
53.46 + val pblID2guh : Problem.id -> Check_Unique.guh (* for datatypes.sml *)
53.47 + val metID2guh : Method.id -> Check_Unique.guh (* for datatypes.sml *)
53.48 val kestoreID2guh : Celem.ketype -> Celem.kestoreID -> Check_Unique.guh (* for datatypes.sml *)
53.49 val guh2kestoreID : Check_Unique.guh -> string list (* for interface.sml *)
53.50 (* for Knowledge/, if below at left margin *)
53.51 - val prep_pbt : theory -> Check_Unique.guh -> string list -> Spec.pblID ->
53.52 - string list * (string * string list) list * Rule_Set.T * string option * Spec.metID list ->
53.53 - Problem.T * Spec.pblID
53.54 - val prep_met : theory -> string -> string list -> Spec.pblID ->
53.55 + val prep_pbt : theory -> Check_Unique.guh -> string list -> Problem.id ->
53.56 + string list * (string * string list) list * Rule_Set.T * string option * Method.id list ->
53.57 + Problem.T * Problem.id
53.58 + val prep_met : theory -> string -> string list -> Problem.id ->
53.59 string list * (string * string list) list *
53.60 {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
53.61 rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
53.62 - Method.T * Spec.metID
53.63 + Method.T * Method.id
53.64 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
53.65 val show_ptyps : unit -> unit
53.66 val show_mets : unit -> unit
53.67 datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
53.68 val match_pbl : Selem.fmz_ -> Problem.T -> match'
53.69 - val refine : Selem.fmz_ -> Spec.pblID -> Stool.match list
53.70 + val refine : Selem.fmz_ -> Problem.id -> Stool.match list
53.71 val e_errpat : Error_Fill_Def.errpat
53.72 val show_pblguhs : unit -> unit
53.73 val sort_pblguhs : unit -> unit
53.74 @@ -282,13 +282,13 @@
53.75
53.76 (* pblID are reverted _on calling_ the retrieve-funs *)
53.77 type pblRD = (*e.g. ["equations","univariate","normalise"] for internal retrieval *)
53.78 - Spec.pblID; (*e.g. ["normalise","univariate","equations"] presented to student *)
53.79 + Problem.id; (*e.g. ["normalise","univariate","equations"] presented to student *)
53.80
53.81 (* apply a fun to a ptyps node *)
53.82 fun app_ptyp x = Store.apply (get_ptyps ()) x;
53.83
53.84 (* TODO: generalize search for subthy *)
53.85 -fun get_pbt (pblID: Spec.pblID) =Store.get (get_ptyps ()) pblID (rev pblID)
53.86 +fun get_pbt (pblID: Problem.id) =Store.get (get_ptyps ()) pblID (rev pblID)
53.87
53.88 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
53.89 fun get_met metID =Store.get (get_mets ()) metID metID;
53.90 @@ -686,7 +686,7 @@
53.91 val opt = app_ptyp (refin ((rev o tl) pblID) oris) pblID (rev pblID);
53.92 in case opt of
53.93 SOME pblRD =>
53.94 - let val pblID': Spec.pblID = rev pblRD
53.95 + let val pblID': Problem.id = rev pblRD
53.96 in if pblID' = pblID then NONE else SOME pblID' end
53.97 | NONE => NONE
53.98 end;
54.1 --- a/src/Tools/isac/Specify/specify.sml Wed Apr 22 11:23:30 2020 +0200
54.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Apr 22 14:36:27 2020 +0200
54.3 @@ -33,8 +33,8 @@
54.4 | _ => ("ok", (Pbl, Tactic.Model_Problem))
54.5 else
54.6 let
54.7 - val cpI = if pI = Spec.e_pblID then pI' else pI;
54.8 - val cmI = if mI = Spec.e_metID then mI' else mI;
54.9 + val cpI = if pI = Problem.id_empty then pI' else pI;
54.10 + val cmI = if mI = Method.id_empty then mI' else mI;
54.11 val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
54.12 val pre = Stool.check_preconds "thy 100820" prls where_ pbl;
54.13 val preok = foldl and_ (true, map fst pre);
54.14 @@ -44,7 +44,7 @@
54.15 case p_ of
54.16 Pbl =>
54.17 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
54.18 - else if pI' = Spec.e_pblID andalso pI = Spec.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
54.19 + else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
54.20 else
54.21 case find_first (is_error o #5) pbl of
54.22 SOME (_, _, _, fd, itm_) =>
54.23 @@ -55,8 +55,8 @@
54.24 | NONE => (*pbl-items complete*)
54.25 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
54.26 else if dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
54.27 - else if pI = Spec.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
54.28 - else if mI = Spec.e_metID then ("dummy", (Pbl, Tactic.Specify_Method mI'))
54.29 + else if pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
54.30 + else if mI = Method.id_empty then ("dummy", (Pbl, Tactic.Specify_Method mI'))
54.31 else
54.32 case find_first (is_error o #5) met of
54.33 SOME (_, _, _, fd, itm_) => ("dummy", (Met, mk_delete (ThyC.get_theory dI) fd itm_))
54.34 @@ -72,7 +72,7 @@
54.35 SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))
54.36 | NONE =>
54.37 (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI'))
54.38 - else if pI = Spec.e_pblID then ("dummy", (Met, Tactic.Specify_Problem pI'))
54.39 + else if pI = Problem.id_empty then ("dummy", (Met, Tactic.Specify_Problem pI'))
54.40 else if not preok then ("dummy", (Met, Tactic.Specify_Method mI))
54.41 else ("dummy", (Met, Tactic.Apply_Method mI))))
54.42 | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)
55.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Apr 22 11:23:30 2020 +0200
55.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Apr 22 14:36:27 2020 +0200
55.3 @@ -60,7 +60,7 @@
55.4 let
55.5 val {met, ...} = Specify.get_pbt pI'
55.6 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
55.7 - val mI = if length met = 0 then Spec.e_metID else hd met
55.8 + val mI = if length met = 0 then Method.id_empty else hd met
55.9 val thy = ThyC.get_theory dI
55.10 val (pos, c, _, pt) =
55.11 Generate.generate1 (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
55.12 @@ -96,7 +96,7 @@
55.13 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
55.14 val {ppc,where_,prls,...} = Specify.get_pbt pI
55.15 val pbl =
55.16 - if pI' = Spec.e_pblID andalso pI = Spec.e_pblID
55.17 + if pI' = Problem.id_empty andalso pI = Problem.id_empty
55.18 then (false, (Generate.init_pbl ppc, []))
55.19 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
55.20 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
55.21 @@ -151,7 +151,7 @@
55.22 let (* either """"""""""""""" all empty or complete *)
55.23 val thy = ThyC.get_theory dI'
55.24 val (oris, ctxt) =
55.25 - if dI' = ThyC.id_empty orelse pI' = Spec.e_pblID (*andalso? WN110511*)
55.26 + if dI' = ThyC.id_empty orelse pI' = Problem.id_empty (*andalso? WN110511*)
55.27 then ([], ContextC.empty)
55.28 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
55.29 (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
55.30 @@ -189,7 +189,7 @@
55.31 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
55.32 | _ => error "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
55.33 val {met, thy,...} = Specify.get_pbt pIre
55.34 - val (domID, metID) = (Context.theory_name thy, if length met = 0 then Spec.e_metID else hd met)
55.35 + val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)
55.36 val ((p,_), _, _, pt) =
55.37 Generate.generate1 (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
55.38 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
55.39 @@ -251,9 +251,9 @@
55.40 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
55.41 | _ => error "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"
55.42 val _ = case p_ of Met => met | _ => pbl
55.43 - val cpI = if pI = Spec.e_pblID then pI' else pI
55.44 + val cpI = if pI = Problem.id_empty then pI' else pI
55.45 val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
55.46 - val cmI = if mI = Spec.e_metID then mI' else mI
55.47 + val cmI = if mI = Method.id_empty then mI' else mI
55.48 val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
55.49 val pre = case p_ of
55.50 Met => (Stool.check_preconds thy mer mwh met)
56.1 --- a/src/Tools/isac/TODO.thy Wed Apr 22 11:23:30 2020 +0200
56.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 22 14:36:27 2020 +0200
56.3 @@ -168,7 +168,7 @@
56.4 \end{itemize}
56.5 \item xxx
56.6 \item unify in signature LANGUAGE_TOOLS =\\
56.7 - val pblterm: ThyC.id -> Spec.pblID -> term vvv vvv\\
56.8 + val pblterm: ThyC.id -> Problem.id -> term vvv vvv\\
56.9 val subpbl: string -> string list -> term unify with ^^^
56.10 \item xxx
56.11 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
57.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Apr 22 11:23:30 2020 +0200
57.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Apr 22 14:36:27 2020 +0200
57.3 @@ -883,8 +883,8 @@
57.4 \em Z\_Transform\normalfont.\<close>
57.5
57.6 setup \<open>KEStore_Elems.add_pbts
57.7 - [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
57.8 - prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
57.9 + [prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
57.10 + prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
57.11 (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
57.12
57.13 text\<open>\noindent For the suddenly created node we have to define the input
57.14 @@ -892,7 +892,7 @@
57.15 Section~\ref{sec:deffdes}.\<close>
57.16
57.17 setup \<open>KEStore_Elems.add_pbts
57.18 - [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
57.19 + [prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
57.20 (["Inverse", "Z_Transform", "SignalProcessing"],
57.21 [("#Given" ,["filterExpression X_eq"]),
57.22 ("#Find", ["stepResponse n_eq"])],
58.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Wed Apr 22 11:23:30 2020 +0200
58.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Wed Apr 22 14:36:27 2020 +0200
58.3 @@ -157,11 +157,11 @@
58.4 text \<open>The simplifiers are quite busy when finding the above results. you can
58.5 watch them at work by setting the switch 'Rewrite.trace_on:\<close>
58.6 ML \<open>
58.7 -Celem.Rewrite.trace_on := false;
58.8 +Rewrite.trace_on := false;
58.9 tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
58.10 val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
58.11 tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
58.12 -Celem.Rewrite.trace_on := false;
58.13 +Rewrite.trace_on := false;
58.14 \<close>
58.15 text \<open>You see what happend when you click the checkbox <Tracing> on the bar
58.16 separating this window from the Output-window.
59.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 11:23:30 2020 +0200
59.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 14:36:27 2020 +0200
59.3 @@ -264,14 +264,14 @@
59.4 Model_Problem: Tactic.input;
59.5 Or_to_List: Tactic.input;
59.6
59.7 -Apply_Method: Spec.metID -> Tactic.input;
59.8 -Refine_Tacitly: Spec.pblID -> Tactic.input;
59.9 -Specify_Problem: Spec.pblID -> Tactic.input;
59.10 -Specify_Method: Spec.metID -> Tactic.input;
59.11 +Apply_Method: Method.id -> Tactic.input;
59.12 +Refine_Tacitly: Problem.id -> Tactic.input;
59.13 +Specify_Problem: Problem.id -> Tactic.input;
59.14 +Specify_Method: Method.id -> Tactic.input;
59.15 Substitute: sube -> Tactic.input;; (* Substitute: sube -> tac; e_sube: TermC.as_string list; UNCLEAR HOW TO INPUT *)
59.16 -Check_Postcond: Spec.pblID -> Tactic.input;
59.17 +Check_Postcond: Problem.id -> Tactic.input;
59.18
59.19 -Apply_Method: Spec.metID -> Tactic.input;
59.20 +Apply_Method: Method.id -> Tactic.input;
59.21 val tac = Apply_Method(["test", "equation", "simplify"]);
59.22 xml_of_tac tac;(*
59.23 <STRINGLISTTACTIC name="Apply_Method">
60.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 22 11:23:30 2020 +0200
60.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 22 14:36:27 2020 +0200
60.3 @@ -127,16 +127,16 @@
60.4 "~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);
60.5 val po' = lev_on po;
60.6 wfn (*= pbl2file*)
60.7 -"~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id: Spec.metID), (pbl as {guh,...})) =
60.8 +"~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id: Method.id), (pbl as {guh,...})) =
60.9 (pa, po', (ids@[id]), n);
60.10 strs2str id = "[\"e_pblID\"]"; (*true*)
60.11 pos2str pos = "[1]"; (*true*)
60.12 path ^ guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
60.13 -"~~~~~ fun pbl2xml, args:"; val (id: Spec.pblID, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
60.14 +"~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
60.15 (id, pbl);
60.16 "~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id);
60.17 if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
60.18 - "Problem (Pure', [e_pblID])"
60.19 + "Problem (Pure', [empty_probl_id])"
60.20 then () else error "fun pbl2term changed";
60.21
60.22
61.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 22 11:23:30 2020 +0200
61.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 22 14:36:27 2020 +0200
61.3 @@ -195,7 +195,7 @@
61.4
61.5 Step_Solve.by_tactic m (pt, p);
61.6 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
61.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
61.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
61.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
61.10 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
61.11 val Safe_Step (istate, _, tac) =
61.12 @@ -585,7 +585,7 @@
61.13 setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
61.14 refFormula 1 (get_pos 1 1);
61.15 val ((pt,_),_) = get_calc 1;
61.16 - if get_obj g_spec pt [] = ("thy_empty_id",
61.17 + if get_obj g_spec pt [] = ("empty_thy_id",
61.18 ["LINEAR", "univariate","equation","test"],
61.19 ["Test","solve_linear"]) then ()
61.20 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
61.21 @@ -925,7 +925,7 @@
61.22 loc = (SOME scrst_ctxt, NONE),
61.23 ctxt,
61.24 meth,
61.25 - spec = ("thy_empty_id", ["e_pblID"], ["e_metID"]),
61.26 + spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
61.27 probl,
61.28 branch = TransitiveB,
61.29 origin,
61.30 @@ -987,7 +987,7 @@
61.31 Relate ["relations"]],
61.32 (*input (Arbfix will dissappear soon)*)
61.33 Pbl (*belongsto*),
61.34 - Spec.Spec.empty (*no input to the specification*));
61.35 + Spec.empty (*no input to the specification*));
61.36
61.37 (*the user does not know, what 'superfluous' for 'maximum b' may mean
61.38 and asks what to do next*)
61.39 @@ -1001,7 +1001,7 @@
61.40 [Given ["fixedValues [r=Arbfix]"],
61.41 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
61.42 Relate ["relations [A=a*b, \
61.43 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, Spec.Spec.empty);
61.44 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, Spec.empty);
61.45
61.46 (*specification is not interesting and should be skipped by the dialogguide;
61.47 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
61.48 @@ -1010,14 +1010,14 @@
61.49 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
61.50 Relate ["relations [A=a*b, \
61.51 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
61.52 - ("DiffApp", ["e_pblID"], ["e_metID"]));
61.53 + ("DiffApp", ["empty_probl_id"], ["empty_meth_id"]));
61.54 modifyCalcHead 1 (([],Pbl), "not used here",
61.55 [Given ["fixedValues [r=Arbfix]"],
61.56 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
61.57 Relate ["relations [A=a*b, \
61.58 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
61.59 ("DiffApp", ["maximum_of","function"],
61.60 - ["e_metID"]));
61.61 + ["empty_meth_id"]));
61.62 modifyCalcHead 1 (([],Pbl), "not used here",
61.63 [Given ["fixedValues [r=Arbfix]"],
61.64 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
61.65 @@ -1530,7 +1530,7 @@
61.66 "--------- UC errpat add-fraction, fillpat by input --------------";
61.67 "--------- UC errpat add-fraction, fillpat by input --------------";
61.68 (*cp from BridgeLog Java <=> SML*)
61.69 -CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
61.70 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
61.71 Iterator 1;
61.72 moveActiveRoot 1;
61.73 moveActiveFormula 1 ([],Pbl);
62.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 22 11:23:30 2020 +0200
62.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 22 14:36:27 2020 +0200
62.3 @@ -471,7 +471,7 @@
62.4 "--------- CAS-command on ([],Pbl) -------------------------------";
62.5 "--------- CAS-command on ([],Pbl) -------------------------------";
62.6 val (p,_,f,nxt,_,pt) =
62.7 - CalcTreeTEST [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
62.8 + CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
62.9 val ifo = "solve(x+1=2,x)";
62.10 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
62.11 show_pt pt;
62.12 @@ -485,7 +485,7 @@
62.13 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
62.14 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
62.15 reset_states ();
62.16 -CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
62.17 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
62.18 Iterator 1;
62.19 moveActiveRoot 1;
62.20 replaceFormula 1 "solve(x+1=2,x)";
62.21 @@ -636,7 +636,7 @@
62.22 atomty t;
62.23 "-----------------------------------------------------------------";
62.24 (*1>*)reset_states ();
62.25 -(*2>*)CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
62.26 +(*2>*)CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
62.27 (*3>*)Iterator 1;moveActiveRoot 1;
62.28 "----- here the Headline has been finished";
62.29 (*4>*)moveActiveFormula 1 ([],Pbl);
62.30 @@ -738,7 +738,7 @@
62.31 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
62.32 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
62.33 reset_states ();
62.34 -CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
62.35 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
62.36 (*[[from sml: > @@@@@begin@@@@@
62.37 [[from sml: 1
62.38 [[from sml: <CALCTREE>
62.39 @@ -814,7 +814,7 @@
62.40 [[from sml: <THEORYID> ThyC.id_empty </THEORYID>
62.41 [[from sml: <PROBLEMID>
62.42 [[from sml: <STRINGLIST>
62.43 -[[from sml: <STRING> e_pblID </STRING>
62.44 +[[from sml: <STRING> Problem.id_empty </STRING>
62.45 [[from sml: </STRINGLIST>
62.46 [[from sml: </PROBLEMID>
62.47 [[from sml: <METHODID>
63.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 22 11:23:30 2020 +0200
63.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 22 14:36:27 2020 +0200
63.3 @@ -71,7 +71,7 @@
63.4 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
63.5 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
63.6
63.7 -Spec.e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
63.8 +Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
63.9 val ctxt = get_ctxt pt po;
63.10
63.11 (*generate1 m (Istate.empty, ctxt) (p,p_) pt;
63.12 @@ -203,7 +203,7 @@
63.13 val thy = ThyC.get_theory thy'
63.14 val metID = get_obj g_metID pt pp
63.15 val metID' =
63.16 - if metID = Spec.e_metID
63.17 + if metID = Method.id_empty
63.18 then (thd3 o snd3) (get_obj g_origin pt pp)
63.19 else metID
63.20 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
64.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 22 11:23:30 2020 +0200
64.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 22 14:36:27 2020 +0200
64.3 @@ -118,7 +118,7 @@
64.4 Step_Solve.by_tactic m ptp;
64.5 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
64.6 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
64.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
64.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
64.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
64.10 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
64.11
64.12 @@ -272,7 +272,7 @@
64.13
64.14 Step_Solve.by_tactic m (pt, p);
64.15 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
64.16 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.17 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.18 val thy' = get_obj g_domID pt (par_pblobj pt p);
64.19 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
64.20
64.21 @@ -367,7 +367,7 @@
64.22 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
64.23 Step_Solve.do_next (pt, ip);
64.24 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
64.25 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.26 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.27 val thy' = get_obj g_domID pt (par_pblobj pt p);
64.28 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
64.29
64.30 @@ -418,7 +418,7 @@
64.31 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
64.32 Step_Solve.do_next (pt, ip);
64.33 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
64.34 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.35 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.36 val thy' = get_obj g_domID pt (par_pblobj pt p);
64.37 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
64.38
65.1 --- a/test/Tools/isac/Interpret/ptyps.thy Wed Apr 22 11:23:30 2020 +0200
65.2 +++ b/test/Tools/isac/Interpret/ptyps.thy Wed Apr 22 14:36:27 2020 +0200
65.3 @@ -13,30 +13,30 @@
65.4
65.5 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
65.6 setup \<open>KEStore_Elems.add_pbts
65.7 -[(Specify.prep_pbt thy "pbl_test_refine" [] Spec.e_pblID
65.8 +[(Specify.prep_pbt thy "pbl_test_refine" [] Problem.id_empty
65.9 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
65.10 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Spec.e_pblID
65.11 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
65.12 (["pbla", "refine", "test"],
65.13 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
65.14 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Spec.e_pblID
65.15 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
65.16 (["pbla1","pbla", "refine", "test"],
65.17 [("#Given", ["fixedValues a_a","maximum a_1"])], Rule_Set.empty, NONE, [])),
65.18 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Spec.e_pblID
65.19 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
65.20 (["pbla2","pbla", "refine", "test"],
65.21 [("#Given", ["fixedValues a_a","valuesFor a_2"])], Rule_Set.empty, NONE, [])),
65.22 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Spec.e_pblID
65.23 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
65.24 (["pbla2x","pbla2","pbla", "refine", "test"],
65.25 [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
65.26 Rule_Set.empty, NONE, [])),
65.27 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Spec.e_pblID
65.28 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
65.29 (["pbla2y","pbla2","pbla", "refine", "test"],
65.30 [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
65.31 Rule_Set.empty, NONE, [])),
65.32 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Spec.e_pblID
65.33 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
65.34 (["pbla2z","pbla2","pbla", "refine", "test"],
65.35 [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
65.36 Rule_Set.empty, NONE, [])),
65.37 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Spec.e_pblID
65.38 +(Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
65.39 (["pbla3","pbla", "refine", "test"],
65.40 [("#Given" ,["fixedValues a_a","relations a_3"])],
65.41 Rule_Set.empty, NONE, []))]
66.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 22 11:23:30 2020 +0200
66.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 22 14:36:27 2020 +0200
66.3 @@ -238,7 +238,7 @@
66.4 val {ppc, pre, prls,...} = Specify.get_met mID
66.5 val thy = ThyC.get_theory dI
66.6 val dI'' = if dI = ThyC.id_empty then dI' else dI
66.7 - val pI'' = if pI = Spec.e_pblID then pI' else pI
66.8 + val pI'' = if pI = Problem.id_empty then pI' else pI
66.9 ;
66.10 (*+*)writeln (oris2str oris); (*[
66.11 (1, ["1"], #Given,Streckenlast, ["q_0"]),
67.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 22 11:23:30 2020 +0200
67.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 22 14:36:27 2020 +0200
67.3 @@ -282,7 +282,7 @@
67.4 "solveForVars [c, c_2]", "solution LL"];
67.5
67.6 (*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*)
67.7 -"~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:Spec.pblID)) = (fmz, ["LINEAR","system"]);
67.8 +"~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]);
67.9 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
67.10 ((rev o tl) pblID, fmz, [(*match list*)],
67.11 ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node));
68.1 --- a/test/Tools/isac/Knowledge/equation.sml Wed Apr 22 11:23:30 2020 +0200
68.2 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Apr 22 14:36:27 2020 +0200
68.3 @@ -18,7 +18,7 @@
68.4 "----------- CAS input -------------------------------------------";
68.5 "----------- CAS input -------------------------------------------";
68.6 reset_states ();
68.7 -CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
68.8 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
68.9 Iterator 1;
68.10 moveActiveRoot 1;
68.11 replaceFormula 1 "solve (x+1=2, x)";
69.1 --- a/test/Tools/isac/Knowledge/inssort.sml Wed Apr 22 11:23:30 2020 +0200
69.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Wed Apr 22 14:36:27 2020 +0200
69.3 @@ -119,7 +119,7 @@
69.4 "----------- insertion sort: CAS-command -------------------------------------";
69.5 "----------- insertion sort: CAS-command -------------------------------------";
69.6 "----------- insertion sort: CAS-command -------------------------------------";
69.7 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
69.8 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
69.9 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt, p) "Sort {||1, 3, 2||}";
69.10 show_pt pt;
69.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*)
70.1 --- a/test/Tools/isac/Knowledge/integrate.thy Wed Apr 22 11:23:30 2020 +0200
70.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Wed Apr 22 14:36:27 2020 +0200
70.3 @@ -15,7 +15,7 @@
70.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
70.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
70.6 setup \<open>KEStore_Elems.add_mets
70.7 - [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Spec.e_metID
70.8 + [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Method.id_empty
70.9 (["diff","integration","test"],
70.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
70.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
71.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 22 11:23:30 2020 +0200
71.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 22 14:36:27 2020 +0200
71.3 @@ -371,7 +371,7 @@
71.4 (*solve m (pt, pos);
71.5 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
71.6 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
71.7 -Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
71.8 +Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
71.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
71.10 val (is, sc) = resume_prog thy' (p,p_) pt;
71.11 val d = Rule_Set.empty;
72.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Wed Apr 22 11:23:30 2020 +0200
72.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Apr 22 14:36:27 2020 +0200
72.3 @@ -336,7 +336,7 @@
72.4
72.5 LI.do_next (pt, input_pos);
72.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
72.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
72.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
72.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
72.10
72.11 val (_, (ist, ctxt), sc) =
73.1 --- a/test/Tools/isac/Knowledge/simplify.sml Wed Apr 22 11:23:30 2020 +0200
73.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Wed Apr 22 14:36:27 2020 +0200
73.3 @@ -23,7 +23,7 @@
73.4 "----------- CAS-command Simplify -----------------------";
73.5 "----------- CAS-command Simplify -----------------------";
73.6 reset_states ();
73.7 -CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
73.8 +CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
73.9 Iterator 1;
73.10 moveActiveRoot 1;
73.11 replaceFormula 1 "Simplify (2*a + 3*a)";
74.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 22 11:23:30 2020 +0200
74.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 22 14:36:27 2020 +0200
74.3 @@ -58,7 +58,7 @@
74.4 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
74.5 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
74.6 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)
74.7 -val cpI = if pI = e_pblID then pI' else pI;
74.8 +val cpI = if pI = Problem.id_empty then pI' else pI;
74.9 val cmI = if mI = e_metID then mI' else mI;
74.10 val {ppc, prls, where_, ...} = get_pbt cpI;
74.11 val pre = check_preconds "thy 100820" prls where_ probl;
74.12 @@ -70,7 +70,7 @@
74.13 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
74.14 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
74.15 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
74.16 -val cpI = if pI = e_pblID then pI' else pI;
74.17 +val cpI = if pI = Problem.id_empty then pI' else pI;
74.18 val ctxt = get_ctxt pt (p, Pbl);
74.19 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
74.20 val SOME t = parseNEW ctxt str;
75.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Wed Apr 22 11:23:30 2020 +0200
75.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Wed Apr 22 14:36:27 2020 +0200
75.3 @@ -66,7 +66,7 @@
75.4 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
75.5
75.6 val pt = EmptyPtree;
75.7 -val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], Spec.Spec.empty, TermC.empty, ContextC.empty) pt;
75.8 +val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt;
75.9 val ctxt = get_obj g_ctxt pt [];
75.10 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
75.11
76.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Wed Apr 22 11:23:30 2020 +0200
76.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Wed Apr 22 14:36:27 2020 +0200
76.3 @@ -58,7 +58,7 @@
76.4 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
76.5 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
76.6 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)
76.7 -val cpI = if pI = e_pblID then pI' else pI;
76.8 +val cpI = if pI = Problem.id_empty then pI' else pI;
76.9 val cmI = if mI = e_metID then mI' else mI;
76.10 val {ppc, prls, where_, ...} = get_pbt cpI;
76.11 val pre = check_preconds "thy 100820" prls where_ probl;
76.12 @@ -70,7 +70,7 @@
76.13 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
76.14 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
76.15 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
76.16 -val cpI = if pI = e_pblID then pI' else pI;
76.17 +val cpI = if pI = Problem.id_empty then pI' else pI;
76.18 val ctxt = get_ctxt pt (p, Pbl);
76.19 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
76.20 val SOME t = parseNEW ctxt str;
77.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 11:23:30 2020 +0200
77.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 14:36:27 2020 +0200
77.3 @@ -49,7 +49,7 @@
77.4 case context_pbl keID pt pp of (true,["univariate","equation"],_,_,_)=>()
77.5 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
77.6
77.7 -case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
77.8 +case get_obj g_spec pt p of (_, ["empty_probl_id"], _) => ()
77.9 | _ => error "mathengine.sml: context_pbl .. pbl still empty";
77.10 setContext 1 pos guh;
77.11 val ((pt,_),_) = get_calc 1;
77.12 @@ -116,7 +116,7 @@
77.13 ip = p; (*false*)
77.14 member op = [Pbl,Met] p_; (*false*)
77.15 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
77.16 -Spec.e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
77.17 +Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
77.18 val thy' = get_obj g_domID pt (par_pblobj pt p);
77.19 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
77.20
77.21 @@ -165,7 +165,7 @@
77.22 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
77.23 dI = ThyC.id_empty; (*true*)
77.24 odI = "Build_Inverse_Z_Transform"; (*true*)
77.25 -dI = "thy_empty_id"; (*true*)
77.26 +dI = "empty_thy_id"; (*true*)
77.27 "~~~~~ after fun some_spec:";
77.28 val (dI, pI, mI) = some_spec ospec spec;
77.29 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
77.30 @@ -204,7 +204,7 @@
77.31 val is = init_istate tac t
77.32 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
77.33 is wrong for simpl, but working ?!? *)
77.34 - val tac_ = Apply_Method' (Spec.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
77.35 + val tac_ = Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
77.36 val pos' = ((lev_on o lev_dn) p, Frm)
77.37 val thy = ThyC.get_theory "Isac_Knowledge"
77.38 val (_,_,_,pt') = (*implicit Take*)generate1 tac_ (is, ctxt) (pt, pos');
77.39 @@ -220,7 +220,7 @@
77.40 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
77.41 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
77.42 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
77.43 -Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
77.44 +Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
77.45 val thy' = get_obj g_domID pt (par_pblobj pt p);
77.46 val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
77.47 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
78.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Apr 22 11:23:30 2020 +0200
78.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Apr 22 14:36:27 2020 +0200
78.3 @@ -11,7 +11,7 @@
78.4 ("Isac_Knowledge", ["sqroot-test","univariate","equation","test"],
78.5 ["Test","squ-equ-test-subpbl1"]);
78.6 "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
78.7 -"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : fmz_, (dI, pI, mI) : Spec.spec) = (fmz, sp);
78.8 +"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : fmz_, (dI, pI, mI) : Spec.T) = (fmz, sp);
78.9 val thy = ThyC.get_theory dI;
78.10 (*if*) mI = ["no_met"]; (*else*)
78.11 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
79.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Wed Apr 22 11:23:30 2020 +0200
79.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Wed Apr 22 14:36:27 2020 +0200
79.3 @@ -32,8 +32,8 @@
79.4 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
79.5 probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
79.6 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*)
79.7 - val cpI = if pI = Spec.e_pblID then pI' else pI;
79.8 - val cmI = if mI = Spec.e_metID then mI' else mI;
79.9 + val cpI = if pI = Problem.id_empty then pI' else pI;
79.10 + val cmI = if mI = Method.id_empty then mI' else mI;
79.11 val {ppc, prls, where_, ...} = get_pbt cpI;
79.12 val pre = check_preconds "thy 100820" prls where_ probl;
79.13 val pb = foldl and_ (true, map fst pre);
79.14 @@ -41,13 +41,13 @@
79.15 (* val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
79.16 (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
79.17 ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
79.18 -"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : Spec.spec),
79.19 - ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : Spec.spec)) =
79.20 +"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : Spec.T),
79.21 + ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) =
79.22 (p_, pb, oris, (dI',pI',mI'), (probl, meth),
79.23 (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
79.24
79.25 dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
79.26 -pI' = Spec.e_pblID andalso pI = Spec.e_pblID; (* = false*)
79.27 +pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)
79.28 find_first (is_error o #5) (pbl:itm list); (* = NONE*)
79.29
79.30 (* nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl;
80.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Wed Apr 22 11:23:30 2020 +0200
80.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Wed Apr 22 14:36:27 2020 +0200
80.3 @@ -42,8 +42,8 @@
80.4 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
80.5 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
80.6 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
80.7 - val cpI = if pI = Spec.e_pblID then pI' else pI;
80.8 - val cmI = if mI = Spec.e_metID then mI' else mI;
80.9 + val cpI = if pI = Problem.id_empty then pI' else pI;
80.10 + val cmI = if mI = Method.id_empty then mI' else mI;
80.11 val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
80.12
80.13 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
81.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 22 11:23:30 2020 +0200
81.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 22 14:36:27 2020 +0200
81.3 @@ -64,14 +64,14 @@
81.4 (*expects same sequence of (actual) args in itms and (formal) args in met*)
81.5 fun msg_miss sc metID caller f formals actuals =
81.6 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
81.7 - "and the actual args., ie. items of the guard of \"" ^ Spec.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
81.8 + "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
81.9 "formal arg \"" ^ UnparseC.term f ^ "\" doesn't mach an actual arg.\n" ^
81.10 "with:\n" ^
81.11 (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms formals ^ "\n" ^
81.12 (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms actuals
81.13 fun msg_ambiguous sc metID f aas formals actuals =
81.14 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
81.15 - "and the actual args., ie. items of the guard of \"" ^ Spec.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
81.16 + "and the actual args., ie. items of the guard of \"" ^ Method.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
81.17 "formal arg. \"" ^ UnparseC.term f ^ "\" type-matches with several..." ^
81.18 "actual args. \"" ^ UnparseC.terms aas ^ "\"\n" ^
81.19 "selected \"" ^ UnparseC.term (hd aas) ^ "\"\n" ^
81.20 @@ -125,7 +125,7 @@
81.21 case pIopt of SOME _ => ();
81.22
81.23 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
81.24 -Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
81.25 +Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = false*);
81.26 val thy' = get_obj g_domID pt (par_pblobj pt p);
81.27 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
81.28 "~~~~~ fun find_next_step , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
82.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 22 11:23:30 2020 +0200
82.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 22 14:36:27 2020 +0200
82.3 @@ -41,7 +41,7 @@
82.4
82.5 Step_Solve.by_tactic m ptp;
82.6 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
82.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);
82.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);
82.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
82.10 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
82.11
82.12 @@ -96,8 +96,8 @@
82.13 (*if*) member op = [Pbl, Met] p_ = false;
82.14
82.15 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
82.16 - Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
82.17 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*);
82.18 + Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
82.19 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p)(*else*);
82.20 val thy' = get_obj g_domID pt (par_pblobj pt p);
82.21 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
82.22
82.23 @@ -150,7 +150,7 @@
82.24
82.25 Step_Solve.do_next (pt, ip);
82.26 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
82.27 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
82.28 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
82.29 val thy' = get_obj g_domID pt (par_pblobj pt p);
82.30 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
82.31
83.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Apr 22 11:23:30 2020 +0200
83.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Apr 22 14:36:27 2020 +0200
83.3 @@ -35,8 +35,8 @@
83.4 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
83.5
83.6 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
83.7 - val cpI = if pI = Spec.e_pblID then pI' else pI;
83.8 - val cmI = if mI = Spec.e_metID then mI' else mI;
83.9 + val cpI = if pI = Problem.id_empty then pI' else pI;
83.10 + val cmI = if mI = Method.id_empty then mI' else mI;
83.11 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
83.12 val pre = Stool.check_preconds "thy 100820" prls where_ probl;
83.13 val pb = foldl and_ (true, map fst pre);
84.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 22 11:23:30 2020 +0200
84.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 22 14:36:27 2020 +0200
84.3 @@ -37,7 +37,7 @@
84.4 (*val (msg, cs') =*)
84.5 Step_Solve.by_tactic m (pt, p);
84.6 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
84.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
84.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
84.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
84.10 val (is, sc) = resume_prog thy' (p,p_) pt;
84.11
85.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Apr 22 11:23:30 2020 +0200
85.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Wed Apr 22 14:36:27 2020 +0200
85.3 @@ -52,7 +52,7 @@
85.4
85.5 LI.do_next (pt, ip);
85.6 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
85.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
85.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
85.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
85.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
85.11
86.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Apr 22 11:23:30 2020 +0200
86.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Wed Apr 22 14:36:27 2020 +0200
86.3 @@ -44,7 +44,7 @@
86.4 (*if*) member op = [Pbl,Met] p_; (*= false*)
86.5
86.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
86.7 -(*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
86.8 +(*if*) Method.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
87.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Apr 22 11:23:30 2020 +0200
87.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Apr 22 14:36:27 2020 +0200
87.3 @@ -53,7 +53,7 @@
87.4 tacis; (*= []*)
87.5 member op = [Pbl,Met] p_; (*= false*)
87.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
87.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
87.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
87.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
87.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
87.11
88.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Wed Apr 22 11:23:30 2020 +0200
88.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Wed Apr 22 14:36:27 2020 +0200
88.3 @@ -106,7 +106,7 @@
88.4
88.5 Step_Solve.do_next (pt, ip);
88.6 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
88.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
88.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
88.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
88.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
88.11
89.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Apr 22 11:23:30 2020 +0200
89.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Apr 22 14:36:27 2020 +0200
89.3 @@ -91,7 +91,7 @@
89.4
89.5 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
89.6
89.7 - val tac_ = Tactic.Apply_Method' (Spec.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
89.8 + val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
89.9 val pos' = ((lev_on o lev_dn) p, Frm)
89.10 val thy = ThyC.get_theory "Isac_Knowledge"
89.11 val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *);
90.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Apr 22 11:23:30 2020 +0200
90.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Apr 22 14:36:27 2020 +0200
90.3 @@ -49,7 +49,7 @@
90.4
90.5 LI.do_next (pt, input_pos);
90.6 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
90.7 - (*if*) Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
90.8 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
90.9 val thy' = get_obj g_domID pt (par_pblobj pt p);
90.10 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
90.11
91.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 22 11:23:30 2020 +0200
91.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 22 14:36:27 2020 +0200
91.3 @@ -276,15 +276,15 @@
91.4 val pt = update_met pt [] [];
91.5 (*
91.6 > get_obj g_spec pt [];
91.7 -val it = ("thy_empty_id",["e_pblID"],("thy_empty_id","e_metID")) : spec
91.8 +val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec
91.9 > val pt = update_domID pt [] "RatArith";
91.10 > get_obj g_spec pt [];
91.11 -val it = ("RatArith",["e_pblID"],("thy_empty_id","e_metID")) : spec
91.12 +val it = ("RatArith",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec
91.13 > val pt = update_pblID pt [] ["RatArith",
91.14 "equations","univariate","square-root"];
91.15 > get_obj g_spec pt [];
91.16 ("RatArith",["RatArith","equations","univariate","square-root"],
91.17 - ("thy_empty_id","e_metID")) : spec
91.18 + ("empty_thy_id","empty_meth_id")) : spec
91.19 > val pt = update_metID pt [] ("RatArith","sqrt-equ-test");
91.20 > get_obj g_spec pt [];
91.21 ("RatArith",["RatArith","equations","univariate","square-root"],
91.22 @@ -413,7 +413,7 @@
91.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
91.24 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
91.25 > get_obj g_spec pt (fst p);
91.26 -val it = ("thy_empty_id",["e_pblID"],("thy_empty_id","e_metID")) : spec*)
91.27 +val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec*)
91.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
91.29 (*val nxt = ("Specify_Problem", Specify_Problem *)
91.30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
92.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Apr 22 11:23:30 2020 +0200
92.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Apr 22 14:36:27 2020 +0200
92.3 @@ -20,9 +20,9 @@
92.4 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
92.5 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
92.6 KEStore_Elems.add_pbts
92.7 - [prep_pbt Test.thy "pbl_testss" [] e_pblID
92.8 + [prep_pbt Test.thy "pbl_testss" [] Problem.id_empty
92.9 (["tests"], []:(string * string list) list, Rule_Set.empty, NONE, []),
92.10 - prep_pbt Test.thy "pbl_testss_term" [] e_pblID
92.11 + prep_pbt Test.thy "pbl_testss_term" [] Problem.id_empty
92.12 (["met_testterm","tests"],
92.13 [("#Given" ,["realTestGiven g_"]),
92.14 ("#Find" ,["realTestFind f_"])],
92.15 @@ -90,7 +90,7 @@
92.16 " --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
92.17 " --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
92.18 KEStore_Elems.add_pbts
92.19 - [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
92.20 + [prep_pbt Test.thy "pbl_testss_eq" [] Problem.id_empty
92.21 (["met_testeq","tests"],
92.22 [("#Given" ,["boolTestGiven e_e"]),
92.23 ("#Find" ,["boolTestFind v_i_"])],
93.1 --- a/test/Tools/isac/ProgLang/calculate.thy Wed Apr 22 11:23:30 2020 +0200
93.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed Apr 22 14:36:27 2020 +0200
93.3 @@ -18,8 +18,8 @@
93.4 \<close>
93.5
93.6 setup \<open>KEStore_Elems.add_pbts
93.7 - [Specify.prep_pbt @{theory "Test"} "pbl_ttest" [] Spec.e_pblID (["test"], [], Rule_Set.empty, NONE, []),
93.8 - Specify.prep_pbt @{theory "Test"} "pbl_ttest_calc" [] Spec.e_pblID
93.9 + [Specify.prep_pbt @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
93.10 + Specify.prep_pbt @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
93.11 (["calculate", "test"],
93.12 [("#Given", ["realTestGiven t_t"]),
93.13 ("#Find", ["realTestFind s_s"])],
93.14 @@ -34,7 +34,7 @@
93.15 (Try (Repeat (Calculate ''DIVIDE''))) #>
93.16 (Try (Repeat (Calculate ''POWER''))))) t_t"
93.17 setup \<open>KEStore_Elems.add_mets
93.18 - [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Spec.e_metID
93.19 + [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Method.id_empty
93.20 (["Test","test_calculate"],
93.21 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
93.22 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
94.1 --- a/test/Tools/isac/Specify/appl.sml Wed Apr 22 11:23:30 2020 +0200
94.2 +++ b/test/Tools/isac/Specify/appl.sml Wed Apr 22 14:36:27 2020 +0200
94.3 @@ -58,7 +58,7 @@
94.4 val pblobj as (PblObj{meth, origin = origin as (oris,(dI', pI', mI'), _),
94.5 probl, spec = (dI, pI, mI), ...}) = get_obj I pt p;
94.6 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
94.7 -val cpI = if pI = e_pblID then pI' else pI;
94.8 +val cpI = if pI = Problem.id_empty then pI' else pI;
94.9 val cmI = if mI = e_metID then mI' else mI;
94.10 val {ppc, prls, where_, ...} = get_pbt cpI;
94.11 val pre = check_preconds "thy 100820" prls where_ probl;
94.12 @@ -74,7 +74,7 @@
94.13 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
94.14 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
94.15 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
94.16 -val cpI = if pI = e_pblID then pI' else pI;
94.17 +val cpI = if pI = Problem.id_empty then pI' else pI;
94.18 val ctxt = get_ctxt pt (p, Pbl);
94.19 oris; (*= [(1, [1], "#Given", Const ("Input_Descript.equality", "HOL.bool...*)
94.20 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
95.1 --- a/test/Tools/isac/Specify/calchead.sml Wed Apr 22 11:23:30 2020 +0200
95.2 +++ b/test/Tools/isac/Specify/calchead.sml Wed Apr 22 14:36:27 2020 +0200
95.3 @@ -234,12 +234,12 @@
95.4 EmptyPtree;
95.5 val nxt = tac2tac_ pt p nxt;
95.6 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
95.7 -(*val nxt = Specify_Theory "thy_empty_id" : tac*)
95.8 +(*val nxt = Specify_Theory "empty_thy_id" : tac*)
95.9
95.10 val nxt = Specify_Theory "DiffApp";
95.11 val nxt = tac2tac_ pt p nxt;
95.12 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
95.13 -(*val nxt = Specify_Problem ["e_pblID"] : tac*)
95.14 +(*val nxt = Specify_Problem ["empty_probl_id"] : tac*)
95.15
95.16 val nxt = Specify_Problem ["maximum_of","function"];
95.17 val nxt = tac2tac_ pt p nxt;
95.18 @@ -275,7 +275,7 @@
95.19 val nxt = Add_Relation "relations [(A=a+b)]";
95.20 val nxt = tac2tac_ pt p nxt;
95.21 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
95.22 -(*val nxt = Specify_Method ("thy_empty_id","e_metID") : tac*)
95.23 +(*val nxt = Specify_Method ("empty_thy_id","empty_meth_id") : tac*)
95.24
95.25 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
95.26 val nxt = tac2tac_ pt p nxt;
95.27 @@ -689,7 +689,7 @@
95.28 loc =
95.29 (Some (Pstate ([], [], None, Const ("empty", "'a"), Sundef, false)),
95.30 None),
95.31 - cell = None, meth = [], spec = ("thy_empty_id", ["e_pblID"], ["e_metID"]),
95.32 + cell = None, meth = [], spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
95.33 probl = [], branch = TransitiveB,
95.34 origin =
95.35 ([(1, [1], "#Given",
95.36 @@ -751,7 +751,7 @@
95.37 (Pstate ([], [], None, Const ("empty", "'a"), Sundef, false)),
95.38 None),
95.39 cell = None, meth = [], spec =
95.40 - ("thy_empty_id", ["e_pblID"], ["e_metID"]), probl =
95.41 + ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]), probl =
95.42 [(0, [], false, "#Given",
95.43 Inc ((Const ("Input_Descript.functionTerm",
95.44 "Real.real => Tools.una"),[]),
96.1 --- a/test/Tools/isac/Specify/step-specify.sml Wed Apr 22 11:23:30 2020 +0200
96.2 +++ b/test/Tools/isac/Specify/step-specify.sml Wed Apr 22 14:36:27 2020 +0200
96.3 @@ -27,7 +27,7 @@
96.4 pt;(*isa==REP*)
96.5 val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _)
96.6 = get_obj g_origin pt (fst p);
96.7 -get_obj g_spec pt (fst p) = ("thy_empty_id", ["e_pblID"], ["e_metID"]); (*isa==REP*)
96.8 +get_obj g_spec pt (fst p) = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]); (*isa==REP*)
96.9
96.10 (*this steps into according to "----- step 2 ---" below*)
96.11 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
96.12 @@ -57,8 +57,8 @@
96.13 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
96.14 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
96.15 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
96.16 - val cpI = if pI = Spec.e_pblID then pI' else pI;
96.17 - val cmI = if mI = Spec.e_metID then mI' else mI;
96.18 + val cpI = if pI = Problem.id_empty then pI' else pI;
96.19 + val cmI = if mI = Method.id_empty then mI' else mI;
96.20 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
96.21 val pre = Stool.check_preconds "thy 100820" prls where_ probl;
96.22 val pb = foldl and_ (true, map fst pre);
96.23 @@ -69,7 +69,7 @@
96.24 (* vv----^^*)
96.25 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI));
96.26 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
96.27 - (*if*) pI' = Spec.e_pblID andalso pI = Spec.e_pblID (*else*);
96.28 + (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
96.29 val NONE = (*case*) find_first (is_error o #5) pbl (*of*);
96.30 val NONE = (*case*) nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
96.31 (*if*) not preok (*else*);
96.32 @@ -95,7 +95,7 @@
96.33 Nd (PblObj
96.34 :
96.35 result = (Const ("empty", "??.'a"), []), spec =
96.36 - ("Integrate", ["integrate", "function"], ["e_metID"])},
96.37 + ("Integrate", ["integrate", "function"], ["empty_meth_id"])},
96.38 []):
96.39 ctree*)
96.40