1 (* Title: BaseDefinitions/method-def.sml
3 (c) due to copyright terms
5 Will be enhanced by Method later.
7 signature METHOD_DEFINITION =
11 val id_to_string: id -> string
19 val empty_store: T Store.node
20 (*val e_Mets: T Store.node*)
21 val check_unique: Check_Unique.guh -> T Store.T -> unit
22 (*val check_metguh_unique: Check_Unique.guh -> T Store.T -> unit*)
23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31 structure Meth_Def(**): METHOD_DEFINITION(**) =
36 val id_empty = Spec.empty_meth_id;
37 val id_to_string = Spec.id_to_string;
39 (* data for methods stored in 'methods'-database*)
41 {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
42 mathauthors: string list, (* copyright *)
43 init : Spec.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE! *)
44 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
45 TODO.WN0509 store fun itself, see 'type pbt' *)
46 erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
47 instead erls in "fun prep_met" *)
48 srls : Rule_Set.T, (* for evaluating list expressions in scr *)
49 crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
50 nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
51 errpats : Error_Fill_Def.errpat list,(* error patterns expected in this method *)
52 calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
53 (*branch : TransitiveB set in append_problem at generation ob pblobj *)
54 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
55 (*TODO: abstract to ?pre_model?...*)
56 prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
57 ppc : Celem4.pat list, (* items in given, find, relate;
58 items (in "#Find") which need not occur in the arg-list of a SubProblem
59 are 'copy-named' with an identifier "*'.'".
60 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
61 see ME/calchead.sml 'fun is_copy_named'. *)
62 pre : term list (* preconditions in where *)
64 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
65 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
66 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
67 val empty_store = Store.Node ("empty_meth_id", [empty],[]);
69 type store = (T Store.node) list;
70 (*\------- to Celem6 -------/*)
73 Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.guh));