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