(* Title:  BaseDefinitions/method-def.sml

   Author: Walther Neuper

   (c) due to copyright terms

Here is a minimum of code required for Know_Store.thy.

For main code see structure Method.

*)

signature METHOD_DEFINITION =

sig

  type id = References_Def.id;

  val id_empty: id

  val id_to_string: id -> string

  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.id -> T Store.T -> unit

(*val check_metguh_unique: Check_Unique.id -> 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

(**)

type id = References_Def.id;

val id_empty = References_Def.empty_meth_id;

val id_to_string = References_Def.id_to_string;

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

type T = 

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

      mathauthors: string list,       (* copyright                                     *)

      init       : References_Def.id, (* WN060721 pblID 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_Pattern_Def.T 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        : Model_Pattern.T,   (* 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 = id_empty, 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 ("empty_meth_id", [empty],[]);

type store = (T Store.node) list;

val check_unique =

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

(**)end(**)