(* Title:  BaseDefinitions/model-pattern.sml

    Author: Walther Neuper

    (c) due to copyright terms

 A pattern to be combined with a formalisation (Formalise.T) yielding an O_Model.T..

 *)

 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

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

 (**)end(**)