1.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Sun Jun 14 15:39:55 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Mon Jun 29 15:43:35 2020 +0200
1.3 @@ -37,31 +37,24 @@
1.4 val id_empty = References_Def.empty_meth_id;
1.5 val id_to_string = References_Def.id_to_string;
1.6
1.7 -(* data for methods stored in 'methods'-database*)
1.8 -type T =
1.9 - {guh : Check_Unique.id, (* unique within this isac-knowledge *)
1.10 - mathauthors: string list, (* copyright *)
1.11 - init : References_Def.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE! *)
1.12 - rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
1.13 - TODO.WN0509 store fun itself, see 'type pbt' *)
1.14 - erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
1.15 - instead erls in "fun prep_met" *)
1.16 - srls : Rule_Set.T, (* for evaluating list expressions in scr *)
1.17 - crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
1.18 - nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
1.19 - errpats : Error_Pattern_Def.T list,(* error patterns expected in this method *)
1.20 - calc : Rule_Def.calc list,(* Theory_Data in fun prep_met *)
1.21 - (*branch : TransitiveB set in append_problem at generation ob pblobj *)
1.22 - scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
1.23 -(*TODO: abstract to ?pre_model?...*)
1.24 - prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
1.25 - ppc : Model_Pattern.T, (* items in given, find, relate;
1.26 - items (in "#Find") which need not occur in the arg-list of a SubProblem
1.27 - are 'copy-named' with an identifier "*'.'".
1.28 - copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
1.29 - see ME/calchead.sml 'fun is_copy_named'. *)
1.30 - pre : term list (* preconditions in where *)
1.31 - };
1.32 +(* data for methods stored in 'methods'-database *)
1.33 +type T = (* TODO WN200620: review ---------------------vvvvv *)
1.34 + {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *)
1.35 + mathauthors: string list, (* copyright *)
1.36 + init : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly *)
1.37 + rew_ord' : Rule_Def.rew_ord', (* for ordered rewriting by Tactic.Rewrite *)
1.38 + erls : Rule_Set.T, (* for conditions in rewriting by Tactic.Rewrite *)
1.39 + srls : Rule_Set.T, (* for evaluating Prog_Expr *)
1.40 + crls : Rule_Set.T, (* DEL: for check_elementwise *)
1.41 + nrls : Rule_Set.T, (* for rewriting by Tactic.Rewrite *)
1.42 + errpats : Error_Pattern_Def.T list, (* error patterns expected in this method *)
1.43 + calc : Rule_Def.calc list,(* ?DEL *)
1.44 + scr : Rule.program, (* filled in Method.prep_input *)
1.45 + prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
1.46 + ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate"
1.47 + for constraints on identifiers see "O_Model.cpy_nam" *)
1.48 + pre : term list (* ? DEL, as soon as they are input interactively ? *)
1.49 + };
1.50 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
1.51 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
1.52 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};