1.1 --- a/src/Tools/isac/Specify/i-model.sml	Tue Sep 26 15:57:12 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Wed Sep 27 12:17:44 2023 +0200
     1.3 @@ -62,18 +62,10 @@
     1.4      (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
     1.5  
     1.6    val add: single -> T -> T
     1.7 -(**)
     1.8    val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
     1.9      T_TEST * T_TEST
    1.10 -(** )
    1.11 -  val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
    1.12 -  val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
    1.13 -( **)
    1.14 -  val complete': Model_Pattern.T -> O_Model.single -> single
    1.15 -(*^^^--- s_make_complete SHALL REPLACE ALL THESE*)
    1.16  
    1.17    val is_error: feedback -> bool
    1.18 -
    1.19    val is_complete: T -> bool
    1.20    val is_complete_variant: Model_Def.variant -> T_TEST-> bool
    1.21    val to_p_model: theory -> feedback -> string
    1.22 @@ -475,14 +467,6 @@
    1.23      end
    1.24  (*T_TESTnew*)
    1.25  
    1.26 -(*filter oris which are in pbt, too*)
    1.27 -fun filter_pbt oris pbt =
    1.28 -  let
    1.29 -    val dscs = map (fst o snd) pbt
    1.30 -  in
    1.31 -    filter ((member op= dscs) o (#4)) oris
    1.32 -  end
    1.33 -
    1.34  fun is_error (Cor _) = false
    1.35    | is_error (Sup _) = false
    1.36    | is_error (Inc _) = false
    1.37 @@ -504,54 +488,6 @@
    1.38     handles superfluous items carelessly                       *)
    1.39  fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
    1.40  
    1.41 -(*combine itms from pbl + met and complete them wrt. pbt*)
    1.42 -(* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
    1.43 -fun complete oris pits mits met = 
    1.44 -  let
    1.45 -    val vat = Pre_Conds.max_variant pits;
    1.46 -    val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
    1.47 -    val ors = filter ((member_swap op= vat) o (#2)) oris
    1.48 -    val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
    1.49 -  in
    1.50 -    itms @ (map (complete' met) os)
    1.51 -  end
    1.52 -(**)
    1.53 -
    1.54 -(*T_TESTold*)
    1.55 -(*complete model and guard of a calc-head*)
    1.56 -fun complete_method (oris, mpc, model, probl) =
    1.57 -  let
    1.58 -    val pits = filter_out ((curry op= false) o (#3)) probl
    1.59 -    val vat = if probl = [] then 1 else Pre_Conds.max_variant probl
    1.60 -    val pors = filter ((member_swap op = vat) o (#2)) oris
    1.61 -    val pors = filter_outs pors pits (*which are in pbl already*)
    1.62 -    val pors = (filter_pbt pors model) (*which are in pbt, too*)
    1.63 -    val pits = pits @ (map (complete' model) pors)
    1.64 -    val mits = complete oris pits [] mpc
    1.65 -  in (pits, mits) end
    1.66 -(*T_TEST*)
    1.67 -fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
    1.68 -  "variants " ^ ints2str' vnts ^ " and descriptor " ^
    1.69 -  (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
    1.70 -fun transfer_terms (i, vnts, m_field, descr, ts) =
    1.71 -  (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
    1.72 -fun fill_method o_model pbl_imod met_patt =
    1.73 -  let
    1.74 -    val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
    1.75 -    val from_pbl = map (fn (_, (descr, _)) =>
    1.76 -      Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
    1.77 -    val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
    1.78 -      if is_empty_single_TEST i_single
    1.79 -      then
    1.80 -        case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
    1.81 -            [] => raise ERROR (msg pbl_max_vnts feedb)
    1.82 -          | o_singles => map transfer_terms o_singles
    1.83 -      else [i_single (*fetched before from pbl_imod*)])) from_pbl
    1.84 -  in
    1.85 -    from_o_model |> flat
    1.86 -  end
    1.87 -(*T_TESTnew*)
    1.88 -
    1.89  (*TODO: also check if all elements are I_Model.Cor*)
    1.90  fun is_complete ([]: T) = false
    1.91    | is_complete itms = foldl and_ (true, (map #3 itms))
    1.92 @@ -562,6 +498,11 @@
    1.93  
    1.94  val of_max_variant = Pre_Conds.of_max_variant
    1.95  
    1.96 +fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
    1.97 +  "variants " ^ ints2str' vnts ^ " and descriptor " ^
    1.98 +  (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
    1.99 +fun transfer_terms (i, vnts, m_field, descr, ts) =
   1.100 +  (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
   1.101  fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
   1.102    let
   1.103      val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;