1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Aug 15 17:44:56 2023 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Aug 17 08:01:45 2023 +0200
1.3 @@ -167,11 +167,8 @@
1.4 begin
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -val (nxt, tac) = (Tactic.Empty_Tac, Tactic.Empty_Tac)
1.8 \<close> ML \<open>
1.9 -val xxx = nxt;
1.10 \<close> ML \<open>
1.11 -val xxx = tac;
1.12 \<close> ML \<open>
1.13 \<close>
1.14 subsection \<open>make Minisubpbl independent from Thy_Info\<close>
2.1 --- a/src/Tools/isac/Specify/i-model.sml Tue Aug 15 17:44:56 2023 +0200
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Thu Aug 17 08:01:45 2023 +0200
2.3 @@ -66,8 +66,10 @@
2.4 val to_p_model: theory -> feedback -> string
2.5 val eq1: ''a -> 'b * (''a * 'c) -> bool
2.6
2.7 +(** )
2.8 val is_complete_OLD: Proof.context -> Model_Pattern.T -> Rule_Def.rule_set ->
2.9 Pre_Conds.unchecked -> T_TEST -> variants option
2.10 +( **)
2.11 val is_complete_variant: int -> T_TEST-> bool
2.12
2.13 (*T_TESTold* )
2.14 @@ -508,6 +510,7 @@
2.15 fun is_complete_variant no_model_items i_model =
2.16 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
2.17
2.18 +(** )
2.19 fun is_complete_OLD ctxt model_patt where_rls pres i_model =
2.20 let
2.21 val no_model_items = length model_patt
2.22 @@ -522,6 +525,7 @@
2.23 then NONE
2.24 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
2.25 end
2.26 +( **)
2.27
2.28 val of_max_variant = Pre_Conds.of_max_variant
2.29
3.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Tue Aug 15 17:44:56 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Thu Aug 17 08:01:45 2023 +0200
3.3 @@ -22,15 +22,23 @@
3.4 val max_variant: Model_Def.i_model -> int
3.5 val environment: Model_Def.i_model -> Env.T
3.6
3.7 - (* WRONG ENVS *)
3.8 + (* WRONG ENVS * )
3.9 val check: Proof.context -> Rule_Set.T -> unchecked -> Model_Def.i_model -> 'a -> checked
3.10 - (* WRONG ENVS *)
3.11 +( **)
3.12 +(*T_TESTold* )
3.13 val check_from_store: Proof.context -> Rule_Set.T -> unchecked -> env_subst -> env_eval -> checked
3.14 - (* vvv-replaces-^^^*)
3.15 - val check_envs_TEST: Proof.context -> Rule_Def.rule_set -> term list ->
3.16 - Env.T * (env_subst * env_eval) -> checked
3.17 - (* WRONG ENVS *)
3.18 - val check_TEST : Proof.context -> Rule_Set.T -> unchecked_TEST -> env_eval -> checked_TEST
3.19 +( *T_TEST*)
3.20 +(*RN check_with_envs*)
3.21 + val check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
3.22 + -> checked
3.23 +(*T_TESTnew*)
3.24 +(**)
3.25 + (*T_TESTold* )
3.26 + val check_TEST: Proof.context -> Rule_Set.T -> unchecked_TEST -> env_eval -> checked_TEST
3.27 +( *T_TEST*)
3.28 + val check_pos: Proof.context -> Rule_Set.T -> unchecked_TEST ->
3.29 + Model_Pattern.T * Model_Def.i_model_TEST -> checked_TEST
3.30 +(*T_TESTnew*)
3.31
3.32 (*this makes the OLD tests run AFTER introduction of I_Model.T_TEST..*)
3.33 val check_OLD: Proof.context -> Rule_Set.T -> unchecked ->
3.34 @@ -38,16 +46,18 @@
3.35
3.36 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
3.37 val feedback_TEST_to_string: Model_Def.i_model_feedback_TEST -> string
3.38 -
3.39 +(** )
3.40 val check_variant_envs: Proof.context -> Rule_Set.T -> unchecked ->
3.41 env_subst -> env_eval -> checked
3.42 +( **)
3.43
3.44 (*val sep_variants_envs replaced by of_max_variant TODO
3.45 - for that purpose compare with sep_variants_envs_OLD TODO*)
3.46 + for that purpose compare with sep_variants_envs_OLD TODO* )
3.47 val sep_variants_envs: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.48 ((Model_Def.i_model_TEST * env_subst * env_eval) * Model_Def.variant) list
3.49 val sep_variants_envs_OLD: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.50 env_subst * env_eval;
3.51 +( **)
3.52
3.53 (*T_TESTold* )
3.54 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.55 @@ -66,9 +76,11 @@
3.56
3.57 val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T
3.58
3.59 +(** )
3.60 val mk_env: Model_Def.i_model_feedback_TEST -> Env.T
3.61 val mk_env_subst: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst
3.62 val mk_env_subst_DEL: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst
3.63 +( **)
3.64 val mk_env_eval: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_eval
3.65 val mk_env_eval_DEL: Model_Def.i_model_single_TEST list -> env_eval
3.66 val arrange_args2: 'a list -> 'b list -> 'c list -> int * 'd list -> (('a * 'b * 'c) * 'd) list
3.67 @@ -113,7 +125,7 @@
3.68 type unchecked = term list
3.69 type unchecked_TEST = (term * Position.T) list
3.70 type checked = bool * (bool * term) list
3.71 -type checked_TEST = bool * (bool * (term * Position.T)) list
3.72 +type checked_TEST = bool * ((bool * (term * Position.T)) list)
3.73
3.74 (*
3.75 we have three kinds of Env.T in the specification-phase:
3.76 @@ -304,11 +316,13 @@
3.77 end
3.78 | mk_env feedb =
3.79 raise ERROR ("mk_env not reasonable for " ^ quote (feedback_TEST_to_string feedb))
3.80 +(** )
3.81 fun mk_env_subst equal_descr_pairs =
3.82 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
3.83 => (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id)) equal_descr_pairs
3.84 |> flat
3.85 |> repair_env
3.86 +( **)
3.87 (*fun mk_env_eval unused? DEL!*)
3.88 fun mk_env_eval equal_descr_pairs =
3.89 map (fn (_, (_, _, _, _, (feedb, _))) => mk_env feedb) equal_descr_pairs
3.90 @@ -431,7 +445,7 @@
3.91
3.92
3.93 (*** old check_variant_envs, sep_variants_envs/_OLD, of_max_variant, check/_TEST/_OLD ***)
3.94 -
3.95 +(** )
3.96 fun check_variant_envs ctxt where_rls pres env_subst env_eval =
3.97 let
3.98 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
3.99 @@ -440,6 +454,7 @@
3.100 in
3.101 (foldl and_ (true, map fst evals), pres_subst)
3.102 end
3.103 +( **)
3.104
3.105
3.106 (* check_variant_envs for PIDE *)
3.107 @@ -472,6 +487,7 @@
3.108 | arrange_args2 (b :: bs) (c :: cs) (d :: ds) (cnt, all) =
3.109 ((b, c, d), nth cnt all) :: (arrange_args2 bs cs ds (cnt + 1, all))
3.110 | arrange_args2 _ _ _ _ = raise ERROR "I_Model.arrange_args2 UnequalLengths"
3.111 +(** )
3.112 fun sep_variants_envs model_patt i_model =
3.113 let
3.114 val equal_descr_pairs =
3.115 @@ -490,8 +506,10 @@
3.116 in
3.117 arrange_args2 i_models envs_subst envs_eval (1, all_variants)
3.118 end
3.119 +( **)
3.120
3.121 (* smash all environments into one; this works only for old test before Maximum-example *)
3.122 +(** )
3.123 fun sep_variants_envs_OLD model_patt i_model =
3.124 let
3.125 val equal_descr_pairs =
3.126 @@ -509,6 +527,7 @@
3.127 in
3.128 (flat envs_subst, flat envs_eval)
3.129 end
3.130 +( **)
3.131
3.132 (** of_max_variant **)
3.133
3.134 @@ -674,7 +693,8 @@
3.135 val pres' = map (TermC.subst_atomic_all env) pres;
3.136 val evals = map (eval ctxt where_rls) pres';
3.137 in (foldl and_ (true, map fst evals), evals) end;
3.138 -(* WRONG ENVS expects the precondition from PIDE, ie. already substituted *)
3.139 +
3.140 +(*T_TESTold* )
3.141 fun check_TEST _ _ [] _ = (true, [])
3.142 | check_TEST ctxt where_rls preconds env_eval =
3.143 let
3.144 @@ -685,7 +705,22 @@
3.145 in
3.146 (foldl and_ (true, map fst evals), (map fst evals) ~~ preconds)
3.147 end;
3.148 -(* WRONG ENVS *)
3.149 +( *T_TEST*)
3.150 +fun check_pos ctxt where_rls where_POS (model_patt, i_model) =
3.151 + let
3.152 + val (_, _, (_, env_eval)) = of_max_variant model_patt
3.153 + (filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)
3.154 + val full_subst = if env_eval = []
3.155 + then map (fn (t, pos) => ((true, t), pos)) where_POS
3.156 + else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;
3.157 + val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
3.158 + val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)
3.159 + in
3.160 + (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
3.161 + end;
3.162 +(*T_TESTnew*)
3.163 +
3.164 +(*T_TESTold* )
3.165 fun check_from_store ctxt where_rls pres env_subst env_eval =
3.166 let
3.167 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
3.168 @@ -694,19 +729,23 @@
3.169 in
3.170 (foldl and_ (true, map fst evals), pres_subst)
3.171 end
3.172 -(* vvv-replaces-^^^*)
3.173 -fun check_envs_TEST ctxt where_rls pres (env_model, (env_subst, env_eval)) =
3.174 +( *T_TEST*)
3.175 +(* takes the envs resulting from of_max_variant *)
3.176 +fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
3.177 let
3.178 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
3.179 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
3.180 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
3.181 val full_subst = if env_eval = [] then pres_subst_other
3.182 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
3.183 val evals = map (eval ctxt where_rls) full_subst
3.184 - in
3.185 + in
3.186 (foldl and_ (true, map fst evals), pres_subst_other)
3.187 - end
3.188 + end
3.189 +(*T_TESTnew*)
3.190 +(* vvv-replaces-^^^*)
3.191
3.192 (* expects the precondition from Problem, ie. needs substitution by env_model*)
3.193 +(* TODO: check_OLD shall call check_envs_TEST *)
3.194 fun check_OLD _ _ [] _ = (true, [])
3.195 | check_OLD ctxt where_rls where_ (model_patt, i_model) =
3.196 let
4.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Tue Aug 15 17:44:56 2023 +0200
4.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Thu Aug 17 08:01:45 2023 +0200
4.3 @@ -93,10 +93,10 @@
4.4 ( *\----- ERROR: mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"-------------/*)
4.5 (*reminder for Template.show ----------------------------------------------------------------/*)
4.6
4.7 -(*reminder for Pre_Conds.check_TEST ---------------------------------------------------------\*)
4.8 +(*reminder for Pre_Conds.check_TEST ---------------------------------------------------------\* )
4.9 val (true, [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
4.10 Free ("r", _), _))]) = Pre_Conds.check_TEST ctxt where_rls where_ env_eval;
4.11 -(*reminder for Pre_Conds.check_TEST ---------------------------------------------------------/*)
4.12 +( *reminder for Pre_Conds.check_TEST ---------------------------------------------------------/*)
4.13 (**)
4.14 val ((_, _, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =
4.15 References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref
5.1 --- a/test/Tools/isac/BridgeJEdit/calculation.sml Tue Aug 15 17:44:56 2023 +0200
5.2 +++ b/test/Tools/isac/BridgeJEdit/calculation.sml Thu Aug 17 08:01:45 2023 +0200
5.3 @@ -254,10 +254,10 @@
5.4 ( *\----- ERROR: mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"-------------/*)
5.5 (*reminder for Template.show ----------------------------------------------------------------/*)
5.6
5.7 -(*reminder for Pre_Conds.check_TEST ---------------------------------------------------------\*)
5.8 +(*reminder for Pre_Conds.check_TEST ---------------------------------------------------------\* )
5.9 val (true, [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
5.10 Free ("r", _), _))]) = Pre_Conds.check_TEST ctxt where_rls where_ env_eval;
5.11 -(*reminder for Pre_Conds.check_TEST ---------------------------------------------------------/*)
5.12 +( *reminder for Pre_Conds.check_TEST ---------------------------------------------------------/*)
5.13 (**)
5.14 val ((_, true, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =
5.15 References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref
6.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue Aug 15 17:44:56 2023 +0200
6.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Thu Aug 17 08:01:45 2023 +0200
6.3 @@ -399,7 +399,8 @@
6.4 = formals |> UnparseC.terms @{context}
6.5 (*+*)val 7 = length formals
6.6
6.7 - val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
6.8 + val preconds =
6.9 + Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
6.10 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
6.11 val ist = Istate.e_pstate
6.12 |> Istate.set_eval prog_rls
7.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Aug 15 17:44:56 2023 +0200
7.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Aug 17 08:01:45 2023 +0200
7.3 @@ -98,9 +98,9 @@
7.4 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
7.5 (ctxt, where_rls, where_, (pbt, OLD_to_TEST pbl)); (*..delete double above --- adhoc inserted n ---*)
7.6
7.7 -(*NEW*)val (env_subst, env_eval) =
7.8 - sep_variants_envs_OLD model_patt i_model; (** )ERROR lhs called with x_i WN230401 ( **)
7.9 -"~~~~~ fun sep_variants_envs_OLD , args:"; val (model_patt, i_model) = (model_patt, i_model);
7.10 + val (_, env_model, (env_subst, env_eval)) =
7.11 + of_max_variant model_patt i_model;
7.12 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
7.13
7.14 (*+*)(pbt |> Model_Pattern.to_string @{context}) = "[\"" ^
7.15 "(#Given, (equality, e_e))\", \"" ^
7.16 @@ -111,46 +111,34 @@
7.17 "(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T)), \n" ^
7.18 "(3, [1], true ,#Find, (Cor_TEST solutions x_i ,(v_v'i', [x_i]), Position.T))]";
7.19
7.20 - val equal_descr_pairs =
7.21 - map (get_equal_descr i_model) model_patt
7.22 - |> flat
7.23 val all_variants =
7.24 - map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs
7.25 + map (fn (_, variants, _, _, _) => variants) i_model
7.26 |> flat
7.27 |> distinct op =
7.28 - val variants_separated = map (filter_variants equal_descr_pairs) all_variants
7.29 -(*NEW*)val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>
7.30 - m_field = "#Given")) variants_separated
7.31 - val envs_subst = map
7.32 - Pre_Conds.mk_env_subst (*NEW..*)restricted_to_given(*..NEW* )variants_separated( **);
7.33 + val variants_separated = map (filter_variants' i_model) all_variants
7.34 + val sums_corr = map (cnt_corrects) variants_separated
7.35 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
7.36 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
7.37 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
7.38 + val i_model_max =
7.39 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
7.40 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
7.41 + val env_model = make_env_model equal_descr_pairs
7.42 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
7.43
7.44 -(*//------------------ step into mk_env_subst ----------------------------------------------\\*)
7.45 -"~~~~~ fun mk_env_subst , args:"; val (equal_descr_pairs) = (restricted_to_given);
7.46 + val subst_eval_list =
7.47 + make_envs_preconds equal_givens;
7.48 +(*//------------------ step into make_envs_preconds ----------------------------------------\\*)
7.49 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
7.50 +"~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = (nth 1 equal_givens);
7.51
7.52 -val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
7.53 - => (mk_env feedb) |> map fst |> map (pair id))
7.54 -: Model_Pattern.single * I_Model.single_TEST -> Env.T;
7.55 -"~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = nth 1 (nth 1 equal_descr_pairs);
7.56 -(*------------------------------------------------------------------ item-^^^^^ ^^^^^-variant*)
7.57 -(*+*)val [(Const ("HOL.eq", _) $
7.58 - (Const ("Groups.plus_class.plus", _) $ (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) $ Free ("x", _)) $
7.59 - Const ("Groups.zero_class.zero", _),
7.60 - Const ("empty", _))] = mk_env feedb;
7.61 +val [] =
7.62 + discern_feedback id feedb;
7.63 +(*\\------------------ step into make_envs_preconds ----------------------------------------//*)
7.64
7.65 -"~~~~~ fun mk_env , args:"; val (Model_Def.Cor_TEST ((descr, [ts]), _)) = (feedb);
7.66 - val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]
7.67 -
7.68 -(*+*)val "[- 1 + x = 0]" = ts |> UnparseC.terms @{context}
7.69 -
7.70 -val _ (*Maximum A*) = (*fall through*)
7.71 - (*case*) type_of descr (*of*);
7.72 -
7.73 -(*+*)type_of descr(* = "bool \<Rightarrow> una"*);
7.74 -(*\\------------------ step into mk_env_subst ----------------------------------------------//*)
7.75 -val return_mk_env = (hd ts, TermC.empty)
7.76 -
7.77 -(*-------------------- continuing sep_variants_envs ------------------------------------------*)
7.78 - val envs_eval = map Pre_Conds.mk_env_eval (*NEW..*)restricted_to_given(*..NEW* )variants_separated( **)
7.79 +(*-------------------- continuing of_max_variant ---------------------------------------------*)
7.80 + val (env_subst, env_eval) = split_list subst_eval_list
7.81 +val return_of_max_variant = (i_model_max, env_model, (env_subst, env_eval))
7.82 (*\------------------- step into me Add_Find ------------------------------------------------/*)
7.83 val (p,_,f,nxt,_,pt) = return_Add_Find; (** )val Specify_Theory "Test" = nxt;( **)
7.84
8.1 --- a/test/Tools/isac/Specify/pre-conditions.sml Tue Aug 15 17:44:56 2023 +0200
8.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml Thu Aug 17 08:01:45 2023 +0200
8.3 @@ -6,17 +6,18 @@
8.4 "-----------------------------------------------------------------------------------------------";
8.5 "table of contents -----------------------------------------------------------------------------";
8.6 "-----------------------------------------------------------------------------------------------";
8.7 -"----------- build Pre_Conds.check_TEST --------------------------------------------------------";
8.8 +"----------- build Pre_Conds.check_pos ---------------------------------------------------------";
8.9 "-----------------------------------------------------------------------------------------------";
8.10 "-----------------------------------------------------------------------------------------------";
8.11 "-----------------------------------------------------------------------------------------------";
8.12
8.13 -"----------- build Pre_Conds.check_TEST --------------------------------------------------------";
8.14 -"----------- build Pre_Conds.check_TEST --------------------------------------------------------";
8.15 -"----------- build Pre_Conds.check_TEST --------------------------------------------------------";
8.16 +"----------- build Pre_Conds.check_pos ---------------------------------------------------------";
8.17 +"----------- build Pre_Conds.check_pos ---------------------------------------------------------";
8.18 +"----------- build Pre_Conds.check_pos ---------------------------------------------------------";
8.19 (*see Outer_Syntax: val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)
8.20 +open Model_Def;
8.21 +open Pre_Conds;
8.22 open I_Model
8.23 -open Pre_Conds;
8.24 (*//------------------ test data setup -----------------------------------------------------\\*)
8.25 val thy = @{theory Calculation}
8.26
8.27 @@ -28,14 +29,16 @@
8.28 val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
8.29 CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data
8.30 ;
8.31 -probl: Model_Def.i_model_TEST
8.32 -(*[(1, [1, 2, 3], false, "#Given", (Inp_TEST (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
8.33 - (2, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
8.34 - (3, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
8.35 - (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
8.36 - (5, [1, 2], false, "#Relate", (Inp_TEST (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
8.37 -;
8.38 -val probl_POS = (*from above, #1 and #2 replaced by complete items*)
8.39 +if (probl |> I_Model.to_string_TEST @{context}) = "[\n" ^
8.40 + "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n" ^
8.41 + "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n" ^
8.42 + "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n" ^
8.43 + "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n" ^
8.44 + "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
8.45 +then () else error "probl FROM state CHANGED";
8.46 +
8.47 +(* probl_POS from above, #1 and #2 replaced by complete items, in order to evaluate to true*)
8.48 +val probl_POS =
8.49 (1, [1,2,3], true, "#Given",
8.50 (Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),
8.51 (@{term "fixes::real"}, [@{term "r::real"}])), Position.none )) ::
8.52 @@ -43,75 +46,74 @@
8.53 (5, [1,2], true, "#Relate",
8.54 (Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
8.55 (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))
8.56 - :: [];
8.57 -val probl_OLD = I_Model.TEST_to_OLD probl;
8.58 + :: [] : I_Model.T_TEST;
8.59 +val probl_OLD = I_Model.TEST_to_OLD probl : I_Model.T;
8.60
8.61 val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)
8.62 Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")
8.63 ;
8.64 -(model_patt |> Model_Pattern.to_string ctxt) =
8.65 +if (model_patt |> Model_Pattern.to_string ctxt) =
8.66 "[\"(#Given, (Constants, fixes))\", " ^
8.67 "\"(#Find, (Maximum, maxx))\", " ^
8.68 "\"(#Find, (AdditionalValues, vals))\", " ^
8.69 "\"(#Relate, (Extremum, extr))\", " ^
8.70 - "\"(#Relate, (SideConditions, sideconds))\"]";
8.71 + "\"(#Relate, (SideConditions, sideconds))\"]"
8.72 +then () else error "i_model FROM state CHANGED";
8.73 val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})
8.74
8.75 (*prepare check input with Position.T----------------------------------------------------------^^-*)
8.76 val where_POS = [(@{term "0 < (r::real)"}, Position.none)];
8.77 (*\\------------------ test data setup -----------------------------------------------------//*)
8.78
8.79 -(*//------------------ test on old code (partially with Position.T) ------------------------\\*)
8.80 -(*ERROR DURING TRANSITION I_Model.T \<longrightarrow> T_TEST penv_value: no values in 'Constants * )
8.81 - check ctxt where_rls where_OLD probl_OLD "DEL: variants";
8.82 -( **)
8.83 -"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, pbl) =
8.84 - (ctxt, where_rls, where_OLD, probl_OLD);
8.85 - (*the values wanted, not yet achieved..* )
8.86 - val env = Pre_Conds.environment pbl: Env.T
8.87 - ( * [(fixes, r)] *)
8.88 -(*/----- already in test/../preconditions ---------------------------------------------*)
8.89 - val pres' = map (TermC.subst_atomic_all env) pres: (bool * term) list
8.90 - (* [(true, 0 < x)] .. true: all substituted*)
8.91 - val evals = map (eval ctxt where_rls) pres': (bool * term) list
8.92 - (* [(true, 0 < x)] .. true: evaluated to true*)
8.93 -val return_check =
8.94 - (foldl and_ (true, map fst evals), evals): bool * (bool * term) list;
8.95 +(*//------------------ build new code (with Position.T) ------------------------------------\\*)
8.96 + Pre_Conds.check_pos ctxt where_rls where_POS (model_patt, probl);
8.97 +"~~~~~ fun check_pos , args:"; val (ctxt, where_rls, where_POS, (model_patt, i_model)) =
8.98 + (ctxt, where_rls, where_POS, (model_patt, probl));
8.99
8.100 - eval ctxt where_rls (hd pres');
8.101 -"~~~~~ fun eval , args:"; val (ctxt, where_rls, (bool, where_)) = (ctxt, where_rls, hd pres');
8.102 - (*if*) Rewrite.eval_true ctxt [where_] where_rls (*then*);
8.103 +(*+*)val [(prec, _)] = where_POS;
8.104 +(*+*)val "0 < r" = prec |> UnparseC.term @{context} (* 1st substitution already done*)
8.105 +
8.106 +(*+*)val ((1, [1, 2, 3], false, "#Given", (Inc_TEST _, _)) :: _) = probl
8.107 +(*+*)val 5 = length probl;
8.108 +(*!!!*)val ((1, [1, 2, 3], true, "#Given", (Cor_TEST _, _)) :: _) = probl_POS
8.109 +(*!!!*)val 5 = length probl_POS; (*thus subst_atomic_all \<longrightarrow> false, replaces for test -------vvvv*)
8.110 +
8.111 +
8.112 + val (_, (** )_( **)env_model(**), ((** )_( **)env_subst(**), env_eval)) = of_max_variant model_patt
8.113 + (filter (fn (_, _, _, m_field ,_) => m_field = "#Given") probl_POS)
8.114 +
8.115 +(*+*)val "[\"\n(fixes, [[r = 7]])\"]" = env_model |> Subst.to_string @{context}
8.116 +(*+*)val "[\"\n(fixes, r)\"]" = env_subst |> Subst.to_string @{context}
8.117 +(*+*)val "[\"\n(r, 7)\"]" = env_eval |> Subst.to_string @{context}
8.118 +
8.119 + val full_subst = if env_eval = []
8.120 + then map (fn (t, pos) => ((true, t), pos)) where_POS
8.121 + else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;
8.122 +
8.123 +(*+*)val [((true, precond), pos)] = full_subst;
8.124 +(*+*)val "0 < 7" = precond |> UnparseC.term @{context}
8.125 +
8.126 + val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
8.127 +
8.128 +(*+*)val (true, precond) = eval ctxt where_rls (true, precond)
8.129 +(*+*)val "0 < 7" = precond |> UnparseC.term @{context}
8.130 +(*+*)val [((true, precond), pos)] = evals
8.131 +(*+*)val "0 < 7" = precond |> UnparseC.term @{context}
8.132 +
8.133 + val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)
8.134 +(*
8.135 + NOTE ON IMPROVEMENT: one could do all subst + eval without Position.T and by ------ ^^^
8.136 + finally pair with bool (! the sequence of list items is NOT changed)
8.137 +*)
8.138 +(*+*)val [(true, (precond, pos))] = display
8.139 +(*+*)val "0 < r" = precond |> UnparseC.term @{context}
8.140 +
8.141 +val return_check_pos =
8.142 + (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
8.143 +:
8.144 +checked_TEST
8.145
8.146 (* final test ... ----------------------------------------------------------------------------*)
8.147 -val (false, (*230311: should become true ! TODO-----vvvvvvv substituted with \<open>r\<close> *)
8.148 - [(false, (*Pre_Conds.eval wrong, because of: ... *)
8.149 - Const ("Orderings.ord_class.less", _) $
8.150 - Const ("Groups.zero_class.zero", _) $ Free ("fixes", _))]) = return_check;
8.151 -(*\\------------------ test on old code (partially with Position.T) ------------------------//*)
8.152 -
8.153 -(*//------------------ build new code (with Position.T) ------------------------------------\\*)
8.154 - Pre_Conds.check_TEST ctxt where_rls where_POS;
8.155 -"~~~~~ fun check_TEST , args:"; val (ctxt, where_rls, preconds) =
8.156 - (ctxt, where_rls, where_POS);
8.157 -
8.158 -(*+*)val [(Const ("Orderings.ord_class.less", _) $
8.159 - Const ("Groups.zero_class.zero", _) $ Free ("r", _), _)] = where_POS
8.160 -
8.161 - val full_subst =
8.162 - map (fn (t, pos) => (subst_atomic env_eval t, pos)) where_POS
8.163 - val evals =
8.164 - map (fn (term, pos) => (Rewrite.eval_true ctxt [term] where_rls, (term, pos))) preconds
8.165 -(*+*)val [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
8.166 - Free ("r", _), _))] = evals
8.167 -
8.168 -(** )declare [[rewrite_trace = true]](**)
8.169 -val [(term, _)] = full_subst (*ERROR "true" with where_POS*);
8.170 -Rewrite.eval_true @{context} [term] where_rls (*true by code ERROR WN230329*)
8.171 -(**)declare [[rewrite_trace = false]]( **)
8.172 -
8.173 -val return_check_TEST =
8.174 - (foldl and_ (true, map fst evals), (map fst evals) ~~ preconds)
8.175 -(* final test ... ----------------------------------------------------------------------------*)
8.176 -val (true, [(true, (Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
8.177 - Free ("r", _), _))]) = return_check_TEST
8.178 +val (true, [(true, (Const ("Orderings.ord_class.less", _) $
8.179 + Const ("Groups.zero_class.zero", _) $ Free ("r", _), _))]) = return_check_pos
8.180 (*\\------------------ build new code (with Position.T) ------------------------------------//*)
9.1 --- a/test/Tools/isac/Test_Theory.thy Tue Aug 15 17:44:56 2023 +0200
9.2 +++ b/test/Tools/isac/Test_Theory.thy Thu Aug 17 08:01:45 2023 +0200
9.3 @@ -61,7 +61,8 @@
9.4 \<close> ML \<open>
9.5 \<close>
9.6
9.7 -section \<open>====="Minisubpbl/150a-add-given-Maximum.sml"=======================================\<close>
9.8 +section \<open>===================================================================================\<close>
9.9 +section \<open>=====maxi 150a-add-given-Maximum.sml ==============================================\<close>
9.10 ML \<open>
9.11 \<close> ML \<open>
9.12 (* Title: "Minisubpbl/150a-add-given-Maximum.sml"
9.13 @@ -265,7 +266,7 @@
9.14 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
9.15
9.16 \<close> ML \<open> (*//----------- adhoc inserted fun check_OLD ----------------------------------------\\*)
9.17 -(*//------------------ adhoc inserted fun check_OLD ----------------------------------------\\* )
9.18 +(*//------------------ adhoc inserted fun check_OLD ----------------------------------------\\*)
9.19
9.20 (*T_TESTold* )
9.21 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
9.22 @@ -463,20 +464,36 @@
9.23 check_OLD: Proof.context -> Rule_Def.rule_set -> term list -> Model_Pattern.T * I_Model.T_TEST ->
9.24 checked;
9.25
9.26 -fun check_envs_TEST ctxt where_rls pres (env_model, (env_subst, env_eval)) =
9.27 +\<close> ML \<open>
9.28 +\<close> ML \<open>
9.29 +(*T_TESTold*)
9.30 +fun check_from_store ctxt where_rls pres env_subst env_eval =
9.31 let
9.32 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.33 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.34 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
9.35 + val evals = map (eval ctxt where_rls) full_subst
9.36 + in
9.37 + (foldl and_ (true, map fst evals), pres_subst)
9.38 + end
9.39 +(*T_TEST*)
9.40 +fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
9.41 + let
9.42 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
9.43 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
9.44 val full_subst = if env_eval = [] then pres_subst_other
9.45 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
9.46 val evals = map (eval ctxt where_rls) full_subst
9.47 - in
9.48 + in
9.49 (foldl and_ (true, map fst evals), pres_subst_other)
9.50 - end
9.51 + end
9.52 ;
9.53 -check_envs_TEST: Proof.context -> Rule_Def.rule_set -> term list ->
9.54 - Env.T * (env_subst * env_eval) -> checked
9.55 -( *\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
9.56 + check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
9.57 + -> checked
9.58 +\<close> ML \<open>
9.59 +(*T_TESTnew*)
9.60 +\<close> ML \<open>
9.61 +\<close> ML \<open>
9.62 +(*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
9.63 \<close> ML \<open> (*\\----------- adhoc inserted fun check_OLD ----------------------------------------//*)
9.64 \<close> ML \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
9.65 val return_check_OLD =
9.66 @@ -1448,7 +1465,7 @@
9.67 \<close> ML \<open>
9.68 \<close>
9.69
9.70 -section \<open>===== "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" =================================\<close>
9.71 +section \<open>=====equa "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" =================================\<close>
9.72 ML \<open>
9.73 \<close> ML \<open>
9.74 (* Title: "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml"
9.75 @@ -1983,7 +2000,7 @@
9.76 \<close>
9.77
9.78
9.79 -section \<open>===== Interpret/li-tool.sml =======================================================\<close>
9.80 +section \<open>=====bieg Interpret/li-tool.sml =======================================================\<close>
9.81 ML \<open>
9.82 \<close> ML \<open>
9.83 (* Title: Interpret/li-tool.sml
9.84 @@ -2224,7 +2241,8 @@
9.85 (*+*)val 7 = length formals
9.86
9.87 \<close> ML \<open>
9.88 - val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
9.89 + val preconds =
9.90 + Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
9.91 \<close> ML \<open>
9.92 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
9.93 val ist = Istate.e_pstate
9.94 @@ -2250,8 +2268,7 @@
9.95 \<close> ML \<open>
9.96 \<close>
9.97
9.98 -section \<open>===================================================================================\<close>
9.99 -section \<open>===== refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ==================\<close>
9.100 +section \<open>=====eqsy refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ==================\<close>
9.101 ML \<open> (*\<longrightarrow> refine.sml*)
9.102 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
9.103 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
9.104 @@ -2435,7 +2452,7 @@
9.105 \<close>
9.106
9.107 section \<open>===================================================================================\<close>
9.108 -section \<open>===== me IntegrierenUndKonstanteBestimmen2 ALL ====================================\<close>
9.109 +section \<open>=====isa2 -> me IntegrierenUndKonstanteBestimmen2 ALL ====================================\<close>
9.110 ML \<open>
9.111 open Sub_Problem
9.112 \<close> ML \<open> (*\<rightarrow> biegelinie-4.sml OR NEW biegelinie-5.sml *)