1.1 --- a/TODO.md Sun Dec 10 17:35:07 2023 +0100
1.2 +++ b/TODO.md Mon Dec 11 09:24:02 2023 +0100
1.3 @@ -46,12 +46,7 @@
1.4
1.5 * WN:
1.6 * WN: clarify handling "#undef" -> type m_field +++ bool in i_single
1.7 - ?RN?or?just for OLD? ori_2itm -> single_from_o, ori_2itm_POS -> single_from_o_POS
1.8 * WN: replace I_Model.feedb_values -> val get_values = Pre_Conds.get_values
1.9 -* WN: RN o_model_values -> get_values, feedb_values -> get_values_POS,
1.10 - TEST_to_OLD -> POS_to_OLD, TEST_to_OLD_single -> POS_to_OLD_single,
1.11 -
1.12 -* WN: eliminate max_variant in favour of max_variants
1.13 * WN: replace I_Model.descriptor with fun descr_exists: descriptor -> feedback -> bool
1.14 * WN: review Model_Def.is_list_descr, replace by Term.is_list. Exception: make_values
1.15 (values determine handling_lists by [[..], [..], ..])
2.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Sun Dec 10 17:35:07 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Mon Dec 11 09:24:02 2023 +0100
2.3 @@ -30,6 +30,7 @@
2.4 datatype for = Problem | Method | Undef
2.5
2.6 val adapt_to_type: Proof.context -> single -> single
2.7 +
2.8 (*from isac_test for Minisubpbl*)
2.9 val split_descriptor: Proof.context -> m_field * term * Position.T ->
2.10 (m_field * (term * term) * Position.T)
3.1 --- a/src/Tools/isac/Specify/cas-command.sml Sun Dec 10 17:35:07 2023 +0100
3.2 +++ b/src/Tools/isac/Specify/cas-command.sml Mon Dec 11 09:24:02 2023 +0100
3.3 @@ -1,6 +1,5 @@
3.4 -(* Title: Interpret/lucas-interpreter.sml
3.5 +(* Title: Interpret/cas-command.sml
3.6 Author: Walther Neuper 2019
3.7 - (c) due to copyright terms
3.8 *)
3.9
3.10 signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
3.11 @@ -14,7 +13,7 @@
3.12 val input_: References.T -> (term * term list) list ->
3.13 Problem.id * I_Model.T_POS * MethodC.id * I_Model.T_POS * Pre_Conds.T * Proof.context
3.14 val dtss2itm_: Model_Pattern.T -> term * term list ->
3.15 - int list * bool * string * I_Model.feedback (*I_Model.single'*)
3.16 + int list * bool * Model_Def.m_field * (I_Model.feedback_POS * Position.T)
3.17 val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
3.18 (*\----- from isac_test for Minisubpbl*)
3.19
3.20 @@ -37,7 +36,7 @@
3.21 (#1: (term * term) -> term) o
3.22 (#2: Model_Pattern.single -> (term * term))) model)
3.23 in
3.24 - ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
3.25 + ([1], true, f, (I_Model.Cor_POS (d, ts), Position.none))
3.26 end
3.27
3.28 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
3.29 @@ -57,16 +56,16 @@
3.30 if mI <> ["no_met"]
3.31 then (pI, mI)
3.32 else
3.33 - case Refine.problem thy pI (I_Model.OLD_to_POS pits) of
3.34 + case Refine.problem thy pI pits of
3.35 SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
3.36 | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
3.37 val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI
3.38 val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
3.39 val its = O_Model.add_enumerate its_
3.40 val mits = map flattup2 its
3.41 - val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_POS mits)
3.42 + val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, mits)
3.43 val ctxt = Proof_Context.init_global thy
3.44 - in (pI, I_Model.OLD_to_POS pits, mI, I_Model.OLD_to_POS mits, where_, ctxt) end;
3.45 + in (pI, pits, mI, mits, where_, ctxt) end;
3.46
3.47 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
3.48 fun input hdt =
4.1 --- a/src/Tools/isac/Specify/i-model.sml Sun Dec 10 17:35:07 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Dec 11 09:24:02 2023 +0100
4.3 @@ -34,10 +34,7 @@
4.4 type env
4.5 type message
4.6
4.7 - val single_to_string: Proof.context -> single -> string
4.8 val single_to_string_POS: Proof.context -> single_POS -> string
4.9 - val single_to_string_POS': single_POS -> string
4.10 - val to_string: Proof.context -> T -> string
4.11 val to_string_POS: Proof.context -> T_POS -> string
4.12
4.13 val feedback_OLD_to_POS: feedback -> feedback_POS
4.14 @@ -48,24 +45,20 @@
4.15 datatype add_single = Add of single_POS | Err of string
4.16 val init: Model_Pattern.T -> T
4.17 val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
4.18 - val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
4.19 + val check_single: Proof.context -> m_field -> O_Model.T -> T_POS -> Model_Pattern.T ->
4.20 TermC.as_string -> add_single
4.21 val add_single: theory -> single_POS -> T_POS -> T_POS
4.22
4.23 val make_tactic: m_field -> TermC.as_string * T_POS -> Tactic.T
4.24
4.25 - val descriptor: feedback -> descriptor
4.26 val descriptor_POS: feedback_POS -> descriptor
4.27 - val values: feedback -> values option
4.28 val get_values: T_POS -> values list
4.29 - val o_model_values: feedback -> values
4.30 val feedb_values: feedback_POS -> values
4.31 val order_by_patt: Model_Pattern.T -> T_POS ->T_POS
4.32 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
4.33 val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
4.34 val is_notyet_input: Proof.context -> T_POS -> O_Model.values -> O_Model.single ->
4.35 Model_Pattern.T -> message * single_POS
4.36 - val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
4.37
4.38 val fill_from_o: O_Model.T -> single_POS -> single_POS option
4.39
4.40 @@ -82,12 +75,11 @@
4.41 val msg: variants -> feedback_POS -> string
4.42 val transfer_terms: O_Model.single -> single_POS
4.43
4.44 - val feedback_to_string: Proof.context -> feedback -> string
4.45 val feedback_POS_to_string: Proof.context -> feedback_POS -> string
4.46 val descr_vals_to_string: Proof.context -> descriptor * values -> string
4.47 val feedb_args_to_string: Proof.context -> feedback_POS -> string
4.48
4.49 - val ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> single_POS
4.50 + val single_from_o: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> single_POS
4.51 val seek_ppc: int -> single_POS list -> single_POS option
4.52 val overwrite_ppc: theory -> single_POS -> T_POS -> T_POS
4.53 (*\----- from isac_test for Minisubpbl*)
4.54 @@ -155,19 +147,6 @@
4.55 fun TEST_to_OLD i_model = map TEST_to_OLD_single i_model
4.56
4.57 type message = string;
4.58 -
4.59 -fun feedback_to_string ctxt (Cor ((d, ts), _)) =
4.60 - "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
4.61 - | feedback_to_string _ (Syn c) = "Syn " ^ c
4.62 - | feedback_to_string _ (Typ c) = "Typ " ^ c
4.63 - | feedback_to_string ctxt (Inc ((d, ts), _)) =
4.64 - "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
4.65 - | feedback_to_string ctxt (Sup (d, ts)) =
4.66 - "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
4.67 - | feedback_to_string ctxt (Mis (d, pid)) =
4.68 - "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
4.69 - | feedback_to_string _ (Par s) = "Trm "^s;
4.70 -
4.71 fun feedback_POS_to_string ctxt (Cor_POS (d, ts)) =
4.72 "Cor_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
4.73 | feedback_POS_to_string _ (Syn_POS c) =
4.74 @@ -194,17 +173,9 @@
4.75 | feedb_args_to_string ctxt (Sup_POS (descr, values)) =
4.76 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
4.77
4.78 -fun single_to_string ctxt (i, is, b, s, itm_) =
4.79 - "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
4.80 - s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
4.81 fun single_to_string_POS ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
4.82 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
4.83 s ^ ", (" ^ feedback_POS_to_string ctxt itm_ ^ ", Position.T))";
4.84 -fun single_to_string_POS' (i, is, b, s, (itm_, _(*Position.T*))) =
4.85 - "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
4.86 - s ^ ", (" ^ feedback_POS_to_string (ContextC.for_ERROR ()) itm_ ^ ", Position.T))";
4.87 -
4.88 -fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
4.89 fun to_string_POS ctxt itms = strs2str' (map (linefeed o (single_to_string_POS ctxt)) itms);
4.90
4.91
4.92 @@ -249,34 +220,10 @@
4.93
4.94 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
4.95 (*DANGEROUS: do NOT use "UnIqE_tErM" *)
4.96 -fun descriptor (Cor ((d ,_), _)) = d
4.97 - | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
4.98 - | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
4.99 - | descriptor (Inc ((d, _), _)) = d
4.100 - | descriptor (Sup (d, _)) = d
4.101 - | descriptor (Mis (d, _)) = d
4.102 - | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
4.103 -(*DANGEROUS: do NOT use "UnIqE_tErM" *)
4.104 fun descriptor_POS (Cor_POS (d ,_)) = d
4.105 | descriptor_POS (Syn_POS _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
4.106 | descriptor_POS (Inc_POS (d, _)) = d
4.107 | descriptor_POS (Sup_POS (d, _)) = d
4.108 -
4.109 -fun values (Cor ((_ , ts), _)) = SOME ts
4.110 - | values (Syn _) = NONE
4.111 - | values (Typ _) = NONE
4.112 - | values (Inc ((_, ts), _)) = SOME ts
4.113 - | values (Sup (_, ts)) = SOME ts
4.114 - | values (Mis (_, t)) = SOME [t]
4.115 - | values _ = raise ERROR "descriptor: uncovered case in fun.def.";
4.116 -fun o_model_values (Cor ((_, ts), _)) = ts
4.117 - | o_model_values (Syn _) = []
4.118 - | o_model_values (Typ _) = []
4.119 - | o_model_values (Inc ((_, ts), _)) = ts
4.120 - | o_model_values (Sup (_, ts)) = ts
4.121 - | o_model_values (Mis _) = []
4.122 - | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
4.123 -(*RN feedb_vals'*)
4.124 fun feedb_values (Cor_POS (_, ts)) = ts
4.125 | feedb_values (Syn_POS _) = raise ERROR "feedb_values NOT for Syn_POS"
4.126 | feedb_values (Inc_POS (_, ts)) = ts
4.127 @@ -308,17 +255,8 @@
4.128 Pre_Conds.environment_POS model_patt i_model
4.129 |> map snd
4.130
4.131 -(*
4.132 -val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
4.133 -*)
4.134 -(* get a term from O_Model, notyet input in I_Model.
4.135 - the term from O_Model is thrown back to a string in order to reuse
4.136 - machinery for immediate input by the user. *)
4.137 -fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
4.138 - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
4.139 -
4.140 (*update the itm_ already input, all..from ori*)
4.141 -fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) =
4.142 +fun single_from_o (feedb:feedback_POS) _ all (id, vt, fd, d, ts) =
4.143 let
4.144 val ts' = union op = (feedb_values feedb) ts;
4.145 val complete = if eq_set op = (ts', all) then true else false
4.146 @@ -332,7 +270,7 @@
4.147 else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))
4.148 | Sup_POS (d, ts') =>
4.149 (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
4.150 - | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
4.151 + | i => raise ERROR ("single_from_o: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
4.152 end
4.153
4.154
4.155 @@ -350,10 +288,10 @@
4.156 in
4.157 if subset op = (ts, ts')
4.158 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
4.159 - else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))
4.160 + else ("", single_from_o feedb pid all (i, v, f, d, subtract op = ts' ts))
4.161 end
4.162 - | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
4.163 - | NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
4.164 + | NONE => ("", single_from_o (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
4.165 + | NONE => ("", single_from_o (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
4.166
4.167 datatype add_single =
4.168 Add of single_POS (* return-value of check_single *)
4.169 @@ -381,13 +319,13 @@
4.170 (case find_first (fn (_, (d', _)) => d = d') m_patt of
4.171 NONE => Add (i, [], true, m_field, (Sup_POS (d,ts), Position.none))
4.172 | SOME (f, (_, id)) =>
4.173 - case find_first (fn (i, _, _, _, feedb) => d = (descriptor feedb) andalso i <> 0) i_model of
4.174 + case find_first (fn (i, _, _, _, (feedb, _)) => d = (descriptor_POS feedb) andalso i <> 0) i_model of
4.175 NONE =>
4.176 Add (i, [], true, f, (Cor_POS (d, ts), Position.none))
4.177 - | SOME (i', _, _, _, itm_) =>
4.178 + | SOME (i', _, _, _, (itm_, _)) =>
4.179 if Input_Descript.for_list d then
4.180 let
4.181 - val in_itm = o_model_values itm_
4.182 + val in_itm = feedb_values itm_
4.183 val ts' = union op = ts in_itm
4.184 val i'' = if in_itm = [] then i else i'
4.185 in Add (i'', [], true, f, (Cor_POS (d, ts'), Position.none)) end
4.186 @@ -410,7 +348,7 @@
4.187 else
4.188 case O_Model.contains ctxt m_field o_model t of
4.189 ("", ori', all) =>
4.190 - (case is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt of
4.191 + (case is_notyet_input ctxt i_model all ori' m_patt of
4.192 ("", itm) => Add itm
4.193 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
4.194 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
5.1 --- a/src/Tools/isac/Specify/o-model.sml Sun Dec 10 17:35:07 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon Dec 11 09:24:02 2023 +0100
5.3 @@ -48,8 +48,6 @@
5.4 val is_copy_named': string -> bool
5.5 val is_copy_named_generating: Model_Pattern.single -> bool
5.6
5.7 - val get_field_term: theory -> single -> m_field * UnparseC.term_as_string
5.8 -
5.9 \<^isac_test>\<open>
5.10 val is_copy_named_generating_idstr: string -> bool
5.11 val string_of_preoris : preori list -> string
5.12 @@ -97,10 +95,6 @@
5.13 val string_of_preoris = (strs2str' o (map (linefeed o preori2str)));
5.14 \<close>
5.15
5.16 -(* get the first term in ts from ori *)
5.17 -fun get_field_term thy (_, _, fd, d, ts) =
5.18 - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
5.19 -
5.20
5.21 (** initialise O_Model **)
5.22
6.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Sun Dec 10 17:35:07 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Mon Dec 11 09:24:02 2023 +0100
6.3 @@ -18,9 +18,7 @@
6.4 val to_string : Proof.context -> T -> string
6.5 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
6.6
6.7 - val max_variant: Model_Def.i_model -> Model_Def.variant
6.8 val environment_POS: Model_Pattern.T -> Model_Def.i_model_POS -> Env.T
6.9 -
6.10 val make_environments: Model_Pattern.T -> Model_Def.i_model_POS -> Env.T * (env_subst * env_eval)
6.11 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_POS) list ->
6.12 ((term * term) * (term * term)) list
6.13 @@ -117,26 +115,6 @@
6.14
6.15 (** find the maximal variant within an I_Model.T **)
6.16
6.17 -(* old code before I_Model.T_POS *)
6.18 -(*ATTENTION: misses variants with equal number of items, etc*)
6.19 -fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
6.20 -fun count_variants vts itms = map (cnt itms) vts;
6.21 -
6.22 -fun max_list [] = raise ERROR "max_list of []"
6.23 - | max_list (y :: ys) =
6.24 - let
6.25 - fun mx (a, x) [] = (a, x)
6.26 - | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
6.27 - in mx y ys end;
6.28 -
6.29 -(*find most frequent variant v in itms*)
6.30 -fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;
6.31 -(*find the variant with most items already input, without Pre_Conds (make_environments)*)
6.32 -(*T_POSold \<rightarrow> fun max_variants*)
6.33 -fun max_variant itms =
6.34 - let val vts = (count_variants (variants itms)) itms;
6.35 - in if vts = [] then 0 else (fst o max_list) vts end;
6.36 -
6.37 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
6.38 let
6.39 val equal_descr =
7.1 --- a/src/Tools/isac/Specify/specify.sml Sun Dec 10 17:35:07 2023 +0100
7.2 +++ b/src/Tools/isac/Specify/specify.sml Mon Dec 11 09:24:02 2023 +0100
7.3 @@ -153,7 +153,7 @@
7.4 (pbl,
7.5 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
7.6 in
7.7 - case I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct of
7.8 + case I_Model.check_single ctxt m_field oris i_model m_patt ct of
7.9 I_Model.Add i_single => (*..union old input *)
7.10 let
7.11 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
8.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sun Dec 10 17:35:07 2023 +0100
8.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Mon Dec 11 09:24:02 2023 +0100
8.3 @@ -720,25 +720,15 @@
8.4 val ((pt,_),_) = States.get_calc 1;
8.5 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
8.6 val (SOME istate, NONE) = loc;
8.7 -(*default_print_depth 5;*) writeln (Istate.string_of ctxt (fst istate)); (*default_print_depth 3;*)
8.8 -(*Pstate ([],
8.9 - [], NONE,
8.10 - ??.empty, Sundef, false)*)
8.11 -(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
8.12 -(*("Isac_Knowledge",
8.13 - ["derivative_of", "function"],
8.14 - ["diff", "differentiate_on_R"]) : spec*)
8.15 -writeln (I_Model.to_string ctxt probl);
8.16 -(*[
8.17 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
8.18 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
8.19 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
8.20 -writeln (I_Model.to_string ctxt meth);
8.21 -(*[
8.22 -(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
8.23 -(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
8.24 -(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
8.25 -writeln"-----------------------------------------------------------";
8.26 +
8.27 +val "Pstate ([], [], empty, NONE, \n??.empty, ORundef, false, false)"
8.28 + = fst istate |> Istate.string_of ctxt
8.29 +val ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) = spec;
8.30 +val "[\n(1, [1], true ,#Given, (Cor_POS functionTerm (x \<up> 2 + x + 1) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS differentiateFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS derivative f_'_f , pen2str, Position.T))]"
8.31 + = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
8.32 +val "[\n(1, [1], true ,#Given, (Cor_POS functionTerm (x \<up> 2 + x + 1) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS differentiateFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS derivative f_'_f , pen2str, Position.T))]"
8.33 + = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
8.34 +
8.35 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
8.36 autoCalculate 1 (Steps 1);
8.37 val ((pt,p),_) = States.get_calc 1;
9.1 --- a/test/Tools/isac/Knowledge/diff-app.sml Sun Dec 10 17:35:07 2023 +0100
9.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Mon Dec 11 09:24:02 2023 +0100
9.3 @@ -312,7 +312,7 @@
9.4 === inhibit exn 110722=============================================================*)
9.5
9.6 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string @{context} oris);
9.7 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
9.8 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS pits));
9.9
9.10 (*=== inhibit exn 110722=============================================================
9.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.12 @@ -382,11 +382,11 @@
9.13
9.14 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string @{context} oris);
9.15
9.16 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
9.17 -val pits = get_obj g_pbl pt [];writeln(I_Model.to_string ctxt pits);
9.18 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS pits));
9.19 +val pits = get_obj g_pbl pt [];writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS pits));
9.20
9.21 -val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string ctxt mits);
9.22 -val mits = get_obj g_met pt [];writeln(I_Model.to_string ctxt mits);
9.23 +val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS mits));
9.24 +val mits = get_obj g_met pt [];writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS mits));
9.25
9.26 (*=== inhibit exn 110722=============================================================
9.27 arguments_from_model ["Diff_App", "max_by_calculus"] mits;
9.28 @@ -438,7 +438,7 @@
9.29 fetchProposedTactic 1;
9.30 val ((pt,p),_) = States.get_calc 1;
9.31 val mits = get_obj g_met pt (fst p);
9.32 - writeln (I_Model.to_string ctxt mits);
9.33 + writeln (I_Model.to_string_POS ctxt (I_Model.OLD_to_POS mits));
9.34 (*
9.35 if I_Model.to_string ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then ()
9.36 else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
10.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml Sun Dec 10 17:35:07 2023 +0100
10.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Mon Dec 11 09:24:02 2023 +0100
10.3 @@ -63,13 +63,9 @@
10.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt
10.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.7 +
10.8 val PblObj {probl,...} = get_obj I pt [5];
10.9 - (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
10.10 -(*[
10.11 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
10.12 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
10.13 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
10.14 -*)
10.15 +
10.16 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
10.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
10.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
11.1 --- a/test/Tools/isac/MathEngine/step.sml Sun Dec 10 17:35:07 2023 +0100
11.2 +++ b/test/Tools/isac/MathEngine/step.sml Mon Dec 11 09:24:02 2023 +0100
11.3 @@ -303,12 +303,8 @@
11.4 (*** Problem model is complete ============================================================ ***)
11.5 val PblObj {probl, ...} = get_obj I (fst ptp) [];
11.6
11.7 -if I_Model.to_string @{context} probl = "[\n" ^
11.8 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^
11.9 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^
11.10 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^
11.11 - "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str)]"
11.12 -then () else error "I_Model.to_string probl CHANGED";
11.13 +val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
11.14 + = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
11.15
11.16 (*** Specification of References ========================================================== ***)
11.17 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
11.18 @@ -329,8 +325,8 @@
11.19
11.20 val PblObj {meth, ...} = get_obj I (fst ptp) [];
11.21
11.22 -(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n(6 ,[1] ,true ,#Given ,Cor boundVariable a , pen2str), \n(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) , pen2str)]"
11.23 - = meth |> I_Model.to_string @{context}
11.24 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(6, [1], true ,#Given, (Cor_POS boundVariable a , pen2str, Position.T)), \n(9, [1, 2], true ,#Given, (Cor_POS interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str, Position.T)), \n(11, [1, 2, 3], true ,#Given, (Cor_POS errorBound (eps = 0) , pen2str, Position.T))]"
11.25 + = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
11.26
11.27 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
11.28
12.1 --- a/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml Sun Dec 10 17:35:07 2023 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml Mon Dec 11 09:24:02 2023 +0100
12.3 @@ -369,8 +369,8 @@
12.4 (*if*) subset op = (ts, ts')
12.5
12.6 val return_is_notyet_input = ("",
12.7 - ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts));
12.8 -"~~~~~ fun ori_2itm , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) =
12.9 + single_from_o feedb pid all (i, v, f, d, subtract op = ts' ts));
12.10 +"~~~~~ fun single_from_o , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) =
12.11 (feedb, pid, all, (i, v, f, d, subtract op = ts' ts));
12.12 val ts' = union op = (feedb_values feedb) ts;
12.13 val pval = [Input_Descript.join'''' (d, ts')]
13.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Sun Dec 10 17:35:07 2023 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Dec 11 09:24:02 2023 +0100
13.3 @@ -104,7 +104,7 @@
13.4 (pbl,
13.5 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
13.6 val I_Model.Add i_single =
13.7 - (*case*) I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct;
13.8 + (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct;
13.9
13.10 (** )val i_model' =( **)
13.11 (**)val return_add_single =(**)
13.12 @@ -124,13 +124,13 @@
13.13 = i_model' |> I_Model.to_string_POS ctxt
13.14
13.15 val tac' = I_Model.make_tactic m_field (ct, i_model')
13.16 - val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
13.17 + val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
13.18 val return_by_Add_step =
13.19 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
13.20 [], (pt', pos)))
13.21 (*+++*)val {probl, ...} = Calc.specify_data (pt', pos);
13.22 -(*+++*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
13.23 - = probl |> I_Model.to_string ctxt
13.24 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
13.25 + = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
13.26 (*\\\\---------------- step into by_Add_ ---------------------------------------------------//*)
13.27 val return_by_tactic_step = return_by_Add_
13.28 (*\\\----------------- step into Step_Specify.by_tactic ------------------------------------//*)
13.29 @@ -141,8 +141,8 @@
13.30
13.31 (*+++*)val (pt, p) = ptp
13.32 (*+++*)val {probl, ...} = Calc.specify_data (pt, p);
13.33 -(*+++*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
13.34 - = probl |> I_Model.to_string ctxt;
13.35 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
13.36 + = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
13.37
13.38 val (pt, p) = ptp; (*case*)
13.39 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
13.40 @@ -171,8 +171,8 @@
13.41 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
13.42 spec = refs, ...} = Calc.specify_data (pt, pos);
13.43 val ctxt = Ctree.get_ctxt pt pos;
13.44 -(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
13.45 - = pbl|> I_Model.to_string ctxt
13.46 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
13.47 + = pbl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt(*+*)
13.48
13.49 val false =
13.50 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
13.51 @@ -752,7 +752,7 @@
13.52 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)
13.53 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
13.54
13.55 -(*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string ctxt
13.56 +(*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
13.57
13.58 val ctxt = Ctree.get_ctxt pt p
13.59 val (pt, p) =
13.60 @@ -772,8 +772,8 @@
13.61 (* M_Match.by_i_models*)
13.62 "~~~~~ fun by_i_models , args:"; val () = ();
13.63
13.64 -(*+isa*)val"[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
13.65 - = get_obj g_met pt (fst p) |> I_Model.to_string ctxt;
13.66 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
13.67 + = get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
13.68
13.69 (*case*)
13.70 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
13.71 @@ -804,8 +804,8 @@
13.72 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
13.73 (*if*) p_ = Pos.Pbl (*else*);
13.74
13.75 -(*+isa*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
13.76 - = met |> I_Model.to_string ctxt;
13.77 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
13.78 + = met |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
13.79
13.80 (**)val ("dummy", (Met, Add_Given "FunctionVariable a")) =(**)
13.81 Specify.for_method ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
14.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Sun Dec 10 17:35:07 2023 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Dec 11 09:24:02 2023 +0100
14.3 @@ -1,6 +1,6 @@
14.4 (* Title: "Minisubpbl/200-start-method-NEXT_STEP.sml"
14.5 Author: Walther Neuper 1105
14.6 - (c) copyright due to lincense terms.
14.7 + (c) copyright due to lincense terms.
14.8 *)
14.9
14.10 open Ctree;
14.11 @@ -67,35 +67,29 @@
14.12 val (_, (i_model, _)) =
14.13 M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob,
14.14 I_Model.OLD_to_POS i_prob) (m_patt, where_, where_rls);
14.15 -"~~~~~ fun by_i_models , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
14.16 - (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
14.17 - (*0*)val mv = Pre_Conds.max_variant pbl;
14.18 +"~~~~~ fun by_i_models , args:"; val (ctxt, o_model, (pbl_imod, met_imod), (met_patt, where_, where_rls)) =
14.19 + (ctxt, o_model, (I_Model.OLD_to_POS i_prob,(*<--? --v?*)
14.20 + I_Model.OLD_to_POS i_prob), (m_patt, where_, where_rls));
14.21 + val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt
14.22
14.23 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
14.24 - fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
14.25 - SOME _ => false | NONE => true;
14.26 - (*1*)val mis = (filter (notmem pbl)) pbt;
14.27 -
14.28 - fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
14.29 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
14.30 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
14.31 - val news = (flat o (map (oris2itms oris))) mis;
14.32 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
14.33 - val newitms = filter mem_vat news;
14.34 - (*4*)val itms' = pbl @ newitms;
14.35 -
14.36 - val (pb, where_') = Pre_Conds.check ctxt where_rls where_
14.37 - (pbt, I_Model.OLD_to_POS itms');
14.38 + val (check, preconds) =
14.39 + Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod);
14.40 "~~~~~ fun check , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
14.41 - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_POS itms'));
14.42 + (ctxt, where_rls, where_, (met_patt, met_imod));
14.43 val (env_model, (env_subst, env_eval)) = make_environments model_patt i_model
14.44 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
14.45 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
14.46 val full_subst = if env_eval = [] then pres_subst_other
14.47 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
14.48
14.49 -(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
14.50 -(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
14.51 +(*+isa==isa2*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
14.52 +(*+isa==isa2*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
14.53 +(*+isa==isa2*)val [Const ("Test.precond_rootmet", _) $ Free ("v_v", _)] = where_
14.54 +(*+*)val "[\"(#Given, (equality, e_e))\", \"(#Given, (solveFor, v_v))\", \"(#Find, (solutions, v_v'i'))\"]"
14.55 + = model_patt |> Model_Pattern.to_string ctxt(*+*)
14.56 +(*+*)val "[\n(1, [1], true ,#Given, (Cor_POS equality (x + 1 = 2) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS solveFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS solutions L , pen2str, Position.T))]"
14.57 + = i_model |> I_Model.to_string_POS ctxt(*+*)
14.58 +
14.59 (*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst
14.60
14.61 (*+*)val ctxt = Config.put rewrite_trace true ctxt;
15.1 --- a/test/Tools/isac/Specify/i-model.sml Sun Dec 10 17:35:07 2023 +0100
15.2 +++ b/test/Tools/isac/Specify/i-model.sml Mon Dec 11 09:24:02 2023 +0100
15.3 @@ -149,7 +149,7 @@
15.4 = pbl |> I_Model.to_string_POS ctxt
15.5
15.6 val return_check_single = (*case*)
15.7 - I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*);
15.8 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
15.9 (*//------------------ step into check_single ----------------------------------------------\\*)
15.10 "~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
15.11 = (ctxt, m_field, oris, (I_Model.TEST_to_OLD i_model), m_patt, ct);
16.1 --- a/test/Tools/isac/Test_Isac.thy Sun Dec 10 17:35:07 2023 +0100
16.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Dec 11 09:24:02 2023 +0100
16.3 @@ -245,11 +245,21 @@
16.4 ML_file "Minisubpbl/150a-add-given-Maximum.sml"
16.5 ML_file "Minisubpbl/150-add-given-Equation.sml"
16.6 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
16.7 +ML \<open>
16.8 +\<close> ML \<open>
16.9 +
16.10 +\<close> ML \<open>
16.11 +\<close>
16.12 ML_file "Minisubpbl/200-start-method.sml"
16.13 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
16.14 ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
16.15 ML_file "Minisubpbl/300-init-subpbl.sml"
16.16 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
16.17 +ML \<open>
16.18 +\<close> ML \<open>
16.19 +
16.20 +\<close> ML \<open>
16.21 +\<close>
16.22 ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
16.23 ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
16.24 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"