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