neuper@37906: (* elements of calculations. neuper@37906: they are partially held in association lists as ref's for neuper@37906: switching language levels (meta-string, object-values). neuper@37906: 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: neuper@38061: (* neuper@38061: structure CalcElems = neuper@38061: struct neuper@38061: *) neuper@37906: val linefeed = (curry op^) "\n"; neuper@37906: type authors = string list; neuper@37906: neuper@37906: type cterm' = string; neuper@37906: val empty_cterm' = "empty_cterm'"; neuper@42399: 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: neuper@37906: type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*) neuper@37906: type thm'' = thmID * term; neuper@37906: type rls' = string; 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: val e_guh = "e_guh":guh; neuper@37906: neuper@37906: type xml = string; neuper@37906: neuper@52154: (* eval function calling sml code during rewriting. neuper@52154: Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient, neuper@52154: see "fun rule2stac": instead of neuper@52154: Calc: calID * eval_fn -> rule neuper@52154: would be better neuper@52154: Calc: prog_calcID * (calID * eval_fn)) -> rule*) neuper@37906: type eval_fn = (string -> term -> theory -> (string * term) option); neuper@37906: fun e_evalfn (_:'a) (_:term) (_:theory) = NONE:(string * term) option; neuper@37906: (*. op in isa-term 'Const(op,_)' .*) neuper@37906: type calID = string; neuper@52154: neuper@52154: (* *) neuper@37906: type cal = (calID * eval_fn); neuper@37906: (*. fun calculate_ fetches the evaluation-function via this list. *) neuper@52117: type prog_calcID = string; neuper@52117: type calc = (prog_calcID * cal); neuper@52141: type calc_elem = neuper@52141: prog_calcID * (* a simple identifier used in programs *) neuper@52141: (calID * (* a long identifier used in Const *) neuper@52141: eval_fn) (* an ML function *) neuper@52141: fun calc_eq ((pi1, (ci1, _)) : calc_elem, (pi2, (ci2, _)) : calc_elem) = neuper@52141: if pi1 = pi2 neuper@52141: then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2) neuper@52141: else false neuper@52141: neuper@37906: neuper@37906: type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*) neuper@37906: type subst = (term * term) list; (*here for ets2str*) neuper@37906: val e_subst = []:(term * term) list; neuper@37906: neuper@37906: (*TODO.WN060610 make use of "type rew_ord" total*) neuper@37906: type rew_ord' = string; neuper@37906: val e_rew_ord' = "e_rew_ord" : rew_ord'; neuper@37906: type rew_ord_ = subst -> Term.term * Term.term -> bool; neuper@37906: fun dummy_ord (_:subst) (_:term,_:term) = true; neuper@37906: val e_rew_ord_ = dummy_ord; neuper@37906: type rew_ord = rew_ord' * rew_ord_; neuper@37906: val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*) neuper@37906: val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord; neuper@37906: neuper@42451: (* error patterns and fill patterns *) neuper@42451: type errpatID = string neuper@42451: type errpat = neuper@42451: errpatID (* one identifier for a list of patterns neuper@42451: DESIGN ?TODO: errpatID list for hierarchy of errpats ? *) neuper@42451: * term list (* error patterns *) neuper@42451: * thm list (* thms related to error patterns; note that respective lhs neuper@42451: do not match (which reflects student's error). neuper@42451: fillpatterns are stored with these thms. *) 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 *) neuper@42451: * errpatID; (* which the fillpat would be a help for neuper@42451: DESIGN ?TODO: list for several patterns ? *) neuper@37906: neuper@40836: datatype rule = neuper@37906: Erule (*.the empty rule .*) neuper@40836: | Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*) neuper@37906: | Calc of string * (*.sml-code manipulating a (sub)term .*) neuper@37906: (string -> term -> theory -> (string * term) option) neuper@37906: | Cal1 of string * (*.sml-code applied only to whole term neuper@37906: or left/right-hand-side of eqality .*) neuper@37906: (string -> term -> theory -> (string * term) option) neuper@37906: | Rls_ of rls (*.ie. rule sets may be nested.*) neuper@40836: and scr = neuper@40836: EmptyScr neuper@52084: | Prog of term (* for met *) neuper@52101: | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *) neuper@52084: {init_state : (* initialise for reverse rewriting by the Interpreter *) neuper@52084: term -> (* for this the rrlsstate is initialised: *) neuper@52084: term * (* the current formula: goes locate_gen -> next_tac via istate *) neuper@52084: term * (* the final formula *) neuper@52084: rule list (* of reverse rewrite set (#1#) *) neuper@52084: list * (* may be serveral, eg. in norm_rational *) neuper@52084: ( rule * (* Thm (+ Thm generated from Calc) resulting in ... *) neuper@52084: (term * (* ... rewrite with ... *) neuper@52084: term list)) (* ... assumptions *) neuper@52084: list, (* derivation from given term to normalform neuper@52084: in reverse order with sym_thm; neuper@52084: (#1#) could be extracted from here #1 *) neuper@52084: normal_form: (* the function which drives the Rrls ##############################*) neuper@52084: term -> (term * term list) option, neuper@52084: locate_rule: (* checks a rule R for being a cancel-rule, and if it is, neuper@52084: then return the list of rules (+ the terms they are rewriting to) neuper@52084: which need to be applied before R should be applied. neuper@52084: precondition: the rule is applicable to the argument-term. *) neuper@52084: rule list list -> (* the reverse rule list *) neuper@52084: term -> (* ... to which the rule shall be applied *) neuper@52084: rule -> (* ... to be applied to term *) neuper@52084: ( rule * (* value: a rule rewriting to ... *) neuper@52084: (term * (* ... the resulting term ... *) neuper@52084: term list)) (* ... with the assumptions ( //#0) *) neuper@52084: list, (* there may be several such rules; the list is empty, neuper@52084: if the rule has nothing to do with e.g. cancelation *) neuper@52084: next_rule: (* for a given term return the next rules to be done for cancelling *) neuper@52084: rule list list->(* the reverse rule list *) neuper@52084: term -> (* the term for which ... *) neuper@52084: rule option, (* ... this rule is appropriate for cancellation; neuper@52084: there may be no such rule (if the term is eg.canceled already*) neuper@52084: attach_form: (* checks an input term TI, if it may belong to e.g. a current neuper@52084: cancellation, by trying to derive it from the given term TG. neuper@52084: NOT IMPLEMENTED *) neuper@52084: rule list list->(**) neuper@52084: term -> (* TG, the last one agreed upon by user + math-eng *) neuper@52084: term -> (* TI, the next one input by the user *) neuper@52084: ( rule * (* the rule to be applied in order to reach TI *) neuper@52084: (term * (* ... obtained by applying the rule ... *) neuper@52084: term list)) (* ... and the respective assumptions *) neuper@52084: list} (* there may be several such rules; the list is empty, if the neuper@52084: users term does not belong to e.g. a cancellation of the term neuper@52084: last agreed upon. *) neuper@37906: and rls = neuper@37906: Erls (*for init e_rls*) neuper@40836: neuper@37906: | Rls of (*a confluent and terminating ruleset, in general *) neuper@37906: {id : string, (*for trace_rewrite:=true *) neuper@37906: preconds : term list, (*unused WN020820 *) neuper@37906: (*WN060616 for efficiency... s1210629013@55444: bdvs : false, (*set in prep_rls' for get_bdvs *)*) neuper@37906: rew_ord : rew_ord, (*for rules*) neuper@37906: erls : rls, (*for the conditions in rules *) neuper@37906: srls : rls, (*for evaluation of list_fns in script *) s1210629013@55444: calc : calc list, (*for Calculate in scr, set by prep_rls' *) neuper@37906: rules : rule list, neuper@42451: errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*) neuper@48763: scr : scr} (*Prog term: generating intermed.steps *) neuper@37906: | Seq of (*a sequence of rules to be tried only once *) neuper@37906: {id : string, (*for trace_rewrite:=true *) neuper@37906: preconds : term list, (*unused 20.8.02 *) neuper@37906: (*WN060616 for efficiency... s1210629013@55444: bdvs : false, (*set in prep_rls' for get_bdvs *)*) neuper@37906: rew_ord : rew_ord, (*for rules *) neuper@37906: erls : rls, (*for the conditions in rules *) neuper@37906: srls : rls, (*for evaluation of list_fns in script *) s1210629013@55444: calc : calc list, (*for Calculate in scr, set by prep_rls' *) neuper@37906: rules : rule list, neuper@42451: errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*) neuper@48763: scr : scr} (*Prog term (how to restrict type ???)*) neuper@52084: neuper@37906: (*Rrls call SML-code and simulate an rls neuper@37906: difference: there is always _ONE_ redex rewritten in 1 call, neuper@37906: thus wrap Rrls by: Rls (Rls_ ...)*) neuper@52084: | Rrls of (* SML-functions within rewriting; step-wise execution provided; neuper@52084: Rrls simulate an rls neuper@52084: difference: there is always _ONE_ redex rewritten in 1 call, neuper@52084: thus wrap Rrls by: Rls (Rls_ ...) *) neuper@38036: {id : string, (* for trace_rewrite := true *) neuper@40836: prepat : (term list *(* preconds, eval with subst from pattern; neuper@52084: if [@{term True}], match decides alone *) neuper@52084: term ) (* pattern matched with current (sub)term *) neuper@52084: list, (* meta-conjunction is or *) neuper@38036: rew_ord : rew_ord, (* for rules *) neuper@38036: erls : rls, (* for the conditions in rules and preconds *) s1210629013@55444: calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *) neuper@42451: errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*) neuper@38036: scr : scr}; (* Rfuns {...} (how to restrict type ???) *) neuper@37906: neuper@48760: fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*) neuper@48760: fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*) neuper@37906: neuper@48760: fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*) neuper@48760: neuper@40836: val e_rule = Thm ("refl", @{thm refl}); neuper@37906: fun id_of_thm (Thm (id, _)) = id neuper@52101: | id_of_thm _ = error "error id_of_thm"; neuper@37906: fun thm_of_thm (Thm (_, thm)) = thm neuper@52101: | thm_of_thm _ = error "error thm_of_thm"; neuper@37906: fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); neuper@38061: neuper@38061: fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); neuper@38061: fun thyID_of_derivation_name dn = hd (space_explode "." dn); neuper@38061: neuper@37906: fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = neuper@37906: (strip_thy thmid1) = (strip_thy thmid2); neuper@42372: (*WN120201 weakened*) neuper@42372: fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _)) = thmid1 = thmid2; neuper@38002: (*version typed weaker WN100910*) neuper@38002: fun eq_thmI' ((thmid1, _), (thmid2, _)) = neuper@38061: (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); neuper@37906: neuper@42437: val string_of_thm = Thm.get_name_hint; (*FIXME.2009*) neuper@42437: fun thm'_of_thm thm = neuper@42437: ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm' neuper@37906: neuper@37906: (*check for [.] as caused by "fun assoc_thm'"*) neuper@37906: fun string_of_thmI thm = neuper@37906: let val ct' = (de_quote o string_of_thm) thm neuper@40836: val (a, b) = split_nlast (5, Symbol.explode ct') neuper@40836: in case b of neuper@37906: [" ", " ","[", ".", "]"] => implode a neuper@37906: | _ => ct' neuper@37906: end; neuper@37906: neuper@37906: (*.id requested for all, Rls,Seq,Rrls.*) neuper@37906: fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*) neuper@37906: | id_rls (Rls {id,...}) = id neuper@37906: | id_rls (Seq {id,...}) = id neuper@37906: | id_rls (Rrls {id,...}) = id; neuper@37906: val rls2str = id_rls; neuper@37906: fun id_rule (Thm (id, _)) = id neuper@37906: | id_rule (Calc (id, _)) = id neuper@37906: | id_rule (Rls_ rls) = id_rls rls; neuper@37906: neuper@37906: fun get_rules (Rls {rules,...}) = rules neuper@37906: | get_rules (Seq {rules,...}) = rules neuper@37906: | get_rules (Rrls _) = []; neuper@37906: neuper@37906: fun rule2str Erule = "Erule" neuper@37906: | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")" neuper@37906: | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)" neuper@37906: | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" neuper@37906: | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; neuper@37906: fun rule2str' Erule = "Erule" neuper@37906: | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")" neuper@37906: | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)" neuper@37906: | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)" neuper@37906: | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")"; neuper@37906: neuper@37906: (*WN080102 compare eq_rule ?!?*) neuper@37906: fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2 neuper@37906: | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2 neuper@37906: | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2 neuper@37906: | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*) neuper@37906: | eqrule _ = false; neuper@37906: neuper@52084: type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *) neuper@52084: (term * term * rule list list * (rule * (term * term list)) list); neuper@37906: neuper@37906: val e_type = Type("empty",[]); neuper@37906: val a_type = TFree("'a",[]); neuper@37906: val e_term = Const("empty",e_type); neuper@37906: val a_term = Free("empty",a_type); neuper@37906: val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate; neuper@37906: neuper@37906: val e_term = Const("empty", Type("'a", [])); neuper@48763: val e_scr = Prog e_term; neuper@37906: neuper@37906: (*ad thm': neuper@37906: there are two kinds of theorems ... neuper@37906: (1) known by isabelle neuper@37906: (2) not known, eg. calc_thm, instantiated rls neuper@37906: the latter have a thmid "#..." neuper@37906: and thus outside isa we ALWAYS transport both (thmid,string_of_thmI) neuper@37906: and have a special assoc_thm / assoc_rls in this interface *) neuper@38058: type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*) neuper@38058: type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*) neuper@37906: type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*) neuper@37906: neuper@37906: fun string_of_thy thy = Context.theory_name thy: theory'; neuper@37906: val theory2domID = string_of_thy; neuper@37906: val theory2thyID = (get_thy o string_of_thy) : theory -> thyID; neuper@37906: val theory2theory' = string_of_thy; neuper@37906: val theory2str = string_of_thy; (*WN050903 ..most consistent naming*) neuper@40836: val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy; neuper@48795: (* fun theory'2theory = fun thyID2thy ... see fun assoc_thy (...Thy_Info.get_theory string); neuper@37906: al it = "Isac" : string neuper@37906: *) neuper@37906: neuper@38058: fun thyID2theory' (thyID:thyID) = thyID; neuper@38058: (* neuper@40836: let val ss = Symbol.explode thyID neuper@37906: val ext = implode (takelast (4, ss)) neuper@37906: in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*) neuper@37906: else thyID ^ ".thy" neuper@37906: end; neuper@38058: *) neuper@37906: (* thyID2theory' "Isac" (*ok*); neuper@38050: val it = "Isac" : theory' neuper@38050: > thyID2theory' "Isac" (*abuse, goes ok...*); neuper@38050: val it = "Isac" : theory' neuper@37906: *) neuper@48880: neuper@38058: fun theory'2thyID (theory':theory') = theory'; neuper@38058: (* neuper@40836: let val ss = Symbol.explode theory' neuper@37906: val ext = implode (takelast (4, ss)) neuper@37906: in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID neuper@37906: else theory' (*disarm abuse of theory'*) neuper@37906: end; neuper@38058: *) neuper@38050: (* theory'2thyID "Isac"; neuper@37906: val it = "Isac" : thyID neuper@37906: > theory'2thyID "Isac"; neuper@37906: val it = "Isac" : thyID*) neuper@37906: neuper@37906: neuper@37906: (*. 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: neuper@40836: # always parse and type-check with Thy_Info.get_theory "Isac" neuper@37906: (rejected tue 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: # ??? neuper@37906: .*) neuper@40836: (*WN0509 TODO "ProtoPure" ... would be more consistent neuper@37906: with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*) neuper@37906: val e_domID = "e_domID":domID; neuper@37906: neuper@37906: (*the key into the hierarchy ob theory elements*) neuper@37906: type theID = string list; neuper@37906: val e_theID = ["e_theID"]; neuper@37906: val theID2str = strs2str; neuper@37906: (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*) neuper@37906: fun theID2thyID (theID:theID) = neuper@37906: if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID neuper@38031: else error ("theID2thyID called with "^ theID2str theID); neuper@37906: neuper@37906: (*the key into the hierarchy ob problems*) neuper@37906: type pblID = string list; (* domID::...*) neuper@37906: val e_pblID = ["e_pblID"]:pblID; neuper@37906: val pblID2str = strs2str; neuper@37906: neuper@37906: (*the key into the hierarchy ob methods*) neuper@37906: type metID = string list; neuper@37906: val e_metID = ["e_metID"]:metID; neuper@37906: val metID2str = strs2str; neuper@37906: s1210629013@52166: type spec = s1210629013@52166: domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in: s1210629013@52166: specify (Init_Proof..), nxt_specify_init_calc, s1210629013@52166: assod (.SubProblem...), stac2tac (.SubProblem...)*) s1210629013@52166: pblID * s1210629013@52166: metID; s1210629013@52166: s1210629013@52171: fun spec2str ((dom,pbl,met)(*:spec*)) = s1210629013@52171: "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^ s1210629013@52171: ", " ^ (strs2str met) ^ ")"; s1210629013@52171: (*> spec2str empty_spec; s1210629013@52171: val it = "(\"\", [], (\"\", \"\"))" : string *) s1210629013@52171: val empty_spec = (e_domID,e_pblID,e_metID):spec; s1210629013@52171: val e_spec = empty_spec; s1210629013@52171: s1210629013@52166: (*.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: val e_kestoreID = ["e_kestoreID"]; neuper@37906: val kestoreID2str = strs2str; neuper@37906: neuper@48892: (*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"; neuper@37906: neuper@37906: (*rewrite orders, also stored in 'type met' and type 'and rls' neuper@37906: The association list is required for 'rewrite.."rew_ord"..' neuper@37947: WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*) neuper@55432: val rew_ord' = Unsynchronized.ref neuper@38007: ([]:(rew_ord' * (*the key for the association list *) neuper@37906: (subst (*the bound variables - they get high order*) neuper@37906: -> (term * term) (*(t1, t2) to be compared *) neuper@37906: -> bool)) (*if t1 <= t2 then true else false *) neuper@37906: list); (*association list *) neuper@38061: neuper@37906: rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), neuper@37906: ("dummy_ord", dummy_ord)]); neuper@37906: 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. neuper@48887: 'a is for pbt | met | thydata; after WN030424 naming became inappropriate *) neuper@40836: datatype 'a ptyp = neuper@48887: Ptyp of string * (* element of the key *) neuper@48887: 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69) neuper@48887: presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *) neuper@48887: ('a ptyp) list;(* the children nodes *) neuper@37906: neuper@37906: (*.datatype for collecting thydata for hierarchy.*) neuper@37906: (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*) neuper@37906: (*WN0606 Htxt contains html which does not belong to the sml-kernel*) neuper@37906: datatype thydata = Html of {guh: guh, neuper@37906: coursedesign: authors, neuper@37906: mathauthors: authors, neuper@37906: html: string} (*html; for demos before database*) neuper@37906: | Hthm of {guh: guh, neuper@37906: coursedesign: authors, neuper@37906: mathauthors: authors, neuper@42429: fillpats: fillpat list, neuper@38002: thm: term} neuper@37906: | Hrls of {guh: guh, neuper@37906: coursedesign: authors, neuper@37906: mathauthors: authors, neuper@37906: thy_rls: (thyID * rls)} neuper@37906: | Hcal of {guh: guh, neuper@37906: coursedesign: authors, neuper@37906: mathauthors: authors, neuper@37906: calc: calc} neuper@37906: | Hord of {guh: guh, neuper@37906: coursedesign: authors, neuper@37906: mathauthors: authors, neuper@37906: ord: (subst -> (term * term) -> bool)}; neuper@37906: val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; neuper@55435: fun the2str (Html {guh, coursedesign, mathauthors, html}) = guh : string neuper@55435: | the2str (Hthm {guh, coursedesign, mathauthors, fillpats, thm}) = guh neuper@55435: | the2str (Hrls {guh, coursedesign, mathauthors, thy_rls}) = guh neuper@55435: | the2str (Hcal {guh, coursedesign, mathauthors, calc}) = guh neuper@55435: | the2str (Hord {guh, coursedesign, mathauthors, ord}) = guh neuper@55435: fun thes2str thes = map the2str thes |> list2str; neuper@37906: neuper@37906: type thehier = (thydata ptyp) list; neuper@55405: (* required to determine sequence of main nodes of thehier in KEStore.thy *) neuper@55405: fun part2guh ([str]:theID) = neuper@55405: (case str of neuper@55405: "Isabelle" => "thy_isab_" ^ str ^ "-part" : guh neuper@55405: | "IsacScripts" => "thy_scri_" ^ str ^ "-part" neuper@55405: | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part" neuper@55405: | str => error ("thy2guh: called with '"^str^"'")) neuper@55405: | part2guh theID = error ("part2guh called with theID = " ^ theID2str theID); neuper@37906: neuper@55437: fun thy2guh ([part, thyID] : theID) = (case part of neuper@55437: "Isabelle" => "thy_isab_" ^ thyID : guh neuper@55437: | "IsacScripts" => "thy_scri_" ^ thyID neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ thyID neuper@55437: | str => error ("thy2guh: called with '" ^ str ^ "'")) neuper@55437: | thy2guh theID = error ("thy2guh called with '" ^ strs2str' theID ^ "'"); neuper@55437: neuper@55437: fun thypart2guh ([part, thyID, thypart] : theID) = case part of neuper@55437: "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh neuper@55437: | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart neuper@55437: | str => error ("thypart2guh: called with '" ^ str ^ "'"); neuper@55437: neuper@55437: (* convert the data got via contextToThy to a globally unique handle neuper@55437: there is another way to get the guh out of the 'theID' in the hierarchy *) neuper@55437: fun thm2guh (isa, thyID:thyID) (thmID:thmID) = case isa of neuper@55437: "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID neuper@55437: | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID neuper@55437: | str => error ("thm2guh called with isa = '" ^ isa ^ "' for thm = " ^ thmID ^ "'"); neuper@55437: neuper@55437: fun rls2guh (isa, thyID:thyID) (rls':rls') = case isa of neuper@55437: "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' neuper@55437: | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' neuper@55437: | str => error ("rls2guh called with isa = '" ^ isa ^ "' for rls = '" ^ rls' ^ "'"); neuper@55437: neuper@55437: fun cal2guh (isa, thyID:thyID) calID = case isa of neuper@55437: "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID neuper@55437: | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID neuper@55437: | str => error ("cal2guh called with isa = '" ^ isa ^ "' for cal = '" ^ calID ^ "'"); neuper@55437: neuper@55437: fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') = case isa of neuper@55437: "Isabelle" => "thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh neuper@55437: | "IsacKnowledge" => "thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' neuper@55437: | "IsacScripts" => "thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' neuper@55437: | str => error ("ord2guh called with isa = '" ^ isa ^ "' for ord = '" ^ rew_ord' ^ "'"); neuper@55437: neuper@55437: (* not only for thydata, but also for thy's etc *) neuper@55437: fun theID2guh (theID : 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] neuper@55437: | str => error ("theID2guh: called with theID = " ^ strs2str' theID) neuper@55437: end neuper@55437: | n => error ("theID2guh called with theID = " ^ strs2str' theID); neuper@55437: neuper@40836: (* an association list, gets the value once in Isac.ML. neuper@38061: stores Isabelle's thms as terms for compatibility with Theory.axioms_of. neuper@38061: WN1-1-28 make this data arguments and del ref ?*) neuper@42400: val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list); neuper@42400: val isabthys = Unsynchronized.ref ([] : theory list); neuper@42400: neuper@37906: neuper@37906: type path = string; neuper@37906: type filename = string; neuper@37906: neuper@37906: (*val xxx = fn: a b => (a,b); ??? fun-definition ???*) neuper@37906: local neuper@37906: fun ii (_:term) = e_rrlsstate; neuper@37906: fun no (_:term) = SOME (e_term,[e_term]); neuper@37906: fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))]; neuper@37906: fun ne (_:rule list list) (_:term) = SOME e_rule; neuper@37906: fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))]; neuper@37906: in neuper@37906: val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo, neuper@37906: next_rule=ne,attach_form=fo}; neuper@37906: end; neuper@37906: neuper@42458: val e_rls = neuper@42458: Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls, neuper@42458: srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls; neuper@42458: val e_rrls = neuper@42458: Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls, neuper@42458: calc = [], errpatts = [], scr=e_rfuns}:rls; neuper@42451: neuper@42451: fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) = neuper@37906: {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, neuper@37906: (*asm_thm=asm_thm,*)rules=rules,scr=scr} neuper@42451: | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,errpatts,rules,scr}) = neuper@37906: {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, neuper@37906: (*asm_thm=asm_thm,*)rules=rules,scr=scr} neuper@37906: | rep_rls Erls = rep_rls e_rls neuper@37906: | rep_rls (Rrls {id,...}) = rep_rls e_rls neuper@38031: (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*); neuper@40836: (*| rep_rls (Seq {id,...}) = neuper@38031: error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); neuper@37906: --1.7.03*) neuper@42451: fun rep_rrls (Rrls {id, calc, erls, prepat, rew_ord, errpatts, neuper@42451: scr = Rfuns {attach_form, init_state, locate_rule, next_rule, normal_form}}) = neuper@42451: {id=id, calc=calc, erls=erls, prepat=prepat, neuper@42451: rew_ord=rew_ord, errpatts=errpatts, attach_form=attach_form, init_state=init_state, neuper@37906: locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} neuper@40836: | rep_rrls (Rls {id,...}) = neuper@38031: error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) neuper@40836: | rep_rrls (Seq {id,...}) = neuper@38031: error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); neuper@37906: neuper@37906: fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules =rs, errpatts=errpatts, scr=sc}) r = neuper@37906: (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules = rs @ r, errpatts=errpatts, scr=sc}:rls) neuper@37906: | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules =rs, errpatts=errpatts, scr=sc}) r = neuper@37906: (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules = rs @ r, errpatts=errpatts, scr=sc}:rls) neuper@40836: | append_rls id (Rrls _) _ = neuper@38031: error ("append_rls: not for reverse-rewrite-rule-set "^id); neuper@37906: neuper@37906: (*. are _atomic_ rules equal ?.*) neuper@37906: (*WN080102 compare eqrule ?!?*) neuper@37906: fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2 neuper@37906: | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2 neuper@37906: | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2 neuper@37906: (*id_rls checks for Rls, Seq, Rrls*) neuper@37906: | eq_rule _ = false; neuper@37906: neuper@52141: fun merge_ids rls1 rls2 = neuper@52141: let neuper@52141: val id1 = (#id o rep_rls) rls1 neuper@52141: val id2 = (#id o rep_rls) rls2 neuper@52141: in neuper@52141: if id1 = id2 then id1 neuper@52141: else "merged_" ^ id1 ^ "_" ^ id2 neuper@52141: end neuper@37906: fun merge_rls _ Erls rls = rls neuper@37906: | merge_rls _ rls Erls = rls neuper@52141: | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *) neuper@52141: | merge_rls _ _ (Rrls x) = Rrls x neuper@37906: | merge_rls id neuper@52141: (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1, neuper@52141: rules = rs1, errpatts = eps1, scr = sc1, ...}) neuper@52141: (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2, neuper@52141: rules = rs2, errpatts = eps2, ...}) neuper@52141: = neuper@52141: (Rls {id = id, rew_ord = ro1, scr = sc1, neuper@52141: preconds = union (op =) pc1 pc2, neuper@52141: erls = merge_rls (merge_ids er1 er2) er1 er2, neuper@52141: srls = merge_rls (merge_ids sr1 sr2) sr1 sr2, neuper@52141: calc = union calc_eq ca1 ca2, neuper@52141: rules = union eq_rule rs1 rs2, neuper@52141: errpatts = union (op =) eps1 eps2} : rls) neuper@37906: | merge_rls id neuper@52141: (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1, neuper@52141: rules = rs1, errpatts = eps1, scr = sc1, ...}) neuper@52141: (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2, neuper@52141: rules = rs2, errpatts = eps2, ...}) neuper@52141: = neuper@52141: (Seq {id = id, rew_ord = ro1, scr = sc1, neuper@52141: preconds = union (op =) pc1 pc2, neuper@52141: erls = merge_rls (merge_ids er1 er2) er1 er2, neuper@52141: srls = merge_rls (merge_ids sr1 sr2) sr1 sr2, neuper@52141: calc = union calc_eq ca1 ca2, neuper@52141: rules = union eq_rule rs1 rs2, neuper@52141: errpatts = union (op =) eps1 eps2} : rls) neuper@52141: | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^ neuper@52141: "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq"); neuper@42451: neuper@37906: fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules=rs, errpatts=eps, scr=sc}) r = neuper@37906: (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules = gen_rems eq_rule (rs, r), neuper@42451: errpatts = eps(*gen_rems op= (eps, TODO)*), neuper@37906: scr=sc}:rls) neuper@37906: | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules =rs, errpatts=eps, scr=sc}) r = neuper@37906: (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, neuper@42451: rules = gen_rems eq_rule (rs, r), neuper@42451: errpatts = eps(*gen_rems op= (eps, TODO)*), neuper@37906: scr=sc}:rls) neuper@40836: | remove_rls id (Rrls _) _ = error neuper@37906: ("remove_rls: not for reverse-rewrite-rule-set "^id); neuper@37906: neuper@52141: (* datastructure for KEStore_Elems, intermediate for thehier *) neuper@52141: type rlss_elem = neuper@52141: (rls' * (* identifier unique within Isac *) neuper@52141: (theory' * (* just for assignment in thehier, not appropriate for parsing etc *) neuper@52141: 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 = neuper@52141: case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of neuper@52141: NONE => re :: ys neuper@52141: | SOME (i, (_, (_, r2))) => neuper@52141: let neuper@52141: val r12 = merge_rls id r1 r2 neuper@52141: in list_update ys i (id, (thyID, r12)) end neuper@52141: neuper@52141: fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2; neuper@52141: neuper@52141: neuper@37906: fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) neuper@37906: | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) neuper@38031: | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r)); neuper@37906: neuper@38031: fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known") neuper@37906: | assoc' ((keyi, xi) :: pairs, key) = neuper@37906: if key = keyi then SOME xi else assoc' (pairs, key); neuper@37906: neuper@37927: (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) neuper@38031: handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*) neuper@38056: fun assoc_thy (thy:theory') = neuper@40836: if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*) neuper@40836: else (Thy_Info.get_theory thy) neuper@38056: handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system"); neuper@40836: neuper@37906: (*.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; neuper@37906: this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*) neuper@40836: (*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... neuper@37906: actually a hack to get alltogether run again with minimal effort*) neuper@37906: fun insthy thy' (rls', rls) = (rls', (thy', rls)); neuper@37906: fun overwritelthy thy (al, bl:(rls' * rls) list) = neuper@37906: let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl neuper@37906: in overwritel (al, bl') end; neuper@37906: neuper@37906: fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro)) neuper@38031: handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system"); neuper@37906: (*get the string for stac from rule*) neuper@37906: neuper@52070: fun term_to_string' ctxt t = neuper@52065: let neuper@52070: val ctxt' = Config.put show_markup false ctxt neuper@52070: in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; neuper@52070: fun term_to_string'' (thyID : thyID) t = neuper@52070: let neuper@52070: val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID)) neuper@52070: in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; neuper@52070: fun term_to_string''' thy t = neuper@52070: let neuper@52070: val ctxt' = Config.put show_markup false (Proof_Context.init_global thy) neuper@52065: in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; neuper@38051: s1210629013@55443: fun term2str t = term_to_string' (assoc_thy "Isac" |> thy2ctxt) t; s1210629013@55345: fun terms2strs ts = map term2str ts; s1210629013@55345: (*terms2strs [t1,t2] = ["1 + 2", "abc"];*) s1210629013@55345: val terms2str = strs2str o terms2strs; neuper@38022: (*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*) s1210629013@55345: val terms2str' = strs2str' o terms2strs; neuper@38022: (*terms2str' [t1,t2] = "[1 + 2,abc]";*) neuper@38013: s1210629013@55345: fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")" neuper@38053: | termopt2str NONE = "NONE"; neuper@38053: neuper@52070: fun type_to_string' ctxt t = neuper@52070: let neuper@52070: val ctxt' = Config.put show_markup false ctxt neuper@52070: in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end; neuper@52070: fun type_to_string'' (thyID : thyID) t = neuper@52070: let neuper@52070: val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID)) neuper@52070: in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end; neuper@52070: fun type_to_string''' thy t = neuper@52070: let neuper@52070: val ctxt' = Config.put show_markup false (Proof_Context.init_global thy) neuper@52070: in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end; neuper@37906: neuper@52070: fun type2str typ = type_to_string'' "Isac" typ; (*legacy*) neuper@52070: val string_of_typ = type2str; (*legacy*) neuper@52070: fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*) neuper@52070: neuper@40836: fun subst2str (s:subst) = neuper@40836: (strs2str o neuper@37906: (map (linefeed o pair2str o neuper@40836: (apsnd term2str) o neuper@37906: (apfst term2str)))) s; neuper@40836: fun subst2str' (s:subst) = neuper@40836: (strs2str' o neuper@37906: (map (pair2str o neuper@40836: (apsnd term2str) o neuper@37906: (apfst term2str)))) s; neuper@37906: (*> subst2str' [(str2term "bdv", str2term "x"), neuper@37906: (str2term "bdv_2", str2term "y")]; neuper@37906: val it = "[(bdv, x)]" : string neuper@37906: *) neuper@37906: val env2str = subst2str; neuper@37906: neuper@37906: neuper@37906: (*recursive defs:*) neuper@48763: fun scr2str (Prog s) = "Prog " ^ term2str s neuper@37906: | scr2str (Rfuns _) = "Rfuns"; neuper@37906: neuper@37906: neuper@37906: fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1; neuper@37906: neuper@37906: neuper@37906: (*.trace internal steps of isac's rewriter*) neuper@38006: val trace_rewrite = Unsynchronized.ref false; neuper@37906: (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) neuper@38006: val depth = Unsynchronized.ref 99999; neuper@37906: (*.no of rewrites exceeding this int -> NO rewrite.*) neuper@37906: (*WN060829 still unused...*) neuper@38006: val lim_rewrite = Unsynchronized.ref 99999; neuper@37906: (*.no of derivation-elements exceeding this int -> SOME derivation-elements.*) neuper@38006: val lim_deriv = Unsynchronized.ref 100; neuper@37906: (*.switch for checking guhs unique before storing a pbl or met; neuper@37906: set true at startup (done at begin of ROOT.ML) neuper@37906: set false for editing IsacKnowledge (done at end of ROOT.ML).*) neuper@41905: val check_guhs_unique = Unsynchronized.ref true; neuper@37906: neuper@37906: neuper@37906: datatype lrd = (*elements of a path (=loc_) into an Isabelle term*) neuper@40836: L (*go left at $*) neuper@37906: | R (*go right at $*) neuper@37906: | 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"; neuper@37906: fun loc_2str (k:loc_) = (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) = neuper@55335: pair2str (field, pair2str (term2str dsc, 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: val e_pbt_ = ("#Undef", (e_term, e_term)) : pbt_ neuper@55335: type pbt = neuper@55335: {guh : guh, (* unique within this isac-knowledge *) neuper@55335: mathauthors : string list, (* copyright *) neuper@55335: init : pblID, (* to start refinement with *) neuper@55335: thy : theory, (* which allows to compile that pbt neuper@55335: TODO: search generalized for subthy (ref.p.69*) neuper@55335: (*^^^ WN050912 NOT used during application of the problem, neuper@55335: because applied terms may be from 'subthy' as well as from super; neuper@55335: thus we take 'maxthy'; see match_ags !*) neuper@55335: cas : term option, (* 'CAS-command'*) neuper@55335: prls : rls, (* for preds in where_*) neuper@55335: where_ : term list, (* where - predicates*) neuper@55335: ppc : pat list, (* this is the model-pattern; neuper@55335: it contains "#Given","#Where","#Find","#Relate"-patterns neuper@55335: for constraints on identifiers see "fun cpy_nam" *) neuper@55335: met : metID list} (* methods solving the pbt*) neuper@55335: neuper@55335: val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure", neuper@55335: cas = NONE, prls = Erls, where_ = [], ppc = [], met = []} : pbt s1210629013@55344: fun pbt2str s1210629013@55344: ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc', s1210629013@55345: prls = prls', thy = thy', where_ = w'} : pbt) = s1210629013@55344: "{cas = " ^ (termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = " s1210629013@55345: ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = " s1210629013@55345: ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = " s1210629013@55345: ^ (rls2str prls' |> quote) ^ ", thy = {" ^ (theory2str thy') ^ "}, where_ = " s1210629013@55345: ^ (terms2str w') ^ "}" |> linefeed; s1210629013@55345: fun pbts2str pbts = map pbt2str pbts |> list2str; neuper@55335: neuper@55335: val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]) neuper@55335: type ptyps = (pbt ptyp) list neuper@55335: neuper@55357: fun coll_pblguhs pbls = neuper@55357: let fun node coll (Ptyp (_,[n],ns)) = neuper@55357: [(#guh : pbt -> guh) n] @ (nodes coll ns) neuper@55357: and nodes coll [] = coll neuper@55357: | nodes coll (n::ns) = (node coll n) @ (nodes coll ns); neuper@55357: in nodes [] pbls end; neuper@55357: fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) = neuper@55357: if member op = (coll_pblguhs pbls) guh neuper@55357: then error ("check_guh_unique failed with '"^guh^"';\n"^ neuper@55357: "use 'sort_pblguhs()' for a list of guhs;\n"^ neuper@55357: "consider setting 'check_guhs_unique := false'") neuper@55357: else (); s1210629013@55339: neuper@55453: fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])] neuper@55453: | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) = neuper@55453: ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*) neuper@55453: if k = k' neuper@55453: then ((Ptyp (k', [pbt], ps)) :: pys) neuper@55453: else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys)) neuper@55453: ) s1210629013@55339: | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) = neuper@55453: ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*) neuper@55453: if k = k' neuper@55453: then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys) neuper@55453: else neuper@55453: if length pys = 0 neuper@55453: then error ("insert: not found " ^ (strs2str (d : pblID))) neuper@55453: else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys)) neuper@55453: ); 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)) 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 s1210629013@55346: | merge_ptyps ((x' as Ptyp (k, x, 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'); neuper@55448: fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2) s1210629013@55372: s1210629013@55372: (* data for methods stored in 'methods'-database*) s1210629013@55372: type met = s1210629013@55372: {guh : guh, (*unique within this isac-knowledge *) s1210629013@55372: mathauthors: string list,(*copyright *) s1210629013@55372: init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*) s1210629013@55372: rew_ord' : rew_ord', (*for rules in Detail s1210629013@55372: TODO.WN0509 store fun itself, see 'type pbt'*) s1210629013@55372: erls : rls, (*the eval_rls for cond. in rules FIXME "rls' s1210629013@55372: instead erls in "fun prep_met" *) s1210629013@55372: srls : rls, (*for evaluating list expressions in scr *) s1210629013@55372: prls : rls, (*for evaluating predicates in modelpattern *) s1210629013@55372: crls : rls, (*for check_elementwise, ie. formulae in calc.*) s1210629013@55372: nrls : rls, (*canonical simplifier specific for this met *) s1210629013@55372: errpats : errpat list,(*error patterns expected in this method *) s1210629013@55372: calc : calc list, (*Theory_Data in fun prep_met *) s1210629013@55372: (*branch : TransitiveB set in append_problem at generation ob pblobj s1210629013@55372: 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?? s1210629013@55372: see ME/calchead.sml 'fun is_copy_named'. *) s1210629013@55372: pre : term list, (*preconditions in where *) s1210629013@55372: scr : scr (*prep_met gets progam or string "empty_script"*) s1210629013@55372: }; s1210629013@55372: val e_met = {guh="met_empty",mathauthors=[],init=e_metID, s1210629013@55372: rew_ord' = "e_rew_ord'": rew_ord', s1210629013@55372: erls = e_rls, srls = e_rls, prls = e_rls, s1210629013@55372: calc = [], crls = e_rls, errpats = [], nrls= e_rls, s1210629013@55372: ppc = []: (string * (term * term)) list, s1210629013@55372: pre = []: term list, s1210629013@55372: scr = EmptyScr: scr}:met; s1210629013@55372: s1210629013@55372: s1210629013@55372: val e_Mets = Ptyp ("e_metID",[e_met],[]); s1210629013@55372: s1210629013@55372: type mets = (met ptyp) list; neuper@55335: s1210629013@55373: fun coll_metguhs mets = s1210629013@55373: let fun node coll (Ptyp (_,[n],ns)) = neuper@55428: [(#guh : met -> guh) n] @ (nodes coll ns) s1210629013@55373: and nodes coll [] = coll s1210629013@55373: | nodes coll (n::ns) = (node coll n) @ (nodes coll ns); s1210629013@55373: in nodes [] mets end; s1210629013@55373: s1210629013@55373: (* val (guh, mets) = ("met_test", !mets); s1210629013@55373: *) s1210629013@55373: fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = s1210629013@55373: if member op = (coll_metguhs mets) guh s1210629013@55373: then error ("check_guh_unique failed with '"^guh^"';\n"^ s1210629013@55373: "use 'sort_metguhs()' for a list of guhs;\n"^ s1210629013@55373: "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: neuper@55450: fun fill_parents (exist, [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]) neuper@55450: | fill_parents _ _ = 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 neuper@55450: | add_thydata _ _ _ = 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} neuper@55448: | update_hthm _ _ = raise ERROR "wrong data"; neuper@55448: neuper@55448: (* for interface for dialog-authoring *) neuper@55448: fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs = neuper@55448: let neuper@55448: val rls' = neuper@55448: case rls of neuper@55448: Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} => neuper@55448: Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, neuper@55448: calc = calc, rules = rules, scr = scr, errpatts = errpatIDs} neuper@55448: | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} => neuper@55448: Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, neuper@55448: calc = calc, rules = rules, scr = scr, errpatts = errpatIDs} neuper@55448: | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} => neuper@55448: Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc, neuper@55448: scr = scr, errpatts = errpatIDs} neuper@55448: | Erls => Erls neuper@55448: in neuper@55448: Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors, neuper@55448: thy_rls = (thyID, rls')} neuper@55448: end neuper@55448: | update_hrls _ _ = raise ERROR "wrong data"; neuper@55448: neuper@55448: fun app_py p f (d:pblID) (k(*:pblRD*)) = let neuper@55448: fun py_err _ = neuper@55448: error ("app_py: not found: " ^ (strs2str d)); neuper@55448: fun app_py' _ [] = py_err () neuper@55448: | app_py' [] _ = py_err () neuper@55448: | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) = neuper@55448: if k0 = k' then f p' else app_py' [k0] ps neuper@55448: | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') = neuper@55448: if k0 = k'' then app_py' ks ps else app_py' k' ps'; neuper@55448: in app_py' k p end; neuper@55448: neuper@55448: fun get_py p = let neuper@55448: fun extract_py (Ptyp (_, [py], _)) = py neuper@55448: | extract_py _ = error ("extract_py: Ptyp has wrong format."); neuper@55448: 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" *) neuper@55456: fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*) neuper@55456: let neuper@55456: val allthys = Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata") neuper@55456: in neuper@55456: drop ((find_index (curry Theory.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 neuper@55456: val allthys = filter_out (member Theory.eq_thy neuper@55456: [(*Thy_Info.get_theory "ProgLang",*) Thy_Info.get_theory "Interpret", neuper@55456: Thy_Info.get_theory "xmlsrc", Thy_Info.get_theory "Frontend"]) neuper@55456: (Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata")) neuper@55456: in neuper@55456: take ((find_index (curry Theory.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), neuper@55456: allthys) neuper@55456: end neuper@55456: val isacthys' = isacthys () neuper@55456: val proglang_parent = Thy_Info.get_theory "ProgLang" neuper@55456: in neuper@55456: take ((find_index (curry Theory.eq_thy proglang_parent) isacthys'), isacthys') neuper@55456: end neuper@55456: fun progthys () = (*["Isac", .., "Descript", "Delete"]*) neuper@55456: let neuper@55456: fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *) neuper@55456: let neuper@55456: val allthys = filter_out (member Theory.eq_thy neuper@55456: [(*Thy_Info.get_theory "ProgLang",*) Thy_Info.get_theory "Interpret", neuper@55456: Thy_Info.get_theory "xmlsrc", Thy_Info.get_theory "Frontend"]) neuper@55456: (Theory.ancestors_of (Thy_Info.get_theory "Build_Thydata")) neuper@55456: in neuper@55456: take ((find_index (curry Theory.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), neuper@55456: allthys) neuper@55456: end neuper@55456: val isacthys' = isacthys () neuper@55456: val proglang_parent = Thy_Info.get_theory "ProgLang" neuper@55456: in neuper@55456: drop ((find_index (curry Theory.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys') neuper@55456: end neuper@55456: neuper@55456: fun partID thy = neuper@55456: if member Theory.eq_thy (knowthys ()) thy then "IsacKnowledge" neuper@55456: else if member Theory.eq_thy (progthys ()) thy then "IsacScripts" neuper@55456: else if member Theory.eq_thy (isabthys ()) thy then "Isabelle" neuper@55456: else error ("closure of thys in Isac is broken by " ^ string_of_thy thy) neuper@55456: fun partID' (thy' : theory') = partID (Thy_Info.get_theory thy') neuper@38061: (* neuper@38061: end (*struct*) neuper@38061: *)