1.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml	Mon Sep 18 08:38:33 2023 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml	Mon Sep 18 10:26:35 2023 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5    type variant
     1.6    type variants
     1.7 +
     1.8    type m_field = Model_Pattern.m_field
     1.9    type descriptor = Model_Pattern.descriptor
    1.10    type values
    1.11 @@ -45,6 +46,18 @@
    1.12  
    1.13    val i_model_empty : i_model_single
    1.14    val i_model_empty_TEST: i_model_single_TEST
    1.15 +
    1.16 +  val max_variants: i_model_TEST -> variant list * i_model_TEST list
    1.17 +
    1.18 +(*from isac_test for Minisubpbl*)
    1.19 +  val filter_variants': i_model_TEST -> variant -> i_model_TEST
    1.20 +  val cnt_corrects: i_model_TEST -> int
    1.21 +  val arrange_args: int list -> int * variant list -> (int * variant) list
    1.22 +
    1.23 +\<^isac_test>\<open>
    1.24 +(**)
    1.25 +\<close>
    1.26 +
    1.27  end
    1.28  
    1.29  (**)                   
    1.30 @@ -66,25 +79,6 @@
    1.31  type variants = variant list; (* variants given by Formalise.T *)
    1.32  type values = term list;
    1.33  
    1.34 -(** definitions for O_Model.T **)
    1.35 -
    1.36 -type o_model_single =
    1.37 -  (int *       (* sequence of input, 0 = untouched, drop with PIDE *)
    1.38 -	variants *   (* pointers to variants given in Formalise.T        *)
    1.39 -	m_field *    (* #Given | #Find | #Relate + TODO: #Where          *)
    1.40 -	descriptor * (* see Input_Descript.thy                           *)
    1.41 -	values       (* isalist2list t | [t]: the values of in item      *)
    1.42 -	);
    1.43 -type o_model = o_model_single list;  
    1.44 -val o_model_empty = (0, [], "", TermC.empty, [TermC.empty]) : o_model_single;
    1.45 -
    1.46 -fun o_model_single_to_string ctxt (i, vs, fi, t, ts) = 
    1.47 -  "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
    1.48 -  UnparseC.term ctxt t ^ ", " ^ (strs2str o (map (UnparseC.term ctxt))) ts ^ ")";
    1.49 -fun o_model_to_string ctxt o_model =
    1.50 -  (strs2str' o (map (linefeed o (o_model_single_to_string ctxt)))) o_model;
    1.51 -
    1.52 -
    1.53  (** definitions for I_Model.T **)
    1.54  
    1.55  datatype i_model_feedback = 
    1.56 @@ -137,4 +131,58 @@
    1.57  val i_model_empty = (0, [], false, "i_model_empty", Syn "i_model_empty");
    1.58  val i_model_empty_TEST = (0, [], false, "i_model_empty", (feedback_empty_TEST, Position.none));
    1.59  
    1.60 +
    1.61 +(** max_variants **)
    1.62 +
    1.63 +fun filter_variants' i_singles n = 
    1.64 +  filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
    1.65 +fun cnt_corrects i_model = 
    1.66 +  fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
    1.67 +fun arrange_args [] _ = []
    1.68 +  | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all)) 
    1.69 +
    1.70 +fun max_variants i_model =
    1.71 +    let
    1.72 +      val all_variants =
    1.73 +          map (fn (_, variants, _, _, _) => variants) i_model
    1.74 +          |> flat
    1.75 +          |> distinct op =
    1.76 +      val variants_separated = map (filter_variants' i_model) all_variants
    1.77 +      val sums_corr = map (cnt_corrects) variants_separated
    1.78 +      val sum_variant_s = arrange_args sums_corr (1, all_variants)
    1.79 +
    1.80 +      val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
    1.81 +      val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
    1.82 +        |> map snd
    1.83 +      val option_sequence = map 
    1.84 +        (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
    1.85 +(*THAT IS NONSENSE, SEE Test_Theory (*+*)if (pbl_max_imos*)
    1.86 +      val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
    1.87 +            if is_some pos_in_sum_variant_s then i_model else [])
    1.88 +          (option_sequence ~~ variants_separated)
    1.89 +        |> filter_out (fn place_holder => place_holder = []);
    1.90 +    in
    1.91 +      (maxes, max_i_models)
    1.92 +    end 
    1.93 +
    1.94 +
    1.95 +(** definitions for O_Model.T **)
    1.96 +
    1.97 +type o_model_single =
    1.98 +  (int *       (* sequence of input, 0 = untouched, drop with PIDE *)
    1.99 +	variants *   (* pointers to variants given in Formalise.T        *)
   1.100 +	m_field *    (* #Given | #Find | #Relate + TODO: #Where          *)
   1.101 +	descriptor * (* see Input_Descript.thy                           *)
   1.102 +	values       (* isalist2list t | [t]: the values of in item      *)
   1.103 +	);
   1.104 +type o_model = o_model_single list;  
   1.105 +val o_model_empty = (0, [], "", TermC.empty, [TermC.empty]) : o_model_single;
   1.106 +
   1.107 +fun o_model_single_to_string ctxt (i, vs, fi, t, ts) = 
   1.108 +  "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
   1.109 +  UnparseC.term ctxt t ^ ", " ^ (strs2str o (map (UnparseC.term ctxt))) ts ^ ")";
   1.110 +fun o_model_to_string ctxt o_model =
   1.111 +  (strs2str' o (map (linefeed o (o_model_single_to_string ctxt)))) o_model;
   1.112 +
   1.113 +
   1.114  (**)end(**)

     2.1 --- a/src/Tools/isac/Specify/i-model.sml	Mon Sep 18 08:38:33 2023 +0200
     2.2 +++ b/src/Tools/isac/Specify/i-model.sml	Mon Sep 18 10:26:35 2023 +0200
     2.3 @@ -553,7 +553,7 @@
     2.4    (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
     2.5  fun fill_method o_model pbl_imod met_patt =
     2.6    let
     2.7 -    val (pbl_max_vnts, _) = Pre_Conds.max_variants met_patt pbl_imod;
     2.8 +    val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
     2.9      val from_pbl = map (fn (_, (descr, _)) =>
    2.10        Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
    2.11      val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

     3.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Mon Sep 18 08:38:33 2023 +0200
     3.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Mon Sep 18 10:26:35 2023 +0200
     3.3 @@ -23,8 +23,6 @@
     3.4  
     3.5    val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
     3.6         (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
     3.7 -  val max_variants: Model_Pattern.T -> Model_Def.i_model_TEST ->
     3.8 -       ( Model_Def.variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*)
     3.9    val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
    3.10      ((term * term) * (term * term)) list
    3.11  
    3.12 @@ -40,9 +38,6 @@
    3.13      (Model_Pattern.single * Model_Def.i_model_single_TEST) list
    3.14    val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
    3.15  
    3.16 -  val arrange_args: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
    3.17 -  val cnt_corrects: Model_Def.i_model_TEST -> int
    3.18 -
    3.19    val all_lhs_atoms: term list -> bool
    3.20    val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
    3.21    val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
    3.22 @@ -253,20 +248,6 @@
    3.23    map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
    3.24    |> flat
    3.25  
    3.26 -(*  filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST*)
    3.27 -fun filter_variants' i_singles n = 
    3.28 -  filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
    3.29 -(*arrange_args: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)
    3.30 -fun arrange_args [] _ = []
    3.31 -  | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all)) 
    3.32 -(*cnt_corrects: I_Model.T_TEST -> int*)
    3.33 -fun cnt_corrects i_model = 
    3.34 -  fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
    3.35 -
    3.36 -(*get data wrt. maximal variant; NO Pre_Conds.check
    3.37 -  TODO: separate determining i_model(s!) with max_variant from creating environments;
    3.38 -    single i_model with max_variant can ONLY be determined Problem.mode + MethodC.model together.
    3.39 -*)
    3.40  (*T_TESTold*)
    3.41  fun of_max_variant _ [] = ((false, 0, []), [], ([], []))
    3.42    | of_max_variant model_patt i_model =
    3.43 @@ -292,7 +273,7 @@
    3.44          = length model_patt, max_variant, i_model_max),
    3.45        env_model, (env_subst, env_eval))
    3.46    end
    3.47 -(*T_TEST*)
    3.48 +(*T_TEST* \<longrightarrow> Model_Def)
    3.49  fun max_variants model_patt i_model =
    3.50      let
    3.51        val all_variants =
    3.52 @@ -308,7 +289,7 @@
    3.53          |> map snd
    3.54        val option_sequence = map 
    3.55          (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
    3.56 -(*das ist UNSINN .., siehe (*+*)if (pbl_max_imos*)
    3.57 +(*THAT IS NONSENSE, SEE Test_Theory (*+*)if (pbl_max_imos*)
    3.58        val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
    3.59              if is_some pos_in_sum_variant_s then i_model else [])
    3.60            (option_sequence ~~ variants_separated)
    3.61 @@ -339,13 +320,7 @@
    3.62                               (env_model, (env_subst, env_eval)
    3.63  ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
    3.64      end 
    3.65 -(*T_TESTnew*)
    3.66 -
    3.67 -(*T_TESTold*)
    3.68 -(*T_TEST*)
    3.69 -(*T_TESTnew*)
    3.70 -
    3.71 -
    3.72 +( *T_TESTnew*)
    3.73  
    3.74  
    3.75  (*extract the environment from an I_Model.of_max_variant*)

     4.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Mon Sep 18 08:38:33 2023 +0200
     4.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Mon Sep 18 10:26:35 2023 +0200
     4.3 @@ -174,8 +174,8 @@
     4.4          |> flat
     4.5          |> distinct op =
     4.6      val variants_separated = map (filter_variants' i_model) all_variants
     4.7 -    val sums_corr = map (cnt_corrects) variants_separated
     4.8 -    val sum_variant_s = arrange_args sums_corr (1, all_variants)
     4.9 +    val sums_corr = map (Model_Def.cnt_corrects) variants_separated
    4.10 +    val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
    4.11  (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
    4.12      val (_, max_variant) = hd (*..crude decision, up to improvement *)
    4.13        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
    4.14 @@ -564,8 +564,8 @@
    4.15          |> flat
    4.16          |> distinct op =
    4.17      val variants_separated = map (filter_variants' i_model) all_variants
    4.18 -    val sums_corr = map (cnt_corrects) variants_separated
    4.19 -    val sum_variant_s = arrange_args sums_corr (1, all_variants)
    4.20 +    val sums_corr = map (Model_Def.cnt_corrects) variants_separated
    4.21 +    val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
    4.22      val (_, max_variant) = hd (*..crude decision, up to improvement *)
    4.23        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
    4.24      val i_model_max =

     5.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Mon Sep 18 08:38:33 2023 +0200
     5.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Mon Sep 18 10:26:35 2023 +0200
     5.3 @@ -116,8 +116,8 @@
     5.4          |> flat
     5.5          |> distinct op =
     5.6      val variants_separated = map (filter_variants' i_model) all_variants
     5.7 -    val sums_corr = map (cnt_corrects) variants_separated
     5.8 -    val sum_variant_s = arrange_args sums_corr (1, all_variants)
     5.9 +    val sums_corr = map (Model_Def.cnt_corrects) variants_separated
    5.10 +    val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
    5.11      val (_, max_variant) = hd (*..crude decision, up to improvement *)
    5.12        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
    5.13      val i_model_max =

     6.1 --- a/test/Tools/isac/Test_Theory.thy	Mon Sep 18 08:38:33 2023 +0200
     6.2 +++ b/test/Tools/isac/Test_Theory.thy	Mon Sep 18 10:26:35 2023 +0200
     6.3 @@ -71,7 +71,7 @@
     6.4  (**)open I_Model(**)
     6.5  \<close> ML \<open>
     6.6  \<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*)
     6.7 -fun max_variants model_patt i_model =
     6.8 +fun max_variants i_model =
     6.9      let
    6.10        val all_variants =
    6.11            map (fn (_, variants, _, _, _) => variants) i_model
    6.12 @@ -118,7 +118,7 @@
    6.13  ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
    6.14      end 
    6.15  ;
    6.16 -max_variants: Model_Pattern.T -> Model_Def.i_model_TEST ->
    6.17 +max_variants: Model_Def.i_model_TEST ->
    6.18         (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*)
    6.19  \<close> ML \<open>
    6.20  \<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*)
    6.21 @@ -176,7 +176,7 @@
    6.22  \<close> ML \<open>
    6.23  fun fill_method o_model pbl_imod met_patt =
    6.24    let
    6.25 -    val (pbl_max_vnts, _) = max_variants met_patt pbl_imod;
    6.26 +    val (pbl_max_vnts, _) = max_variants pbl_imod;
    6.27      val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
    6.28      val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
    6.29        if is_empty_single_TEST i_single
    6.30 @@ -1188,7 +1188,7 @@
    6.31  (*new below step into*)
    6.32  
    6.33  val return_max_variants =
    6.34 -(*I_Model.*)max_variants met_patt pbl_imod;
    6.35 +(*I_Model.*)max_variants pbl_imod;
    6.36  \<close> ML \<open> (*////--------- step into max_variants ----------------------------------------------\\*)
    6.37  (*////---------------- step into max_variants ----------------------------------------------\\*)
    6.38  "~~~~~ fun max_variants , args:"; val (model_patt, i_model) = (pbl_patt, pbl_imod);
    6.39 @@ -1267,7 +1267,7 @@
    6.40  \<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*)
    6.41  (*|||----------------- continue fill_method --------------------------------------------------*)
    6.42  \<close> ML \<open>
    6.43 -      val (pbl_max_vnts, pbl_max_imos) = (*I_Model.*)max_variants pbl_patt pbl_imod
    6.44 +      val (pbl_max_vnts, pbl_max_imos) = (*I_Model.*)max_variants  pbl_imod
    6.45  ;
    6.46  (*+*)val [2, 1] = pbl_max_vnts;
    6.47  (*-------pbl_max_imos is NONSENSE (*+*)if (pbl_max_imos ..*)