neuper@37906: (* elements of calculations. neuper@37906: they are partially held in association lists as ref's for wneuper@59405: switching language levels (meta-string, object-values). wneuper@59405: in order to keep these ref's during re-evaluation of code, neuper@42399: they are defined here at the beginning of the code. neuper@42399: Author: Walther Neuper 2003 neuper@42399: (c) copyright due to lincense terms neuper@37906: *) neuper@37906: wneuper@59405: signature CALC_ELEMENT = wneuper@59405: sig wneuper@59413: type cas_elem wneuper@59413: type pbt wneuper@59413: type ptyps wneuper@59413: type metID wneuper@59413: type pblID wneuper@59413: type mets wneuper@59413: type met wneuper@59405: datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list wneuper@59405: wneuper@59413: type authors wneuper@59405: type guh wneuper@59416: val env2str: Rule.subst -> string wneuper@59416: val subst2str: Rule.subst -> string wneuper@59416: val subst2str': Rule.subst -> string wneuper@59414: wneuper@59413: type fillpat wneuper@59405: datatype thydata wneuper@59416: = Hcal of {calc: Rule.calc, coursedesign: authors, guh: guh, mathauthors: authors} wneuper@59416: | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool} wneuper@59416: | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule.rls} wneuper@59405: | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm} wneuper@59405: | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors} wneuper@59413: type theID wneuper@59413: type rlss_elem wneuper@59405: val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list wneuper@59405: val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool wneuper@59413: type spec wneuper@59405: val cas_eq: cas_elem * cas_elem -> bool wneuper@59405: val e_Ptyp: pbt ptyp wneuper@59405: val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list wneuper@59405: val check_guhs_unique: bool Unsynchronized.ref wneuper@59405: val check_pblguh_unique: guh -> pbt ptyp list -> unit wneuper@59405: val insrt: pblID -> 'a -> string list -> 'a ptyp list -> 'a ptyp list wneuper@59405: val e_Mets: met ptyp wneuper@59405: val check_metguh_unique: guh -> met ptyp list -> unit wneuper@59405: val add_thydata: string list * string list -> thydata -> thydata ptyp list -> thydata ptyp list wneuper@59405: val get_py: 'a ptyp list -> pblID -> string list -> 'a wneuper@59405: val update_hthm: thydata -> fillpat list -> thydata wneuper@59405: val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list wneuper@59405: val part2guh: theID -> guh wneuper@59405: val spec2str: string * string list * string list -> string wneuper@59405: val linefeed: string -> string wneuper@59405: val pbts2str: pbt list -> string wneuper@59405: val thes2str: thydata list -> string wneuper@59405: val theID2str: string list -> string wneuper@59405: val the2str: thydata -> string wneuper@59405: val trace_calc: bool Unsynchronized.ref wneuper@59405: eqtype thmID wneuper@59413: type thm' wneuper@59405: datatype lrd = D | L | R wneuper@59405: val trace_rewrite: bool Unsynchronized.ref wneuper@59405: val depth: int Unsynchronized.ref wneuper@59416: val id_rls: Rule.rls -> string wneuper@59416: val rls2str: Rule.rls -> string wneuper@59414: type errpat wneuper@59415: val assoc_thy: Rule.theory' -> theory wneuper@59405: eqtype cterm' wneuper@59413: type loc_ wneuper@59405: val loc_2str: loc_ -> string wneuper@59405: eqtype rew_ord' wneuper@59413: type thm'' wneuper@59405: val metID2str: string list -> string wneuper@59405: val e_pblID: pblID wneuper@59405: val e_metID: metID wneuper@59405: val empty_spec: spec wneuper@59414: val e_spec: spec wneuper@59405: datatype ketype = Exp_ | Met_ | Pbl_ | Thy_ wneuper@59413: type kestoreID wneuper@59405: val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b wneuper@59405: val ketype2str: ketype -> string wneuper@59405: val coll_pblguhs: pbt ptyp list -> guh list wneuper@59405: val coll_metguhs: met ptyp list -> guh list wneuper@59413: type pat wneuper@59405: val pats2str: pat list -> string wneuper@59405: val maxthy: theory -> theory -> theory wneuper@59405: eqtype filename wneuper@59405: val lim_deriv: int Unsynchronized.ref wneuper@59416: val id_of_thm: Rule.rule -> string wneuper@59405: val isabthys: unit -> theory list wneuper@59405: val thyID_of_derivation_name: string -> string wneuper@59415: val partID': Rule.theory' -> string wneuper@59415: val thm2guh: string * Rule.thyID -> thmID -> guh wneuper@59405: val thmID_of_derivation_name: string -> string wneuper@59416: val rls2guh: string * Rule.thyID -> Rule.rls' -> guh wneuper@59405: val theID2guh: theID -> guh wneuper@59405: eqtype fillpatID wneuper@59405: type pbt_ = string * (term * term) wneuper@59416: val e_rew_ord: Rule.subst -> term * term -> bool wneuper@59405: eqtype xml wneuper@59415: val cal2guh: string * Rule.thyID -> string -> guh wneuper@59405: val ketype2str': ketype -> string wneuper@59405: val str2ketype': string -> ketype wneuper@59405: val thmID_of_derivation_name': thm -> string wneuper@59405: eqtype path wneuper@59415: val theID2thyID: theID -> Rule.thyID wneuper@59405: val thy2guh: theID -> guh wneuper@59405: val thypart2guh: theID -> guh wneuper@59415: val ord2guh: string * Rule.thyID -> rew_ord' -> guh wneuper@59416: val update_hrls: thydata -> Rule.errpatID list -> thydata wneuper@59405: eqtype iterID wneuper@59405: eqtype calcID wneuper@59405: val thm''_of_thm: thm -> thm'' wneuper@59416: val rew_ord': (rew_ord' * (Rule.subst -> term * term -> bool)) list Unsynchronized.ref wneuper@59416: val thm_of_thm: Rule.rule -> thm wneuper@59408: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) wneuper@59414: val thm2str: thm -> string wneuper@59414: val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list -> wneuper@59414: thydata ptyp list wneuper@59408: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59411: val knowthys: unit -> theory list wneuper@59411: val e_pbt: pbt wneuper@59408: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59414: wneuper@59414: (*----- unused code, kept as hints to design ideas ---------------------------------------------*) wneuper@59416: val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list -> wneuper@59416: (Rule.rls' * (string * Rule.rls)) list end wneuper@59414: wneuper@59416: wneuper@59405: (**) wneuper@59415: structure Celem(*: CALC_ELEMENT*) = neuper@38061: struct wneuper@59405: (**) wneuper@59405: wneuper@59414: val linefeed = (curry op^) "\n"; (* ?\ libraryC ?*) neuper@37906: type authors = string list; neuper@37906: wneuper@59414: type iterID = int; wneuper@59414: type calcID = int; neuper@42399: neuper@55481: (* TODO CLEANUP Thm: neuper@55487: type rule = neuper@55487: Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end; neuper@55487: (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI neuper@55487: thmID : type for data from user input + program neuper@55487: thmDeriv : type for thy_hierarchy ONLY neuper@55487: obsolete types : thm' (SEE "ad thm'"), thm''. wneuper@59250: revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm. neuper@55487: activate : thmID_of_derivation_name' neuper@55481: *) neuper@42399: type thmID = string; (* identifier for a thm (the shortest possible identifier) *) neuper@42434: type thmDeriv = string; (* WN120524 deprecated neuper@42434: thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name neuper@42434: WN120524: dont use Thm.derivation_name, this is destroyed by num_str; neuper@42434: Thm.get_name_hint survives num_str and seems perfectly reliable *) neuper@42399: wneuper@59415: type thm' = thmID * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review: wneuper@59414: val thm'2xml : int -> Celem.thm' -> Celem.xml wneuper@59414: val assoc_thm': theory -> Celem.thm' -> thm wneuper@59416: | Calculate' of Rule.theory' * string * term * (term * Celem.thm') wneuper@59414: *) wneuper@59251: (* tricky combination of (string, term) for theorems in Isac: wneuper@59251: * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm) wneuper@59251: by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid. wneuper@59251: * case 2 "sym_..": Global_Theory.get_thm..RS sym wneuper@59251: * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_: wneuper@59255: from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm) wneuper@59251: *) wneuper@59253: type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *) neuper@42399: neuper@40836: (*.a 'guh'='globally unique handle' is a string unique for each element neuper@37906: of isac's KEStore and persistent over time neuper@37906: (in particular under shifts within the respective hierarchy); neuper@40836: specialty for thys: neuper@37906: # guh NOT resistant agains shifts from one thy to another neuper@37906: (which is the price for Isabelle's design: thy's overwrite ids of subthy's) neuper@37906: # requirement for matchTheory: induce guh from tac + current thy neuper@37906: (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.) neuper@40836: TODO: introduce to pbl, met.*) neuper@37906: type guh = string; neuper@37906: wneuper@59141: type xml = string; (* rm together with old code replaced by XML.tree *) neuper@37906: neuper@42451: neuper@42451: (* for (at least) 2 kinds of access: neuper@42451: (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats) neuper@42451: (2) given a thm, find respective fillpats *) neuper@42451: type fillpatID = string neuper@42451: type fillpat = neuper@42451: fillpatID (* DESIGN ?TODO: give an order w.r.t difficulty ? *) neuper@42451: * term (* the pattern with fill-in gaps *) wneuper@59415: * Rule.errpatID; (* which the fillpat would be a help for neuper@42451: DESIGN ?TODO: list for several patterns ? *) neuper@37906: neuper@40836: wneuper@59414: (* WN0509 discussion: neuper@37906: ############################################################################# neuper@37906: # How to manage theorys in subproblems wrt. the requirement, # neuper@37906: # that scripts should be re-usable ? # neuper@37906: ############################################################################# neuper@37906: neuper@37988: eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..' neuper@37906: which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script neuper@40836: because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b neuper@37906: is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard neuper@37906: (see match_ags). neuper@37906: neuper@37906: Preliminary solution: neuper@38011: # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically, neuper@38011: # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl neuper@40836: # however, a thy specified by the user in the rootpbl may lead to neuper@40836: errors in far-off subpbls (which are not yet reported properly !!!) neuper@37906: and interactively specifiying thys in subpbl is not very relevant. neuper@37906: neuper@37906: Other solutions possible: wneuper@59352: # always parse and type-check with Thy_Info_get_theory "Isac" wneuper@59414: (rejected due to the vague idea eg. to re-use equations for R in C etc.) neuper@37906: # regard the subthy-relation in specifying thys of subpbls neuper@38011: # specifically handle 'SubProblem (undefined, pbl, arglist)' neuper@37906: # ??? wneuper@59414: *) wneuper@59414: wneuper@59414: fun thm2str thm = wneuper@59414: let wneuper@59414: val t = Thm.prop_of thm wneuper@59414: val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac")) wneuper@59414: val ctxt' = Config.put show_markup false ctxt wneuper@59414: in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; wneuper@59414: wneuper@59415: fun id_of_thm (Rule.Thm (id, _)) = id (* TODO re-arrange code for rule2str *) wneuper@59414: | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *)) wneuper@59415: fun thm_of_thm (Rule.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *) wneuper@59414: | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *)) wneuper@59414: wneuper@59414: fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); wneuper@59414: fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm wneuper@59414: fun thyID_of_derivation_name dn = hd (space_explode "." dn); wneuper@59414: fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm'' wneuper@59414: wneuper@59414: neuper@37906: neuper@37906: (*the key into the hierarchy ob theory elements*) neuper@37906: type theID = string list; wneuper@59414: val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*) wneuper@59414: fun theID2thyID theID = wneuper@59414: if length theID >= 3 then (last_elem o (drop_last_n 2)) theID wneuper@59414: else error ("theID2thyID called with " ^ theID2str theID); neuper@37906: neuper@37906: (*the key into the hierarchy ob problems*) wneuper@59414: type pblID = string list; (* domID :: ...*) wneuper@59414: val e_pblID = ["e_pblID"]; neuper@37906: neuper@37906: (*the key into the hierarchy ob methods*) neuper@37906: type metID = string list; wneuper@59415: type spec = Rule.domID * pblID * metID; wneuper@59414: fun spec2str (dom, pbl, met) = wneuper@59414: "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")"; wneuper@59414: val e_metID = ["e_metID"]; neuper@37906: val metID2str = strs2str; wneuper@59415: val empty_spec = (Rule.e_domID, e_pblID, e_metID); s1210629013@52171: val e_spec = empty_spec; s1210629013@52171: wneuper@59414: (* association list with cas-commands, for generating a complete calc-head *) neuper@52169: type generate_fn = neuper@52169: (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *) neuper@52169: (term * (* description of an element *) neuper@52169: term list) (* value of the element (always put into a list) *) neuper@52169: list) (* of elements in the formalization *) neuper@52169: type cas_elem = neuper@52169: (term * (* cas-command, eg. 'solve' *) neuper@52169: (spec * (* theory, problem, method *) s1210629013@52174: generate_fn)) neuper@52169: fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2 s1210629013@52167: neuper@37906: (*either theID or pblID or metID*) neuper@37906: type kestoreID = string list; neuper@37906: wneuper@59414: (* for distinction of contexts WN130621: disambiguate with Isabelle's Context *) neuper@37906: datatype ketype = Exp_ | Thy_ | Pbl_ | Met_; neuper@37906: fun ketype2str Exp_ = "Exp_" neuper@40836: | ketype2str Thy_ = "Thy_" neuper@40836: | ketype2str Pbl_ = "Pbl_" neuper@37906: | ketype2str Met_ = "Met_"; neuper@37906: fun ketype2str' Exp_ = "Example" neuper@40836: | ketype2str' Thy_ = "Theory" neuper@40836: | ketype2str' Pbl_ = "Problem" neuper@37906: | ketype2str' Met_ = "Method"; wneuper@59172: (* for conversion from XML *) wneuper@59172: fun str2ketype' "exp" = Exp_ wneuper@59172: | str2ketype' "thy" = Thy_ wneuper@59172: | str2ketype' "pbl" = Pbl_ wneuper@59172: | str2ketype' "met" = Met_ wneuper@59172: | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str) neuper@37906: neuper@48887: (* A tree for storing data defined in different theories neuper@48887: for access from the Interpreter and from dialogue authoring neuper@48887: using a string list as key. wneuper@59414: 'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *) neuper@40836: datatype 'a ptyp = wneuper@59414: Ptyp of string * (* element of the key *) wneuper@59414: 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69) wneuper@59414: presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *) wneuper@59414: ('a ptyp) list; (* the children nodes *) neuper@37906: wneuper@59414: (* datatype for collecting thydata for hierarchy *) neuper@37906: (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*) wneuper@59414: datatype thydata = wneuper@59414: Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string} wneuper@59414: | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list, wneuper@59414: thm: thm} (* here no sym_thm, thus no thmID required *) wneuper@59415: | Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule.rls)} wneuper@59415: | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule.calc} wneuper@59414: | Hord of {guh: guh, coursedesign: authors, mathauthors: authors, wneuper@59415: ord: (Rule.subst -> (term * term) -> bool)}; wneuper@59414: fun the2str (Html {guh, ...}) = guh wneuper@59414: | the2str (Hthm {guh, ...}) = guh wneuper@59414: | the2str (Hrls {guh, ...}) = guh wneuper@59414: | the2str (Hcal {guh, ...}) = guh wneuper@59414: | the2str (Hord {guh, ...}) = guh neuper@55435: fun thes2str thes = map the2str thes |> list2str; neuper@37906: neuper@55483: (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting) neuper@55487: (a): thehier does not contain sym_thmID theorems neuper@55485: (b): lookup for sym_thmID directly from Isabelle using sym_thm neuper@55485: (within math-engine NO lookup in thehier -- within java in *.xml only!) neuper@55483: TODO (c): export from thehier to xml neuper@55483: TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy neuper@55483: TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml" neuper@55483: TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml) neuper@55483: stands for both, "thmID" and "sym_thmID" neuper@55483: TODO (d1) lookup from calctxt neuper@55483: TODO (d1) lookup from from rule set in MiniBrowser *) neuper@37906: type thehier = (thydata ptyp) list; neuper@55405: (* required to determine sequence of main nodes of thehier in KEStore.thy *) wneuper@59414: fun part2guh [str] = (case str of wneuper@59414: "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh neuper@55405: | "IsacScripts" => "thy_scri_" ^ str ^ "-part" neuper@55405: | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part" wneuper@59414: | str => raise ERROR ("thy2guh: called with \""^ str ^"\"")) wneuper@59414: | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'"); neuper@37906: wneuper@59414: fun thy2guh [part, thyID] = (case part of wneuper@59414: "Isabelle" => "thy_isab_" ^ thyID neuper@55437: | "IsacScripts" => "thy_scri_" ^ thyID neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ thyID wneuper@59414: | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\"")) wneuper@59414: | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\""); neuper@55437: wneuper@59414: fun thypart2guh ([part, thyID, thypart] : theID) = (case part of wneuper@59414: "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh wneuper@59414: | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart wneuper@59414: | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart wneuper@59414: | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'")) wneuper@59414: | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\""); wneuper@59414: neuper@55437: wneuper@59414: (* convert the data got via contextToThy to a globally unique handle. wneuper@59414: there is another way to get the guh: get out of the 'theID' in the hierarchy *) wneuper@59414: fun thm2guh (isa, thyID) thmID = case isa of wneuper@59415: "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh wneuper@59415: | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID wneuper@59415: | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID wneuper@59414: | _ => raise ERROR wneuper@59414: ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\""); neuper@55437: wneuper@59414: fun rls2guh (isa, thyID) rls' = case isa of wneuper@59415: "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls' : guh wneuper@59415: | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls' wneuper@59415: | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls' wneuper@59414: | _ => raise ERROR wneuper@59414: ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\""); neuper@55437: wneuper@59414: fun cal2guh (isa, thyID) calID = case isa of wneuper@59415: "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID : guh wneuper@59415: | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID wneuper@59415: | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID wneuper@59414: | _ => raise ERROR wneuper@59414: ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\""); neuper@55437: wneuper@59414: fun ord2guh (isa, thyID) rew_ord' = case isa of wneuper@59415: "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh wneuper@59415: | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord' wneuper@59415: | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord' wneuper@59414: | _ => raise ERROR wneuper@59414: ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\""); neuper@55437: neuper@55437: (* not only for thydata, but also for thy's etc *) wneuper@59414: (* TODO wneuper@59414: fun theID2guh theID = case length theID of neuper@55437: 0 => error ("theID2guh: called with theID = " ^ strs2str' theID) neuper@55437: | 1 => part2guh theID neuper@55437: | 2 => thy2guh theID neuper@55437: | 3 => thypart2guh theID neuper@55437: | 4 => neuper@55437: let val [isa, thyID, typ, elemID] = theID neuper@55437: in case typ of neuper@55437: "Theorems" => thm2guh (isa, thyID) elemID neuper@55437: | "Rulesets" => rls2guh (isa, thyID) elemID neuper@55437: | "Calculations" => cal2guh (isa, thyID) elemID neuper@55437: | "Orders" => ord2guh (isa, thyID) elemID neuper@55437: | "Theorems" => thy2guh [isa, thyID] wneuper@59414: | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID) neuper@55437: end wneuper@59414: | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID); wneuper@59414: *) wneuper@59414: (* not only for thydata, but also for thy's etc *) wneuper@59414: fun theID2guh [] = raise ERROR ("theID2guh: called with []") wneuper@59414: | theID2guh [str] = part2guh [str] wneuper@59414: | theID2guh [s1, s2] = thy2guh [s1, s2] wneuper@59414: | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3] wneuper@59414: | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of wneuper@59414: "Theorems" => thm2guh (isa, thyID) elemID wneuper@59414: | "Rulesets" => rls2guh (isa, thyID) elemID wneuper@59414: | "Calculations" => cal2guh (isa, thyID) elemID wneuper@59414: | "Orders" => ord2guh (isa, thyID) elemID wneuper@59414: | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs)) wneuper@59414: | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs); neuper@55437: neuper@37906: type path = string; neuper@37906: type filename = string; neuper@37906: neuper@42451: neuper@37906: neuper@52141: (* datastructure for KEStore_Elems, intermediate for thehier *) neuper@52141: type rlss_elem = wneuper@59416: (Rule.rls' * (* identifier unique within Isac *) wneuper@59415: (Rule.theory' * (* just for assignment in thehier, not appropriate for parsing etc *) wneuper@59415: Rule.rls)) (* ((#id o rep_rls) rls) = rls' by coding discipline *) neuper@52141: fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2 neuper@37906: neuper@52141: fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys = wneuper@59414: case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of wneuper@59414: NONE => re :: ys wneuper@59414: | SOME (i, (_, (_, r2))) => neuper@52141: let wneuper@59415: val r12 = Rule.merge_rls id r1 r2 neuper@52141: in list_update ys i (id, (thyID, r12)) end neuper@52141: fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2; neuper@52141: neuper@52141: wneuper@59414: fun assoc_thy thy = wneuper@59414: if thy = "e_domID" wneuper@59415: then (Rule.Thy_Info_get_theory "Script") (*lower bound of Knowledge*) wneuper@59415: else (Rule.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system"); neuper@37906: wneuper@59414: (* overwrite an element in an association list and pair it with a thyID neuper@37906: in order to create the thy_hierarchy; neuper@37906: overwrites existing rls' even if they are defined in a different thy; wneuper@59414: this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc *) wneuper@59414: (* WN060120 ...these are NOT compatible to "fun assoc_thm'" in that neuper@37906: they do NOT handle overlays by re-using an identifier in different thys; neuper@37906: "thyID.rlsID" would be a good solution, if the "." would be possible neuper@37906: in scripts... wneuper@59414: actually a hack to get alltogether run again with minimal effort *) neuper@37906: fun insthy thy' (rls', rls) = (rls', (thy', rls)); wneuper@59416: fun overwritelthy thy (al, bl: (Rule.rls' * Rule.rls) list) = wneuper@59415: let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl neuper@37906: in overwritel (al, bl') end; neuper@37906: wneuper@59414: fun subst2str s = neuper@40836: (strs2str o wneuper@59414: (map ( wneuper@59415: linefeed o pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s; wneuper@59415: fun subst2str' s = neuper@40836: (strs2str' o wneuper@59414: (map ( wneuper@59415: pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s; neuper@37906: val env2str = subst2str; neuper@37906: wneuper@59332: fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; neuper@37906: neuper@37906: wneuper@59387: (* trace internal steps of isac's numeral calculations *) wneuper@59387: val trace_calc = Unsynchronized.ref false; wneuper@59414: (* trace internal steps of isac's rewriter *) neuper@38006: val trace_rewrite = Unsynchronized.ref false; wneuper@59414: (* depth of recursion in traces of the rewriter, if trace_rewrite:=true *) neuper@38006: val depth = Unsynchronized.ref 99999; wneuper@59414: (* no of rewrites exceeding this int -> NO rewrite *) neuper@38006: val lim_deriv = Unsynchronized.ref 100; wneuper@59414: (* switch for checking guhs unique before storing a pbl or met; neuper@37906: set true at startup (done at begin of ROOT.ML) wneuper@59414: set false for editing IsacKnowledge (done at end of ROOT.ML) *) neuper@41905: val check_guhs_unique = Unsynchronized.ref true; neuper@37906: neuper@37906: wneuper@59414: datatype lrd = (*elements of "type loc_" into an Isabelle term*) wneuper@59414: L (*go left at $*) wneuper@59414: | R (*go right at $*) wneuper@59414: | D; (*go down at Abs*) neuper@37906: type loc_ = lrd list; neuper@37906: fun ldr2str L = "L" neuper@37906: | ldr2str R = "R" neuper@37906: | ldr2str D = "D"; wneuper@59414: fun loc_2str k = (strs2str' o (map ldr2str)) k; neuper@37906: neuper@55335: neuper@55335: (* the pattern for an item of a problems model or a methods guard *) neuper@55335: type pat = neuper@55335: (string * (* field *) neuper@55335: (term * (* description *) neuper@55335: term)) (* id | arbitrary term *); neuper@55335: fun pat2str ((field, (dsc, id)) : pat) = wneuper@59415: pair2str (field, pair2str (Rule.term2str dsc, Rule.term2str id)) neuper@55335: fun pats2str pats = (strs2str o (map pat2str)) pats neuper@55335: neuper@55357: (* types for problems models (TODO rename to specification models) *) neuper@55335: type pbt_ = neuper@55335: (string * (* field "#Given",..*)(*deprecated due to 'type pat'*) neuper@55335: (term * (* description *) neuper@55335: term)); (* id | struct-var *) neuper@55335: type pbt = wneuper@59414: {guh : guh, (* unique within this isac-knowledge *) wneuper@59414: mathauthors : string list, (* copyright *) wneuper@59414: init : pblID, (* to start refinement with *) neuper@55335: thy : theory, (* which allows to compile that pbt wneuper@59414: TODO: search generalized for subthy (ref.p.69*) wneuper@59414: (*^^^ WN050912 NOT used during application of the problem, wneuper@59414: because applied terms may be from 'subthy' as well as from super; wneuper@59414: thus we take 'maxthy'; see match_ags ! *) wneuper@59414: cas : term option, (* 'CAS-command' *) wneuper@59415: prls : Rule.rls, (* for preds in where_ *) wneuper@59414: where_ : term list, (* where - predicates *) neuper@55335: ppc : pat list, (* this is the model-pattern; wneuper@59414: it contains "#Given","#Where","#Find","#Relate"-patterns wneuper@59414: for constraints on identifiers see "fun cpy_nam" *) wneuper@59414: met : metID list} (* methods solving the pbt *) neuper@55335: wneuper@59397: val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure", wneuper@59416: cas = NONE, prls = Rule.Erls, where_ = [], ppc = [], met = []} : pbt wneuper@59414: fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc', wneuper@59414: prls = prls', thy = thy', where_ = w'} : pbt) wneuper@59415: = "{cas = " ^ (Rule.termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = " wneuper@59414: ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = " wneuper@59414: ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = " wneuper@59415: ^ (Rule.rls2str prls' |> quote) ^ ", thy = {" ^ (Rule.theory2str thy') ^ "}, where_ = " wneuper@59415: ^ (Rule.terms2str w') ^ "}" |> linefeed; s1210629013@55345: fun pbts2str pbts = map pbt2str pbts |> list2str; neuper@55335: wneuper@59416: val e_Ptyp = Ptyp ("e_pblID", [e_pbt], []) neuper@55335: type ptyps = (pbt ptyp) list neuper@55335: neuper@55357: fun coll_pblguhs pbls = wneuper@59414: let wneuper@59414: fun node coll (Ptyp (_, [n], ns)) = [(#guh : pbt -> guh) n] @ (nodes coll ns) wneuper@59414: | node _ _ = raise ERROR "coll_pblguhs - node" wneuper@59414: and nodes coll [] = coll wneuper@59414: | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns); wneuper@59414: in nodes [] pbls end; wneuper@59414: fun check_pblguh_unique guh pbls = wneuper@59414: if member op = (coll_pblguhs pbls) guh wneuper@59414: then error ("check_guh_unique failed with \""^ guh ^"\";\n"^ wneuper@59414: "use \"sort_pblguhs()\" for a list of guhs;\n"^ wneuper@59414: "consider setting \"check_guhs_unique := false\"") wneuper@59414: else (); s1210629013@55339: neuper@55453: fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])] neuper@55453: | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) = wneuper@59414: ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*) wneuper@59414: if k = k' wneuper@59414: then ((Ptyp (k', [pbt], ps)) :: pys) wneuper@59414: else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys)) wneuper@59414: ) wneuper@59414: | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) = wneuper@59414: ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*) wneuper@59414: if k = k' wneuper@59414: then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys) wneuper@59414: else wneuper@59414: if length pys = 0 wneuper@59414: then error ("insert: not found " ^ (strs2str (d : pblID))) wneuper@59414: else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys)) wneuper@59414: ) wneuper@59414: | insrt _ _ _ _ = raise ERROR ""; s1210629013@55339: neuper@55448: fun update_ptyps ID _ _ [] = neuper@55448: error ("update_ptyps: " ^ strs2str' ID ^ " does not exist") neuper@55448: | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) = neuper@55448: if i = key neuper@55448: then neuper@55448: if length pys = 0 neuper@55448: then ((Ptyp (key, [data], [])) :: pyss) neuper@55448: else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants") neuper@55448: else py :: update_ptyps ID [i] data pyss neuper@55448: | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) = neuper@55448: if i = key neuper@55448: then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss) neuper@55448: else (py :: (update_ptyps ID (i :: is) data pyss)) wneuper@59414: | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern."; neuper@55448: s1210629013@55339: (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge s1210629013@55339: function for trees / ptyps *) s1210629013@55339: fun merge_ptyps ([], pt) = pt s1210629013@55339: | merge_ptyps (pt, []) = pt wneuper@59414: | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) = s1210629013@55346: if k = k' s1210629013@55346: then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys) s1210629013@55346: else x' :: merge_ptyps (xs, xs'); s1210629013@55372: s1210629013@55372: (* data for methods stored in 'methods'-database*) s1210629013@55372: type met = wneuper@59415: {guh : guh, (*unique within this isac-knowledge *) wneuper@59415: mathauthors: string list, (*copyright *) wneuper@59415: init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*) wneuper@59415: rew_ord' : Rule.rew_ord', (*for rules in Detail wneuper@59415: TODO.WN0509 store fun itself, see 'type pbt'*) wneuper@59415: erls : Rule.rls, (*the eval_rls for cond. in rules FIXME "rls' wneuper@59415: instead erls in "fun prep_met" *) wneuper@59415: srls : Rule.rls, (*for evaluating list expressions in scr *) wneuper@59415: prls : Rule.rls, (*for evaluating predicates in modelpattern *) wneuper@59415: crls : Rule.rls, (*for check_elementwise, ie. formulae in calc.*) wneuper@59415: nrls : Rule.rls, (*canonical simplifier specific for this met *) wneuper@59415: errpats : Rule.errpat list,(*error patterns expected in this method *) wneuper@59415: calc : Rule.calc list, (*Theory_Data in fun prep_met *) s1210629013@55372: (*branch : TransitiveB set in append_problem at generation ob pblobj wneuper@59415: FIXXXME.0308: set branch from met in Apply_Method ? *) s1210629013@55372: ppc : pat list, (*.items in given, find, relate; s1210629013@55372: items (in "#Find") which need not occur in the arg-list of a SubProblem s1210629013@55372: are 'copy-named' with an identifier "*'.'". s1210629013@55372: copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? wneuper@59415: see ME/calchead.sml 'fun is_copy_named'. *) wneuper@59415: pre : term list, (*preconditions in where *) wneuper@59415: scr : Rule.scr (*prep_met gets progam or string "empty_script" *) s1210629013@55372: }; wneuper@59414: val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'", wneuper@59415: erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls, wneuper@59415: errpats = [], nrls = Rule.e_rls, ppc = [], pre = [], scr = Rule.EmptyScr}; wneuper@59414: val e_Mets = Ptyp ("e_metID", [e_met],[]); s1210629013@55372: s1210629013@55372: type mets = (met ptyp) list; s1210629013@55373: fun coll_metguhs mets = wneuper@59414: let wneuper@59414: fun node coll (Ptyp (_, [n], ns)) = [(#guh : met -> guh) n] @ (nodes coll ns) wneuper@59414: | node _ _ = raise ERROR "coll_pblguhs - node" wneuper@59414: and nodes coll [] = coll wneuper@59414: | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns); s1210629013@55373: in nodes [] mets end; s1210629013@55373: fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = s1210629013@55373: if member op = (coll_metguhs mets) guh wneuper@59414: then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^ wneuper@59414: "use \"sort_metguhs()\" for a list of guhs;\n" ^ wneuper@59414: "consider setting \"check_guhs_unique := false\"") s1210629013@55373: else (); s1210629013@55373: neuper@55450: fun Html_default exist = (Html {guh = theID2guh exist, neuper@55450: coursedesign = ["isac team 2006"], mathauthors = [], html = ""}) neuper@55450: wneuper@59414: fun fill_parents (_, [i]) thydata = Ptyp (i, [thydata], []) neuper@55450: | fill_parents (exist, i :: is) thydata = neuper@55450: Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata]) wneuper@59414: | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive" neuper@55450: neuper@55450: fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata] neuper@55450: | add_thydata (exist, [i]) data (pys as (py as Ptyp (key, _, _)) :: pyss) = neuper@55450: if i = key neuper@55450: then pys (* preserve existing thydata *) neuper@55450: else py :: add_thydata (exist, [i]) data pyss neuper@55450: | add_thydata (exist, iss as (i :: is)) data ((py as Ptyp (key, d, pys)) :: pyss) = neuper@55450: if i = key neuper@55450: then neuper@55450: if length pys = 0 neuper@55450: then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss neuper@55450: else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss neuper@55450: else py :: add_thydata (exist, iss) data pyss wneuper@59414: | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive" neuper@55448: neuper@55448: fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' = neuper@55448: Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, neuper@55448: fillpats = fillpats', thm = thm} wneuper@59414: | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments"; neuper@55448: wneuper@59414: (* for dialog-authoring *) neuper@55448: fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs = wneuper@59414: let wneuper@59414: val rls' = wneuper@59414: case rls of wneuper@59415: Rule.Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} wneuper@59415: => Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, wneuper@59414: calc = calc, rules = rules, scr = scr, errpatts = errpatIDs} wneuper@59415: | Rule.Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} wneuper@59415: => Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, wneuper@59414: calc = calc, rules = rules, scr = scr, errpatts = errpatIDs} wneuper@59415: | Rule.Rrls {id, prepat, rew_ord, erls, calc, scr, ...} wneuper@59415: => Rule.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc, wneuper@59414: scr = scr, errpatts = errpatIDs} wneuper@59414: | Erls => Erls wneuper@59414: in wneuper@59414: Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, wneuper@59414: thy_rls = (thyID, rls')} wneuper@59414: end wneuper@59414: | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments"; wneuper@59414: wneuper@59414: fun app_py p f (d:pblID) (k(*:pblRD*)) = neuper@55448: let wneuper@59414: fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d); neuper@55448: fun app_py' _ [] = py_err () neuper@55448: | app_py' [] _ = py_err () wneuper@59414: | app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) = wneuper@59414: if k0 = k' then f p' else app_py' [k0] ps wneuper@59414: | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') = wneuper@59414: if k0 = k'' then app_py' ks ps else app_py' k' ps'; neuper@55448: in app_py' k p end; wneuper@59414: fun get_py p = wneuper@59414: let wneuper@59414: fun extract_py (Ptyp (_, [py], _)) = py wneuper@59414: | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format."); wneuper@59414: in app_py p extract_py end; neuper@55448: neuper@55448: fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *) neuper@55448: let neuper@55448: fun update_elem th (theID, fillpats) = neuper@55437: let neuper@55448: val hthm = get_py th theID theID neuper@55448: val hthm' = update_hthm hthm fillpats neuper@55448: handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") neuper@55448: in update_ptyps theID theID hthm' end neuper@55448: in fold (update_elem th) fis end neuper@55456: neuper@55456: (* group the theories defined in Isac, compare Build_Thydata: neuper@55456: section "Get and group the theories defined in Isac" *) wneuper@59397: fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*) neuper@55456: let wneuper@59415: val allthys = Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata") neuper@55456: in wneuper@59366: drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys) neuper@55456: end neuper@55456: fun knowthys () = (*["Isac", .., "Descript", "Delete"]*) neuper@55456: let neuper@55456: fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *) neuper@55456: let wneuper@59332: val allthys = filter_out (member Context.eq_thy wneuper@59415: [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret", wneuper@59415: Rule.Thy_Info_get_theory "xmlsrc", Rule.Thy_Info_get_theory "Frontend"]) wneuper@59415: (Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata")) neuper@55456: in wneuper@59366: take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), neuper@55456: allthys) neuper@55456: end neuper@55456: val isacthys' = isacthys () wneuper@59415: val proglang_parent = Rule.Thy_Info_get_theory "ProgLang" neuper@55456: in wneuper@59332: take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys') neuper@55456: end wneuper@59414: neuper@55456: fun progthys () = (*["Isac", .., "Descript", "Delete"]*) neuper@55456: let neuper@55456: fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *) wneuper@59415: let wneuper@59332: val allthys = filter_out (member Context.eq_thy wneuper@59415: [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret", wneuper@59415: Rule.Thy_Info_get_theory "xmlsrc", Rule.Thy_Info_get_theory "Frontend"]) wneuper@59415: (Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata")) neuper@55456: in wneuper@59366: take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), neuper@55456: allthys) neuper@55456: end neuper@55456: val isacthys' = isacthys () wneuper@59415: val proglang_parent = Rule.Thy_Info_get_theory "ProgLang" neuper@55456: in wneuper@59332: drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys') neuper@55456: end neuper@55456: neuper@55456: fun partID thy = wneuper@59332: if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge" wneuper@59332: else if member Context.eq_thy (progthys ()) thy then "IsacScripts" wneuper@59332: else if member Context.eq_thy (isabthys ()) thy then "Isabelle" wneuper@59415: else error ("closure of thys in Isac is broken by " ^ Rule.string_of_thy thy) wneuper@59415: fun partID' thy' = partID (Rule.Thy_Info_get_theory thy') wneuper@59405: neuper@38061: end (*struct*) wneuper@59405: