(* Title:  BaseDefinitions/method-def.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Will be enhanced by Method later.

 *)

 signature METHOD_DEFINITION =

 sig

   type T

 (*type met*)

   val empty: T

 (*val e_met: T*)

   type store

 (*type mets*)

   val empty_store: T Store.ptyp

 (*val e_Mets: T Store.ptyp*)

   val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit

 (*val check_metguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*)

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

   (*NONE*)

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

   (*NONE*)

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

 end

 (**)

 structure Meth_Def(**): METHOD_DEFINITION(**) =

 struct

 (**)

 (* data for methods stored in 'methods'-database*)

 type T = 

      {guh        : Check_Unique.guh,             (* unique within this isac-knowledge             *)

       mathauthors: string list,     (* copyright                                     *)

       init       : Spec.pblID,           (* WN060721 introduced mistakenly--TODO.REMOVE!  *)

       rew_ord'   : Rule_Def.rew_ord',  (* for rules in Detail                           

 			                                 TODO.WN0509 store fun itself, see 'type pbt'  *)

       erls       : Rule_Set.T,        (* the eval_rls for cond. in rules FIXME "rls'   

 				                               instead erls in "fun prep_met"                *)

       srls       : Rule_Set.T,        (* for evaluating list expressions in scr        *)

       crls       : Rule_Set.T,        (* for check_elementwise, ie. formulae in calc.  *)

       nrls       : Rule_Set.T,        (* canonical simplifier specific for this met    *)

       errpats    : Error_Fill_Def.errpat list,(* error patterns expected in this method        *)

       calc       : Rule_Def.calc list, (* Theory_Data in fun prep_met                   *)

       (*branch   : TransitiveB set in append_problem at generation ob pblobj         *)

       scr        : Rule.program,    (* progam, empty as @{thm refl} or Rfuns         *)

 (*TODO: abstract to ?pre_model?...*)

       prls       : Rule_Set.T,        (* for evaluating predicates in modelpattern     *)

       ppc        : Celem4.pat list,        (* items in given, find, relate;

 	      items (in "#Find") which need not occur in the arg-list of a SubProblem

         are 'copy-named' with an identifier "*'.'".

         copy-named items are 'generating' if they are NOT "*'''" ?WN120516??

         see ME/calchead.sml 'fun is_copy_named'.                                     *)

       pre        : term list        (* preconditions in where                        *)

 	   };

 val empty = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',

 	erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,

 	errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};

 val empty_store = Store.Ptyp ("e_metID", [empty],[]);

 type store = (T Store.ptyp) list;

 (*\------- to Celem6 -------/*)

 val check_unique =

   Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.guh));

 (**)end(**)