walther@59892: (* Title:  BaseDefinitions/method-def.sml
walther@59882:    Author: Walther Neuper
walther@59882:    (c) due to copyright terms
walther@59882: 
walther@59892: Will be enhanced by Method later.
walther@59892: *)
walther@59893: signature METHOD_DEFINITION =
walther@59882: sig
walther@59888:   type met
walther@59888:   val e_met: met
walther@59884:   type mets
walther@59890:   val e_Mets: met Store.ptyp
walther@59892: (*vvv check_unique*)
walther@59892:   val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit
walther@59882: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
walther@59882:   (*NONE*)
walther@59886: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
walther@59882:   (*NONE*)
walther@59886: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
walther@59882: end
walther@59882: 
walther@59882: (**)
walther@59893: structure Meth_Def(**): METHOD_DEFINITION(**) =
walther@59882: struct
walther@59882: (**)
walther@59882: 
walther@59882: (*/------- to Celem6 -------\*)
walther@59884: (* data for methods stored in 'methods'-database*)
walther@59884: type met = 
walther@59892:      {guh        : Check_Unique.guh,             (* unique within this isac-knowledge             *)
walther@59884:       mathauthors: string list,     (* copyright                                     *)
walther@59891:       init       : Spec.pblID,           (* WN060721 introduced mistakenly--TODO.REMOVE!  *)
walther@59884:       rew_ord'   : Rule_Def.rew_ord',  (* for rules in Detail                           
walther@59884: 			                                 TODO.WN0509 store fun itself, see 'type pbt'  *)
walther@59884:       erls       : Rule_Set.T,        (* the eval_rls for cond. in rules FIXME "rls'   
walther@59884: 				                               instead erls in "fun prep_met"                *)
walther@59884:       srls       : Rule_Set.T,        (* for evaluating list expressions in scr        *)
walther@59884:       crls       : Rule_Set.T,        (* for check_elementwise, ie. formulae in calc.  *)
walther@59884:       nrls       : Rule_Set.T,        (* canonical simplifier specific for this met    *)
walther@59884:       errpats    : Error_Fill_Def.errpat list,(* error patterns expected in this method        *)
walther@59884:       calc       : Rule_Def.calc list, (* Theory_Data in fun prep_met                   *)
walther@59884:       (*branch   : TransitiveB set in append_problem at generation ob pblobj         *)
walther@59884:       scr        : Rule.program,    (* progam, empty as @{thm refl} or Rfuns         *)
walther@59884: (*TODO: abstract to ?pre_model?...*)
walther@59884:       prls       : Rule_Set.T,        (* for evaluating predicates in modelpattern     *)
walther@59884:       ppc        : Celem4.pat list,        (* items in given, find, relate;
walther@59884: 	      items (in "#Find") which need not occur in the arg-list of a SubProblem
walther@59884:         are 'copy-named' with an identifier "*'.'".
walther@59884:         copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
walther@59884:         see ME/calchead.sml 'fun is_copy_named'.                                     *)
walther@59884:       pre        : term list        (* preconditions in where                        *)
walther@59884: 	   };
walther@59891: val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
walther@59884: 	erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
walther@59884: 	errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
walther@59890: val e_Mets = Store.Ptyp ("e_metID", [e_met],[]);
walther@59884: 
walther@59890: type mets = (met Store.ptyp) list;
walther@59882: (*\------- to Celem6 -------/*)
walther@59882: 
walther@59892: val check_metguh_unique =
walther@59893:   Check_Unique.message (Check_Unique.collect (#guh: met -> Check_Unique.guh));
walther@59892: 
walther@59882: (**)end(**)