(* Title:  BaseDefinitions/model-pattern.sml

   Author: Walther Neuper

   (c) due to copyright terms

A \<open>Model_Pattern\<close> defines a -> \<open>Problem\<close>-type: its \<open>variables\<close> are to be instantiated

by the values for particular \<open>Problem\<close>s.

The \<open>variables\<close> are used twice, in a model and as formal arguments in a \<open>Program\<close>.

The \<open>descriptor\<close>s are unique identifiers within one \<open>Model_Pattern\<close>.

*)

signature MODEL_PATTERN =

sig

  type T

  type single

  val to_string: single list -> string

  type m_field = string

  type descriptor = term

  val variables: T -> term list

  val get_field: descriptor -> T -> m_field option

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

  val to_string': T -> string

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

  (*NONE*)                                                                      

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

end

(**)

structure Model_Pattern(**): MODEL_PATTERN(**) =

struct

(**)

(* the pattern for an item of a problems model or a methods guard *)

type m_field = string;

type descriptor = term;

type single =

  (m_field *      (* field Given, Find, Relate *)

	  (descriptor * (* for snd term              *)

	     term))     (* id | arbitrary term       *);

type T = single list;

fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));

fun to_string pats = (strs2str o (map pat2str)) pats;

fun pat2str' (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n";

fun to_string' pats = (strs2str o (map pat2str')) pats;

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

fun variables pbl_ = 

  let

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

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

fun get_field descriptor m_patt = 

  (filter ((curry (fn (desc, (_, (desc', _))) => desc = desc')) descriptor) m_patt

    |> the_single

    |> (fn (a, _) => SOME a))

  handle List.Empty => NONE

(**)end(**)