1 (* Title: BaseDefinitions/method-def.sml
3 (c) due to copyright terms
5 Here is a minimum of code required for Know_Store.thy.
6 For main code see structure MethodC.
8 signature METHOD_DEFINITION =
10 type id = References_Def.id;
12 val id_to_string: id -> string
20 val empty_store: T Store.node
21 (*val e_Mets: T Store.node*)
22 val check_unique: Check_Unique.id -> T Store.T -> unit
23 (*val check_metguh_unique: Check_Unique.id -> T Store.T -> unit*)
27 structure Meth_Def(**): METHOD_DEFINITION(**) =
31 type id = References_Def.id;
32 val id_empty = References_Def.empty_meth_id;
33 val id_to_string = References_Def.id_to_string;
35 (* data for methods stored in 'methods'-database *)
36 type T = (* TODO WN200620: review ---------------------vvvvv *)
37 {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *)
38 mathauthors: string list, (* copyright *)
39 init : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly *)
40 rew_ord' : Rewrite_Ord.id, (* for ordered rewriting by Tactic.Rewrite *)
41 erls : Rule_Set.T, (* for conditions in rewriting by Tactic.Rewrite *)
42 srls : Rule_Set.T, (* for evaluating Prog_Expr *)
43 crls : Rule_Set.T, (* DEL: for check_elementwise *)
44 nrls : Rule_Set.T, (* for rewriting by Tactic.Rewrite *)
45 errpats : Error_Pattern_Def.T list, (* error patterns expected in this method *)
46 calc : Rule_Def.calc list,(* ?DEL *)
47 scr : Rule.program, (* filled in MethodC.prep_input *)
48 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
49 ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate"
50 for constraints on identifiers see "O_Model.copy_name" *)
51 pre : term list (* ? DEL, as soon as they are input interactively ? *)
53 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.id_empty,
54 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
55 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
56 val empty_store = Store.Node ("empty_meth_id", [empty],[]);
58 type store = (T Store.node) list;
61 Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.id));