(* Title:  Specify/o-model.sml

    Author: Walther Neuper 110226

    (c) due to copyright terms

 An original model is created initially from Formalise.T and Model_Pattern.T;

 This model makes student's editing via I_Model.T more efficient.

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

 *)

 signature ORIGINAL_MODEL =

 sig

   type T

   type single

   type variants

   type m_field

   type descriptor

   val to_string: T -> string

   val single_to_string: single -> string

   val single_empty: single

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

   val add : theory -> Model_Pattern.T -> T -> T

   val values : T -> term list

 (*/--- use struct.id for appropriate names ..*)

   val match_ags: theory -> Model_Pattern.T -> term list -> T (*?\<rightarrow>M_Match?*)

   val match_ags_msg: Problem.id -> term -> term list -> unit (*?\<rightarrow>M_Match?*)

   val oris2fmz_vals: T -> string list * term list

 (*val variables: Model_Pattern.T -> term list*)              (*(*?\<rightarrow>Model_Pattern?*)*)

   val vars_of_pbl_': Model_Pattern.T -> term list            (*(*?\<rightarrow>Model_Pattern?*)*)

 (*put add_id into a new auxiliary fun..*)

   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 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 matc: theory -> Model_Pattern.T -> term list -> preori list -> preori list

   val mtc: theory -> Model_Pattern.single -> term -> preori option

   val preoris2str : preori list -> string

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

   val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b

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

   val max: variants -> int

   val coll_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

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

 end

 (**)

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

 struct

 (**)

 (** types **)

 type variants =  Model_Def.variants;

 type m_field = Model_Def.m_field;

 type descriptor = Model_Def.descriptor;

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

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

 (** add new m_field's from method **)

 fun add _ mpc ori =

   let

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

     fun repl mpc (i, v, _, d, ts) = 

       case filter (eq d) mpc of

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

       | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)    

       | _ => raise ERROR ("O_Model.add: " ^ UnparseC.term d ^ " more than once in met");

   in flat ((map (repl mpc)) ori) 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;

 fun values oris =

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

 (** ? ? ? **)

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

 (* split type-wrapper from scr-arg and build part of an ori;

    an type-error is reported immediately, raises an exn, 

    subsequent handling of exn provides 2nd part of error message *)

 fun mtc thy (str, (dsc, _)) (ty $ var) =

     ((Thm.global_cterm_of thy (dsc $ var);(*type check*)

       SOME (([1], str, dsc, (*[var]*)

 	    Input_Descript.split' (dsc, var))) (*:ori without leading #*))

       handle e as TYPE _ => 

 	      (tracing (dashs 70 ^ "\n"

 	        ^ "*** ERROR while creating the items for the model of the ->problem\n"

 	        ^ "*** from the ->stac with ->typeconstructor in arglist:\n"

 	        ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"

 	        ^ "*** description: " ^ TermC.term_detail2str dsc

 	        ^ "*** value: " ^ TermC.term_detail2str var

 	        ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty

 	        ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"

 	        ^ "*** " ^ dots 66);

           writeln (@{make_string} e);

           Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)

       NONE))

   | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)

 (* match each pat of the model-pattern with an actual argument;

    precondition: copy-named vars are filtered out            *)

 fun matc _ [] _ oris = oris

   | matc _ pbt [] _ =

     (tracing (dashs 70);

      raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))

   | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =

     (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris

     else(*..del?*)

       let val opt = mtc thy p a

       in

         case opt of

           SOME ori => matc thy pbt ags (oris @ [ori])

 	      | NONE => [](*WN050903 skipped by exn handled in match_ags*)

 	 end

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

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

 fun oris2fmz_vals 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

 (* match the actual arguments of a SubProblem with a model-pattern

    and create an ori list (in root-pbl created from formalization).

    expects ags:pats = 1:1, while copy-named are filtered out of pats;

    if no 1:1 then exn raised by matc/mtc and handled at call.

    copy-named pats are appended in order to get them into the model-items *)

 fun match_ags thy pbt ags =

   let

     fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)

     val pbt' = filter_out is_copy_named pbt

     val cy = filter is_copy_named pbt  (* cy is NOT a (formal) argument, but the fun's result *)

     val oris' = matc thy pbt' ags []

     val cy' = map (cpy_nam pbt' oris') cy

     val ors = add_id (oris' @ cy') (*...appended in order to get into the model-items *)

   in (map flattup ors) end

 (* report part of the error-msg which is not available in match_args *)

 fun match_ags_msg pI stac ags =

   let

     val pats = (#ppc o Problem.from_store) pI

     val msg = (dots 70 ^ "\n"

        ^ "*** problem " ^ strs2str pI ^ " has the ...\n"

        ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"

        ^ "*** stac   '" ^ UnparseC.term stac ^ "' has the ...\n"

        ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"

        ^ dashs 70)

 	  (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)

   in tracing msg end

 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)

 fun vars_of_pbl_' pbl_ = 

   let

     fun var_of_pbl_ (_, (_, t)) = t: term

   in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end

 (**)end(**);