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

  val empty: T

  val empty_POS: T_POS

  type single

  type single_POS

  val empty_single: single

  val empty_single_POS: single_POS

  val is_empty_single_POS: single_POS -> bool

  type variant

  type variants

  type m_field

  type descriptor

  type values

  datatype feedback = datatype Model_Def.i_model_feedback

  datatype feedback_POS = datatype Model_Def.i_model_feedback_POS

  val feedback_empty_POS: Model_Def.i_model_feedback_POS

  type env

  type message

  val single_to_string_POS: Proof.context -> single_POS -> string

  val to_string_POS: Proof.context -> T_POS -> string

  datatype add_single = Add of single_POS | Err of string

  val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS

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

    TermC.as_string -> add_single

  val add_single: theory -> single_POS -> T_POS -> T_POS

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

  val descriptor_POS: feedback_POS -> descriptor

  val get_values: T_POS -> values list

  val feedb_values: feedback_POS -> values

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

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

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

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

    Model_Pattern.T -> message * single_POS

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

  val add_other: variant -> T_POS -> single_POS -> single_POS

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

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

    T_POS * T_POS

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

  val is_error: feedback_POS -> bool

  val to_p_model: theory -> feedback_POS -> string

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

  val msg: variants -> feedback_POS -> string

  val transfer_terms: O_Model.single -> single_POS

  val feedback_POS_to_string: Proof.context -> feedback_POS -> string

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

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

  val single_from_o: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> single_POS

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

  val overwrite_ppc: theory -> single_POS -> T_POS -> T_POS

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

(* for developing input from PIDE, we use T_POS 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 *_POS) of essential parts of the Specification's semantics,

      we adapt the old tests to the new T_POS

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

*)

type T_POS = Model_Def.i_model_single_POS list;

datatype feedback = datatype Model_Def.i_model_feedback;

datatype feedback_POS = datatype Model_Def.i_model_feedback_POS;

val feedback_empty_POS = Model_Def.feedback_empty_POS

type single = Model_Def.i_model_single;

type single_POS = Model_Def.i_model_single_POS;

val empty_single = Model_Def.i_model_empty;

val empty_single_POS = Model_Def.i_model_empty_POS;

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

  | is_empty_single_POS _ = false

val empty = []: T;

val empty_POS = []: T_POS;

type env = Env.T

type message = string;

fun feedback_POS_to_string ctxt (Cor_POS (d, ts)) = 

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

  | feedback_POS_to_string _ (Syn_POS c) =

    "Syn_POS " ^ c

  | feedback_POS_to_string ctxt (Inc_POS (d, [])) = 

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

      Model_Pattern.empty_for d

  | feedback_POS_to_string ctxt (Inc_POS (d, ts)) =

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

  | feedback_POS_to_string ctxt (Sup_POS (d, ts)) = 

    "Sup_POS " ^ 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_POS does NOT raise an exn*)

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

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

  | feedb_args_to_string _ (Syn_POS str) = str

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

    UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr

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

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

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

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

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

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

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

fun to_string_POS ctxt itms = strs2str' (map (linefeed o (single_to_string_POS 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

(*

  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_POS (descr, []), Position.none))

fun init_POS 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_POS (Cor_POS (d ,_)) = d

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

  | descriptor_POS (Inc_POS (d, _)) = d

  | descriptor_POS (Sup_POS (d, _)) = d

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

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

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

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

(*assumption: i_model has filtered max_vnt*)

local

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

   case find_first (fn (_, _, _, _, (feedb, _)) => descr = descriptor_POS 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_POS (_, ts)) = [ts]

  | feedb_vals (Syn_POS _) = []

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

  | feedb_vals (Sup_POS (_, 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_POS ctxt b)

    |> pair2str) equal_descr_pairs)

  |> strs2str'

fun variables model_patt i_model =

  Pre_Conds.environment_POS model_patt i_model

  |> map snd

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

fun single_from_o (feedb:feedback_POS) _ 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_POS _ => if fd = "#undef"

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

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

    | Inc_POS _ => if complete

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

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

    | Sup_POS (d, ts') =>

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

    | i => raise ERROR ("single_from_o: uncovered case of " ^ feedback_POS_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_POS 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_POS)

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

	        end

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

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

datatype add_single =

	Add of single_POS   (* 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_POS (d,ts), Position.none))

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

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

            NONE =>

              Add (i, [], true, f, (Cor_POS (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_POS (d, ts'), Position.none)) end

            else Add (i', [], true, f, (Cor_POS (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_POS_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_POS) 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_POS 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_POS 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_POS _) = false

  | is_error (Sup_POS _) = false

  | is_error (Inc_POS _) = false

  | is_error (Syn_POS _) = true

(*create output-string for itm*)

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

  | to_p_model _ (Syn_POS c) = c

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

  | to_p_model thy (Sup_POS (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_POS (descr, [Model_Def.values_to_present ts]), pos))

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

      end

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

  end

(*

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

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

  otherwise keep the items of i2_model.

*)

fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_POS (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_POS (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_POS (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_POS 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_POS 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(**);