(* Title:  BaseDefstart_refineions/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                                                *)

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

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

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

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

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

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

   calc: Rule_Def.eval_ml_from_prog list,(* Eval.ml_from_prog filled in Auto_Prog, also in rls   *)

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

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

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

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

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

 	};

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

 	asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, calc = [], (*crls = Rule_Set.empty,*)

 	errpats = [], rew_rls = Rule_Set.empty, model = [], where_ = [], program = 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(**)