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

(*val e_Mets: T Store.node*)

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

(*val check_metguh_unique: Check_Unique.guh -> T Store.T -> 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.Node ("e_metID", [empty],[]);

type store = (T Store.node) list;

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

val check_unique =

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

(**)end(**)