(* elements of calculations.

    they are partially held in association lists as ref's for

    switching language levels (meta-string, object-values).

    in order to keep these ref's during re-evaluation of code,

    they are defined here at the beginning of the code.

    Author: Walther Neuper 2003

    (c) copyright due to lincense terms

 *)

 (*

 structure CalcElems =

 struct

 *)

 val linefeed = (curry op^) "\n";

 type authors = string list;

 type cterm' = string;

 val empty_cterm' = "empty_cterm'";

 type thmID = string;    (* identifier for a thm (the shortest possible identifier)       *)

 type thmDeriv = string; (* WN120524 deprecated

   thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name 

   WN120524: dont use Thm.derivation_name, this is destroyed by num_str;

   Thm.get_name_hint survives num_str and seems perfectly reliable *)

 type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)

 type thm'' = thmID * term;

 type rls' = string;

 (*.a 'guh'='globally unique handle' is a string unique for each element

    of isac's KEStore and persistent over time

    (in particular under shifts within the respective hierarchy);

    specialty for thys:

    # guh NOT resistant agains shifts from one thy to another

    (which is the price for Isabelle's design: thy's overwrite ids of subthy's)

    # requirement for matchTheory: induce guh from tac + current thy

    (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)

    TODO: introduce to pbl, met.*)

 type guh = string;

 val e_guh = "e_guh":guh;

 type xml = string;

 (* eval function calling sml code during rewriting.

 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,

   see "fun rule2stac": instead of 

     Calc: calID * eval_fn -> rule

   would be better

     Calc: prog_calcID * (calID * eval_fn)) -> rule*)

 type eval_fn = (string -> term -> theory -> (string * term) option);

 fun e_evalfn (_:'a) (_:term) (_:theory) = NONE:(string * term) option;

 (*. op in isa-term 'Const(op,_)' .*)

 type calID = string;

 (* *)

 type cal = (calID * eval_fn);

 (*. fun calculate_ fetches the evaluation-function via this list. *)

 type prog_calcID = string;

 type calc = (prog_calcID * cal);

 type calc_elem =

   prog_calcID *   (* a simple identifier used in programs *)

   (calID *        (* a long identifier used in Const *)

     eval_fn)      (* an ML function *)

 fun calc_eq ((pi1, (ci1, _)) : calc_elem, (pi2, (ci2, _)) : calc_elem) =

   if pi1 = pi2

   then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)

   else false

 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)

 type subst = (term * term) list; (*here for ets2str*)

 val e_subst = []:(term * term) list;

 (*TODO.WN060610 make use of "type rew_ord" total*)

 type rew_ord' = string;

 val e_rew_ord' = "e_rew_ord" : rew_ord';

 type rew_ord_ = subst -> Term.term * Term.term -> bool;

 fun dummy_ord (_:subst) (_:term,_:term) = true;

 val e_rew_ord_ = dummy_ord;

 type rew_ord = rew_ord' * rew_ord_;

 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)

 val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;

 (* error patterns and fill patterns *)

 type errpatID = string

 type errpat =

   errpatID    (* one identifier for a list of patterns                       

                  DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)

   * term list (* error patterns                                              *)

   * thm list  (* thms related to error patterns; note that respective lhs 

                  do not match (which reflects student's error).

                  fillpatterns are stored with these thms.                    *)

 (* for (at least) 2 kinds of access:

   (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)

   (2) given a thm, find respective fillpats *)

 type fillpatID = string

 type fillpat =

   fillpatID   (* DESIGN ?TODO: give an order w.r.t difficulty ? *)

   * term      (* the pattern with fill-in gaps                  *)

   * errpatID; (* which the fillpat would be a help for          

                  DESIGN ?TODO: list for several patterns ?      *)

 datatype rule =

   Erule                (*.the empty rule                     .*)

 | Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*)

 | Calc of string *     (*.sml-code manipulating a (sub)term  .*)

 	  (string -> term -> theory -> (string * term) option)

 | Cal1 of string *     (*.sml-code applied only to whole term

                           or left/right-hand-side of eqality .*)

 	  (string -> term -> theory -> (string * term) option)

 | Rls_ of rls          (*.ie. rule sets may be nested.*)

 and scr =

     EmptyScr

   | Prog of term (* for met *)

   | Rfuns of     (* for Rrls, usage see rational.sml ----- reverse rewrite -----      *)

     {init_state : (* initialise for reverse rewriting by the Interpreter              *)

       term ->         (* for this the rrlsstate is initialised:                       *)

       term *          (* the current formula: goes locate_gen -> next_tac via istate  *)

       term *          (* the final formula                                            *)

       rule list       (* of reverse rewrite set (#1#)                                 *)

         list *        (*   may be serveral, eg. in norm_rational                      *)

       ( rule *        (* Thm (+ Thm generated from Calc) resulting in ...             *)

         (term *       (*   ... rewrite with ...                                       *)

         term list))   (*   ... assumptions                                            *)

       list,           (* derivation from given term to normalform

                          in reverse order with sym_thm;

                                                 (#1#) could be extracted from here #1 *)  

 	  normal_form:  (* the function which drives the Rrls ##############################*)

 	    term -> (term * term list) option,

 	  locate_rule:  (* checks a rule R for being a cancel-rule, and if it is,

                      then return the list of rules (+ the terms they are rewriting to)

                      which need to be applied before R should be applied.

                      precondition: the rule is applicable to the argument-term.       *)

 	    rule list list -> (* the reverse rule list                                      *)

 	    term ->         (* ... to which the rule shall be applied                       *)

 	    rule ->         (* ... to be applied to term                                    *)

 	    ( rule *        (* value: a rule rewriting to ...                               *)

 	      (term *       (*   ... the resulting term ...                                 *)

 	      term list))   (*   ... with the assumptions ( //#0)                           *)

 	    list,           (*   there may be several such rules; the list is empty,          

                            if the rule has nothing to do with e.g. cancelation        *)

 	  next_rule:    (* for a given term return the next rules to be done for cancelling *)

 	    rule list list->(* the reverse rule list                                        *)

 	    term ->         (* the term for which ...                                       *)

 	    rule option,    (* ... this rule is appropriate for cancellation;

 		                     there may be no such rule (if the term is eg.canceled already*)

 	  attach_form:  (* checks an input term TI, if it may belong to e.g. a current 

                      cancellation, by trying to derive it from the given term TG.     

                      NOT IMPLEMENTED                                                 *)

 	    rule list list->(**)

 	    term ->         (* TG, the last one agreed upon by user + math-eng              *)

 	    term ->         (* TI, the next one input by the user                           *)

 	    ( rule *        (* the rule to be applied in order to reach TI                  *) 

 	      (term *       (* ... obtained by applying the rule ...                        *)

 	      term list))   (* ... and the respective assumptions                           *) 

 	    list}           (* there may be several such rules; the list is empty, if the 

                          users term does not belong to e.g. a cancellation of the term 

                          last agreed upon.                                            *)

 and rls =

     Erls                          (*for init e_rls*)

   | Rls of (*a confluent and terminating ruleset, in general         *)

     {id : string,          (*for trace_rewrite:=true                 *)

      preconds : term list, (*unused WN020820                         *)

      (*WN060616 for efficiency...

       bdvs    : false,       (*set in prep_rls' for get_bdvs *)*)

      rew_ord  : rew_ord,   (*for rules*)

      erls     : rls,       (*for the conditions in rules             *)

      srls     : rls,       (*for evaluation of list_fns in script    *)

      calc     : calc list, (*for Calculate in scr, set by prep_rls'   *)

      rules    : rule list,

      errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)

      scr      : scr}       (*Prog term: generating intermed.steps  *)

   | Seq of (*a sequence of rules to be tried only once               *)

     {id : string,          (*for trace_rewrite:=true                 *)

      preconds : term list, (*unused 20.8.02                          *)

      (*WN060616 for efficiency...

       bdvs    : false,       (*set in prep_rls' for get_bdvs *)*)

      rew_ord  : rew_ord,   (*for rules                               *)

      erls     : rls,       (*for the conditions in rules             *)

      srls     : rls,       (*for evaluation of list_fns in script    *)

      calc     : calc list, (*for Calculate in scr, set by prep_rls'   *)

      rules    : rule list,

      errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)

      scr      : scr}  (*Prog term  (how to restrict type ???)*)

   (*Rrls call SML-code and simulate an rls

     difference: there is always _ONE_ redex rewritten in 1 call,

     thus wrap Rrls by: Rls (Rls_ ...)*)

   | Rrls of (* SML-functions within rewriting; step-wise execution provided;   

                Rrls simulate an rls

                difference: there is always _ONE_ redex rewritten in 1 call,

                thus wrap Rrls by: Rls (Rls_ ...)                              *)

     {id : string,          (* for trace_rewrite := true                       *)

      prepat  : (term list *(* preconds, eval with subst from pattern;

                               if [@{term True}], match decides alone          *)

 		            term )     (* pattern matched with current (sub)term          *)

 		   list,               (* meta-conjunction is or                          *)

      rew_ord  : rew_ord,   (* for rules                                       *)

      erls     : rls,       (* for the conditions in rules and preconds        *)

      calc     : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)

      errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)

      scr      : scr};      (* Rfuns {...}  (how to restrict type ???)         *)

 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)

 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)

 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)

 val e_rule = Thm ("refl", @{thm refl});

 fun id_of_thm (Thm (id, _)) = id

   | id_of_thm _ = error "error id_of_thm";

 fun thm_of_thm (Thm (_, thm)) = thm

   | thm_of_thm _ = error "error thm_of_thm";

 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);

 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);

 fun thyID_of_derivation_name dn = hd (space_explode "." dn);

 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =

     (strip_thy thmid1) = (strip_thy thmid2);

 (*WN120201 weakened*)

 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _)) = thmid1 = thmid2;

 (*version typed weaker WN100910*)

 fun eq_thmI' ((thmid1, _), (thmid2, _)) =

     (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);

 val string_of_thm =  Thm.get_name_hint; (*FIXME.2009*)

 fun thm'_of_thm thm =

   ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm'

 (*check for [.] as caused by "fun assoc_thm'"*)

 fun string_of_thmI thm =

     let val ct' = (de_quote o string_of_thm) thm

 	val (a, b) = split_nlast (5, Symbol.explode ct')

     in case b of

 	   [" ", " ","[", ".", "]"] => implode a

 	 | _ => ct'

     end;

 (*.id requested for all, Rls,Seq,Rrls.*)

 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)

   | id_rls (Rls {id,...}) = id

   | id_rls (Seq {id,...}) = id

   | id_rls (Rrls {id,...}) = id;

 val rls2str = id_rls;

 fun id_rule (Thm (id, _)) = id

   | id_rule (Calc (id, _)) = id

   | id_rule (Rls_ rls) = id_rls rls;

 fun get_rules (Rls {rules,...}) = rules

   | get_rules (Seq {rules,...}) = rules

   | get_rules (Rrls _) = [];

 fun rule2str Erule = "Erule"

   | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"

   | rule2str (Calc (str,f))  = "Calc (\""^str^"\",fn)"

   | rule2str (Cal1 (str,f))  = "Cal1 (\""^str^"\",fn)"

   | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";

 fun rule2str' Erule = "Erule"

   | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"

   | rule2str' (Calc (str,f))  = "Calc (\""^str^"\",fn)"

   | rule2str' (Cal1 (str,f))  = "Cal1 (\""^str^"\",fn)"

   | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";

 (*WN080102 compare eq_rule ?!?*)

 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2

   | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2

   | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2

   | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)

   | eqrule _ = false;

 type rrlsstate =  (* state for reverse rewriting, comments see type rule and scr | Rfuns *)

   (term * term * rule list list * (rule * (term * term list)) list);

 val e_type = Type("empty",[]);

 val a_type = TFree("'a",[]);

 val e_term = Const("empty",e_type);

 val a_term = Free("empty",a_type);

 val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;

 val e_term = Const("empty", Type("'a", []));

 val e_scr = Prog e_term;

 (*ad thm':

    there are two kinds of theorems ...

    (1) known by isabelle

    (2) not known, eg. calc_thm, instantiated rls

        the latter have a thmid "#..."

    and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)

    and have a special assoc_thm / assoc_rls in this interface      *)

 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)

 type domID = string;   (* domID ^".thy" = theory' WN.101011 replace by thyID*)

 type thyID = string;    (*WN.3.11.03 TODO: replace domID with thyID*)

 fun string_of_thy thy = Context.theory_name thy: theory';

 val theory2domID = string_of_thy;

 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;

 val theory2theory' = string_of_thy;

 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)

 val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;

 (* fun theory'2theory = fun thyID2thy ... see fun assoc_thy (...Thy_Info.get_theory string);

 al it = "Isac" : string

 *)

 fun thyID2theory' (thyID:thyID) = thyID;

 (*

     let val ss = Symbol.explode thyID

 	val ext = implode (takelast (4, ss))

     in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)

        else thyID ^ ".thy"

     end;

 *)

 (* thyID2theory' "Isac" (*ok*);

 val it = "Isac" : theory'

  > thyID2theory' "Isac" (*abuse, goes ok...*);

 val it = "Isac" : theory'

 *)

 fun theory'2thyID (theory':theory') = theory';

 (*

     let val ss = Symbol.explode theory'

 	val ext = implode (takelast (4, ss))

     in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID

        else theory' (*disarm abuse of theory'*)

     end;

 *)

 (* theory'2thyID "Isac";

 val it = "Isac" : thyID

 > theory'2thyID "Isac";

 val it = "Isac" : thyID*)

 (*. WN0509 discussion:

 #############################################################################

 #   How to manage theorys in subproblems wrt. the requirement,              #

 #   that scripts should be re-usable ?                                      #

 #############################################################################

     eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'

     which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script

     because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b

     is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard

     (see match_ags).

     Preliminary solution:

     # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,

     # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl

     # however, a thy specified by the user in the rootpbl may lead to

       errors in far-off subpbls (which are not yet reported properly !!!)

       and interactively specifiying thys in subpbl is not very relevant.

     Other solutions possible:

     # always parse and type-check with Thy_Info.get_theory "Isac"

       (rejected tue to the vague idea eg. to re-use equations for R in C etc.)

     # regard the subthy-relation in specifying thys of subpbls

     # specifically handle 'SubProblem (undefined, pbl, arglist)'

     # ???

 .*)

 (*WN0509 TODO "ProtoPure" ... would be more consistent

   with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)

 val e_domID = "e_domID":domID;

 (*the key into the hierarchy ob theory elements*)

 type theID = string list;

 val e_theID = ["e_theID"];

 val theID2str = strs2str;

 (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)

 fun theID2thyID (theID:theID) =

     if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID

     else error ("theID2thyID called with "^ theID2str theID);

 (*the key into the hierarchy ob problems*)

 type pblID = string list; (* domID::...*)

 val e_pblID = ["e_pblID"]:pblID;

 val pblID2str = strs2str;

 (*the key into the hierarchy ob methods*)

 type metID = string list;

 val e_metID = ["e_metID"]:metID;

 val metID2str = strs2str;

 type spec = 

      domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:

 	      specify (Init_Proof..), nxt_specify_init_calc,

 	      assod (.SubProblem...), stac2tac (.SubProblem...)*)

      pblID * 

      metID;

 fun spec2str ((dom,pbl,met)(*:spec*)) = 

   "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^ 

   ", " ^ (strs2str met) ^ ")";

 (*> spec2str empty_spec;

 val it = "(\"\", [], (\"\", \"\"))" : string *)

 val empty_spec = (e_domID,e_pblID,e_metID):spec;

 val e_spec = empty_spec;

 (*.association list with cas-commands, for generating a complete calc-head.*)

 type generate_fn = 

   (term list ->    (* the arguments of the cas-command, eg. (x+1=2, x) *)

     (term *        (* description of an element                        *)

       term list)   (* value of the element (always put into a list)    *)

   list)            (* of elements in the formalization                 *)

 type cas_elem = 

   (term *          (* cas-command, eg. 'solve'                         *)

     (spec *        (* theory, problem, method                          *)

     generate_fn))

 fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2

 (*either theID or pblID or metID*)

 type kestoreID = string list;

 val e_kestoreID = ["e_kestoreID"];

 val kestoreID2str = strs2str;

 (*for distinction of contexts WN130621: disambiguate with Isabelle's Context !*)

 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;

 fun ketype2str Exp_ = "Exp_"

   | ketype2str Thy_ = "Thy_"

   | ketype2str Pbl_ = "Pbl_"

   | ketype2str Met_ = "Met_";

 fun ketype2str' Exp_ = "Example"

   | ketype2str' Thy_ = "Theory"

   | ketype2str' Pbl_ = "Problem"

   | ketype2str' Met_ = "Method";

 (*see 'How to manage theorys in subproblems' at 'type thyID'*)

 val theory'  = Unsynchronized.ref ([]:(theory' * theory) list);

 (*rewrite orders, also stored in 'type met' and type 'and rls'

   The association list is required for 'rewrite.."rew_ord"..'

   WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)

 val rew_ord' = Unsynchronized.ref

         ([]:(rew_ord' *        (*the key for the association list         *)

 	     (subst 	       (*the bound variables - they get high order*)

 	      -> (term * term) (*(t1, t2) to be compared                  *)

 	      -> bool))        (*if t1 <= t2 then true else false         *)

 		list);         (*association list                         *)

 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),

 				    ("dummy_ord", dummy_ord)]);

 (* A tree for storing data defined in different theories 

   for access from the Interpreter and from dialogue authoring 

   using a string list as key.

   'a is for pbt | met | thydata; after WN030424 naming became inappropriate *)

 datatype 'a ptyp =

 	Ptyp of string * (* element of the key *)

 		'a list *      (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)

 			                presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)

 		('a ptyp) list;(* the children nodes *)

 (*.datatype for collecting thydata for hierarchy.*)

 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)

 (*WN0606 Htxt contains html which does not belong to the sml-kernel*)

 datatype thydata = Html of {guh: guh,

 			    coursedesign: authors,

 			    mathauthors: authors,

 			    html: string} (*html; for demos before database*)

 		 | Hthm of {guh: guh,

 			    coursedesign: authors,

 			    mathauthors: authors,

 			    fillpats: fillpat list,

 			    thm: term}

 		 | Hrls of {guh: guh,

 			    coursedesign: authors,

 			    mathauthors: authors,

 			    thy_rls: (thyID * rls)}

 		 | Hcal of {guh: guh,

 			    coursedesign: authors,

 			    mathauthors: authors,

 			    calc: calc}

 		 | Hord of {guh: guh,

 			    coursedesign: authors,

 			    mathauthors: authors,

 			    ord: (subst -> (term * term) -> bool)};

 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};

 fun the2str (Html {guh, coursedesign, mathauthors, html}) = guh : string

   | the2str (Hthm {guh, coursedesign, mathauthors, fillpats, thm}) = guh

   | the2str (Hrls {guh, coursedesign, mathauthors, thy_rls}) = guh

   | the2str (Hcal {guh, coursedesign, mathauthors, calc}) = guh

   | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh

 fun thes2str thes = map the2str thes |> list2str;

 type thehier = (thydata ptyp) list;

 (* required to determine sequence of main nodes of thehier in KEStore.thy *)

 fun part2guh ([str]:theID) =

     (case str of

 	"Isabelle" => "thy_isab_" ^ str ^ "-part" : guh

       | "IsacScripts" => "thy_scri_" ^ str ^ "-part"

       | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"

       | str => error ("thy2guh: called with '"^str^"'"))

   | part2guh theID = error ("part2guh called with theID = " ^ theID2str theID);

 fun thy2guh ([part, thyID] : theID) = (case part of

       "Isabelle" => "thy_isab_" ^ thyID : guh

     | "IsacScripts" => "thy_scri_" ^ thyID

     | "IsacKnowledge" => "thy_isac_" ^ thyID

     | str => error ("thy2guh: called with '" ^ str ^ "'"))

   | thy2guh theID = error ("thy2guh called with '" ^ strs2str' theID ^ "'");

 fun thypart2guh ([part, thyID, thypart] : theID) = case part of

     "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh

   | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart

   | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart

   | str => error ("thypart2guh: called with '" ^ str ^ "'");

 (* convert the data got via contextToThy to a globally unique handle

    there is another way to get the guh out of the 'theID' in the hierarchy *)

 fun thm2guh (isa, thyID:thyID) (thmID:thmID) = case isa of

     "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh

   | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID

   | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID

   | str => error ("thm2guh called with isa = '" ^ isa ^ "' for thm = " ^ thmID ^ "'");

 fun rls2guh (isa, thyID:thyID) (rls':rls') = case isa of

     "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh

   | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'

   | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'

   | str => error ("rls2guh called with isa = '" ^ isa ^ "' for rls = '" ^ rls' ^ "'");

 fun cal2guh (isa, thyID:thyID) calID = case isa of

     "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh

   | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID

   | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID

   | str => error ("cal2guh called with isa = '" ^ isa ^ "' for cal = '" ^ calID ^ "'");

 fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') = case isa of

     "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh

   | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'

   | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'

   | str => error ("ord2guh called with isa = '" ^ isa ^ "' for ord = '" ^ rew_ord' ^ "'");

 (* not only for thydata, but also for thy's etc *)

 fun theID2guh (theID : theID) = case length theID of

     0 => error ("theID2guh: called with theID = " ^ strs2str' theID)

   | 1 => part2guh theID

   | 2 => thy2guh theID

   | 3 => thypart2guh theID

   | 4 => 

     let val [isa, thyID, typ, elemID] = theID

     in case typ of

         "Theorems" => thm2guh (isa, thyID) elemID

       | "Rulesets" => rls2guh (isa, thyID) elemID

       | "Calculations" => cal2guh (isa, thyID) elemID

       | "Orders" => ord2guh (isa, thyID) elemID

       | "Theorems" => thy2guh [isa, thyID]

       | str => error ("theID2guh: called with theID = " ^ strs2str' theID)

     end

   | n => error ("theID2guh called with theID = " ^ strs2str' theID);

 (* an association list, gets the value once in Isac.ML.

    stores Isabelle's thms as terms for compatibility with Theory.axioms_of.

    WN1-1-28 make this data arguments and del ref ?*)

 val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);

 val isabthys = Unsynchronized.ref ([] : theory list);

 type path = string;

 type filename = string;

 (*val xxx = fn: a b => (a,b);   ??? fun-definition ???*)

 local

     fun ii (_:term) = e_rrlsstate;

     fun no (_:term) = SOME (e_term,[e_term]);

     fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];

     fun ne (_:rule list list) (_:term) = SOME e_rule;

     fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];

 in

 val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,

 		     next_rule=ne,attach_form=fo};

 end;

 val e_rls =

   Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,

     srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls;

 val e_rrls =

   Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,

     calc = [], errpatts = [], scr=e_rfuns}:rls;

 fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =

   {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,

    (*asm_thm=asm_thm,*)rules=rules,scr=scr}

   | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) =

   {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,

    (*asm_thm=asm_thm,*)rules=rules,scr=scr}

   | rep_rls Erls = rep_rls e_rls

   | rep_rls (Rrls {id,...})  = rep_rls e_rls

     (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);

 (*| rep_rls (Seq {id,...})  =

     error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);

 --1.7.03*)

 fun rep_rrls (Rrls {id, calc, erls, prepat, rew_ord, errpatts,

 	      scr = Rfuns {attach_form, init_state, locate_rule, next_rule, normal_form}}) =

   {id=id, calc=calc, erls=erls, prepat=prepat,

      rew_ord=rew_ord, errpatts=errpatts, attach_form=attach_form, init_state=init_state,

      locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}

   | rep_rrls (Rls {id,...}) =

     error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)

   | rep_rrls (Seq {id,...}) =

     error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);

 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 			rules =rs, errpatts=errpatts, scr=sc}) r =

     (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 	 rules = rs @ r, errpatts=errpatts, scr=sc}:rls)

   | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 			rules =rs, errpatts=errpatts, scr=sc}) r =

     (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 	 rules = rs @ r, errpatts=errpatts, scr=sc}:rls)

   | append_rls id (Rrls _) _ =

     error ("append_rls: not for reverse-rewrite-rule-set "^id);

 (*. are _atomic_ rules equal ?.*)

 (*WN080102 compare eqrule ?!?*)

 fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2

   | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2

   | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2

   (*id_rls checks for Rls, Seq, Rrls*)

   | eq_rule _ = false;

 fun merge_ids rls1 rls2 =

   let 

     val id1 = (#id o rep_rls) rls1

     val id2 = (#id o rep_rls) rls2

   in

     if id1 = id2 then id1

     else "merged_" ^ id1 ^ "_" ^ id2

   end

 fun merge_rls _ Erls rls = rls

   | merge_rls _ rls Erls = rls

   | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)

   | merge_rls _ _ (Rrls x) = Rrls x

   | merge_rls id

 	  (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,

 	    rules = rs1, errpatts = eps1, scr = sc1, ...})

 	  (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,

 	    rules = rs2, errpatts = eps2, ...})

     =

 	  (Rls {id = id, rew_ord = ro1, scr = sc1,

 	    preconds = union (op =) pc1 pc2,	    

 	    erls = merge_rls (merge_ids er1 er2) er1 er2,

 	    srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,

 	    calc = union calc_eq ca1 ca2,

 		  rules = union eq_rule rs1 rs2,

       errpatts = union (op =) eps1 eps2} : rls)

   | merge_rls id

 	  (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,

 	    rules = rs1, errpatts = eps1, scr = sc1, ...})

 	  (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,

 	    rules = rs2, errpatts = eps2, ...})

     =

 	  (Seq {id = id, rew_ord = ro1, scr = sc1,

 	    preconds = union (op =) pc1 pc2,	    

 	    erls = merge_rls (merge_ids er1 er2) er1 er2,

 	    srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,

 	    calc = union calc_eq ca1 ca2,

 		  rules = union eq_rule rs1 rs2,

       errpatts = union (op =) eps1 eps2} : rls)

   | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^ 

     "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");

 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 		     rules=rs, errpatts=eps, scr=sc}) r =

     (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 	   rules = gen_rems eq_rule (rs, r),

 	   errpatts = eps(*gen_rems op= (eps, TODO)*),

 	 scr=sc}:rls)

   | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 		     rules =rs, errpatts=eps, scr=sc}) r =

     (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

 	   rules = gen_rems eq_rule (rs, r),

 	   errpatts = eps(*gen_rems op= (eps, TODO)*),

 	 scr=sc}:rls)

   | remove_rls id (Rrls _) _ = error

                    ("remove_rls: not for reverse-rewrite-rule-set "^id);

 (* datastructure for KEStore_Elems, intermediate for thehier *)

 type rlss_elem = 

   (rls' *     (* identifier unique within Isac *)

   (theory' *  (* just for assignment in thehier, not appropriate for parsing etc *)

     rls))     (* ((#id o rep_rls) rls) = rls'   by coding discipline *)

 fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2

 fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys = 

   case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of

     NONE => re :: ys

   | SOME (i, (_, (_, r2))) => 

       let

         val r12 = merge_rls id r1 r2

       in list_update ys i (id, (thyID, r12)) end

 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;

 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)

   | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)

   | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));

 fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")

   | assoc' ((keyi, xi) :: pairs, key) =

       if key = keyi then SOME xi else assoc' (pairs, key);

 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))

   handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)

 fun assoc_thy (thy:theory') =

     if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)

     else (Thy_Info.get_theory thy)

          handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");

 (*.overwrite an element in an association list and pair it with a thyID

    in order to create the thy_hierarchy;

    overwrites existing rls' even if they are defined in a different thy;

    this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)

 (*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that

    they do NOT handle overlays by re-using an identifier in different thys;

    "thyID.rlsID" would be a good solution, if the "." would be possible

    in scripts...

    actually a hack to get alltogether run again with minimal effort*)

 fun insthy thy' (rls', rls) = (rls', (thy', rls));

 fun overwritelthy thy (al, bl:(rls' * rls) list) =

     let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl

     in overwritel (al, bl') end;

 fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))

   handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");

 (*get the string for stac from rule*)

 fun term_to_string' ctxt t =

   let

     val ctxt' = Config.put show_markup false ctxt

   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

 fun term_to_string'' (thyID : thyID) t =

   let

     val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))

   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

 fun term_to_string''' thy t =

   let

     val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)

   in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

 fun term2str t = term_to_string' (assoc_thy "Isac" |> thy2ctxt) t;

 fun terms2strs ts = map term2str ts;

 (*terms2strs [t1,t2] = ["1 + 2", "abc"];*)

 val terms2str = strs2str o terms2strs;

 (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)

 val terms2str' = strs2str' o terms2strs;

 (*terms2str' [t1,t2] = "[1 + 2,abc]";*)

 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"

   | termopt2str NONE = "NONE";

 fun type_to_string' ctxt t =

   let

     val ctxt' = Config.put show_markup false ctxt

   in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;

 fun type_to_string'' (thyID : thyID) t =

   let

     val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))

   in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;

 fun type_to_string''' thy t =

   let

     val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)

   in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;

 fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)

 val string_of_typ = type2str; (*legacy*)

 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)

 fun subst2str (s:subst) =

     (strs2str o

      (map (linefeed o pair2str o

 	   (apsnd term2str) o

 	   (apfst term2str)))) s;

 fun subst2str' (s:subst) =

     (strs2str' o

      (map (pair2str o

 	   (apsnd term2str) o

 	   (apfst term2str)))) s;

 (*> subst2str' [(str2term "bdv", str2term "x"),

 		(str2term "bdv_2", str2term "y")];

 val it = "[(bdv, x)]" : string

 *)

 val env2str = subst2str;

 (*recursive defs:*)

 fun scr2str (Prog s) = "Prog " ^ term2str s

   | scr2str (Rfuns _)  = "Rfuns";

 fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;

 (*.trace internal steps of isac's rewriter*)

 val trace_rewrite = Unsynchronized.ref false;

 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)

 val depth = Unsynchronized.ref 99999;

 (*.no of rewrites exceeding this int -> NO rewrite.*)

 (*WN060829 still unused...*)

 val lim_rewrite = Unsynchronized.ref 99999;

 (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)

 val lim_deriv = Unsynchronized.ref 100;

 (*.switch for checking guhs unique before storing a pbl or met;

    set true at startup (done at begin of ROOT.ML)

    set false for editing IsacKnowledge (done at end of ROOT.ML).*)

 val check_guhs_unique = Unsynchronized.ref true;

 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)

 	 L     (*go left at $*)

        | R     (*go right at $*)

        | D;     (*go down at Abs*)

 type loc_ = lrd list;

 fun ldr2str L = "L"

   | ldr2str R = "R"

   | ldr2str D = "D";

 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;

 (* the pattern for an item of a problems model or a methods guard *)

 type pat =

   (string *     (* field               *)

 	  (term *     (* description         *)

 	     term))   (* id | arbitrary term *);

 fun pat2str ((field, (dsc, id)) : pat) = 

   pair2str (field, pair2str (term2str dsc, term2str id))

 fun pats2str pats = (strs2str o (map pat2str)) pats

 (* types for problems models (TODO rename to specification models) *)

 type pbt_ =

   (string *   (* field "#Given",..*)(*deprecated due to 'type pat'*)

     (term *   (* description      *)

       term)); (* id | struct-var  *)

 val e_pbt_ = ("#Undef", (e_term, e_term)) : pbt_

 type pbt = 

   {guh : guh,         (* unique within this isac-knowledge *)

   mathauthors : string list, (* copyright *)

   init : pblID,       (* to start refinement with *)

   thy  : theory,      (* which allows to compile that pbt

                       TODO: search generalized for subthy (ref.p.69*)

                       (*^^^ WN050912 NOT used during application of the problem,

                       because applied terms may be from 'subthy' as well as from super;

                       thus we take 'maxthy'; see match_ags !*)

   cas : term option,  (* 'CAS-command'*)

   prls : rls,         (* for preds in where_*)

   where_ : term list, (* where - predicates*)

   ppc : pat list,     (* this is the model-pattern; 

                        it contains "#Given","#Where","#Find","#Relate"-patterns

                        for constraints on identifiers see "fun cpy_nam" *)

   met : metID list}   (* methods solving the pbt*)

 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",

   cas = NONE, prls = Erls, where_ = [], ppc = [], met = []} : pbt

 fun pbt2str

         ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',

           prls = prls', thy = thy', where_ = w'} : pbt) =

       "{cas = " ^ (termopt2str cas') ^  ", guh = \"" ^ guh'  ^ "\", init = "

         ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "

         ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "

         ^ (rls2str prls' |> quote) ^ ", thy = {" ^ (theory2str thy') ^ "}, where_ = "

         ^ (terms2str w') ^ "}" |> linefeed;

 fun pbts2str pbts = map pbt2str pbts |> list2str;

 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[])

 type ptyps = (pbt ptyp) list

 fun coll_pblguhs pbls =

     let fun node coll (Ptyp (_,[n],ns)) =

 	    [(#guh : pbt -> guh) n] @ (nodes coll ns)

 	and nodes coll [] = coll

 	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);

     in nodes [] pbls end;

 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =

     if member op = (coll_pblguhs pbls) guh

     then error ("check_guh_unique failed with '"^guh^"';\n"^

 		      "use 'sort_pblguhs()' for a list of guhs;\n"^

 		      "consider setting 'check_guhs_unique := false'")

     else ();

 fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]

   | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =

 ((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)

      if k=k'

      then ((Ptyp (k', [pbt], ps))::pys)

      else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)

 	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))

 )			 

   | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =

 ((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)

      if k=k'

      then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)

      else 

 	 if length pys = 0

 	 then error ("insert: not found "^(strs2str (d:pblID)))

 	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))

 );

 fun update_ptyps ID _ _ [] =

     error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")

   | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =

     if i = key

     then 

       if length pys = 0

       then ((Ptyp (key, [data], [])) :: pyss)

       else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")

     else py :: update_ptyps ID [i] data pyss

   | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =

     if i = key

     then ((Ptyp (key,  d, update_ptyps ID is data pys)) :: pyss)

     else (py :: (update_ptyps ID (i :: is) data pyss))

 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge

   function for trees / ptyps *)

 fun merge_ptyps ([], pt) = pt

   | merge_ptyps (pt, []) = pt

   | merge_ptyps ((x' as Ptyp (k, x, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =

       if k = k'

       then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)

       else x' :: merge_ptyps (xs, xs');

 fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2)

 (* data for methods stored in 'methods'-database*)

 type met = 

      {guh        : guh,        (*unique within this isac-knowledge           *)

       mathauthors: string list,(*copyright                                   *)

       init       : pblID,      (*WN060721 introduced mistakenly--TODO.REMOVE!*)

       rew_ord'   : rew_ord',   (*for rules in Detail

 			                           TODO.WN0509 store fun itself, see 'type pbt'*)

       erls       : rls,        (*the eval_rls for cond. in rules FIXME "rls'

 				                         instead erls in "fun prep_met"              *)

       srls       : rls,        (*for evaluating list expressions in scr      *)

       prls       : rls,        (*for evaluating predicates in modelpattern   *)

       crls       : rls,        (*for check_elementwise, ie. formulae in calc.*)

       nrls       : rls,        (*canonical simplifier specific for this met  *)

       errpats    : errpat list,(*error patterns expected in this method      *)

       calc       : calc list,  (*Theory_Data in fun prep_met                 *)

       (*branch   : TransitiveB set in append_problem at generation ob pblobj

           FIXXXME.0308: set branch from met in Apply_Method ?                *)

       ppc        : pat list,   (*.items in given, find, relate;

 	      items (in "#Find") which need not occur in the arg-list of a SubProblem

         are 'copy-named' with an identifier "*'.'".

         copy-named items are 'generating' if they are NOT "*'''" ?WN120516??

         see ME/calchead.sml 'fun is_copy_named'.                              *)

       pre        : term list,  (*preconditions in where                       *)

       scr        : scr         (*prep_met gets progam or string "empty_script"*)

 	   };

 val e_met = {guh="met_empty",mathauthors=[],init=e_metID,

 	     rew_ord' = "e_rew_ord'": rew_ord',

 	      erls = e_rls, srls = e_rls, prls = e_rls,

 	      calc = [], crls = e_rls, errpats = [], nrls= e_rls,

 	      ppc = []: (string * (term * term)) list,

 	      pre = []: term list,

 	      scr = EmptyScr: scr}:met;

 val e_Mets = Ptyp ("e_metID",[e_met],[]);

 type mets = (met ptyp) list;

 fun coll_metguhs mets =

     let fun node coll (Ptyp (_,[n],ns)) =

 	    [(#guh : met -> guh) n] @ (nodes coll ns)

 	and nodes coll [] = coll

 	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);

     in nodes [] mets end;

 (* val (guh, mets) = ("met_test", !mets);

    *)

 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =

     if member op = (coll_metguhs mets) guh

     then error ("check_guh_unique failed with '"^guh^"';\n"^

 		      "use 'sort_metguhs()' for a list of guhs;\n"^

 		      "consider setting 'check_guhs_unique := false'")

     else ();

 (* for preserving elements created by 'fun store_thy' *)

 fun exist_the (theID : theID) (thy_hie : thehier) =

   let 

     fun node theID ids (Ptyp (id, _, ns)) =

       if theID = ids @ [id] then true else nodes theID (ids @ [id]) ns

     and nodes _ _ [] = false

       | nodes theID ids (n::ns) =

         if node theID ids n then true else nodes theID ids ns

   in nodes theID [] thy_hie end;

 (* insrt requires a parent; see 'fun fill_parents' *)

 fun can_insert (theID : theID) (thy_hie : thehier) = 

   (insrt theID e_thydata theID thy_hie; true)

     handle _ => false;

 (* cut 'theID', the ID of theory elements from tail to head

    until insertion into the hierarchy of theory elements 'th' is possible

    (the hierarchy requires the parentnode to exist for insertion) *)

 fun cut_theID th ([] : theID) = error "could not insert into thy-hierarchy"

   | cut_theID th theID  = 

     if can_insert theID th

     then theID else cut_theID th (drop_last theID);

 (* insert empty parents 'Html' into the hierarchy of theory elements 'th'

    until the actual node can be inserted with key 'theID' *)

 fun fill_parents th cutID theID =

   let val cutID' = cut_theID th cutID

   in if cutID' = theID

     then th

     else 

       let 

         val th' = insrt cutID' (Html {guh=theID2guh theID, coursedesign = ["isac team 2006"],

           mathauthors = [], html = ""}) cutID' th

         val cutID_ = cutID' @ [nth ((length cutID') + 1) theID]

       in fill_parents th' cutID_ theID end

   end;

 (* argument 1 "th : thehier": contains some thydata from "setup {* KEStore_Elems.add_thes ..."

    argument 1 "th : thehier": contains some thydata from "store_thes ..."

       already in some "ProgLang/*.thy" or "Knowledge/*.thy"

    argument 2 "(theID, thydata)::_ : (theID * thydata) list: contains thydata collected

       automatically in Build_Thydata.thy finally.

    parents of thydata in list, missing in thehier, are inserted 

       (causing msgs '*** insert: not found');

    (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)

 fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)

   let

     fun add_the th ((thydata, theID)) =

       if can_insert theID th 

       then

         if exist_the theID th

         then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))

         else insrt theID thydata theID

       else

         let

           val th' = fill_parents th theID theID (*..*** insert: not found*)

           val th' = insrt theID thydata theID th'

         in merge_ptyps' th' end;

 in fold (add_the th) thes end

 fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =

   Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

     fillpats = fillpats', thm = thm}

   | update_hthm _ _ = raise ERROR "wrong data";

 (* for interface for dialog-authoring *)

 fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =

   let

     val rls' = 

       case rls of

         Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>

           Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

             calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

       | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>

             Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

               calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}

       | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>

             Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,

               scr = scr, errpatts = errpatIDs}

       | Erls => Erls

   in

     Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,

       thy_rls = (thyID, rls')}

   end

   | update_hrls _ _ = raise ERROR "wrong data";

 fun app_py p f (d:pblID) (k(*:pblRD*)) = let

     fun py_err _ =

           error ("app_py: not found: " ^ (strs2str d));

     fun app_py' _ [] = py_err ()

       | app_py' [] _ = py_err ()

       | app_py' [k0] ((p' as Ptyp (k', _, _  ))::ps) =

           if k0 = k' then f p' else app_py' [k0] ps

       | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =

           if k0 = k'' then app_py' ks ps else app_py' k' ps';

   in app_py' k p end;

 fun get_py p = let

         fun extract_py (Ptyp (_, [py], _)) = py

           | extract_py _ = error ("extract_py: Ptyp has wrong format.");

       in app_py p extract_py end;

 (*

 fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)

   let

     fun update_elem th (theID, fillpats) =

       let

         val hthm = get_py th theID theID

         val hthm' = update_hthm hthm fillpats

           handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")

       in update_ptyps theID theID hthm' end

   in fold (update_elem th) fis end

   *)

 (*

 end (*struct*)

 *)