neuper@37906
|
1 |
(* elements of calculations.
|
neuper@37906
|
2 |
they are partially held in association lists as ref's for
|
neuper@37906
|
3 |
switching language levels (meta-string, object-values).
|
neuper@37906
|
4 |
in order to keep these ref's during re-evaluation of code,
|
neuper@37906
|
5 |
they are defined here at the beginning of the code.
|
neuper@37906
|
6 |
author: Walther Neuper
|
neuper@37906
|
7 |
(c) isac-team 2003
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
use"calcelems.sml";
|
neuper@37906
|
10 |
*)
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
val linefeed = (curry op^) "\n";
|
neuper@37906
|
13 |
type authors = string list;
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
type cterm' = string;
|
neuper@37906
|
16 |
val empty_cterm' = "empty_cterm'";
|
neuper@37906
|
17 |
type thmID = string;
|
neuper@37906
|
18 |
type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
|
neuper@37906
|
19 |
type thm'' = thmID * term;
|
neuper@37906
|
20 |
type rls' = string;
|
neuper@37906
|
21 |
(*.a 'guh'='globally unique handle' is a string unique for each element
|
neuper@37906
|
22 |
of isac's KEStore and persistent over time
|
neuper@37906
|
23 |
(in particular under shifts within the respective hierarchy);
|
neuper@37906
|
24 |
specialty for thys:
|
neuper@37906
|
25 |
# guh NOT resistant agains shifts from one thy to another
|
neuper@37906
|
26 |
(which is the price for Isabelle's design: thy's overwrite ids of subthy's)
|
neuper@37906
|
27 |
# requirement for matchTheory: induce guh from tac + current thy
|
neuper@37906
|
28 |
(see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
|
neuper@37906
|
29 |
TODO: introduce to pbl, met.*)
|
neuper@37906
|
30 |
type guh = string;
|
neuper@37906
|
31 |
val e_guh = "e_guh":guh;
|
neuper@37906
|
32 |
|
neuper@37906
|
33 |
type xml = string;
|
neuper@37906
|
34 |
|
neuper@37906
|
35 |
(*. eval function calling sml code during rewriting.*)
|
neuper@37906
|
36 |
type eval_fn = (string -> term -> theory -> (string * term) option);
|
neuper@37906
|
37 |
fun e_evalfn (_:'a) (_:term) (_:theory) = NONE:(string * term) option;
|
neuper@37906
|
38 |
(*. op in isa-term 'Const(op,_)' .*)
|
neuper@37906
|
39 |
type calID = string;
|
neuper@37906
|
40 |
type cal = (calID * eval_fn);
|
neuper@37906
|
41 |
(*. fun calculate_ fetches the evaluation-function via this list. *)
|
neuper@37906
|
42 |
type calcID = string;
|
neuper@37906
|
43 |
type calc = (calcID * cal);
|
neuper@37906
|
44 |
|
neuper@37906
|
45 |
type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)
|
neuper@37906
|
46 |
type subst = (term * term) list; (*here for ets2str*)
|
neuper@37906
|
47 |
val e_subst = []:(term * term) list;
|
neuper@37906
|
48 |
|
neuper@37906
|
49 |
(*TODO.WN060610 make use of "type rew_ord" total*)
|
neuper@37906
|
50 |
type rew_ord' = string;
|
neuper@37906
|
51 |
val e_rew_ord' = "e_rew_ord" : rew_ord';
|
neuper@37906
|
52 |
type rew_ord_ = subst -> Term.term * Term.term -> bool;
|
neuper@37906
|
53 |
fun dummy_ord (_:subst) (_:term,_:term) = true;
|
neuper@37906
|
54 |
val e_rew_ord_ = dummy_ord;
|
neuper@37906
|
55 |
type rew_ord = rew_ord' * rew_ord_;
|
neuper@37906
|
56 |
val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
|
neuper@37906
|
57 |
val e_rew_ordX = (e_rew_ord', e_rew_ord_) : rew_ord;
|
neuper@37906
|
58 |
|
neuper@37906
|
59 |
|
neuper@37906
|
60 |
datatype rule =
|
neuper@37906
|
61 |
Erule (*.the empty rule .*)
|
neuper@37906
|
62 |
| Thm of (string * thm)(*.a theorem, ie (identifier, Thm.thm).*)
|
neuper@37906
|
63 |
| Calc of string * (*.sml-code manipulating a (sub)term .*)
|
neuper@37906
|
64 |
(string -> term -> theory -> (string * term) option)
|
neuper@37906
|
65 |
| Cal1 of string * (*.sml-code applied only to whole term
|
neuper@37906
|
66 |
or left/right-hand-side of eqality .*)
|
neuper@37906
|
67 |
(string -> term -> theory -> (string * term) option)
|
neuper@37906
|
68 |
| Rls_ of rls (*.ie. rule sets may be nested.*)
|
neuper@37906
|
69 |
and scr =
|
neuper@37906
|
70 |
EmptyScr
|
neuper@37906
|
71 |
| Script of term (*for met*)
|
neuper@37906
|
72 |
| Rfuns of {init_state : term ->
|
neuper@37906
|
73 |
(term * (*the current formula:
|
neuper@37906
|
74 |
goes locate_gen -> next_tac via istate*)
|
neuper@37906
|
75 |
term * (*the final formula*)
|
neuper@37906
|
76 |
rule list (*of reverse rewrite set (#1#)*)
|
neuper@37906
|
77 |
list * (*may be serveral, eg. in norm_rational*)
|
neuper@37906
|
78 |
(rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
|
neuper@37906
|
79 |
(term * (*... rewrite with ...*)
|
neuper@37906
|
80 |
term list)) (*... assumptions*)
|
neuper@37906
|
81 |
list), (*derivation from given term to normalform
|
neuper@37906
|
82 |
in reverse order with sym_thm;
|
neuper@37906
|
83 |
(#1#) could be extracted from here #1*)
|
neuper@37906
|
84 |
|
neuper@37906
|
85 |
normal_form: term -> (term * term list) option,
|
neuper@37906
|
86 |
locate_rule: rule list list -> term -> rule
|
neuper@37906
|
87 |
-> (rule * (term * term list)) list,
|
neuper@37906
|
88 |
next_rule : rule list list -> term -> rule option,
|
neuper@37906
|
89 |
attach_form: rule list list -> term -> term
|
neuper@37906
|
90 |
-> (rule * (term * term list)) list}
|
neuper@37906
|
91 |
and rls =
|
neuper@37906
|
92 |
Erls (*for init e_rls*)
|
neuper@37906
|
93 |
|
neuper@37906
|
94 |
| Rls of (*a confluent and terminating ruleset, in general *)
|
neuper@37906
|
95 |
{id : string, (*for trace_rewrite:=true *)
|
neuper@37906
|
96 |
preconds : term list, (*unused WN020820 *)
|
neuper@37906
|
97 |
(*WN060616 for efficiency...
|
neuper@37906
|
98 |
bdvs : false, (*set in prep_rls for get_bdvs *)*)
|
neuper@37906
|
99 |
rew_ord : rew_ord, (*for rules*)
|
neuper@37906
|
100 |
erls : rls, (*for the conditions in rules *)
|
neuper@37906
|
101 |
srls : rls, (*for evaluation of list_fns in script *)
|
neuper@37906
|
102 |
calc : calc list, (*for Calculate in scr, set by prep_rls *)
|
neuper@37906
|
103 |
rules : rule list,
|
neuper@37906
|
104 |
scr : scr} (*Script term: generating intermed.steps *)
|
neuper@37906
|
105 |
| Seq of (*a sequence of rules to be tried only once *)
|
neuper@37906
|
106 |
{id : string, (*for trace_rewrite:=true *)
|
neuper@37906
|
107 |
preconds : term list, (*unused 20.8.02 *)
|
neuper@37906
|
108 |
(*WN060616 for efficiency...
|
neuper@37906
|
109 |
bdvs : false, (*set in prep_rls for get_bdvs *)*)
|
neuper@37906
|
110 |
rew_ord : rew_ord, (*for rules *)
|
neuper@37906
|
111 |
erls : rls, (*for the conditions in rules *)
|
neuper@37906
|
112 |
srls : rls, (*for evaluation of list_fns in script *)
|
neuper@37906
|
113 |
calc : calc list, (*for Calculate in scr, set by prep_rls *)
|
neuper@37906
|
114 |
rules : rule list,
|
neuper@37906
|
115 |
scr : scr} (*Script term (how to restrict type ???)*)
|
neuper@37906
|
116 |
(*Rrls call SML-code and simulate an rls
|
neuper@37906
|
117 |
difference: there is always _ONE_ redex rewritten in 1 call,
|
neuper@37906
|
118 |
thus wrap Rrls by: Rls (Rls_ ...)*)
|
neuper@37906
|
119 |
|
neuper@38036
|
120 |
| Rrls of (* for 'reverse rewriting' by SML-functions instead Script *)
|
neuper@38036
|
121 |
{id : string, (* for trace_rewrite := true *)
|
neuper@38036
|
122 |
prepat : (term list *(* preconds, eval with subst from pattern;
|
neuper@38036
|
123 |
if [HOLogic.true_const], match decides alone *)
|
neuper@38036
|
124 |
term ) (* pattern matched with current (sub)term *)
|
neuper@38036
|
125 |
list, (* meta-conjunction is or *)
|
neuper@38036
|
126 |
rew_ord : rew_ord, (* for rules *)
|
neuper@38036
|
127 |
erls : rls, (* for the conditions in rules and preconds *)
|
neuper@38036
|
128 |
calc : calc list, (* for Calculate in scr, set automatic.in prep_rls *)
|
neuper@38036
|
129 |
scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
|
neuper@37906
|
130 |
(*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
|
neuper@37906
|
131 |
from rls, and then contain both Script _AND_ Rfuns !!!*)
|
neuper@37906
|
132 |
|
neuper@37928
|
133 |
fun thy2ctxt' thy' = ProofContext.init_global (theory thy');(*FIXXXME thy-ctxt*)
|
neuper@37928
|
134 |
fun thy2ctxt thy = ProofContext.init_global thy;(*FIXXXME thy-ctxt*)
|
neuper@37906
|
135 |
|
neuper@37906
|
136 |
(*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
|
neuper@37924
|
137 |
(*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
|
neuper@37929
|
138 |
(*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
|
neuper@37906
|
139 |
(*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
|
neuper@37929
|
140 |
(*fun ctxt_Isac _ = thy2ctxt' "Isac";*)
|
neuper@37929
|
141 |
fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
|
neuper@37906
|
142 |
|
neuper@37929
|
143 |
val e_rule =
|
neuper@37929
|
144 |
Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
|
neuper@37906
|
145 |
fun id_of_thm (Thm (id, _)) = id
|
neuper@38031
|
146 |
| id_of_thm _ = error "id_of_thm";
|
neuper@37906
|
147 |
fun thm_of_thm (Thm (_, thm)) = thm
|
neuper@38031
|
148 |
| thm_of_thm _ = error "thm_of_thm";
|
neuper@37906
|
149 |
fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
|
neuper@37906
|
150 |
fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
|
neuper@37906
|
151 |
(strip_thy thmid1) = (strip_thy thmid2);
|
neuper@38002
|
152 |
(*version typed weaker WN100910*)
|
neuper@38002
|
153 |
fun eq_thmI' ((thmid1, _), (thmid2, _)) =
|
neuper@38002
|
154 |
(strip_thy thmid1) = (strip_thy thmid2);
|
neuper@37906
|
155 |
|
neuper@37906
|
156 |
|
neuper@37906
|
157 |
val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
|
neuper@37906
|
158 |
(*check for [.] as caused by "fun assoc_thm'"*)
|
neuper@37906
|
159 |
fun string_of_thmI thm =
|
neuper@37906
|
160 |
let val ct' = (de_quote o string_of_thm) thm
|
neuper@37906
|
161 |
val (a, b) = split_nlast (5, explode ct')
|
neuper@37906
|
162 |
in case b of
|
neuper@37906
|
163 |
[" ", " ","[", ".", "]"] => implode a
|
neuper@37906
|
164 |
| _ => ct'
|
neuper@37906
|
165 |
end;
|
neuper@37906
|
166 |
|
neuper@37906
|
167 |
(*.id requested for all, Rls,Seq,Rrls.*)
|
neuper@37906
|
168 |
fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
|
neuper@37906
|
169 |
| id_rls (Rls {id,...}) = id
|
neuper@37906
|
170 |
| id_rls (Seq {id,...}) = id
|
neuper@37906
|
171 |
| id_rls (Rrls {id,...}) = id;
|
neuper@37906
|
172 |
val rls2str = id_rls;
|
neuper@37906
|
173 |
fun id_rule (Thm (id, _)) = id
|
neuper@37906
|
174 |
| id_rule (Calc (id, _)) = id
|
neuper@37906
|
175 |
| id_rule (Rls_ rls) = id_rls rls;
|
neuper@37906
|
176 |
|
neuper@37906
|
177 |
fun get_rules (Rls {rules,...}) = rules
|
neuper@37906
|
178 |
| get_rules (Seq {rules,...}) = rules
|
neuper@37906
|
179 |
| get_rules (Rrls _) = [];
|
neuper@37906
|
180 |
|
neuper@37906
|
181 |
fun rule2str Erule = "Erule"
|
neuper@37906
|
182 |
| rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
|
neuper@37906
|
183 |
| rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)"
|
neuper@37906
|
184 |
| rule2str (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
|
neuper@37906
|
185 |
| rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
|
neuper@37906
|
186 |
fun rule2str' Erule = "Erule"
|
neuper@37906
|
187 |
| rule2str' (Thm (str, thm)) = "Thm (\""^str^"\",\"\")"
|
neuper@37906
|
188 |
| rule2str' (Calc (str,f)) = "Calc (\""^str^"\",fn)"
|
neuper@37906
|
189 |
| rule2str' (Cal1 (str,f)) = "Cal1 (\""^str^"\",fn)"
|
neuper@37906
|
190 |
| rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
|
neuper@37906
|
191 |
|
neuper@37906
|
192 |
(*WN080102 compare eq_rule ?!?*)
|
neuper@37906
|
193 |
fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2
|
neuper@37906
|
194 |
| eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2
|
neuper@37906
|
195 |
| eqrule (Cal1 (id1,_), Cal1 (id2,_)) = id1 = id2
|
neuper@37906
|
196 |
| eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
|
neuper@37906
|
197 |
| eqrule _ = false;
|
neuper@37906
|
198 |
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
type rrlsstate = (*state for reverse rewriting*)
|
neuper@37906
|
201 |
(term * (*the current formula:
|
neuper@37906
|
202 |
goes locate_gen -> next_tac via istate*)
|
neuper@37906
|
203 |
term * (*the final formula*)
|
neuper@37906
|
204 |
rule list (*of reverse rewrite set (#1#)*)
|
neuper@37906
|
205 |
list * (*may be serveral, eg. in norm_rational*)
|
neuper@37906
|
206 |
(rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
|
neuper@37906
|
207 |
(term * (*... rewrite with ...*)
|
neuper@37906
|
208 |
term list)) (*... assumptions*)
|
neuper@37906
|
209 |
list); (*derivation from given term to normalform
|
neuper@37906
|
210 |
in reverse order with sym_thm;
|
neuper@37906
|
211 |
(#1#) could be extracted from here #1*)
|
neuper@37906
|
212 |
val e_type = Type("empty",[]);
|
neuper@37906
|
213 |
val a_type = TFree("'a",[]);
|
neuper@37906
|
214 |
val e_term = Const("empty",e_type);
|
neuper@37906
|
215 |
val a_term = Free("empty",a_type);
|
neuper@37906
|
216 |
val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
|
neuper@37906
|
219 |
|
neuper@37906
|
220 |
|
neuper@37906
|
221 |
(*22.2.02: ging auf Linux nicht (Stefan)
|
neuper@37906
|
222 |
val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
|
neuper@37906
|
223 |
val e_term = Const("empty", Type("'a", []));
|
neuper@37906
|
224 |
val e_scr = Script e_term;
|
neuper@37906
|
225 |
|
neuper@37906
|
226 |
|
neuper@37906
|
227 |
(*ad thm':
|
neuper@37906
|
228 |
there are two kinds of theorems ...
|
neuper@37906
|
229 |
(1) known by isabelle
|
neuper@37906
|
230 |
(2) not known, eg. calc_thm, instantiated rls
|
neuper@37906
|
231 |
the latter have a thmid "#..."
|
neuper@37906
|
232 |
and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
|
neuper@37906
|
233 |
and have a special assoc_thm / assoc_rls in this interface *)
|
neuper@37906
|
234 |
type theory' = string; (* = domID ^".thy" *)
|
neuper@37906
|
235 |
type domID = string; (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
|
neuper@37906
|
236 |
type thyID = string; (*WN.3.11.03 TODO: replace domID with thyID*)
|
neuper@37906
|
237 |
|
neuper@37906
|
238 |
fun string_of_thy thy = Context.theory_name thy: theory';
|
neuper@37906
|
239 |
val theory2domID = string_of_thy;
|
neuper@37906
|
240 |
val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
|
neuper@37906
|
241 |
val theory2theory' = string_of_thy;
|
neuper@37906
|
242 |
val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
|
neuper@37906
|
243 |
val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;
|
neuper@37906
|
244 |
(*> theory2str' Isac.thy;
|
neuper@37906
|
245 |
al it = "Isac" : string
|
neuper@37906
|
246 |
*)
|
neuper@37906
|
247 |
|
neuper@37906
|
248 |
fun thyID2theory' (thyID:thyID) =
|
neuper@37906
|
249 |
let val ss = explode thyID
|
neuper@37906
|
250 |
val ext = implode (takelast (4, ss))
|
neuper@37906
|
251 |
in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)
|
neuper@37906
|
252 |
else thyID ^ ".thy"
|
neuper@37906
|
253 |
end;
|
neuper@37906
|
254 |
(* thyID2theory' "Isac" (*ok*);
|
neuper@37906
|
255 |
val it = "Isac.thy" : theory'
|
neuper@37906
|
256 |
> thyID2theory' "Isac.thy" (*abuse, goes ok...*);
|
neuper@37906
|
257 |
val it = "Isac.thy" : theory'
|
neuper@37906
|
258 |
*)
|
neuper@37906
|
259 |
|
neuper@37906
|
260 |
fun theory'2thyID (theory':theory') =
|
neuper@37906
|
261 |
let val ss = explode theory'
|
neuper@37906
|
262 |
val ext = implode (takelast (4, ss))
|
neuper@37906
|
263 |
in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID
|
neuper@37906
|
264 |
else theory' (*disarm abuse of theory'*)
|
neuper@37906
|
265 |
end;
|
neuper@37906
|
266 |
(* theory'2thyID "Isac.thy";
|
neuper@37906
|
267 |
val it = "Isac" : thyID
|
neuper@37906
|
268 |
> theory'2thyID "Isac";
|
neuper@37906
|
269 |
val it = "Isac" : thyID*)
|
neuper@37906
|
270 |
|
neuper@37906
|
271 |
|
neuper@37906
|
272 |
(*. WN0509 discussion:
|
neuper@37906
|
273 |
#############################################################################
|
neuper@37906
|
274 |
# How to manage theorys in subproblems wrt. the requirement, #
|
neuper@37906
|
275 |
# that scripts should be re-usable ? #
|
neuper@37906
|
276 |
#############################################################################
|
neuper@37906
|
277 |
|
neuper@37988
|
278 |
eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
|
neuper@37906
|
279 |
which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
|
neuper@37906
|
280 |
because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
|
neuper@37906
|
281 |
is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
|
neuper@37906
|
282 |
(see match_ags).
|
neuper@37906
|
283 |
|
neuper@37906
|
284 |
Preliminary solution:
|
neuper@38011
|
285 |
# the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
|
neuper@38011
|
286 |
# instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
|
neuper@37906
|
287 |
# however, a thy specified by the user in the rootpbl may lead to
|
neuper@37906
|
288 |
errors in far-off subpbls (which are not yet reported properly !!!)
|
neuper@37906
|
289 |
and interactively specifiying thys in subpbl is not very relevant.
|
neuper@37906
|
290 |
|
neuper@37906
|
291 |
Other solutions possible:
|
neuper@38011
|
292 |
# always parse and type-check with theory "Isac"
|
neuper@37906
|
293 |
(rejected tue to the vague idea eg. to re-use equations for R in C etc.)
|
neuper@37906
|
294 |
# regard the subthy-relation in specifying thys of subpbls
|
neuper@38011
|
295 |
# specifically handle 'SubProblem (undefined, pbl, arglist)'
|
neuper@37906
|
296 |
# ???
|
neuper@37906
|
297 |
.*)
|
neuper@37906
|
298 |
(*WN0509 TODO "ProtoPure" ... would be more consistent
|
neuper@37906
|
299 |
with assoc_thy <--> theory2theory' +FIXME assoc_thy "e_domID" -> Script.thy*)
|
neuper@37906
|
300 |
val e_domID = "e_domID":domID;
|
neuper@37906
|
301 |
|
neuper@37906
|
302 |
(*the key into the hierarchy ob theory elements*)
|
neuper@37906
|
303 |
type theID = string list;
|
neuper@37906
|
304 |
val e_theID = ["e_theID"];
|
neuper@37906
|
305 |
val theID2str = strs2str;
|
neuper@37906
|
306 |
(*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
|
neuper@37906
|
307 |
fun theID2thyID (theID:theID) =
|
neuper@37906
|
308 |
if length theID >= 3 then (last_elem o (drop_last_n 2)) theID : thyID
|
neuper@38031
|
309 |
else error ("theID2thyID called with "^ theID2str theID);
|
neuper@37906
|
310 |
|
neuper@37906
|
311 |
(*the key into the hierarchy ob problems*)
|
neuper@37906
|
312 |
type pblID = string list; (* domID::...*)
|
neuper@37906
|
313 |
val e_pblID = ["e_pblID"]:pblID;
|
neuper@37906
|
314 |
val pblID2str = strs2str;
|
neuper@37906
|
315 |
|
neuper@37906
|
316 |
(*the key into the hierarchy ob methods*)
|
neuper@37906
|
317 |
type metID = string list;
|
neuper@37906
|
318 |
val e_metID = ["e_metID"]:metID;
|
neuper@37906
|
319 |
val metID2str = strs2str;
|
neuper@37906
|
320 |
|
neuper@37906
|
321 |
(*either theID or pblID or metID*)
|
neuper@37906
|
322 |
type kestoreID = string list;
|
neuper@37906
|
323 |
val e_kestoreID = ["e_kestoreID"];
|
neuper@37906
|
324 |
val kestoreID2str = strs2str;
|
neuper@37906
|
325 |
|
neuper@37906
|
326 |
(*for distinction of contexts*)
|
neuper@37906
|
327 |
datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
|
neuper@37906
|
328 |
fun ketype2str Exp_ = "Exp_"
|
neuper@37906
|
329 |
| ketype2str Thy_ = "Thy_"
|
neuper@37906
|
330 |
| ketype2str Pbl_ = "Pbl_"
|
neuper@37906
|
331 |
| ketype2str Met_ = "Met_";
|
neuper@37906
|
332 |
fun ketype2str' Exp_ = "Example"
|
neuper@37906
|
333 |
| ketype2str' Thy_ = "Theory"
|
neuper@37906
|
334 |
| ketype2str' Pbl_ = "Problem"
|
neuper@37906
|
335 |
| ketype2str' Met_ = "Method";
|
neuper@37906
|
336 |
|
neuper@37906
|
337 |
(*see 'How to manage theorys in subproblems' at 'type thyID'*)
|
neuper@38006
|
338 |
val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
|
neuper@37906
|
339 |
|
neuper@37906
|
340 |
(*.all theories defined for Scripts, recorded in Scripts/Script.ML;
|
neuper@37906
|
341 |
in order to distinguish them from general IsacKnowledge defined later on.*)
|
neuper@38006
|
342 |
val script_thys = Unsynchronized.ref ([] : (theory' * theory) list);
|
neuper@37906
|
343 |
|
neuper@37906
|
344 |
|
neuper@37906
|
345 |
(*rewrite orders, also stored in 'type met' and type 'and rls'
|
neuper@37906
|
346 |
The association list is required for 'rewrite.."rew_ord"..'
|
neuper@37947
|
347 |
WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
|
neuper@38007
|
348 |
val rew_ord' =
|
neuper@38007
|
349 |
Unsynchronized.ref
|
neuper@38007
|
350 |
([]:(rew_ord' * (*the key for the association list *)
|
neuper@37906
|
351 |
(subst (*the bound variables - they get high order*)
|
neuper@37906
|
352 |
-> (term * term) (*(t1, t2) to be compared *)
|
neuper@37906
|
353 |
-> bool)) (*if t1 <= t2 then true else false *)
|
neuper@37906
|
354 |
list); (*association list *)
|
neuper@37906
|
355 |
rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
|
neuper@37906
|
356 |
("dummy_ord", dummy_ord)]);
|
neuper@37906
|
357 |
|
neuper@37906
|
358 |
|
neuper@37906
|
359 |
(*WN060120 a hack to get alltogether run again with minimal effort:
|
neuper@37906
|
360 |
theory' is inserted for creating thy_hierarchy; calls for assoc_rls
|
neuper@37906
|
361 |
need not be called*)
|
neuper@38006
|
362 |
val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
|
neuper@37906
|
363 |
|
neuper@37906
|
364 |
(*FIXME.040207 calclist': used by prep_rls, NOT in met*)
|
neuper@38006
|
365 |
val calclist'= Unsynchronized.ref ([]: calc list);
|
neuper@37906
|
366 |
|
neuper@37906
|
367 |
(*.the hierarchy of thydata.*)
|
neuper@37906
|
368 |
|
neuper@37906
|
369 |
(*.'a is for pbt | met.*)
|
neuper@37906
|
370 |
(*WN.24.4.03 -"- ... type parameters; afterwards naming inconsistent*)
|
neuper@37906
|
371 |
datatype 'a ptyp =
|
neuper@37906
|
372 |
Ptyp of string * (*element within pblID*)
|
neuper@37906
|
373 |
'a list * (*several pbts with different domIDs/thy
|
neuper@37906
|
374 |
TODO: select by subthy (isaref.p.69)
|
neuper@37906
|
375 |
presently only _ONE_ elem*)
|
neuper@37906
|
376 |
('a ptyp) list; (*the children nodes*)
|
neuper@37906
|
377 |
|
neuper@37906
|
378 |
(*.datatype for collecting thydata for hierarchy.*)
|
neuper@37906
|
379 |
(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
|
neuper@37906
|
380 |
(*WN0606 Htxt contains html which does not belong to the sml-kernel*)
|
neuper@37906
|
381 |
datatype thydata = Html of {guh: guh,
|
neuper@37906
|
382 |
coursedesign: authors,
|
neuper@37906
|
383 |
mathauthors: authors,
|
neuper@37906
|
384 |
html: string} (*html; for demos before database*)
|
neuper@37906
|
385 |
| Hthm of {guh: guh,
|
neuper@37906
|
386 |
coursedesign: authors,
|
neuper@37906
|
387 |
mathauthors: authors,
|
neuper@38002
|
388 |
thm: term}
|
neuper@37906
|
389 |
| Hrls of {guh: guh,
|
neuper@37906
|
390 |
coursedesign: authors,
|
neuper@37906
|
391 |
mathauthors: authors,
|
neuper@37906
|
392 |
(*like vvvvvvvvvvvvv val ruleset'
|
neuper@37906
|
393 |
WN060711 redesign together !*)
|
neuper@37906
|
394 |
thy_rls: (thyID * rls)}
|
neuper@37906
|
395 |
| Hcal of {guh: guh,
|
neuper@37906
|
396 |
coursedesign: authors,
|
neuper@37906
|
397 |
mathauthors: authors,
|
neuper@37906
|
398 |
calc: calc}
|
neuper@37906
|
399 |
| Hord of {guh: guh,
|
neuper@37906
|
400 |
coursedesign: authors,
|
neuper@37906
|
401 |
mathauthors: authors,
|
neuper@37906
|
402 |
ord: (subst -> (term * term) -> bool)};
|
neuper@37906
|
403 |
val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
|
neuper@37906
|
404 |
|
neuper@37906
|
405 |
type thehier = (thydata ptyp) list;
|
neuper@38006
|
406 |
val thehier = Unsynchronized.ref ([] : thehier);
|
neuper@37906
|
407 |
|
neuper@37906
|
408 |
(*.an association list, gets the value once in Isac.ML.*)
|
neuper@38006
|
409 |
val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
|
neuper@37906
|
410 |
|
neuper@37906
|
411 |
|
neuper@37906
|
412 |
type path = string;
|
neuper@37906
|
413 |
type filename = string;
|
neuper@37906
|
414 |
|
neuper@37906
|
415 |
(*val xxx = fn: a b => (a,b); ??? fun-definition ???*)
|
neuper@37906
|
416 |
local
|
neuper@37906
|
417 |
fun ii (_:term) = e_rrlsstate;
|
neuper@37906
|
418 |
fun no (_:term) = SOME (e_term,[e_term]);
|
neuper@37906
|
419 |
fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];
|
neuper@37906
|
420 |
fun ne (_:rule list list) (_:term) = SOME e_rule;
|
neuper@37906
|
421 |
fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];
|
neuper@37906
|
422 |
in
|
neuper@37906
|
423 |
val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,
|
neuper@37906
|
424 |
next_rule=ne,attach_form=fo};
|
neuper@37906
|
425 |
end;
|
neuper@37906
|
426 |
|
neuper@37906
|
427 |
val e_rls =
|
neuper@37906
|
428 |
Rls{id = "e_rls",
|
neuper@37906
|
429 |
preconds = [],
|
neuper@37906
|
430 |
rew_ord = ("dummy_ord", dummy_ord),
|
neuper@37906
|
431 |
erls = Erls,srls = Erls,
|
neuper@37906
|
432 |
calc = [],
|
neuper@37906
|
433 |
rules = [], scr = EmptyScr}:rls;
|
neuper@37906
|
434 |
val e_rrls = Rrls {id = "e_rrls",
|
neuper@37906
|
435 |
prepat = [],
|
neuper@37906
|
436 |
rew_ord = ("dummy_ord", dummy_ord),
|
neuper@37906
|
437 |
erls = Erls,
|
neuper@37906
|
438 |
calc = [],
|
neuper@37906
|
439 |
(*asm_thm=[],*)
|
neuper@37906
|
440 |
scr=e_rfuns}:rls;
|
neuper@37906
|
441 |
ruleset' := overwritel (!ruleset', [("e_rls",("Tools",e_rls)),
|
neuper@37906
|
442 |
("e_rrls",("Tools",e_rrls))
|
neuper@37906
|
443 |
]);
|
neuper@37906
|
444 |
|
neuper@37906
|
445 |
fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
|
neuper@37906
|
446 |
{id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
|
neuper@37906
|
447 |
(*asm_thm=asm_thm,*)rules=rules,scr=scr}
|
neuper@37906
|
448 |
| rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,(*asm_thm,*)rules,scr}) =
|
neuper@37906
|
449 |
{id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,
|
neuper@37906
|
450 |
(*asm_thm=asm_thm,*)rules=rules,scr=scr}
|
neuper@37906
|
451 |
| rep_rls Erls = rep_rls e_rls
|
neuper@37906
|
452 |
| rep_rls (Rrls {id,...}) = rep_rls e_rls
|
neuper@38031
|
453 |
(*error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)*);
|
neuper@37906
|
454 |
(*| rep_rls (Seq {id,...}) =
|
neuper@38031
|
455 |
error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);
|
neuper@37906
|
456 |
--1.7.03*)
|
neuper@37906
|
457 |
fun rep_rrls
|
neuper@37906
|
458 |
(Rrls {id,(*asm_thm,*) calc, erls, prepat, rew_ord,
|
neuper@37906
|
459 |
scr=Rfuns
|
neuper@37906
|
460 |
{attach_form,init_state,locate_rule,
|
neuper@37906
|
461 |
next_rule,normal_form}}) =
|
neuper@37906
|
462 |
{id=id,(*asm_thm=asm_thm,*) calc=calc, erls=erls, prepat=prepat,
|
neuper@37906
|
463 |
rew_ord=rew_ord, attach_form=attach_form, init_state=init_state,
|
neuper@37906
|
464 |
locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}
|
neuper@37906
|
465 |
| rep_rrls (Rls {id,...}) =
|
neuper@38031
|
466 |
error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)
|
neuper@37906
|
467 |
| rep_rrls (Seq {id,...}) =
|
neuper@38031
|
468 |
error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);
|
neuper@37906
|
469 |
|
neuper@37906
|
470 |
fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
471 |
rules =rs,scr=sc}) r =
|
neuper@37906
|
472 |
(Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
473 |
rules = rs @ r,scr=sc}:rls)
|
neuper@37906
|
474 |
| append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
475 |
rules =rs,scr=sc}) r =
|
neuper@37906
|
476 |
(Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
477 |
rules = rs @ r,scr=sc}:rls)
|
neuper@37906
|
478 |
| append_rls id (Rrls _) _ =
|
neuper@38031
|
479 |
error ("append_rls: not for reverse-rewrite-rule-set "^id);
|
neuper@37906
|
480 |
|
neuper@37906
|
481 |
(*. are _atomic_ rules equal ?.*)
|
neuper@37906
|
482 |
(*WN080102 compare eqrule ?!?*)
|
neuper@37906
|
483 |
fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
|
neuper@37906
|
484 |
| eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
|
neuper@37906
|
485 |
| eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
|
neuper@37906
|
486 |
(*id_rls checks for Rls, Seq, Rrls*)
|
neuper@37906
|
487 |
| eq_rule _ = false;
|
neuper@37906
|
488 |
|
neuper@37906
|
489 |
fun merge_rls _ Erls rls = rls
|
neuper@37906
|
490 |
| merge_rls _ rls Erls = rls
|
neuper@37906
|
491 |
| merge_rls id
|
neuper@37906
|
492 |
(Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
|
neuper@37906
|
493 |
(*asm_thm=at1,*)rules =rs1,scr=sc1})
|
neuper@37906
|
494 |
(r2 as Rls {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
|
neuper@37906
|
495 |
(*asm_thm=at2,*)rules =rs2,scr=sc2}) =
|
neuper@37906
|
496 |
(Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
|
neuper@37906
|
497 |
rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
|
neuper@37906
|
498 |
srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
|
neuper@37906
|
499 |
((#srls o rep_rls) r2),
|
neuper@37906
|
500 |
calc=ca1 @ ((#calc o rep_rls) r2),
|
neuper@37906
|
501 |
(*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
|
neuper@37906
|
502 |
rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
|
neuper@37906
|
503 |
scr=sc1}:rls)
|
neuper@37906
|
504 |
| merge_rls id
|
neuper@37906
|
505 |
(Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,
|
neuper@37906
|
506 |
(*asm_thm=at1,*)rules =rs1,scr=sc1})
|
neuper@37906
|
507 |
(r2 as Seq {id=id2,preconds=pc2,rew_ord=ro2,erls=er2,srls=sr2,calc=ca2,
|
neuper@37906
|
508 |
(*asm_thm=at2,*)rules =rs2,scr=sc2}) =
|
neuper@37906
|
509 |
(Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),
|
neuper@37906
|
510 |
rew_ord=ro1,erls=merge_rls "" er1 er2(*er1*),
|
neuper@37906
|
511 |
srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1
|
neuper@37906
|
512 |
((#srls o rep_rls) r2),
|
neuper@37906
|
513 |
calc=ca1 @ ((#calc o rep_rls) r2),
|
neuper@37906
|
514 |
(*asm_thm=at1 @ ((#asm_thm o rep_rls) r2),*)
|
neuper@37906
|
515 |
rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),
|
neuper@37906
|
516 |
scr=sc1}:rls)
|
neuper@37906
|
517 |
| merge_rls _ _ _ =
|
neuper@38031
|
518 |
error "merge_rls: not for reverse-rewrite-rule-sets\
|
neuper@37906
|
519 |
\and not for mixed Rls -- Seq";
|
neuper@37906
|
520 |
fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
521 |
(*asm_thm=at,*)rules =rs,scr=sc}) r =
|
neuper@37906
|
522 |
(Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
523 |
(*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
|
neuper@37906
|
524 |
scr=sc}:rls)
|
neuper@37906
|
525 |
| remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
526 |
(*asm_thm=at,*)rules =rs,scr=sc}) r =
|
neuper@37906
|
527 |
(Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,
|
neuper@37906
|
528 |
(*asm_thm=at,*)rules = gen_rems eq_rule (rs, r),
|
neuper@37906
|
529 |
scr=sc}:rls)
|
neuper@38031
|
530 |
| remove_rls id (Rrls _) _ = error
|
neuper@37906
|
531 |
("remove_rls: not for reverse-rewrite-rule-set "^id);
|
neuper@37906
|
532 |
|
neuper@37906
|
533 |
(*!!!> gen_rems (op=) ([1,2,3,4], [3,4,5]);
|
neuper@37906
|
534 |
val it = [1, 2] : int list*)
|
neuper@37906
|
535 |
|
neuper@37906
|
536 |
(*elder version: migrated 3 calls in smtest to memrls
|
neuper@37906
|
537 |
fun mem_rls id rls =
|
neuper@37906
|
538 |
case find_first ((curry op=) id) (map id_rule ((#rules o rep_rls) rls)) of
|
neuper@37906
|
539 |
SOME _ => true | NONE => false;*)
|
neuper@37906
|
540 |
fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)
|
neuper@37906
|
541 |
| memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)
|
neuper@38031
|
542 |
| memrls r _ = error ("memrls: incomplete impl. r= "^(rule2str r));
|
neuper@37906
|
543 |
fun rls_get_thm rls (id: xstring) =
|
neuper@37906
|
544 |
case find_first (curry eq_rule e_rule)
|
neuper@37906
|
545 |
((#rules o rep_rls) rls) of
|
neuper@37906
|
546 |
SOME thm => SOME thm | NONE => NONE;
|
neuper@37906
|
547 |
|
neuper@38031
|
548 |
fun assoc' ([], key) = error ("ME_Isa: '"^key^"' not known")
|
neuper@37906
|
549 |
| assoc' ((keyi, xi) :: pairs, key) =
|
neuper@37906
|
550 |
if key = keyi then SOME xi else assoc' (pairs, key);
|
neuper@37906
|
551 |
|
neuper@37927
|
552 |
(*100818 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))
|
neuper@38031
|
553 |
handle _ => error ("ME_Isa: thy '"^thy^"' not in system");*)
|
neuper@37928
|
554 |
fun assoc_thy (thy:theory') = (*FIXME100818 abolish*)
|
neuper@38042
|
555 |
(theory thy) handle _ => error ("ME_Isa: thy '" ^ thy ^ "' not in system");
|
neuper@37928
|
556 |
|
neuper@37906
|
557 |
(*.associate an rls-identifier with an rls; related to 'fun assoc_rls';
|
neuper@37906
|
558 |
these are NOT compatible to "fun assoc_thm'" in that they do NOT handle
|
neuper@37906
|
559 |
overlays by re-using an identifier in different thys.*)
|
neuper@37906
|
560 |
fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
|
neuper@38031
|
561 |
handle _ => error ("ME_Isa: '"^rls^"' not in system");
|
neuper@37906
|
562 |
(*fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))
|
neuper@38031
|
563 |
handle _ => error ("ME_Isa: '"^rls^"' not in system");*)
|
neuper@37906
|
564 |
|
neuper@37906
|
565 |
(*.overwrite an element in an association list and pair it with a thyID
|
neuper@37906
|
566 |
in order to create the thy_hierarchy;
|
neuper@37906
|
567 |
overwrites existing rls' even if they are defined in a different thy;
|
neuper@37906
|
568 |
this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc;.*)
|
neuper@37906
|
569 |
(*WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
|
neuper@37906
|
570 |
they do NOT handle overlays by re-using an identifier in different thys;
|
neuper@37906
|
571 |
"thyID.rlsID" would be a good solution, if the "." would be possible
|
neuper@37906
|
572 |
in scripts...
|
neuper@37906
|
573 |
actually a hack to get alltogether run again with minimal effort*)
|
neuper@37906
|
574 |
fun insthy thy' (rls', rls) = (rls', (thy', rls));
|
neuper@37906
|
575 |
fun overwritelthy thy (al, bl:(rls' * rls) list) =
|
neuper@37906
|
576 |
let val bl' = map (insthy ((get_thy o theory2theory') thy)) bl
|
neuper@37906
|
577 |
in overwritel (al, bl') end;
|
neuper@37906
|
578 |
|
neuper@37906
|
579 |
fun assoc_rew_ord ro = ((the o assoc') (!rew_ord',ro))
|
neuper@38031
|
580 |
handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
|
neuper@37906
|
581 |
(*get the string for stac from rule*)
|
neuper@38031
|
582 |
fun assoc_calc ([], key) = error ("assoc_calc: '"^ key ^"' not found")
|
neuper@37906
|
583 |
| assoc_calc ((calc, (keyi, xi)) :: pairs, key) =
|
neuper@37906
|
584 |
if key = keyi then calc else assoc_calc (pairs, key);
|
neuper@37906
|
585 |
(*only used for !calclist'...*)
|
neuper@38031
|
586 |
fun assoc1 ([], key) = error ("assoc1 (for met.calc=): '"^ key
|
neuper@37906
|
587 |
^"' not found")
|
neuper@37906
|
588 |
| assoc1 ((all as (keyi, _)) :: pairs, key) =
|
neuper@37906
|
589 |
if key = keyi then all else assoc1 (pairs, key);
|
neuper@37906
|
590 |
|
neuper@37906
|
591 |
(*TODO.WN080102 clarify usage of type cal and type calc..*)
|
neuper@37906
|
592 |
fun calID2calcID (calID : calID) =
|
neuper@38031
|
593 |
let fun ass [] = error ("calID2calcID: "^calID^"not in calclist'")
|
neuper@37906
|
594 |
| ass ((calci, (cali, eval_fn))::ids) =
|
neuper@37906
|
595 |
if calID = cali then calci
|
neuper@37906
|
596 |
else ass ids
|
neuper@37906
|
597 |
in ass (!calclist') : calcID end;
|
neuper@37906
|
598 |
|
neuper@37906
|
599 |
fun termopt2str (SOME t) =
|
neuper@37929
|
600 |
"SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
|
neuper@37906
|
601 |
| termopt2str NONE = "NONE";
|
neuper@38013
|
602 |
(*fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; Isa2002*)
|
neuper@38013
|
603 |
(*Florian1009: 'val' would ensure static lookup, i.e. only at compile time;
|
neuper@38013
|
604 |
however, dynamic lookup is required, since "Isac" is not yet built here.*)
|
neuper@38013
|
605 |
fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
|
neuper@38013
|
606 |
(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
|
neuper@38022
|
607 |
fun terms2str ts = (strs2str o (map term2str )) ts;
|
neuper@38022
|
608 |
(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
|
neuper@38022
|
609 |
fun terms2str' ts = (strs2str' o (map term2str )) ts;
|
neuper@38022
|
610 |
(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
|
neuper@38022
|
611 |
fun terms2strs ts = (map term2str) ts;
|
neuper@38022
|
612 |
(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
|
neuper@38013
|
613 |
|
neuper@38024
|
614 |
fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
|
neuper@37906
|
615 |
val string_of_typ = type2str;
|
neuper@37906
|
616 |
|
neuper@37906
|
617 |
fun subst2str (s:subst) =
|
neuper@37906
|
618 |
(strs2str o
|
neuper@37906
|
619 |
(map (linefeed o pair2str o
|
neuper@37906
|
620 |
(apsnd term2str) o
|
neuper@37906
|
621 |
(apfst term2str)))) s;
|
neuper@37906
|
622 |
fun subst2str' (s:subst) =
|
neuper@37906
|
623 |
(strs2str' o
|
neuper@37906
|
624 |
(map (pair2str o
|
neuper@37906
|
625 |
(apsnd term2str) o
|
neuper@37906
|
626 |
(apfst term2str)))) s;
|
neuper@37906
|
627 |
(*> subst2str' [(str2term "bdv", str2term "x"),
|
neuper@37906
|
628 |
(str2term "bdv_2", str2term "y")];
|
neuper@37906
|
629 |
val it = "[(bdv, x)]" : string
|
neuper@37906
|
630 |
*)
|
neuper@37906
|
631 |
val env2str = subst2str;
|
neuper@37906
|
632 |
|
neuper@37906
|
633 |
|
neuper@37906
|
634 |
(*recursive defs:*)
|
neuper@37906
|
635 |
fun scr2str (Script s) = "Script "^(term2str s)
|
neuper@37906
|
636 |
| scr2str (Rfuns _) = "Rfuns";
|
neuper@37906
|
637 |
|
neuper@37906
|
638 |
|
neuper@37906
|
639 |
fun maxthy thy1 thy2 = if Theory.subthy (thy1, thy2) then thy2 else thy1;
|
neuper@37906
|
640 |
|
neuper@37906
|
641 |
|
neuper@37906
|
642 |
(*.trace internal steps of isac's rewriter*)
|
neuper@38006
|
643 |
val trace_rewrite = Unsynchronized.ref false;
|
neuper@37906
|
644 |
(*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
|
neuper@38006
|
645 |
val depth = Unsynchronized.ref 99999;
|
neuper@37906
|
646 |
(*.no of rewrites exceeding this int -> NO rewrite.*)
|
neuper@37906
|
647 |
(*WN060829 still unused...*)
|
neuper@38006
|
648 |
val lim_rewrite = Unsynchronized.ref 99999;
|
neuper@37906
|
649 |
(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
|
neuper@38006
|
650 |
val lim_deriv = Unsynchronized.ref 100;
|
neuper@37906
|
651 |
(*.switch for checking guhs unique before storing a pbl or met;
|
neuper@37906
|
652 |
set true at startup (done at begin of ROOT.ML)
|
neuper@37906
|
653 |
set false for editing IsacKnowledge (done at end of ROOT.ML).*)
|
neuper@38006
|
654 |
val check_guhs_unique = Unsynchronized.ref false;
|
neuper@37906
|
655 |
|
neuper@37906
|
656 |
|
neuper@37906
|
657 |
datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
|
neuper@37906
|
658 |
L (*go left at $*)
|
neuper@37906
|
659 |
| R (*go right at $*)
|
neuper@37906
|
660 |
| D; (*go down at Abs*)
|
neuper@37906
|
661 |
type loc_ = lrd list;
|
neuper@37906
|
662 |
fun ldr2str L = "L"
|
neuper@37906
|
663 |
| ldr2str R = "R"
|
neuper@37906
|
664 |
| ldr2str D = "D";
|
neuper@37906
|
665 |
fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
|
neuper@37906
|
666 |
|