1.1 --- a/src/Tools/isac/calcelems.sml Tue Jan 11 15:28:03 2011 +0100
1.2 +++ b/src/Tools/isac/calcelems.sml Mon Feb 21 19:40:36 2011 +0100
1.3 @@ -20,15 +20,15 @@
1.4 type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
1.5 type thm'' = thmID * term;
1.6 type rls' = string;
1.7 -(*.a 'guh'='globally unique handle' is a string unique for each element
1.8 +(*.a 'guh'='globally unique handle' is a string unique for each element
1.9 of isac's KEStore and persistent over time
1.10 (in particular under shifts within the respective hierarchy);
1.11 - specialty for thys:
1.12 + specialty for thys:
1.13 # guh NOT resistant agains shifts from one thy to another
1.14 (which is the price for Isabelle's design: thy's overwrite ids of subthy's)
1.15 # requirement for matchTheory: induce guh from tac + current thy
1.16 (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
1.17 - TODO: introduce to pbl, met.*)
1.18 + TODO: introduce to pbl, met.*)
1.19 type guh = string;
1.20 val e_guh = "e_guh":guh;
1.21
1.22 @@ -59,20 +59,20 @@
1.23 val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
1.24
1.25
1.26 -datatype rule =
1.27 +datatype rule =
1.28 Erule (*.the empty rule .*)
1.29 -| Thm of (string * thm)(*.a theorem, ie (identifier, Thm.thm).*)
1.30 +| Thm of (string * Basic_Thm.thm)(*.a theorem, ie (identifier, Thm.thm).*)
1.31 | Calc of string * (*.sml-code manipulating a (sub)term .*)
1.32 (string -> term -> theory -> (string * term) option)
1.33 | Cal1 of string * (*.sml-code applied only to whole term
1.34 or left/right-hand-side of eqality .*)
1.35 (string -> term -> theory -> (string * term) option)
1.36 | Rls_ of rls (*.ie. rule sets may be nested.*)
1.37 -and scr =
1.38 - EmptyScr
1.39 +and scr =
1.40 + EmptyScr
1.41 | Script of term (*for met*)
1.42 - | Rfuns of {init_state : term ->
1.43 - (term * (*the current formula:
1.44 + | Rfuns of {init_state : term ->
1.45 + (term * (*the current formula:
1.46 goes locate_gen -> next_tac via istate*)
1.47 term * (*the final formula*)
1.48 rule list (*of reverse rewrite set (#1#)*)
1.49 @@ -81,18 +81,19 @@
1.50 (term * (*... rewrite with ...*)
1.51 term list)) (*... assumptions*)
1.52 list), (*derivation from given term to normalform
1.53 - in reverse order with sym_thm;
1.54 + in reverse order with sym_thm;
1.55 (#1#) could be extracted from here #1*)
1.56
1.57 normal_form: term -> (term * term list) option,
1.58 - locate_rule: rule list list -> term -> rule
1.59 + locate_rule: rule list list -> term -> rule
1.60 -> (rule * (term * term list)) list,
1.61 next_rule : rule list list -> term -> rule option,
1.62 - attach_form: rule list list -> term -> term
1.63 + attach_form: rule list list -> term -> term
1.64 -> (rule * (term * term list)) list}
1.65 +
1.66 and rls =
1.67 Erls (*for init e_rls*)
1.68 -
1.69 +
1.70 | Rls of (*a confluent and terminating ruleset, in general *)
1.71 {id : string, (*for trace_rewrite:=true *)
1.72 preconds : term list, (*unused WN020820 *)
1.73 @@ -112,16 +113,16 @@
1.74 rew_ord : rew_ord, (*for rules *)
1.75 erls : rls, (*for the conditions in rules *)
1.76 srls : rls, (*for evaluation of list_fns in script *)
1.77 - calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.78 + calc : calc list, (*for Calculate in scr, set by prep_rls *)
1.79 rules : rule list,
1.80 scr : scr} (*Script term (how to restrict type ???)*)
1.81 (*Rrls call SML-code and simulate an rls
1.82 difference: there is always _ONE_ redex rewritten in 1 call,
1.83 thus wrap Rrls by: Rls (Rls_ ...)*)
1.84 -
1.85 +
1.86 | Rrls of (* for 'reverse rewriting' by SML-functions instead Script *)
1.87 {id : string, (* for trace_rewrite := true *)
1.88 - prepat : (term list *(* preconds, eval with subst from pattern;
1.89 + prepat : (term list *(* preconds, eval with subst from pattern;
1.90 if [HOLogic.true_const], match decides alone *)
1.91 term ) (* pattern matched with current (sub)term *)
1.92 list, (* meta-conjunction is or *)
1.93 @@ -132,18 +133,17 @@
1.94 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
1.95 from rls, and then contain both Script _AND_ Rfuns !!!*)
1.96
1.97 -fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*)
1.98 +fun thy2ctxt' thy' = ProofContext.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
1.99 fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*)
1.100
1.101 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
1.102 -(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
1.103 +(*val ctxt_HOL = ProofContext.init_global (Thy_Info.get_theory "Complex_Main");*)
1.104 (*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
1.105 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
1.106 (*fun ctxt_Isac _ = thy2ctxt' "Isac";*)
1.107 fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
1.108
1.109 -val e_rule =
1.110 - Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
1.111 +val e_rule = Thm ("refl", @{thm refl});
1.112 fun id_of_thm (Thm (id, _)) = id
1.113 | id_of_thm _ = error "id_of_thm";
1.114 fun thm_of_thm (Thm (_, thm)) = thm
1.115 @@ -164,8 +164,8 @@
1.116 (*check for [.] as caused by "fun assoc_thm'"*)
1.117 fun string_of_thmI thm =
1.118 let val ct' = (de_quote o string_of_thm) thm
1.119 - val (a, b) = split_nlast (5, explode ct')
1.120 - in case b of
1.121 + val (a, b) = split_nlast (5, Symbol.explode ct')
1.122 + in case b of
1.123 [" ", " ","[", ".", "]"] => implode a
1.124 | _ => ct'
1.125 end;
1.126 @@ -204,7 +204,7 @@
1.127
1.128
1.129 type rrlsstate = (*state for reverse rewriting*)
1.130 - (term * (*the current formula:
1.131 + (term * (*the current formula:
1.132 goes locate_gen -> next_tac via istate*)
1.133 term * (*the final formula*)
1.134 rule list (*of reverse rewrite set (#1#)*)
1.135 @@ -213,7 +213,7 @@
1.136 (term * (*... rewrite with ...*)
1.137 term list)) (*... assumptions*)
1.138 list); (*derivation from given term to normalform
1.139 - in reverse order with sym_thm;
1.140 + in reverse order with sym_thm;
1.141 (#1#) could be extracted from here #1*)
1.142 val e_type = Type("empty",[]);
1.143 val a_type = TFree("'a",[]);
1.144 @@ -246,14 +246,14 @@
1.145 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
1.146 val theory2theory' = string_of_thy;
1.147 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
1.148 -val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;
1.149 -(*> theory2str' (theory "Isac");
1.150 +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
1.151 +(*> theory2str' (Thy_Info.get_theory "Isac");
1.152 al it = "Isac" : string
1.153 *)
1.154
1.155 fun thyID2theory' (thyID:thyID) = thyID;
1.156 (*
1.157 - let val ss = explode thyID
1.158 + let val ss = Symbol.explode thyID
1.159 val ext = implode (takelast (4, ss))
1.160 in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
1.161 else thyID ^ ".thy"
1.162 @@ -267,7 +267,7 @@
1.163
1.164 fun theory'2thyID (theory':theory') = theory';
1.165 (*
1.166 - let val ss = explode theory'
1.167 + let val ss = Symbol.explode theory'
1.168 val ext = implode (takelast (4, ss))
1.169 in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
1.170 else theory' (*disarm abuse of theory'*)
1.171 @@ -287,25 +287,25 @@
1.172
1.173 eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
1.174 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
1.175 - because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
1.176 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
1.177 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
1.178 (see match_ags).
1.179
1.180 Preliminary solution:
1.181 # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
1.182 # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
1.183 - # however, a thy specified by the user in the rootpbl may lead to
1.184 - errors in far-off subpbls (which are not yet reported properly !!!)
1.185 + # however, a thy specified by the user in the rootpbl may lead to
1.186 + errors in far-off subpbls (which are not yet reported properly !!!)
1.187 and interactively specifiying thys in subpbl is not very relevant.
1.188
1.189 Other solutions possible:
1.190 - # always parse and type-check with theory "Isac"
1.191 + # always parse and type-check with Thy_Info.get_theory "Isac"
1.192 (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.193 # regard the subthy-relation in specifying thys of subpbls
1.194 # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.195 # ???
1.196 .*)
1.197 -(*WN0509 TODO "ProtoPure" ... would be more consistent
1.198 +(*WN0509 TODO "ProtoPure" ... would be more consistent
1.199 with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
1.200 val e_domID = "e_domID":domID;
1.201
1.202 @@ -336,18 +336,18 @@
1.203 (*for distinction of contexts*)
1.204 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
1.205 fun ketype2str Exp_ = "Exp_"
1.206 - | ketype2str Thy_ = "Thy_"
1.207 - | ketype2str Pbl_ = "Pbl_"
1.208 + | ketype2str Thy_ = "Thy_"
1.209 + | ketype2str Pbl_ = "Pbl_"
1.210 | ketype2str Met_ = "Met_";
1.211 fun ketype2str' Exp_ = "Example"
1.212 - | ketype2str' Thy_ = "Theory"
1.213 - | ketype2str' Pbl_ = "Problem"
1.214 + | ketype2str' Thy_ = "Theory"
1.215 + | ketype2str' Pbl_ = "Problem"
1.216 | ketype2str' Met_ = "Method";
1.217
1.218 (*see 'How to manage theorys in subproblems' at 'type thyID'*)
1.219 val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
1.220
1.221 -(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
1.222 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
1.223 in order to distinguish them from general IsacKnowledge defined later on.*)
1.224 val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
1.225
1.226 @@ -379,7 +379,7 @@
1.227
1.228 (*.'a is for pbt | met.*)
1.229 (*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
1.230 -datatype 'a ptyp =
1.231 +datatype 'a ptyp =
1.232 Ptyp of string * (*element within pblID*)
1.233 'a list * (*several pbts with different domIDs/thy
1.234 TODO: select by subthy (isaref.p.69)
1.235 @@ -416,7 +416,7 @@
1.236 type thehier = (thydata ptyp) list;
1.237 val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
1.238
1.239 -(* an association list, gets the value once in Isac.ML.
1.240 +(* an association list, gets the value once in Isac.ML.
1.241 stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
1.242 WN1-1-28 make this data arguments and del ref ?*)
1.243 val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
1.244 @@ -437,9 +437,9 @@
1.245 next_rule=ne,attach_form=fo};
1.246 end;
1.247
1.248 -val e_rls =
1.249 +val e_rls =
1.250 Rls{id = "e_rls",
1.251 - preconds = [],
1.252 + preconds = [],
1.253 rew_ord = ("dummy_ord", dummy_ord),
1.254 erls = Erls,srls = Erls,
1.255 calc = [],
1.256 @@ -464,20 +464,20 @@
1.257 | rep_rls Erls = rep_rls e_rls
1.258 | rep_rls (Rrls {id,...}) = rep_rls e_rls
1.259 (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.260 -(*| rep_rls (Seq {id,...}) =
1.261 +(*| rep_rls (Seq {id,...}) =
1.262 error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.263 --1.7.03*)
1.264 -fun rep_rrls
1.265 - (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.266 +fun rep_rrls
1.267 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.268 scr=Rfuns
1.269 {attach_form,init_state,locate_rule,
1.270 next_rule,normal_form}}) =
1.271 - {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
1.272 - rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.273 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
1.274 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.275 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.276 - | rep_rrls (Rls {id,...}) =
1.277 + | rep_rrls (Rls {id,...}) =
1.278 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.279 - | rep_rrls (Seq {id,...}) =
1.280 + | rep_rrls (Seq {id,...}) =
1.281 error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.282
1.283 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.284 @@ -488,7 +488,7 @@
1.285 rules =rs,scr=sc}) r =
1.286 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.287 rules = rs @ r,scr=sc}:rls)
1.288 - | append_rls id (Rrls _) _ =
1.289 + | append_rls id (Rrls _) _ =
1.290 error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.291
1.292 (*. are _atomic_ rules equal ?.*)
1.293 @@ -503,12 +503,12 @@
1.294 | merge_rls _ rls Erls = rls
1.295 | merge_rls id
1.296 (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.297 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.298 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.299 (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.300 (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.301 (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.302 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.303 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.304 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.305 ((#srls o rep_rls) r2),
1.306 calc=ca1 @ ((#calc o rep_rls) r2),
1.307 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.308 @@ -516,18 +516,18 @@
1.309 scr=sc1}:rls)
1.310 | merge_rls id
1.311 (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.312 - (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.313 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.314 (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.315 (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.316 (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.317 rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.318 - srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.319 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.320 ((#srls o rep_rls) r2),
1.321 calc=ca1 @ ((#calc o rep_rls) r2),
1.322 (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.323 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.324 scr=sc1}:rls)
1.325 - | merge_rls _ _ _ =
1.326 + | merge_rls _ _ _ =
1.327 error "merge_rls: not for reverse-rewrite-rule-sets\
1.328 \and not for mixed Rls -- Seq";
1.329 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.330 @@ -540,21 +540,21 @@
1.331 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.332 (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.333 scr=sc}:rls)
1.334 - | remove_rls id (Rrls _) _ = error
1.335 + | remove_rls id (Rrls _) _ = error
1.336 ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.337
1.338 (*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
1.339 val it = [1, 2] : int list*)
1.340
1.341 (*elder version: migrated 3 calls in smtest to memrls
1.342 -fun mem_rls id rls =
1.343 +fun mem_rls id rls =
1.344 case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
1.345 SOME _ => true | NONE => false;*)
1.346 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.347 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.348 | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
1.349 fun rls_get_thm rls (id: xstring) =
1.350 - case find_first (curry eq_rule e_rule)
1.351 + case find_first (curry eq_rule e_rule)
1.352 ((#rules o rep_rls) rls) of
1.353 SOME thm => SOME thm | NONE => NONE;
1.354
1.355 @@ -565,10 +565,10 @@
1.356 (*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
1.357 handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
1.358 fun assoc_thy (thy:theory') =
1.359 - if thy = "e_domID" then (theory "Script") (*lower bound of Knowledge*)
1.360 - else (theory thy)
1.361 + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
1.362 + else (Thy_Info.get_theory thy)
1.363 handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.364 -
1.365 +
1.366 (*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
1.367 these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
1.368 overlays by re-using an identifier in different thys.*)
1.369 @@ -581,7 +581,7 @@
1.370 in order to create the thy_hierarchy;
1.371 overwrites existing rls' even if they are defined in a different thy;
1.372 this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
1.373 -(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.374 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.375 they do NOT handle overlays by re-using an identifier in different thys;
1.376 "thyID.rlsID" would be a good solution, if the "." would be possible
1.377 in scripts...
1.378 @@ -598,13 +598,13 @@
1.379 | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
1.380 if key = keyi then calc else assoc_calc (pairs, key);
1.381 (*only used for !calclist'...*)
1.382 -fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
1.383 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
1.384 ^"' not found")
1.385 | assoc1 ((all as (keyi, _)) :: pairs, key) =
1.386 if key = keyi then all else assoc1 (pairs, key);
1.387
1.388 (*TODO.WN080102 clarify usage of type cal and type calc..*)
1.389 -fun calID2calcID (calID : calID) =
1.390 +fun calID2calcID (calID : calID) =
1.391 let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
1.392 | ass ((calci, (cali, eval_fn))::ids) =
1.393 if calID = cali then calci
1.394 @@ -624,19 +624,19 @@
1.395 fun termopt2str (SOME t) = "SOME " ^ term2str t
1.396 | termopt2str NONE = "NONE";
1.397
1.398 -fun type2str typ =
1.399 +fun type2str typ =
1.400 Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
1.401 val string_of_typ = type2str;
1.402
1.403 -fun subst2str (s:subst) =
1.404 - (strs2str o
1.405 +fun subst2str (s:subst) =
1.406 + (strs2str o
1.407 (map (linefeed o pair2str o
1.408 - (apsnd term2str) o
1.409 + (apsnd term2str) o
1.410 (apfst term2str)))) s;
1.411 -fun subst2str' (s:subst) =
1.412 - (strs2str' o
1.413 +fun subst2str' (s:subst) =
1.414 + (strs2str' o
1.415 (map (pair2str o
1.416 - (apsnd term2str) o
1.417 + (apsnd term2str) o
1.418 (apfst term2str)))) s;
1.419 (*> subst2str' [(str2term "bdv", str2term "x"),
1.420 (str2term "bdv_2", str2term "y")];
1.421 @@ -669,7 +669,7 @@
1.422
1.423
1.424 datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
1.425 - L (*go left at $*)
1.426 + L (*go left at $*)
1.427 | R (*go right at $*)
1.428 | D; (*go down at Abs*)
1.429 type loc_ = lrd list;
1.430 @@ -681,3 +681,1089 @@
1.431 (*
1.432 end (*struct*)
1.433 *)
1.434 +
1.435 +
1.436 +
1.437 +val e_rule =
1.438 + Thm ("refl", @{thm refl});
1.439 +fun id_of_thm (Thm (id, _)) = id
1.440 + | id_of_thm _ = error "id_of_thm";
1.441 +fun thm_of_thm (Thm (_, thm)) = thm
1.442 + | thm_of_thm _ = error "thm_of_thm";
1.443 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
1.444 +
1.445 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
1.446 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
1.447 +
1.448 +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
1.449 + (strip_thy thmid1) = (strip_thy thmid2);
1.450 +(*version typed weaker WN100910*)
1.451 +fun eq_thmI' ((thmid1, _), (thmid2, _)) =
1.452 + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
1.453 +
1.454 +
1.455 +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
1.456 +(*check for [.] as caused by "fun assoc_thm'"*)
1.457 +fun string_of_thmI thm =
1.458 + let val ct' = (de_quote o string_of_thm) thm
1.459 + val (a, b) = split_nlast (5, Symbol.explode ct')
1.460 + in case b of
1.461 + [" ", " ","[", ".", "]"] => implode a
1.462 + | _ => ct'
1.463 + end;
1.464 +
1.465 +(*.id requested for all, Rls,Seq,Rrls.*)
1.466 +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
1.467 + | id_rls (Rls {id,...}) = id
1.468 + | id_rls (Seq {id,...}) = id
1.469 + | id_rls (Rrls {id,...}) = id;
1.470 +val rls2str = id_rls;
1.471 +fun id_rule (Thm (id, _)) = id
1.472 + | id_rule (Calc (id, _)) = id
1.473 + | id_rule (Rls_ rls) = id_rls rls;
1.474 +
1.475 +fun get_rules (Rls {rules,...}) = rules
1.476 + | get_rules (Seq {rules,...}) = rules
1.477 + | get_rules (Rrls _) = [];
1.478 +
1.479 +fun rule2str Erule = "Erule"
1.480 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
1.481 + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.482 + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.483 + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.484 +fun rule2str' Erule = "Erule"
1.485 + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
1.486 + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.487 + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.488 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.489 +
1.490 +(*WN080102 compare eq_rule ?!?*)
1.491 +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
1.492 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.493 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
1.494 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
1.495 + | eqrule _ = false;
1.496 +
1.497 +
1.498 +type rrlsstate = (*state for reverse rewriting*)
1.499 + (term * (*the current formula:
1.500 + goes locate_gen -> next_tac via istate*)
1.501 + term * (*the final formula*)
1.502 + rule list (*of reverse rewrite set (#1#)*)
1.503 + list * (*may be serveral, eg. in norm_rational*)
1.504 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
1.505 + (term * (*... rewrite with ...*)
1.506 + term list)) (*... assumptions*)
1.507 + list); (*derivation from given term to normalform
1.508 + in reverse order with sym_thm;
1.509 + (#1#) could be extracted from here #1*)
1.510 +val e_type = Type("empty",[]);
1.511 +val a_type = TFree("'a",[]);
1.512 +val e_term = Const("empty",e_type);
1.513 +val a_term = Free("empty",a_type);
1.514 +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
1.515 +
1.516 +
1.517 +
1.518 +
1.519 +(*22.2.02: ging auf Linux nicht (Stefan)
1.520 +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
1.521 +val e_term = Const("empty", Type("'a", []));
1.522 +val e_scr = Script e_term;
1.523 +
1.524 +
1.525 +(*ad thm':
1.526 + there are two kinds of theorems ...
1.527 + (1) known by isabelle
1.528 + (2) not known, eg. calc_thm, instantiated rls
1.529 + the latter have a thmid "#..."
1.530 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
1.531 + and have a special assoc_thm / assoc_rls in this interface *)
1.532 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
1.533 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
1.534 +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.535 +
1.536 +fun string_of_thy thy = Context.theory_name thy: theory';
1.537 +val theory2domID = string_of_thy;
1.538 +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
1.539 +val theory2theory' = string_of_thy;
1.540 +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
1.541 +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
1.542 +(*> theory2str' (Thy_Info.get_theory "Isac");
1.543 +al it = "Isac" : string
1.544 +*)
1.545 +
1.546 +fun thyID2theory' (thyID:thyID) = thyID;
1.547 +(*
1.548 + let val ss = Symbol.explode thyID
1.549 + val ext = implode (takelast (4, ss))
1.550 + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
1.551 + else thyID ^ ".thy"
1.552 + end;
1.553 +*)
1.554 +(* thyID2theory' "Isac" (*ok*);
1.555 +val it = "Isac" : theory'
1.556 + > thyID2theory' "Isac" (*abuse, goes ok...*);
1.557 +val it = "Isac" : theory'
1.558 +*)
1.559 +
1.560 +fun theory'2thyID (theory':theory') = theory';
1.561 +(*
1.562 + let val ss = Symbol.explode theory'
1.563 + val ext = implode (takelast (4, ss))
1.564 + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
1.565 + else theory' (*disarm abuse of theory'*)
1.566 + end;
1.567 +*)
1.568 +(* theory'2thyID "Isac";
1.569 +val it = "Isac" : thyID
1.570 +> theory'2thyID "Isac";
1.571 +val it = "Isac" : thyID*)
1.572 +
1.573 +
1.574 +(*. WN0509 discussion:
1.575 +#############################################################################
1.576 +# How to manage theorys in subproblems wrt. the requirement, #
1.577 +# that scripts should be re-usable ? #
1.578 +#############################################################################
1.579 +
1.580 + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
1.581 + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
1.582 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
1.583 + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
1.584 + (see match_ags).
1.585 +
1.586 + Preliminary solution:
1.587 + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
1.588 + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
1.589 + # however, a thy specified by the user in the rootpbl may lead to
1.590 + errors in far-off subpbls (which are not yet reported properly !!!)
1.591 + and interactively specifiying thys in subpbl is not very relevant.
1.592 +
1.593 + Other solutions possible:
1.594 + # always parse and type-check with Thy_Info.get_theory "Isac"
1.595 + (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.596 + # regard the subthy-relation in specifying thys of subpbls
1.597 + # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.598 + # ???
1.599 +.*)
1.600 +(*WN0509 TODO "ProtoPure" ... would be more consistent
1.601 + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
1.602 +val e_domID = "e_domID":domID;
1.603 +
1.604 +(*the key into the hierarchy ob theory elements*)
1.605 +type theID = string list;
1.606 +val e_theID = ["e_theID"];
1.607 +val theID2str = strs2str;
1.608 +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
1.609 +fun theID2thyID (theID:theID) =
1.610 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
1.611 + else error ("theID2thyID called with "^ theID2str theID);
1.612 +
1.613 +(*the key into the hierarchy ob problems*)
1.614 +type pblID = string list; (* domID::...*)
1.615 +val e_pblID = ["e_pblID"]:pblID;
1.616 +val pblID2str = strs2str;
1.617 +
1.618 +(*the key into the hierarchy ob methods*)
1.619 +type metID = string list;
1.620 +val e_metID = ["e_metID"]:metID;
1.621 +val metID2str = strs2str;
1.622 +
1.623 +(*either theID or pblID or metID*)
1.624 +type kestoreID = string list;
1.625 +val e_kestoreID = ["e_kestoreID"];
1.626 +val kestoreID2str = strs2str;
1.627 +
1.628 +(*for distinction of contexts*)
1.629 +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
1.630 +fun ketype2str Exp_ = "Exp_"
1.631 + | ketype2str Thy_ = "Thy_"
1.632 + | ketype2str Pbl_ = "Pbl_"
1.633 + | ketype2str Met_ = "Met_";
1.634 +fun ketype2str' Exp_ = "Example"
1.635 + | ketype2str' Thy_ = "Theory"
1.636 + | ketype2str' Pbl_ = "Problem"
1.637 + | ketype2str' Met_ = "Method";
1.638 +
1.639 +(*see 'How to manage theorys in subproblems' at 'type thyID'*)
1.640 +val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
1.641 +
1.642 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
1.643 + in order to distinguish them from general IsacKnowledge defined later on.*)
1.644 +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
1.645 +
1.646 +
1.647 +(*rewrite orders, also stored in 'type met' and type 'and rls'
1.648 + The association list is required for 'rewrite.."rew_ord"..'
1.649 + WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
1.650 +val rew_ord' =
1.651 + Unsynchronized.ref
1.652 + ([]:(rew_ord' * (*the key for the association list *)
1.653 + (subst (*the bound variables - they get high order*)
1.654 + -> (term * term) (*(t1, t2) to be compared *)
1.655 + -> bool)) (*if t1 <= t2 then true else false *)
1.656 + list); (*association list *)
1.657 +
1.658 +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
1.659 + ("dummy_ord", dummy_ord)]);
1.660 +
1.661 +
1.662 +(*WN060120 a hack to get alltogether run again with minimal effort:
1.663 + theory' is inserted for creating thy_hierarchy; calls for assoc_rls
1.664 + need not be called*)
1.665 +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
1.666 +
1.667 +(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
1.668 +val calclist'= Unsynchronized.ref ([]: calc list);
1.669 +
1.670 +(*.the hierarchy of thydata.*)
1.671 +
1.672 +(*.'a is for pbt | met.*)
1.673 +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
1.674 +datatype 'a ptyp =
1.675 + Ptyp of string * (*element within pblID*)
1.676 + 'a list * (*several pbts with different domIDs/thy
1.677 + TODO: select by subthy (isaref.p.69)
1.678 + presently only _ONE_ elem*)
1.679 + ('a ptyp) list; (*the children nodes*)
1.680 +
1.681 +(*.datatype for collecting thydata for hierarchy.*)
1.682 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
1.683 +(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
1.684 +datatype thydata = Html of {guh: guh,
1.685 + coursedesign: authors,
1.686 + mathauthors: authors,
1.687 + html: string} (*html; for demos before database*)
1.688 + | Hthm of {guh: guh,
1.689 + coursedesign: authors,
1.690 + mathauthors: authors,
1.691 + thm: term}
1.692 + | Hrls of {guh: guh,
1.693 + coursedesign: authors,
1.694 + mathauthors: authors,
1.695 + (*like vvvvvvvvvvvvv val ruleset'
1.696 + WN060711 redesign together !*)
1.697 + thy_rls: (thyID * rls)}
1.698 + | Hcal of {guh: guh,
1.699 + coursedesign: authors,
1.700 + mathauthors: authors,
1.701 + calc: calc}
1.702 + | Hord of {guh: guh,
1.703 + coursedesign: authors,
1.704 + mathauthors: authors,
1.705 + ord: (subst -> (term * term) -> bool)};
1.706 +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
1.707 +
1.708 +type thehier = (thydata ptyp) list;
1.709 +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
1.710 +
1.711 +(* an association list, gets the value once in Isac.ML.
1.712 + stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
1.713 + WN1-1-28 make this data arguments and del ref ?*)
1.714 +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
1.715 +
1.716 +
1.717 +type path = string;
1.718 +type filename = string;
1.719 +
1.720 +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
1.721 +local
1.722 + fun ii (_:term) = e_rrlsstate;
1.723 + fun no (_:term) = SOME (e_term,[e_term]);
1.724 + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
1.725 + fun ne (_:rule list list) (_:term) = SOME e_rule;
1.726 + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
1.727 +in
1.728 +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
1.729 + next_rule=ne,attach_form=fo};
1.730 +end;
1.731 +
1.732 +val e_rls =
1.733 + Rls{id = "e_rls",
1.734 + preconds = [],
1.735 + rew_ord = ("dummy_ord", dummy_ord),
1.736 + erls = Erls,srls = Erls,
1.737 + calc = [],
1.738 + rules = [], scr = EmptyScr}:rls;
1.739 +val e_rrls = Rrls {id = "e_rrls",
1.740 + prepat = [],
1.741 + rew_ord = ("dummy_ord", dummy_ord),
1.742 + erls = Erls,
1.743 + calc = [],
1.744 + (*asm_thm=[],*)
1.745 + scr=e_rfuns}:rls;
1.746 +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
1.747 + ("e_rrls",("Tools",e_rrls))
1.748 + ]);
1.749 +
1.750 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.751 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.752 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.753 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.754 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.755 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.756 + | rep_rls Erls = rep_rls e_rls
1.757 + | rep_rls (Rrls {id,...}) = rep_rls e_rls
1.758 + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.759 +(*| rep_rls (Seq {id,...}) =
1.760 + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.761 +--1.7.03*)
1.762 +fun rep_rrls
1.763 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.764 + scr=Rfuns
1.765 + {attach_form,init_state,locate_rule,
1.766 + next_rule,normal_form}}) =
1.767 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
1.768 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.769 + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.770 + | rep_rrls (Rls {id,...}) =
1.771 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.772 + | rep_rrls (Seq {id,...}) =
1.773 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.774 +
1.775 +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.776 + rules =rs,scr=sc}) r =
1.777 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.778 + rules = rs @ r,scr=sc}:rls)
1.779 + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.780 + rules =rs,scr=sc}) r =
1.781 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.782 + rules = rs @ r,scr=sc}:rls)
1.783 + | append_rls id (Rrls _) _ =
1.784 + error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.785 +
1.786 +(*. are _atomic_ rules equal ?.*)
1.787 +(*WN080102 compare eqrule ?!?*)
1.788 +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
1.789 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.790 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
1.791 + (*id_rls checks for Rls, Seq, Rrls*)
1.792 + | eq_rule _ = false;
1.793 +
1.794 +fun merge_rls _ Erls rls = rls
1.795 + | merge_rls _ rls Erls = rls
1.796 + | merge_rls id
1.797 + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.798 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.799 + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.800 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.801 + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.802 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.803 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.804 + ((#srls o rep_rls) r2),
1.805 + calc=ca1 @ ((#calc o rep_rls) r2),
1.806 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.807 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.808 + scr=sc1}:rls)
1.809 + | merge_rls id
1.810 + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.811 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.812 + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.813 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.814 + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.815 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.816 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.817 + ((#srls o rep_rls) r2),
1.818 + calc=ca1 @ ((#calc o rep_rls) r2),
1.819 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.820 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.821 + scr=sc1}:rls)
1.822 + | merge_rls _ _ _ =
1.823 + error "merge_rls: not for reverse-rewrite-rule-sets\
1.824 + \and not for mixed Rls -- Seq";
1.825 +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.826 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.827 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.828 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.829 + scr=sc}:rls)
1.830 + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.831 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.832 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.833 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.834 + scr=sc}:rls)
1.835 + | remove_rls id (Rrls _) _ = error
1.836 + ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.837 +
1.838 +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
1.839 +val it = [1, 2] : int list*)
1.840 +
1.841 +(*elder version: migrated 3 calls in smtest to memrls
1.842 +fun mem_rls id rls =
1.843 + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
1.844 + SOME _ => true | NONE => false;*)
1.845 +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.846 + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.847 + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
1.848 +fun rls_get_thm rls (id: xstring) =
1.849 + case find_first (curry eq_rule e_rule)
1.850 + ((#rules o rep_rls) rls) of
1.851 + SOME thm => SOME thm | NONE => NONE;
1.852 +
1.853 +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
1.854 + | assoc' ((keyi, xi) :: pairs, key) =
1.855 + if key = keyi then SOME xi else assoc' (pairs, key);
1.856 +
1.857 +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
1.858 + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
1.859 +fun assoc_thy (thy:theory') =
1.860 + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
1.861 + else (Thy_Info.get_theory thy)
1.862 + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.863 +
1.864 +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
1.865 + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
1.866 + overlays by re-using an identifier in different thys.*)
1.867 +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
1.868 + handle _ => error ("ME_Isa: '"^rls^"' not in system");
1.869 +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
1.870 + handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
1.871 +
1.872 +(*.overwrite an element in an association list and pair it with a thyID
1.873 + in order to create the thy_hierarchy;
1.874 + overwrites existing rls' even if they are defined in a different thy;
1.875 + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
1.876 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.877 + they do NOT handle overlays by re-using an identifier in different thys;
1.878 + "thyID.rlsID" would be a good solution, if the "." would be possible
1.879 + in scripts...
1.880 + actually a hack to get alltogether run again with minimal effort*)
1.881 +fun insthy thy' (rls', rls) = (rls', (thy', rls));
1.882 +fun overwritelthy thy (al, bl:(rls' * rls) list) =
1.883 + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
1.884 + in overwritel (al, bl') end;
1.885 +
1.886 +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
1.887 + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.888 +(*get the string for stac from rule*)
1.889 +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
1.890 + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
1.891 + if key = keyi then calc else assoc_calc (pairs, key);
1.892 +(*only used for !calclist'...*)
1.893 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
1.894 + ^"' not found")
1.895 + | assoc1 ((all as (keyi, _)) :: pairs, key) =
1.896 + if key = keyi then all else assoc1 (pairs, key);
1.897 +
1.898 +(*TODO.WN080102 clarify usage of type cal and type calc..*)
1.899 +fun calID2calcID (calID : calID) =
1.900 + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
1.901 + | ass ((calci, (cali, eval_fn))::ids) =
1.902 + if calID = cali then calci
1.903 + else ass ids
1.904 + in ass (!calclist') : calcID end;
1.905 +
1.906 +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
1.907 +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
1.908 +
1.909 +fun terms2str ts = (strs2str o (map term2str )) ts;
1.910 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
1.911 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
1.912 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
1.913 +fun terms2strs ts = (map term2str) ts;
1.914 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
1.915 +
1.916 +fun termopt2str (SOME t) = "SOME " ^ term2str t
1.917 + | termopt2str NONE = "NONE";
1.918 +
1.919 +fun type2str typ =
1.920 + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
1.921 +val string_of_typ = type2str;
1.922 +
1.923 +fun subst2str (s:subst) =
1.924 + (strs2str o
1.925 + (map (linefeed o pair2str o
1.926 + (apsnd term2str) o
1.927 + (apfst term2str)))) s;
1.928 +fun subst2str' (s:subst) =
1.929 + (strs2str' o
1.930 + (map (pair2str o
1.931 + (apsnd term2str) o
1.932 + (apfst term2str)))) s;
1.933 +(*> subst2str' [(str2term "bdv", str2term "x"),
1.934 + (str2term "bdv_2", str2term "y")];
1.935 +val it = "[(bdv, x)]" : string
1.936 +*)
1.937 +val env2str = subst2str;
1.938 +
1.939 +
1.940 +(*recursive defs:*)
1.941 +fun scr2str (Script s) = "Script "^(term2str s)
1.942 + | scr2str (Rfuns _) = "Rfuns";
1.943 +
1.944 +
1.945 +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
1.946 +
1.947 +
1.948 +(*.trace internal steps of isac's rewriter*)
1.949 +val trace_rewrite = Unsynchronized.ref false;
1.950 +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
1.951 +val depth = Unsynchronized.ref 99999;
1.952 +(*.no of rewrites exceeding this int -> NO rewrite.*)
1.953 +(*WN060829 still unused...*)
1.954 +val lim_rewrite = Unsynchronized.ref 99999;
1.955 +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
1.956 +val lim_deriv = Unsynchronized.ref 100;
1.957 +(*.switch for checking guhs unique before storing a pbl or met;
1.958 + set true at startup (done at begin of ROOT.ML)
1.959 + set false for editing IsacKnowledge (done at end of ROOT.ML).*)
1.960 +val check_guhs_unique = Unsynchronized.ref false;
1.961 +
1.962 +
1.963 +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
1.964 + L (*go left at $*)
1.965 + | R (*go right at $*)
1.966 + | D; (*go down at Abs*)
1.967 +type loc_ = lrd list;
1.968 +fun ldr2str L = "L"
1.969 + | ldr2str R = "R"
1.970 + | ldr2str D = "D";
1.971 +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
1.972 +
1.973 +(*
1.974 +end (*struct*)
1.975 +*)
1.976 +
1.977 +
1.978 +val e_rule =
1.979 + Thm ("refl", @{thm refl});
1.980 +fun id_of_thm (Thm (id, _)) = id
1.981 + | id_of_thm _ = error "id_of_thm";
1.982 +fun thm_of_thm (Thm (_, thm)) = thm
1.983 + | thm_of_thm _ = error "thm_of_thm";
1.984 +fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
1.985 +
1.986 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
1.987 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
1.988 +
1.989 +fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
1.990 + (strip_thy thmid1) = (strip_thy thmid2);
1.991 +(*version typed weaker WN100910*)
1.992 +fun eq_thmI' ((thmid1, _), (thmid2, _)) =
1.993 + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
1.994 +
1.995 +
1.996 +val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
1.997 +(*check for [.] as caused by "fun assoc_thm'"*)
1.998 +fun string_of_thmI thm =
1.999 + let val ct' = (de_quote o string_of_thm) thm
1.1000 + val (a, b) = split_nlast (5, Symbol.explode ct')
1.1001 + in case b of
1.1002 + [" ", " ","[", ".", "]"] => implode a
1.1003 + | _ => ct'
1.1004 + end;
1.1005 +
1.1006 +(*.id requested for all, Rls,Seq,Rrls.*)
1.1007 +fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
1.1008 + | id_rls (Rls {id,...}) = id
1.1009 + | id_rls (Seq {id,...}) = id
1.1010 + | id_rls (Rrls {id,...}) = id;
1.1011 +val rls2str = id_rls;
1.1012 +fun id_rule (Thm (id, _)) = id
1.1013 + | id_rule (Calc (id, _)) = id
1.1014 + | id_rule (Rls_ rls) = id_rls rls;
1.1015 +
1.1016 +fun get_rules (Rls {rules,...}) = rules
1.1017 + | get_rules (Seq {rules,...}) = rules
1.1018 + | get_rules (Rrls _) = [];
1.1019 +
1.1020 +fun rule2str Erule = "Erule"
1.1021 + | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
1.1022 + | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.1023 + | rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.1024 + | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.1025 +fun rule2str' Erule = "Erule"
1.1026 + | rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
1.1027 + | rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
1.1028 + | rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
1.1029 + | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
1.1030 +
1.1031 +(*WN080102 compare eq_rule ?!?*)
1.1032 +fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
1.1033 + | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.1034 + | eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
1.1035 + | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
1.1036 + | eqrule _ = false;
1.1037 +
1.1038 +
1.1039 +type rrlsstate = (*state for reverse rewriting*)
1.1040 + (term * (*the current formula:
1.1041 + goes locate_gen -> next_tac via istate*)
1.1042 + term * (*the final formula*)
1.1043 + rule list (*of reverse rewrite set (#1#)*)
1.1044 + list * (*may be serveral, eg. in norm_rational*)
1.1045 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
1.1046 + (term * (*... rewrite with ...*)
1.1047 + term list)) (*... assumptions*)
1.1048 + list); (*derivation from given term to normalform
1.1049 + in reverse order with sym_thm;
1.1050 + (#1#) could be extracted from here #1*)
1.1051 +val e_type = Type("empty",[]);
1.1052 +val a_type = TFree("'a",[]);
1.1053 +val e_term = Const("empty",e_type);
1.1054 +val a_term = Free("empty",a_type);
1.1055 +val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
1.1056 +
1.1057 +
1.1058 +
1.1059 +
1.1060 +(*22.2.02: ging auf Linux nicht (Stefan)
1.1061 +val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
1.1062 +val e_term = Const("empty", Type("'a", []));
1.1063 +val e_scr = Script e_term;
1.1064 +
1.1065 +
1.1066 +(*ad thm':
1.1067 + there are two kinds of theorems ...
1.1068 + (1) known by isabelle
1.1069 + (2) not known, eg. calc_thm, instantiated rls
1.1070 + the latter have a thmid "#..."
1.1071 + and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
1.1072 + and have a special assoc_thm / assoc_rls in this interface *)
1.1073 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
1.1074 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
1.1075 +type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
1.1076 +
1.1077 +fun string_of_thy thy = Context.theory_name thy: theory';
1.1078 +val theory2domID = string_of_thy;
1.1079 +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
1.1080 +val theory2theory' = string_of_thy;
1.1081 +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
1.1082 +val theory2str' = implode o (drop_last_n 4) o Symbol.explode o string_of_thy;
1.1083 +(*> theory2str' (Thy_Info.get_theory "Isac");
1.1084 +al it = "Isac" : string
1.1085 +*)
1.1086 +
1.1087 +fun thyID2theory' (thyID:thyID) = thyID;
1.1088 +(*
1.1089 + let val ss = Symbol.explode thyID
1.1090 + val ext = implode (takelast (4, ss))
1.1091 + in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
1.1092 + else thyID ^ ".thy"
1.1093 + end;
1.1094 +*)
1.1095 +(* thyID2theory' "Isac" (*ok*);
1.1096 +val it = "Isac" : theory'
1.1097 + > thyID2theory' "Isac" (*abuse, goes ok...*);
1.1098 +val it = "Isac" : theory'
1.1099 +*)
1.1100 +
1.1101 +fun theory'2thyID (theory':theory') = theory';
1.1102 +(*
1.1103 + let val ss = Symbol.explode theory'
1.1104 + val ext = implode (takelast (4, ss))
1.1105 + in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
1.1106 + else theory' (*disarm abuse of theory'*)
1.1107 + end;
1.1108 +*)
1.1109 +(* theory'2thyID "Isac";
1.1110 +val it = "Isac" : thyID
1.1111 +> theory'2thyID "Isac";
1.1112 +val it = "Isac" : thyID*)
1.1113 +
1.1114 +
1.1115 +(*. WN0509 discussion:
1.1116 +#############################################################################
1.1117 +# How to manage theorys in subproblems wrt. the requirement, #
1.1118 +# that scripts should be re-usable ? #
1.1119 +#############################################################################
1.1120 +
1.1121 + eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
1.1122 + which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
1.1123 + because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
1.1124 + is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
1.1125 + (see match_ags).
1.1126 +
1.1127 + Preliminary solution:
1.1128 + # the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
1.1129 + # instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
1.1130 + # however, a thy specified by the user in the rootpbl may lead to
1.1131 + errors in far-off subpbls (which are not yet reported properly !!!)
1.1132 + and interactively specifiying thys in subpbl is not very relevant.
1.1133 +
1.1134 + Other solutions possible:
1.1135 + # always parse and type-check with Thy_Info.get_theory "Isac"
1.1136 + (rejected tue to the vague idea eg. to re-use equations for R in C etc.)
1.1137 + # regard the subthy-relation in specifying thys of subpbls
1.1138 + # specifically handle 'SubProblem (undefined, pbl, arglist)'
1.1139 + # ???
1.1140 +.*)
1.1141 +(*WN0509 TODO "ProtoPure" ... would be more consistent
1.1142 + with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
1.1143 +val e_domID = "e_domID":domID;
1.1144 +
1.1145 +(*the key into the hierarchy ob theory elements*)
1.1146 +type theID = string list;
1.1147 +val e_theID = ["e_theID"];
1.1148 +val theID2str = strs2str;
1.1149 +(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
1.1150 +fun theID2thyID (theID:theID) =
1.1151 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
1.1152 + else error ("theID2thyID called with "^ theID2str theID);
1.1153 +
1.1154 +(*the key into the hierarchy ob problems*)
1.1155 +type pblID = string list; (* domID::...*)
1.1156 +val e_pblID = ["e_pblID"]:pblID;
1.1157 +val pblID2str = strs2str;
1.1158 +
1.1159 +(*the key into the hierarchy ob methods*)
1.1160 +type metID = string list;
1.1161 +val e_metID = ["e_metID"]:metID;
1.1162 +val metID2str = strs2str;
1.1163 +
1.1164 +(*either theID or pblID or metID*)
1.1165 +type kestoreID = string list;
1.1166 +val e_kestoreID = ["e_kestoreID"];
1.1167 +val kestoreID2str = strs2str;
1.1168 +
1.1169 +(*for distinction of contexts*)
1.1170 +datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
1.1171 +fun ketype2str Exp_ = "Exp_"
1.1172 + | ketype2str Thy_ = "Thy_"
1.1173 + | ketype2str Pbl_ = "Pbl_"
1.1174 + | ketype2str Met_ = "Met_";
1.1175 +fun ketype2str' Exp_ = "Example"
1.1176 + | ketype2str' Thy_ = "Theory"
1.1177 + | ketype2str' Pbl_ = "Problem"
1.1178 + | ketype2str' Met_ = "Method";
1.1179 +
1.1180 +(*see 'How to manage theorys in subproblems' at 'type thyID'*)
1.1181 +val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
1.1182 +
1.1183 +(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
1.1184 + in order to distinguish them from general IsacKnowledge defined later on.*)
1.1185 +val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
1.1186 +
1.1187 +
1.1188 +(*rewrite orders, also stored in 'type met' and type 'and rls'
1.1189 + The association list is required for 'rewrite.."rew_ord"..'
1.1190 + WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
1.1191 +val rew_ord' =
1.1192 + Unsynchronized.ref
1.1193 + ([]:(rew_ord' * (*the key for the association list *)
1.1194 + (subst (*the bound variables - they get high order*)
1.1195 + -> (term * term) (*(t1, t2) to be compared *)
1.1196 + -> bool)) (*if t1 <= t2 then true else false *)
1.1197 + list); (*association list *)
1.1198 +
1.1199 +rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
1.1200 + ("dummy_ord", dummy_ord)]);
1.1201 +
1.1202 +
1.1203 +(*WN060120 a hack to get alltogether run again with minimal effort:
1.1204 + theory' is inserted for creating thy_hierarchy; calls for assoc_rls
1.1205 + need not be called*)
1.1206 +val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
1.1207 +
1.1208 +(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
1.1209 +val calclist'= Unsynchronized.ref ([]: calc list);
1.1210 +
1.1211 +(*.the hierarchy of thydata.*)
1.1212 +
1.1213 +(*.'a is for pbt | met.*)
1.1214 +(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
1.1215 +datatype 'a ptyp =
1.1216 + Ptyp of string * (*element within pblID*)
1.1217 + 'a list * (*several pbts with different domIDs/thy
1.1218 + TODO: select by subthy (isaref.p.69)
1.1219 + presently only _ONE_ elem*)
1.1220 + ('a ptyp) list; (*the children nodes*)
1.1221 +
1.1222 +(*.datatype for collecting thydata for hierarchy.*)
1.1223 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
1.1224 +(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
1.1225 +datatype thydata = Html of {guh: guh,
1.1226 + coursedesign: authors,
1.1227 + mathauthors: authors,
1.1228 + html: string} (*html; for demos before database*)
1.1229 + | Hthm of {guh: guh,
1.1230 + coursedesign: authors,
1.1231 + mathauthors: authors,
1.1232 + thm: term}
1.1233 + | Hrls of {guh: guh,
1.1234 + coursedesign: authors,
1.1235 + mathauthors: authors,
1.1236 + (*like vvvvvvvvvvvvv val ruleset'
1.1237 + WN060711 redesign together !*)
1.1238 + thy_rls: (thyID * rls)}
1.1239 + | Hcal of {guh: guh,
1.1240 + coursedesign: authors,
1.1241 + mathauthors: authors,
1.1242 + calc: calc}
1.1243 + | Hord of {guh: guh,
1.1244 + coursedesign: authors,
1.1245 + mathauthors: authors,
1.1246 + ord: (subst -> (term * term) -> bool)};
1.1247 +val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
1.1248 +
1.1249 +type thehier = (thydata ptyp) list;
1.1250 +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
1.1251 +
1.1252 +(* an association list, gets the value once in Isac.ML.
1.1253 + stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
1.1254 + WN1-1-28 make this data arguments and del ref ?*)
1.1255 +val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
1.1256 +
1.1257 +
1.1258 +type path = string;
1.1259 +type filename = string;
1.1260 +
1.1261 +(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
1.1262 +local
1.1263 + fun ii (_:term) = e_rrlsstate;
1.1264 + fun no (_:term) = SOME (e_term,[e_term]);
1.1265 + fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
1.1266 + fun ne (_:rule list list) (_:term) = SOME e_rule;
1.1267 + fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
1.1268 +in
1.1269 +val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
1.1270 + next_rule=ne,attach_form=fo};
1.1271 +end;
1.1272 +
1.1273 +val e_rls =
1.1274 + Rls{id = "e_rls",
1.1275 + preconds = [],
1.1276 + rew_ord = ("dummy_ord", dummy_ord),
1.1277 + erls = Erls,srls = Erls,
1.1278 + calc = [],
1.1279 + rules = [], scr = EmptyScr}:rls;
1.1280 +val e_rrls = Rrls {id = "e_rrls",
1.1281 + prepat = [],
1.1282 + rew_ord = ("dummy_ord", dummy_ord),
1.1283 + erls = Erls,
1.1284 + calc = [],
1.1285 + (*asm_thm=[],*)
1.1286 + scr=e_rfuns}:rls;
1.1287 +ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
1.1288 + ("e_rrls",("Tools",e_rrls))
1.1289 + ]);
1.1290 +
1.1291 +fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.1292 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.1293 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.1294 + | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
1.1295 + {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
1.1296 + (*asm_thm=asm_thm,*)rules=rules,scr=scr}
1.1297 + | rep_rls Erls = rep_rls e_rls
1.1298 + | rep_rls (Rrls {id,...}) = rep_rls e_rls
1.1299 + (*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
1.1300 +(*| rep_rls (Seq {id,...}) =
1.1301 + error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
1.1302 +--1.7.03*)
1.1303 +fun rep_rrls
1.1304 + (Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
1.1305 + scr=Rfuns
1.1306 + {attach_form,init_state,locate_rule,
1.1307 + next_rule,normal_form}}) =
1.1308 + {id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
1.1309 + rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
1.1310 + locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
1.1311 + | rep_rrls (Rls {id,...}) =
1.1312 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
1.1313 + | rep_rrls (Seq {id,...}) =
1.1314 + error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
1.1315 +
1.1316 +fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1317 + rules =rs,scr=sc}) r =
1.1318 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1319 + rules = rs @ r,scr=sc}:rls)
1.1320 + | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1321 + rules =rs,scr=sc}) r =
1.1322 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1323 + rules = rs @ r,scr=sc}:rls)
1.1324 + | append_rls id (Rrls _) _ =
1.1325 + error ("append_rls: not for reverse-rewrite-rule-set "^id);
1.1326 +
1.1327 +(*. are _atomic_ rules equal ?.*)
1.1328 +(*WN080102 compare eqrule ?!?*)
1.1329 +fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
1.1330 + | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
1.1331 + | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
1.1332 + (*id_rls checks for Rls, Seq, Rrls*)
1.1333 + | eq_rule _ = false;
1.1334 +
1.1335 +fun merge_rls _ Erls rls = rls
1.1336 + | merge_rls _ rls Erls = rls
1.1337 + | merge_rls id
1.1338 + (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.1339 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.1340 + (r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.1341 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.1342 + (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.1343 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.1344 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.1345 + ((#srls o rep_rls) r2),
1.1346 + calc=ca1 @ ((#calc o rep_rls) r2),
1.1347 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.1348 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.1349 + scr=sc1}:rls)
1.1350 + | merge_rls id
1.1351 + (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
1.1352 + (*asm_thm=at1,*)rules =rs1,scr=sc1})
1.1353 + (r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
1.1354 + (*asm_thm=at2,*)rules =rs2,scr=sc2}) =
1.1355 + (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
1.1356 + rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
1.1357 + srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
1.1358 + ((#srls o rep_rls) r2),
1.1359 + calc=ca1 @ ((#calc o rep_rls) r2),
1.1360 + (*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
1.1361 + rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
1.1362 + scr=sc1}:rls)
1.1363 + | merge_rls _ _ _ =
1.1364 + error "merge_rls: not for reverse-rewrite-rule-sets\
1.1365 + \and not for mixed Rls -- Seq";
1.1366 +fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1367 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.1368 + (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1369 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.1370 + scr=sc}:rls)
1.1371 + | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1372 + (*asm_thm=at,*)rules =rs,scr=sc}) r =
1.1373 + (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
1.1374 + (*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
1.1375 + scr=sc}:rls)
1.1376 + | remove_rls id (Rrls _) _ = error
1.1377 + ("remove_rls: not for reverse-rewrite-rule-set "^id);
1.1378 +
1.1379 +(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
1.1380 +val it = [1, 2] : int list*)
1.1381 +
1.1382 +(*elder version: migrated 3 calls in smtest to memrls
1.1383 +fun mem_rls id rls =
1.1384 + case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
1.1385 + SOME _ => true | NONE => false;*)
1.1386 +fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
1.1387 + | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
1.1388 + | memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
1.1389 +fun rls_get_thm rls (id: xstring) =
1.1390 + case find_first (curry eq_rule e_rule)
1.1391 + ((#rules o rep_rls) rls) of
1.1392 + SOME thm => SOME thm | NONE => NONE;
1.1393 +
1.1394 +fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
1.1395 + | assoc' ((keyi, xi) :: pairs, key) =
1.1396 + if key = keyi then SOME xi else assoc' (pairs, key);
1.1397 +
1.1398 +(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
1.1399 + handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
1.1400 +fun assoc_thy (thy:theory') =
1.1401 + if thy = "e_domID" then (Thy_Info.get_theory "Script") (*lower bound of Knowledge*)
1.1402 + else (Thy_Info.get_theory thy)
1.1403 + handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
1.1404 +
1.1405 +(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
1.1406 + these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
1.1407 + overlays by re-using an identifier in different thys.*)
1.1408 +fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
1.1409 + handle _ => error ("ME_Isa: '"^rls^"' not in system");
1.1410 +(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
1.1411 + handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
1.1412 +
1.1413 +(*.overwrite an element in an association list and pair it with a thyID
1.1414 + in order to create the thy_hierarchy;
1.1415 + overwrites existing rls' even if they are defined in a different thy;
1.1416 + this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
1.1417 +(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
1.1418 + they do NOT handle overlays by re-using an identifier in different thys;
1.1419 + "thyID.rlsID" would be a good solution, if the "." would be possible
1.1420 + in scripts...
1.1421 + actually a hack to get alltogether run again with minimal effort*)
1.1422 +fun insthy thy' (rls', rls) = (rls', (thy', rls));
1.1423 +fun overwritelthy thy (al, bl:(rls' * rls) list) =
1.1424 + let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
1.1425 + in overwritel (al, bl') end;
1.1426 +
1.1427 +fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
1.1428 + handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
1.1429 +(*get the string for stac from rule*)
1.1430 +fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
1.1431 + | assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
1.1432 + if key = keyi then calc else assoc_calc (pairs, key);
1.1433 +(*only used for !calclist'...*)
1.1434 +fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
1.1435 + ^"' not found")
1.1436 + | assoc1 ((all as (keyi, _)) :: pairs, key) =
1.1437 + if key = keyi then all else assoc1 (pairs, key);
1.1438 +
1.1439 +(*TODO.WN080102 clarify usage of type cal and type calc..*)
1.1440 +fun calID2calcID (calID : calID) =
1.1441 + let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
1.1442 + | ass ((calci, (cali, eval_fn))::ids) =
1.1443 + if calID = cali then calci
1.1444 + else ass ids
1.1445 + in ass (!calclist') : calcID end;
1.1446 +
1.1447 +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
1.1448 +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
1.1449 +
1.1450 +fun terms2str ts = (strs2str o (map term2str )) ts;
1.1451 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
1.1452 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
1.1453 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
1.1454 +fun terms2strs ts = (map term2str) ts;
1.1455 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
1.1456 +
1.1457 +fun termopt2str (SOME t) = "SOME " ^ term2str t
1.1458 + | termopt2str NONE = "NONE";
1.1459 +
1.1460 +fun type2str typ =
1.1461 + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
1.1462 +val string_of_typ = type2str;
1.1463 +
1.1464 +fun subst2str (s:subst) =
1.1465 + (strs2str o
1.1466 + (map (linefeed o pair2str o
1.1467 + (apsnd term2str) o
1.1468 + (apfst term2str)))) s;
1.1469 +fun subst2str' (s:subst) =
1.1470 + (strs2str' o
1.1471 + (map (pair2str o
1.1472 + (apsnd term2str) o
1.1473 + (apfst term2str)))) s;
1.1474 +(*> subst2str' [(str2term "bdv", str2term "x"),
1.1475 + (str2term "bdv_2", str2term "y")];
1.1476 +val it = "[(bdv, x)]" : string
1.1477 +*)
1.1478 +val env2str = subst2str;
1.1479 +
1.1480 +
1.1481 +(*recursive defs:*)
1.1482 +fun scr2str (Script s) = "Script "^(term2str s)
1.1483 + | scr2str (Rfuns _) = "Rfuns";
1.1484 +
1.1485 +
1.1486 +fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
1.1487 +
1.1488 +
1.1489 +(*.trace internal steps of isac's rewriter*)
1.1490 +val trace_rewrite = Unsynchronized.ref false;
1.1491 +(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
1.1492 +val depth = Unsynchronized.ref 99999;
1.1493 +(*.no of rewrites exceeding this int -> NO rewrite.*)
1.1494 +(*WN060829 still unused...*)
1.1495 +val lim_rewrite = Unsynchronized.ref 99999;
1.1496 +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
1.1497 +val lim_deriv = Unsynchronized.ref 100;
1.1498 +(*.switch for checking guhs unique before storing a pbl or met;
1.1499 + set true at startup (done at begin of ROOT.ML)
1.1500 + set false for editing IsacKnowledge (done at end of ROOT.ML).*)
1.1501 +val check_guhs_unique = Unsynchronized.ref false;
1.1502 +
1.1503 +
1.1504 +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
1.1505 + L (*go left at $*)
1.1506 + | R (*go right at $*)
1.1507 + | D; (*go down at Abs*)
1.1508 +type loc_ = lrd list;
1.1509 +fun ldr2str L = "L"
1.1510 + | ldr2str R = "R"
1.1511 + | ldr2str D = "D";
1.1512 +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
1.1513 +
1.1514 +(*
1.1515 +end (*struct*)
1.1516 +*)
1.1517 +
1.1518 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.1519 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)