neuper@37906
|
1 |
(* the problems and methods as stored in hierarchies
|
neuper@37906
|
2 |
author Walther Neuper 1998
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
use"ME/ptyps.sml";
|
neuper@37906
|
6 |
use"ptyps.sml";
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
(*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
|
neuper@37928
|
10 |
val dsc_unknown = (term_of o the o (parseold @{theory Script}))
|
neuper@37906
|
11 |
"unknown::'a => unknow";
|
neuper@37906
|
12 |
(*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
|
neuper@37906
|
13 |
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
(*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
|
neuper@37906
|
16 |
|
neuper@37928
|
17 |
fun itm_2item thy (Cor ((d,ts),_)) =
|
neuper@37929
|
18 |
Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
|
neuper@37928
|
19 |
| itm_2item _ (Syn c) = SyntaxE c
|
neuper@37928
|
20 |
| itm_2item _ (Typ c) = TypeE c
|
neuper@37928
|
21 |
| itm_2item thy (Inc ((d,ts),_)) =
|
neuper@37929
|
22 |
Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
|
neuper@37928
|
23 |
| itm_2item thy (Sup (d,ts)) =
|
neuper@37929
|
24 |
Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
|
neuper@37928
|
25 |
| itm_2item _ (Mis (d,pid)) =
|
neuper@37929
|
26 |
Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
|
neuper@37929
|
27 |
Syntax.string_of_term (thy2ctxt' "Isac") pid);
|
neuper@37906
|
28 |
|
neuper@37906
|
29 |
|
neuper@37906
|
30 |
(* --- 8.3.00
|
neuper@37906
|
31 |
fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list)
|
neuper@37906
|
32 |
handle _ => error ("get_dsc_in not for "^sel);
|
neuper@37906
|
33 |
|
neuper@37906
|
34 |
fun dscs_in dscppc =
|
neuper@37906
|
35 |
((get_dsc_in dscppc "#Given") @
|
neuper@37906
|
36 |
(get_dsc_in dscppc "#Find") @
|
neuper@37906
|
37 |
(get_dsc_in dscppc "#Relate")):term list;
|
neuper@37906
|
38 |
|
neuper@37906
|
39 |
--- 26.1.88
|
neuper@37906
|
40 |
fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel)));
|
neuper@37906
|
41 |
fun get_dsc pblID =
|
neuper@37906
|
42 |
(get_dsc_of pblID "#Given") @
|
neuper@37906
|
43 |
(get_dsc_of pblID "#Find") @
|
neuper@37906
|
44 |
(get_dsc_of pblID "#Relate");
|
neuper@37906
|
45 |
--- *)
|
neuper@37906
|
46 |
|
neuper@37906
|
47 |
fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
|
neuper@37906
|
48 |
{Given=map f gi, Where=map f wh,
|
neuper@37906
|
49 |
Find=map f fi, With=map f wi, Relate=map f re}:'b ppc;
|
neuper@37906
|
50 |
fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
|
neuper@37906
|
51 |
{Given=f gi, Where=f wh,
|
neuper@37906
|
52 |
Find=f fi, With=f wi, Relate=f re}:'b ppc;
|
neuper@37906
|
53 |
|
neuper@37906
|
54 |
(*for ppc of changing type*)
|
neuper@37906
|
55 |
fun sel_ppc sel ppc =
|
neuper@37906
|
56 |
case sel of
|
neuper@37906
|
57 |
"#Given" => #Given (ppc:'a ppc)
|
neuper@37906
|
58 |
| "#Where" => #Where (ppc:'a ppc)
|
neuper@37906
|
59 |
| "#Find" => #Find (ppc:'a ppc)
|
neuper@37906
|
60 |
| "#With" => #With (ppc:'a ppc)
|
neuper@37906
|
61 |
| "#Relate" => #Relate (ppc:'a ppc)
|
neuper@37906
|
62 |
| _ => raise error ("sel_ppc tried to select by '"^sel^"'");
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
fun repl_sel_ppc sel
|
neuper@37906
|
65 |
({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
|
neuper@37906
|
66 |
case sel of
|
neuper@37906
|
67 |
"#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
|
neuper@37906
|
68 |
| "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
|
neuper@37906
|
69 |
| "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
|
neuper@37906
|
70 |
| "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
|
neuper@37906
|
71 |
| "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
|
neuper@37906
|
72 |
| _ => raise error ("repl_sel_ppc tried to select by '"^sel^"'");
|
neuper@37906
|
73 |
|
neuper@37906
|
74 |
fun add_sel_ppc thy sel
|
neuper@37906
|
75 |
({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
|
neuper@37906
|
76 |
case sel of
|
neuper@37906
|
77 |
"#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
|
neuper@37906
|
78 |
| "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}
|
neuper@37906
|
79 |
| "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
|
neuper@37906
|
80 |
| "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
|
neuper@37906
|
81 |
| "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
|
neuper@37906
|
82 |
| _ => raise error ("add_sel_ppc tried to select by '"^sel^"'");
|
neuper@37906
|
83 |
fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
|
neuper@37906
|
84 |
({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
|
neuper@37906
|
85 |
|
neuper@37906
|
86 |
(*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*)
|
neuper@37906
|
87 |
|
neuper@37906
|
88 |
|
neuper@37906
|
89 |
(*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*)
|
neuper@37906
|
90 |
|
neuper@37906
|
91 |
|
neuper@37906
|
92 |
|
neuper@37906
|
93 |
(*decompose a problem-type into description and identifier
|
neuper@37906
|
94 |
FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
|
neuper@37906
|
95 |
fun split_dsc thy t =
|
neuper@37906
|
96 |
(let val (hd,args) = strip_comb t
|
neuper@37906
|
97 |
in if is_dsc hd
|
neuper@37906
|
98 |
then (hd, args)
|
neuper@37906
|
99 |
else (e_term, [t]) (*??? 9.01 just copied*)
|
neuper@37906
|
100 |
end)
|
neuper@37906
|
101 |
handle _ => raise error ("split_dsc: called with "^
|
neuper@37929
|
102 |
(Syntax.string_of_term (thy2ctxt' "Isac") t));
|
neuper@37906
|
103 |
(*
|
neuper@37906
|
104 |
> val t1 = (term_of o the o (parse thy)) "errorBound err_";
|
neuper@37906
|
105 |
> split_dsc t1;
|
neuper@37906
|
106 |
(Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
|
neuper@37906
|
107 |
: term * term
|
neuper@37906
|
108 |
> val t3 = (term_of o the o (parse thy)) "valuesFor vs_";
|
neuper@37906
|
109 |
> split_dsc t3;
|
neuper@37906
|
110 |
(Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
|
neuper@37906
|
111 |
Free ("vs_","bool List.list")) : term * term*)
|
neuper@37906
|
112 |
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
|
neuper@37906
|
115 |
(*. take the first two return-values; for prep_ori .*)
|
neuper@37906
|
116 |
(*WN.13.5.03fun split_dts' thy t =
|
neuper@37906
|
117 |
let val (d, ts, _) = split_dts thy t
|
neuper@37906
|
118 |
in (d, ts) end;*)
|
neuper@37906
|
119 |
(*WN.8.12.03 quick for prep_ori'*)
|
neuper@37906
|
120 |
fun split_dsc' t =
|
neuper@37906
|
121 |
(let val dsc $ var = t
|
neuper@37906
|
122 |
in var end)
|
neuper@37906
|
123 |
handle _ => raise error ("split_dsc': called with "^term2str t);
|
neuper@37906
|
124 |
|
neuper@37906
|
125 |
(*9.3.00*)
|
neuper@37906
|
126 |
(* split a term into description and (id | structured variable)
|
neuper@37906
|
127 |
for pbt, met.ppc *)
|
neuper@37906
|
128 |
fun split_did t =
|
neuper@37906
|
129 |
(let val (hd,[arg]) = strip_comb t
|
neuper@37906
|
130 |
in (hd,arg) end)
|
neuper@37906
|
131 |
handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
|
neuper@37928
|
132 |
^(Syntax.string_of_term (thy2ctxt' "Script") t));
|
neuper@37906
|
133 |
|
neuper@37906
|
134 |
|
neuper@37906
|
135 |
|
neuper@37906
|
136 |
(*create output-string for itm_*)
|
neuper@37929
|
137 |
fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
|
neuper@37906
|
138 |
| itm_out thy (Syn c) = c
|
neuper@37906
|
139 |
| itm_out thy (Typ c) = c
|
neuper@37929
|
140 |
| itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
|
neuper@37929
|
141 |
| itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
|
neuper@37906
|
142 |
| itm_out thy (Mis (d,pid)) =
|
neuper@37929
|
143 |
Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
|
neuper@37929
|
144 |
Syntax.string_of_term (thy2ctxt' "Isac") pid;
|
neuper@37906
|
145 |
|
neuper@37906
|
146 |
(*22.11.00 unused
|
neuper@37906
|
147 |
fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
|
neuper@37906
|
148 |
|
neuper@37906
|
149 |
|
neuper@37906
|
150 |
(*--3.3.
|
neuper@37906
|
151 |
fun itms2dts itms =
|
neuper@37906
|
152 |
let
|
neuper@37906
|
153 |
fun coll itms' [] = itms'
|
neuper@37906
|
154 |
| coll itms' (i::itms) =
|
neuper@37906
|
155 |
case i of
|
neuper@37906
|
156 |
(Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms
|
neuper@37906
|
157 |
| (Syn c) => coll (itms' ) itms
|
neuper@37906
|
158 |
| (Typ c) => coll (itms' ) itms
|
neuper@37906
|
159 |
| (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms
|
neuper@37906
|
160 |
| (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms
|
neuper@37906
|
161 |
| (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms
|
neuper@37906
|
162 |
in coll [] itms end;
|
neuper@37906
|
163 |
*)
|
neuper@37906
|
164 |
(*--3.3.00
|
neuper@37906
|
165 |
fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
|
neuper@37929
|
166 |
Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
|
neuper@37906
|
167 |
| itm2item (_,_,_,_,Syn (c)) = SyntaxE c
|
neuper@37906
|
168 |
| itm2item (_,_,_,_,Typ (c)) = TypeE c
|
neuper@37906
|
169 |
| itm2item (_,_,_,_,Fal (d,ts)) =
|
neuper@37929
|
170 |
False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
|
neuper@37906
|
171 |
| itm2item (_,_,_,_,Inc (d,ts)) =
|
neuper@37929
|
172 |
Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
|
neuper@37906
|
173 |
| itm2item (_,_,_,_,Sup (d,ts)) =
|
neuper@37929
|
174 |
Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));
|
neuper@37906
|
175 |
*)
|
neuper@37906
|
176 |
|
neuper@37906
|
177 |
fun boolterm2item (true, term) = Correct (term2str term)
|
neuper@37906
|
178 |
| boolterm2item (false, term) = False (term2str term);
|
neuper@37906
|
179 |
|
neuper@37906
|
180 |
(* use"ME/modspec.sml";
|
neuper@37906
|
181 |
*)
|
neuper@37906
|
182 |
fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) =
|
neuper@37906
|
183 |
let
|
neuper@37906
|
184 |
fun coll ppc [] = ppc
|
neuper@37906
|
185 |
| coll ppc ((_,_,_,field,itm_)::itms) =
|
neuper@37906
|
186 |
coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
|
neuper@37906
|
187 |
val gfr = coll empty_ppc itms;
|
neuper@37906
|
188 |
in add_where gfr (map boolterm2item pre) end;
|
neuper@37906
|
189 |
(*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*)
|
neuper@37906
|
190 |
|
neuper@37906
|
191 |
(*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*)
|
neuper@37906
|
192 |
|
neuper@37906
|
193 |
(* --- 9.3.fun add_field dscs (d,ts) =
|
neuper@37906
|
194 |
if d mem (get_dsc_in dscs "#Given")
|
neuper@37906
|
195 |
then ("#Given",d,ts:term list)
|
neuper@37906
|
196 |
else if d mem (get_dsc_in dscs "#Find")
|
neuper@37906
|
197 |
then ("#Find",d,ts)
|
neuper@37906
|
198 |
else if d mem (get_dsc_in dscs "#Relate")
|
neuper@37906
|
199 |
then ("#Relate",d,ts)
|
neuper@37906
|
200 |
else ("#undef",d,ts);
|
neuper@37906
|
201 |
(* 28.1.00 raise error ("add_field: '"^
|
neuper@37929
|
202 |
(Syntax.string_of_term (thy2ctxt' "Isac") d)^
|
neuper@37906
|
203 |
"' not in ppc-description "); *)
|
neuper@37906
|
204 |
------9.3. *)
|
neuper@37906
|
205 |
|
neuper@37906
|
206 |
(* 9.3.00
|
neuper@37906
|
207 |
compare d and dsc in pbt and transfer field to pre-ori *)
|
neuper@37906
|
208 |
fun add_field thy pbt (d,ts) =
|
neuper@37906
|
209 |
let fun eq d pt = (d = (fst o snd) pt);
|
neuper@37906
|
210 |
in case filter (eq d) pbt of
|
neuper@37906
|
211 |
[(fi,(dsc,_))] => (fi,d,ts)
|
neuper@37906
|
212 |
| [] => ("#undef",d,ts) (*may come with met.ppc*)
|
neuper@37906
|
213 |
| _ => raise error ("add_field: "^
|
neuper@37929
|
214 |
(Syntax.string_of_term (thy2ctxt' "Isac") d)^
|
neuper@37906
|
215 |
" more than once in pbt")
|
neuper@37906
|
216 |
end;
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
(*. take over field from met.ppc at 'Specify_Method' into ori,
|
neuper@37906
|
219 |
i.e. also removes "#undef" fields .*)
|
neuper@37906
|
220 |
(* val (mpc, ori) = ((#ppc o get_met) mID, oris);
|
neuper@37906
|
221 |
*)
|
neuper@37906
|
222 |
fun add_field' thy mpc (ori:ori list) =
|
neuper@37906
|
223 |
let fun eq d pt = (d = (fst o snd) pt);
|
neuper@37906
|
224 |
fun repl mpc (i,v,_,d,ts) =
|
neuper@37906
|
225 |
case filter (eq d) mpc of
|
neuper@37906
|
226 |
[(fi,(dsc,_))] => [(i,v,fi,d,ts)]
|
neuper@37906
|
227 |
| [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
|
neuper@37906
|
228 |
(*raise error ("add_field': "^
|
neuper@37929
|
229 |
(Syntax.string_of_term (thy2ctxt' "Isac") d)^
|
neuper@37906
|
230 |
" not in met"*)
|
neuper@37906
|
231 |
| _ => raise error ("add_field': "^
|
neuper@37929
|
232 |
(Syntax.string_of_term (thy2ctxt' "Isac") d)^
|
neuper@37906
|
233 |
" more than once in met");
|
neuper@37906
|
234 |
in (flat ((map (repl mpc)) ori)):ori list end;
|
neuper@37906
|
235 |
|
neuper@37906
|
236 |
|
neuper@37906
|
237 |
(*.mark an element with the position within a plateau;
|
neuper@37906
|
238 |
a plateau with length 1 is marked with 0 .*)
|
neuper@37906
|
239 |
fun mark eq [] = raise error "mark []"
|
neuper@37906
|
240 |
| mark eq xs =
|
neuper@37906
|
241 |
let
|
neuper@37906
|
242 |
fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
|
neuper@37906
|
243 |
| mar xx eq (x::x'::xs) n =
|
neuper@37906
|
244 |
if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)
|
neuper@37906
|
245 |
else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1;
|
neuper@37906
|
246 |
in mar [] eq xs 1 end;
|
neuper@37906
|
247 |
(*
|
neuper@37906
|
248 |
> val xs = [1,1,1,2,4,4,5];
|
neuper@37906
|
249 |
> mark (op=) xs;
|
neuper@37906
|
250 |
val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
|
neuper@37906
|
251 |
*)
|
neuper@37906
|
252 |
|
neuper@37906
|
253 |
(*.assumes equal descriptions to be in adjacent 'plateaus',
|
neuper@37906
|
254 |
items at a certain position within the plateaus form a variant;
|
neuper@37906
|
255 |
length = 1 ... marked with 0: covers all variants .*)
|
neuper@37906
|
256 |
fun add_variants fdts =
|
neuper@37906
|
257 |
let
|
neuper@37906
|
258 |
fun eq (a,b) = curry op= (snd3 a) (snd3 b);
|
neuper@37906
|
259 |
in mark eq fdts end;
|
neuper@37906
|
260 |
|
neuper@37906
|
261 |
(* collect equal elements: the model for coll_variants *)
|
neuper@37906
|
262 |
fun coll eq xs =
|
neuper@37906
|
263 |
let
|
neuper@37906
|
264 |
fun col xs eq x [] = xs @ [x]
|
neuper@37906
|
265 |
| col xs eq x (y::ys) =
|
neuper@37906
|
266 |
if eq(x,y) then col xs eq x ys
|
neuper@37906
|
267 |
else col (xs @ [x]) eq y ys;
|
neuper@37906
|
268 |
in col [] eq (hd xs) xs end;
|
neuper@37906
|
269 |
(*
|
neuper@37906
|
270 |
> val xs = [1,1,1,2,4,4,4];
|
neuper@37906
|
271 |
> coll (op=) xs;
|
neuper@37906
|
272 |
val it = [1,2,4] : int list
|
neuper@37906
|
273 |
*)
|
neuper@37906
|
274 |
|
neuper@37906
|
275 |
fun max [] = raise error "max of []"
|
neuper@37906
|
276 |
| max (y::ys) =
|
neuper@37906
|
277 |
let fun mx x [] = x
|
neuper@37906
|
278 |
| mx x (y::ys) = if x < y then mx y ys else mx x ys;
|
neuper@37906
|
279 |
in mx y ys end;
|
neuper@37906
|
280 |
fun gen_max _ [] = raise error "gen_max of []"
|
neuper@37906
|
281 |
| gen_max ord (y::ys) =
|
neuper@37906
|
282 |
let fun mx x [] = x
|
neuper@37906
|
283 |
| mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
|
neuper@37906
|
284 |
in mx y ys end;
|
neuper@37906
|
285 |
|
neuper@37906
|
286 |
|
neuper@37906
|
287 |
|
neuper@37906
|
288 |
(* assumes *)
|
neuper@37906
|
289 |
fun coll_variants (((v,x)::vxs)) =
|
neuper@37906
|
290 |
let
|
neuper@37906
|
291 |
fun col xs (vs,x) [] = xs @ [(vs,x)]
|
neuper@37906
|
292 |
| col xs (vs,x) ((v',x')::vxs') =
|
neuper@37906
|
293 |
if x=x' then col xs (vs @ [v'], x') vxs'
|
neuper@37906
|
294 |
else col (xs @ [(vs,x)]) ([v'], x') vxs';
|
neuper@37906
|
295 |
in col [] ([v],x) vxs end;
|
neuper@37906
|
296 |
(* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
|
neuper@37906
|
297 |
> col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);
|
neuper@37906
|
298 |
val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *)
|
neuper@37906
|
299 |
|
neuper@37906
|
300 |
|
neuper@37906
|
301 |
fun replace_0 vm [0] = intsto vm
|
neuper@37906
|
302 |
| replace_0 vm vs = vs;
|
neuper@37906
|
303 |
|
neuper@37906
|
304 |
fun add_id [] = raise error "add_id []"
|
neuper@37906
|
305 |
| add_id xs =
|
neuper@37906
|
306 |
let fun add n [] = []
|
neuper@37906
|
307 |
| add n (x::xs) = (n,x) :: add (n+1) xs;
|
neuper@37906
|
308 |
in add 1 xs end;
|
neuper@37906
|
309 |
(*
|
neuper@37906
|
310 |
> val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
|
neuper@37906
|
311 |
> add_id xs;
|
neuper@37906
|
312 |
val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]
|
neuper@37906
|
313 |
*)
|
neuper@37906
|
314 |
|
neuper@37906
|
315 |
fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e);
|
neuper@37906
|
316 |
fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e);
|
neuper@37906
|
317 |
fun flat3 (a,(b,c)) = (a,b,c);
|
neuper@37906
|
318 |
(*
|
neuper@37906
|
319 |
val pI = pI';
|
neuper@37906
|
320 |
!pbts;
|
neuper@37906
|
321 |
*)
|
neuper@37906
|
322 |
(* in root (only!) fmz may be empty: fill with ..,dsc,[]
|
neuper@37906
|
323 |
fun init_ori fmz thy pI =
|
neuper@37906
|
324 |
if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*)
|
neuper@37906
|
325 |
else
|
neuper@37906
|
326 |
let
|
neuper@37906
|
327 |
val fds = map (cons2 (fst, fst o snd)) (get_pbt pI);
|
neuper@37906
|
328 |
val vfds = map ((pair [1]) o (rpair [])) fds;
|
neuper@37906
|
329 |
val ivfds = add_id vfds
|
neuper@37906
|
330 |
in (map flattup' ivfds):ori list end; 10.3.00---*)
|
neuper@37906
|
331 |
(* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];
|
neuper@37906
|
332 |
val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
|
neuper@37906
|
333 |
val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
|
neuper@37906
|
334 |
*)
|
neuper@37906
|
335 |
fun prep_ori [] _ _ = []
|
neuper@37906
|
336 |
| prep_ori fmz thy pbt =
|
neuper@37906
|
337 |
let
|
neuper@37906
|
338 |
val ctopts = map (parse thy) fmz
|
neuper@37906
|
339 |
val _= (*FIXME.WN060916 improve error report*)
|
neuper@37906
|
340 |
if null (filter is_none ctopts) then ()
|
neuper@37906
|
341 |
else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
|
neuper@37906
|
342 |
val dts = map ((split_dts thy) o term_of o the) ctopts
|
neuper@37906
|
343 |
val ori = map (add_field thy pbt) dts;
|
neuper@37906
|
344 |
(* val ori = map (flat3 o (pair "#undef")) dts; *)
|
neuper@37906
|
345 |
val ori' = add_variants ori;
|
neuper@37906
|
346 |
val maxv = max (map fst ori');
|
neuper@37906
|
347 |
val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv;
|
neuper@37906
|
348 |
val ori'' = coll_variants ori';
|
neuper@37906
|
349 |
val ori''' = map (apfst (replace_0 maxv)) ori'';
|
neuper@37906
|
350 |
val ori'''' = add_id ori'''
|
neuper@37906
|
351 |
in (map flattup ori''''):ori list end;
|
neuper@37906
|
352 |
|
neuper@37906
|
353 |
|
neuper@37906
|
354 |
(*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
(*.the pattern for an item of a problems model or a methods guard.*)
|
neuper@37906
|
357 |
type pat = (string * (*field*)
|
neuper@37906
|
358 |
(term * (*description*)
|
neuper@37906
|
359 |
term)) (*id | struct-var*);
|
neuper@37906
|
360 |
fun pat2str ((field, (dsc, id)):pat) =
|
neuper@37906
|
361 |
pair2str (field, pair2str (term2str dsc, term2str id));
|
neuper@37906
|
362 |
fun pats2str pats = (strs2str o (map pat2str)) pats;
|
neuper@37906
|
363 |
|
neuper@37906
|
364 |
(* data for methods stored in 'methods'-database *)
|
neuper@37906
|
365 |
type met =
|
neuper@37906
|
366 |
{guh : guh, (*unique within this isac-knowledge *)
|
neuper@37906
|
367 |
mathauthors: string list,(*copyright *)
|
neuper@37906
|
368 |
init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
|
neuper@37906
|
369 |
rew_ord' : rew_ord', (*for rules in Detail
|
neuper@37906
|
370 |
TODO.WN0509 store fun itself, see 'type pbt'*)
|
neuper@37906
|
371 |
erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
|
neuper@37906
|
372 |
instead erls in "fun prep_met" *)
|
neuper@37906
|
373 |
srls : rls, (*for evaluating list expressions in scr *)
|
neuper@37906
|
374 |
prls : rls, (*for evaluating predicates in modelpattern *)
|
neuper@37906
|
375 |
crls : rls, (*for check_elementwise, ie. formulae in calc.*)
|
neuper@37906
|
376 |
nrls : rls, (*canonical simplifier specific for this met *)
|
neuper@37906
|
377 |
calc : calc list, (*040207: <--- calclist' in fun prep_met *)
|
neuper@37906
|
378 |
(*branch : TransitiveB set in append_problem at generation ob pblobj
|
neuper@37906
|
379 |
FIXXXME.8.03: set branch from met in Apply_Method *)
|
neuper@37906
|
380 |
|
neuper@37906
|
381 |
(* compare type pbt:*)
|
neuper@37906
|
382 |
ppc: pat list,
|
neuper@37906
|
383 |
(*.items in given, find, relate;
|
neuper@37906
|
384 |
items (in "#Find") which need not occur in the arg-list of a SubProblem
|
neuper@37906
|
385 |
are 'copy-named' with an identifier "*_!_".
|
neuper@37906
|
386 |
copy-named items are 'generating' if they are NOT "*___"
|
neuper@37906
|
387 |
see ME/calchead.sml 'fun is_copy_named'.*)
|
neuper@37906
|
388 |
pre: term list, (*preconditions in where*)
|
neuper@37906
|
389 |
(*script*)
|
neuper@37906
|
390 |
scr: scr (*prep_met requires either script or string "empty_script"*)
|
neuper@37906
|
391 |
};
|
neuper@37906
|
392 |
(* ------- template ------------------------------------------------------
|
neuper@37906
|
393 |
store_met
|
neuper@37906
|
394 |
(prep_met *.thy
|
neuper@37906
|
395 |
([(*"EqSystem","normalize"*)],
|
neuper@37906
|
396 |
[("#Given" ,[ (*"equalities es_", "solveForVars vs_"*)]),
|
neuper@37906
|
397 |
("#Find" ,[ (*dont forget typing non-reals *)]),
|
neuper@37906
|
398 |
("#Relate",[])(*may be omitted *) ],
|
neuper@37906
|
399 |
{calc = [], (*filled autom. in prep_met *)
|
neuper@37906
|
400 |
crls = Erls, (*for check_elementwise *)
|
neuper@37906
|
401 |
prls = Erls, (*for evaluating preds in guard *)
|
neuper@37906
|
402 |
nrls = Erls, (*can.simplifier for all formulae*)
|
neuper@37906
|
403 |
rew_ord'="tless_true", (*for rules in Detail *)
|
neuper@37906
|
404 |
rls' = Erls, (*erls, the eval_rls for cond. in rules*)
|
neuper@37906
|
405 |
srls = Erls}, (*for evaluating list expr in scr*)
|
neuper@37906
|
406 |
"empty_script"
|
neuper@37906
|
407 |
));
|
neuper@37906
|
408 |
---------- template ----------------------------------------------------*)
|
neuper@37906
|
409 |
val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
|
neuper@37906
|
410 |
rew_ord' = "e_rew_ord'": rew_ord',
|
neuper@37906
|
411 |
erls = e_rls, srls = e_rls, prls = e_rls,
|
neuper@37906
|
412 |
calc = [], crls = e_rls, nrls = e_rls,
|
neuper@37906
|
413 |
(*asm_thm = []: thm' list,
|
neuper@37906
|
414 |
asm_rls = []: rls' list,*)
|
neuper@37906
|
415 |
ppc = []: (string * (term * term)) list,
|
neuper@37906
|
416 |
pre = []: term list,
|
neuper@37906
|
417 |
scr = EmptyScr: scr}:met;
|
neuper@37906
|
418 |
|
neuper@37906
|
419 |
|
neuper@37906
|
420 |
(** problem-types stored in format for usage in specify **)
|
neuper@37906
|
421 |
(*25.8.01 ----
|
neuper@37906
|
422 |
val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
|
neuper@37906
|
423 |
(term * (* description *)
|
neuper@37906
|
424 |
term)) (* id | struct-var *)
|
neuper@37906
|
425 |
list)
|
neuper@37906
|
426 |
) list);*)
|
neuper@37906
|
427 |
|
neuper@37906
|
428 |
(*deprecated due to 'type pat'*)
|
neuper@37906
|
429 |
type pbt_ = (string * (* field "#Given",..*)
|
neuper@37906
|
430 |
(term * (* description *)
|
neuper@37906
|
431 |
term)); (* id | struct-var *)
|
neuper@37906
|
432 |
val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_;
|
neuper@37906
|
433 |
type pbt =
|
neuper@37906
|
434 |
{guh : guh, (*unique within this isac-knowledge*)
|
neuper@37906
|
435 |
mathauthors: string list, (*copyright*)
|
neuper@37906
|
436 |
init : pblID, (*to start refinement with*)
|
neuper@37906
|
437 |
thy : theory, (* which allows to compile that pbt
|
neuper@37906
|
438 |
TODO: search generalized for subthy (ref.p.69*)
|
neuper@37906
|
439 |
(*^^^ WN050912 NOT used during application of the problem,
|
neuper@37906
|
440 |
because applied terms may be from 'subthy' as well as from super;
|
neuper@37906
|
441 |
thus we take 'maxthy'; see match_ags !*)
|
neuper@37906
|
442 |
cas : term option,(*'CAS-command'*)
|
neuper@37906
|
443 |
prls : rls, (* for preds in where_*)
|
neuper@37906
|
444 |
where_: term list, (* where - predicates*)
|
neuper@37906
|
445 |
ppc : pat list,
|
neuper@37906
|
446 |
(*this is the model-pattern;
|
neuper@37906
|
447 |
it contains "#Given","#Where","#Find","#Relate"-patterns*)
|
neuper@37906
|
448 |
met : metID list}; (* methods solving the pbt*)
|
neuper@37928
|
449 |
val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure",
|
neuper@37926
|
450 |
cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
|
neuper@37906
|
451 |
fun pbt2 (str, (t1, t2)) =
|
neuper@37906
|
452 |
pair2str (str, pair2str (term2str t1, term2str t2));
|
neuper@37906
|
453 |
fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;
|
neuper@37906
|
454 |
|
neuper@37906
|
455 |
|
neuper@37906
|
456 |
val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]);
|
neuper@37906
|
457 |
val e_Mets = Ptyp ("e_metID",[e_met],[]);
|
neuper@37906
|
458 |
|
neuper@37906
|
459 |
type ptyps = (pbt ptyp) list;
|
neuper@37906
|
460 |
val ptyps = ref ([e_Ptyp]:ptyps);
|
neuper@37906
|
461 |
|
neuper@37906
|
462 |
type mets = (met ptyp) list;
|
neuper@37906
|
463 |
val mets = ref ([e_Mets]:mets);
|
neuper@37906
|
464 |
|
neuper@37906
|
465 |
|
neuper@37906
|
466 |
(**+ breadth-first search on hierarchy of problem-types +**)
|
neuper@37906
|
467 |
|
neuper@37906
|
468 |
type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)
|
neuper@37906
|
469 |
(* eg. ["equations","univariate","normalize"] while
|
neuper@37906
|
470 |
["normalize","univariate","equations"] is the related pblID
|
neuper@37906
|
471 |
WN.24.4.03: also used for metID*)
|
neuper@37906
|
472 |
|
neuper@37906
|
473 |
fun get_py thy d _ [] =
|
neuper@37906
|
474 |
error ("get_pbt not found: "^(strs2str d))
|
neuper@37906
|
475 |
| get_py thy d [k] ((Ptyp (k',[py],_))::pys) =
|
neuper@37906
|
476 |
if k=k' then py
|
neuper@37906
|
477 |
else get_py thy d ([k]:pblRD) pys
|
neuper@37906
|
478 |
| get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') =
|
neuper@37906
|
479 |
if k=k' then get_py thy d ks pys
|
neuper@37906
|
480 |
else get_py thy d (k::ks) pys';
|
neuper@37906
|
481 |
(*> ptyps:=
|
neuper@37906
|
482 |
[Ptyp ("1",[("ptyp 1",([],[]))],
|
neuper@37906
|
483 |
[Ptyp ("11",[("ptyp 11",([],[]))],
|
neuper@37906
|
484 |
[])
|
neuper@37906
|
485 |
]),
|
neuper@37906
|
486 |
Ptyp ("2",[("ptyp 2",([],[]))],
|
neuper@37906
|
487 |
[Ptyp ("21",[("ptyp 21",([],[]))],
|
neuper@37906
|
488 |
[])
|
neuper@37906
|
489 |
])
|
neuper@37906
|
490 |
];
|
neuper@37906
|
491 |
> get_py SqRoot.thy ["1"] ["1"] (!ptyps);
|
neuper@37906
|
492 |
> get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);
|
neuper@37906
|
493 |
_REVERSE_ .......... !!!!!!!!!!*)
|
neuper@37906
|
494 |
|
neuper@37906
|
495 |
(*TODO: search generalized for subthy*)
|
neuper@37906
|
496 |
fun get_pbt (pblID:pblID) =
|
neuper@37906
|
497 |
let val pblRD = rev pblID;
|
neuper@37928
|
498 |
in get_py (theory "Pure") pblID pblRD (!ptyps) end;
|
neuper@37906
|
499 |
(* get_pbt thy ["1"];
|
neuper@37906
|
500 |
get_pbt thy ["21","2"];
|
neuper@37906
|
501 |
*)
|
neuper@37906
|
502 |
|
neuper@37906
|
503 |
(*TODO: throws exn 'get_pbt not found: ' ... confusing !!
|
neuper@37906
|
504 |
take 'ketype' as an argument !!!!!*)
|
neuper@37928
|
505 |
fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets);
|
neuper@37928
|
506 |
fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier);
|
neuper@37906
|
507 |
|
neuper@37906
|
508 |
|
neuper@37906
|
509 |
|
neuper@37906
|
510 |
fun del_eq k ptyps =
|
neuper@37906
|
511 |
let fun del k ptyps [] = ptyps
|
neuper@37906
|
512 |
| del k ptyps ((Ptyp (k', [p], ps))::pys) =
|
neuper@37906
|
513 |
if k=k' then del k ptyps pys
|
neuper@37906
|
514 |
else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
|
neuper@37906
|
515 |
in del k [] ptyps end;
|
neuper@37906
|
516 |
|
neuper@37906
|
517 |
fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])]
|
neuper@37906
|
518 |
|
neuper@37906
|
519 |
| insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
|
neuper@37906
|
520 |
((*writeln("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
|
neuper@37906
|
521 |
if k=k'
|
neuper@37906
|
522 |
then ((Ptyp (k', [pbt], ps))::pys)
|
neuper@37906
|
523 |
else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
|
neuper@37906
|
524 |
((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
|
neuper@37906
|
525 |
)
|
neuper@37906
|
526 |
| insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
|
neuper@37906
|
527 |
((*writeln("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
|
neuper@37906
|
528 |
if k=k'
|
neuper@37906
|
529 |
then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
|
neuper@37906
|
530 |
else
|
neuper@37906
|
531 |
if length pys = 0
|
neuper@37906
|
532 |
then error ("insert: not found "^(strs2str (d:pblID)))
|
neuper@37906
|
533 |
else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
|
neuper@37906
|
534 |
);
|
neuper@37906
|
535 |
|
neuper@37906
|
536 |
|
neuper@37906
|
537 |
fun coll_pblguhs pbls =
|
neuper@37906
|
538 |
let fun node coll (Ptyp (_,[n],ns)) =
|
neuper@37906
|
539 |
[(#guh : pbt -> guh) n] @ (nodes coll ns)
|
neuper@37906
|
540 |
and nodes coll [] = coll
|
neuper@37906
|
541 |
| nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
|
neuper@37906
|
542 |
in nodes [] pbls end;
|
neuper@37906
|
543 |
fun coll_metguhs mets =
|
neuper@37906
|
544 |
let fun node coll (Ptyp (_,[n],ns)) =
|
neuper@37906
|
545 |
[(#guh : met -> guh) n]
|
neuper@37906
|
546 |
and nodes coll [] = coll
|
neuper@37906
|
547 |
| nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
|
neuper@37906
|
548 |
in nodes [] mets end;
|
neuper@37906
|
549 |
|
neuper@37906
|
550 |
(*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
|
neuper@37906
|
551 |
fun guh2kestoreID (guh:guh) =
|
neuper@37906
|
552 |
case (implode o (take_fromto 1 4) o explode) guh of
|
neuper@37906
|
553 |
"pbl_" =>
|
neuper@37906
|
554 |
let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
|
neuper@37906
|
555 |
if gu = guh
|
neuper@37926
|
556 |
then SOME ((ids@[id]) : kestoreID)
|
neuper@37906
|
557 |
else nodes (ids@[id]) gu ns
|
neuper@37926
|
558 |
and nodes _ _ [] = NONE
|
neuper@37906
|
559 |
| nodes ids gu (n::ns) =
|
neuper@37926
|
560 |
case node ids gu n of SOME id => SOME id
|
neuper@37926
|
561 |
| NONE => nodes ids gu ns
|
neuper@37906
|
562 |
in case nodes [] guh (!ptyps) of
|
neuper@37926
|
563 |
SOME id => rev id
|
neuper@37926
|
564 |
| NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
|
neuper@37906
|
565 |
"not found in (!ptyps)")
|
neuper@37906
|
566 |
end
|
neuper@37906
|
567 |
| "met_" =>
|
neuper@37906
|
568 |
let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =
|
neuper@37906
|
569 |
if gu = guh
|
neuper@37926
|
570 |
then SOME ((ids@[id]) : kestoreID)
|
neuper@37906
|
571 |
else nodes (ids@[id]) gu ns
|
neuper@37926
|
572 |
and nodes _ _ [] = NONE
|
neuper@37906
|
573 |
| nodes ids gu (n::ns) =
|
neuper@37926
|
574 |
case node ids gu n of SOME id => SOME id
|
neuper@37926
|
575 |
| NONE => nodes ids gu ns
|
neuper@37906
|
576 |
in case nodes [] guh (!mets) of
|
neuper@37926
|
577 |
SOME id => id
|
neuper@37926
|
578 |
| NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
|
neuper@37906
|
579 |
"not found in (!mets)") end
|
neuper@37906
|
580 |
| _ => error ("guh2kestoreID called with '" ^ guh ^ "'");
|
neuper@37906
|
581 |
(*> guh2kestoreID "pbl_equ_univ_lin";
|
neuper@37906
|
582 |
val it = ["linear", "univariate", "equation"] : string list*)
|
neuper@37906
|
583 |
|
neuper@37906
|
584 |
|
neuper@37906
|
585 |
fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
|
neuper@37928
|
586 |
if member op = (coll_pblguhs pbls) guh
|
neuper@37906
|
587 |
then error ("check_guh_unique failed with '"^guh^"';\n"^
|
neuper@37906
|
588 |
"use 'sort_pblguhs()' for a list of guhs;\n"^
|
neuper@37906
|
589 |
"consider setting 'check_guhs_unique := false'")
|
neuper@37906
|
590 |
else ();
|
neuper@37906
|
591 |
(* val (guh, mets) = ("met_test", !mets);
|
neuper@37906
|
592 |
*)
|
neuper@37906
|
593 |
fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
|
neuper@37928
|
594 |
if member op = (coll_metguhs mets) guh
|
neuper@37906
|
595 |
then error ("check_guh_unique failed with '"^guh^"';\n"^
|
neuper@37906
|
596 |
"use 'sort_metguhs()' for a list of guhs;\n"^
|
neuper@37906
|
597 |
"consider setting 'check_guhs_unique := false'")
|
neuper@37906
|
598 |
else ();
|
neuper@37906
|
599 |
|
neuper@37906
|
600 |
|
neuper@37906
|
601 |
|
neuper@37906
|
602 |
(*.the pblID has the leaf-element as first; better readability achieved;.*)
|
neuper@37906
|
603 |
fun store_pbt (pbt as {guh,...}, pblID) =
|
neuper@37906
|
604 |
(if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else ();
|
neuper@37906
|
605 |
ptyps:= insrt pblID pbt (rev pblID) (!ptyps));
|
neuper@37906
|
606 |
|
neuper@37906
|
607 |
(*.the metID has the root-element as first; compare 'fun store_pbt'.*)
|
neuper@37906
|
608 |
(* val (met as {guh,...}, metID) =
|
neuper@37906
|
609 |
((prep_met EqSystem.thy "met_eqsys" [] e_metID
|
neuper@37906
|
610 |
(["EqSystem"],
|
neuper@37906
|
611 |
[],
|
neuper@37906
|
612 |
{rew_ord'="tless_true", rls' = Erls, calc = [],
|
neuper@37906
|
613 |
srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
|
neuper@37906
|
614 |
"empty_script"
|
neuper@37906
|
615 |
)));
|
neuper@37906
|
616 |
*)
|
neuper@37906
|
617 |
fun store_met (met as {guh,...}, metID) =
|
neuper@37906
|
618 |
(if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
|
neuper@37906
|
619 |
mets:= insrt metID met metID (!mets));
|
neuper@37906
|
620 |
|
neuper@37906
|
621 |
|
neuper@37906
|
622 |
(*. prepare problem-types before storing in pbltypes;
|
neuper@37906
|
623 |
dont forget to 'check_guh_unique' before ins.*)
|
neuper@37906
|
624 |
fun prep_pbt thy guh maa init
|
neuper@37906
|
625 |
(pblID, dsc_dats: (string * (string list)) list,
|
neuper@37906
|
626 |
ev:rls, ca: string option, metIDs:metID list) =
|
neuper@37906
|
627 |
(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
|
neuper@37906
|
628 |
ev:rls, ca: string option, metIDs:metID list)) =
|
neuper@37906
|
629 |
((EqSystem.thy, (["system"],
|
neuper@37906
|
630 |
[("#Given" ,["equalities es_", "solveForVars vs_"]),
|
neuper@37906
|
631 |
("#Find" ,["solution ss___"](*___ is copy-named*))
|
neuper@37906
|
632 |
],
|
neuper@37906
|
633 |
append_rls "e_rls" e_rls [(*for preds in where_*)],
|
neuper@37926
|
634 |
SOME "solveSystem es_ vs_",
|
neuper@37906
|
635 |
[])));
|
neuper@37906
|
636 |
*)
|
neuper@37906
|
637 |
let fun eq f (f', _) = f = f';
|
neuper@37906
|
638 |
val gi = filter (eq "#Given") dsc_dats;
|
neuper@37906
|
639 |
(*val gi = [("#Given",["equality e_","solveFor v_"])]
|
neuper@37906
|
640 |
: (string * string list) list*)
|
neuper@37906
|
641 |
val gi = (case gi of
|
neuper@37906
|
642 |
[] => []
|
neuper@37906
|
643 |
| ((_,gi')::[]) =>
|
neuper@37906
|
644 |
((map (split_did o term_of o the o (parse thy)) gi')
|
neuper@37906
|
645 |
handle _ => error
|
neuper@37906
|
646 |
("prep_pbt: syntax error in '#Given' of "^
|
neuper@37906
|
647 |
(strs2str pblID)))
|
neuper@37906
|
648 |
| _ =>
|
neuper@37906
|
649 |
(error ("prep_pbt: more than one '#Given' in "^
|
neuper@37906
|
650 |
(strs2str pblID))));
|
neuper@37906
|
651 |
(*val gi =
|
neuper@37906
|
652 |
[(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")),
|
neuper@37906
|
653 |
(Const ("Descript.solveFor","RealDef.real => Tools.una"),
|
neuper@37906
|
654 |
Free ("v_","RealDef.real"))] : (term * term) list *)
|
neuper@37906
|
655 |
val gi = map (pair "#Given") gi;
|
neuper@37906
|
656 |
(*val gi =
|
neuper@37906
|
657 |
[("#Given",
|
neuper@37906
|
658 |
(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))),
|
neuper@37906
|
659 |
("#Given",
|
neuper@37906
|
660 |
(Const ("Descript.solveFor","RealDef.real => Tools.una"),
|
neuper@37906
|
661 |
Free ("v_","RealDef.real")))] : (string * (term * term)) list*)
|
neuper@37906
|
662 |
|
neuper@37906
|
663 |
val fi = filter (eq "#Find") dsc_dats;
|
neuper@37906
|
664 |
val fi = (case fi of
|
neuper@37906
|
665 |
[] => [](*28.8.01: ["tool"] ...// raise error
|
neuper@37906
|
666 |
("prep_pbt: no '#Find' in "^(strs2str pblID))*)
|
neuper@37906
|
667 |
(* val ((_,fi')::[]) = fi;
|
neuper@37906
|
668 |
*)
|
neuper@37906
|
669 |
| ((_,fi')::[]) =>
|
neuper@37906
|
670 |
((map (split_did o term_of o the o (parse thy)) fi')
|
neuper@37906
|
671 |
handle _ => raise error
|
neuper@37906
|
672 |
("prep_pbt: syntax error in '#Find' of "^
|
neuper@37906
|
673 |
(strs2str pblID)))
|
neuper@37906
|
674 |
| _ =>
|
neuper@37906
|
675 |
(raise error ("prep_pbt: more than one '#Find' in "^
|
neuper@37906
|
676 |
(strs2str pblID))));
|
neuper@37906
|
677 |
val fi = map (pair "#Find") fi;
|
neuper@37906
|
678 |
|
neuper@37906
|
679 |
val re = filter (eq "#Relate") dsc_dats;
|
neuper@37906
|
680 |
val re = (case re of
|
neuper@37906
|
681 |
[] => []
|
neuper@37906
|
682 |
| ((_,re')::[]) =>
|
neuper@37906
|
683 |
((map (split_did o term_of o the o (parse thy)) re')
|
neuper@37906
|
684 |
handle _ => raise error
|
neuper@37906
|
685 |
("prep_pbt: syntax error in '#Relate' of "^
|
neuper@37906
|
686 |
(strs2str pblID)))
|
neuper@37906
|
687 |
| _ =>
|
neuper@37906
|
688 |
(raise error ("prep_pbt: more than one '#Relate' in "^
|
neuper@37906
|
689 |
(strs2str pblID))));
|
neuper@37906
|
690 |
val re = map (pair "#Relate") re;
|
neuper@37906
|
691 |
|
neuper@37906
|
692 |
val wh = filter (eq "#Where") dsc_dats;
|
neuper@37906
|
693 |
val wh = (case wh of
|
neuper@37906
|
694 |
[] => []
|
neuper@37906
|
695 |
| ((_,wh')::[]) =>
|
neuper@37977
|
696 |
((map (parse_patt thy) wh')
|
neuper@37977
|
697 |
handle _ => raise error
|
neuper@37906
|
698 |
("prep_pbt: syntax error in '#Where' of "^
|
neuper@37906
|
699 |
(strs2str pblID)))
|
neuper@37906
|
700 |
| _ =>
|
neuper@37906
|
701 |
(raise error ("prep_pbt: more than one '#Where' in "^
|
neuper@37906
|
702 |
(strs2str pblID))));
|
neuper@37906
|
703 |
in ({guh=guh,mathauthors=maa,init=init,
|
neuper@37926
|
704 |
thy=thy,cas= case ca of NONE => NONE
|
neuper@37926
|
705 |
| SOME s =>
|
neuper@37926
|
706 |
SOME ((term_of o the o (parse thy)) s),
|
neuper@37906
|
707 |
prls=ev,where_=wh,ppc= gi @ fi @ re,
|
neuper@37906
|
708 |
met=metIDs}, pblID):pbt * pblID end;
|
neuper@37906
|
709 |
(* prep_pbt thy (pblID, dsc_dats, metIDs);
|
neuper@37906
|
710 |
val it =
|
neuper@37906
|
711 |
({met=[],
|
neuper@37906
|
712 |
ppc=[("#Given",(Const (#,#),Free (#,#))),
|
neuper@37906
|
713 |
("#Given",(Const (#,#),Free (#,#))),
|
neuper@37906
|
714 |
("#Find",(Const (#,#),Free (#,#)))],
|
neuper@37906
|
715 |
thy={ProtoPure, ..., Atools, RatArith},
|
neuper@37906
|
716 |
where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $
|
neuper@37906
|
717 |
Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *)
|
neuper@37906
|
718 |
|
neuper@37906
|
719 |
|
neuper@37906
|
720 |
|
neuper@37906
|
721 |
|
neuper@37906
|
722 |
(*. prepare met for storage analogous to pbt .*)
|
neuper@37906
|
723 |
fun prep_met thy guh maa init
|
neuper@37906
|
724 |
(metID, ppc: (string * string list) list (*'#Where' -> #pre*),
|
neuper@37906
|
725 |
{rew_ord'=ro, rls'=rls, srls=srls, prls=prls,
|
neuper@37906
|
726 |
calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
|
neuper@37906
|
727 |
crls=cr, nrls=nr}, scr) =
|
neuper@37906
|
728 |
let fun eq f (f', _) = f = f';
|
neuper@37906
|
729 |
(*val thy = (assoc_thy o fst) metID*)
|
neuper@37906
|
730 |
val gi = filter (eq "#Given") ppc;
|
neuper@37906
|
731 |
val gi = (case gi of
|
neuper@37906
|
732 |
[] => []
|
neuper@37906
|
733 |
| ((_,gi')::[]) =>
|
neuper@37906
|
734 |
((map (split_did o term_of o the o (parse thy)) gi')
|
neuper@37906
|
735 |
handle _ => raise error
|
neuper@37906
|
736 |
("prep_pbt: syntax error in '#Given' of "^
|
neuper@37906
|
737 |
(strs2str metID)))
|
neuper@37906
|
738 |
| _ =>
|
neuper@37906
|
739 |
(raise error ("prep_pbt: more than one '#Given' in "^
|
neuper@37906
|
740 |
(strs2str metID))));
|
neuper@37906
|
741 |
val gi = map (pair "#Given") gi;
|
neuper@37906
|
742 |
|
neuper@37906
|
743 |
val fi = filter (eq "#Find") ppc;
|
neuper@37906
|
744 |
val fi = (case fi of
|
neuper@37906
|
745 |
[] => [](*28.8.01: ["tool"] ...// raise error
|
neuper@37906
|
746 |
("prep_pbt: no '#Find' in "^(strs2str metID))*)
|
neuper@37906
|
747 |
| ((_,fi')::[]) =>
|
neuper@37906
|
748 |
((map (split_did o term_of o the o (parse thy)) fi')
|
neuper@37906
|
749 |
handle _ => raise error
|
neuper@37906
|
750 |
("prep_pbt: syntax error in '#Find' of "^
|
neuper@37906
|
751 |
(strs2str metID)))
|
neuper@37906
|
752 |
| _ =>
|
neuper@37906
|
753 |
(raise error ("prep_pbt: more than one '#Find' in "^
|
neuper@37906
|
754 |
(strs2str metID))));
|
neuper@37906
|
755 |
val fi = map (pair "#Find") fi;
|
neuper@37906
|
756 |
|
neuper@37906
|
757 |
val re = filter (eq "#Relate") ppc;
|
neuper@37906
|
758 |
val re = (case re of
|
neuper@37906
|
759 |
[] => []
|
neuper@37906
|
760 |
| ((_,re')::[]) =>
|
neuper@37906
|
761 |
((map (split_did o term_of o the o (parse thy)) re')
|
neuper@37906
|
762 |
handle _ => raise error
|
neuper@37906
|
763 |
("prep_pbt: syntax error in '#Relate' of "^
|
neuper@37906
|
764 |
(strs2str metID)))
|
neuper@37906
|
765 |
| _ =>
|
neuper@37906
|
766 |
(raise error ("prep_pbt: more than one '#Relate' in "^
|
neuper@37906
|
767 |
(strs2str metID))));
|
neuper@37906
|
768 |
val re = map (pair "#Relate") re;
|
neuper@37906
|
769 |
|
neuper@37906
|
770 |
val wh = filter (eq "#Where") ppc;
|
neuper@37906
|
771 |
val wh = (case wh of
|
neuper@37906
|
772 |
[] => []
|
neuper@37906
|
773 |
| ((_,wh')::[]) =>
|
neuper@37977
|
774 |
((map (parse_patt thy) wh')
|
neuper@37906
|
775 |
handle _ => raise error
|
neuper@37906
|
776 |
("prep_pbt: syntax error in '#Where' of "^
|
neuper@37906
|
777 |
(strs2str metID)))
|
neuper@37906
|
778 |
| _ =>
|
neuper@37906
|
779 |
(raise error ("prep_pbt: more than one '#Where' in "^
|
neuper@37906
|
780 |
(strs2str metID))));
|
neuper@37906
|
781 |
val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
|
neuper@37906
|
782 |
in ({guh=guh,mathauthors=maa,init=init,
|
neuper@37906
|
783 |
ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
|
neuper@37906
|
784 |
calc = if scr = "empty_script" then []
|
neuper@37906
|
785 |
else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
|
neuper@37906
|
786 |
(filter is_calc) o stacpbls) sc,
|
neuper@37906
|
787 |
crls=cr, nrls=nr, scr=Script sc}:met,
|
neuper@37906
|
788 |
metID:metID)
|
neuper@37906
|
789 |
end;
|
neuper@37906
|
790 |
|
neuper@37906
|
791 |
|
neuper@37906
|
792 |
(**. get pblIDs of all entries in mat3D .**)
|
neuper@37906
|
793 |
|
neuper@37906
|
794 |
|
neuper@37906
|
795 |
fun format_pblID strl = enclose " [" "]" (commas_quote strl);
|
neuper@37906
|
796 |
fun format_pblIDl strll = enclose "[\n" "\n]\n"
|
neuper@37906
|
797 |
(space_implode ",\n" (map format_pblID strll));
|
neuper@37906
|
798 |
|
neuper@37906
|
799 |
fun scan _ [] = [] (* no base case, for empty doms only *)
|
neuper@37906
|
800 |
| scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]]
|
neuper@37906
|
801 |
| scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl
|
neuper@37906
|
802 |
| scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
|
neuper@37906
|
803 |
| scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
|
neuper@37906
|
804 |
|
neuper@37906
|
805 |
fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);
|
neuper@37906
|
806 |
(* ptyps:=[];
|
neuper@37906
|
807 |
show_ptyps();
|
neuper@37906
|
808 |
*)
|
neuper@37906
|
809 |
fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);
|
neuper@37906
|
810 |
|
neuper@37906
|
811 |
|
neuper@37906
|
812 |
|
neuper@37906
|
813 |
(*vvvvv---------- preparational work 8.01. UNUSED *)
|
neuper@37906
|
814 |
(**+ instantiate a problem-type +**)
|
neuper@37906
|
815 |
|
neuper@37906
|
816 |
(*+ transform oris +*)
|
neuper@37906
|
817 |
|
neuper@37928
|
818 |
fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs;
|
neuper@37906
|
819 |
(*> coll_vats [11,22] (hd oris);
|
neuper@37906
|
820 |
val it = [22,11,1,2,3] : int list
|
neuper@37906
|
821 |
|
neuper@37906
|
822 |
> foldl coll_vats ([],oris);
|
neuper@37906
|
823 |
val it = [1,2,3] : int list
|
neuper@37906
|
824 |
|
neuper@37906
|
825 |
> val i=1;
|
neuper@37906
|
826 |
> filter ((curry (op mem) i) o #2) oris;
|
neuper@37906
|
827 |
val it =
|
neuper@37906
|
828 |
[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
|
neuper@37906
|
829 |
(2,[1,2,3],"#Find",Const (#,#),[Free #]),
|
neuper@37906
|
830 |
(3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
831 |
(4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
832 |
(6,[1],"#undef",Const (#,#),[Free #]),
|
neuper@37906
|
833 |
(9,[1,2],"#undef",Const (#,#),[# $ #]),
|
neuper@37906
|
834 |
(11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
|
neuper@37906
|
835 |
|
neuper@37936
|
836 |
local infix mem; (*from Isabelle2002*)
|
neuper@37928
|
837 |
fun x mem [] = false
|
neuper@37928
|
838 |
| x mem (y :: ys) = x = y orelse x mem ys;
|
neuper@37928
|
839 |
in
|
neuper@37928
|
840 |
fun filter_vat oris i =
|
neuper@37928
|
841 |
filter ((curry (op mem) i) o (#2 : ori -> int list)) oris;
|
neuper@37928
|
842 |
end;
|
neuper@37906
|
843 |
(*> map (filter_vat oris) [1,2,3];
|
neuper@37906
|
844 |
val it =
|
neuper@37906
|
845 |
[[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
|
neuper@37906
|
846 |
(2,[1,2,3],"#Find",Const (#,#),[Free #]),
|
neuper@37906
|
847 |
(3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
848 |
(4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
849 |
(6,[1],"#undef",Const (#,#),[Free #]),
|
neuper@37906
|
850 |
(9,[1,2],"#undef",Const (#,#),[# $ #]),
|
neuper@37906
|
851 |
(11,[1,2,3],"#undef",Const (#,#),[# $ #])],
|
neuper@37906
|
852 |
[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
|
neuper@37906
|
853 |
(2,[1,2,3],"#Find",Const (#,#),[Free #]),
|
neuper@37906
|
854 |
(3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
855 |
(4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
856 |
(7,[2],"#undef",Const (#,#),[Free #]),
|
neuper@37906
|
857 |
(9,[1,2],"#undef",Const (#,#),[# $ #]),
|
neuper@37906
|
858 |
(11,[1,2,3],"#undef",Const (#,#),[# $ #])],
|
neuper@37906
|
859 |
[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
|
neuper@37906
|
860 |
(2,[1,2,3],"#Find",Const (#,#),[Free #]),
|
neuper@37906
|
861 |
(3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
|
neuper@37906
|
862 |
(5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
|
neuper@37906
|
863 |
(8,[3],"#undef",Const (#,#),[Free #]),
|
neuper@37906
|
864 |
(10,[3],"#undef",Const (#,#),[# $ #]),
|
neuper@37906
|
865 |
(11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
|
neuper@37906
|
866 |
|
neuper@37906
|
867 |
fun separate_vats oris =
|
neuper@37928
|
868 |
let val vats = foldl coll_vats ([] : int list, oris);
|
neuper@37906
|
869 |
in map (filter_vat oris) vats end;
|
neuper@37906
|
870 |
(*^^^ end preparational work 8.01.*)
|
neuper@37906
|
871 |
|
neuper@37906
|
872 |
|
neuper@37906
|
873 |
|
neuper@37906
|
874 |
(**. check a problem (ie. itm list) for matching a problemtype .**)
|
neuper@37906
|
875 |
|
neuper@37906
|
876 |
fun eq1 d (_,(d',_)) = (d = d');
|
neuper@37906
|
877 |
fun itm_id ((i,_,_,_,_):itm) = i;
|
neuper@37906
|
878 |
fun ori_id ((i,_,_,_,_):ori) = i;
|
neuper@37906
|
879 |
fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm);
|
neuper@37906
|
880 |
(*see + add_sel_ppc ~~~~~~~*)
|
neuper@37906
|
881 |
fun field_eq f ((_,_,f',_,_):ori) = f = f';
|
neuper@37906
|
882 |
|
neuper@37906
|
883 |
(*. check an item (with arbitrary itm_ from previous matchings)
|
neuper@37906
|
884 |
for matching a problemtype; returns true only for itms found in pbt .*)
|
neuper@37906
|
885 |
fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
|
neuper@37906
|
886 |
(case find_first (eq1 d) pbt of
|
neuper@37926
|
887 |
SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
|
neuper@37906
|
888 |
(id, pbl_ids' thy d vs))):itm)
|
neuper@37926
|
889 |
| NONE => (i,vats,false,f,Sup (d,vs)))
|
neuper@37906
|
890 |
| chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
|
neuper@37906
|
891 |
(case find_first (eq1 d) pbt of
|
neuper@37926
|
892 |
SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
|
neuper@37906
|
893 |
(id, pbl_ids' thy d vs))):itm)
|
neuper@37926
|
894 |
| NONE => (i,vats,false,f,Sup (d,vs)))
|
neuper@37906
|
895 |
|
neuper@37906
|
896 |
| chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
|
neuper@37906
|
897 |
| chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm
|
neuper@37906
|
898 |
|
neuper@37906
|
899 |
| chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
|
neuper@37906
|
900 |
(case find_first (eq1 d) pbt of
|
neuper@37926
|
901 |
SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
|
neuper@37906
|
902 |
(id, pbl_ids' thy d vs))):itm)
|
neuper@37926
|
903 |
| NONE => (i,vats,false,f,Sup (d,vs)))
|
neuper@37906
|
904 |
(* val (i,vats,b,f,Mis (d,vs)) = i4;
|
neuper@37906
|
905 |
*)
|
neuper@37906
|
906 |
| chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
|
neuper@37906
|
907 |
(case find_first (eq1 d) pbt of
|
neuper@37926
|
908 |
(* val SOME (_,(_,id)) = find_first (eq1 d) pbt;
|
neuper@37906
|
909 |
*)
|
neuper@37926
|
910 |
SOME (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
|
neuper@37906
|
911 |
\(id, pbl_ids' d vs))):itm)"
|
neuper@37926
|
912 |
| NONE => (i,vats,false,f,Sup (d,[vs])));
|
neuper@37906
|
913 |
|
neuper@37906
|
914 |
(* chk_ thy pbt i
|
neuper@37906
|
915 |
*)
|
neuper@37906
|
916 |
|
neuper@37906
|
917 |
fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;
|
neuper@37906
|
918 |
fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
|
neuper@37906
|
919 |
fun eq0 ((0,_,_,_,_):itm) = true
|
neuper@37906
|
920 |
| eq0 _ = false;
|
neuper@37906
|
921 |
fun max_i i [] = i
|
neuper@37906
|
922 |
| max_i i ((id,_,_,_,_)::is) =
|
neuper@37906
|
923 |
if i > id then max_i i is else max_i id is;
|
neuper@37906
|
924 |
fun max_id [] = 0
|
neuper@37906
|
925 |
| max_id ((id,_,_,_,_)::is) = max_i id is;
|
neuper@37906
|
926 |
fun add_idvat itms _ _ [] = itms
|
neuper@37906
|
927 |
| add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) =
|
neuper@37906
|
928 |
add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *)
|
neuper@37906
|
929 |
],b,f,itm_):itm]) (i+1) mvat its;
|
neuper@37906
|
930 |
|
neuper@37906
|
931 |
|
neuper@37906
|
932 |
(*. find elements of pbt not contained in itms;
|
neuper@37906
|
933 |
if such one is untouched, return this one, otherwise create new itm .*)
|
neuper@37906
|
934 |
fun chk_m (itms:itm list) untouched (p as (f,(d,id))) =
|
neuper@37906
|
935 |
case find_first (eq2 p) itms of
|
neuper@37926
|
936 |
SOME _ => []
|
neuper@37926
|
937 |
| NONE => (case find_first (eq2 p) untouched of
|
neuper@37926
|
938 |
SOME itm => [itm]
|
neuper@37926
|
939 |
| NONE => [(0,[],false,f,Mis (d,id)):itm]);
|
neuper@37906
|
940 |
(* val itms = itms'';
|
neuper@37906
|
941 |
*)
|
neuper@37906
|
942 |
fun chk_mis mvat itms untouched pbt =
|
neuper@37906
|
943 |
let val mis = (flat o (map (chk_m itms untouched))) pbt;
|
neuper@37906
|
944 |
val mid = max_id itms;
|
neuper@37906
|
945 |
in add_idvat [] (mid + 1) mvat mis end;
|
neuper@37906
|
946 |
|
neuper@37906
|
947 |
(*. check a problem (ie. itm list) for matching a problemtype,
|
neuper@37906
|
948 |
takes the max_vt for concluding completeness (could be another!) .*)
|
neuper@37906
|
949 |
(* val itms = itms'; val (pbt,pre) = (ppc, pre);
|
neuper@37906
|
950 |
val itms = itms; val (pbt,pre) = (ppc, pre);
|
neuper@37906
|
951 |
*)
|
neuper@37906
|
952 |
fun match_itms thy itms (pbt,pre,prls) =
|
neuper@37928
|
953 |
(let fun okv mvat (_,vats,b,_,_) = member op = vats mvat
|
neuper@37928
|
954 |
andalso b;
|
neuper@37906
|
955 |
val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
|
neuper@37906
|
956 |
val mvat = max_vt itms';
|
neuper@37906
|
957 |
val itms'' = filter (okv mvat) itms';
|
neuper@37906
|
958 |
val untouched = filter eq0 itms;(*i.e. dsc only (from init)*)
|
neuper@37906
|
959 |
val mis = chk_mis mvat itms'' untouched pbt;
|
neuper@37906
|
960 |
val pre' = check_preconds' prls pre itms'' mvat
|
neuper@37906
|
961 |
val pb = foldl and_ (true, map fst pre')
|
neuper@37906
|
962 |
in (length mis = 0 andalso pb, (itms'@ mis, pre')) end);
|
neuper@37906
|
963 |
|
neuper@37906
|
964 |
(*. check a problem pbl (ie. itm list) for matching a problemtype pbt,
|
neuper@37906
|
965 |
for missing items get data from formalization (ie. ori list);
|
neuper@37906
|
966 |
takes the max_vt for concluding completeness (could be another!) .*)
|
neuper@37906
|
967 |
(* (0) determine the most frequent variant mv in pbl
|
neuper@37906
|
968 |
ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
|
neuper@37906
|
969 |
(2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
|
neuper@37906
|
970 |
(3) newitms = filter (mv mem vat(news)) news
|
neuper@37906
|
971 |
(4) pbt @ newitms *)
|
neuper@37906
|
972 |
(* val (pbl, pbt, pre) = (met, mtt, pre);
|
neuper@37906
|
973 |
val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt);
|
neuper@37906
|
974 |
val (pbl, pbt, pre) = (itms, ppc, where_);
|
neuper@37906
|
975 |
*)
|
neuper@37906
|
976 |
fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris =
|
neuper@37906
|
977 |
let
|
neuper@37906
|
978 |
(*0*)val mv = max_vt pbl;
|
neuper@37906
|
979 |
|
neuper@37906
|
980 |
fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
|
neuper@37906
|
981 |
fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
|
neuper@37926
|
982 |
SOME _ => false | NONE => true;
|
neuper@37906
|
983 |
(*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;
|
neuper@37906
|
984 |
|
neuper@37906
|
985 |
fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
|
neuper@37906
|
986 |
fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) =
|
neuper@37906
|
987 |
(i,v,false,f,Mis (d,pid)):itm;
|
neuper@37906
|
988 |
(*2*)fun oris2itms oris mis1 =
|
neuper@37906
|
989 |
((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
|
neuper@37906
|
990 |
val news = (flat o (map (oris2itms oris))) mis;
|
neuper@37928
|
991 |
(*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv;
|
neuper@37906
|
992 |
val newitms = filter mem_vat news;
|
neuper@37906
|
993 |
(*4*)val itms' = pbl @ newitms;
|
neuper@37906
|
994 |
val pre' = check_preconds' prls pre itms' mv
|
neuper@37906
|
995 |
val pb = foldl and_ (true, map fst pre')
|
neuper@37906
|
996 |
in (length mis = 0 andalso pb, (itms', pre')) end;
|
neuper@37906
|
997 |
(*handle _ => (false,([],[]))*);
|
neuper@37906
|
998 |
|
neuper@37906
|
999 |
|
neuper@37906
|
1000 |
(*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris
|
neuper@37906
|
1001 |
allow for faster access to descriptions and terms *)
|
neuper@37906
|
1002 |
(**. check a problem (ie. itm list) for matching a problemtype .**)
|
neuper@37906
|
1003 |
|
neuper@37906
|
1004 |
(*. check an ori for matching a problemtype by description;
|
neuper@37906
|
1005 |
returns true only for itms found in pbt .*)
|
neuper@37906
|
1006 |
fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
|
neuper@37906
|
1007 |
case find_first (eq1 d) pbt of
|
neuper@37926
|
1008 |
SOME (_,(_,id)) => [(i,vats,true,f,
|
neuper@37906
|
1009 |
Cor ((d,vs), (id, pbl_ids' thy d vs))):itm]
|
neuper@37926
|
1010 |
| NONE => [];
|
neuper@37906
|
1011 |
|
neuper@37906
|
1012 |
(* elem 'p' of pbt contained in itms ? *)
|
neuper@37906
|
1013 |
fun chk1_m (itms:itm list) p =
|
neuper@37906
|
1014 |
case find_first (eq2 p) itms of
|
neuper@37926
|
1015 |
SOME _ => true | NONE => false;
|
neuper@37906
|
1016 |
fun chk1_m' (oris: ori list) (p as (f,(d,t))) =
|
neuper@37906
|
1017 |
case find_first (eq2' p) oris of
|
neuper@37926
|
1018 |
SOME _ => []
|
neuper@37926
|
1019 |
| NONE => [(f, Mis (d, t))];
|
neuper@37906
|
1020 |
fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;
|
neuper@37906
|
1021 |
|
neuper@37906
|
1022 |
fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
|
neuper@37906
|
1023 |
fun chk1_mis' oris ppc =
|
neuper@37906
|
1024 |
map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
|
neuper@37906
|
1025 |
|
neuper@37906
|
1026 |
|
neuper@37906
|
1027 |
(*. check a problem (ie. ori list) for matching a problemtype,
|
neuper@37906
|
1028 |
takes the max_vt for concluding completeness (FIXME could be another!) .*)
|
neuper@37906
|
1029 |
(* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py);
|
neuper@37906
|
1030 |
*)
|
neuper@37906
|
1031 |
fun match_oris thy prls oris (pbt,pre) =
|
neuper@37906
|
1032 |
let val itms = (flat o (map (chk1_ thy pbt))) oris;
|
neuper@37906
|
1033 |
val mvat = max_vt itms;
|
neuper@37906
|
1034 |
val complete = chk1_mis mvat itms pbt;
|
neuper@37906
|
1035 |
val pre' = check_preconds' prls pre itms mvat
|
neuper@37906
|
1036 |
val pb = foldl and_ (true, map fst pre')
|
neuper@37906
|
1037 |
in if complete andalso pb then true else false end;
|
neuper@37906
|
1038 |
(*run subp-rooteq.sml 'root-eq + subpbl: solve_linear'
|
neuper@37906
|
1039 |
until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"...
|
neuper@37906
|
1040 |
> val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_,
|
neuper@37906
|
1041 |
Nd(PblObj{origin=(oris,_,_),...},[])]) = pt;
|
neuper@37906
|
1042 |
> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
|
neuper@37906
|
1043 |
(#where_ o get_pbt) ["linear","univariate","equation"]);
|
neuper@37906
|
1044 |
> match_oris oris (pbt,pre);
|
neuper@37906
|
1045 |
val it = true : bool
|
neuper@37906
|
1046 |
|
neuper@37906
|
1047 |
|
neuper@37906
|
1048 |
> val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"],
|
neuper@37906
|
1049 |
(#where_ o get_pbt)["plain_square","univariate","equation"]);
|
neuper@37906
|
1050 |
> match_oris oris (pbt,pre);
|
neuper@37906
|
1051 |
val it = false : bool
|
neuper@37906
|
1052 |
|
neuper@37906
|
1053 |
|
neuper@37906
|
1054 |
---------------------------------------------------
|
neuper@37906
|
1055 |
run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square'
|
neuper@37906
|
1056 |
until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ...
|
neuper@37906
|
1057 |
> val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]),
|
neuper@37906
|
1058 |
Nd (PblObj {origin=(oris,_,_),...},[])]) = pt;
|
neuper@37906
|
1059 |
> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
|
neuper@37906
|
1060 |
(#where_ o get_pbt) ["linear","univariate","equation"]);
|
neuper@37906
|
1061 |
> match_oris oris (pbt,pre);
|
neuper@37906
|
1062 |
val it = false : bool
|
neuper@37906
|
1063 |
|
neuper@37906
|
1064 |
|
neuper@37906
|
1065 |
> val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"],
|
neuper@37906
|
1066 |
(#where_ o get_pbt) ["plain_square","univariate","equation"]);
|
neuper@37906
|
1067 |
> match_oris oris (pbt,pre);
|
neuper@37906
|
1068 |
val it = true : bool
|
neuper@37906
|
1069 |
*)
|
neuper@37906
|
1070 |
(*^^^--- doubled 20.9.01 *)
|
neuper@37906
|
1071 |
|
neuper@37906
|
1072 |
|
neuper@37906
|
1073 |
(*. check a problem (ie. ori list) for matching a problemtype,
|
neuper@37906
|
1074 |
returns items for output to math-experts .*)
|
neuper@37906
|
1075 |
(* val (ppc,pre) = (#ppc py, #where_ py);
|
neuper@37906
|
1076 |
*)
|
neuper@37906
|
1077 |
fun match_oris' thy oris (ppc,pre,prls) =
|
neuper@37906
|
1078 |
(* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));
|
neuper@37906
|
1079 |
*)
|
neuper@37906
|
1080 |
let val itms = (flat o (map (chk1_ thy ppc))) oris;
|
neuper@37906
|
1081 |
val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris;
|
neuper@37906
|
1082 |
val mvat = max_vt itms;
|
neuper@37906
|
1083 |
val miss = chk1_mis' oris ppc;
|
neuper@37906
|
1084 |
val pre' = check_preconds' prls pre itms mvat
|
neuper@37906
|
1085 |
val pb = foldl and_ (true, map fst pre')
|
neuper@37906
|
1086 |
in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
|
neuper@37906
|
1087 |
|
neuper@37906
|
1088 |
(*. for the user .*)
|
neuper@37906
|
1089 |
datatype match' =
|
neuper@37906
|
1090 |
Matches' of item ppc
|
neuper@37906
|
1091 |
| NoMatch' of item ppc;
|
neuper@37906
|
1092 |
|
neuper@37906
|
1093 |
(*. match a formalization with a problem type .*)
|
neuper@37906
|
1094 |
fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
|
neuper@37906
|
1095 |
let val oris = prep_ori fmz thy ppc;
|
neuper@37906
|
1096 |
val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
|
neuper@37906
|
1097 |
in if bool then Matches' (itms2itemppc thy itms pre')
|
neuper@37906
|
1098 |
else NoMatch' (itms2itemppc thy itms pre') end;
|
neuper@37906
|
1099 |
(*
|
neuper@37906
|
1100 |
val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
|
neuper@37906
|
1101 |
"solveFor x","errorBound (eps=0)","solutions L"];
|
neuper@37906
|
1102 |
val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
|
neuper@37906
|
1103 |
get_pbt ["univariate","equation"];
|
neuper@37906
|
1104 |
match_pbl fmz pbt;
|
neuper@37906
|
1105 |
*)
|
neuper@37906
|
1106 |
|
neuper@37906
|
1107 |
|
neuper@37906
|
1108 |
(*. refine a problem; construct pblRD while scanning .*)
|
neuper@37906
|
1109 |
(* val (pblRD,ori)=("xxx",oris);
|
neuper@37906
|
1110 |
val py = get_pbt ["equation"];
|
neuper@37906
|
1111 |
val py = get_pbt ["univariate","equation"];
|
neuper@37906
|
1112 |
val py = get_pbt ["linear","univariate","equation"];
|
neuper@37986
|
1113 |
val py = get_pbt ["root'","univariate","equation"];
|
neuper@37906
|
1114 |
match_oris (#prls py) ori (#ppc py, #where_ py);
|
neuper@37906
|
1115 |
|
neuper@37906
|
1116 |
*)
|
neuper@37906
|
1117 |
fun refin (pblRD:pblRD) ori
|
neuper@37906
|
1118 |
((Ptyp (pI,[py],[])):pbt ptyp) =
|
neuper@37906
|
1119 |
if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
|
neuper@37926
|
1120 |
then SOME ((pblRD @ [pI]):pblRD)
|
neuper@37926
|
1121 |
else NONE
|
neuper@37906
|
1122 |
| refin pblRD ori (Ptyp (pI,[py],pys)) =
|
neuper@37906
|
1123 |
if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
|
neuper@37906
|
1124 |
then (case refins (pblRD @ [pI]) ori pys of
|
neuper@37926
|
1125 |
SOME pblRD' => SOME pblRD'
|
neuper@37926
|
1126 |
| NONE => SOME (pblRD @ [pI]))
|
neuper@37926
|
1127 |
else NONE
|
neuper@37926
|
1128 |
and refins pblRD ori [] = NONE
|
neuper@37906
|
1129 |
| refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =
|
neuper@37906
|
1130 |
(case refin pblRD ori p of
|
neuper@37926
|
1131 |
SOME pblRD' => SOME pblRD'
|
neuper@37926
|
1132 |
| NONE => refins pblRD ori pts);
|
neuper@37906
|
1133 |
|
neuper@37906
|
1134 |
(*. refine a problem; version providing output for math-experts .*)
|
neuper@37906
|
1135 |
fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
|
neuper@37906
|
1136 |
(* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
|
neuper@37906
|
1137 |
(rev ["linear","system"], fmz, [(*match list*)],
|
neuper@37906
|
1138 |
((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
|
neuper@37906
|
1139 |
*)
|
neuper@37906
|
1140 |
let val _ = (writeln o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
|
neuper@37906
|
1141 |
val {thy,ppc,where_,prls,...} = py
|
neuper@37906
|
1142 |
val oris = prep_ori fmz thy ppc
|
neuper@37906
|
1143 |
(*8.3.02: itms!: oris ev. are _not_ complete here*)
|
neuper@37906
|
1144 |
val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
|
neuper@37906
|
1145 |
in if b then pbls @ [Matches (rev (pblRD @ [pI]),
|
neuper@37906
|
1146 |
itms2itemppc thy itms pre')]
|
neuper@37906
|
1147 |
else pbls @ [NoMatch (rev (pblRD @ [pI]),
|
neuper@37906
|
1148 |
itms2itemppc thy itms pre')]
|
neuper@37906
|
1149 |
end
|
neuper@37906
|
1150 |
(* val pblRD = ["pbla"]; val fmz = fmz1; val pbls = [];
|
neuper@37906
|
1151 |
val Ptyp (pI,[py],pys) = hd (!ptyps);
|
neuper@37906
|
1152 |
refin' pblRD fmz pbls (Ptyp (pI,[py],pys));
|
neuper@37906
|
1153 |
*)
|
neuper@37906
|
1154 |
| refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) =
|
neuper@37906
|
1155 |
let val _ = (writeln o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
|
neuper@37906
|
1156 |
val {thy,ppc,where_,prls,...} = py
|
neuper@37906
|
1157 |
val oris = prep_ori fmz thy ppc;
|
neuper@37906
|
1158 |
(*8.3.02: itms!: oris ev. are _not_ complete here*)
|
neuper@37906
|
1159 |
val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
|
neuper@37906
|
1160 |
in if b
|
neuper@37906
|
1161 |
then let val pbl = Matches (rev (pblRD @ [pI]),
|
neuper@37906
|
1162 |
itms2itemppc thy itms pre')
|
neuper@37906
|
1163 |
in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
|
neuper@37906
|
1164 |
else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
|
neuper@37906
|
1165 |
end
|
neuper@37906
|
1166 |
and refins' pblRD fmz pbls [] = pbls
|
neuper@37906
|
1167 |
| refins' pblRD fmz pbls ((p as Ptyp (pI,_,_))::pts) =
|
neuper@37906
|
1168 |
let val pbls' = refin' pblRD fmz pbls p
|
neuper@37906
|
1169 |
in case last_elem pbls' of
|
neuper@37906
|
1170 |
Matches _ => pbls'
|
neuper@37906
|
1171 |
| NoMatch _ => refins' pblRD fmz pbls' pts end;
|
neuper@37906
|
1172 |
|
neuper@37906
|
1173 |
(*. refine a problem; version for tactic Refine_Problem .*)
|
neuper@37906
|
1174 |
fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
|
neuper@37906
|
1175 |
let (*val _ = writeln("### refin''1: pI="^pI);*)
|
neuper@37906
|
1176 |
val {thy,ppc,where_,prls,...} = py
|
neuper@37906
|
1177 |
val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
|
neuper@37906
|
1178 |
in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
|
neuper@37906
|
1179 |
else pbls @ [NoMatch_]
|
neuper@37906
|
1180 |
end
|
neuper@37906
|
1181 |
(* val pblRD = (rev o tl) pblID; val pbls = [];
|
neuper@37906
|
1182 |
val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);
|
neuper@37906
|
1183 |
*)
|
neuper@37906
|
1184 |
| refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =
|
neuper@37906
|
1185 |
let (*val _ = writeln("### refin''2: pI="^pI);*)
|
neuper@37906
|
1186 |
val {thy,ppc,where_,prls,...} = py
|
neuper@37906
|
1187 |
val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
|
neuper@37906
|
1188 |
in if b
|
neuper@37906
|
1189 |
then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
|
neuper@37906
|
1190 |
in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
|
neuper@37906
|
1191 |
else (pbls @ [NoMatch_])
|
neuper@37906
|
1192 |
end
|
neuper@37906
|
1193 |
and refins'' thy pblRD itms pbls [] = pbls
|
neuper@37906
|
1194 |
| refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) =
|
neuper@37906
|
1195 |
let val pbls' = refin'' thy pblRD itms pbls p
|
neuper@37906
|
1196 |
in case last_elem pbls' of
|
neuper@37906
|
1197 |
Match_ _ => pbls'
|
neuper@37906
|
1198 |
| NoMatch_ => refins'' thy pblRD itms pbls' pts end;
|
neuper@37906
|
1199 |
|
neuper@37906
|
1200 |
|
neuper@37906
|
1201 |
(*. apply a fun to a ptyps node; copied from get_py .*)
|
neuper@37906
|
1202 |
fun app_ptyp f (d:pblID) _ [] =
|
neuper@37906
|
1203 |
raise error ("app_ptyp not found: "^(strs2str d))
|
neuper@37906
|
1204 |
| app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =
|
neuper@37906
|
1205 |
if k=k' then f p
|
neuper@37906
|
1206 |
else app_ptyp f d ([k]:pblRD) pys
|
neuper@37906
|
1207 |
| app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') =
|
neuper@37906
|
1208 |
if k=k' then app_ptyp f d ks pys
|
neuper@37906
|
1209 |
else app_ptyp f d (k::ks) pys';
|
neuper@37906
|
1210 |
|
neuper@37906
|
1211 |
(*. for tactic Refine_Tacitly .*)
|
neuper@37906
|
1212 |
(*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*)
|
neuper@37906
|
1213 |
(* val (thy,pblID) = (assoc_thy dI',pI);
|
neuper@37906
|
1214 |
*)
|
neuper@37906
|
1215 |
fun refine_ori oris (pblID:pblID) =
|
neuper@37906
|
1216 |
let val opt = app_ptyp (refin ((rev o tl) pblID) oris)
|
neuper@37906
|
1217 |
pblID (rev pblID) (!ptyps);
|
neuper@37906
|
1218 |
in case opt of
|
neuper@37926
|
1219 |
SOME pblRD => let val (pblID':pblID) =(rev pblRD)
|
neuper@37926
|
1220 |
in if pblID' = pblID then NONE
|
neuper@37926
|
1221 |
else SOME pblID' end
|
neuper@37926
|
1222 |
| NONE => NONE end;
|
neuper@37906
|
1223 |
fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
|
neuper@37906
|
1224 |
|
neuper@37906
|
1225 |
(*. for tactic Refine_Problem .*);
|
neuper@37906
|
1226 |
(* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
|
neuper@37906
|
1227 |
(* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);
|
neuper@37906
|
1228 |
*)
|
neuper@37906
|
1229 |
fun refine_pbl thy (pblID:pblID) itms =
|
neuper@37906
|
1230 |
case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms [])
|
neuper@37906
|
1231 |
pblID (rev pblID) (!ptyps)) of
|
neuper@37926
|
1232 |
NONE => NONE
|
neuper@37926
|
1233 |
| SOME (Match_ (rfd as (pI',_))) =>
|
neuper@37926
|
1234 |
if pblID = pI' then NONE else SOME rfd;
|
neuper@37906
|
1235 |
|
neuper@37906
|
1236 |
|
neuper@37906
|
1237 |
(*. for math-experts .*)
|
neuper@37906
|
1238 |
(*19.10.02FIXME: needs thy for parsing fmz*)
|
neuper@37906
|
1239 |
(* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
|
neuper@37906
|
1240 |
val pbls = []; val ptys = !ptyps;
|
neuper@37906
|
1241 |
*)
|
neuper@37906
|
1242 |
fun refine (fmz:fmz_) (pblID:pblID) =
|
neuper@37906
|
1243 |
app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps);
|
neuper@37906
|
1244 |
|
neuper@37906
|
1245 |
|
neuper@37906
|
1246 |
(*.make a guh from a reference to an element in the kestore;
|
neuper@37906
|
1247 |
EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
|
neuper@37906
|
1248 |
fun pblID2guh (pblID:pblID) =
|
neuper@37906
|
1249 |
(((#guh o get_pbt) pblID)
|
neuper@37906
|
1250 |
handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
|
neuper@37906
|
1251 |
fun metID2guh (metID:metID) =
|
neuper@37906
|
1252 |
(((#guh o get_met) metID)
|
neuper@37906
|
1253 |
handle _ => raise error ("metID2guh: no 'Met_' for '"^
|
neuper@37906
|
1254 |
strs2str' metID ^ "'"));
|
neuper@37906
|
1255 |
fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
|
neuper@37906
|
1256 |
| kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
|
neuper@37906
|
1257 |
| kestoreID2guh ketype kestoreID =
|
neuper@37906
|
1258 |
raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
|
neuper@37906
|
1259 |
strs2str' kestoreID ^ "'");
|
neuper@37906
|
1260 |
|
neuper@37906
|
1261 |
fun show_pblguhs () =
|
neuper@37906
|
1262 |
(print_depth 999;
|
neuper@37906
|
1263 |
(writeln o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));
|
neuper@37906
|
1264 |
print_depth 3);
|
neuper@37906
|
1265 |
fun sort_pblguhs () =
|
neuper@37906
|
1266 |
(print_depth 999;
|
neuper@37906
|
1267 |
(writeln o strs2str o (map linefeed))
|
neuper@37906
|
1268 |
(((sort string_ord) o coll_pblguhs) (!ptyps));
|
neuper@37906
|
1269 |
print_depth 3);
|
neuper@37906
|
1270 |
|
neuper@37906
|
1271 |
fun show_metguhs () =
|
neuper@37906
|
1272 |
(print_depth 999;
|
neuper@37906
|
1273 |
(writeln o strs2str o (map linefeed)) (coll_metguhs (!mets));
|
neuper@37906
|
1274 |
print_depth 3);
|
neuper@37906
|
1275 |
fun sort_metguhs () =
|
neuper@37906
|
1276 |
(print_depth 999;
|
neuper@37906
|
1277 |
(writeln o strs2str o (map linefeed))
|
neuper@37906
|
1278 |
(((sort string_ord) o coll_metguhs) (!mets));
|
neuper@37906
|
1279 |
print_depth 3);
|