1 (* Title: BaseDefinitions/problem-def.sml |
|
2 Author: Walther Neuper |
|
3 (c) due to copyright terms |
|
4 |
|
5 Will be enhanced by Problem later. |
|
6 *) |
|
7 signature CALCELEMENT_5 = |
|
8 sig |
|
9 type pbt |
|
10 type ptyps |
|
11 val pbts2str: pbt list -> string |
|
12 val e_Ptyp: pbt Store.ptyp |
|
13 (*vvv check_unique*) |
|
14 val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit |
|
15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
|
16 val e_pbt: pbt |
|
17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
|
18 (*NONE*) |
|
19 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
|
20 end |
|
21 |
|
22 (**) |
|
23 structure Celem5(**): CALCELEMENT_5(**) = |
|
24 struct |
|
25 (**) |
|
26 |
|
27 (*/------- to Celem5 -------\*) |
|
28 type pbt = |
|
29 {guh : Check_Unique.guh, (* unique within this isac-knowledge *) |
|
30 mathauthors : string list, (* copyright *) |
|
31 init : Spec.pblID, (* to start refinement with *) |
|
32 thy : theory, (* which allows to compile that pbt |
|
33 TODO: search generalized for subthy (ref.p.69*) |
|
34 (*^^^ WN050912 NOT used during application of the problem, |
|
35 because applied terms may be from 'subthy' as well as from super; |
|
36 thus we take 'maxthy'; see match_ags ! *) |
|
37 cas : term option, (* 'CAS-command' *) |
|
38 met : Spec.metID list, (* methods solving the pbt *) |
|
39 (*TODO: abstract to ?pre_model?...*) |
|
40 prls : Rule_Set.T, (* for preds in where_ *) |
|
41 where_ : term list, (* where - predicates *) |
|
42 ppc : Celem4.pat list (* this is the model-pattern; |
|
43 it contains "#Given","#Where","#Find","#Relate"-patterns |
|
44 for constraints on identifiers see "fun cpy_nam" *) |
|
45 } |
|
46 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure", |
|
47 cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt |
|
48 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc', |
|
49 prls = prls', thy = thy', where_ = w'} : pbt) |
|
50 = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = " |
|
51 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = " |
|
52 ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = " |
|
53 ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = " |
|
54 ^ (UnparseC.terms w') ^ "}" |> linefeed; |
|
55 fun pbts2str pbts = map pbt2str pbts |> list2str; |
|
56 (*\------- to Celem5 -------/*) |
|
57 (*/------- to Celem5 -------\*) |
|
58 val e_Ptyp = Store.Ptyp ("e_pblID", [e_pbt], []) |
|
59 type ptyps = (pbt Store.ptyp) list |
|
60 (*\------- to Celem5 -------/*) |
|
61 |
|
62 val check_pblguh_unique = |
|
63 Check_Unique.messsage (Check_Unique.collect (#guh : pbt -> Check_Unique.guh)); |
|
64 |
|
65 (**)end(**) |
|