1 (* Title: BaseDefinitions/celem-6.sml
3 (c) due to copyright terms
6 signature CALCELEMENT_6 =
7 (*/------- to Celem6 -------\*)
8 (*\------- to Celem6 -------/*)
10 (*/------- to Celem6 -------\*)
14 val e_Mets: met Celem1.ptyp
15 (*\------- to Celem6 -------/*)
16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
20 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24 structure Celem6(**): CALCELEMENT_6(**) =
28 (*/------- to Celem6 -------\*)
29 (* data for methods stored in 'methods'-database*)
31 {guh : Celem2.guh, (* unique within this isac-knowledge *)
32 mathauthors: string list, (* copyright *)
33 init : Celem3.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
34 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
35 TODO.WN0509 store fun itself, see 'type pbt' *)
36 erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
37 instead erls in "fun prep_met" *)
38 srls : Rule_Set.T, (* for evaluating list expressions in scr *)
39 crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
40 nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
41 errpats : Error_Fill_Def.errpat list,(* error patterns expected in this method *)
42 calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
43 (*branch : TransitiveB set in append_problem at generation ob pblobj *)
44 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
45 (*TODO: abstract to ?pre_model?...*)
46 prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
47 ppc : Celem4.pat list, (* items in given, find, relate;
48 items (in "#Find") which need not occur in the arg-list of a SubProblem
49 are 'copy-named' with an identifier "*'.'".
50 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
51 see ME/calchead.sml 'fun is_copy_named'. *)
52 pre : term list (* preconditions in where *)
54 val e_met = {guh = "met_empty", mathauthors = [], init = Celem3.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
55 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
56 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
57 val e_Mets = Celem1.Ptyp ("e_metID", [e_met],[]);
59 type mets = (met Celem1.ptyp) list;
60 (*\------- to Celem6 -------/*)