wneuper@59540
|
1 |
(* ~~/src/Tools/isac/calcelems.sml
|
wneuper@59540
|
2 |
elements of calculations.
|
neuper@37906
|
3 |
they are partially held in association lists as ref's for
|
wneuper@59405
|
4 |
switching language levels (meta-string, object-values).
|
wneuper@59405
|
5 |
in order to keep these ref's during re-evaluation of code,
|
neuper@42399
|
6 |
they are defined here at the beginning of the code.
|
neuper@42399
|
7 |
Author: Walther Neuper 2003
|
neuper@42399
|
8 |
(c) copyright due to lincense terms
|
neuper@37906
|
9 |
*)
|
neuper@37906
|
10 |
|
wneuper@59405
|
11 |
signature CALC_ELEMENT =
|
wneuper@59405
|
12 |
sig
|
wneuper@59413
|
13 |
type cas_elem
|
wneuper@59413
|
14 |
type pbt
|
wneuper@59413
|
15 |
type ptyps
|
wneuper@59413
|
16 |
type metID
|
wneuper@59413
|
17 |
type pblID
|
wneuper@59413
|
18 |
type mets
|
wneuper@59413
|
19 |
type met
|
wneuper@59405
|
20 |
datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
|
wneuper@59405
|
21 |
|
wneuper@59413
|
22 |
type authors
|
wneuper@59405
|
23 |
type guh
|
wneuper@59416
|
24 |
val env2str: Rule.subst -> string
|
wneuper@59416
|
25 |
val subst2str: Rule.subst -> string
|
wneuper@59416
|
26 |
val subst2str': Rule.subst -> string
|
wneuper@59414
|
27 |
|
wneuper@59413
|
28 |
type fillpat
|
wneuper@59405
|
29 |
datatype thydata
|
wneuper@59416
|
30 |
= Hcal of {calc: Rule.calc, coursedesign: authors, guh: guh, mathauthors: authors}
|
wneuper@59416
|
31 |
| Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}
|
wneuper@59416
|
32 |
| Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule.rls}
|
wneuper@59405
|
33 |
| Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
|
wneuper@59405
|
34 |
| Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
|
wneuper@59413
|
35 |
type theID
|
wneuper@59413
|
36 |
type rlss_elem
|
wneuper@59405
|
37 |
val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list
|
wneuper@59405
|
38 |
val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
|
wneuper@59413
|
39 |
type spec
|
wneuper@59405
|
40 |
val cas_eq: cas_elem * cas_elem -> bool
|
wneuper@59405
|
41 |
val e_Ptyp: pbt ptyp
|
wneuper@59405
|
42 |
val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
|
wneuper@59405
|
43 |
val check_guhs_unique: bool Unsynchronized.ref
|
wneuper@59405
|
44 |
val check_pblguh_unique: guh -> pbt ptyp list -> unit
|
wneuper@59405
|
45 |
val insrt: pblID -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
|
wneuper@59405
|
46 |
val e_Mets: met ptyp
|
wneuper@59405
|
47 |
val check_metguh_unique: guh -> met ptyp list -> unit
|
wneuper@59405
|
48 |
val add_thydata: string list * string list -> thydata -> thydata ptyp list -> thydata ptyp list
|
wneuper@59405
|
49 |
val get_py: 'a ptyp list -> pblID -> string list -> 'a
|
wneuper@59405
|
50 |
val update_hthm: thydata -> fillpat list -> thydata
|
wneuper@59405
|
51 |
val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
|
wneuper@59405
|
52 |
val part2guh: theID -> guh
|
wneuper@59405
|
53 |
val spec2str: string * string list * string list -> string
|
wneuper@59405
|
54 |
val linefeed: string -> string
|
wneuper@59405
|
55 |
val pbts2str: pbt list -> string
|
wneuper@59405
|
56 |
val thes2str: thydata list -> string
|
wneuper@59405
|
57 |
val theID2str: string list -> string
|
wneuper@59405
|
58 |
val the2str: thydata -> string
|
wneuper@59405
|
59 |
val trace_calc: bool Unsynchronized.ref
|
wneuper@59405
|
60 |
eqtype thmID
|
wneuper@59413
|
61 |
type thm'
|
wneuper@59405
|
62 |
datatype lrd = D | L | R
|
wneuper@59405
|
63 |
val trace_rewrite: bool Unsynchronized.ref
|
wneuper@59405
|
64 |
val depth: int Unsynchronized.ref
|
wneuper@59415
|
65 |
val assoc_thy: Rule.theory' -> theory
|
wneuper@59413
|
66 |
type loc_
|
wneuper@59405
|
67 |
val loc_2str: loc_ -> string
|
wneuper@59413
|
68 |
type thm''
|
wneuper@59405
|
69 |
val metID2str: string list -> string
|
wneuper@59405
|
70 |
val e_pblID: pblID
|
wneuper@59405
|
71 |
val e_metID: metID
|
wneuper@59405
|
72 |
val empty_spec: spec
|
wneuper@59414
|
73 |
val e_spec: spec
|
wneuper@59405
|
74 |
datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
|
wneuper@59413
|
75 |
type kestoreID
|
wneuper@59405
|
76 |
val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> pblID -> string list -> 'b
|
wneuper@59405
|
77 |
val ketype2str: ketype -> string
|
wneuper@59405
|
78 |
val coll_pblguhs: pbt ptyp list -> guh list
|
wneuper@59405
|
79 |
val coll_metguhs: met ptyp list -> guh list
|
wneuper@59413
|
80 |
type pat
|
wneuper@59405
|
81 |
val pats2str: pat list -> string
|
wneuper@59405
|
82 |
val maxthy: theory -> theory -> theory
|
wneuper@59405
|
83 |
eqtype filename
|
wneuper@59405
|
84 |
val lim_deriv: int Unsynchronized.ref
|
wneuper@59416
|
85 |
val id_of_thm: Rule.rule -> string
|
wneuper@59405
|
86 |
val isabthys: unit -> theory list
|
wneuper@59405
|
87 |
val thyID_of_derivation_name: string -> string
|
wneuper@59415
|
88 |
val partID': Rule.theory' -> string
|
wneuper@59415
|
89 |
val thm2guh: string * Rule.thyID -> thmID -> guh
|
wneuper@59405
|
90 |
val thmID_of_derivation_name: string -> string
|
wneuper@59416
|
91 |
val rls2guh: string * Rule.thyID -> Rule.rls' -> guh
|
wneuper@59405
|
92 |
val theID2guh: theID -> guh
|
wneuper@59405
|
93 |
eqtype fillpatID
|
wneuper@59405
|
94 |
type pbt_ = string * (term * term)
|
wneuper@59405
|
95 |
eqtype xml
|
wneuper@59415
|
96 |
val cal2guh: string * Rule.thyID -> string -> guh
|
wneuper@59405
|
97 |
val ketype2str': ketype -> string
|
wneuper@59405
|
98 |
val str2ketype': string -> ketype
|
wneuper@59405
|
99 |
val thmID_of_derivation_name': thm -> string
|
wneuper@59405
|
100 |
eqtype path
|
wneuper@59415
|
101 |
val theID2thyID: theID -> Rule.thyID
|
wneuper@59405
|
102 |
val thy2guh: theID -> guh
|
wneuper@59405
|
103 |
val thypart2guh: theID -> guh
|
wneuper@59474
|
104 |
val ord2guh: string * Rule.theory' -> string -> string
|
wneuper@59416
|
105 |
val update_hrls: thydata -> Rule.errpatID list -> thydata
|
wneuper@59405
|
106 |
eqtype iterID
|
wneuper@59405
|
107 |
eqtype calcID
|
wneuper@59405
|
108 |
val thm''_of_thm: thm -> thm''
|
wneuper@59416
|
109 |
val thm_of_thm: Rule.rule -> thm
|
wneuper@59408
|
110 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59540
|
111 |
val pats2str' : pat list -> string
|
wneuper@59414
|
112 |
val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
|
wneuper@59414
|
113 |
thydata ptyp list
|
wneuper@59408
|
114 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59411
|
115 |
val knowthys: unit -> theory list
|
wneuper@59411
|
116 |
val e_pbt: pbt
|
wneuper@59507
|
117 |
val e_met: met
|
wneuper@59408
|
118 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59414
|
119 |
|
wneuper@59414
|
120 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59416
|
121 |
val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->
|
wneuper@59416
|
122 |
(Rule.rls' * (string * Rule.rls)) list end
|
wneuper@59414
|
123 |
|
wneuper@59416
|
124 |
|
wneuper@59540
|
125 |
structure Celem(**): CALC_ELEMENT(**) =
|
neuper@38061
|
126 |
struct
|
wneuper@59405
|
127 |
|
wneuper@59414
|
128 |
val linefeed = (curry op^) "\n"; (* ?\<longrightarrow> libraryC ?*)
|
neuper@37906
|
129 |
type authors = string list;
|
neuper@37906
|
130 |
|
wneuper@59414
|
131 |
type iterID = int;
|
wneuper@59414
|
132 |
type calcID = int;
|
neuper@42399
|
133 |
|
neuper@55481
|
134 |
(* TODO CLEANUP Thm:
|
neuper@55487
|
135 |
Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
|
neuper@55487
|
136 |
(b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
|
neuper@55487
|
137 |
thmID : type for data from user input + program
|
neuper@55487
|
138 |
thmDeriv : type for thy_hierarchy ONLY
|
neuper@55487
|
139 |
obsolete types : thm' (SEE "ad thm'"), thm''.
|
wneuper@59250
|
140 |
revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
|
neuper@55487
|
141 |
activate : thmID_of_derivation_name'
|
neuper@55481
|
142 |
*)
|
neuper@42399
|
143 |
type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
|
neuper@42434
|
144 |
type thmDeriv = string; (* WN120524 deprecated
|
neuper@42434
|
145 |
thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name
|
neuper@42434
|
146 |
WN120524: dont use Thm.derivation_name, this is destroyed by num_str;
|
neuper@42434
|
147 |
Thm.get_name_hint survives num_str and seems perfectly reliable *)
|
neuper@42399
|
148 |
|
wneuper@59415
|
149 |
type thm' = thmID * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
|
wneuper@59414
|
150 |
val thm'2xml : int -> Celem.thm' -> Celem.xml
|
wneuper@59414
|
151 |
val assoc_thm': theory -> Celem.thm' -> thm
|
wneuper@59416
|
152 |
| Calculate' of Rule.theory' * string * term * (term * Celem.thm')
|
wneuper@59414
|
153 |
*)
|
wneuper@59251
|
154 |
(* tricky combination of (string, term) for theorems in Isac:
|
wneuper@59251
|
155 |
* case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
|
wneuper@59251
|
156 |
by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
|
wneuper@59251
|
157 |
* case 2 "sym_..": Global_Theory.get_thm..RS sym
|
wneuper@59251
|
158 |
* case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
|
wneuper@59255
|
159 |
from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
|
wneuper@59251
|
160 |
*)
|
wneuper@59253
|
161 |
type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
|
neuper@42399
|
162 |
|
neuper@40836
|
163 |
(*.a 'guh'='globally unique handle' is a string unique for each element
|
neuper@37906
|
164 |
of isac's KEStore and persistent over time
|
neuper@37906
|
165 |
(in particular under shifts within the respective hierarchy);
|
neuper@40836
|
166 |
specialty for thys:
|
neuper@37906
|
167 |
# guh NOT resistant agains shifts from one thy to another
|
neuper@37906
|
168 |
(which is the price for Isabelle's design: thy's overwrite ids of subthy's)
|
neuper@37906
|
169 |
# requirement for matchTheory: induce guh from tac + current thy
|
neuper@37906
|
170 |
(see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.)
|
neuper@40836
|
171 |
TODO: introduce to pbl, met.*)
|
neuper@37906
|
172 |
type guh = string;
|
neuper@37906
|
173 |
|
wneuper@59141
|
174 |
type xml = string; (* rm together with old code replaced by XML.tree *)
|
neuper@37906
|
175 |
|
neuper@42451
|
176 |
|
neuper@42451
|
177 |
(* for (at least) 2 kinds of access:
|
neuper@42451
|
178 |
(1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
|
neuper@42451
|
179 |
(2) given a thm, find respective fillpats *)
|
neuper@42451
|
180 |
type fillpatID = string
|
neuper@42451
|
181 |
type fillpat =
|
neuper@42451
|
182 |
fillpatID (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
|
neuper@42451
|
183 |
* term (* the pattern with fill-in gaps *)
|
wneuper@59415
|
184 |
* Rule.errpatID; (* which the fillpat would be a help for
|
neuper@42451
|
185 |
DESIGN ?TODO: list for several patterns ? *)
|
neuper@37906
|
186 |
|
neuper@40836
|
187 |
|
wneuper@59414
|
188 |
(* WN0509 discussion:
|
neuper@37906
|
189 |
#############################################################################
|
neuper@37906
|
190 |
# How to manage theorys in subproblems wrt. the requirement, #
|
neuper@37906
|
191 |
# that scripts should be re-usable ? #
|
neuper@37906
|
192 |
#############################################################################
|
neuper@37906
|
193 |
|
neuper@37988
|
194 |
eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
|
neuper@37906
|
195 |
which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
|
neuper@40836
|
196 |
because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
|
neuper@37906
|
197 |
is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
|
neuper@37906
|
198 |
(see match_ags).
|
neuper@37906
|
199 |
|
neuper@37906
|
200 |
Preliminary solution:
|
neuper@38011
|
201 |
# the thy in 'SubProblem (thy', pbl, arglist)' is not taken automatically,
|
neuper@38011
|
202 |
# instead the 'maxthy (rootthy pt) thy' is taken for each subpbl
|
neuper@40836
|
203 |
# however, a thy specified by the user in the rootpbl may lead to
|
neuper@40836
|
204 |
errors in far-off subpbls (which are not yet reported properly !!!)
|
neuper@37906
|
205 |
and interactively specifiying thys in subpbl is not very relevant.
|
neuper@37906
|
206 |
|
neuper@37906
|
207 |
Other solutions possible:
|
wneuper@59352
|
208 |
# always parse and type-check with Thy_Info_get_theory "Isac"
|
wneuper@59414
|
209 |
(rejected due to the vague idea eg. to re-use equations for R in C etc.)
|
neuper@37906
|
210 |
# regard the subthy-relation in specifying thys of subpbls
|
neuper@38011
|
211 |
# specifically handle 'SubProblem (undefined, pbl, arglist)'
|
neuper@37906
|
212 |
# ???
|
wneuper@59414
|
213 |
*)
|
wneuper@59414
|
214 |
|
wneuper@59415
|
215 |
fun id_of_thm (Rule.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
|
wneuper@59414
|
216 |
| id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
|
wneuper@59415
|
217 |
fun thm_of_thm (Rule.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
|
wneuper@59414
|
218 |
| thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
|
wneuper@59414
|
219 |
|
wneuper@59414
|
220 |
fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
|
wneuper@59414
|
221 |
fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
|
wneuper@59414
|
222 |
fun thyID_of_derivation_name dn = hd (space_explode "." dn);
|
wneuper@59414
|
223 |
fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
|
wneuper@59414
|
224 |
|
wneuper@59414
|
225 |
|
neuper@37906
|
226 |
|
neuper@37906
|
227 |
(*the key into the hierarchy ob theory elements*)
|
neuper@37906
|
228 |
type theID = string list;
|
wneuper@59414
|
229 |
val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
|
wneuper@59414
|
230 |
fun theID2thyID theID =
|
wneuper@59414
|
231 |
if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
|
wneuper@59414
|
232 |
else error ("theID2thyID called with " ^ theID2str theID);
|
neuper@37906
|
233 |
|
neuper@37906
|
234 |
(*the key into the hierarchy ob problems*)
|
wneuper@59414
|
235 |
type pblID = string list; (* domID :: ...*)
|
wneuper@59414
|
236 |
val e_pblID = ["e_pblID"];
|
neuper@37906
|
237 |
|
neuper@37906
|
238 |
(*the key into the hierarchy ob methods*)
|
neuper@37906
|
239 |
type metID = string list;
|
wneuper@59415
|
240 |
type spec = Rule.domID * pblID * metID;
|
wneuper@59414
|
241 |
fun spec2str (dom, pbl, met) =
|
wneuper@59414
|
242 |
"(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
|
wneuper@59414
|
243 |
val e_metID = ["e_metID"];
|
neuper@37906
|
244 |
val metID2str = strs2str;
|
wneuper@59415
|
245 |
val empty_spec = (Rule.e_domID, e_pblID, e_metID);
|
s1210629013@52171
|
246 |
val e_spec = empty_spec;
|
s1210629013@52171
|
247 |
|
wneuper@59414
|
248 |
(* association list with cas-commands, for generating a complete calc-head *)
|
neuper@52169
|
249 |
type generate_fn =
|
neuper@52169
|
250 |
(term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
|
neuper@52169
|
251 |
(term * (* description of an element *)
|
neuper@52169
|
252 |
term list) (* value of the element (always put into a list) *)
|
neuper@52169
|
253 |
list) (* of elements in the formalization *)
|
neuper@52169
|
254 |
type cas_elem =
|
neuper@52169
|
255 |
(term * (* cas-command, eg. 'solve' *)
|
neuper@52169
|
256 |
(spec * (* theory, problem, method *)
|
s1210629013@52174
|
257 |
generate_fn))
|
neuper@52169
|
258 |
fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
|
s1210629013@52167
|
259 |
|
neuper@37906
|
260 |
(*either theID or pblID or metID*)
|
neuper@37906
|
261 |
type kestoreID = string list;
|
neuper@37906
|
262 |
|
wneuper@59414
|
263 |
(* for distinction of contexts WN130621: disambiguate with Isabelle's Context *)
|
neuper@37906
|
264 |
datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
|
neuper@37906
|
265 |
fun ketype2str Exp_ = "Exp_"
|
neuper@40836
|
266 |
| ketype2str Thy_ = "Thy_"
|
neuper@40836
|
267 |
| ketype2str Pbl_ = "Pbl_"
|
neuper@37906
|
268 |
| ketype2str Met_ = "Met_";
|
neuper@37906
|
269 |
fun ketype2str' Exp_ = "Example"
|
neuper@40836
|
270 |
| ketype2str' Thy_ = "Theory"
|
neuper@40836
|
271 |
| ketype2str' Pbl_ = "Problem"
|
neuper@37906
|
272 |
| ketype2str' Met_ = "Method";
|
wneuper@59172
|
273 |
(* for conversion from XML *)
|
wneuper@59172
|
274 |
fun str2ketype' "exp" = Exp_
|
wneuper@59172
|
275 |
| str2ketype' "thy" = Thy_
|
wneuper@59172
|
276 |
| str2ketype' "pbl" = Pbl_
|
wneuper@59172
|
277 |
| str2ketype' "met" = Met_
|
wneuper@59172
|
278 |
| str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
|
neuper@37906
|
279 |
|
neuper@48887
|
280 |
(* A tree for storing data defined in different theories
|
neuper@48887
|
281 |
for access from the Interpreter and from dialogue authoring
|
neuper@48887
|
282 |
using a string list as key.
|
wneuper@59414
|
283 |
'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)
|
neuper@40836
|
284 |
datatype 'a ptyp =
|
wneuper@59414
|
285 |
Ptyp of string * (* element of the key *)
|
wneuper@59414
|
286 |
'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
|
wneuper@59414
|
287 |
presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
|
wneuper@59414
|
288 |
('a ptyp) list; (* the children nodes *)
|
neuper@37906
|
289 |
|
wneuper@59414
|
290 |
(* datatype for collecting thydata for hierarchy *)
|
neuper@37906
|
291 |
(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
|
wneuper@59414
|
292 |
datatype thydata =
|
wneuper@59414
|
293 |
Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
|
wneuper@59414
|
294 |
| Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,
|
wneuper@59414
|
295 |
thm: thm} (* here no sym_thm, thus no thmID required *)
|
wneuper@59415
|
296 |
| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule.rls)}
|
wneuper@59415
|
297 |
| Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule.calc}
|
wneuper@59414
|
298 |
| Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
|
wneuper@59415
|
299 |
ord: (Rule.subst -> (term * term) -> bool)};
|
wneuper@59414
|
300 |
fun the2str (Html {guh, ...}) = guh
|
wneuper@59414
|
301 |
| the2str (Hthm {guh, ...}) = guh
|
wneuper@59414
|
302 |
| the2str (Hrls {guh, ...}) = guh
|
wneuper@59414
|
303 |
| the2str (Hcal {guh, ...}) = guh
|
wneuper@59414
|
304 |
| the2str (Hord {guh, ...}) = guh
|
neuper@55435
|
305 |
fun thes2str thes = map the2str thes |> list2str;
|
neuper@37906
|
306 |
|
neuper@55483
|
307 |
(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
|
neuper@55487
|
308 |
(a): thehier does not contain sym_thmID theorems
|
neuper@55485
|
309 |
(b): lookup for sym_thmID directly from Isabelle using sym_thm
|
neuper@55485
|
310 |
(within math-engine NO lookup in thehier -- within java in *.xml only!)
|
neuper@55483
|
311 |
TODO (c): export from thehier to xml
|
neuper@55483
|
312 |
TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
|
neuper@55483
|
313 |
TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
|
neuper@55483
|
314 |
TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
|
neuper@55483
|
315 |
stands for both, "thmID" and "sym_thmID"
|
neuper@55483
|
316 |
TODO (d1) lookup from calctxt
|
neuper@55483
|
317 |
TODO (d1) lookup from from rule set in MiniBrowser *)
|
neuper@37906
|
318 |
type thehier = (thydata ptyp) list;
|
neuper@55405
|
319 |
(* required to determine sequence of main nodes of thehier in KEStore.thy *)
|
wneuper@59414
|
320 |
fun part2guh [str] = (case str of
|
wneuper@59414
|
321 |
"Isabelle" => "thy_isab_" ^ str ^ "-part" : guh
|
neuper@55405
|
322 |
| "IsacScripts" => "thy_scri_" ^ str ^ "-part"
|
neuper@55405
|
323 |
| "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
|
wneuper@59414
|
324 |
| str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
|
wneuper@59414
|
325 |
| part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
|
neuper@37906
|
326 |
|
wneuper@59414
|
327 |
fun thy2guh [part, thyID] = (case part of
|
wneuper@59414
|
328 |
"Isabelle" => "thy_isab_" ^ thyID
|
neuper@55437
|
329 |
| "IsacScripts" => "thy_scri_" ^ thyID
|
neuper@55437
|
330 |
| "IsacKnowledge" => "thy_isac_" ^ thyID
|
wneuper@59414
|
331 |
| str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
|
wneuper@59414
|
332 |
| thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
|
neuper@55437
|
333 |
|
wneuper@59414
|
334 |
fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
|
wneuper@59414
|
335 |
"Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh
|
wneuper@59414
|
336 |
| "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
|
wneuper@59414
|
337 |
| "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
|
wneuper@59414
|
338 |
| str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
|
wneuper@59414
|
339 |
| thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
|
wneuper@59414
|
340 |
|
neuper@55437
|
341 |
|
wneuper@59414
|
342 |
(* convert the data got via contextToThy to a globally unique handle.
|
wneuper@59414
|
343 |
there is another way to get the guh: get out of the 'theID' in the hierarchy *)
|
wneuper@59414
|
344 |
fun thm2guh (isa, thyID) thmID = case isa of
|
wneuper@59415
|
345 |
"Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
|
wneuper@59415
|
346 |
| "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
|
wneuper@59415
|
347 |
| "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
|
wneuper@59414
|
348 |
| _ => raise ERROR
|
wneuper@59414
|
349 |
("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
|
neuper@55437
|
350 |
|
wneuper@59414
|
351 |
fun rls2guh (isa, thyID) rls' = case isa of
|
wneuper@59415
|
352 |
"Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls' : guh
|
wneuper@59415
|
353 |
| "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls'
|
wneuper@59415
|
354 |
| "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls'
|
wneuper@59414
|
355 |
| _ => raise ERROR
|
wneuper@59414
|
356 |
("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
|
neuper@55437
|
357 |
|
wneuper@59414
|
358 |
fun cal2guh (isa, thyID) calID = case isa of
|
wneuper@59415
|
359 |
"Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID : guh
|
wneuper@59415
|
360 |
| "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID
|
wneuper@59415
|
361 |
| "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID
|
wneuper@59414
|
362 |
| _ => raise ERROR
|
wneuper@59414
|
363 |
("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
|
neuper@55437
|
364 |
|
wneuper@59414
|
365 |
fun ord2guh (isa, thyID) rew_ord' = case isa of
|
wneuper@59415
|
366 |
"Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
|
wneuper@59415
|
367 |
| "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord'
|
wneuper@59415
|
368 |
| "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord'
|
wneuper@59414
|
369 |
| _ => raise ERROR
|
wneuper@59414
|
370 |
("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
|
neuper@55437
|
371 |
|
neuper@55437
|
372 |
(* not only for thydata, but also for thy's etc *)
|
wneuper@59414
|
373 |
(* TODO
|
wneuper@59414
|
374 |
fun theID2guh theID = case length theID of
|
neuper@55437
|
375 |
0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
|
neuper@55437
|
376 |
| 1 => part2guh theID
|
neuper@55437
|
377 |
| 2 => thy2guh theID
|
neuper@55437
|
378 |
| 3 => thypart2guh theID
|
neuper@55437
|
379 |
| 4 =>
|
neuper@55437
|
380 |
let val [isa, thyID, typ, elemID] = theID
|
neuper@55437
|
381 |
in case typ of
|
neuper@55437
|
382 |
"Theorems" => thm2guh (isa, thyID) elemID
|
neuper@55437
|
383 |
| "Rulesets" => rls2guh (isa, thyID) elemID
|
neuper@55437
|
384 |
| "Calculations" => cal2guh (isa, thyID) elemID
|
neuper@55437
|
385 |
| "Orders" => ord2guh (isa, thyID) elemID
|
neuper@55437
|
386 |
| "Theorems" => thy2guh [isa, thyID]
|
wneuper@59414
|
387 |
| str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
|
neuper@55437
|
388 |
end
|
wneuper@59414
|
389 |
| n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
|
wneuper@59414
|
390 |
*)
|
wneuper@59414
|
391 |
(* not only for thydata, but also for thy's etc *)
|
wneuper@59414
|
392 |
fun theID2guh [] = raise ERROR ("theID2guh: called with []")
|
wneuper@59414
|
393 |
| theID2guh [str] = part2guh [str]
|
wneuper@59414
|
394 |
| theID2guh [s1, s2] = thy2guh [s1, s2]
|
wneuper@59414
|
395 |
| theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
|
wneuper@59414
|
396 |
| theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
|
wneuper@59414
|
397 |
"Theorems" => thm2guh (isa, thyID) elemID
|
wneuper@59414
|
398 |
| "Rulesets" => rls2guh (isa, thyID) elemID
|
wneuper@59414
|
399 |
| "Calculations" => cal2guh (isa, thyID) elemID
|
wneuper@59414
|
400 |
| "Orders" => ord2guh (isa, thyID) elemID
|
wneuper@59414
|
401 |
| _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
|
wneuper@59414
|
402 |
| theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
|
neuper@55437
|
403 |
|
neuper@37906
|
404 |
type path = string;
|
neuper@37906
|
405 |
type filename = string;
|
neuper@37906
|
406 |
|
neuper@42451
|
407 |
|
neuper@37906
|
408 |
|
neuper@52141
|
409 |
(* datastructure for KEStore_Elems, intermediate for thehier *)
|
neuper@52141
|
410 |
type rlss_elem =
|
wneuper@59416
|
411 |
(Rule.rls' * (* identifier unique within Isac *)
|
wneuper@59415
|
412 |
(Rule.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
|
wneuper@59415
|
413 |
Rule.rls)) (* ((#id o rep_rls) rls) = rls' by coding discipline *)
|
neuper@52141
|
414 |
fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2
|
neuper@37906
|
415 |
|
neuper@52141
|
416 |
fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys =
|
wneuper@59414
|
417 |
case get_index (fn y => if curry rls_eq re y then SOME y else NONE) ys of
|
wneuper@59414
|
418 |
NONE => re :: ys
|
wneuper@59414
|
419 |
| SOME (i, (_, (_, r2))) =>
|
neuper@52141
|
420 |
let
|
wneuper@59415
|
421 |
val r12 = Rule.merge_rls id r1 r2
|
neuper@52141
|
422 |
in list_update ys i (id, (thyID, r12)) end
|
neuper@52141
|
423 |
fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;
|
neuper@52141
|
424 |
|
neuper@52141
|
425 |
|
wneuper@59414
|
426 |
fun assoc_thy thy =
|
wneuper@59414
|
427 |
if thy = "e_domID"
|
wneuper@59415
|
428 |
then (Rule.Thy_Info_get_theory "Script") (*lower bound of Knowledge*)
|
wneuper@59415
|
429 |
else (Rule.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
|
neuper@37906
|
430 |
|
wneuper@59414
|
431 |
(* overwrite an element in an association list and pair it with a thyID
|
neuper@37906
|
432 |
in order to create the thy_hierarchy;
|
neuper@37906
|
433 |
overwrites existing rls' even if they are defined in a different thy;
|
wneuper@59414
|
434 |
this is related to assoc_rls, TODO.WN060120: assoc_rew_ord, assoc_calc *)
|
wneuper@59414
|
435 |
(* WN060120 ...these are NOT compatible to "fun assoc_thm'" in that
|
neuper@37906
|
436 |
they do NOT handle overlays by re-using an identifier in different thys;
|
neuper@37906
|
437 |
"thyID.rlsID" would be a good solution, if the "." would be possible
|
neuper@37906
|
438 |
in scripts...
|
wneuper@59414
|
439 |
actually a hack to get alltogether run again with minimal effort *)
|
neuper@37906
|
440 |
fun insthy thy' (rls', rls) = (rls', (thy', rls));
|
wneuper@59416
|
441 |
fun overwritelthy thy (al, bl: (Rule.rls' * Rule.rls) list) =
|
wneuper@59415
|
442 |
let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl
|
neuper@37906
|
443 |
in overwritel (al, bl') end;
|
neuper@37906
|
444 |
|
wneuper@59414
|
445 |
fun subst2str s =
|
neuper@40836
|
446 |
(strs2str o
|
wneuper@59414
|
447 |
(map (
|
wneuper@59415
|
448 |
linefeed o pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;
|
wneuper@59415
|
449 |
fun subst2str' s =
|
neuper@40836
|
450 |
(strs2str' o
|
wneuper@59414
|
451 |
(map (
|
wneuper@59415
|
452 |
pair2str o (apsnd Rule.term2str) o (apfst Rule.term2str)))) s;
|
neuper@37906
|
453 |
val env2str = subst2str;
|
neuper@37906
|
454 |
|
wneuper@59332
|
455 |
fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
|
neuper@37906
|
456 |
|
neuper@37906
|
457 |
|
wneuper@59387
|
458 |
(* trace internal steps of isac's numeral calculations *)
|
wneuper@59387
|
459 |
val trace_calc = Unsynchronized.ref false;
|
wneuper@59414
|
460 |
(* trace internal steps of isac's rewriter *)
|
neuper@38006
|
461 |
val trace_rewrite = Unsynchronized.ref false;
|
wneuper@59414
|
462 |
(* depth of recursion in traces of the rewriter, if trace_rewrite:=true *)
|
neuper@38006
|
463 |
val depth = Unsynchronized.ref 99999;
|
wneuper@59414
|
464 |
(* no of rewrites exceeding this int -> NO rewrite *)
|
neuper@38006
|
465 |
val lim_deriv = Unsynchronized.ref 100;
|
wneuper@59414
|
466 |
(* switch for checking guhs unique before storing a pbl or met;
|
neuper@37906
|
467 |
set true at startup (done at begin of ROOT.ML)
|
wneuper@59414
|
468 |
set false for editing IsacKnowledge (done at end of ROOT.ML) *)
|
neuper@41905
|
469 |
val check_guhs_unique = Unsynchronized.ref true;
|
neuper@37906
|
470 |
|
neuper@37906
|
471 |
|
wneuper@59414
|
472 |
datatype lrd = (*elements of "type loc_" into an Isabelle term*)
|
wneuper@59414
|
473 |
L (*go left at $*)
|
wneuper@59414
|
474 |
| R (*go right at $*)
|
wneuper@59414
|
475 |
| D; (*go down at Abs*)
|
neuper@37906
|
476 |
type loc_ = lrd list;
|
neuper@37906
|
477 |
fun ldr2str L = "L"
|
neuper@37906
|
478 |
| ldr2str R = "R"
|
neuper@37906
|
479 |
| ldr2str D = "D";
|
wneuper@59414
|
480 |
fun loc_2str k = (strs2str' o (map ldr2str)) k;
|
neuper@37906
|
481 |
|
neuper@55335
|
482 |
|
neuper@55335
|
483 |
(* the pattern for an item of a problems model or a methods guard *)
|
neuper@55335
|
484 |
type pat =
|
neuper@55335
|
485 |
(string * (* field *)
|
neuper@55335
|
486 |
(term * (* description *)
|
neuper@55335
|
487 |
term)) (* id | arbitrary term *);
|
neuper@55335
|
488 |
fun pat2str ((field, (dsc, id)) : pat) =
|
wneuper@59415
|
489 |
pair2str (field, pair2str (Rule.term2str dsc, Rule.term2str id))
|
neuper@55335
|
490 |
fun pats2str pats = (strs2str o (map pat2str)) pats
|
wneuper@59540
|
491 |
fun pat2str' ((field, (dsc, id)) : pat) =
|
wneuper@59540
|
492 |
pair2str (field, pair2str (Rule.term2str dsc, Rule.term2str id)) ^ "\n"
|
wneuper@59540
|
493 |
fun pats2str' pats = (strs2str o (map pat2str')) pats
|
neuper@55335
|
494 |
|
neuper@55357
|
495 |
(* types for problems models (TODO rename to specification models) *)
|
neuper@55335
|
496 |
type pbt_ =
|
neuper@55335
|
497 |
(string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
|
neuper@55335
|
498 |
(term * (* description *)
|
neuper@55335
|
499 |
term)); (* id | struct-var *)
|
neuper@55335
|
500 |
type pbt =
|
wneuper@59414
|
501 |
{guh : guh, (* unique within this isac-knowledge *)
|
wneuper@59414
|
502 |
mathauthors : string list, (* copyright *)
|
wneuper@59414
|
503 |
init : pblID, (* to start refinement with *)
|
neuper@55335
|
504 |
thy : theory, (* which allows to compile that pbt
|
wneuper@59414
|
505 |
TODO: search generalized for subthy (ref.p.69*)
|
wneuper@59414
|
506 |
(*^^^ WN050912 NOT used during application of the problem,
|
wneuper@59414
|
507 |
because applied terms may be from 'subthy' as well as from super;
|
wneuper@59414
|
508 |
thus we take 'maxthy'; see match_ags ! *)
|
wneuper@59414
|
509 |
cas : term option, (* 'CAS-command' *)
|
wneuper@59415
|
510 |
prls : Rule.rls, (* for preds in where_ *)
|
wneuper@59414
|
511 |
where_ : term list, (* where - predicates *)
|
neuper@55335
|
512 |
ppc : pat list, (* this is the model-pattern;
|
wneuper@59414
|
513 |
it contains "#Given","#Where","#Find","#Relate"-patterns
|
wneuper@59414
|
514 |
for constraints on identifiers see "fun cpy_nam" *)
|
wneuper@59414
|
515 |
met : metID list} (* methods solving the pbt *)
|
neuper@55335
|
516 |
|
wneuper@59397
|
517 |
val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
|
wneuper@59416
|
518 |
cas = NONE, prls = Rule.Erls, where_ = [], ppc = [], met = []} : pbt
|
wneuper@59414
|
519 |
fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
|
wneuper@59414
|
520 |
prls = prls', thy = thy', where_ = w'} : pbt)
|
wneuper@59415
|
521 |
= "{cas = " ^ (Rule.termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
|
wneuper@59414
|
522 |
^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
|
wneuper@59414
|
523 |
^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
|
wneuper@59415
|
524 |
^ (Rule.rls2str prls' |> quote) ^ ", thy = {" ^ (Rule.theory2str thy') ^ "}, where_ = "
|
wneuper@59415
|
525 |
^ (Rule.terms2str w') ^ "}" |> linefeed;
|
s1210629013@55345
|
526 |
fun pbts2str pbts = map pbt2str pbts |> list2str;
|
neuper@55335
|
527 |
|
wneuper@59416
|
528 |
val e_Ptyp = Ptyp ("e_pblID", [e_pbt], [])
|
neuper@55335
|
529 |
type ptyps = (pbt ptyp) list
|
neuper@55335
|
530 |
|
neuper@55357
|
531 |
fun coll_pblguhs pbls =
|
wneuper@59414
|
532 |
let
|
wneuper@59414
|
533 |
fun node coll (Ptyp (_, [n], ns)) = [(#guh : pbt -> guh) n] @ (nodes coll ns)
|
wneuper@59414
|
534 |
| node _ _ = raise ERROR "coll_pblguhs - node"
|
wneuper@59414
|
535 |
and nodes coll [] = coll
|
wneuper@59414
|
536 |
| nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
|
wneuper@59414
|
537 |
in nodes [] pbls end;
|
wneuper@59414
|
538 |
fun check_pblguh_unique guh pbls =
|
wneuper@59414
|
539 |
if member op = (coll_pblguhs pbls) guh
|
wneuper@59414
|
540 |
then error ("check_guh_unique failed with \""^ guh ^"\";\n"^
|
wneuper@59414
|
541 |
"use \"sort_pblguhs()\" for a list of guhs;\n"^
|
wneuper@59414
|
542 |
"consider setting \"check_guhs_unique := false\"")
|
wneuper@59414
|
543 |
else ();
|
s1210629013@55339
|
544 |
|
neuper@55453
|
545 |
fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
|
neuper@55453
|
546 |
| insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
|
wneuper@59414
|
547 |
((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
|
wneuper@59414
|
548 |
if k = k'
|
wneuper@59414
|
549 |
then ((Ptyp (k', [pbt], ps)) :: pys)
|
wneuper@59414
|
550 |
else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
|
wneuper@59414
|
551 |
)
|
wneuper@59414
|
552 |
| insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =
|
wneuper@59414
|
553 |
((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
|
wneuper@59414
|
554 |
if k = k'
|
wneuper@59414
|
555 |
then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
|
wneuper@59414
|
556 |
else
|
wneuper@59414
|
557 |
if length pys = 0
|
wneuper@59414
|
558 |
then error ("insert: not found " ^ (strs2str (d : pblID)))
|
wneuper@59414
|
559 |
else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
|
wneuper@59414
|
560 |
)
|
wneuper@59414
|
561 |
| insrt _ _ _ _ = raise ERROR "";
|
s1210629013@55339
|
562 |
|
neuper@55448
|
563 |
fun update_ptyps ID _ _ [] =
|
neuper@55448
|
564 |
error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
|
neuper@55448
|
565 |
| update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
|
neuper@55448
|
566 |
if i = key
|
neuper@55448
|
567 |
then
|
neuper@55448
|
568 |
if length pys = 0
|
neuper@55448
|
569 |
then ((Ptyp (key, [data], [])) :: pyss)
|
neuper@55448
|
570 |
else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
|
neuper@55448
|
571 |
else py :: update_ptyps ID [i] data pyss
|
neuper@55448
|
572 |
| update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
|
neuper@55448
|
573 |
if i = key
|
neuper@55448
|
574 |
then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
|
neuper@55448
|
575 |
else (py :: (update_ptyps ID (i :: is) data pyss))
|
wneuper@59414
|
576 |
| update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
|
neuper@55448
|
577 |
|
s1210629013@55339
|
578 |
(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
|
s1210629013@55339
|
579 |
function for trees / ptyps *)
|
s1210629013@55339
|
580 |
fun merge_ptyps ([], pt) = pt
|
s1210629013@55339
|
581 |
| merge_ptyps (pt, []) = pt
|
wneuper@59414
|
582 |
| merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
|
s1210629013@55346
|
583 |
if k = k'
|
s1210629013@55346
|
584 |
then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
|
s1210629013@55346
|
585 |
else x' :: merge_ptyps (xs, xs');
|
s1210629013@55372
|
586 |
|
s1210629013@55372
|
587 |
(* data for methods stored in 'methods'-database*)
|
s1210629013@55372
|
588 |
type met =
|
wneuper@59429
|
589 |
{guh : guh, (* unique within this isac-knowledge *)
|
wneuper@59429
|
590 |
mathauthors: string list, (* copyright *)
|
wneuper@59429
|
591 |
init : pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
|
wneuper@59429
|
592 |
rew_ord' : Rule.rew_ord', (* for rules in Detail
|
wneuper@59429
|
593 |
TODO.WN0509 store fun itself, see 'type pbt' *)
|
wneuper@59429
|
594 |
erls : Rule.rls, (* the eval_rls for cond. in rules FIXME "rls'
|
wneuper@59429
|
595 |
instead erls in "fun prep_met" *)
|
wneuper@59429
|
596 |
srls : Rule.rls, (* for evaluating list expressions in scr *)
|
wneuper@59429
|
597 |
prls : Rule.rls, (* for evaluating predicates in modelpattern *)
|
wneuper@59429
|
598 |
crls : Rule.rls, (* for check_elementwise, ie. formulae in calc. *)
|
wneuper@59429
|
599 |
nrls : Rule.rls, (* canonical simplifier specific for this met *)
|
wneuper@59429
|
600 |
errpats : Rule.errpat list,(* error patterns expected in this method *)
|
wneuper@59429
|
601 |
calc : Rule.calc list, (* Theory_Data in fun prep_met *)
|
wneuper@59429
|
602 |
(*branch : TransitiveB set in append_problem at generation ob pblobj *)
|
wneuper@59429
|
603 |
ppc : pat list, (* items in given, find, relate;
|
s1210629013@55372
|
604 |
items (in "#Find") which need not occur in the arg-list of a SubProblem
|
s1210629013@55372
|
605 |
are 'copy-named' with an identifier "*'.'".
|
s1210629013@55372
|
606 |
copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
|
wneuper@59429
|
607 |
see ME/calchead.sml 'fun is_copy_named'. *)
|
wneuper@59429
|
608 |
pre : term list, (* preconditions in where *)
|
wneuper@59563
|
609 |
scr : Rule.program (* progam, empty as @{thm refl} or Rfuns *)
|
s1210629013@55372
|
610 |
};
|
wneuper@59414
|
611 |
val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
|
wneuper@59415
|
612 |
erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls,
|
wneuper@59415
|
613 |
errpats = [], nrls = Rule.e_rls, ppc = [], pre = [], scr = Rule.EmptyScr};
|
wneuper@59414
|
614 |
val e_Mets = Ptyp ("e_metID", [e_met],[]);
|
s1210629013@55372
|
615 |
|
s1210629013@55372
|
616 |
type mets = (met ptyp) list;
|
s1210629013@55373
|
617 |
fun coll_metguhs mets =
|
wneuper@59414
|
618 |
let
|
wneuper@59414
|
619 |
fun node coll (Ptyp (_, [n], ns)) = [(#guh : met -> guh) n] @ (nodes coll ns)
|
wneuper@59414
|
620 |
| node _ _ = raise ERROR "coll_pblguhs - node"
|
wneuper@59414
|
621 |
and nodes coll [] = coll
|
wneuper@59414
|
622 |
| nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
|
s1210629013@55373
|
623 |
in nodes [] mets end;
|
s1210629013@55373
|
624 |
fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
|
s1210629013@55373
|
625 |
if member op = (coll_metguhs mets) guh
|
wneuper@59414
|
626 |
then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
|
wneuper@59473
|
627 |
(*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
|
wneuper@59414
|
628 |
"consider setting \"check_guhs_unique := false\"")
|
s1210629013@55373
|
629 |
else ();
|
s1210629013@55373
|
630 |
|
neuper@55450
|
631 |
fun Html_default exist = (Html {guh = theID2guh exist,
|
neuper@55450
|
632 |
coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
|
neuper@55450
|
633 |
|
wneuper@59414
|
634 |
fun fill_parents (_, [i]) thydata = Ptyp (i, [thydata], [])
|
neuper@55450
|
635 |
| fill_parents (exist, i :: is) thydata =
|
neuper@55450
|
636 |
Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
|
wneuper@59414
|
637 |
| fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
|
neuper@55450
|
638 |
|
neuper@55450
|
639 |
fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
|
neuper@55450
|
640 |
| add_thydata (exist, [i]) data (pys as (py as Ptyp (key, _, _)) :: pyss) =
|
neuper@55450
|
641 |
if i = key
|
neuper@55450
|
642 |
then pys (* preserve existing thydata *)
|
neuper@55450
|
643 |
else py :: add_thydata (exist, [i]) data pyss
|
neuper@55450
|
644 |
| add_thydata (exist, iss as (i :: is)) data ((py as Ptyp (key, d, pys)) :: pyss) =
|
neuper@55450
|
645 |
if i = key
|
neuper@55450
|
646 |
then
|
neuper@55450
|
647 |
if length pys = 0
|
neuper@55450
|
648 |
then Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
|
neuper@55450
|
649 |
else Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
|
neuper@55450
|
650 |
else py :: add_thydata (exist, iss) data pyss
|
wneuper@59414
|
651 |
| add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
|
neuper@55448
|
652 |
|
neuper@55448
|
653 |
fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
|
neuper@55448
|
654 |
Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
|
neuper@55448
|
655 |
fillpats = fillpats', thm = thm}
|
wneuper@59414
|
656 |
| update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
|
neuper@55448
|
657 |
|
wneuper@59414
|
658 |
(* for dialog-authoring *)
|
neuper@55448
|
659 |
fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
|
wneuper@59414
|
660 |
let
|
wneuper@59414
|
661 |
val rls' =
|
wneuper@59414
|
662 |
case rls of
|
wneuper@59415
|
663 |
Rule.Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
|
wneuper@59415
|
664 |
=> Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
|
wneuper@59414
|
665 |
calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
|
wneuper@59415
|
666 |
| Rule.Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
|
wneuper@59415
|
667 |
=> Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
|
wneuper@59414
|
668 |
calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
|
wneuper@59415
|
669 |
| Rule.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
|
wneuper@59415
|
670 |
=> Rule.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
|
wneuper@59414
|
671 |
scr = scr, errpatts = errpatIDs}
|
wneuper@59414
|
672 |
| Erls => Erls
|
wneuper@59414
|
673 |
in
|
wneuper@59414
|
674 |
Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
|
wneuper@59414
|
675 |
thy_rls = (thyID, rls')}
|
wneuper@59414
|
676 |
end
|
wneuper@59414
|
677 |
| update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
|
wneuper@59414
|
678 |
|
wneuper@59414
|
679 |
fun app_py p f (d:pblID) (k(*:pblRD*)) =
|
neuper@55448
|
680 |
let
|
wneuper@59414
|
681 |
fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);
|
neuper@55448
|
682 |
fun app_py' _ [] = py_err ()
|
neuper@55448
|
683 |
| app_py' [] _ = py_err ()
|
wneuper@59414
|
684 |
| app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) =
|
wneuper@59414
|
685 |
if k0 = k' then f p' else app_py' [k0] ps
|
wneuper@59414
|
686 |
| app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =
|
wneuper@59414
|
687 |
if k0 = k'' then app_py' ks ps else app_py' k' ps';
|
neuper@55448
|
688 |
in app_py' k p end;
|
wneuper@59414
|
689 |
fun get_py p =
|
wneuper@59414
|
690 |
let
|
wneuper@59414
|
691 |
fun extract_py (Ptyp (_, [py], _)) = py
|
wneuper@59414
|
692 |
| extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");
|
wneuper@59414
|
693 |
in app_py p extract_py end;
|
neuper@55448
|
694 |
|
neuper@55448
|
695 |
fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)
|
neuper@55448
|
696 |
let
|
neuper@55448
|
697 |
fun update_elem th (theID, fillpats) =
|
neuper@55437
|
698 |
let
|
neuper@55448
|
699 |
val hthm = get_py th theID theID
|
neuper@55448
|
700 |
val hthm' = update_hthm hthm fillpats
|
neuper@55448
|
701 |
handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
|
neuper@55448
|
702 |
in update_ptyps theID theID hthm' end
|
neuper@55448
|
703 |
in fold (update_elem th) fis end
|
neuper@55456
|
704 |
|
neuper@55456
|
705 |
(* group the theories defined in Isac, compare Build_Thydata:
|
neuper@55456
|
706 |
section "Get and group the theories defined in Isac" *)
|
wneuper@59397
|
707 |
fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
|
neuper@55456
|
708 |
let
|
wneuper@59415
|
709 |
val allthys = Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata")
|
neuper@55456
|
710 |
in
|
wneuper@59366
|
711 |
drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
|
neuper@55456
|
712 |
end
|
neuper@55456
|
713 |
fun knowthys () = (*["Isac", .., "Descript", "Delete"]*)
|
neuper@55456
|
714 |
let
|
neuper@55456
|
715 |
fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
|
neuper@55456
|
716 |
let
|
wneuper@59332
|
717 |
val allthys = filter_out (member Context.eq_thy
|
wneuper@59415
|
718 |
[(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret",
|
wneuper@59415
|
719 |
Rule.Thy_Info_get_theory "xmlsrc", Rule.Thy_Info_get_theory "Frontend"])
|
wneuper@59415
|
720 |
(Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata"))
|
neuper@55456
|
721 |
in
|
wneuper@59366
|
722 |
take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
|
neuper@55456
|
723 |
allthys)
|
neuper@55456
|
724 |
end
|
neuper@55456
|
725 |
val isacthys' = isacthys ()
|
wneuper@59415
|
726 |
val proglang_parent = Rule.Thy_Info_get_theory "ProgLang"
|
neuper@55456
|
727 |
in
|
wneuper@59332
|
728 |
take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
|
neuper@55456
|
729 |
end
|
wneuper@59414
|
730 |
|
neuper@55456
|
731 |
fun progthys () = (*["Isac", .., "Descript", "Delete"]*)
|
neuper@55456
|
732 |
let
|
neuper@55456
|
733 |
fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
|
wneuper@59415
|
734 |
let
|
wneuper@59332
|
735 |
val allthys = filter_out (member Context.eq_thy
|
wneuper@59415
|
736 |
[(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret",
|
wneuper@59415
|
737 |
Rule.Thy_Info_get_theory "xmlsrc", Rule.Thy_Info_get_theory "Frontend"])
|
wneuper@59415
|
738 |
(Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata"))
|
neuper@55456
|
739 |
in
|
wneuper@59366
|
740 |
take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
|
neuper@55456
|
741 |
allthys)
|
neuper@55456
|
742 |
end
|
neuper@55456
|
743 |
val isacthys' = isacthys ()
|
wneuper@59415
|
744 |
val proglang_parent = Rule.Thy_Info_get_theory "ProgLang"
|
neuper@55456
|
745 |
in
|
wneuper@59332
|
746 |
drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
|
neuper@55456
|
747 |
end
|
neuper@55456
|
748 |
|
neuper@55456
|
749 |
fun partID thy =
|
wneuper@59332
|
750 |
if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
|
wneuper@59332
|
751 |
else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
|
wneuper@59332
|
752 |
else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
|
wneuper@59415
|
753 |
else error ("closure of thys in Isac is broken by " ^ Rule.string_of_thy thy)
|
wneuper@59415
|
754 |
fun partID' thy' = partID (Rule.Thy_Info_get_theory thy')
|
wneuper@59405
|
755 |
|
neuper@38061
|
756 |
end (*struct*)
|
wneuper@59405
|
757 |
|