(* Title:  Specify/i-model.sml

   Author: Walther Neuper 110226

   (c) due to copyright terms

 *)

signature MODEL_FOR_INTERACTION =

sig

  type T

  type single

  val empty: single 

  type variants

  type m_field

  type descriptor

  datatype feedback = datatype Model_Def.i_model_feedback

  val feedback_to_string': feedback -> string

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

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

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

  datatype additm = Add of single | Err of string

  val init: Model_Pattern.T -> T

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

    T -> Model_Pattern.T -> TermC.as_string -> additm

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

(*/------- to I_Model from Specify -------\*)

(*val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T*)

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

(*\------- to I_Model from Specify -------/*)

(*/------- rename -------\*)

  val d_in: feedback -> term

  val ts_in: feedback -> term list

  val vars_of: T -> term list

  val max_vt: T -> int

  val is_known: Proof.context -> string -> O_Model.T -> term -> string * O_Model.single * term list

  val is_notyet_input : Proof.context -> T -> term list -> O_Model.single -> ('a * (term * term)) list

    -> string * single

  val dsc_unknown: term

  val geti_ct: theory -> O_Model.single -> single -> m_field * UnparseC.term_as_string

  val pbl_ids': term -> term list -> term list

  val mk_env: T -> (term * term) list

  val penvval_in: feedback -> term list

(*\------- rename -------/*)

  val complete: O_Model.T -> T -> 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

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

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val is_complete: T -> bool

  val to_p_model: theory -> feedback -> string

(*/------- rename -------\*)

  val dts2str: term * (term list) -> string

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

(*\------- rename -------/*)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

(*/------- rename -------\*)

  val vts_in: T -> int list

  val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list

(*\------- rename -------/*)

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure I_Model(**) : MODEL_FOR_INTERACTION(**) =

struct

(**)

(** data types **)

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;

datatype feedback = datatype Model_Def.i_model_feedback;

type single = Model_Def.i_model_single;

val empty = Model_Def.i_model_empty;

fun pen2str ctxt (t, ts) =

  pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt  ctxt)) ts);

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

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

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

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

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

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

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

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

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

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

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

fun feedback_to_string' t = feedback_to_string (ThyC.id_to_ctxt "Isac_Knowledge") t;

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

(*/------- to I_Model from Specify -------\*)

fun get_tac 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);

(*\------- to I_Model from Specify -------/*)

(** initialise a model **)

fun init pbt = 

  let

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

  in map pbt2itm pbt end

(** check input on a model **)

(* find most frequent variant v in itms *)

fun vts_in itms = (distinct o flat o (map #2)) (itms: T);

fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map #2)) itms);

fun vts_cnt vts itms = map (cnt itms) vts;

fun max2 [] = raise ERROR "max2 of []"

  | max2 (y :: ys) =

    let

      fun mx (a,x) [] = (a,x)

  	    | mx (a, x) ((b,y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;

    in mx y ys end;

(* get the constant value from a penv *)

fun getval (id, values) = 

  case values of

	  [] => raise ERROR ("penv_value: no values in '" ^ UnparseC.term id)

  | [v] => (id, v)

  | (v1 :: v2 :: _) => (case v1 of 

	      Const ("Program.Arbfix",_) => (id, v2)

	    | _ => (id, v1));

(* find the variant with most items already input *)

fun max_vt itms = 

    let val vts = (vts_cnt (vts_in itms)) itms;

    in if vts = [] then 0 else (fst o max2) vts end;

(* TODO ev. make more efficient by avoiding flat *)

fun mk_e (Cor (_, iv)) = [getval iv]

  | mk_e (Syn _) = []

  | mk_e (Typ _) = [] 

  | mk_e (Inc (_, iv)) = [getval iv]

  | mk_e (Sup _) = []

  | mk_e (Mis _) = []

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

fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];

(* extract the environment from an item list; takes the variant with most items *)

fun mk_env itms = 

  let val vt = max_vt itms

  in (flat o (map (mk_en vt))) itms end;

(**)

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

  | ts_in (Syn _) = []

  | ts_in (Typ _) = []

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

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

  | ts_in (Mis _) = []

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

val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";

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

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

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

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

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

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

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

fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);

fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d, ts)]

  | penvval_in (Syn  (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])

  | penvval_in (Typ  (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])

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

  | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])

  | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^

			pair2str(UnparseC.term d, UnparseC.term t));*) [])

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

fun vars_of itms = itms |> mk_env |> map snd

fun seek_oridts ctxt sel (d, ts) [] =

    ("seek_oridts: input ('" ^

        (UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",

      (0, [], sel, d, ts),

      [])

  | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =

    if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []

    then ("", (id, vat, sel, d, inter op = ts ts'), ts')

    else seek_oridts ctxt sel (d, ts) oris

fun test_types ctxt (d,ts) =

  let 

    val opt = (try Input_Descript.join) (d, ts)

    val msg = case opt of 

      SOME _ => "" 

    | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^

	    (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts ^ " is illtyped")

  in msg end

(* to an input (_,ts) find the according ori and insert the ts *)

fun seek_orits ctxt _ ts [] = 

    ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^

    "') not found in oris (typed)", O_Model.single_empty, [])

  | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =

    if sel = sel' andalso (inter op = ts ts') <> [] 

    then

      if sel = sel' 

      then ("", (id, vat, sel, d, inter op = ts ts'), ts')

      else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, O_Model.single_empty, [])

    else seek_orits ctxt sel ts oris

(* make a term 'typeless' for comparing with another 'typeless' term;

   'type-less' usually is illtyped                                  *)

fun typeless (Const (s, _)) = (Const (s, TermC.typ_empty)) 

  | typeless (Free (s, _)) = (Free (s, TermC.typ_empty))

  | typeless (Var (n, _)) = (Var (n, TermC.typ_empty))

  | typeless (Bound i) = (Bound i)

  | typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, typeless t)

  | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)

(* is the term t input (or taken from fmz) known in oris ?

   give feedback on all(?) strange input;

   return _all_ terms already input to this item (e.g. valuesFor a,b) *)

fun is_known ctxt sel ori t =

  let

    val ots = (distinct o flat o (map #5)) ori

    val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots

    val (d, ts) = Input_Descript.split t

    val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)

  in

    if (subtract op = oids ids) <> []

    then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", O_Model.single_empty, [])

    else 

	    if d = TermC.empty 

	    then 

	      if not (subset op = (map typeless ts, map typeless ots))

	      then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^

		      "' not in example (typeless)", O_Model.single_empty, [])

	      else 

          (case seek_orits ctxt sel ts ori of

		         ("", ori_ as (_,_,_,d,ts), all) =>

		            (case test_types ctxt (d,ts) of

		              "" => ("", ori_, all)

		            | msg => (msg, O_Model.single_empty, []))

		       | (msg, _, _) => (msg, O_Model.single_empty, []))

	    else 

	      if member op = (map #4 ori) d

	      then seek_oridts ctxt sel (d, ts) ori

	      else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])

  end

val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";

(* get a term from ori, notyet input in itm.

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

   machinery for immediate input by the user. *)

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

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

(* 9.5.03 penv postponed: pbl_ids' *)

fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];

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

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

  let 

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

    val pval =pbl_ids' 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' i)

  end

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

fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in 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 = (ts_in itm_) ts

          in 

            if subset op = (ts, ts') 

            then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", empty) (*2*)

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

	          end

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

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

datatype additm =

	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 from Formalise.T)

  check_single is extremely permissive.

*)

fun check_single ctxt m_field [] i_model m_patt ct =

      let

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

      in 

        case TermC.parseNEW ctxt ct of

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

        | SOME t =>

            let

              val (d, ts) = Input_Descript.split t

            in 

              if d = TermC.empty then

                Add (i, [], false, m_field, Mis (dsc_unknown, 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 = (d_in itm_) andalso i <> 0

                    in

                      case find_first (eq2 d) i_model of

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

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

                          if Input_Descript.for_list d then 

                            let

                              val in_itm = ts_in 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, pbl_ids' d ts')))end

                          else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))

                    end)

            end

      end

  | check_single ctxt m_field o_model i_model m_patt str =

      case TermC.parseNEW ctxt str of

        NONE => Err ("check_single: syntax error in '" ^ str ^ "'")

      | SOME t => 

          case is_known 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: is_known: " ^ msg);

(** add input **)

fun overwrite_ppc thy itm ppc =

  let 

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

        raise ERROR ("overwrite_ppc: " ^ (feedback_to_string (ThyC.to_ctxt thy) itm_) ^ " not found")

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

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

	      then ppc' @ [itm] @ ppc

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

  in repl [] itm ppc end

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

fun seek_ppc _ [] = NONE

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

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

  let 

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

      | eq_untouched _ _ = false

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

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

    | NONE => (ppc @ [itm])

  in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end

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

  (i, v, true, f, Cor ((d, ts), ((snd o snd o the o (find_first (eq1 d))) pbt, ts)))

    handle _ => (i, v, true, f, Cor ((d, ts), (d, ts)))

      (*dsc in oris, but not in pbl pat list: keep this dsc*)

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

fun filter_outs oris [] = oris

  | filter_outs oris (i::itms) = 

    let

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

    in

      filter_outs ors itms

    end

(* 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 _ (Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))

  | to_p_model _ (Syn c) = c

  | to_p_model _ (Typ c) = c

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

  | to_p_model _ (Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))

  | to_p_model _ (Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid

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

fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (d_in itm_ = d_in 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 = max_vt 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

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

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

  let

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

    val vat = if probl = [] then 1 else max_vt 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 ppc) (*which are in pbt, too*)

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

    val mits = complete oris pits [] mpc

  in (pits, mits) end

(* WN0312: use in nxt_spec, too ? what about variants ??? *)

fun is_complete [] = false

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

(**)end(**);