1.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Tue May 12 17:42:29 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Wed May 13 11:34:05 2020 +0200
1.3 @@ -7,19 +7,17 @@
1.4 signature STORE_TREE =
1.5 sig
1.6 type key
1.7 -(*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list *)
1.8 datatype 'a node = Node of string * 'a list * 'a node list
1.9 type 'a T = 'a node list
1.10
1.11 -(*val merge_ptyps: 'a T * 'a T -> 'a T *)
1.12 val merge: 'a T * 'a T -> 'a T
1.13 -(*val insrt: key -> 'a -> string list -> 'a T -> 'a T *)
1.14 val insert: key -> 'a -> string list -> 'a T -> 'a T
1.15 -(*val get_py: 'a T -> key -> (*rev*)key -> 'a *)
1.16 + val scan : string list -> 'a T -> string list list
1.17 +
1.18 val get: 'a T -> key -> (*rev*)key -> 'a
1.19 -(*val update_ptyps: key -> string list -> 'a -> 'a T -> 'a T *)
1.20 + val get_all: 'a T -> 'a list
1.21 +
1.22 val update: key -> string list -> 'a -> 'a T -> 'a T
1.23 -(*val app_py: 'a T -> ('a node -> 'b) -> key -> (*rev*)key -> 'b *)
1.24 val apply: 'a T -> ('a node -> 'b) -> key -> (*rev*)key -> 'b
1.25
1.26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.27 @@ -74,7 +72,14 @@
1.28 )
1.29 | insert _ _ _ _ = raise ERROR "";
1.30
1.31 -fun apply p f (d(*:pblID*)) (k(*:pblRD*)) =
1.32 +fun scan _ [] = [] (* no base case, for empty doms only *)
1.33 + | scan id ((Node ((i, _, []))) :: []) = [id @ [i]]
1.34 + | scan id ((Node ((i, _, pl))) :: []) = scan (id @ [i]) pl
1.35 + | scan id ((Node ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
1.36 + | scan id ((Node ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
1.37 +
1.38 +
1.39 + fun apply p f (d(*:pblID*)) (k(*:pblRD*)) =
1.40 let
1.41 fun py_err _ = raise ERROR ("apply: not found: " ^ strs2str d);
1.42 fun app_py' _ [] = py_err ()
1.43 @@ -90,6 +95,15 @@
1.44 | extract_py _ = raise ERROR ("extract_py: Node has wrong format.");
1.45 in apply p extract_py end;
1.46
1.47 +fun get_all ptyp =
1.48 +let
1.49 + fun scan [] = []
1.50 + | scan ((Node ((_, data, []))) :: []) = data
1.51 + | scan ((Node ((_, data, pl))) :: []) = data @ scan pl
1.52 + | scan ((Node ((_, data, []))) :: ps) = data @ scan ps
1.53 + | scan ((Node ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
1.54 +in scan ptyp end
1.55 +
1.56 fun update ID _ _ [] =
1.57 raise ERROR ("update: " ^ strs2str' ID ^ " does not exist")
1.58 | update ID [i] data ((py as Node (key, _, pys)) :: pyss) =
2.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue May 12 17:42:29 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed May 13 11:34:05 2020 +0200
2.3 @@ -4,6 +4,7 @@
2.4 *)
2.5 signature PROBLEM_METHOD_HIERARCHY =
2.6 sig
2.7 + val format_pblIDl : string list list -> string
2.8 eqtype filepath
2.9 val file2str: filepath -> Thy_Present.filename -> string
2.10 val hierarchy: string -> 'a Store.node list -> string
2.11 @@ -33,6 +34,9 @@
2.12 struct
2.13 (**)
2.14
2.15 +fun format_pblID strl = enclose " [" "]" (commas_quote strl);
2.16 +fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
2.17 +
2.18 type filepath = string;
2.19
2.20 fun file2str path fnm =
3.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue May 12 17:42:29 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed May 13 11:34:05 2020 +0200
3.3 @@ -46,6 +46,7 @@
3.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.5 (*NONE*)
3.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.7 + val get_fun_ids: theory -> (string * typ) list
3.8 val thenode: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
3.9 string list -> 'a -> 'b) -> 'a Store.node -> unit
3.10 val thenodes: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
3.11 @@ -59,10 +60,27 @@
3.12 (**)
3.13 open TermC (* allows contains_one_of to be infix *)
3.14
3.15 +fun fun_id_of ({scr = prog, ...} : Method.T) =
3.16 + case prog of
3.17 + Rule.Empty_Prog => NONE
3.18 + | Rule.Prog t =>
3.19 + (case t of
3.20 + Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
3.21 + | _ => SOME (Program.get_fun_id t))
3.22 + | Rule.Rfuns _ => NONE
3.23 +fun get_fun_ids thy =
3.24 + let
3.25 + val mets = Store.get_all (KEStore_Elems.get_mets thy)
3.26 + (* all mets of the respective theory PLUS of all ancestor theories*)
3.27 + val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
3.28 + in
3.29 + filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
3.30 + end
3.31 +
3.32 (* copy from mutabelle_extra.ML, fun thms_of *)
3.33 fun thms_of thy = (* das ist zu verbessern *)
3.34 let
3.35 - val fun_ids = Specify.get_fun_ids thy
3.36 + val fun_ids = get_fun_ids thy
3.37 in
3.38 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
3.39 andalso not (thm contains_one_of fun_ids)
3.40 @@ -135,7 +153,7 @@
3.41 thm = thm})
3.42 end
3.43
3.44 -fun show_thes () = (writeln o Specify.format_pblIDl o (Specify.scan [])) (get_thes ());
3.45 +fun show_thes () = (writeln o Pbl_Met_Hierarchy.format_pblIDl o (Store.scan [])) (get_thes ());
3.46
3.47
3.48 (** create an xml representation for thehier: hierarchy of entries + files per entry **)
4.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Tue May 12 17:42:29 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed May 13 11:34:05 2020 +0200
4.3 @@ -12,9 +12,12 @@
4.4 type id = Error_Pattern_Def.id
4.5 type T = Error_Pattern_Def.T
4.6 val s_to_string : T list -> string
4.7 + val empty: T
4.8
4.9 type fill_in_id = Error_Pattern_Def.fill_in_id
4.10 type fill_in = Error_Pattern_Def.fill_in
4.11 + val fill_in_empty: fill_in
4.12 +
4.13 type record
4.14
4.15 val from_store: Tactic.input -> Error_Pattern_Def.id list
4.16 @@ -40,9 +43,12 @@
4.17 type id = Error_Pattern_Def.id;
4.18 type T = Error_Pattern_Def.T;
4.19 val s_to_string = Error_Pattern_Def.s_to_string;
4.20 +val empty = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}])
4.21
4.22 type fill_in_id = Error_Pattern_Def.fill_in_id;
4.23 type fill_in = Error_Pattern_Def.fill_in;
4.24 +val fill_in_empty = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
4.25 +
4.26 type record = (fill_in_id * term * thm * Subst.input option);
4.27
4.28 (*
5.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Tue May 12 17:42:29 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Wed May 13 11:34:05 2020 +0200
5.3 @@ -85,7 +85,7 @@
5.4 bool * (* input on this item is not/complete *)
5.5 m_field * (* #Given | #Find | #Relate *)
5.6 i_model_feedback; (* see above *)
5.7 - type i_model = i_model_single list;
5.8 +type i_model = i_model_single list;
5.9 val i_model_empty = (0, [], false, "i_model_empty", Syn "i_model_empty");
5.10
5.11 (**)end(**)
6.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 12 17:42:29 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed May 13 11:34:05 2020 +0200
6.3 @@ -148,7 +148,7 @@
6.4 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
6.5 else pI'
6.6 val {ppc, where_, prls, ...} = Problem.from_store pblID
6.7 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
6.8 + val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
6.9 in
6.10 (model_ok, pblID, hdl, pbl, pre)
6.11 end
6.12 @@ -163,7 +163,7 @@
6.13 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
6.14 else mI'
6.15 val {ppc, pre, prls, scr, ...} = Method.from_store metID
6.16 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
6.17 + val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
6.18 in
6.19 (model_ok, metID, scr, pbl, pre)
6.20 end
6.21 @@ -176,7 +176,7 @@
6.22 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
6.23 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
6.24 val {ppc,where_,prls,...} = Problem.from_store pI
6.25 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
6.26 + val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
6.27 in
6.28 (model_ok, pI, hdl, pbl, pre)
6.29 end
6.30 @@ -188,7 +188,7 @@
6.31 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
6.32 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
6.33 val {ppc,pre,prls,scr,...} = Method.from_store mI
6.34 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
6.35 + val (model_ok, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
6.36 in
6.37 (model_ok, mI, scr, pbl, pre)
6.38 end
6.39 @@ -204,7 +204,7 @@
6.40 NONE => (*copy from context_pbl*)
6.41 let
6.42 val {ppc,where_,prls,...} = Problem.from_store pI
6.43 - val (_, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
6.44 + val (_, (pbl, pre)) = Model.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
6.45 in
6.46 (false, pI, hdl, pbl, pre)
6.47 end
7.1 --- a/src/Tools/isac/Specify/model.sml Tue May 12 17:42:29 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/model.sml Wed May 13 11:34:05 2020 +0200
7.3 @@ -9,16 +9,22 @@
7.4 sig
7.5 datatype match =
7.6 Matches of Problem.id * P_Model.T
7.7 - | NoMatch of Problem.id * P_Model.T
7.8 + | NoMatch of Problem.id * P_Model.T
7.9 val matchs2str : match list -> string
7.10
7.11 - val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Def.rule_set ->
7.12 - bool * (O_Model.T * Pre_Conds.T)
7.13 + val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
7.14 +(*unify ^^^^^^^^^^ vvvvvvvvvv
7.15 + vvvvvvvvv ^^^^^^^^^*)
7.16 + val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
7.17 + bool * (I_Model.T * Pre_Conds.T)
7.18 + val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
7.19 + O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
7.20
7.21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.22 + datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
7.23 + val match_pbl : Formalise.model -> Problem.T -> match'
7.24 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.25 (*NONE*)
7.26 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.27 - val match_oris: theory -> Rule_Def.rule_set -> O_Model.T -> Model_Pattern.T * term list -> bool
7.28 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.29 end
7.30
7.31 @@ -74,7 +80,7 @@
7.32
7.33 (* check a problem (ie. ori list) for matching a problemtype,
7.34 returns items for output to math-experts *)
7.35 -fun match_oris' thy oris (ppc,pre,prls) =
7.36 +fun match_oris' thy oris (ppc, pre, prls) =
7.37 let
7.38 val itms = (flat o (map (chk1_ thy ppc))) oris;
7.39 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
7.40 @@ -84,4 +90,54 @@
7.41 val pb = foldl and_ (true, map fst pre');
7.42 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
7.43
7.44 +
7.45 +(** check a problem (ie. itm list) for matching a problemtype **)
7.46 +
7.47 +(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
7.48 + for missing items get data from formalization (ie. ori list);
7.49 + takes the I_Model.vars_of for concluding completeness (could be another!)
7.50 +
7.51 + (0) determine the most frequent variant mv in pbl
7.52 + ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
7.53 + (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
7.54 + (3) newitms = filter (mv mem vat(news)) news
7.55 + (4) pbt @ newitms *)
7.56 +fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
7.57 + let
7.58 + (*0*)val mv = I_Model.max_vt pbl;
7.59 +
7.60 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
7.61 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
7.62 + SOME _ => false | NONE => true;
7.63 + (*1*)val mis = (filter (notmem pbl)) pbt;
7.64 +
7.65 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
7.66 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
7.67 + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
7.68 + val news = (flat o (map (oris2itms oris))) mis;
7.69 + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
7.70 + val newitms = filter mem_vat news;
7.71 + (*4*)val itms' = pbl @ newitms;
7.72 + val pre' = Pre_Conds.check prls pre itms' mv;
7.73 + val pb = foldl and_ (true, map fst pre');
7.74 + in (length mis = 0 andalso pb, (itms', pre')) end;
7.75 +
7.76 +
7.77 +(** for use by math-authors **)
7.78 +
7.79 +datatype match' = (* for the user *)
7.80 + Matches' of P_Model.T
7.81 +| NoMatch' of P_Model.T;
7.82 +
7.83 +(* match a formalization with a problem type, for tests *)
7.84 +fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
7.85 + let
7.86 + val oris = O_Model.init fmz thy ppc(* |> #1*);
7.87 + val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
7.88 + in
7.89 + if bool
7.90 + then Matches' (P_Model.from thy itms pre')
7.91 + else NoMatch' (P_Model.from thy itms pre')
7.92 + end;
7.93 +
7.94 (**)end(**)
8.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue May 12 17:42:29 2020 +0200
8.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed May 13 11:34:05 2020 +0200
8.3 @@ -7,14 +7,7 @@
8.4 sig
8.5 val hack_until_review_Specify_1: Method.id -> I_Model.T -> I_Model.T
8.6 val hack_until_review_Specify_2: Method.id -> I_Model.T -> I_Model.T
8.7 -
8.8 - val get_fun_ids : theory -> (string * typ) list
8.9
8.10 - val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
8.11 - O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
8.12 -
8.13 - val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
8.14 - val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *)
8.15 val itm_out : theory -> I_Model.feedback -> string
8.16
8.17 datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
8.18 @@ -27,33 +20,21 @@
8.19 val metID2guh : Method.id -> Check_Unique.id (* for datatypes.sml *)
8.20 val kestoreID2guh : ketype -> kestoreID -> Check_Unique.id (* for datatypes.sml *)
8.21 val guh2kestoreID : Check_Unique.id -> string list (* for interface.sml *)
8.22 - (* for Knowledge/, if below at left margin *)
8.23 +
8.24 val prep_pbt : theory -> Check_Unique.id -> string list -> Problem.id ->
8.25 string list * (string * string list) list * Rule_Set.T * string option * Method.id list ->
8.26 - Problem.T * Problem.id
8.27 + Problem.T * Problem.id
8.28 val prep_met : theory -> string -> string list -> Problem.id ->
8.29 string list * (string * string list) list *
8.30 {calc: 'a, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T, prls: Rule_Set.T,
8.31 rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
8.32 Method.T * Method.id
8.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.34 - val show_ptyps : unit -> unit
8.35 - val show_mets : unit -> unit
8.36 - datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
8.37 - val match_pbl : Formalise.model -> Problem.T -> match'
8.38 - val e_errpat : Error_Pattern_Def.T
8.39 - val show_pblguhs : unit -> unit
8.40 - val sort_pblguhs : unit -> unit
8.41 + (*NONE*)
8.42 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.43 val split_did: term -> term * term
8.44 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.45
8.46 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
8.47 - val e_fillpat : string * term * string
8.48 - val coll_vats : ''a list * ('b * ''a list * 'c * 'd * 'e) -> ''a list
8.49 - val filter_vat : O_Model.T -> int -> O_Model.T
8.50 - val show_metguhs : unit -> unit
8.51 - val sort_metguhs : unit -> unit
8.52 end
8.53
8.54 (**)
8.55 @@ -95,34 +76,6 @@
8.56 (*either ThyC.id or Problem.id or Method.id*)
8.57 type kestoreID = string list;
8.58
8.59 -fun fun_id_of ({scr = prog, ...} : Method.T) =
8.60 - case prog of
8.61 - Rule.Empty_Prog => NONE
8.62 - | Rule.Prog t =>
8.63 - (case t of
8.64 - Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
8.65 - | _ => SOME (Program.get_fun_id t))
8.66 - | Rule.Rfuns _ => NONE
8.67 -
8.68 -(* get all data from a Ptyp tree *)
8.69 -fun get_data ptyp =
8.70 -let
8.71 - fun scan [] = []
8.72 - | scan ((Store.Node ((_, data, []))) :: []) = data
8.73 - | scan ((Store.Node ((_, data, pl))) :: []) = data @ scan pl
8.74 - | scan ((Store.Node ((_, data, []))) :: ps) = data @ scan ps
8.75 - | scan ((Store.Node ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
8.76 -in scan ptyp end
8.77 -
8.78 -fun get_fun_ids thy =
8.79 - let
8.80 - val mets = get_data (KEStore_Elems.get_mets thy)
8.81 - (* all mets of the respective theory PLUS of all ancestor theories*)
8.82 - val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
8.83 - in
8.84 - filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
8.85 - end
8.86 -
8.87 (* split a term into description and (id | structured variable) for pbt, met.ppc *)
8.88 fun split_did t =
8.89 let
8.90 @@ -140,9 +93,6 @@
8.91 | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
8.92 | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
8.93
8.94 -val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Pattern_Def.T
8.95 -val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
8.96 -
8.97 (* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)
8.98 fun guh2kestoreID guh =
8.99 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
8.100 @@ -262,77 +212,6 @@
8.101 crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
8.102 end;
8.103
8.104 -
8.105 -(** get pblIDs of all entries in mat3D **)
8.106 -
8.107 -fun format_pblID strl = enclose " [" "]" (commas_quote strl);
8.108 -fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
8.109 -
8.110 -fun scan _ [] = [] (* no base case, for empty doms only *)
8.111 - | scan id ((Store.Node ((i, _, []))) :: []) = [id @ [i]]
8.112 - | scan id ((Store.Node ((i, _, pl))) :: []) = scan (id @ [i]) pl
8.113 - | scan id ((Store.Node ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
8.114 - | scan id ((Store.Node ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
8.115 -
8.116 -fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ()); (* for tests *)
8.117 -fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)
8.118 -
8.119 -(* transform oris *)
8.120 -
8.121 -fun coll_vats (vats, (_, vs, _, _, _)) = union op = vats vs;
8.122 -fun filter_vat oris i = filter ((member_swap op = i) o (#2 : O_Model.single -> int list)) oris;
8.123 -
8.124 -
8.125 -(** check a problem (ie. itm list) for matching a problemtype **)
8.126 -
8.127 -(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
8.128 - for missing items get data from formalization (ie. ori list);
8.129 - takes the I_Model.vars_of for concluding completeness (could be another!)
8.130 -
8.131 - (0) determine the most frequent variant mv in pbl
8.132 - ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
8.133 - (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
8.134 - (3) newitms = filter (mv mem vat(news)) news
8.135 - (4) pbt @ newitms *)
8.136 -fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
8.137 - let
8.138 - (*0*)val mv = I_Model.max_vt pbl;
8.139 -
8.140 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
8.141 - fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
8.142 - SOME _ => false | NONE => true;
8.143 - (*1*)val mis = (filter (notmem pbl)) pbt;
8.144 -
8.145 - fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
8.146 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
8.147 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
8.148 - val news = (flat o (map (oris2itms oris))) mis;
8.149 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
8.150 - val newitms = filter mem_vat news;
8.151 - (*4*)val itms' = pbl @ newitms;
8.152 - val pre' = Pre_Conds.check prls pre itms' mv;
8.153 - val pb = foldl and_ (true, map fst pre');
8.154 - in (length mis = 0 andalso pb, (itms', pre')) end;
8.155 -
8.156 -
8.157 -(** check a problem (ie. itm list) for matching a problemtype **)
8.158 -
8.159 -datatype match' = (* for the user *)
8.160 - Matches' of P_Model.T
8.161 -| NoMatch' of P_Model.T;
8.162 -
8.163 -(* match a formalization with a problem type, for tests *)
8.164 -fun match_pbl fmz {thy = thy, where_ = pre, ppc, prls = er, ...} =
8.165 - let
8.166 - val oris = O_Model.init fmz thy ppc(* |> #1*);
8.167 - val (bool, (itms, pre')) = Model.match_oris' thy oris (ppc, pre, er);
8.168 - in
8.169 - if bool
8.170 - then Matches' (P_Model.from thy itms pre')
8.171 - else NoMatch' (P_Model.from thy itms pre')
8.172 - end;
8.173 -
8.174 -(*/------- from Celem to Specify -------\*)
8.175 (* for distinction of contexts WN130621: disambiguate with Isabelle's Context *)
8.176 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
8.177 fun ketype2str Exp_ = "Exp_"
8.178 @@ -349,7 +228,7 @@
8.179 | str2ketype' "pbl" = Pbl_
8.180 | str2ketype' "met" = Met_
8.181 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
8.182 -(*\------- from Celem to Specify -------/*)
8.183 +
8.184 (* make a guh from a reference to an element in the kestore;
8.185 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
8.186 fun pblID2guh pblID = (((#guh o Problem.from_store) pblID)
8.187 @@ -361,20 +240,4 @@
8.188 | kestoreID2guh ketype kestoreID =
8.189 raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
8.190
8.191 -fun show_pblguhs () = (* for tests *)
8.192 - (tracing o strs2str o (map linefeed))
8.193 - (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id) (get_ptyps ()))
8.194 -fun sort_pblguhs () = (* for tests *)
8.195 - (tracing o strs2str o (map linefeed))
8.196 - (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)))
8.197 - (get_ptyps ()))
8.198 -
8.199 -fun show_metguhs () = (* for tests *)
8.200 - (tracing o strs2str o (map linefeed))
8.201 - (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id) (get_mets ()))
8.202 -fun sort_metguhs () = (* for tests *)
8.203 - (tracing o strs2str o (map linefeed))
8.204 - (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)))
8.205 - (get_mets ()))
8.206 -
8.207 (**)end(**)
9.1 --- a/src/Tools/isac/Specify/specify-step.sml Tue May 12 17:42:29 2020 +0200
9.2 +++ b/src/Tools/isac/Specify/specify-step.sml Wed May 13 11:34:05 2020 +0200
9.3 @@ -79,7 +79,7 @@
9.4 val {ppc, where_, prls, ...} = Problem.from_store pID;
9.5 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
9.6 then (false, (I_Model.init ppc, []))
9.7 - else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
9.8 + else Model.match_itms_oris thy itms (ppc, where_, prls) oris;
9.9 in
9.10 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
9.11 end
10.1 --- a/src/Tools/isac/Specify/step-specify.sml Tue May 12 17:42:29 2020 +0200
10.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed May 13 11:34:05 2020 +0200
10.3 @@ -97,7 +97,7 @@
10.4 val pbl =
10.5 if pI' = Problem.id_empty andalso pI = Problem.id_empty
10.6 then (false, (I_Model.init ppc, []))
10.7 - else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
10.8 + else Model.match_itms_oris thy probl (ppc,where_,prls) oris
10.9 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
10.10 val (c, pt) =
10.11 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
10.12 @@ -118,7 +118,7 @@
10.13 val thy = ThyC.get_theory dI
10.14 val oris = O_Model.add thy ppc oris
10.15 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
10.16 - val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
10.17 + val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris
10.18 val itms = Specify.hack_until_review_Specify_2 mID itms
10.19 val (pos, c, _, pt) =
10.20 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
10.21 @@ -214,7 +214,7 @@
10.22 val thy = ThyC.get_theory dI
10.23 val oris = O_Model.add thy ppc oris
10.24 val met = if met = [] then pbl else met
10.25 - val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
10.26 + val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris
10.27 val itms = Specify.hack_until_review_Specify_1 mI' itms
10.28 val (pos, _, _, pt) =
10.29 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
11.1 --- a/src/Tools/isac/Test_Code/Test_Code.thy Tue May 12 17:42:29 2020 +0200
11.2 +++ b/src/Tools/isac/Test_Code/Test_Code.thy Wed May 13 11:34:05 2020 +0200
11.3 @@ -10,6 +10,7 @@
11.4 begin
11.5
11.6 ML_file "test-code.sml"
11.7 + ML_file "test-tool.sml"
11.8
11.9 ML \<open>
11.10 \<close> ML \<open>
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/Test_Code/test-tool.sml Wed May 13 11:34:05 2020 +0200
12.3 @@ -0,0 +1,50 @@
12.4 +(* Title: Test_Code/test-tool.sml
12.5 + Author: Walther Neuper 110226
12.6 + (c) due to copyright terms
12.7 +*)
12.8 +signature TEST_TOOL =
12.9 +sig
12.10 + val show_ptyps : unit -> unit
12.11 + val show_mets : unit -> unit
12.12 +
12.13 + val show_pblguhs : unit -> unit
12.14 + val sort_pblguhs : unit -> unit
12.15 + val show_metguhs : unit -> unit
12.16 + val sort_metguhs : unit -> unit
12.17 +
12.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.19 + (*NONE*)
12.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.21 + (*NONE*)
12.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.23 +
12.24 +end
12.25 +
12.26 +(**)
12.27 +structure Test_Tool(**) : TEST_TOOL(**) =
12.28 +struct
12.29 +(**)
12.30 +
12.31 +fun format_pblID strl = enclose " [" "]" (commas_quote strl);
12.32 +fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
12.33 +
12.34 +fun show_ptyps () = (writeln o format_pblIDl o (Store.scan [])) (get_ptyps ()); (* for tests *)
12.35 +fun show_mets () = (writeln o format_pblIDl o (Store.scan [])) (get_mets ()); (* for tests *)
12.36 +
12.37 +fun show_pblguhs () =
12.38 + (tracing o strs2str o (map linefeed))
12.39 + (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id) (get_ptyps ()))
12.40 +fun sort_pblguhs () =
12.41 + (tracing o strs2str o (map linefeed))
12.42 + (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)))
12.43 + (get_ptyps ()))
12.44 +
12.45 +fun show_metguhs () =
12.46 + (tracing o strs2str o (map linefeed))
12.47 + (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id) (get_mets ()))
12.48 +fun sort_metguhs () =
12.49 + (tracing o strs2str o (map linefeed))
12.50 + (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)))
12.51 + (get_mets ()))
12.52 +
12.53 +end
13.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue May 12 17:42:29 2020 +0200
13.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed May 13 11:34:05 2020 +0200
13.3 @@ -266,7 +266,7 @@
13.4 text \<open>\noindent Check if the given equation matches the specification of this
13.5 equation type.\<close>
13.6 ML \<open>
13.7 - Specify.match_pbl fmz (Problem.from_store ["univariate","equation"]);
13.8 + Model.match_pbl fmz (Problem.from_store ["univariate","equation"]);
13.9 \<close>
13.10
13.11 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
13.12 @@ -290,7 +290,7 @@
13.13 specification of this equation type.\<close>
13.14
13.15 ML \<open>
13.16 - Specify.match_pbl fmz (Problem.from_store
13.17 + Model.match_pbl fmz (Problem.from_store
13.18 ["abcFormula","degree_2","polynomial","univariate","equation"]);
13.19 \<close>
13.20
13.21 @@ -900,7 +900,7 @@
13.22 NONE,
13.23 [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
13.24 ML \<open>
13.25 - Specify.show_ptyps() ();
13.26 + Test_Tool.show_ptyps() ();
13.27 Problem.from_store ["Inverse","Z_Transform","SignalProcessing"];
13.28 \<close>
13.29
14.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Tue May 12 17:42:29 2020 +0200
14.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Wed May 13 11:34:05 2020 +0200
14.3 @@ -29,7 +29,7 @@
14.4 ad (2) The problem of 'vereinfachen' is one of many other problems;
14.5 the function 'get_pbt' gets the one we need:
14.6 \<close>
14.7 -ML \<open>Specify.show_ptyps ();
14.8 +ML \<open>Test_Tool.show_ptyps ();
14.9 Problem.from_store ["plus_minus", "polynom", "vereinfachen"];
14.10 \<close>
14.11 text \<open>However, 'get_pbt' shows an internal format; for a human readable format
15.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue May 12 17:42:29 2020 +0200
15.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed May 13 11:34:05 2020 +0200
15.3 @@ -134,7 +134,7 @@
15.4 path ^ Thy_Present.guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
15.5 "~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
15.6 (id, pbl);
15.7 -"~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id);
15.8 +"~~~~~ fun pbl2term, args:"; val (thy, (pblRD:Problem.id)) = (thy, id);
15.9 if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
15.10 "Problem (Pure', [empty_probl_id])"
15.11 then () else error "fun pbl2term changed";
16.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 12 17:42:29 2020 +0200
16.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed May 13 11:34:05 2020 +0200
16.3 @@ -988,7 +988,7 @@
16.4
16.5 val env = [(str2term "v_v", str2term "x")];
16.6 val errpats =
16.7 - [e_errpat, (*generalised for testing*)
16.8 + [Error_Pattern.empty, (*generalised for testing*)
16.9 ("chain-rule-diff-both",
16.10 [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
16.11 parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
17.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue May 12 17:42:29 2020 +0200
17.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed May 13 11:34:05 2020 +0200
17.3 @@ -283,7 +283,7 @@
17.4
17.5 (*WN120313 in "solution L" above "Refine.refine fmz ["LINEAR","system"]" caused an error...*)
17.6 "~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]);
17.7 -"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
17.8 +"~~~~~ fun refin', args:"; val ((pblRD: Problem.id), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
17.9 ((rev o tl) pblID, fmz, [(*match list*)],
17.10 ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR","system"]], [])): Problem.T Store.node));
17.11 val {thy, ppc, where_, prls, ...} = py ;
17.12 @@ -427,8 +427,8 @@
17.13 (*default_print_depth 11;*) matches; (*default_print_depth 3;*)
17.14 (*brought: 'False "length_ es_ = 2"'*)
17.15
17.16 -(*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
17.17 -(* val ((pblRD:pblRD), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
17.18 +(*-----fun refin' (pblRD:Problem.id) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
17.19 +(* val ((pblRD:Problem.id), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
17.20 (rev ["LINEAR","system"], fmz, [(*match list*)],
17.21 ((Store.Node ("2x2",[Problem.from_store ["2x2","LINEAR","system"]],[])):pbt Store.store));
17.22 *)
18.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue May 12 17:42:29 2020 +0200
18.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed May 13 11:34:05 2020 +0200
18.3 @@ -361,7 +361,7 @@
18.4 if F1_type = F3_type then ()
18.5 else error "integrate.sml: unequal types in find's";
18.6
18.7 -show_ptyps();
18.8 +Test_Tool.show_ptyps();
18.9 val pbl = Problem.from_store ["integrate","function"];
18.10 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
18.11 | _ => error "integrate.sml: Integrate.Integrate ???";
19.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue May 12 17:42:29 2020 +0200
19.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed May 13 11:34:05 2020 +0200
19.3 @@ -574,12 +574,12 @@
19.4 val pbt = Problem.from_store ["polynomial","simplification"];
19.5 (*default_print_depth 3;*)
19.6 (*if there is ...
19.7 -> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
19.8 +> val Model.NoMatch' {Given=gi, Where=wh, Find=fi,...} = Model.match_pbl fmz pbt;
19.9 ... then Rewrite.trace_on:*)
19.10
19.11 "-----2 ---";
19.12 Rewrite.trace_on := false;
19.13 -match_pbl fmz pbt;
19.14 +Model.match_pbl fmz pbt;
19.15 Rewrite.trace_on := false;
19.16 (*... if there is no rewrite, then there is something wrong with prls*)
19.17
19.18 @@ -596,10 +596,10 @@
19.19 "-----4 ---";
19.20 (*show_types:=true;*)
19.21 (*
19.22 -> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
19.23 +> val Model.NoMatch' {Given=gi, Where=wh, Find=fi,...} = Model.match_pbl fmz pbt;
19.24 val wh = [False "(t_::real => real) (is_polyexp::real)"]
19.25 ......................^^^^^^^^^^^^...............^^^^*)
19.26 -val Matches' _ = match_pbl fmz pbt;
19.27 +val Model.Matches' _ = Model.match_pbl fmz pbt;
19.28 (*show_types:=false;*)
19.29
19.30
20.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue May 12 17:42:29 2020 +0200
20.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed May 13 11:34:05 2020 +0200
20.3 @@ -109,22 +109,22 @@
20.4 "----------- test matching problems --------------------------0---";
20.5 "----------- test matching problems --------------------------0---";
20.6 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
20.7 -if match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) =
20.8 - Matches' {Find = [Correct "solutions L"],
20.9 +if Model.match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) =
20.10 + Model.Matches' {Find = [Correct "solutions L"],
20.11 With = [],
20.12 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
20.13 Where = [Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
20.14 Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],
20.15 Relate = []}
20.16 -then () else error "match_pbl [expanded,univariate,equation]";
20.17 +then () else error "Model.match_pbl [expanded,univariate,equation]";
20.18
20.19 -if match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) =
20.20 - Matches' {Find = [Correct "solutions L"],
20.21 +if Model.match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) =
20.22 + Model.Matches' {Find = [Correct "solutions L"],
20.23 With = [],
20.24 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
20.25 Where = [Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x = 2"],
20.26 Relate = []} (*before WN110906 was: has_degree_in x =!= 2"]*)
20.27 -then () else error "match_pbl [degree_2,expanded,univariate,equation]";
20.28 +then () else error "Model.match_pbl [degree_2,expanded,univariate,equation]";
20.29
20.30
20.31 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
21.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue May 12 17:42:29 2020 +0200
21.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed May 13 11:34:05 2020 +0200
21.3 @@ -40,13 +40,13 @@
21.4 val result = UnparseC.term t_;
21.5 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
21.6
21.7 -val result = match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
21.8 +val result = Model.match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
21.9 (Problem.from_store ["rational","univariate","equation"]);
21.10 -case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
21.11 +case result of Model.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
21.12
21.13 -val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
21.14 +val result = Model.match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
21.15 (Problem.from_store ["rational","univariate","equation"]);
21.16 -case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
21.17 +case result of Model.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
21.18
21.19 "------------ solve (1/x = 5, x) by me ---------------------------";
21.20 "------------ solve (1/x = 5, x) by me ---------------------------";
22.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Tue May 12 17:42:29 2020 +0200
22.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed May 13 11:34:05 2020 +0200
22.3 @@ -84,13 +84,13 @@
22.4
22.5
22.6
22.7 -val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
22.8 +val result = Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
22.9 (Problem.from_store ["rootX","univariate","equation"]);
22.10 -case result of Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
22.11 +case result of Model.Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
22.12
22.13 -val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
22.14 +val result = Model.match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
22.15 (Problem.from_store ["rootX","univariate","equation"]);
22.16 -case result of NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
22.17 +case result of Model.NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
22.18
22.19 (*---------rooteq---- 23.8.02 ---------------------*)
22.20 "---------(1/sqrt(x)=5)---------------------";
22.21 @@ -778,6 +778,6 @@
22.22
22.23
22.24 Refine.refine fmz ["univariate","equation","test"];
22.25 -match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]);
22.26 +Model.match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]);
22.27
22.28 ===== copied here from OLDTESTS in case there is a Program ===^^^=============================*)
23.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Tue May 12 17:42:29 2020 +0200
23.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Wed May 13 11:34:05 2020 +0200
23.3 @@ -65,7 +65,7 @@
23.4 [("Test","methode")])]
23.5 thy;
23.6
23.7 -match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);
23.8 +Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);
23.9
23.10 KEStore_Elems.add_pbts
23.11 [prep_pbt (theory "Isac_Knowledge")
24.1 --- a/test/Tools/isac/Specify/ptyps.sml Tue May 12 17:42:29 2020 +0200
24.2 +++ b/test/Tools/isac/Specify/ptyps.sml Wed May 13 11:34:05 2020 +0200
24.3 @@ -45,8 +45,8 @@
24.4
24.5 ((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id))) (get_ptyps ());
24.6 sort string_ord (((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id))) (get_ptyps ()));
24.7 -show_pblguhs ();
24.8 -sort_pblguhs ();
24.9 +Test_Tool.show_pblguhs ();
24.10 +Test_Tool.sort_pblguhs ();
24.11
24.12 "----------- fun guh2kestoreID -----------------------------------";
24.13 "----------- fun guh2kestoreID -----------------------------------";
24.14 @@ -138,7 +138,7 @@
24.15 "solveFor x","errorBound (eps=0)","solutions L"];
24.16 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
24.17 Problem.from_store ["univariate","equation"];
24.18 -match_pbl fmz pbt;
24.19 +Model.match_pbl fmz pbt;
24.20 *)
24.21 "----------- fun match_oris --------------------------------------";
24.22 "----------- fun match_oris --------------------------------------";
25.1 --- a/test/Tools/isac/Specify/refine.sml Tue May 12 17:42:29 2020 +0200
25.2 +++ b/test/Tools/isac/Specify/refine.sml Wed May 13 11:34:05 2020 +0200
25.3 @@ -20,7 +20,7 @@
25.4 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
25.5 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
25.6 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
25.7 -Specify.show_ptyps();
25.8 +Test_Tool.show_ptyps();
25.9 val thy = @{theory "Isac_Knowledge"};
25.10 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
25.11
26.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 12 17:42:29 2020 +0200
26.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 13 11:34:05 2020 +0200
26.3 @@ -112,7 +112,7 @@
26.4 open Prog_Expr;
26.5 open Auto_Prog; rule2stac;
26.6 open Input_Descript;
26.7 - open Specify; show_ptyps;
26.8 + open Specify;
26.9 open SpecifyNEW;
26.10 open Step_Specify;
26.11 open Step_Solve;
27.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue May 12 17:42:29 2020 +0200
27.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed May 13 11:34:05 2020 +0200
27.3 @@ -112,7 +112,7 @@
27.4 open Prog_Expr;
27.5 open Auto_Prog; rule2stac;
27.6 open Input_Descript;
27.7 - open Specify; show_ptyps;
27.8 + open Specify;
27.9 open SpecifyNEW;
27.10 open Step_Specify;
27.11 open Step_Solve;
28.1 --- a/test/Tools/isac/Test_Some.thy Tue May 12 17:42:29 2020 +0200
28.2 +++ b/test/Tools/isac/Test_Some.thy Wed May 13 11:34:05 2020 +0200
28.3 @@ -29,7 +29,7 @@
28.4 open Prog_Expr;
28.5 open Auto_Prog; rule2stac;
28.6 open Input_Descript;
28.7 - open Specify; show_ptyps;
28.8 + open Specify;
28.9 open SpecifyNEW;
28.10 open Step_Specify;
28.11 open Step_Solve;
29.1 --- a/test/Tools/isac/Test_Some_meld.thy Tue May 12 17:42:29 2020 +0200
29.2 +++ b/test/Tools/isac/Test_Some_meld.thy Wed May 13 11:34:05 2020 +0200
29.3 @@ -22,7 +22,7 @@
29.4 open Prog_Expr;
29.5 open Auto_Prog; rule2stac;
29.6 open Input_Descript;
29.7 - open Specify; show_ptyps;
29.8 + open Specify;
29.9 open ApplicableOLD; mk_set;
29.10 open Solve; (* NONE *)
29.11 open Selem; Formalise.empty;