596 then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys) |
596 then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys) |
597 else x' :: merge_ptyps (xs, xs'); |
597 else x' :: merge_ptyps (xs, xs'); |
598 |
598 |
599 (* data for methods stored in 'methods'-database*) |
599 (* data for methods stored in 'methods'-database*) |
600 type met = |
600 type met = |
601 {guh : guh, (*unique within this isac-knowledge *) |
601 {guh : guh, (* unique within this isac-knowledge *) |
602 mathauthors: string list, (*copyright *) |
602 mathauthors: string list, (* copyright *) |
603 init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*) |
603 init : pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *) |
604 rew_ord' : Rule.rew_ord', (*for rules in Detail |
604 rew_ord' : Rule.rew_ord', (* for rules in Detail |
605 TODO.WN0509 store fun itself, see 'type pbt'*) |
605 TODO.WN0509 store fun itself, see 'type pbt' *) |
606 erls : Rule.rls, (*the eval_rls for cond. in rules FIXME "rls' |
606 erls : Rule.rls, (* the eval_rls for cond. in rules FIXME "rls' |
607 instead erls in "fun prep_met" *) |
607 instead erls in "fun prep_met" *) |
608 srls : Rule.rls, (*for evaluating list expressions in scr *) |
608 srls : Rule.rls, (* for evaluating list expressions in scr *) |
609 prls : Rule.rls, (*for evaluating predicates in modelpattern *) |
609 prls : Rule.rls, (* for evaluating predicates in modelpattern *) |
610 crls : Rule.rls, (*for check_elementwise, ie. formulae in calc.*) |
610 crls : Rule.rls, (* for check_elementwise, ie. formulae in calc. *) |
611 nrls : Rule.rls, (*canonical simplifier specific for this met *) |
611 nrls : Rule.rls, (* canonical simplifier specific for this met *) |
612 errpats : Rule.errpat list,(*error patterns expected in this method *) |
612 errpats : Rule.errpat list,(* error patterns expected in this method *) |
613 calc : Rule.calc list, (*Theory_Data in fun prep_met *) |
613 calc : Rule.calc list, (* Theory_Data in fun prep_met *) |
614 (*branch : TransitiveB set in append_problem at generation ob pblobj |
614 (*branch : TransitiveB set in append_problem at generation ob pblobj *) |
615 FIXXXME.0308: set branch from met in Apply_Method ? *) |
615 ppc : pat list, (* items in given, find, relate; |
616 ppc : pat list, (*.items in given, find, relate; |
|
617 items (in "#Find") which need not occur in the arg-list of a SubProblem |
616 items (in "#Find") which need not occur in the arg-list of a SubProblem |
618 are 'copy-named' with an identifier "*'.'". |
617 are 'copy-named' with an identifier "*'.'". |
619 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
618 copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? |
620 see ME/calchead.sml 'fun is_copy_named'. *) |
619 see ME/calchead.sml 'fun is_copy_named'. *) |
621 pre : term list, (*preconditions in where *) |
620 pre : term list, (* preconditions in where *) |
622 scr : Rule.scr (*prep_met gets progam or string "empty_script" *) |
621 scr : Rule.scr (* prep_met gets progam or string "empty_script" *) |
623 }; |
622 }; |
624 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'", |
623 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'", |
625 erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls, |
624 erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls, |
626 errpats = [], nrls = Rule.e_rls, ppc = [], pre = [], scr = Rule.EmptyScr}; |
625 errpats = [], nrls = Rule.e_rls, ppc = [], pre = [], scr = Rule.EmptyScr}; |
627 val e_Mets = Ptyp ("e_metID", [e_met],[]); |
626 val e_Mets = Ptyp ("e_metID", [e_met],[]); |