(* 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

 *)

 signature CALC_ELEMENT =

   sig

     type cas_elem

     type pbt

     type ptyps

     type metID

     type pblID

     type mets

     type met

     datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list

     type authors

     type guh

     val env2str: Rule.subst -> string

     val subst2str: Rule.subst -> string

     val subst2str': Rule.subst -> string

     type fillpat

     datatype thydata

       = Hcal of {calc: Rule.calc, coursedesign: authors, guh: guh, mathauthors: authors}

       | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}

       | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule.rls}

       | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}

       | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}

     type theID

     type rlss_elem

     val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list

     val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool

     type spec

     val cas_eq: cas_elem * cas_elem -> bool

     val e_Ptyp: pbt ptyp

     val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list

     val check_guhs_unique: bool Unsynchronized.ref

     val check_pblguh_unique: guh -> pbt ptyp list -> unit

     val insrt: pblID -> 'a -> string list -> 'a ptyp list -> 'a ptyp list

     val e_Mets: met ptyp

     val check_metguh_unique: guh -> met ptyp list -> unit

     val add_thydata: string list * string list -> thydata -> thydata ptyp list -> thydata ptyp list

     val get_py: 'a ptyp list -> pblID -> string list -> 'a

     val update_hthm: thydata -> fillpat list -> thydata

     val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list

     val part2guh: theID -> guh

     val spec2str: string * string list * string list -> string

     val linefeed: string -> string

     val pbts2str: pbt list -> string

     val thes2str: thydata list -> string

     val theID2str: string list -> string

     val the2str: thydata -> string

     val trace_calc: bool Unsynchronized.ref

     eqtype thmID

     type thm'

     datatype lrd = D | L | R

     val trace_rewrite: bool Unsynchronized.ref

     val depth: int Unsynchronized.ref

     val id_rls: Rule.rls -> string

     val rls2str: Rule.rls -> string

     type errpat

     val assoc_thy: Rule.theory' -> theory

     eqtype cterm'

     type loc_

     val loc_2str: loc_ -> string

     eqtype rew_ord'

     type thm''

     val metID2str: string list -> string

     val e_pblID: pblID

     val e_metID: metID

     val empty_spec: spec

     val e_spec: spec

     datatype ketype = Exp_ | Met_ | Pbl_ | Thy_

     type kestoreID

     val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b

     val ketype2str: ketype -> string

     val coll_pblguhs: pbt ptyp list -> guh list

     val coll_metguhs: met ptyp list -> guh list

     type pat

     val pats2str: pat list -> string

     val maxthy: theory -> theory -> theory

     eqtype filename

     val lim_deriv: int Unsynchronized.ref

     val id_of_thm: Rule.rule -> string

     val isabthys: unit -> theory list

     val thyID_of_derivation_name: string -> string

     val partID': Rule.theory' -> string

     val thm2guh: string * Rule.thyID -> thmID -> guh

     val thmID_of_derivation_name: string -> string

     val rls2guh: string * Rule.thyID -> Rule.rls' -> guh

     val theID2guh: theID -> guh

     eqtype fillpatID

     type pbt_ = string * (term * term)

     val e_rew_ord: Rule.subst -> term * term -> bool

     eqtype xml

     val cal2guh: string * Rule.thyID -> string -> guh

     val ketype2str': ketype -> string

     val str2ketype': string -> ketype

     val thmID_of_derivation_name': thm -> string

     eqtype path

     val theID2thyID: theID -> Rule.thyID

     val thy2guh: theID -> guh

     val thypart2guh: theID -> guh

     val ord2guh: string * Rule.thyID -> rew_ord' -> guh

     val update_hrls: thydata -> Rule.errpatID list -> thydata

     eqtype iterID

     eqtype calcID

     val thm''_of_thm: thm -> thm''

     val rew_ord': (rew_ord' * (Rule.subst -> term * term -> bool)) list Unsynchronized.ref

     val thm_of_thm: Rule.rule -> thm

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

     val thm2str: thm -> string

     val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->

       thydata ptyp list

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

     val knowthys: unit -> theory list

     val e_pbt: pbt

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

 val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->

   (Rule.rls' * (string * Rule.rls)) list  end

 (**)

 structure Celem(*: CALC_ELEMENT*) =

 struct

 (**)

 val linefeed = (curry op^) "\n"; (* ?\<longrightarrow> libraryC ?*)

 type authors = string list;

 type iterID = int;

 type calcID = int;

 (* TODO CLEANUP Thm:

 type rule = 

 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;

                    (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI

 thmID            : type for data from user input + program

 thmDeriv         : type for thy_hierarchy ONLY

 obsolete types   : thm' (SEE "ad thm'"), thm''. 

 revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.

 activate         : thmID_of_derivation_name'

 *)

 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 * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:

 val thm'2xml : int -> Celem.thm' -> Celem.xml

 val assoc_thm': theory -> Celem.thm' -> thm

 | Calculate' of Rule.theory' * string * term * (term * Celem.thm')

 *)

 (* tricky combination of (string, term) for theorems in Isac:

   * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)

     by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.

   * case 2 "sym_..": Global_Theory.get_thm..RS sym

   * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:

     from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)

 *)

 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)

 (*.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;

 type xml = string; (* rm together with old code replaced by XML.tree *)

 (* 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                  *)

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

                  DESIGN ?TODO: list for several patterns ?      *)

 (*  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 due 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)'

     # ???

 *)

 fun thm2str thm =

   let

     val t = Thm.prop_of thm

     val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))

     val ctxt' = Config.put show_markup false ctxt

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

 fun id_of_thm (Rule.Thm (id, _)) = id  (* TODO re-arrange code for rule2str *)

   | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))

 fun thm_of_thm (Rule.Thm (_, thm)) = thm  (* TODO re-arrange code for rule2str *)

   | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))

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

 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm

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

 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''

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

 type theID = string list;

 val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)

 fun theID2thyID theID =

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

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

 (*the key into the hierarchy ob problems*)

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

 val e_pblID = ["e_pblID"];

 (*the key into the hierarchy ob methods*)

 type metID = string list;

 type spec = Rule.domID * pblID * metID;

 fun spec2str (dom, pbl, met) = 

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

 val e_metID = ["e_metID"];

 val metID2str = strs2str;

 val empty_spec = (Rule.e_domID, e_pblID, e_metID);

 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;

 (* 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";

 (* for conversion from XML *)

 fun str2ketype' "exp" = Exp_

   | str2ketype' "thy" = Thy_

   | str2ketype' "pbl" = Pbl_

   | str2ketype' "met" = Met_

   | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)

 (* 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 "pbt" 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'*)

 datatype thydata =

   Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}

 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,

    thm: thm} (* here no sym_thm, thus no thmID required *)

 | Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule.rls)}

 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule.calc}

 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors,

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

 fun the2str (Html {guh, ...}) = guh

   | the2str (Hthm {guh, ...}) = guh

   | the2str (Hrls {guh, ...}) = guh

   | the2str (Hcal {guh, ...}) = guh

   | the2str (Hord {guh, ...}) = guh

 fun thes2str thes = map the2str thes |> list2str;

 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)

      (a): thehier does not contain sym_thmID theorems

      (b): lookup for sym_thmID directly from Isabelle using sym_thm

           (within math-engine NO lookup in thehier -- within java in *.xml only!)

 TODO (c): export from thehier to xml

 TODO (c1)   creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy

 TODO (c2)   creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"

 TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)

           stands for both, "thmID" and "sym_thmID" 

 TODO (d1)   lookup from calctxt          

 TODO (d1)   lookup from from rule set in MiniBrowser *)

 type thehier = (thydata ptyp) list;

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

 fun part2guh [str] = (case str of

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

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

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

       | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))

   | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");

 fun thy2guh [part, thyID] = (case part of

       "Isabelle" => "thy_isab_" ^ thyID

     | "IsacScripts" => "thy_scri_" ^ thyID

     | "IsacKnowledge" => "thy_isac_" ^ thyID

     | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))

   | thy2guh theID = raise 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 => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))

   | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");

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

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

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

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

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

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

   | _ => raise ERROR

     ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");

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

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

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

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

   | _ => raise ERROR

     ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");

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

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

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

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

   | _ => raise ERROR

     ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");

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

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

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

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

   | _ => raise ERROR

     ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");

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

 (* TODO

 fun theID2guh 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 => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)

     end

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

 *)

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

 fun theID2guh [] = raise ERROR ("theID2guh: called with []")

   | theID2guh [str] = part2guh [str]

   | theID2guh [s1, s2] = thy2guh [s1, s2]

   | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]

   | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of

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

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

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

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

     | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))

   | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);

 type path = string;

 type filename = string;

 (* datastructure for KEStore_Elems, intermediate for thehier *)

 type rlss_elem = 

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

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

     Rule.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 = Rule.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 assoc_thy thy =

     if thy = "e_domID"

     then (Rule.Thy_Info_get_theory "Script") (*lower bound of Knowledge*)

     else (Rule.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: (Rule.rls' * Rule.rls) list) =

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

     in overwritel (al, bl') end;

 fun subst2str s =

     (strs2str o

       (map (

         linefeed o pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;

 fun subst2str' s =

     (strs2str' o

      (map (

        pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;

 val env2str = subst2str;

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

 (* trace internal steps of isac's numeral calculations *)

 val trace_calc = Unsynchronized.ref false;

 (* 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 *)

 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 "type 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 = (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 (Rule.term2str dsc, Rule.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  *)

 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 : Rule.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 = Rule.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 = " ^ (Rule.termopt2str cas') ^  ", guh = \"" ^ guh'  ^ "\", init = "

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

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

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

       ^ (Rule.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)

       | node _ _ = raise ERROR "coll_pblguhs - node"

 	  and nodes coll [] = coll

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

   in nodes [] pbls end;

 fun check_pblguh_unique guh pbls =

   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) =

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

     if k = k'

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

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

     )			 

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

     ((*writeln ("### 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))

     )

   | insrt _ _ _ _ = raise ERROR "";

 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))

   | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";

 (* 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, _, 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');

 (* 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'   : Rule.rew_ord',   (*for rules in Detail

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

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

 				                              instead erls in "fun prep_met"              *)

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

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

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

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

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

       calc       : Rule.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        : Rule.scr    (*prep_met gets progam or string "empty_script"    *)

 	   };

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

 	erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls,

 	errpats = [], nrls = Rule.e_rls, ppc = [], pre = [], scr = Rule.EmptyScr};

 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)

       | node _ _ = raise ERROR "coll_pblguhs - node"

   	and nodes coll [] = coll

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

     in nodes [] mets end;

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

     if member op = (coll_metguhs mets) guh

     then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^

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

 		  "consider setting \"check_guhs_unique := false\"")

     else ();

 fun Html_default exist = (Html {guh = theID2guh exist, 

   coursedesign = ["isac team 2006"], mathauthors = [], html = ""})

 fun fill_parents (_, [i]) thydata = Ptyp (i, [thydata], [])

   | fill_parents (exist, i :: is) thydata =

     Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])

   | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"

 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]

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

     if i = key

     then pys (* preserve existing thydata *) 

     else py :: add_thydata (exist, [i]) data pyss

   | add_thydata (exist, iss as (i :: is)) data ((py as Ptyp (key, d, pys)) :: pyss) = 

     if i = key

     then       

       if length pys = 0

       then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss

       else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss

     else py :: add_thydata (exist, iss) data pyss

   | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"

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

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

     fillpats = fillpats', thm = thm}

   | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";

 (* for dialog-authoring *)

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

     let

       val rls' = 

         case rls of

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

           => Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

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

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

           => Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

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

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

           => Rule.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 "update_hrls: wrong arguments";

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

   let

     fun py_err _ = raise 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 _ = raise 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

 (* group the theories defined in Isac, compare Build_Thydata:

   section "Get and group the theories defined in Isac" *) 

 fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)

   let

     val allthys = Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata")

   in

     drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)

   end

 fun knowthys () = (*["Isac", .., "Descript", "Delete"]*)

   let

     fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)

       let

         val allthys = filter_out (member Context.eq_thy

           [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret", 

             Rule.Thy_Info_get_theory "xmlsrc", Rule.Thy_Info_get_theory "Frontend"]) 

           (Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata"))

       in

         take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 

         allthys)

       end

     val isacthys' = isacthys ()

     val proglang_parent = Rule.Thy_Info_get_theory "ProgLang"

   in

     take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')

   end

 fun progthys () = (*["Isac", .., "Descript", "Delete"]*)

   let

     fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)

       let                                                        

         val allthys = filter_out (member Context.eq_thy

           [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret", 

             Rule.Thy_Info_get_theory "xmlsrc", Rule.Thy_Info_get_theory "Frontend"]) 

           (Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata"))

       in

         take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), 

         allthys)

       end

     val isacthys' = isacthys ()

     val proglang_parent = Rule.Thy_Info_get_theory "ProgLang"

   in

     drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')

   end

 fun partID thy = 

   if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"

   else if member Context.eq_thy (progthys ()) thy then "IsacScripts"

   else if member Context.eq_thy (isabthys ()) thy then "Isabelle"

   else error ("closure of thys in Isac is broken by " ^ Rule.string_of_thy thy)

 fun partID' thy' = partID (Rule.Thy_Info_get_theory thy')

 end (*struct*)