walther@59892: (* Title:  BaseDefinitions/method-def.sml
walther@59882:    Author: Walther Neuper
walther@59882:    (c) due to copyright terms
walther@59882: 
walther@59919: Here is a minimum of code required for Know_Store.thy.
walther@59919: For main code see structure Method.
walther@59892: *)
walther@59893: signature METHOD_DEFINITION =
walther@59882: sig
walther@59985:   type id = References_Def.id;
walther@59903:   val id_empty: id
walther@59903:   val id_to_string: id -> string
walther@59903: 
walther@59895:   type T
walther@59895: (*type met*)
walther@59895:   val empty: T
walther@59895: (*val e_met: T*)
walther@59895:   type store
walther@59895: (*type mets*)
walther@59897:   val empty_store: T Store.node
walther@59897: (*val e_Mets: T Store.node*)
walther@59904:   val check_unique: Check_Unique.id -> T Store.T -> unit
walther@59904: (*val check_metguh_unique: Check_Unique.id -> T Store.T -> 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@59985: type id = References_Def.id;
walther@59985: val id_empty = References_Def.empty_meth_id;
walther@59985: val id_to_string = References_Def.id_to_string;
walther@59903: 
walther@59884: (* data for methods stored in 'methods'-database*)
walther@59895: type T = 
walther@59904:      {guh        : Check_Unique.id,             (* unique within this isac-knowledge             *)
walther@59985:       mathauthors: string list,       (* copyright                                     *)
walther@59985:       init       : References_Def.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE!  *)
walther@59985:       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@59985:       errpats    : Error_Pattern_Def.T list,(* error patterns expected in this method  *)
walther@59985:       calc       : Rule_Def.calc list,(* Theory_Data in fun prep_met                   *)
walther@59985:       (*branch   : TransitiveB   set in append_problem at generation ob pblobj         *)
walther@59985:       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@59945:       ppc        : Model_Pattern.T,   (* 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@59985:         see ME/calchead.sml 'fun is_copy_named'.                                       *)
walther@59985:       pre        : term list          (* preconditions in where                        *)
walther@59884: 	   };
walther@59903: val empty = {guh = "met_empty", mathauthors = [], init = id_empty, 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@59903: val empty_store = Store.Node ("empty_meth_id", [empty],[]);
walther@59884: 
walther@59897: type store = (T Store.node) list;
walther@59882: 
walther@59895: val check_unique =
walther@59904:   Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.id));
walther@59892: 
walther@59882: (**)end(**)