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@60154: For main code see structure MethodC.
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: 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@60022: (* data for methods stored in 'methods'-database *)
walther@60022: type T =                          (* TODO WN200620: review ---------------------vvvvv         *)
walther@60022:   {guh       : Check_Unique.id,   (* unique within Isac_Knowledge, for html-presentation      *)
walther@60022:   mathauthors: string list,       (* copyright                                                *)
walther@60022:   init       : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly                *)
Walther@60509:   rew_ord'   : Rewrite_Ord.id,    (* for ordered rewriting by Tactic.Rewrite                  *)
walther@60022:   erls       : Rule_Set.T,        (* for conditions in rewriting by Tactic.Rewrite            *)
walther@60022:   srls       : Rule_Set.T,        (* for evaluating Prog_Expr                                 *)
walther@60022:   crls       : Rule_Set.T,        (* DEL: for check_elementwise                               *)
walther@60022:   nrls       : Rule_Set.T,        (* for rewriting by Tactic.Rewrite                          *)
walther@60022:   errpats    : Error_Pattern_Def.T list, (* error patterns expected in this method            *)
walther@60022:   calc       : Rule_Def.calc list,(* ?DEL                                                     *)
Walther@60469:   scr        : Rule.program,      (* filled in MethodC.prep_input                             *)
walther@60022:   prls       : Rule_Set.T,        (* for evaluation of preconditions in "#Where" on "#Given"  *)
walther@60022:   ppc        : Model_Pattern.T,   (* contains "#Given", "#Where", "#Find", "#Relate"
Walther@60475:                                      for constraints on identifiers see "O_Model.copy_name"   *)
walther@60022:   pre        : term list          (* ? DEL, as soon as they are input interactively ?         *)
walther@60022: 	};
Walther@60509: val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.id_empty,
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(**)