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

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

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