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

   val empty: T

   type single

   type variant

   type variants

   type m_field

   type descriptor

   type values

   type message

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

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

   val single_empty: single

   val init: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context

   val values : T -> term list

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

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

   val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values

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

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

   val make_typeless: term -> term

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

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

   type preori

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

   val is_copy_named: Model_Pattern.single -> bool

   val is_copy_named': string -> bool

   val is_copy_named_generating: Model_Pattern.single -> bool

 \<^isac_test>\<open>

   val is_copy_named_generating_idstr: string -> bool

   val string_of_preoris : preori list -> string

   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 get_max_variant: variants -> variant

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

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

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

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

 \<close>

 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;

 val empty = [] : 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);

 \<^isac_test>\<open>

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

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

     UnparseC.term (ContextC.for_ERROR ()) t ^ ", " ^ 

       (strs2str o (map (UnparseC.term (ContextC.for_ERROR ())) ) ) ts ^ ")";

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

 \<close>

 (** initialise O_Model **)

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

 fun add_field thy 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.model*)

      | _ => raise ERROR ("add_field: " ^ UnparseC.term_in_thy thy 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 partition_variants _ [] = raise ERROR "partition_variants []"

   | partition_variants eq xs =

     let

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

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

         | 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 partition_variants eq fdts end;

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

   | get_max_variant (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 collect_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

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

 fun replace_0 vm [0] = intsto vm

   | replace_0 _ vs = vs;

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

   | add_enumerate 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 _ []  _ = ([], ContextC.empty)

   | init thy fmz pbt =

     let

       val (ts, ctxt) = ContextC.init_while_parsing fmz thy

       val model =

         (map (fn t => t

           |> Input_Descript.split

           |> add_field thy pbt) ts)

         |> add_variants;

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

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

       val model' = model

         |> collect_variants

         |> map (replace_0 maxv |> apfst)

         |> add_enumerate

         |> map flattup

     in (model', ctxt) 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;

 (* from an O_Model create values for ctxt *)

 fun values oris =

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

 (* from an O_Model create (Formalise.model, values)

   e.g. Subproblem ["BOOL (1+x=2)", "REAL x"] 

                  --match_ags--> O_Model.T

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

 *)

 fun values' ctxt oris =

   let

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

       case \<^try>\<open>(((UnparseC.term ctxt) o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of

         SOME x => x

       | NONE => raise ERROR ("O_Model.values' called with " ^ UnparseC.terms ctxt ts)

   in (split_list o (map ori2fmz_vals)) oris end

 (** 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_enumerate                                  (* 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' str =

   case (rev o Symbol.explode) str of

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

   | _ => false

 fun is_copy_named (_, (_, t)) = (is_copy_named' 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' 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 copy_name pbt oris (p as (field, (dsc, t))) =

   case \<^try>\<open>

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

 	\<close> of

     SOME x => x

   | NONE => raise ERROR ("copy_name: for " ^ UnparseC.term (ContextC.for_ERROR ()) t)

 (** tools for I_Model **)

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

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

     ("associate_input: input ('" ^

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

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

   | associate_input 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 associate_input ctxt sel (d, ts) oris

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

 fun associate_input' ctxt _ vals [] = 

     ("associate_input': input (_, '" ^ strs2str (map (UnparseC.term ctxt) vals) ^

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

   | associate_input' 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 ctxt)) vals ^

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

     else associate_input' 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 ctxt d ^ " " ^

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

   in msg end

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

    'type-less' usually is illtyped                                  *)

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

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

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

   | make_typeless (Bound i) = (Bound i)

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

   | make_typeless (t1 $ t2) = (make_typeless t1) $ (make_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 contains 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 make_typeless ts, map make_typeless ots))

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

 		      "' not in example (make_typeless)", single_empty, [])

 	      else 

           (case associate_input' 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 associate_input ctxt sel (d, ts) ori

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

   end

 (**)end(**);