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 Method.
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*)
24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32 structure Meth_Def(**): METHOD_DEFINITION(**) =
36 type id = References_Def.id;
37 val id_empty = References_Def.empty_meth_id;
38 val id_to_string = References_Def.id_to_string;
40 (* data for methods stored in 'methods'-database *)
41 type T = (* TODO WN200620: review ---------------------vvvvv *)
42 {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *)
43 mathauthors: string list, (* copyright *)
44 init : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly *)
45 rew_ord' : Rule_Def.rew_ord', (* for ordered rewriting by Tactic.Rewrite *)
46 erls : Rule_Set.T, (* for conditions in rewriting by Tactic.Rewrite *)
47 srls : Rule_Set.T, (* for evaluating Prog_Expr *)
48 crls : Rule_Set.T, (* DEL: for check_elementwise *)
49 nrls : Rule_Set.T, (* for rewriting by Tactic.Rewrite *)
50 errpats : Error_Pattern_Def.T list, (* error patterns expected in this method *)
51 calc : Rule_Def.calc list,(* ?DEL *)
52 scr : Rule.program, (* filled in Method.prep_input *)
53 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
54 ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate"
55 for constraints on identifiers see "O_Model.cpy_nam" *)
56 pre : term list (* ? DEL, as soon as they are input interactively ? *)
58 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
59 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
60 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
61 val empty_store = Store.Node ("empty_meth_id", [empty],[]);
63 type store = (T Store.node) list;
66 Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.id));