(* 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

   val empty: T

   type single

   val empty_single: single

   val is_empty_single: single -> bool

   type variant

   type variants

   type m_field

   type descriptor

   type values

   datatype feedback = datatype Model_Def.i_model_feedback

   val feedback_empty: Model_Def.i_model_feedback

   type env

   type message

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

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

   datatype add_single = Add of single | Err of string

   val init: Proof.context -> O_Model.T -> Model_Pattern.T -> T

   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 get_values: T -> values list

   val feedb_values: feedback -> values

   val order_by_patt:  Model_Pattern.T -> T ->T

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

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

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

     Model_Pattern.T -> message * single

   val fill_from_o: O_Model.T -> single -> single option

   val add_other: variant -> T -> single -> single

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

   val s_make_complete: Proof.context ->  O_Model.T -> T * T -> Problem.id * MethodC.id ->

     T * T

   val s_are_complete: Proof.context -> O_Model.T -> T * T -> Problem.id * MethodC.id -> bool

   val is_error: feedback -> bool

   val to_p_model: theory -> feedback -> string

 (*/----- from isac_test for Minisubpbl*)

   val msg: variants -> feedback -> string

   val transfer_terms: O_Model.single -> single

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

   val descr_vals_to_string: Proof.context -> descriptor * values -> string

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

   val single_from_o: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single

   val seek_ppc: int -> single list -> single option

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

 (*\----- from isac_test for Minisubpbl*)

 \<^isac_test>\<open>

   (*copy "from isac_test for Minisubpbl" here*)

 \<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 values = Model_Def.values

 type T = Model_Def.i_model_single list;

 datatype feedback = datatype Model_Def.i_model_feedback;

 val feedback_empty = Model_Def.feedback_empty

 type single = Model_Def.i_model_single;

 val empty_single = Model_Def.i_model_empty;

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

   | is_empty_single _ = false

 val empty = []: T;

 type env = Env.T

 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 ctxt (Inc (d, [])) = 

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

       Model_Pattern.empty_for d

   | 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))

 fun descr_vals_to_string ctxt (descr, values) =

   UnparseC.term ctxt (descr $ Model_Def.values_to_present values)

 (*prepare for presentation to user; thus Syn does NOT raise an exn*)

 fun feedb_args_to_string ctxt (Cor (descr, values)) =

     UnparseC.term ctxt (descr $ Model_Def.values_to_present values)

   | feedb_args_to_string _ (Syn str) = str

   | feedb_args_to_string ctxt (Inc (descr, [])) =

     UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr

   | feedb_args_to_string ctxt (Inc (descr, values)) =

     UnparseC.term ctxt (descr $ Model_Def.values_to_present values)

   | feedb_args_to_string ctxt (Sup (descr, values)) =

     UnparseC.term ctxt (descr $ Model_Def.values_to_present values)

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

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

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

 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string 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 **)

 (*

   NEW 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 patt_to_item ctxt o_model (_, (descriptor, _)) =

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

     NONE => raise ERROR ("I_Model.patt_to_item NONE for " ^ UnparseC.term ctxt descriptor)

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

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

 fun init ctxt o_model model_patt =

   let

     val pre_items = map (patt_to_item ctxt o_model) model_patt

   in

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

   end

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

 (*DANGEROUS: do NOT use "UnIqE_tErM" *)

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

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

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

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

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

   | feedb_values (Syn _) = raise ERROR "feedb_values NOT for Syn"

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

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

 (*assumption: i_model has filtered max_vnt*)

 local

  fun order_by_pa i_model (_, (descr, _ )) =

    case find_first (fn (_, _, _, _, (feedb, _)) => descr = descriptor feedb) i_model of

      SOME i_single => [i_single]

    | NONE => []

 in

   fun order_by_patt model_patt i_model = model_patt |> map (order_by_pa i_model) |> flat

 end

 fun feedb_vals (Cor (_, ts)) = [ts]

   | feedb_vals (Syn _) = []

   | feedb_vals (Inc (_, ts)) = [ts]

   | feedb_vals (Sup (_, ts)) = [ts]

 fun get_values i_model =

   map (fn (_, _, _, _, (feedb, _)) => feedb_vals feedb) i_model

   |> flat

 fun descr_pairs_to_string ctxt equal_descr_pairs =

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

     |> pair2str) equal_descr_pairs)

   |> strs2str'

 fun variables model_patt i_model =

   Pre_Conds.environment model_patt i_model

   |> map snd

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

 fun single_from_o (feedb:feedback) _ all (id, vt, fd, d, ts) = 

   let 

     val ts' = union op = (feedb_values feedb) ts;

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

   in

     case feedb of

       Cor _ => if fd = "#undef"

       then (id, vt, complete, fd, (Sup (d, ts'), Position.none))

 	    else (id, vt, complete, fd, (Cor (d, ts'), Position.none))

     | Inc _ => if complete

   	  then (id, vt, true,  fd, (Cor (d, ts'), Position.none))

   	  else (id, vt, false, fd, (Inc (d, ts'), Position.none))

     | Sup (d, ts') =>

   	  (id, vt, complete, fd, (Sup (d, ts'), Position.none))

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

   end

 (** find next step **)

 (*old code kept for test/*)

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

   case find_first (fn (_, (d', _)) => d = d') pbt of

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

       (case find_first (fn (_, _, _, f', (feedb, _)) =>

           f = f' andalso d = (descriptor feedb)) itms of

         SOME (_, _, _, _, (feedb, _)) =>

           let

             val ts' = inter op = (feedb_values feedb) ts

           in

             if subset op = (ts, ts') 

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

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

 	        end

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

   | NONE => ("", single_from_o (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 .. *)

         (case find_first (fn (_, (d', _)) => d = d') m_patt of

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

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

           case find_first (fn (i, _, _, _, (feedb, _)) => d = (descriptor feedb) andalso i <> 0) i_model of

             NONE =>

               Add (i, [], true, f, (Cor (d, ts), Position.none))

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

             if Input_Descript.for_list d then 

               let

                 val in_itm = feedb_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'), Position.none)) end

             else Add (i', [], true, f, (Cor (d, ts), Position.none)))

     end

     (*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 parsed 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 #1 o #5) itm)) model' end

 (** complete I_Model.T **)

 fun s_are_complete _ _ ([], _) _ = false

   | s_are_complete _ _ (_, []) _ = false

   | s_are_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =

   let

     val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod

     val met_max_vnts = Model_Def.max_variants o_model met_imod

     val max_vnts = inter op= pbl_max_vnts met_max_vnts

     val max_vnt = if max_vnts = []

       then raise ERROR "I_Model.s_are_complete: request user to review met_imod"

       else hd max_vnts

     val (pbl_imod', met_imod') = (

       filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) pbl_imod,

       filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) met_imod)

     val (pbl_check, _) = Pre_Conds.check_internal ctxt pbl_imod' (Pos.Pbl, pbl_id)

     val (met_check, _) = Pre_Conds.check_internal ctxt met_imod' (Pos.Met, met_id)

   in

     pbl_check andalso met_check

   end

 fun is_error (Cor _) = false

   | is_error (Sup _) = false

   | is_error (Inc _) = false

   | is_error (Syn _) = 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 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))

 fun fill_from_o o_model (i, vnts, bool, _, (feedb, pos)) = 

   let

     val (m_field, all_values) =

       case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of

         SOME (_, _, m_field, _, ts) =>  (m_field, ts)

       | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"

     val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)

   in

 (*---------------vvvvvvvvvvvvv MV if TermC.is_list all_value-----*)

     if Model_Def.is_list_descr descr

     then

       let

         val already_input = feedb |> feedb_values

         val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)

         val ts = already_input @ [hd miss]

       in

         if length all_values = length ts

         then SOME (i, vnts, bool, m_field, (Cor (descr, [Model_Def.values_to_present ts]), pos))

         else SOME (i, vnts, bool, m_field, (Inc (descr, [Model_Def.values_to_present ts]), pos))

       end

     else SOME (i, vnts, bool, m_field, (Cor (descr, all_values(*only 1 term*)), pos))

   end

 (*

   in case there is an item in i2_model(= met) with Sup, 

   find_first an appropriate (variant, descriptor) item in i1_model(= pbl) and add it instead Sup,

   otherwise keep the items of i2_model.

 *)

 fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup (descr2, ts2), pos2)) =

     (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Model_Def.get_dscr_opt feedb1 of

           NONE => false

         | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of

       NONE =>

         (i2, [max_vnt], bool2, m_field2, (Sup (descr2, ts2), pos2)) (*the present in i2_model*)

     | SOME i1_single => i1_single)                     (*shift the item from i1_model to i2_model*)

   | add_other _ _ i2_single = i2_single                    (*keep all the other items in i2_model*)

 (*fill method from items already input*)

 fun fill_method o_model (pbl_imod, met_imod) met_patt =

   let

     val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod

     (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)

     val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)

       Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)

     val met_max_vnts = Model_Def.max_variants o_model i_from_met;

     val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts);

     (*add items from pbl_imod (without overwriting existing items in met_imod)*)

   in

     map (add_other max_vnt pbl_imod) i_from_met

   end 

 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 |> Model_Def.get_dscr_opt |> the |> UnparseC.term (ContextC.for_ERROR ()))

 fun transfer_terms (i, vnts, m_field, descr, ts) =

   (i, vnts, true, m_field, (Cor (descr, ts), Position.none))

 fun s_make_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =

   let

     val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;

     val {model = met_patt, ...} = MethodC.from_store ctxt met_id;

     val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;

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

       Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt

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

       if is_empty_single i_single

       then

         case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of

             [] => raise ERROR (msg pbl_max_vnts feedb)

           | o_singles => map transfer_terms o_singles

       else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

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

       Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt

     val met_max_vnts = Model_Def.max_variants o_model i_from_met;

     val max_vnt = hd met_max_vnts (*need only one for solve-phase*)

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

       if is_empty_single i_single

       then

         case Pre_Conds.get_descr_vnt' feedb [max_vnt] o_model of

             [] => raise ERROR (msg [max_vnt] feedb)

           | o_singles => map transfer_terms o_singles

       else [i_single (*fetched before from met_imod*)])) i_from_met |> flat

   in

     (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,

       met_from_pbl)

   end

 (**)end(**);