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

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

(**)end(**);