1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/calcelems.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,654 @@
1.4 +(* elements of calculations.
1.5 + they are partially held in association lists as ref's for
1.6 + switching language levels (meta-string, object-values).
1.7 + in order to keep these ref's during re-evaluation of code,
1.8 + they are defined here at the beginning of the code.
1.9 + author: Walther Neuper
1.10 + (c) isac-team 2003
1.11 +
1.12 +use"calcelems.sml";
1.13 +*)
1.14 +
1.15 +val linefeed = (curry op^) "\n";
1.16 +type authors = string list;
1.17 +
1.18 +type cterm' = string;
1.19 +val empty_cterm' = "empty_cterm'";
1.20 +type thmID = string;
1.21 +type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
1.22 +type thm'' = thmID * term;
1.23 +type rls' = string;
1.24 +(*.a 'guh'='globally unique handle' is a string unique for each element
1.25 + of isac's KEStore and persistent over time
1.26 + (in particular under shifts within the respective hierarchy);
1.27 + specialty for thys:
1.28 + # guh NOT resistant agains shifts from one thy to another
1.29 + (which is the price for Isabelle's design: thy's overwrite ids of subthy's)
1.30 + # requirement for matchTheory: induce guh from tac + current thy
1.31 + (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
1.32 + TODO: introduce to pbl, met.*)
1.33 +type guh = string;
1.34 +val e_guh = "e_guh":guh;
1.35 +
1.36 +type xml = string;
1.37 +
1.38 +(*. eval function calling sml code during rewriting.*)
1.39 +type eval_fn = (string -> term -> theory -> (string * term) option);
1.40 +fun e_evalfn (_:'a) (_:term) (_:theory) = NONE:(string * term) option;
1.41 +(*. op in isa-term 'Const(op,_)' .*)
1.42 +type calID = string;
1.43 +type cal = (calID * eval_fn);
1.44 +(*. fun calculate_ fetches the evaluation-function via this list. *)
1.45 +type calcID = string;
1.46 +type calc = (calcID * cal);
1.47 +
1.48 +type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
1.49 +type subst = (term * term) list; (*here for ets2str*)
1.50 +val e_subst = []:(term * term) list;
1.51 +
1.52 +(*TODO.WN060610 make use of "type rew_ord" total*)
1.53 +type rew_ord' = string;
1.54 +val e_rew_ord' = "e_rew_ord" : rew_ord';
1.55 +type rew_ord_ = subst -> Term.term * Term.term -> bool;
1.56 +fun dummy_ord (_:subst) (_:term,_:term) = true;
1.57 +val e_rew_ord_ = dummy_ord;
1.58 +type rew_ord = rew_ord' * rew_ord_;
1.59 +val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
1.60 +val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
1.61 +
1.62 +
1.63 +datatype rule =
1.64 + Erule (*.the empty rule .*)
1.65 +| Thm of (string * thm)(*.a theorem, ie (identifier, Thm.thm).*)
1.66 +| Calc of string * (*.sml-code manipulating a (sub)term .*)
1.67 + (string -> term -> theory -> (string * term) option)
1.68 +| Cal1 of string * (*.sml-code applied only to whole term
1.69 + or left/right-hand-side of eqality .*)
1.70 + (string -> term -> theory -> (string * term) option)
1.71 +| Rls_ of rls (*.ie. rule sets may be nested.*)
1.72 +and scr =
1.73 + EmptyScr
1.74 + | Script of term (*for met*)
1.75 + | Rfuns of {init_state : term ->
1.76 + (term * (*the current formula:
1.77 + goes locate_gen -> next_tac via istate*)
1.78 + term * (*the final formula*)
1.79 + rule list (*of reverse rewrite set (#1#)*)
1.80 + list * (*may be serveral, eg. in norm_rational*)
1.81 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
1.82 + (term * (*... rewrite with ...*)
1.83 + term list)) (*... assumptions*)
1.84 + list), (*derivation from given term to normalform
1.85 + in reverse order with sym_thm;
1.86 + (#1#) could be extracted from here #1*)
1.87 +
1.88 + normal_form: term -> (term * term list) option,
1.89 + locate_rule: rule list list -> term -> rule
1.90 + -> (rule * (term * term list)) list,
1.91 + next_rule : rule list list -> term -> rule option,
1.92 + attach_form: rule list list -> term -> term
1.93 + -> (rule * (term * term list)) list}
1.94 +and rls =
1.95 + Erls (*for init e_rls*)
1.96 +
1.97 + | Rls of (*a confluent and terminating ruleset, in general *)
1.98 + {id : string, (*for trace_rewrite:=true *)
1.99 + preconds : term list, (*unused WN020820 *)
1.100 + (*WN060616 for efficiency...
1.101 + bdvs : false, (*set in prep_rls for get_bdvs *)*)
1.102 + rew_ord : rew_ord, (*for rules*)
1.103 + erls : rls, (*for the conditions in rules *)
1.104 + srls : rls, (*for evaluation of list_fns in script *)
1.105 + calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.106 + rules : rule list,
1.107 + scr : scr} (*Script term: generating intermed.steps *)
1.108 + | Seq of (*a sequence of rules to be tried only once *)
1.109 + {id : string, (*for trace_rewrite:=true *)
1.110 + preconds : term list, (*unused 20.8.02 *)
1.111 + (*WN060616 for efficiency...
1.112 + bdvs : false, (*set in prep_rls for get_bdvs *)*)
1.113 + rew_ord : rew_ord, (*for rules *)
1.114 + erls : rls, (*for the conditions in rules *)
1.115 + srls : rls, (*for evaluation of list_fns in script *)
1.116 + calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.117 + rules : rule list,
1.118 + scr : scr} (*Script term (how to restrict type ???)*)
1.119 + (*Rrls call SML-code and simulate an rls
1.120 + difference: there is always _ONE_ redex rewritten in 1 call,
1.121 + thus wrap Rrls by: Rls (Rls_ ...)*)
1.122 +
1.123 + | Rrls of (*for 'reverse rewriting' by SML-functions instead Script*)
1.124 + {id : string, (*for trace_rewrite:=true *)
1.125 + prepat : (term list *(*preconds, eval with subst from pattern *)
1.126 + term ) (*pattern matched in subterms *)
1.127 + list, (*meta-conjunction is or *)
1.128 + rew_ord : rew_ord, (*for rules *)
1.129 + erls : rls, (*for the conditions in rules and pat *)
1.130 + (* '^ because of rewrite in applicable_in
1.131 + compare type met*)
1.132 + calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.133 + scr : scr}; (*Rfuns {...} (how to restrict type ???)*)
1.134 +(*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
1.135 + from rls, and then contain both Script _AND_ Rfuns !!!*)
1.136 +
1.137 +
1.138 +(*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
1.139 +val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");
1.140 +val HOL = ProofContext.theory_of ctxt_HOL;
1.141 +(*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
1.142 +fun ctxt_Isac _ = ProofContext.init_global (theory "Isac");
1.143 +fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
1.144 +
1.145 +val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
1.146 +fun id_of_thm (Thm (id, _)) = id
1.147 + | id_of_thm _ = raise error "id_of_thm";
1.148 +fun thm_of_thm (Thm (_, thm)) = thm
1.149 + | thm_of_thm _ = raise error "thm_of_thm";
1.150 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
1.151 +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
1.152 + (strip_thy thmid1) = (strip_thy thmid2);
1.153 +
1.154 +
1.155 +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
1.156 +(*check for [.] as caused by "fun assoc_thm'"*)
1.157 +fun string_of_thmI thm =
1.158 + let val ct' = (de_quote o string_of_thm) thm
1.159 + val (a, b) = split_nlast (5, explode ct')
1.160 + in case b of
1.161 + [" ", " ","[", ".", "]"] => implode a
1.162 + | _ => ct'
1.163 + end;
1.164 +
1.165 +(*.id requested for all, Rls,Seq,Rrls.*)
1.166 +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
1.167 + | id_rls (Rls {id,...}) = id
1.168 + | id_rls (Seq {id,...}) = id
1.169 + | id_rls (Rrls {id,...}) = id;
1.170 +val rls2str = id_rls;
1.171 +fun id_rule (Thm (id, _)) = id
1.172 + | id_rule (Calc (id, _)) = id
1.173 + | id_rule (Rls_ rls) = id_rls rls;
1.174 +
1.175 +fun get_rules (Rls {rules,...}) = rules
1.176 + | get_rules (Seq {rules,...}) = rules
1.177 + | get_rules (Rrls _) = [];
1.178 +
1.179 +fun rule2str Erule = "Erule"
1.180 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
1.181 + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.182 + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.183 + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.184 +fun rule2str' Erule = "Erule"
1.185 + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
1.186 + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.187 + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.188 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.189 +
1.190 +(*WN080102 compare eq_rule ?!?*)
1.191 +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
1.192 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.193 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
1.194 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
1.195 + | eqrule _ = false;
1.196 +
1.197 +
1.198 +type rrlsstate = (*state for reverse rewriting*)
1.199 + (term * (*the current formula:
1.200 + goes locate_gen -> next_tac via istate*)
1.201 + term * (*the final formula*)
1.202 + rule list (*of reverse rewrite set (#1#)*)
1.203 + list * (*may be serveral, eg. in norm_rational*)
1.204 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
1.205 + (term * (*... rewrite with ...*)
1.206 + term list)) (*... assumptions*)
1.207 + list); (*derivation from given term to normalform
1.208 + in reverse order with sym_thm;
1.209 + (#1#) could be extracted from here #1*)
1.210 +val e_type = Type("empty",[]);
1.211 +val a_type = TFree("'a",[]);
1.212 +val e_term = Const("empty",e_type);
1.213 +val a_term = Free("empty",a_type);
1.214 +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
1.215 +
1.216 +
1.217 +
1.218 +
1.219 +(*22.2.02: ging auf Linux nicht (Stefan)
1.220 +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
1.221 +val e_term = Const("empty", Type("'a", []));
1.222 +val e_scr = Script e_term;
1.223 +
1.224 +
1.225 +(*ad thm':
1.226 + there are two kinds of theorems ...
1.227 + (1) known by isabelle
1.228 + (2) not known, eg. calc_thm, instantiated rls
1.229 + the latter have a thmid "#..."
1.230 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
1.231 + and have a special assoc_thm / assoc_rls in this interface *)
1.232 +type theory' = string; (* = domID ^".thy" *)
1.233 +type domID = string; (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
1.234 +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.235 +
1.236 +(*2002 fun string_of_thy thy =
1.237 +((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory';*)
1.238 +fun string_of_thy thy = Context.theory_name thy: theory';
1.239 +val theory2domID = string_of_thy;
1.240 +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
1.241 +val theory2theory' = string_of_thy;
1.242 +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
1.243 +val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;
1.244 +(*> theory2str' Isac.thy;
1.245 +al it = "Isac" : string
1.246 +*)
1.247 +
1.248 +fun thyID2theory' (thyID:thyID) =
1.249 + let val ss = explode thyID
1.250 + val ext = implode (takelast (4, ss))
1.251 + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
1.252 + else thyID ^ ".thy"
1.253 + end;
1.254 +(* thyID2theory' "Isac" (*ok*);
1.255 +val it = "Isac.thy" : theory'
1.256 + > thyID2theory' "Isac.thy" (*abuse, goes ok...*);
1.257 +val it = "Isac.thy" : theory'
1.258 +*)
1.259 +
1.260 +fun theory'2thyID (theory':theory') =
1.261 + let val ss = explode theory'
1.262 + val ext = implode (takelast (4, ss))
1.263 + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
1.264 + else theory' (*disarm abuse of theory'*)
1.265 + end;
1.266 +(* theory'2thyID "Isac.thy";
1.267 +val it = "Isac" : thyID
1.268 +> theory'2thyID "Isac";
1.269 +val it = "Isac" : thyID*)
1.270 +
1.271 +
1.272 +(*. WN0509 discussion:
1.273 +#############################################################################
1.274 +# How to manage theorys in subproblems wrt. the requirement, #
1.275 +# that scripts should be re-usable ? #
1.276 +#############################################################################
1.277 +
1.278 + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq_,..'
1.279 + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
1.280 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
1.281 + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
1.282 + (see match_ags).
1.283 +
1.284 + Preliminary solution:
1.285 + # the thy in 'SubProblem (thy_, pbl, arglist)' is not taken automatically,
1.286 + # instead the 'maxthy (rootthy pt) thy_' is taken for each subpbl
1.287 + # however, a thy specified by the user in the rootpbl may lead to
1.288 + errors in far-off subpbls (which are not yet reported properly !!!)
1.289 + and interactively specifiying thys in subpbl is not very relevant.
1.290 +
1.291 + Other solutions possible:
1.292 + # always parse and type-check with Isac.thy
1.293 + (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.294 + # regard the subthy-relation in specifying thys of subpbls
1.295 + # specifically handle 'SubProblem (undefined_, pbl, arglist)'
1.296 + # ???
1.297 +.*)
1.298 +(*WN0509 TODO "ProtoPure" ... would be more consistent
1.299 + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
1.300 +val e_domID = "e_domID":domID;
1.301 +
1.302 +(*the key into the hierarchy ob theory elements*)
1.303 +type theID = string list;
1.304 +val e_theID = ["e_theID"];
1.305 +val theID2str = strs2str;
1.306 +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
1.307 +fun theID2thyID (theID:theID) =
1.308 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
1.309 + else raise error ("theID2thyID called with "^ theID2str theID);
1.310 +
1.311 +(*the key into the hierarchy ob problems*)
1.312 +type pblID = string list; (* domID::...*)
1.313 +val e_pblID = ["e_pblID"]:pblID;
1.314 +val pblID2str = strs2str;
1.315 +
1.316 +(*the key into the hierarchy ob methods*)
1.317 +type metID = string list;
1.318 +val e_metID = ["e_metID"]:metID;
1.319 +val metID2str = strs2str;
1.320 +
1.321 +(*either theID or pblID or metID*)
1.322 +type kestoreID = string list;
1.323 +val e_kestoreID = ["e_kestoreID"];
1.324 +val kestoreID2str = strs2str;
1.325 +
1.326 +(*for distinction of contexts*)
1.327 +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
1.328 +fun ketype2str Exp_ = "Exp_"
1.329 + | ketype2str Thy_ = "Thy_"
1.330 + | ketype2str Pbl_ = "Pbl_"
1.331 + | ketype2str Met_ = "Met_";
1.332 +fun ketype2str' Exp_ = "Example"
1.333 + | ketype2str' Thy_ = "Theory"
1.334 + | ketype2str' Pbl_ = "Problem"
1.335 + | ketype2str' Met_ = "Method";
1.336 +
1.337 +(*see 'How to manage theorys in subproblems' at 'type thyID'*)
1.338 +val theory' = ref ([]:(theory' * theory) list);
1.339 +
1.340 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
1.341 + in order to distinguish them from general IsacKnowledge defined later on.*)
1.342 +val script_thys = ref ([] : (theory' * theory) list);
1.343 +
1.344 +
1.345 +(*rewrite orders, also stored in 'type met' and type 'and rls'
1.346 + The association list is required for 'rewrite.."rew_ord"..'
1.347 + WN0509 tests not well-organized: see smltest/IsacKnowledge/termorder.sml*)
1.348 +val rew_ord' =
1.349 + ref ([]:(rew_ord' * (*the key for the association list *)
1.350 + (subst (*the bound variables - they get high order*)
1.351 + -> (term * term) (*(t1, t2) to be compared *)
1.352 + -> bool)) (*if t1 <= t2 then true else false *)
1.353 + list); (*association list *)
1.354 +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
1.355 + ("dummy_ord", dummy_ord)]);
1.356 +
1.357 +
1.358 +(*WN060120 a hack to get alltogether run again with minimal effort:
1.359 + theory' is inserted for creating thy_hierarchy; calls for assoc_rls
1.360 + need not be called*)
1.361 +val ruleset' = ref ([]:(rls' * (theory' * rls)) list);
1.362 +
1.363 +(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
1.364 +val calclist'= ref ([]: calc list);
1.365 +
1.366 +(*.the hierarchy of thydata.*)
1.367 +
1.368 +(*.'a is for pbt | met.*)
1.369 +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
1.370 +datatype 'a ptyp =
1.371 + Ptyp of string * (*element within pblID*)
1.372 + 'a list * (*several pbts with different domIDs/thy
1.373 + TODO: select by subthy (isaref.p.69)
1.374 + presently only _ONE_ elem*)
1.375 + ('a ptyp) list; (*the children nodes*)
1.376 +
1.377 +(*.datatype for collecting thydata for hierarchy.*)
1.378 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
1.379 +(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
1.380 +datatype thydata = Html of {guh: guh,
1.381 + coursedesign: authors,
1.382 + mathauthors: authors,
1.383 + html: string} (*html; for demos before database*)
1.384 + | Hthm of {guh: guh,
1.385 + coursedesign: authors,
1.386 + mathauthors: authors,
1.387 + thm: Thm.thm}
1.388 + | Hrls of {guh: guh,
1.389 + coursedesign: authors,
1.390 + mathauthors: authors,
1.391 + (*like vvvvvvvvvvvvv val ruleset'
1.392 + WN060711 redesign together !*)
1.393 + thy_rls: (thyID * rls)}
1.394 + | Hcal of {guh: guh,
1.395 + coursedesign: authors,
1.396 + mathauthors: authors,
1.397 + calc: calc}
1.398 + | Hord of {guh: guh,
1.399 + coursedesign: authors,
1.400 + mathauthors: authors,
1.401 + ord: (subst -> (term * term) -> bool)};
1.402 +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
1.403 +
1.404 +type thehier = (thydata ptyp) list;
1.405 +val thehier = ref ([] : thehier);
1.406 +
1.407 +(*.an association list, gets the value once in Isac.ML.*)
1.408 +val isab_thm_thy = ref ([] : (thmID * (thyID * thm)) list);
1.409 +
1.410 +
1.411 +type path = string;
1.412 +type filename = string;
1.413 +
1.414 +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
1.415 +local
1.416 + fun ii (_:term) = e_rrlsstate;
1.417 + fun no (_:term) = SOME (e_term,[e_term]);
1.418 + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
1.419 + fun ne (_:rule list list) (_:term) = SOME e_rule;
1.420 + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
1.421 +in
1.422 +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
1.423 + next_rule=ne,attach_form=fo};
1.424 +end;
1.425 +
1.426 +val e_rls =
1.427 + Rls{id = "e_rls",
1.428 + preconds = [],
1.429 + rew_ord = ("dummy_ord", dummy_ord),
1.430 + erls = Erls,srls = Erls,
1.431 + calc = [],
1.432 + rules = [], scr = EmptyScr}:rls;
1.433 +val e_rrls = Rrls {id = "e_rrls",
1.434 + prepat = [],
1.435 + rew_ord = ("dummy_ord", dummy_ord),
1.436 + erls = Erls,
1.437 + calc = [],
1.438 + (*asm_thm=[],*)
1.439 + scr=e_rfuns}:rls;
1.440 +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
1.441 + ("e_rrls",("Tools",e_rrls))
1.442 + ]);
1.443 +
1.444 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.445 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.446 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.447 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.448 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.449 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.450 + | rep_rls Erls = rep_rls e_rls
1.451 + | rep_rls (Rrls {id,...}) = rep_rls e_rls
1.452 + (*raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.453 +(*| rep_rls (Seq {id,...}) =
1.454 + raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.455 +--1.7.03*)
1.456 +fun rep_rrls
1.457 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.458 + scr=Rfuns
1.459 + {attach_form,init_state,locate_rule,
1.460 + next_rule,normal_form}}) =
1.461 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
1.462 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.463 + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.464 + | rep_rrls (Rls {id,...}) =
1.465 + raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.466 + | rep_rrls (Seq {id,...}) =
1.467 + raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.468 +
1.469 +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.470 + rules =rs,scr=sc}) r =
1.471 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.472 + rules = rs @ r,scr=sc}:rls)
1.473 + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.474 + rules =rs,scr=sc}) r =
1.475 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.476 + rules = rs @ r,scr=sc}:rls)
1.477 + | append_rls id (Rrls _) _ =
1.478 + raise error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.479 +
1.480 +(*. are _atomic_ rules equal ?.*)
1.481 +(*WN080102 compare eqrule ?!?*)
1.482 +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
1.483 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.484 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
1.485 + (*id_rls checks for Rls, Seq, Rrls*)
1.486 + | eq_rule _ = false;
1.487 +
1.488 +fun merge_rls _ Erls rls = rls
1.489 + | merge_rls _ rls Erls = rls
1.490 + | merge_rls id
1.491 + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.492 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.493 + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.494 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.495 + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.496 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.497 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.498 + ((#srls o rep_rls) r2),
1.499 + calc=ca1 @ ((#calc o rep_rls) r2),
1.500 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.501 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.502 + scr=sc1}:rls)
1.503 + | merge_rls id
1.504 + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.505 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.506 + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.507 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.508 + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.509 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.510 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.511 + ((#srls o rep_rls) r2),
1.512 + calc=ca1 @ ((#calc o rep_rls) r2),
1.513 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.514 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.515 + scr=sc1}:rls)
1.516 + | merge_rls _ _ _ =
1.517 + raise error "merge_rls: not for reverse-rewrite-rule-sets\
1.518 + \and not for mixed Rls -- Seq";
1.519 +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.520 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.521 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.522 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.523 + scr=sc}:rls)
1.524 + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.525 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.526 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.527 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.528 + scr=sc}:rls)
1.529 + | remove_rls id (Rrls _) _ = raise error
1.530 + ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.531 +
1.532 +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
1.533 +val it = [1, 2] : int list*)
1.534 +
1.535 +(*elder version: migrated 3 calls in smtest to memrls
1.536 +fun mem_rls id rls =
1.537 + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
1.538 + SOME _ => true | NONE => false;*)
1.539 +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.540 + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.541 + | memrls r _ = raise error ("memrls: incomplete impl. r= "^(rule2str r));
1.542 +fun rls_get_thm rls (id: xstring) =
1.543 + case find_first (curry eq_rule e_rule)
1.544 + ((#rules o rep_rls) rls) of
1.545 + SOME thm => SOME thm | NONE => NONE;
1.546 +
1.547 +fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known")
1.548 + | assoc' ((keyi, xi) :: pairs, key) =
1.549 + if key = keyi then SOME xi else assoc' (pairs, key);
1.550 +
1.551 +fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
1.552 + handle _ => raise error ("ME_Isa: thy '"^thy^"' not in system");
1.553 +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
1.554 + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
1.555 + overlays by re-using an identifier in different thys.*)
1.556 +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
1.557 + handle _ => raise error ("ME_Isa: '"^rls^"' not in system");
1.558 +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
1.559 + handle _ => raise error ("ME_Isa: '"^rls^"' not in system");*)
1.560 +
1.561 +(*.overwrite an element in an association list and pair it with a thyID
1.562 + in order to create the thy_hierarchy;
1.563 + overwrites existing rls' even if they are defined in a different thy;
1.564 + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
1.565 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.566 + they do NOT handle overlays by re-using an identifier in different thys;
1.567 + "thyID.rlsID" would be a good solution, if the "." would be possible
1.568 + in scripts...
1.569 + actually a hack to get alltogether run again with minimal effort*)
1.570 +fun insthy thy' (rls', rls) = (rls', (thy', rls));
1.571 +fun overwritelthy thy (al, bl:(rls' * rls) list) =
1.572 + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
1.573 + in overwritel (al, bl') end;
1.574 +
1.575 +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
1.576 + handle _ => raise error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.577 +(*get the string for stac from rule*)
1.578 +fun assoc_calc ([], key) = raise error ("assoc_calc: '"^ key ^"' not found")
1.579 + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
1.580 + if key = keyi then calc else assoc_calc (pairs, key);
1.581 +(*only used for !calclist'...*)
1.582 +fun assoc1 ([], key) = raise error ("assoc1 (for met.calc=): '"^ key
1.583 + ^"' not found")
1.584 + | assoc1 ((all as (keyi, _)) :: pairs, key) =
1.585 + if key = keyi then all else assoc1 (pairs, key);
1.586 +
1.587 +(*TODO.WN080102 clarify usage of type cal and type calc..*)
1.588 +fun calID2calcID (calID : calID) =
1.589 + let fun ass [] = raise error ("calID2calcID: "^calID^"not in calclist'")
1.590 + | ass ((calci, (cali, eval_fn))::ids) =
1.591 + if calID = cali then calci
1.592 + else ass ids
1.593 + in ass (!calclist') : calcID end;
1.594 +
1.595 +(*fun termopt2str (SOME t) =
1.596 + "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
1.597 + | termopt2str NONE = "NONE";*)
1.598 +fun termopt2str (SOME t) =
1.599 + "SOME " ^ (Syntax.string_of_term (ctxt_Isac"") t)
1.600 + | termopt2str NONE = "NONE";
1.601 +fun term2str t = Syntax.string_of_term (ctxt_Isac"") t;
1.602 +fun terms2str ts= (strs2str o (map (Syntax.string_of_term
1.603 + (ctxt_Isac"")))) ts;
1.604 +(*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
1.605 +fun type2str typ = Syntax.string_of_typ (ctxt_Isac"") typ;
1.606 +val string_of_typ = type2str;
1.607 +
1.608 +fun subst2str (s:subst) =
1.609 + (strs2str o
1.610 + (map (linefeed o pair2str o
1.611 + (apsnd term2str) o
1.612 + (apfst term2str)))) s;
1.613 +fun subst2str' (s:subst) =
1.614 + (strs2str' o
1.615 + (map (pair2str o
1.616 + (apsnd term2str) o
1.617 + (apfst term2str)))) s;
1.618 +(*> subst2str' [(str2term "bdv", str2term "x"),
1.619 + (str2term "bdv_2", str2term "y")];
1.620 +val it = "[(bdv, x)]" : string
1.621 +*)
1.622 +val env2str = subst2str;
1.623 +
1.624 +
1.625 +(*recursive defs:*)
1.626 +fun scr2str (Script s) = "Script "^(term2str s)
1.627 + | scr2str (Rfuns _) = "Rfuns";
1.628 +
1.629 +
1.630 +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
1.631 +
1.632 +
1.633 +(*.trace internal steps of isac's rewriter*)
1.634 +val trace_rewrite = ref false;
1.635 +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
1.636 +val depth = ref 99999;
1.637 +(*.no of rewrites exceeding this int -> NO rewrite.*)
1.638 +(*WN060829 still unused...*)
1.639 +val lim_rewrite = ref 99999;
1.640 +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
1.641 +val lim_deriv = ref 100;
1.642 +(*.switch for checking guhs unique before storing a pbl or met;
1.643 + set true at startup (done at begin of ROOT.ML)
1.644 + set false for editing IsacKnowledge (done at end of ROOT.ML).*)
1.645 +val check_guhs_unique = ref false;
1.646 +
1.647 +
1.648 +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
1.649 + L (*go left at $*)
1.650 + | R (*go right at $*)
1.651 + | D; (*go down at Abs*)
1.652 +type loc_ = lrd list;
1.653 +fun ldr2str L = "L"
1.654 + | ldr2str R = "R"
1.655 + | ldr2str D = "D";
1.656 +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
1.657 +