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

 *)

 signature METHOD_DEFINITION =

 sig

   type id = References_Def.id;

   val id_empty: id

   val id_to_string: id -> string

   type T

   val empty: T

   type store

   val empty_store: T Store.node

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

 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 =                          (* TODO WN200620: review ---------------------vvvvv         *)

   {guh       : Check_Unique.id,   (* unique within Isac_Knowledge, for html-presentation      *)

   mathauthors: string list,       (* copyright                                                *)

   init       : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly                *)

   rew_ord'   : Rewrite_Ord.id,    (* for ordered rewriting by Tactic.Rewrite                  *)

   erls       : Rule_Set.T,        (* for conditions in rewriting by Tactic.Rewrite            *)

   srls       : Rule_Set.T,        (* for evaluating Prog_Expr                                 *)

   crls       : Rule_Set.T,        (* DEL: for check_elementwise                               *)

   nrls       : Rule_Set.T,        (* for rewriting by Tactic.Rewrite                          *)

   errpats    : Error_Pattern_Def.T list, (* error patterns expected in this method            *)

   calc       : Rule_Def.calc list,(* ?DEL                                                     *)

   scr        : Rule.program,      (* filled in MethodC.prep_input                             *)

   prls       : Rule_Set.T,        (* for evaluation of preconditions in "#Where" on "#Given"  *)

   ppc        : Model_Pattern.T,   (* contains "#Given", "#Where", "#Find", "#Relate"

                                      for constraints on identifiers see "O_Model.copy_name"   *)

   pre        : term list          (* ? DEL, as soon as they are input interactively ?         *)

 	};

 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.id_empty,

 	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(**)