1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Thu Aug 17 08:01:45 2023 +0200
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Fri Aug 18 18:51:18 2023 +0200
1.3 @@ -18,6 +18,7 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 +
1.8 \<close> ML \<open>
1.9 \<close>
1.10 end
2.1 --- a/src/Tools/isac/Interpret/solve-step.sml Thu Aug 17 08:01:45 2023 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Fri Aug 18 18:51:18 2023 +0200
2.3 @@ -113,20 +113,28 @@
2.4
2.5 (*
2.6 check tactics (input by the user, mostly) for applicability
2.7 - and determine as much of the result of the tactic as possible initially.
2.8 + and determine of the result as much as possible initially of the tactic.
2.9 *)
2.10 fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
2.11 let
2.12 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
2.13 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
2.14 | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj"
2.15 - val {where_, ...} = Problem.from_store ctxt pI
2.16 + val {model, where_rls, where_, ...} = Problem.from_store ctxt pI
2.17 +(*T_TESTold* )
2.18 val pres = map (Pre_Conds.environment probl |> subst_atomic) where_
2.19 +( *T_TEST*)
2.20 + val checked = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
2.21 + val true_only = checked
2.22 + |> snd
2.23 + |> map (fn (true, prec) => [prec] | (false, _) => [])
2.24 + |> flat
2.25 +(*T_TESTnew*)
2.26 val ctxt = if ContextC.is_empty ctxt (*only in case of input by user*)
2.27 then dI
2.28 |> Know_Store.get_via_last_thy
2.29 |> Proof_Context.init_global
2.30 - |> ContextC.insert_assumptions pres
2.31 + |> ContextC.insert_assumptions true_only
2.32 else ctxt
2.33 in
2.34 Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
3.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Thu Aug 17 08:01:45 2023 +0200
3.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Fri Aug 18 18:51:18 2023 +0200
3.3 @@ -87,10 +87,11 @@
3.4 | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ctxt, ...}) =
3.5 let
3.6 val (dI, pI, _) = Ctree.get_somespec' spec spec'
3.7 - val {cas, ...} = Problem.from_store ctxt pI
3.8 + val {cas, model, ...} = Problem.from_store ctxt pI
3.9 + val env_model = Pre_Conds.environment_TEST model (I_Model.OLD_to_TEST probl)
3.10 in case cas of
3.11 NONE => Ctree.Form (Auto_Prog.pblterm dI pI)
3.12 - | SOME t => Ctree.Form (subst_atomic (Pre_Conds.environment probl) t)
3.13 + | SOME t => Ctree.Form (subst_atomic env_model t)
3.14 end
3.15
3.16 (* pt_extract returns
4.1 --- a/src/Tools/isac/Specify/Specify.thy Thu Aug 17 08:01:45 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Fri Aug 18 18:51:18 2023 +0200
4.3 @@ -24,7 +24,7 @@
4.4
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 -\<close> ML \<open>
4.8 +
4.9 \<close> ML \<open>
4.10 \<close>
4.11 end
5.1 --- a/src/Tools/isac/Specify/i-model.sml Thu Aug 17 08:01:45 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/i-model.sml Fri Aug 18 18:51:18 2023 +0200
5.3 @@ -26,11 +26,15 @@
5.4 type env
5.5 type message
5.6
5.7 +(** )
5.8 val feedback_to_string': feedback -> string
5.9 - val feedback_to_string: Proof.context -> feedback -> string
5.10 +( **)
5.11 + val feedback_to_string: Proof.context -> feedback -> string
5.12 (*eliminate ..*)
5.13 +(** )
5.14 val feedback_to_string'_TEST: Proof.context -> feedback_TEST -> string
5.15 - val feedback_TEST_to_string: feedback_TEST -> string
5.16 +( **)
5.17 + val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
5.18 val single_to_string: Proof.context -> single -> string
5.19 val single_to_string_TEST: Proof.context -> single_TEST -> string
5.20 val to_string: Proof.context -> T -> string
5.21 @@ -49,7 +53,11 @@
5.22 val descriptor_TEST: feedback_TEST -> descriptor
5.23 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
5.24 val o_model_values: feedback -> O_Model.values
5.25 +(*T_TESTold* )
5.26 val variables: T -> term list
5.27 +( *T_TEST*)
5.28 + val variables_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
5.29 +(*T_TEST*)
5.30 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
5.31 -> message * single
5.32 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
5.33 @@ -121,6 +129,8 @@
5.34 val empty_single = Model_Def.i_model_empty;
5.35 val empty = []: T;
5.36 val empty_TEST = []: T_TEST;
5.37 +
5.38 +
5.39 fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST ((d, ts), penv))
5.40 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
5.41 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
5.42 @@ -157,6 +167,19 @@
5.43 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
5.44 | feedback_to_string _ (Par s) = "Trm "^s;
5.45
5.46 +(**)
5.47 +fun feedback_TEST_to_string ctxt (Cor_TEST ((d, ts), penv)) =
5.48 + "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
5.49 + | feedback_TEST_to_string _ (Syn_TEST c) =
5.50 + "Syn_TEST " ^ c
5.51 + | feedback_TEST_to_string ctxt (Inc_TEST ((d, []), _)) =
5.52 + "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
5.53 + Model_Pattern.empty_for d
5.54 + | feedback_TEST_to_string ctxt (Inc_TEST ((d, ts), penv)) =
5.55 + "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
5.56 + | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
5.57 + "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
5.58 +(** )
5.59 fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) =
5.60 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
5.61 | feedback_to_string_TEST _ (Syn_TEST c) =
5.62 @@ -171,13 +194,14 @@
5.63 fun feedback_to_string' t = feedback_to_string (ContextC.for_ERROR ()) t;
5.64 fun feedback_to_string'_TEST _ t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
5.65 fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
5.66 +( **)
5.67
5.68 fun single_to_string ctxt (i, is, b, s, itm_) =
5.69 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
5.70 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
5.71 fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
5.72 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
5.73 - s ^ ", (" ^ feedback_to_string'_TEST ctxt itm_ ^ ", Position.T))";
5.74 + s ^ ", (" ^ feedback_TEST_to_string ctxt itm_ ^ ", Position.T))";
5.75
5.76 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
5.77 fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
5.78 @@ -273,7 +297,13 @@
5.79 pair2str(UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.term (ContextC.for_ERROR ()) t));*) [])
5.80 | penvval_in _ = raise ERROR "penvval_in: uncovered case in fun.def.";
5.81
5.82 -fun variables itms = itms |> Pre_Conds.environment |> map snd
5.83 +(*T_TESTold* )
5.84 +fun variables itms = itms |> Pre_Conds.environment_TEST |> map snd
5.85 +( *T_TEST*)
5.86 +fun variables_TEST model_patt i_model =
5.87 + Pre_Conds.environment_TEST model_patt i_model
5.88 + |> map snd
5.89 +(*T_TEST*)
5.90
5.91 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
5.92
5.93 @@ -309,7 +339,7 @@
5.94 if complete
5.95 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
5.96 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
5.97 - | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string' i)
5.98 + | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string (ContextC.for_ERROR ()) i)
5.99 end
5.100
5.101 fun eq1 d (_, (d', _)) = (d = d')
6.1 --- a/src/Tools/isac/Specify/m-match.sml Thu Aug 17 08:01:45 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/m-match.sml Fri Aug 18 18:51:18 2023 +0200
6.3 @@ -97,7 +97,7 @@
6.4 fun match_oris ctxt where_rls o_model (model_pattern, where_) =
6.5 let
6.6 val i_model = (flat o (map (chk1_ model_pattern))) o_model;
6.7 - val mvat = I_Model.variables i_model;
6.8 + val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
6.9 val complete = chk1_mis mvat i_model model_pattern;
6.10 val (pb, _(*where_'*)) = Pre_Conds.check_OLD ctxt where_rls where_
6.11 (model_pattern, I_Model.OLD_to_TEST i_model);
7.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Thu Aug 17 08:01:45 2023 +0200
7.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Fri Aug 18 18:51:18 2023 +0200
7.3 @@ -20,7 +20,11 @@
7.4 val to_string : Proof.context -> T -> string
7.5
7.6 val max_variant: Model_Def.i_model -> int
7.7 +(*T_TESTold* )
7.8 val environment: Model_Def.i_model -> Env.T
7.9 +( *T_TEST*)
7.10 + val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
7.11 +(*T_TEST*)
7.12
7.13 (* WRONG ENVS * )
7.14 val check: Proof.context -> Rule_Set.T -> unchecked -> Model_Def.i_model -> 'a -> checked
7.15 @@ -45,7 +49,8 @@
7.16 Model_Pattern.T * Model_Def.i_model_TEST -> checked
7.17
7.18 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
7.19 - val feedback_TEST_to_string: Model_Def.i_model_feedback_TEST -> string
7.20 +(**)
7.21 + val feedback_TEST_to_string: Proof.context -> Model_Def.i_model_feedback_TEST -> string
7.22 (** )
7.23 val check_variant_envs: Proof.context -> Rule_Set.T -> unchecked ->
7.24 env_subst -> env_eval -> checked
7.25 @@ -69,21 +74,17 @@
7.26
7.27 (*from isac_test for Minisubpbl*)
7.28 val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
7.29 +(** )
7.30 val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;
7.31 val discern_type_subst: term * term -> term list -> Env.T;
7.32 - val discern_type_eval: Model_Def.descriptor -> term list -> env_eval
7.33 - val discern_atoms: term list -> Env.T;
7.34 -
7.35 - val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T
7.36 +( **)
7.37
7.38 (** )
7.39 val mk_env: Model_Def.i_model_feedback_TEST -> Env.T
7.40 val mk_env_subst: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst
7.41 val mk_env_subst_DEL: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst
7.42 + val mk_env_eval: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_eval
7.43 ( **)
7.44 - val mk_env_eval: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_eval
7.45 - val mk_env_eval_DEL: Model_Def.i_model_single_TEST list -> env_eval
7.46 - val arrange_args2: 'a list -> 'b list -> 'c list -> int * 'd list -> (('a * 'b * 'c) * 'd) list
7.47 val filter_variants: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
7.48 Model_Def.variant -> (Model_Pattern.single * Model_Def.i_model_single_TEST) list
7.49 val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->
7.50 @@ -93,14 +94,16 @@
7.51 val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
7.52 val arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
7.53 val cnt_corrects: Model_Def.i_model_TEST -> int
7.54 +(** )
7.55 val handle_descr_ts: term -> term list -> Env.T
7.56 val distinguish_atoms: term list -> Env.T
7.57 +( **)
7.58 (*REN type_repair_env: Env.T -> Env.T*)
7.59 val repair_env: Env.T -> Env.T
7.60 - val all_atoms: term list -> bool
7.61 val all_lhs_atoms: term list -> bool
7.62 (*from isac_test for Minisubpbl*)
7.63 val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T
7.64 + val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T
7.65 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
7.66 ((term * term) * (term * term)) list
7.67 val switch_type_TEST: Model_Def.descriptor -> term list -> Model_Def.descriptor;
7.68 @@ -183,6 +186,7 @@
7.69 | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
7.70 in mx y ys end;
7.71
7.72 +(** )
7.73 (* get the constant value from a penv *)
7.74 fun getval (id, values) =
7.75 case values of
7.76 @@ -191,12 +195,14 @@
7.77 | (v1 :: v2 :: _) => (case v1 of
7.78 Const (\<^const_name>\<open>Program.Arbfix\<close>, _) => (id, v2)
7.79 | _ => (id, v1));
7.80 +( **)
7.81
7.82 (* find the variant with most items already input *)
7.83 fun max_variant itms =
7.84 let val vts = (count_variants (variants itms)) itms;
7.85 in if vts = [] then 0 else (fst o max2) vts end;
7.86
7.87 +(** )
7.88 fun mk_e (Cor (_, iv)) = [getval iv]
7.89 | mk_e (Syn _) = []
7.90 | mk_e (Typ _) = []
7.91 @@ -205,70 +211,37 @@
7.92 | mk_e (Mis _) = []
7.93 | mk_e _ = raise ERROR "mk_e: uncovered case in fun.def.";
7.94 fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
7.95 +( **)
7.96
7.97 -(* extract the environment from an item list; takes the variant with most items *)
7.98 -fun environment itms =
7.99 - let val vt = max_variant itms
7.100 - in (flat o (map (mk_en vt))) itms end;
7.101
7.102
7.103 (** new code for I_Model.T_TEST **)
7.104
7.105 +(** )
7.106 fun pen2str ctxt (t, ts) =
7.107 pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term ctxt)) ts);
7.108 -fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) =
7.109 - "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
7.110 - | feedback_to_string_TEST _ (Syn_TEST c) =
7.111 +( **)
7.112 +fun feedback_TEST_to_string ctxt (Cor_TEST ((d, ts), _)) =
7.113 + "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
7.114 + | feedback_TEST_to_string _ (Syn_TEST c) =
7.115 "Syn_TEST " ^ c
7.116 - | feedback_to_string_TEST ctxt (Inc_TEST ((d, []), _)) =
7.117 + | feedback_TEST_to_string ctxt (Inc_TEST ((d, []), _)) =
7.118 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
7.119 Model_Pattern.empty_for d
7.120 - | feedback_to_string_TEST ctxt (Inc_TEST ((d, ts), penv)) =
7.121 - "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
7.122 - | feedback_to_string_TEST ctxt (Sup_TEST (d, ts)) =
7.123 + | feedback_TEST_to_string ctxt (Inc_TEST ((d, ts), _)) =
7.124 + "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
7.125 + | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
7.126 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
7.127 +(** )
7.128 fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
7.129 +( **)
7.130
7.131
7.132 (*** make environments for substituting model_pattern+program and for evaluating pre-conditions ***)
7.133
7.134 (** OLD make environment for substituting model_pattern+program and pre-conditions **)
7.135
7.136 -(*val all_atoms_OLD: term list -> bool*)
7.137 -fun all_atoms_OLD ts =
7.138 - fold (curry and_) (map (fn t => TermC.is_atom (TermC.lhs t)) ts) true
7.139 -fun switch_type (Free (id, _)) T = Free (id, T)
7.140 - | switch_type t _ = raise TERM ("switch_type not for", [t])
7.141 -
7.142 -(*
7.143 - this repair is spurious and indicates the need for considering a separate language for Model-ing.
7.144 - E.g. "fixes" is used with 2 different types "bool list" and "real" in the problem-definition
7.145 - problem pbl_opti_univ : "univariate_calculus/Optimisation" = ..
7.146 - Given: "Constants fixes"
7.147 - Where: "0 < fixes"
7.148 - ...
7.149 - (1) Given: Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam") $ Free ("fixes", "bool list")
7.150 - (2) Where: Const ("Orderings.ord_class.less", "real \<Rightarrow> real \<Rightarrow> bool") $
7.151 - Const ("Groups.zero_class.zero", "real") $ Free ("fixes", "real")
7.152 -
7.153 - The intermediately simplistic solution is to build a pair of environments, type env_pair,
7.154 -
7.155 - The simplistic design works for the instantiation of the demo-example
7.156 - "Constants [r = (7::real)]"
7.157 - but it could be extended to instantiations like
7.158 - "Constants [a = (1::real), b = (2::real)]"
7.159 - with the same Where: "0 < fixes" in the problem-definition
7.160 - if indexing / deletion of found elements from the association list is considered.
7.161 -
7.162 - For the purpose of future pimprovements a pair of environments, type env_pair, is built;
7.163 - where as key of the "outer" environment Free ("fixes", "real" kept to future improvements
7.164 - (by indexing "fixes_1", "fixes_2" in case the are more than one element in
7.165 - "Input_Descript.Constants", "bool list..)
7.166 -*)
7.167 -fun repair_env env =
7.168 - map (fn (id_inst, val_) => (switch_type id_inst (type_of val_), val_)) env
7.169 -
7.170 -(* make an Env.T for Prec_Conds.eval *)
7.171 +(* make an Env.T for Prec_Conds.eval * )
7.172 fun mk_env (Model_Def.Cor_TEST ((descr, [ts]), _)) =
7.173 let
7.174 (*val ts = TermC.isalist2list ts*)
7.175 @@ -316,22 +289,24 @@
7.176 end
7.177 | mk_env feedb =
7.178 raise ERROR ("mk_env not reasonable for " ^ quote (feedback_TEST_to_string feedb))
7.179 -(** )
7.180 +( ** )
7.181 fun mk_env_subst equal_descr_pairs =
7.182 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
7.183 => (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id)) equal_descr_pairs
7.184 |> flat
7.185 |> repair_env
7.186 ( **)
7.187 -(*fun mk_env_eval unused? DEL!*)
7.188 +(*fun mk_env_eval unused? DEL!* )
7.189 fun mk_env_eval equal_descr_pairs =
7.190 map (fn (_, (_, _, _, _, (feedb, _))) => mk_env feedb) equal_descr_pairs
7.191 |> flat
7.192 |> filter_out (fn (_, b) => b = TermC.empty) (*drop pairs with dummy rhs*)
7.193 +( **)
7.194
7.195 -(* all_atoms: term list -> bool*)
7.196 +(* all_atoms: term list -> bool* )
7.197 fun all_atoms ts =
7.198 fold (curry and_) (map (fn t => TermC.is_atom t) ts) true
7.199 +( **)
7.200 (* all_lhs_atoms: term list -> bool*)
7.201 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
7.202 if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
7.203 @@ -343,12 +318,14 @@
7.204 ( *T_TEST*)
7.205 (* distinguish_atoms: term list -> Env.T*)
7.206 (*T_TESTnew*)
7.207 +(** )
7.208 fun distinguish_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =
7.209 if all_atoms ts
7.210 then map (rpair TermC.empty (*dummy rhs*)) ts
7.211 else if all_lhs_atoms ts
7.212 then map (fn t => (TermC.lhs t, TermC.rhs t)) ts
7.213 else []
7.214 +( ** )
7.215 (* handle_descr_ts: term -> term list -> (term * term) list*)
7.216 fun handle_descr_ts descr ts =
7.217 (*compare Model_Pattern.empty_for*)
7.218 @@ -362,6 +339,7 @@
7.219 | (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)
7.220 => distinguish_atoms ts
7.221 | _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]
7.222 +( **)
7.223
7.224
7.225 (** NEW make environment for substituting program and pre-conditions **)
7.226 @@ -369,6 +347,31 @@
7.227 fun switch_type (Free (id, _)) T = Free (id, T)
7.228 | switch_type t _ = raise TERM ("switch_type not for", [t])
7.229
7.230 +(*
7.231 + this repair is spurious and indicates the need for considering a separate language for Model-ing.
7.232 + E.g. "fixes" is used with 2 different types "bool list" and "real" in the problem-definition
7.233 + problem pbl_opti_univ : "univariate_calculus/Optimisation" = ..
7.234 + Given: "Constants fixes"
7.235 + Where: "0 < fixes"
7.236 + ...
7.237 + (1) Given: Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam") $ Free ("fixes", "bool list")
7.238 + (2) Where: Const ("Orderings.ord_class.less", "real \<Rightarrow> real \<Rightarrow> bool") $
7.239 + Const ("Groups.zero_class.zero", "real") $ Free ("fixes", "real")
7.240 +
7.241 + The intermediately simplistic solution is to build a pair of environments, type env_pair,
7.242 +
7.243 + The simplistic design works for the instantiation of the demo-example
7.244 + "Constants [r = (7::real)]"
7.245 + but it could be extended to instantiations like
7.246 + "Constants [a = (1::real), b = (2::real)]"
7.247 + with the same Where: "0 < fixes" in the problem-definition
7.248 + if indexing / deletion of found elements from the association list is considered.
7.249 +
7.250 + For the purpose of future pimprovements a pair of environments, type env_pair, is built;
7.251 + where as key of the "outer" environment Free ("fixes", "real" kept to future improvements
7.252 + (by indexing "fixes_1", "fixes_2" in case the are more than one element in
7.253 + "Input_Descript.Constants", "bool list..)
7.254 +*)
7.255 fun repair_env env =
7.256 map (fn (id_inst, val_) => (switch_type id_inst (type_of val_), val_)) env
7.257
7.258 @@ -390,6 +393,7 @@
7.259 else raise error "discern_type_subst list bool DESIGN ERROR"
7.260 | _ (*Maximum A*) => [(id, Library.the_single ts)] (*if length ts = 1 !*)
7.261
7.262 +(** )
7.263 (* discern_feedback_subst: Model_Def.i_model_feedback_TEST -> Env.T*)
7.264 fun discern_feedback_subst id (Model_Def.Cor_TEST ((descr, [ts]), _)) =
7.265 discern_type_subst (descr, id) [ts]
7.266 @@ -407,10 +411,12 @@
7.267 => (discern_feedback_subst id feedb)) equal_descr_pairs
7.268 |> flat
7.269 |> repair_env
7.270 +( **)
7.271
7.272
7.273 (** NEW make environment for evaluating pre-conditions **)
7.274
7.275 +(** )
7.276 (* all_atoms: term list -> bool*)
7.277 fun all_atoms ts =
7.278 fold (curry and_) (map (fn t => TermC.is_atom t) ts) true
7.279 @@ -442,6 +448,7 @@
7.280 map (fn (_, _, _, _, (feedb, _)) => discern_feedback_eval feedb) i_singles
7.281 |> flat
7.282 |> filter_out (fn (_, b) => b = TermC.empty) (*drop pairs with dummy rhs*)
7.283 +( **)
7.284
7.285
7.286 (*** old check_variant_envs, sep_variants_envs/_OLD, of_max_variant, check/_TEST/_OLD ***)
7.287 @@ -483,11 +490,12 @@
7.288 in
7.289 (map (pair m_patt_single) equal_variants)
7.290 end
7.291 +(** )
7.292 fun arrange_args2 [] _ _ _(*all have equal length*) = []
7.293 | arrange_args2 (b :: bs) (c :: cs) (d :: ds) (cnt, all) =
7.294 ((b, c, d), nth cnt all) :: (arrange_args2 bs cs ds (cnt + 1, all))
7.295 | arrange_args2 _ _ _ _ = raise ERROR "I_Model.arrange_args2 UnequalLengths"
7.296 -(** )
7.297 +( ** )
7.298 fun sep_variants_envs model_patt i_model =
7.299 let
7.300 val equal_descr_pairs =
7.301 @@ -682,10 +690,18 @@
7.302 end
7.303 (*T_TESTnew*)
7.304
7.305 +(* extract the environment from an I_Model.of_max_variant *)
7.306 +(*T_TESTold* )
7.307 +fun environment itms =
7.308 + let val vt = max_variant itms
7.309 + in (flat o (map (mk_en vt))) itms end;
7.310 +( *T_TEST*)
7.311 +fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2
7.312 +(*T_TEST*)
7.313
7.314 (** check pre-conditions **)
7.315
7.316 -(* WRONG ENVS expects the precondition from Problem, ie. needs substitution *)
7.317 +(* WRONG ENVS expects the precondition from Problem, ie. needs substitution * )
7.318 fun check _ _ [] _ _ = (true, [])
7.319 | check ctxt where_rls pres pbl (_ (*I_Model.variants UNNECESSARY: I_Model.T filtered for*)) =
7.320 let
7.321 @@ -693,6 +709,7 @@
7.322 val pres' = map (TermC.subst_atomic_all env) pres;
7.323 val evals = map (eval ctxt where_rls) pres';
7.324 in (foldl and_ (true, map fst evals), evals) end;
7.325 +( **)
7.326
7.327 (*T_TESTold* )
7.328 fun check_TEST _ _ [] _ = (true, [])
8.1 --- a/test/Tools/isac/BridgeJEdit/template.sml Thu Aug 17 08:01:45 2023 +0200
8.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml Fri Aug 18 18:51:18 2023 +0200
8.3 @@ -54,11 +54,11 @@
8.4 val empty_i_model = I_Model.init_TEST o_model model_patt;
8.5
8.6 (*+*)if I_Model.to_string_TEST @{context} empty_i_model = "[\n" ^
8.7 -(*+*) "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n" ^
8.8 +(*+*) "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n" ^
8.9 (*+*) "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n" ^
8.10 -(*+*) "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n" ^
8.11 +(*+*) "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n" ^
8.12 (*+*) "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n" ^
8.13 -(*+*) "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
8.14 +(*+*) "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
8.15 (*+*)then () else error "final test of build I_Model.init_TEST FAILED";
8.16
8.17 val {where_rls, where_, ...} = MethodC.from_store ctxt meth_id;
8.18 @@ -67,8 +67,8 @@
8.19 show ctxt preconds empty_i_model in_refs;
8.20 "~~~~~ fun show , args:"; val (ctxt, preconds, i_model, in_refs) =
8.21 (ctxt, preconds, empty_i_model, in_refs);
8.22 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
8.23 -(*+*) = i_model |> I_Model.to_string_TEST @{context}
8.24 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
8.25 + = i_model |> I_Model.to_string_TEST @{context}
8.26 (*let*)
8.27 val model_out =
8.28 model_to_out ctxt preconds i_model;
9.1 --- a/test/Tools/isac/Interpret/li-tool.sml Thu Aug 17 08:01:45 2023 +0200
9.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Fri Aug 18 18:51:18 2023 +0200
9.3 @@ -303,16 +303,6 @@
9.4 "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
9.5 "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
9.6 (*+*)then () else error "init_pstate: initial i_model changed";
9.7 -(*+*)if (itms |> I_Model.penv_to_string @{context}) = "[" ^ (*to be eliminated*)
9.8 -(*1*)"(l_l, [L]), " ^
9.9 -(*2*)"(q_q, [q_0]), " ^
9.10 -(*3*)"(b_b, [y]), " ^
9.11 -(*4*)"(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), " ^
9.12 -(*5*)"(fun_var, [x]), " ^
9.13 -(*6*)"(vs, [[c, c_2, c_3, c_4]]), " ^
9.14 -(*7*)"(id_der, [dy])]"
9.15 -(*+*)then () else error "init_pstate: initial penv changed";
9.16 -
9.17 (*case*)
9.18 LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
9.19 (*//------------------ step into init_pstate -----------------------------------------------\\*)
9.20 @@ -340,22 +330,21 @@
9.21 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
9.22 ;
9.23 (*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
9.24 -(*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
9.25 - "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
9.26 -(*-------------------------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
9.27 +(*defined: in program+model--vvvv--,-----------------------------------------*)
9.28 + "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^
9.29 + "(Cor_TEST Traegerlaenge L , pen2str, Position.T))), " ^
9.30 "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
9.31 - "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
9.32 + "(Cor_TEST Streckenlast q_0 , pen2str, Position.T))), " ^
9.33 "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
9.34 - "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^
9.35 + "(Cor_TEST FunktionsVariable x , pen2str, Position.T))), " ^
9.36 "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^
9.37 - "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^
9.38 + "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] , pen2str, Position.T))), " ^
9.39 "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
9.40 - "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
9.41 - "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
9.42 -(*-----------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
9.43 + "(Cor_TEST AbleitungBiegelinie dy , pen2str, Position.T))), " ^
9.44 + "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, " ^
9.45 + "(Cor_TEST Biegelinie y , pen2str, Position.T))), " ^
9.46 "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
9.47 - "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
9.48 -(*-----------------------------------------------------------------penv-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ DROP!*)
9.49 + "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str, Position.T)))]"
9.50 then () else error "of_max_variant: equal_descr_pairs CHANGED";
9.51
9.52 val return_make_env_model = make_env_model equal_descr_pairs;
10.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Thu Aug 17 08:01:45 2023 +0200
10.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Fri Aug 18 18:51:18 2023 +0200
10.3 @@ -768,16 +768,6 @@
10.4 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
10.5 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
10.6
10.7 -(*see modspec.sml#pt_form
10.8 -fun pt_form (PrfObj {form,...}) = UnparseC.term @{context} form
10.9 - | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
10.10 - let val (dI, pI, _) = get_somespec' spec spec'
10.11 - val {cas,...} = Problem.from_store pI
10.12 - in case cas of
10.13 - NONE => UnparseC.term @{context} (pblterm dI pI)
10.14 - | SOME t => UnparseC.term @{context} (subst_atomic (Pre_Conds.environment probl) t)
10.15 - end;
10.16 -*)
10.17 (*.get an 'interval' from ctree down to a certain level
10.18 by 'take_fromto children' of the nodes with specific 'from' and 'to';
10.19 'i > 0' suppresses output during recursive descent towards 'from'
11.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Thu Aug 17 08:01:45 2023 +0200
11.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Fri Aug 18 18:51:18 2023 +0200
11.3 @@ -18,7 +18,6 @@
11.4 open TermC;
11.5 open Istate;
11.6 open Tactic;
11.7 -open Pre_Conds;
11.8 open I_Model;
11.9 open P_Model
11.10 open Rewrite;
11.11 @@ -28,6 +27,7 @@
11.12 open Test_Code
11.13 open Specify
11.14 open ME_Misc
11.15 +open Pre_Conds;
11.16
11.17 val (_(*example text*),
11.18 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
11.19 @@ -173,8 +173,8 @@
11.20 (*+*)val "[\n(0, [], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(0, [], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(0, [], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(0, [], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(0, [], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
11.21 = i_model |> I_Model.to_string_TEST @ {context}
11.22 ( *with OLD code*)
11.23 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
11.24 - = i_model |> I_Model.to_string_TEST @{context}
11.25 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
11.26 + = i_model |> I_Model.to_string_TEST @{context}
11.27 val all_variants =
11.28 map (fn (_, variants, _, _, _) => variants) i_model
11.29 |> flat
11.30 @@ -659,8 +659,8 @@
11.31 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
11.32 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
11.33 (*+*) = model_patt |> Model_Pattern.to_string @{context}
11.34 -(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A ,(maxx, [A]), Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] ,(vals, [[u, v]]), Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2]), Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]), Position.T))]"
11.35 -(*+*) = i_model |> I_Model.to_string_TEST @{context}
11.36 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
11.37 + = i_model |> I_Model.to_string_TEST @{context}
11.38
11.39 val return_of_max_variant as (_, _, (env_subst, env_eval)) =
11.40 of_max_variant model_patt i_model
12.1 --- a/test/Tools/isac/Specify/i-model.sml Thu Aug 17 08:01:45 2023 +0200
12.2 +++ b/test/Tools/isac/Specify/i-model.sml Fri Aug 18 18:51:18 2023 +0200
12.3 @@ -173,8 +173,8 @@
12.4 I_Model.init_TEST o_model model_patt;
12.5 "~~~~~ fun init_TEST , args:"; val (ctxt, model_patt) = (ctxt, model_patt);
12.6 ;
12.7 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
12.8 -(*+*) = I_Model.to_string_TEST @{context} empty_i_model;
12.9 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
12.10 + = I_Model.to_string_TEST @{context} empty_i_model;
12.11
12.12
12.13 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
13.1 --- a/test/Tools/isac/Specify/pre-conditions.sml Thu Aug 17 08:01:45 2023 +0200
13.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml Fri Aug 18 18:51:18 2023 +0200
13.3 @@ -29,12 +29,12 @@
13.4 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
13.5 CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data
13.6 ;
13.7 -if (probl |> I_Model.to_string_TEST @{context}) = "[\n" ^
13.8 - "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n" ^
13.9 +(*+*)if (probl |> I_Model.to_string_TEST @{context}) = "[\n" ^
13.10 + "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n" ^
13.11 "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n" ^
13.12 - "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n" ^
13.13 + "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n" ^
13.14 "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n" ^
13.15 - "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
13.16 + "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
13.17 then () else error "probl FROM state CHANGED";
13.18
13.19 (* probl_POS from above, #1 and #2 replaced by complete items, in order to evaluate to true*)
14.1 --- a/test/Tools/isac/Specify/refine.sml Thu Aug 17 08:01:45 2023 +0200
14.2 +++ b/test/Tools/isac/Specify/refine.sml Fri Aug 18 18:51:18 2023 +0200
14.3 @@ -393,7 +393,7 @@
14.4 = model_pattern |> Model_Pattern.to_string @{context}
14.5 (*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
14.6
14.7 - val mvat = I_Model.variables i_model;
14.8 + val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
14.9 val complete = chk1_mis mvat i_model model_pattern;
14.10
14.11 val (pb as true, (** )_( **)where_'(**)) =
15.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Aug 17 08:01:45 2023 +0200
15.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Aug 18 18:51:18 2023 +0200
15.3 @@ -168,8 +168,7 @@
15.4 \<close>
15.5 ML \<open>
15.6 \<close> ML \<open>
15.7 -\<close> ML \<open>
15.8 -\<close> ML \<open>
15.9 +
15.10 \<close> ML \<open>
15.11 \<close>
15.12
15.13 @@ -273,6 +272,11 @@
15.14 ML_file "Interpret/istate.sml"
15.15 ML_file "Interpret/error-pattern.sml"
15.16 ML_file "Interpret/li-tool.sml"
15.17 +ML \<open>
15.18 +\<close> ML \<open>
15.19 +
15.20 +\<close> ML \<open>
15.21 +\<close>
15.22 ML_file "Interpret/lucas-interpreter.sml"
15.23 ML_file "Interpret/step-solve.sml"
15.24
16.1 --- a/test/Tools/isac/Test_Theory.thy Thu Aug 17 08:01:45 2023 +0200
16.2 +++ b/test/Tools/isac/Test_Theory.thy Fri Aug 18 18:51:18 2023 +0200
16.3 @@ -57,7 +57,15 @@
16.4 section \<open>===== ============================================================================\<close>
16.5 ML \<open>
16.6 \<close> ML \<open>
16.7 -\<close> ML \<open>
16.8 +
16.9 +\<close> ML \<open>
16.10 +\<close>
16.11 +
16.12 +section \<open>===================================================================================\<close>
16.13 +section \<open>===== ============================================================================\<close>
16.14 +ML \<open>
16.15 +\<close> ML \<open>
16.16 +
16.17 \<close> ML \<open>
16.18 \<close>
16.19
16.20 @@ -515,8 +523,8 @@
16.21 = i_model |> I_Model.to_string_TEST @ {context}
16.22 ( *with OLD code*)
16.23 \<close> ML \<open> (*with NEW code*)
16.24 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
16.25 - = i_model |> I_Model.to_string_TEST @{context}
16.26 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
16.27 + = i_model |> I_Model.to_string_TEST @{context}
16.28 \<close> ML \<open>
16.29 val all_variants =
16.30 map (fn (_, variants, _, _, _) => variants) i_model
16.31 @@ -1149,8 +1157,9 @@
16.32 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
16.33 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
16.34 (*+*) = model_patt |> Model_Pattern.to_string @{context}
16.35 -(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A ,(maxx, [A]), Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] ,(vals, [[u, v]]), Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2]), Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]), Position.T))]"
16.36 -(*+*) = i_model |> I_Model.to_string_TEST @{context}
16.37 +\<close> ML \<open>
16.38 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
16.39 + = i_model |> I_Model.to_string_TEST @{context}
16.40 \<close> ML \<open>
16.41 val return_of_max_variant as (_, _, (env_subst, env_eval)) =
16.42 of_max_variant model_patt i_model
16.43 @@ -1551,8 +1560,8 @@
16.44 val (preok as true, xxx) =
16.45 Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
16.46 \<close> ML \<open>
16.47 -(*+*)val "[\n(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T)), \n(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T)), \n(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T))]"
16.48 - = I_Model.OLD_to_TEST pbl |> I_Model.to_string_TEST @{context};
16.49 +(*+*)val "[\n(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_TEST solveFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_TEST solutions L , pen2str, Position.T))]"
16.50 + = I_Model.OLD_to_TEST pbl |> I_Model.to_string_TEST @{context};
16.51 (*+*)val "[precond_rootpbl v_v]" = where_ |> UnparseC.terms @{context};
16.52 \<close> ML \<open>
16.53 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
16.54 @@ -1863,11 +1872,11 @@
16.55 \<close> ML \<open>
16.56 (*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
16.57 "((#Given, (equality, e_e)), " ^
16.58 - "(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T))), " ^
16.59 + "(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) , pen2str, Position.T))), " ^
16.60 "((#Given, (solveFor, v_v)), " ^
16.61 - "(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T))), " ^
16.62 + "(2, [1], true ,#Given, (Cor_TEST solveFor x , pen2str, Position.T))), " ^
16.63 "((#Find, (solutions, v_v'i')), " ^
16.64 - "(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T)))]"
16.65 + "(3, [1], true ,#Find, (Cor_TEST solutions L , pen2str, Position.T)))]"
16.66 then () else error "equal_descr_pairs CHANGED";
16.67 \<close> ML \<open>(*|||----------- contine of_max_variant ------------------------------------------------*)
16.68 (*|||----------------- contine of_max_variant ------------------------------------------------*)
16.69 @@ -2151,6 +2160,7 @@
16.70 \<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)
16.71 (*///----------------- step into of_max_variant --------------------------------------------\\*)
16.72 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
16.73 +\<close> ML \<open>
16.74 val all_variants =
16.75 map (fn (_, variants, _, _, _) => variants) i_model
16.76 |> flat
16.77 @@ -2164,25 +2174,26 @@
16.78 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
16.79 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
16.80 ;
16.81 +\<close> ML \<open>
16.82 (*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
16.83 (*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
16.84 - "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
16.85 -(*-------------------------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
16.86 + "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^
16.87 + "(Cor_TEST Traegerlaenge L , pen2str, Position.T))), " ^
16.88 "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
16.89 - "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
16.90 + "(Cor_TEST Streckenlast q_0 , pen2str, Position.T))), " ^
16.91 "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
16.92 - "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^
16.93 + "(Cor_TEST FunktionsVariable x , pen2str, Position.T))), " ^
16.94 "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^
16.95 - "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^
16.96 + "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] , pen2str, Position.T))), " ^
16.97 "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
16.98 - "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
16.99 - "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
16.100 -(*-----------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
16.101 + "(Cor_TEST AbleitungBiegelinie dy , pen2str, Position.T))), " ^
16.102 + "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, " ^
16.103 + "(Cor_TEST Biegelinie y , pen2str, Position.T))), " ^
16.104 "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
16.105 - "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
16.106 -(*-----------------------------------------------------------------penv-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ DROP!*)
16.107 + "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str, Position.T)))]"
16.108 then () else error "of_max_variant: equal_descr_pairs CHANGED";
16.109
16.110 +\<close> ML \<open>
16.111 val return_make_env_model = make_env_model equal_descr_pairs;
16.112 \<close> ML \<open> (*////--------- step into make_env_model --------------------------------------------\\*)
16.113 (*////---------------- step into make_env_model --------------------------------------------\\*)
16.114 @@ -2207,6 +2218,12 @@
16.115 val return_handle_lists_step =
16.116 [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
16.117 \<close> ML \<open>
16.118 +\<close> ML \<open>
16.119 +\<close> ML \<open>
16.120 +return_handle_lists_step
16.121 +\<close> ML \<open>
16.122 +(*+*)val xxx = return_handle_lists_step |> Subst.to_string @{context}
16.123 +\<close> ML \<open>
16.124 (*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
16.125 = return_handle_lists_step |> Subst.to_string @{context}
16.126 (*\\\\---------------- step into make_env_model --------------------------------------------//*)
16.127 @@ -2357,7 +2374,7 @@
16.128 = model_pattern |> Model_Pattern.to_string @{context}
16.129 (*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
16.130
16.131 - val mvat = I_Model.variables i_model;
16.132 + val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
16.133 val complete = chk1_mis mvat i_model model_pattern;
16.134
16.135 val (pb as true, (** )_( **)where_'(**)) =