35 |
35 |
36 type id = References_Def.id; |
36 type id = References_Def.id; |
37 val id_empty = References_Def.empty_meth_id; |
37 val id_empty = References_Def.empty_meth_id; |
38 val id_to_string = References_Def.id_to_string; |
38 val id_to_string = References_Def.id_to_string; |
39 |
39 |
40 (* data for methods stored in 'methods'-database*) |
40 (* data for methods stored in 'methods'-database *) |
41 type T = |
41 type T = (* TODO WN200620: review ---------------------vvvvv *) |
42 {guh : Check_Unique.id, (* unique within this isac-knowledge *) |
42 {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *) |
43 mathauthors: string list, (* copyright *) |
43 mathauthors: string list, (* copyright *) |
44 init : References_Def.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE! *) |
44 init : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly *) |
45 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail |
45 rew_ord' : Rule_Def.rew_ord', (* for ordered rewriting by Tactic.Rewrite *) |
46 TODO.WN0509 store fun itself, see 'type pbt' *) |
46 erls : Rule_Set.T, (* for conditions in rewriting by Tactic.Rewrite *) |
47 erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls' |
47 srls : Rule_Set.T, (* for evaluating Prog_Expr *) |
48 instead erls in "fun prep_met" *) |
48 crls : Rule_Set.T, (* DEL: for check_elementwise *) |
49 srls : Rule_Set.T, (* for evaluating list expressions in scr *) |
49 nrls : Rule_Set.T, (* for rewriting by Tactic.Rewrite *) |
50 crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *) |
50 errpats : Error_Pattern_Def.T list, (* error patterns expected in this method *) |
51 nrls : Rule_Set.T, (* canonical simplifier specific for this met *) |
51 calc : Rule_Def.calc list,(* ?DEL *) |
52 errpats : Error_Pattern_Def.T list,(* error patterns expected in this method *) |
52 scr : Rule.program, (* filled in Method.prep_input *) |
53 calc : Rule_Def.calc list,(* Theory_Data in fun prep_met *) |
53 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *) |
54 (*branch : TransitiveB set in append_problem at generation ob pblobj *) |
54 ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate" |
55 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *) |
55 for constraints on identifiers see "O_Model.cpy_nam" *) |
56 (*TODO: abstract to ?pre_model?...*) |
56 pre : term list (* ? DEL, as soon as they are input interactively ? *) |
57 prls : Rule_Set.T, (* for evaluating predicates in modelpattern *) |
57 }; |
58 ppc : Model_Pattern.T, (* items in given, find, relate; |
|
59 items (in "#Find") which need not occur in the arg-list of a SubProblem |
|
60 are 'copy-named' with an identifier "*'.'". |
|
61 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
|
62 see ME/calchead.sml 'fun is_copy_named'. *) |
|
63 pre : term list (* preconditions in where *) |
|
64 }; |
|
65 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord', |
58 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord', |
66 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty, |
59 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty, |
67 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog}; |
60 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog}; |
68 val empty_store = Store.Node ("empty_meth_id", [empty],[]); |
61 val empty_store = Store.Node ("empty_meth_id", [empty],[]); |
69 |
62 |