(* Title:  Specify/i-model.sml

    Author: Walther Neuper 110226

    (c) due to copyright terms

 \<open>I_Model\<close> serves students' interactive modelling and gives feedback in the specify-phase.

 *)

 signature INTERACTION_MODEL =

 sig

   type T

   type T_TEST

   val OLD_to_TEST: T -> T_TEST

   val TEST_to_OLD: T_TEST -> T

   val empty: T

   val empty_TEST: T_TEST

   type single

   type single_TEST

   val empty_single: single

   val empty_single_TEST: single_TEST

   val is_empty_single_TEST: single_TEST -> bool

   type variant

   type variants

   type m_field

   type descriptor

   datatype feedback = datatype Model_Def.i_model_feedback

   datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST

   val feedback_empty_TEST: Model_Def.i_model_feedback_TEST

   type env

   type message

   val single_to_string: Proof.context -> single -> string

   val single_to_string_TEST: Proof.context -> single_TEST -> string

   val to_string: Proof.context -> T -> string

   val to_string_TEST: Proof.context -> T_TEST -> string

   val feedback_OLD_to_TEST: feedback -> feedback_TEST

   datatype add_single = Add of single | Err of string

   val init: Model_Pattern.T -> T

   val init_TEST: O_Model.T -> Model_Pattern.T -> T_TEST

   val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->

     TermC.as_string -> add_single

   val add_single: theory -> single -> T -> T

   val make_tactic: m_field -> TermC.as_string * T -> Tactic.T

   val descriptor: feedback -> descriptor

   val descriptor_TEST: feedback_TEST -> descriptor

   val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string

   val o_model_values: feedback -> O_Model.values

   val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list

   val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T

     -> message * single

   val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string

   val of_max_variant: Model_Pattern.T -> T_TEST ->

     (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)

 (*REN make_complete*)

   val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T

   val add: single -> T -> T

   val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T

   val is_error: feedback -> bool

 (*REN complete_internal*)

   val complete': Model_Pattern.T -> O_Model.single -> single

   val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST

   val is_complete: T -> bool

   val is_complete_variant: Model_Def.variant -> T_TEST-> bool

   val to_p_model: theory -> feedback -> string

 (*from isac_test for Minisubpbl*)

   val eq1: ''a -> 'b * (''a * 'c) -> bool

   val filter_outs: O_Model.T -> T -> O_Model.T

   val filter_outs_TEST: O_Model.T -> T_TEST -> O_Model.T

   val feedback_to_string: Proof.context -> feedback -> string

   val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string

   val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list -> 

     'a * 'b * bool * string * feedback

   val seek_ppc: int -> T -> single option

   val overwrite_ppc: theory -> single -> T -> T

 \<^isac_test>\<open>

   (**)

 \<close>

 end

 (**)

 structure I_Model(**) : INTERACTION_MODEL(**) =

 struct

 (**)

 (** data types **)

 type variant =  Model_Def.variant;

 type variants =  Model_Def.variants;

 type m_field = Model_Def.m_field;

 type descriptor = Model_Def.descriptor;

 type T = Model_Def.i_model_single list;

 (* for developing input from PIDE, we use T_TEST with these ideas:

   (1) the new structure is as close to old T, because we want to preserve the old tests

   (2) after development (with *_TEST) of essential parts of the Specification's semantics,

       we adapt the old tests to the new T_TEST

   (3) together with adaption of the tests we remove the *_TEST

 *)

 type T_TEST = Model_Def.i_model_single_TEST list;

 datatype feedback = datatype Model_Def.i_model_feedback;

 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;

 val feedback_empty_TEST = Model_Def.feedback_empty_TEST

 type single = Model_Def.i_model_single;

 type single_TEST = Model_Def.i_model_single_TEST;

 val empty_single = Model_Def.i_model_empty;

 val empty_single_TEST = Model_Def.i_model_empty_TEST;

 fun is_empty_single_TEST (0, [], false, "i_model_empty", _) = true

   | is_empty_single_TEST _ = false

 val empty = []: T;

 val empty_TEST = []: T_TEST;

 type env = Env.T

 fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST ((d, ts), penv)) 

   | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)

   | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)

   | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST ((d, ts), penv))

   | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))

   | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^

       (UnparseC.term (ContextC.for_ERROR ()) pid))

   | feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)

 fun OLD_to_TEST i_old =

   map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old

 fun feedback_TEST_to_OLD (Model_Def.Cor_TEST ((d, ts), penv)) = (Cor ((d, ts), penv))

   | feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)

   | feedback_TEST_to_OLD (Model_Def.Inc_TEST ((d, ts), penv)) = (Inc ((d, ts), penv))

   | feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))

 fun TEST_to_OLD i_model = 

   map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model

 type message = string;

 fun feedback_to_string ctxt (Cor ((d, ts), _)) = 

     "Cor " ^ UnparseC.term  ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"

   | feedback_to_string _ (Syn c) = "Syn " ^ c

   | feedback_to_string _ (Typ c) = "Typ " ^ c

   | feedback_to_string ctxt (Inc ((d, ts), _)) = 

     "Inc " ^ UnparseC.term  ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"

   | feedback_to_string ctxt (Sup (d, ts)) = 

     "Sup " ^ UnparseC.term  ctxt (Input_Descript.join (d, ts))

   | feedback_to_string ctxt (Mis (d, pid)) = 

     "Mis " ^ UnparseC.term  ctxt d ^ " " ^ UnparseC.term ctxt pid

   | feedback_to_string _ (Par s) = "Trm "^s;

 (**)

 fun feedback_TEST_to_string ctxt (Cor_TEST ((d, ts), _)) = 

     "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"

   | feedback_TEST_to_string _ (Syn_TEST c) =

     "Syn_TEST " ^ c

   | feedback_TEST_to_string ctxt (Inc_TEST ((d, []), _)) = 

     "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^ 

       Model_Pattern.empty_for d

   | feedback_TEST_to_string ctxt (Inc_TEST ((d, ts), _)) =

     "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"

   | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) = 

     "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))

 fun single_to_string ctxt (i, is, b, s, itm_) = 

   "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^

   s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";

 fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) = 

   "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^

   s ^ ", (" ^ feedback_TEST_to_string ctxt itm_ ^ ", Position.T))";

 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);

 fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);

 (** make a Tactic.T **)

 fun make_tactic m_field (term_as_string, i_model) =

   case m_field of

     "#Given" => Tactic.Add_Given' (term_as_string, i_model)

   | "#Find" => Tactic.Add_Find' (term_as_string, i_model)

   | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)

   | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);

 (** initialise a model **)

 fun init pbt = 

   let

     fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))

   in map pbt2itm pbt end

 (*

   Design decision:

 * Now the Model in Specification is intialised such that the placement of items can be

   maximally stable during interactive input to the Specification.

 * Template.show provides the initial output to the user and thus determines what will be parsed

   by Outer_Syntax later during interaction.

 * The relation between O_Model.T and I_Model.T becomes much simpler.

 *)

 (**)

 fun pat_to_item o_model (_, (descriptor, _)) =

   case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of

     NONE => raise ERROR "I_Model.pat_to_item_TEST with NONE"

   | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,

     (Inc_TEST ((descr, []), (descr, [])), Position.none))

 fun init_TEST o_model model_patt =

   let

     val pre_items = map (pat_to_item o_model) model_patt

   in

     O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))

   end

 (*/---------------- old code -----------------------------------------------------------------\*)

 fun o_model_values (Cor ((_, ts), _)) = ts

   | o_model_values (Syn _) = []

   | o_model_values (Typ _) = []

   | o_model_values (Inc ((_, ts), _)) = ts

   | o_model_values (Sup (_, ts)) = ts

   | o_model_values (Mis _) = []

   | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";

 val unique = Syntax.read_term\<^context> "UnIqE_tErM";

 fun descriptor (Cor ((d ,_), _)) = d

   | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)

   | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)

   | descriptor (Inc ((d, _), _)) = d

   | descriptor (Sup (d, _)) = d

   | descriptor (Mis (d, _)) = d

   | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";

 fun descriptor_TEST (Cor_TEST ((d ,_), _)) = d

   | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)

   | descriptor_TEST (Inc_TEST ((d, _), _)) = d

   | descriptor_TEST (Sup_TEST (d, _)) = d

 fun descr_pairs_to_string ctxt equal_descr_pairs =

 (map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)

     |> pair2str) equal_descr_pairs)

   |> strs2str'

 fun variables model_patt i_model =

   Pre_Conds.environment_TEST model_patt i_model

   |> map snd

 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";

 (* get a term from O_Model, notyet input in I_Model.

    the term from O_Model is thrown back to a string in order to reuse

    machinery for immediate input by the user. *)

 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =

   (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))

 (*update the itm_ already input, all..from ori*)

 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) = 

   let 

     val ts' = union op = (o_model_values itm_) ts;

     val pval = [Input_Descript.join'''' (d, ts')]

 	  (*WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc*)

     val complete = if eq_set op = (ts', all) then true else false

   in

     case itm_ of

       (Cor _) => 

         (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts')) 

 	       else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))

     | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)

     | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)

     | (Inc _) =>

       if complete

   	  then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))

   	  else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))

     | (Sup (d,ts')) => (*4.9.01 lost env*)

   	  (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))

   	  (*else (id,vt,complete,fd,Cor((d,ts'),e))*)

       (* 28.1.00: not completely clear ---^^^ etc.*)

     | (Mis _) => (* 4.9.01: Mis just copied *)

        if complete

   		 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))

   		 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))

     | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string (ContextC.for_ERROR ()) i)

   end

 (** find next step **)

 fun eq1 d (_, (d', _)) = (d = d')

 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_) 

 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =

   case find_first (eq1 d) pbt of

     SOME (_, (_, pid)) =>

       (case find_first (eq3 f d) itms of

         SOME (_, _, _, _, itm_) =>

           let val ts' = inter op = (o_model_values itm_) ts

           in 

             if subset op = (ts, ts') 

             then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)

 	          else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))

 	          end

 	    | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))

   | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))

 datatype add_single =

 	Add of single   (* return-value of check_single *)

 | Err of string   (* error-message                *)

 (*

   Create feedback for input of TermC.as_string to m_field;

   check w.r.t. O_Model.T and Model_Pattern.T.

   In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)

   check_single is extremely permissive.

 *)

 (*will come directly from PIDE -----------------vvvvvvvvvvv

   in case t comes from Step.specify_do_next -----------vvv = Position.none*)

 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =

     let

       val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)

     (*/------------ replace by ParseC.term_position -----------\*)

       val t = Syntax.read_term ctxt ct

         handle ERROR msg => error (msg (*^ Position.here pos*))

     (*\------------ replace by ParseC.term_position -----------/*)

         (*NONE => Add (i, [], false, m_field, Syn ct)*)

       val (d, ts) = Input_Descript.split t

     in 

       if d = TermC.empty then

         Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts)) 

       else

         (case find_first (eq1 d) m_patt of

           NONE => Add (i, [], true, m_field, Sup (d,ts))

         | SOME (f, (_, id)) =>

             let

               fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0

             in

               case find_first (eq2 d) i_model of

                 NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))

               | SOME (i', _, _, _, itm_) => 

                   if Input_Descript.for_list d then 

                     let

                       val in_itm = o_model_values itm_

                       val ts' = union op = ts in_itm

                       val i'' = if in_itm = [] then i else i'

                     in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end

                   else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))

             end)

     end

     (*for MethodC:   #undef  completed vvvvv vvvvvv term_as_string*)

     (*will come directly from PIDE ----------------------vvvvvvvvvvv*)

   | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =

     let

       val (t as (descriptor $ _)) = Syntax.read_term ctxt str

         handle ERROR msg => error (msg (*TODO: ^ Position.here pp*))

         (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)

     in 

         case Model_Pattern.get_field descriptor m_patt of

           NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^

             UnparseC.term ctxt descriptor ^ "\"")

         | SOME m_field' => 

           if m_field <> m_field' then

             Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^

              "\" not for field \"" ^ m_field ^ "\"")

           else

             case O_Model.contains ctxt m_field o_model t of

               ("", ori', all) => 

                 (case is_notyet_input ctxt i_model all ori' m_patt of

                    ("", itm) => Add itm

                  | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))

             | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)

     end

 (** add input **)

 fun overwrite_ppc thy itm model =

   let 

     fun repl _ (_, _, _, _, itm_) [] =

         raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_

           ^ " not found")

       | repl model' itm (p :: model) =

 	      if (#1 itm) = (#1 p)

 	      then model' @ [itm] @ model

 	      else repl (model' @ [p]) itm model

   in repl [] itm model end

 (*find_first item with #1 equal to id*)

 fun seek_ppc _ [] = NONE

   | seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model

 (* 10.3.00: insert the already compiled itm into model;

    ev. filter_out  untouched (in FE: (0,...)) item related to insert-item *)

 fun add_single thy itm model =

   let 

     fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)

       | eq_untouched _ _ = false

     val model' = case seek_ppc (#1 itm) model of

       SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)

     | NONE => (model @ [itm])

   in filter_out (eq_untouched ((descriptor o #5) itm)) model' end

 (** complete I_Model.T **)

 (*

   TODO: investigate dependencies between OLD funs (and reconsider (1..4)):

     OLD complete_method uses OLD complete

     ..

   Survey on completion of i-models. There are 2 internal cases and 2 interactive cases

   Internal cases

     (1) fill_both

       for internally automated specify-phase: fill both models from o_model

       TODO random number for selection from variants in o_model

         ? https://www.isa-afp.org/theories/executable_randomized_algorithms/#Dice_Roll.html

       used in Specify.finish_phase -- SubProblem,

         ?! Step_Specify.by_tactic Model_Problem ?!

 \<Longrightarrow> (2) fill_method (WAS complete, which allowed met_imod <> [])

       for skipping model of MethodC; assumes Problem (+Pre_Conds) is complete, MethodC#model = []

       used in LI.by_tactic Apply_Method'

         P_Spec.input_icalhd (will be dropped)

   Interactive cases: assume an interactive element activated by the user

     (3) complete_method_pos

       for interactive specify-phase in case of setting "skip modelling method"

       (needs NOT Problem.is_complete due to (4))

     (4) complete_pos

       for interactive specify-phase on Problem AND MethodC, Position.T for feedback

       used in TODO

   Divide functionality of I_Model.of_max_variant into parts in ordeer for re-use in is_complete

     I_Model.max_variants

       return variant list, because Problem#model might be insufficient to determine

       variant of MethodC.#model (FunctionVariable a ! b)

       + (Model_Pattern.single * I_Model.single) list for make_environments

       ^^NO: need ONLY max_variants

     Pre_Conds.make_environments

       takes above list

   Related

   Coordination with I_Model.is_complete:

     uses I_Model.max_variants, Pre_Conds.make_environments for Pre_Conds.check

     determines by use of both models independently (?)    

 *)

 fun complete' pbt (i, v, f, d, ts) =

   case \<^try>\<open> (i, v, true, f, Cor ((d, ts),

       ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)

     ))\<close> of

     SOME x => x

   | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))

 (*filter out oris which have same description in itms*)

 (* ---------------------------------- type problems ---vv---------vv

 fun filter_outs oris [] = oris

   | filter_outs oris (i::itms) = 

     let

       val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris

     in

       filter_outs ors itms

     end

 *)

 (*with types..*)

 (*T_TESTold*)

 fun filter_outs oris [] = oris

   | filter_outs oris (i::itms) = 

     let

       val ors = filter_out ((curry op = ((descriptor o 

         (#5: single -> feedback)) i)) o

         (#4: O_Model.single -> O_Model.descriptor)) oris

     in

       filter_outs ors itms

     end

 (*T_TEST*)

 fun filter_outs_TEST oris [] = oris

   | filter_outs_TEST oris (i::itms) = 

     let

       val ors = filter_out ((curry op = ((descriptor_TEST o 

         ((#1 o #5): single_TEST -> feedback_TEST) ) i) ) o

         (#4: O_Model.single -> O_Model.descriptor) ) oris

     in

       filter_outs_TEST ors itms

     end

 (*T_TESTnew*)

 (*filter oris which are in pbt, too*)

 fun filter_pbt oris pbt =

   let

     val dscs = map (fst o snd) pbt

   in

     filter ((member op= dscs) o (#4)) oris

   end

 fun is_error (Cor _) = false

   | is_error (Sup _) = false

   | is_error (Inc _) = false

   | is_error (Mis _) = false

   | is_error _ = true

 (*create output-string for itm*)

 fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))

   | to_p_model _ (Syn c) = c

   | to_p_model _ (Typ c) = c

   | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))

   | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))

   | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid

   | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"

 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)

 (* insert_ppc = add for appl_add', input_icalhd 11.03,

    handles superfluous items carelessly                       *)

 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)

 (*combine itms from pbl + met and complete them wrt. pbt*)

 (* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)

 fun complete oris pits mits met = 

   let

     val vat = Pre_Conds.max_variant pits;

     val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)

     val ors = filter ((member_swap op= vat) o (#2)) oris

     val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)

   in

     itms @ (map (complete' met) os)

   end

 (**)

 (*T_TESTold*)

 (*complete model and guard of a calc-head*)

 fun complete_method (oris, mpc, model, probl) =

   let

     val pits = filter_out ((curry op= false) o (#3)) probl

     val vat = if probl = [] then 1 else Pre_Conds.max_variant probl

     val pors = filter ((member_swap op = vat) o (#2)) oris

     val pors = filter_outs pors pits (*which are in pbl already*)

     val pors = (filter_pbt pors model) (*which are in pbt, too*)

     val pits = pits @ (map (complete' model) pors)

     val mits = complete oris pits [] mpc

   in (pits, mits) end

 (*T_TEST*)

 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^

   "variants " ^ ints2str' vnts ^ " and descriptor " ^

   (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))

 fun fill_method o_model pbl_imod met_patt =

   let

     val (pbl_max_vnts, _) = Pre_Conds.max_variants met_patt pbl_imod;

     val from_pbl = map (fn (_, (descr, _)) =>

       Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt

     val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

       if is_empty_single_TEST i_single

       then

         case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of

           NONE => raise ERROR (msg pbl_max_vnts feedb)

         | SOME (i, vnts, m_field, descr, ts) =>

           (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))

       else i_single (*fetched before from pbl_imod*))) from_pbl

   in

     from_o_model

   end

 (*T_TESTnew*)

 (*TODO: also check if all elements are I_Model.Cor*)

 fun is_complete ([]: T) = false

   | is_complete itms = foldl and_ (true, (map #3 itms))

 (*for PIDE: are all feedback Cor ? MISSING: Pre_Conds.check *)

 fun is_complete_variant no_model_items i_model =

   no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) =>  true | _ => false) i_model)

 val of_max_variant = Pre_Conds.of_max_variant

 (**)end(**);