(* Title:  Specify/o-model.sml

   Author: Walther Neuper 110226

   (c) due to copyright terms

An \<open>O_Model\<close> holds \<open>O\<close>riginal data, \<open>descriptor\<close> and \<open>values\<close> parsed from \<open>Formalise.model\<close>

selected with respect to a \<open>Model_Pattern\<close> and combined with respective \<open>m_field\<close>s.

\<open>complete_for\<close> a \<open>Model_Pattern\<close> is done by \<open>Tactic.Model_Problem\<close>

(with defaults from \<open>Formalise\<close>refs), by \<open>Tactic.Specify_Problem\<close> and \<open>Tactic.Specify_Method\<close>

\<open>O_Model\<close> serves efficiency of student's interactive modelling via \<open>I_Model\<close>.

\<open>O_Model\<close> marks elements with  \<open>m_field\<close> \<open>#undef\<close>, which are not required by the \<open>Model_Pattern\<close>

of the \<open>Problem\<close> or the \<open>MethodC\<close> .. TODO redes: \<open>m_field\<close> probably different in root..Subproblem

TODO: revise with an example with more than 1 variant.

    + consider: drop m_field ?

*)

signature ORIGINAL_MODEL =

sig

  type T

  type single

  type variant

  type variants

  type m_field

  type descriptor

  type values

  type message

  val to_string: T -> string

  val single_to_string: single -> string

  val single_empty: single

(*val init: theory -> Formalise.model -> Model_Pattern.T -> T ..TODO*)

  val init: Formalise.model -> theory -> Model_Pattern.T -> T

  val values : T -> term list

  val values': T -> Formalise.model * term list

  val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context

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

(*val seek_oridts: Proof.context -> ?/////? -> descriptor * values -> T -> message * single * values*)

  val seek_oridts: Proof.context -> m_field -> descriptor * values -> T -> message * single * values

(*val single_for_values:!!! values -> Proof.context -> m_field -> T -> message * single * values*)

  val seek_orits: Proof.context -> m_field -> values -> T -> message * single * values

(*val ?contains:!!! term -> Proof.context -> m_field -> T -> message * single * values*)

  val is_known: Proof.context -> m_field -> T -> term -> message * single * values

(*val typeless: term -> term*)

  val typeless: term -> term

(*val test_types: Proof.context -> descriptor * values -> string*)

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

(*put add_id into a new auxiliary fun, see ONLY call..*)

  val add_id: 'a list -> (int * 'a) list

  type preori

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

(*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)

  val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori

  val is_copy_named: Model_Pattern.single -> bool

  val is_copy_named_idstr: string -> bool

  val is_copy_named_generating_idstr: string -> bool

  val is_copy_named_generating: Model_Pattern.single -> bool

  val preoris2str : preori list -> string

(*val getr_ct: theory -> single -> m_field * UnparseC.term_as_string*)

  val getr_ct: theory -> single -> m_field * UnparseC.term_as_string

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

  val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values

  val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list

(*val max: variants -> int*)

  val max: variants -> int

(*val coll_variants: ('a * ''b) list -> ('a list * ''b) list*)

  val coll_variants: ('a * ''b) list -> ('a list * ''b) list

(*val replace_0: int -> int list -> int list*)

  val replace_0: int -> int list -> int list

  val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e

(*val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list*)

  val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list

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

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

end

(**)

structure O_Model(**) : ORIGINAL_MODEL(**) =

struct

(**)

(** 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 message = string;

type T = Model_Def.o_model;

type single = Model_Def.o_model_single

val single_empty = Model_Def.o_model_empty;

val single_to_string = Model_Def.o_model_single_to_string;

val to_string = Model_Def.o_model_to_string;

(* O_Model.single without leading integer *)

type preori = (variants * m_field * term * term list);

fun preori2str (vs, fi, t, ts) = 

  "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^

  UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";

val preoris2str = (strs2str' o (map (linefeed o preori2str)));

(* get the first term in ts from ori *)

fun getr_ct thy (_, _, fd, d, ts) =

  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))

(** initialise O_Model **)

(* compare d and dsc in pbt and transfer field to pre-ori *)

fun add_field (_: theory) pbt (d,ts) = 

  let fun eq d pt = (d = (fst o snd) pt);

  in case filter (eq d) pbt of

       [(fi, (_, _))] => (fi, d, ts)

     | [] => ("#undef", d, ts)   (*may come with met.ppc*)

     | _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")

  end;

(*

  mark an element with the position within a plateau;

  a plateau with length 1 is marked with 0

*)

fun mark _ [] = raise ERROR "mark []"

  | mark eq xs =

    let

      fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]

        | mar _ _ [] _ = raise ERROR "mark []"

        | mar xx eq (x:: x' :: xs) n = 

        if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)

        else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;

    in mar [] eq xs 1 end;

(*

  assumes equal descriptions to be in adjacent 'plateaus',

  items at a certain position within the plateaus form a variant;

  length = 1 ... marked with 0: covers all variants

*)

fun add_variants fdts = 

  let 

    fun eq (a, b) = curry op= (snd3 a) (snd3 b);

  in mark eq fdts end;

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

  | max (y :: ys) =

  let fun mx x [] = x

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

in mx y ys end;

fun coll_variants (((v,x) :: vxs)) =

    let

      fun col xs (vs, x) [] = xs @ [(vs, x)]

        | col xs (vs, x) ((v', x') :: vxs') = 

        if x = x' then col xs (vs @ [v'], x') vxs'

        else col (xs @ [(vs, x)]) ([v'], x') vxs';

    in col [] ([v], x) vxs end

  | coll_variants _ = raise ERROR "coll_variants: called with []";

fun replace_0 vm [0] = intsto vm

  | replace_0 _ vs = vs;

fun add_id [] = raise ERROR "O_Model.add_id []"

  | add_id xs =

    let

      fun add _ [] = []

        | add n (x :: xs) = (n, x) :: add (n + 1) xs;

    in add 1 xs end;

fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);

fun init [] _ _ = []

  | init fmz thy pbt =

    let

      val model =

        (map (fn str => str

          |> TermC.parseNEW'' thy

          |> Input_Descript.split

          |> add_field thy pbt) fmz)

        |> add_variants;

      val maxv = model |> map fst |> max;

      val maxv = if maxv = 0 then 1 else maxv;

      val model' = model

        |> coll_variants

        |> map (replace_0 maxv |> apfst)

        |> add_id

        |> map flattup;

    in model' end;

(** get the values **)

fun mkval _(*dsc*) [] = raise ERROR "mkval called with []"

  | mkval _ [t] = t

  | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;

fun mkval' x = mkval TermC.empty x;

(*TODO: unify with values'*)

fun values (oris:T) =

  ((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris

(** complete wrt. Model_Pattern.T by use of root's O_Model.T **)

fun complete_for m_patt root_model (o_model, ctxt) =

  let

    val  missing = m_patt |> filter_out

      (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))

    val add = (root_model

      |> filter

        (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))

  in

    ((o_model @ add)

      |> map (fn (a, b, _, descr, e) =>

               case Model_Pattern.get_field descr m_patt of

                 SOME m_field => (a, b, m_field, descr, e)

               | NONE => (a, b, "#undef", descr, e))

      |> map (fn (_, b, c, d, e) => (b, c, d, e))      (* for correct enumeration *)

      |> add_id                                        (* for correct enumeration *)

      |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)

    ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))

  end

(** ? ? ? **)

(* make oris from args of the stac SubProblem and from pbt.

   can this formal argument (of a model-pattern) be omitted in the arg-list

   of a SubProblem ? see calcelems.sml 'type met '                        *)

fun is_copy_named_idstr str =

  case (rev o Symbol.explode) str of

	  "'" :: _ :: "'" :: _ => true

  | _ => false

fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.free2str) t

(* should this formal argument (of a model-pattern) create a new identifier? *)

fun is_copy_named_generating_idstr str =

  if is_copy_named_idstr str

  then

    case (rev o Symbol.explode) str of

	    "'" :: "'" :: "'" :: _ => false

    | _ => true

  else false

fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t

(* generate a new variable "x_i" name from a related given one "x"

   by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"

   e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),

   but leave is_copy_named_generating as is, e.t. ss''' *)

fun cpy_nam pbt oris (p as (field, (dsc, t))) =

  (if is_copy_named_generating p

   then (*WN051014 kept strange old code ...*)

     let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts) 

       val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t

       val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t

       val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)

       val vals = map sel oris

       val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext

     in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end

   else ([1], field, dsc, [t])

	) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)

(* ["BOOL (1+x=2)", "REAL x"] --match_ags--> oris 

   --values'--> ["equality (1+x=2)", "boundVariable x", "solutions L"] *)

(*TODO: unify with values*)

fun values' oris =

  let fun ori2fmz_vals (_, _, _, dsc, ts) = 

	  ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts) 

	  handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)

  in (split_list o (map ori2fmz_vals)) oris end

(** tools for I_Model **)

fun seek_oridts ctxt m_field (descript, vals) [] =

    ("seek_oridts: input ('" ^

        (UnparseC.term_in_ctxt ctxt (Input_Descript.join (descript, vals))) ^

          "') not found in oris (typed)", (0, [], m_field, descript, vals), [])

  | 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

(* to an input (_ $ values) find the according O_Model.single and insert the values *)

fun seek_orits ctxt _ vals [] = 

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

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

  | seek_orits ctxt m_field vals ((id, vat, m_field', descr, vals') :: oris) =

    if m_field = m_field' andalso (inter op = vals vals') <> [] 

    then

      if m_field = m_field' 

      then ("", (id, vat, m_field, descr, inter op = vals vals'), vals')

      else ((strs2str' o map (UnparseC.term_in_ctxt ctxt)) vals ^

        " not for " ^ m_field, single_empty, [])

    else seek_orits ctxt m_field vals 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

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

   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 op =) o flat o (map #5)) ori

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

    val (d, ts) = Input_Descript.split t

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

  in

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

    then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", 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)", single_empty, [])

	      else 

          (case seek_orits ctxt sel ts(*..values*) ori of

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

		            (case test_types ctxt (d,ts) of

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

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

		       | (msg, _, _) => (msg, 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

(**)end(**);