1.1 --- a/src/Tools/isac/Specify/i-model.sml	Mon Sep 18 10:26:35 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Wed Sep 20 08:27:21 2023 +0200
     1.3 @@ -413,29 +413,11 @@
     1.4  (** complete I_Model.T **)
     1.5  
     1.6  (*
     1.7 -  TODO: investigate dependencies between OLD funs (and reconsider (1..4)):
     1.8 -    OLD complete_method uses OLD complete
     1.9 -    ..
    1.10 -  
    1.11 -  Survey on completion of i-models. There are 2 internal cases and 2 interactive cases
    1.12 -  Internal cases
    1.13 -    (1) fill_both
    1.14 -      for internally automated specify-phase: fill both models from o_model
    1.15 -      TODO random number for selection from variants in o_model
    1.16 -        ? https://www.isa-afp.org/theories/executable_randomized_algorithms/#Dice_Roll.html
    1.17 -      used in Specify.finish_phase -- SubProblem,
    1.18 -        ?! Step_Specify.by_tactic Model_Problem ?!
    1.19 -\<Longrightarrow> (2) fill_method (WAS complete, which allowed met_imod <> [])
    1.20 -      for skipping model of MethodC; assumes Problem (+Pre_Conds) is complete, MethodC#model = []
    1.21 -      used in LI.by_tactic Apply_Method'
    1.22 -        P_Spec.input_icalhd (will be dropped)
    1.23 -  Interactive cases: assume an interactive element activated by the user
    1.24 -    (3) complete_method_pos
    1.25 -      for interactive specify-phase in case of setting "skip modelling method"
    1.26 -      (needs NOT Problem.is_complete due to (4))
    1.27 -    (4) complete_pos
    1.28 -      for interactive specify-phase on Problem AND MethodC, Position.T for feedback
    1.29 -      used in TODO
    1.30 +  Survey on completion of i-models. There are 2 cases:
    1.31 +  (1) the most general case covering allmost all others:
    1.32 +    I_Model.s_complete: transfer ideas from fill_method
    1.33 +  (2) case for refinement
    1.34 +    TODO: check old code
    1.35  
    1.36    Divide functionality of I_Model.of_max_variant into parts in ordeer for re-use in is_complete
    1.37      I_Model.max_variants
    1.38 @@ -446,8 +428,6 @@
    1.39      Pre_Conds.make_environments
    1.40        takes above list
    1.41  
    1.42 -  Related
    1.43 -
    1.44    Coordination with I_Model.is_complete:
    1.45      uses I_Model.max_variants, Pre_Conds.make_environments for Pre_Conds.check
    1.46      determines by use of both models independently (?)    
    1.47 @@ -551,6 +531,8 @@
    1.48  fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
    1.49    "variants " ^ ints2str' vnts ^ " and descriptor " ^
    1.50    (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
    1.51 +fun transfer_terms (i, vnts, m_field, descr, ts) =
    1.52 +  (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
    1.53  fun fill_method o_model pbl_imod met_patt =
    1.54    let
    1.55      val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
    1.56 @@ -560,12 +542,11 @@
    1.57        if is_empty_single_TEST i_single
    1.58        then
    1.59          case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
    1.60 -          NONE => raise ERROR (msg pbl_max_vnts feedb)
    1.61 -        | SOME (i, vnts, m_field, descr, ts) =>
    1.62 -          (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
    1.63 -      else i_single (*fetched before from pbl_imod*))) from_pbl
    1.64 +            [] => raise ERROR (msg pbl_max_vnts feedb)
    1.65 +          | o_singles => map transfer_terms o_singles
    1.66 +      else [i_single (*fetched before from pbl_imod*)])) from_pbl
    1.67    in
    1.68 -    from_o_model
    1.69 +    from_o_model |> flat
    1.70    end
    1.71  (*T_TESTnew*)
    1.72  

     2.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Mon Sep 18 10:26:35 2023 +0200
     2.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Wed Sep 20 08:27:21 2023 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4    val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model_TEST ->
     2.5      Model_Def.i_model_single_TEST
     2.6    val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T ->
     2.7 -    O_Model.single option
     2.8 +    O_Model.T
     2.9  
    2.10  \<^isac_test>\<open>
    2.11  (**)
    2.12 @@ -165,9 +165,9 @@
    2.13      val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
    2.14        | SOME descr' => if descr = descr' then true else false) i_model 
    2.15    in
    2.16 -    case find_first (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
    2.17 -      SOME item => item
    2.18 -    | NONE => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
    2.19 +    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
    2.20 +      [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
    2.21 +    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
    2.22    end
    2.23  (*
    2.24    get an appropriate (description, variant) item from o_model;
    2.25 @@ -175,7 +175,7 @@
    2.26    (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
    2.27  *)
    2.28  fun get_descr_vnt' feedb vnts o_model =
    2.29 -find_first (fn (_, vnts', _, descr', _) =>
    2.30 +  filter (fn (_, vnts', _, descr', _) =>
    2.31      case get_dscr' feedb of
    2.32        SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
    2.33      | NONE => false) o_model