5 use"ME/ptyps.sml"; |
5 use"ME/ptyps.sml"; |
6 use"ptyps.sml"; |
6 use"ptyps.sml"; |
7 *) |
7 *) |
8 |
8 |
9 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*) |
9 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*) |
10 val dsc_unknown = (term_of o the o (parseold Script.thy)) |
10 val dsc_unknown = (term_of o the o (parseold @{theory Script})) |
11 "unknown::'a => unknow"; |
11 "unknown::'a => unknow"; |
12 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*) |
12 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*) |
13 |
13 |
14 |
14 |
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) |
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) |
16 |
16 |
17 |
17 fun itm_2item thy (Cor ((d,ts),_)) = |
18 |
18 Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) |
19 |
19 | itm_2item _ (Syn c) = SyntaxE c |
20 fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts))) |
20 | itm_2item _ (Typ c) = TypeE c |
21 | itm_2item thy (Syn c) = SyntaxE c |
21 | itm_2item thy (Inc ((d,ts),_)) = |
22 | itm_2item thy (Typ c) = TypeE c |
22 Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) |
23 | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts))) |
23 | itm_2item thy (Sup (d,ts)) = |
24 | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts))) |
24 Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts))) |
25 | itm_2item thy (Mis (d,pid)) = |
25 | itm_2item _ (Mis (d,pid)) = |
26 Missing (Sign.string_of_term (sign_of thy) d ^" "^ |
26 Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^ |
27 Sign.string_of_term (sign_of thy) pid); |
27 Syntax.string_of_term (ctxt_Isac"") pid); |
28 |
|
29 |
|
30 |
|
31 |
28 |
32 |
29 |
33 (* --- 8.3.00 |
30 (* --- 8.3.00 |
34 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list) |
31 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list) |
35 handle _ => error ("get_dsc_in not for "^sel); |
32 handle _ => error ("get_dsc_in not for "^sel); |
100 in if is_dsc hd |
97 in if is_dsc hd |
101 then (hd, args) |
98 then (hd, args) |
102 else (e_term, [t]) (*??? 9.01 just copied*) |
99 else (e_term, [t]) (*??? 9.01 just copied*) |
103 end) |
100 end) |
104 handle _ => raise error ("split_dsc: called with "^ |
101 handle _ => raise error ("split_dsc: called with "^ |
105 (Sign.string_of_term (sign_of thy) t)); |
102 (Syntax.string_of_term (ctxt_Isac"") t)); |
106 (* |
103 (* |
107 > val t1 = (term_of o the o (parse thy)) "errorBound err_"; |
104 > val t1 = (term_of o the o (parse thy)) "errorBound err_"; |
108 > split_dsc t1; |
105 > split_dsc t1; |
109 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool")) |
106 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool")) |
110 : term * term |
107 : term * term |
130 for pbt, met.ppc *) |
127 for pbt, met.ppc *) |
131 fun split_did t = |
128 fun split_did t = |
132 (let val (hd,[arg]) = strip_comb t |
129 (let val (hd,[arg]) = strip_comb t |
133 in (hd,arg) end) |
130 in (hd,arg) end) |
134 handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = " |
131 handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = " |
135 ^(Sign.string_of_term (sign_of Script.thy) t)); |
132 ^(Syntax.string_of_term (thy2ctxt' "Script") t)); |
136 |
133 |
137 |
134 |
138 |
135 |
139 (*create output-string for itm_*) |
136 (*create output-string for itm_*) |
140 fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts))) |
137 fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
141 | itm_out thy (Syn c) = c |
138 | itm_out thy (Syn c) = c |
142 | itm_out thy (Typ c) = c |
139 | itm_out thy (Typ c) = c |
143 | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts))) |
140 | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
144 | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts))) |
141 | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
145 | itm_out thy (Mis (d,pid)) = |
142 | itm_out thy (Mis (d,pid)) = |
146 Sign.string_of_term (sign_of thy) d ^" "^ |
143 Syntax.string_of_term (ctxt_Isac"") d ^" "^ |
147 Sign.string_of_term (sign_of thy) pid; |
144 Syntax.string_of_term (ctxt_Isac"") pid; |
148 |
145 |
149 (*22.11.00 unused |
146 (*22.11.00 unused |
150 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) |
147 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) |
151 |
148 |
152 |
149 |
164 | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms |
161 | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms |
165 in coll [] itms end; |
162 in coll [] itms end; |
166 *) |
163 *) |
167 (*--3.3.00 |
164 (*--3.3.00 |
168 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = |
165 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = |
169 Correct (string_of_cterm (comp_dts thy(d,ts))) |
166 Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
170 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c |
167 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c |
171 | itm2item (_,_,_,_,Typ (c)) = TypeE c |
168 | itm2item (_,_,_,_,Typ (c)) = TypeE c |
172 | itm2item (_,_,_,_,Fal (d,ts)) = |
169 | itm2item (_,_,_,_,Fal (d,ts)) = |
173 False (string_of_cterm (comp_dts thy(d,ts))) |
170 False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
174 | itm2item (_,_,_,_,Inc (d,ts)) = |
171 | itm2item (_,_,_,_,Inc (d,ts)) = |
175 Incompl (string_of_cterm (comp_dts thy(d,ts))) |
172 Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))) |
176 | itm2item (_,_,_,_,Sup (d,ts)) = |
173 | itm2item (_,_,_,_,Sup (d,ts)) = |
177 Superfl (string_of_cterm (comp_dts thy(d,ts))); |
174 Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts))); |
178 *) |
175 *) |
179 |
176 |
180 fun boolterm2item (true, term) = Correct (term2str term) |
177 fun boolterm2item (true, term) = Correct (term2str term) |
181 | boolterm2item (false, term) = False (term2str term); |
178 | boolterm2item (false, term) = False (term2str term); |
182 |
179 |
200 then ("#Find",d,ts) |
197 then ("#Find",d,ts) |
201 else if d mem (get_dsc_in dscs "#Relate") |
198 else if d mem (get_dsc_in dscs "#Relate") |
202 then ("#Relate",d,ts) |
199 then ("#Relate",d,ts) |
203 else ("#undef",d,ts); |
200 else ("#undef",d,ts); |
204 (* 28.1.00 raise error ("add_field: '"^ |
201 (* 28.1.00 raise error ("add_field: '"^ |
205 (Sign.string_of_term (sign_of thy) d)^ |
202 (Syntax.string_of_term (ctxt_Isac"") d)^ |
206 "' not in ppc-description "); *) |
203 "' not in ppc-description "); *) |
207 ------9.3. *) |
204 ------9.3. *) |
208 |
205 |
209 (* 9.3.00 |
206 (* 9.3.00 |
210 compare d and dsc in pbt and transfer field to pre-ori *) |
207 compare d and dsc in pbt and transfer field to pre-ori *) |
212 let fun eq d pt = (d = (fst o snd) pt); |
209 let fun eq d pt = (d = (fst o snd) pt); |
213 in case filter (eq d) pbt of |
210 in case filter (eq d) pbt of |
214 [(fi,(dsc,_))] => (fi,d,ts) |
211 [(fi,(dsc,_))] => (fi,d,ts) |
215 | [] => ("#undef",d,ts) (*may come with met.ppc*) |
212 | [] => ("#undef",d,ts) (*may come with met.ppc*) |
216 | _ => raise error ("add_field: "^ |
213 | _ => raise error ("add_field: "^ |
217 (Sign.string_of_term (sign_of thy) d)^ |
214 (Syntax.string_of_term (ctxt_Isac"") d)^ |
218 " more than once in pbt") |
215 " more than once in pbt") |
219 end; |
216 end; |
220 |
217 |
221 (*. take over field from met.ppc at 'Specify_Method' into ori, |
218 (*. take over field from met.ppc at 'Specify_Method' into ori, |
222 i.e. also removes "#undef" fields .*) |
219 i.e. also removes "#undef" fields .*) |
227 fun repl mpc (i,v,_,d,ts) = |
224 fun repl mpc (i,v,_,d,ts) = |
228 case filter (eq d) mpc of |
225 case filter (eq d) mpc of |
229 [(fi,(dsc,_))] => [(i,v,fi,d,ts)] |
226 [(fi,(dsc,_))] => [(i,v,fi,d,ts)] |
230 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) |
227 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) |
231 (*raise error ("add_field': "^ |
228 (*raise error ("add_field': "^ |
232 (Sign.string_of_term (sign_of thy) d)^ |
229 (Syntax.string_of_term (ctxt_Isac"") d)^ |
233 " not in met"*) |
230 " not in met"*) |
234 | _ => raise error ("add_field': "^ |
231 | _ => raise error ("add_field': "^ |
235 (Sign.string_of_term (sign_of thy) d)^ |
232 (Syntax.string_of_term (ctxt_Isac"") d)^ |
236 " more than once in met"); |
233 " more than once in met"); |
237 in (flat ((map (repl mpc)) ori)):ori list end; |
234 in (flat ((map (repl mpc)) ori)):ori list end; |
238 |
235 |
239 |
236 |
240 (*.mark an element with the position within a plateau; |
237 (*.mark an element with the position within a plateau; |
447 where_: term list, (* where - predicates*) |
444 where_: term list, (* where - predicates*) |
448 ppc : pat list, |
445 ppc : pat list, |
449 (*this is the model-pattern; |
446 (*this is the model-pattern; |
450 it contains "#Given","#Where","#Find","#Relate"-patterns*) |
447 it contains "#Given","#Where","#Find","#Relate"-patterns*) |
451 met : metID list}; (* methods solving the pbt*) |
448 met : metID list}; (* methods solving the pbt*) |
452 val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy, |
449 val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure", |
453 cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt; |
450 cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt; |
454 fun pbt2 (str, (t1, t2)) = |
451 fun pbt2 (str, (t1, t2)) = |
455 pair2str (str, pair2str (term2str t1, term2str t2)); |
452 pair2str (str, pair2str (term2str t1, term2str t2)); |
456 fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt; |
453 fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt; |
457 |
454 |
496 _REVERSE_ .......... !!!!!!!!!!*) |
493 _REVERSE_ .......... !!!!!!!!!!*) |
497 |
494 |
498 (*TODO: search generalized for subthy*) |
495 (*TODO: search generalized for subthy*) |
499 fun get_pbt (pblID:pblID) = |
496 fun get_pbt (pblID:pblID) = |
500 let val pblRD = rev pblID; |
497 let val pblRD = rev pblID; |
501 in get_py ProtoPure.thy pblID pblRD (!ptyps) end; |
498 in get_py (theory "Pure") pblID pblRD (!ptyps) end; |
502 (* get_pbt thy ["1"]; |
499 (* get_pbt thy ["1"]; |
503 get_pbt thy ["21","2"]; |
500 get_pbt thy ["21","2"]; |
504 *) |
501 *) |
505 |
502 |
506 (*TODO: throws exn 'get_pbt not found: ' ... confusing !! |
503 (*TODO: throws exn 'get_pbt not found: ' ... confusing !! |
507 take 'ketype' as an argument !!!!!*) |
504 take 'ketype' as an argument !!!!!*) |
508 fun get_met (metID:metID) = get_py ProtoPure.thy metID metID (!mets); |
505 fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets); |
509 fun get_the (theID:theID) = get_py ProtoPure.thy theID theID (!thehier); |
506 fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier); |
510 |
507 |
511 |
508 |
512 |
509 |
513 fun del_eq k ptyps = |
510 fun del_eq k ptyps = |
514 let fun del k ptyps [] = ptyps |
511 let fun del k ptyps [] = ptyps |
584 (*> guh2kestoreID "pbl_equ_univ_lin"; |
581 (*> guh2kestoreID "pbl_equ_univ_lin"; |
585 val it = ["linear", "univariate", "equation"] : string list*) |
582 val it = ["linear", "univariate", "equation"] : string list*) |
586 |
583 |
587 |
584 |
588 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) = |
585 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) = |
589 if guh mem (coll_pblguhs pbls) |
586 if member op = (coll_pblguhs pbls) guh |
590 then error ("check_guh_unique failed with '"^guh^"';\n"^ |
587 then error ("check_guh_unique failed with '"^guh^"';\n"^ |
591 "use 'sort_pblguhs()' for a list of guhs;\n"^ |
588 "use 'sort_pblguhs()' for a list of guhs;\n"^ |
592 "consider setting 'check_guhs_unique := false'") |
589 "consider setting 'check_guhs_unique := false'") |
593 else (); |
590 else (); |
594 (* val (guh, mets) = ("met_test", !mets); |
591 (* val (guh, mets) = ("met_test", !mets); |
595 *) |
592 *) |
596 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = |
593 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = |
597 if guh mem (coll_metguhs mets) |
594 if member op = (coll_metguhs mets) guh |
598 then error ("check_guh_unique failed with '"^guh^"';\n"^ |
595 then error ("check_guh_unique failed with '"^guh^"';\n"^ |
599 "use 'sort_metguhs()' for a list of guhs;\n"^ |
596 "use 'sort_metguhs()' for a list of guhs;\n"^ |
600 "consider setting 'check_guhs_unique := false'") |
597 "consider setting 'check_guhs_unique := false'") |
601 else (); |
598 else (); |
602 |
599 |
816 (*vvvvv---------- preparational work 8.01. UNUSED *) |
813 (*vvvvv---------- preparational work 8.01. UNUSED *) |
817 (**+ instantiate a problem-type +**) |
814 (**+ instantiate a problem-type +**) |
818 |
815 |
819 (*+ transform oris +*) |
816 (*+ transform oris +*) |
820 |
817 |
821 fun coll_vats (vats, ((_,vs,_,_,_):ori)) = vats union vs; |
818 fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs; |
822 (*> coll_vats [11,22] (hd oris); |
819 (*> coll_vats [11,22] (hd oris); |
823 val it = [22,11,1,2,3] : int list |
820 val it = [22,11,1,2,3] : int list |
824 |
821 |
825 > foldl coll_vats ([],oris); |
822 > foldl coll_vats ([],oris); |
826 val it = [1,2,3] : int list |
823 val it = [1,2,3] : int list |
834 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), |
831 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), |
835 (6,[1],"#undef",Const (#,#),[Free #]), |
832 (6,[1],"#undef",Const (#,#),[Free #]), |
836 (9,[1,2],"#undef",Const (#,#),[# $ #]), |
833 (9,[1,2],"#undef",Const (#,#),[# $ #]), |
837 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *) |
834 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *) |
838 |
835 |
839 fun filter_vat oris i = filter ((curry (op mem) i)o(#2:ori -> int list))oris; |
836 local |
|
837 infix mem; (*from Isabelle2002*) |
|
838 fun x mem [] = false |
|
839 | x mem (y :: ys) = x = y orelse x mem ys; |
|
840 in |
|
841 fun filter_vat oris i = |
|
842 filter ((curry (op mem) i) o (#2 : ori -> int list)) oris; |
|
843 end; |
840 (*> map (filter_vat oris) [1,2,3]; |
844 (*> map (filter_vat oris) [1,2,3]; |
841 val it = |
845 val it = |
842 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]), |
846 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]), |
843 (2,[1,2,3],"#Find",Const (#,#),[Free #]), |
847 (2,[1,2,3],"#Find",Const (#,#),[Free #]), |
844 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), |
848 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), |
859 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]), |
863 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]), |
860 (8,[3],"#undef",Const (#,#),[Free #]), |
864 (8,[3],"#undef",Const (#,#),[Free #]), |
861 (10,[3],"#undef",Const (#,#),[# $ #]), |
865 (10,[3],"#undef",Const (#,#),[# $ #]), |
862 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*) |
866 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*) |
863 |
867 |
864 |
|
865 fun separate_vats oris = |
868 fun separate_vats oris = |
866 let val vats = foldl coll_vats ([],oris); |
869 let val vats = foldl coll_vats ([] : int list, oris); |
867 in map (filter_vat oris) vats end; |
870 in map (filter_vat oris) vats end; |
868 (*^^^ end preparational work 8.01.*) |
871 (*^^^ end preparational work 8.01.*) |
869 |
872 |
870 |
873 |
871 |
874 |
946 takes the max_vt for concluding completeness (could be another!) .*) |
949 takes the max_vt for concluding completeness (could be another!) .*) |
947 (* val itms = itms'; val (pbt,pre) = (ppc, pre); |
950 (* val itms = itms'; val (pbt,pre) = (ppc, pre); |
948 val itms = itms; val (pbt,pre) = (ppc, pre); |
951 val itms = itms; val (pbt,pre) = (ppc, pre); |
949 *) |
952 *) |
950 fun match_itms thy itms (pbt,pre,prls) = |
953 fun match_itms thy itms (pbt,pre,prls) = |
951 (let fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b; |
954 (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat |
|
955 andalso b; |
952 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*) |
956 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*) |
953 val mvat = max_vt itms'; |
957 val mvat = max_vt itms'; |
954 val itms'' = filter (okv mvat) itms'; |
958 val itms'' = filter (okv mvat) itms'; |
955 val untouched = filter eq0 itms;(*i.e. dsc only (from init)*) |
959 val untouched = filter eq0 itms;(*i.e. dsc only (from init)*) |
956 val mis = chk_mis mvat itms'' untouched pbt; |
960 val mis = chk_mis mvat itms'' untouched pbt; |
983 fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) = |
987 fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) = |
984 (i,v,false,f,Mis (d,pid)):itm; |
988 (i,v,false,f,Mis (d,pid)):itm; |
985 (*2*)fun oris2itms oris mis1 = |
989 (*2*)fun oris2itms oris mis1 = |
986 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; |
990 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; |
987 val news = (flat o (map (oris2itms oris))) mis; |
991 val news = (flat o (map (oris2itms oris))) mis; |
988 (*3*)fun mem_vat (_,vats,b,_,_) = mv mem vats; |
992 (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv; |
989 val newitms = filter mem_vat news; |
993 val newitms = filter mem_vat news; |
990 (*4*)val itms' = pbl @ newitms; |
994 (*4*)val itms' = pbl @ newitms; |
991 val pre' = check_preconds' prls pre itms' mv |
995 val pre' = check_preconds' prls pre itms' mv |
992 val pb = foldl and_ (true, map fst pre') |
996 val pb = foldl and_ (true, map fst pre') |
993 in (length mis = 0 andalso pb, (itms', pre')) end; |
997 in (length mis = 0 andalso pb, (itms', pre')) end; |