walther@59892
|
1 |
(* Title: BaseDefinitions/method-def.sml
|
walther@59882
|
2 |
Author: Walther Neuper
|
walther@59882
|
3 |
(c) due to copyright terms
|
walther@59882
|
4 |
|
walther@59919
|
5 |
Here is a minimum of code required for Know_Store.thy.
|
walther@59919
|
6 |
For main code see structure Method.
|
walther@59892
|
7 |
*)
|
walther@59893
|
8 |
signature METHOD_DEFINITION =
|
walther@59882
|
9 |
sig
|
walther@59903
|
10 |
type id = Spec.id;
|
walther@59903
|
11 |
val id_empty: id
|
walther@59903
|
12 |
val id_to_string: id -> string
|
walther@59903
|
13 |
|
walther@59895
|
14 |
type T
|
walther@59895
|
15 |
(*type met*)
|
walther@59895
|
16 |
val empty: T
|
walther@59895
|
17 |
(*val e_met: T*)
|
walther@59895
|
18 |
type store
|
walther@59895
|
19 |
(*type mets*)
|
walther@59897
|
20 |
val empty_store: T Store.node
|
walther@59897
|
21 |
(*val e_Mets: T Store.node*)
|
walther@59904
|
22 |
val check_unique: Check_Unique.id -> T Store.T -> unit
|
walther@59904
|
23 |
(*val check_metguh_unique: Check_Unique.id -> T Store.T -> unit*)
|
walther@59882
|
24 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59882
|
25 |
(*NONE*)
|
walther@59886
|
26 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59882
|
27 |
(*NONE*)
|
walther@59886
|
28 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59882
|
29 |
end
|
walther@59882
|
30 |
|
walther@59882
|
31 |
(**)
|
walther@59893
|
32 |
structure Meth_Def(**): METHOD_DEFINITION(**) =
|
walther@59882
|
33 |
struct
|
walther@59882
|
34 |
(**)
|
walther@59882
|
35 |
|
walther@59903
|
36 |
type id = Spec.id;
|
walther@59903
|
37 |
val id_empty = Spec.empty_meth_id;
|
walther@59903
|
38 |
val id_to_string = Spec.id_to_string;
|
walther@59903
|
39 |
|
walther@59884
|
40 |
(* data for methods stored in 'methods'-database*)
|
walther@59895
|
41 |
type T =
|
walther@59904
|
42 |
{guh : Check_Unique.id, (* unique within this isac-knowledge *)
|
walther@59884
|
43 |
mathauthors: string list, (* copyright *)
|
walther@59903
|
44 |
init : Spec.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE! *)
|
walther@59884
|
45 |
rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
|
walther@59884
|
46 |
TODO.WN0509 store fun itself, see 'type pbt' *)
|
walther@59884
|
47 |
erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
|
walther@59884
|
48 |
instead erls in "fun prep_met" *)
|
walther@59884
|
49 |
srls : Rule_Set.T, (* for evaluating list expressions in scr *)
|
walther@59884
|
50 |
crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
|
walther@59884
|
51 |
nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
|
walther@59909
|
52 |
errpats : Error_Pattern_Def.T list,(* error patterns expected in this method *)
|
walther@59884
|
53 |
calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
|
walther@59884
|
54 |
(*branch : TransitiveB set in append_problem at generation ob pblobj *)
|
walther@59884
|
55 |
scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
|
walther@59884
|
56 |
(*TODO: abstract to ?pre_model?...*)
|
walther@59884
|
57 |
prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
|
walther@59884
|
58 |
ppc : Celem4.pat list, (* items in given, find, relate;
|
walther@59884
|
59 |
items (in "#Find") which need not occur in the arg-list of a SubProblem
|
walther@59884
|
60 |
are 'copy-named' with an identifier "*'.'".
|
walther@59884
|
61 |
copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
|
walther@59884
|
62 |
see ME/calchead.sml 'fun is_copy_named'. *)
|
walther@59884
|
63 |
pre : term list (* preconditions in where *)
|
walther@59884
|
64 |
};
|
walther@59903
|
65 |
val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
|
walther@59884
|
66 |
erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
|
walther@59884
|
67 |
errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
|
walther@59903
|
68 |
val empty_store = Store.Node ("empty_meth_id", [empty],[]);
|
walther@59884
|
69 |
|
walther@59897
|
70 |
type store = (T Store.node) list;
|
walther@59882
|
71 |
|
walther@59895
|
72 |
val check_unique =
|
walther@59904
|
73 |
Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.id));
|
walther@59892
|
74 |
|
walther@59882
|
75 |
(**)end(**)
|