1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/ME/ptyps.sml Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,1276 @@
1.4 +(* the problems and methods as stored in hierarchies
1.5 + author Walther Neuper 1998
1.6 + (c) due to copyright terms
1.7 +
1.8 +use"ME/ptyps.sml";
1.9 +use"ptyps.sml";
1.10 +*)
1.11 +
1.12 +(*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
1.13 +val dsc_unknown = (term_of o the o (parseold Script.thy))
1.14 + "unknown::'a => unknow";
1.15 +(*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
1.16 +
1.17 +
1.18 +(*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
1.19 +
1.20 +
1.21 +
1.22 +
1.23 +fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts)))
1.24 + | itm_2item thy (Syn c) = SyntaxE c
1.25 + | itm_2item thy (Typ c) = TypeE c
1.26 + | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts)))
1.27 + | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts)))
1.28 + | itm_2item thy (Mis (d,pid)) =
1.29 + Missing (Sign.string_of_term (sign_of thy) d ^" "^
1.30 + Sign.string_of_term (sign_of thy) pid);
1.31 +
1.32 +
1.33 +
1.34 +
1.35 +
1.36 +(* --- 8.3.00
1.37 +fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list)
1.38 + handle _ => error ("get_dsc_in not for "^sel);
1.39 +
1.40 +fun dscs_in dscppc =
1.41 + ((get_dsc_in dscppc "#Given") @
1.42 + (get_dsc_in dscppc "#Find") @
1.43 + (get_dsc_in dscppc "#Relate")):term list;
1.44 +
1.45 + --- 26.1.88
1.46 +fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel)));
1.47 +fun get_dsc pblID =
1.48 + (get_dsc_of pblID "#Given") @
1.49 + (get_dsc_of pblID "#Find") @
1.50 + (get_dsc_of pblID "#Relate");
1.51 + --- *)
1.52 +
1.53 +fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
1.54 + {Given=map f gi, Where=map f wh,
1.55 + Find=map f fi, With=map f wi, Relate=map f re}:'b ppc;
1.56 +fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
1.57 + {Given=f gi, Where=f wh,
1.58 + Find=f fi, With=f wi, Relate=f re}:'b ppc;
1.59 +
1.60 +(*for ppc of changing type*)
1.61 +fun sel_ppc sel ppc =
1.62 + case sel of
1.63 + "#Given" => #Given (ppc:'a ppc)
1.64 + | "#Where" => #Where (ppc:'a ppc)
1.65 + | "#Find" => #Find (ppc:'a ppc)
1.66 + | "#With" => #With (ppc:'a ppc)
1.67 + | "#Relate" => #Relate (ppc:'a ppc)
1.68 + | _ => raise error ("sel_ppc tried to select by '"^sel^"'");
1.69 +
1.70 +fun repl_sel_ppc sel
1.71 + ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
1.72 + case sel of
1.73 + "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
1.74 + | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
1.75 + | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
1.76 + | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
1.77 + | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
1.78 + | _ => raise error ("repl_sel_ppc tried to select by '"^sel^"'");
1.79 +
1.80 +fun add_sel_ppc thy sel
1.81 + ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
1.82 + case sel of
1.83 + "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
1.84 + | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}
1.85 + | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
1.86 + | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
1.87 + | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
1.88 + | _ => raise error ("add_sel_ppc tried to select by '"^sel^"'");
1.89 +fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
1.90 + ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
1.91 +
1.92 +(*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*)
1.93 +
1.94 +
1.95 +(*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*)
1.96 +
1.97 +
1.98 +
1.99 +(*decompose a problem-type into description and identifier
1.100 + FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
1.101 +fun split_dsc thy t =
1.102 + (let val (hd,args) = strip_comb t
1.103 + in if is_dsc hd
1.104 + then (hd, args)
1.105 + else (e_term, [t]) (*??? 9.01 just copied*)
1.106 + end)
1.107 + handle _ => raise error ("split_dsc: called with "^
1.108 + (Sign.string_of_term (sign_of thy) t));
1.109 +(*
1.110 +> val t1 = (term_of o the o (parse thy)) "errorBound err_";
1.111 +> split_dsc t1;
1.112 +(Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
1.113 + : term * term
1.114 +> val t3 = (term_of o the o (parse thy)) "valuesFor vs_";
1.115 +> split_dsc t3;
1.116 +(Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
1.117 + Free ("vs_","bool List.list")) : term * term*)
1.118 +
1.119 +
1.120 +
1.121 +(*. take the first two return-values; for prep_ori .*)
1.122 +(*WN.13.5.03fun split_dts' thy t =
1.123 + let val (d, ts, _) = split_dts thy t
1.124 + in (d, ts) end;*)
1.125 +(*WN.8.12.03 quick for prep_ori'*)
1.126 +fun split_dsc' t =
1.127 + (let val dsc $ var = t
1.128 + in var end)
1.129 + handle _ => raise error ("split_dsc': called with "^term2str t);
1.130 +
1.131 +(*9.3.00*)
1.132 +(* split a term into description and (id | structured variable)
1.133 + for pbt, met.ppc *)
1.134 +fun split_did t =
1.135 + (let val (hd,[arg]) = strip_comb t
1.136 + in (hd,arg) end)
1.137 + handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
1.138 + ^(Sign.string_of_term (sign_of Script.thy) t));
1.139 +
1.140 +
1.141 +
1.142 +(*create output-string for itm_*)
1.143 +fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
1.144 + | itm_out thy (Syn c) = c
1.145 + | itm_out thy (Typ c) = c
1.146 + | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
1.147 + | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts)))
1.148 + | itm_out thy (Mis (d,pid)) =
1.149 + Sign.string_of_term (sign_of thy) d ^" "^
1.150 + Sign.string_of_term (sign_of thy) pid;
1.151 +
1.152 +(*22.11.00 unused
1.153 +fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
1.154 +
1.155 +
1.156 +(*--3.3.
1.157 +fun itms2dts itms =
1.158 + let
1.159 + fun coll itms' [] = itms'
1.160 + | coll itms' (i::itms) =
1.161 + case i of
1.162 + (Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.163 + | (Syn c) => coll (itms' ) itms
1.164 + | (Typ c) => coll (itms' ) itms
1.165 + | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.166 + | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.167 + | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.168 + in coll [] itms end;
1.169 +*)
1.170 +(*--3.3.00
1.171 +fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
1.172 + Correct (string_of_cterm (comp_dts thy(d,ts)))
1.173 + | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
1.174 + | itm2item (_,_,_,_,Typ (c)) = TypeE c
1.175 + | itm2item (_,_,_,_,Fal (d,ts)) =
1.176 + False (string_of_cterm (comp_dts thy(d,ts)))
1.177 + | itm2item (_,_,_,_,Inc (d,ts)) =
1.178 + Incompl (string_of_cterm (comp_dts thy(d,ts)))
1.179 + | itm2item (_,_,_,_,Sup (d,ts)) =
1.180 + Superfl (string_of_cterm (comp_dts thy(d,ts)));
1.181 +*)
1.182 +
1.183 +fun boolterm2item (true, term) = Correct (term2str term)
1.184 + | boolterm2item (false, term) = False (term2str term);
1.185 +
1.186 +(* use"ME/modspec.sml";
1.187 + *)
1.188 +fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) =
1.189 + let
1.190 + fun coll ppc [] = ppc
1.191 + | coll ppc ((_,_,_,field,itm_)::itms) =
1.192 + coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
1.193 + val gfr = coll empty_ppc itms;
1.194 + in add_where gfr (map boolterm2item pre) end;
1.195 +(*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*)
1.196 +
1.197 +(*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*)
1.198 +
1.199 +(* --- 9.3.fun add_field dscs (d,ts) =
1.200 + if d mem (get_dsc_in dscs "#Given")
1.201 + then ("#Given",d,ts:term list)
1.202 + else if d mem (get_dsc_in dscs "#Find")
1.203 + then ("#Find",d,ts)
1.204 + else if d mem (get_dsc_in dscs "#Relate")
1.205 + then ("#Relate",d,ts)
1.206 + else ("#undef",d,ts);
1.207 +(* 28.1.00 raise error ("add_field: '"^
1.208 + (Sign.string_of_term (sign_of thy) d)^
1.209 + "' not in ppc-description "); *)
1.210 + ------9.3. *)
1.211 +
1.212 +(* 9.3.00
1.213 + compare d and dsc in pbt and transfer field to pre-ori *)
1.214 +fun add_field thy pbt (d,ts) =
1.215 + let fun eq d pt = (d = (fst o snd) pt);
1.216 + in case filter (eq d) pbt of
1.217 + [(fi,(dsc,_))] => (fi,d,ts)
1.218 + | [] => ("#undef",d,ts) (*may come with met.ppc*)
1.219 + | _ => raise error ("add_field: "^
1.220 + (Sign.string_of_term (sign_of thy) d)^
1.221 + " more than once in pbt")
1.222 + end;
1.223 +
1.224 +(*. take over field from met.ppc at 'Specify_Method' into ori,
1.225 + i.e. also removes "#undef" fields .*)
1.226 +(* val (mpc, ori) = ((#ppc o get_met) mID, oris);
1.227 + *)
1.228 +fun add_field' thy mpc (ori:ori list) =
1.229 + let fun eq d pt = (d = (fst o snd) pt);
1.230 + fun repl mpc (i,v,_,d,ts) =
1.231 + case filter (eq d) mpc of
1.232 + [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
1.233 + | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
1.234 + (*raise error ("add_field': "^
1.235 + (Sign.string_of_term (sign_of thy) d)^
1.236 + " not in met"*)
1.237 + | _ => raise error ("add_field': "^
1.238 + (Sign.string_of_term (sign_of thy) d)^
1.239 + " more than once in met");
1.240 + in (flat ((map (repl mpc)) ori)):ori list end;
1.241 +
1.242 +
1.243 +(*.mark an element with the position within a plateau;
1.244 + a plateau with length 1 is marked with 0 .*)
1.245 +fun mark eq [] = raise error "mark []"
1.246 + | mark eq xs =
1.247 + let
1.248 + fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
1.249 + | mar xx eq (x::x'::xs) n =
1.250 + if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)
1.251 + else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1;
1.252 + in mar [] eq xs 1 end;
1.253 +(*
1.254 +> val xs = [1,1,1,2,4,4,5];
1.255 +> mark (op=) xs;
1.256 +val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
1.257 +*)
1.258 +
1.259 +(*.assumes equal descriptions to be in adjacent 'plateaus',
1.260 + items at a certain position within the plateaus form a variant;
1.261 + length = 1 ... marked with 0: covers all variants .*)
1.262 +fun add_variants fdts =
1.263 + let
1.264 + fun eq (a,b) = curry op= (snd3 a) (snd3 b);
1.265 + in mark eq fdts end;
1.266 +
1.267 +(* collect equal elements: the model for coll_variants *)
1.268 +fun coll eq xs =
1.269 + let
1.270 + fun col xs eq x [] = xs @ [x]
1.271 + | col xs eq x (y::ys) =
1.272 + if eq(x,y) then col xs eq x ys
1.273 + else col (xs @ [x]) eq y ys;
1.274 + in col [] eq (hd xs) xs end;
1.275 +(*
1.276 +> val xs = [1,1,1,2,4,4,4];
1.277 +> coll (op=) xs;
1.278 +val it = [1,2,4] : int list
1.279 +*)
1.280 +
1.281 +fun max [] = raise error "max of []"
1.282 + | max (y::ys) =
1.283 + let fun mx x [] = x
1.284 + | mx x (y::ys) = if x < y then mx y ys else mx x ys;
1.285 +in mx y ys end;
1.286 +fun gen_max _ [] = raise error "gen_max of []"
1.287 + | gen_max ord (y::ys) =
1.288 + let fun mx x [] = x
1.289 + | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
1.290 +in mx y ys end;
1.291 +
1.292 +
1.293 +
1.294 +(* assumes *)
1.295 +fun coll_variants (((v,x)::vxs)) =
1.296 + let
1.297 + fun col xs (vs,x) [] = xs @ [(vs,x)]
1.298 + | col xs (vs,x) ((v',x')::vxs') =
1.299 + if x=x' then col xs (vs @ [v'], x') vxs'
1.300 + else col (xs @ [(vs,x)]) ([v'], x') vxs';
1.301 + in col [] ([v],x) vxs end;
1.302 +(* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
1.303 +> col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);
1.304 +val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *)
1.305 +
1.306 +
1.307 +fun replace_0 vm [0] = intsto vm
1.308 + | replace_0 vm vs = vs;
1.309 +
1.310 +fun add_id [] = raise error "add_id []"
1.311 + | add_id xs =
1.312 + let fun add n [] = []
1.313 + | add n (x::xs) = (n,x) :: add (n+1) xs;
1.314 +in add 1 xs end;
1.315 +(*
1.316 +> val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
1.317 +> add_id xs;
1.318 +val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]
1.319 + *)
1.320 +
1.321 +fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e);
1.322 +fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e);
1.323 +fun flat3 (a,(b,c)) = (a,b,c);
1.324 +(*
1.325 + val pI = pI';
1.326 + !pbts;
1.327 +*)
1.328 +(* in root (only!) fmz may be empty: fill with ..,dsc,[]
1.329 +fun init_ori fmz thy pI =
1.330 + if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*)
1.331 + else
1.332 + let
1.333 + val fds = map (cons2 (fst, fst o snd)) (get_pbt pI);
1.334 + val vfds = map ((pair [1]) o (rpair [])) fds;
1.335 + val ivfds = add_id vfds
1.336 + in (map flattup' ivfds):ori list end; 10.3.00---*)
1.337 +(* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];
1.338 + val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
1.339 + val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
1.340 + *)
1.341 +fun prep_ori [] _ _ = []
1.342 + | prep_ori fmz thy pbt =
1.343 + let
1.344 + val ctopts = map (parse thy) fmz
1.345 + val _= (*FIXME.WN060916 improve error report*)
1.346 + if null (filter is_none ctopts) then ()
1.347 + else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
1.348 + val dts = map ((split_dts thy) o term_of o the) ctopts
1.349 + val ori = map (add_field thy pbt) dts;
1.350 +(* val ori = map (flat3 o (pair "#undef")) dts; *)
1.351 + val ori' = add_variants ori;
1.352 + val maxv = max (map fst ori');
1.353 + val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv;
1.354 + val ori'' = coll_variants ori';
1.355 + val ori''' = map (apfst (replace_0 maxv)) ori'';
1.356 + val ori'''' = add_id ori'''
1.357 + in (map flattup ori''''):ori list end;
1.358 +
1.359 +
1.360 +(*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
1.361 +
1.362 +(*.the pattern for an item of a problems model or a methods guard.*)
1.363 +type pat = (string * (*field*)
1.364 + (term * (*description*)
1.365 + term)) (*id | struct-var*);
1.366 +fun pat2str ((field, (dsc, id)):pat) =
1.367 + pair2str (field, pair2str (term2str dsc, term2str id));
1.368 +fun pats2str pats = (strs2str o (map pat2str)) pats;
1.369 +
1.370 +(* data for methods stored in 'methods'-database *)
1.371 +type met =
1.372 + {guh : guh, (*unique within this isac-knowledge *)
1.373 + mathauthors: string list,(*copyright *)
1.374 + init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
1.375 + rew_ord' : rew_ord', (*for rules in Detail
1.376 + TODO.WN0509 store fun itself, see 'type pbt'*)
1.377 + erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
1.378 + instead erls in "fun prep_met" *)
1.379 + srls : rls, (*for evaluating list expressions in scr *)
1.380 + prls : rls, (*for evaluating predicates in modelpattern *)
1.381 + crls : rls, (*for check_elementwise, ie. formulae in calc.*)
1.382 + nrls : rls, (*canonical simplifier specific for this met *)
1.383 + calc : calc list, (*040207: <--- calclist' in fun prep_met *)
1.384 + (*branch : TransitiveB set in append_problem at generation ob pblobj
1.385 + FIXXXME.8.03: set branch from met in Apply_Method *)
1.386 +
1.387 + (* compare type pbt:*)
1.388 + ppc: pat list,
1.389 + (*.items in given, find, relate;
1.390 + items (in "#Find") which need not occur in the arg-list of a SubProblem
1.391 + are 'copy-named' with an identifier "*_!_".
1.392 + copy-named items are 'generating' if they are NOT "*___"
1.393 + see ME/calchead.sml 'fun is_copy_named'.*)
1.394 + pre: term list, (*preconditions in where*)
1.395 + (*script*)
1.396 + scr: scr (*prep_met requires either script or string "empty_script"*)
1.397 + };
1.398 +(* ------- template ------------------------------------------------------
1.399 +store_met
1.400 + (prep_met *.thy
1.401 + ([(*"EqSystem","normalize"*)],
1.402 + [("#Given" ,[ (*"equalities es_", "solveForVars vs_"*)]),
1.403 + ("#Find" ,[ (*dont forget typing non-reals *)]),
1.404 + ("#Relate",[])(*may be omitted *) ],
1.405 + {calc = [], (*filled autom. in prep_met *)
1.406 + crls = Erls, (*for check_elementwise *)
1.407 + prls = Erls, (*for evaluating preds in guard *)
1.408 + nrls = Erls, (*can.simplifier for all formulae*)
1.409 + rew_ord'="tless_true", (*for rules in Detail *)
1.410 + rls' = Erls, (*erls, the eval_rls for cond. in rules*)
1.411 + srls = Erls}, (*for evaluating list expr in scr*)
1.412 + "empty_script"
1.413 + ));
1.414 +---------- template ----------------------------------------------------*)
1.415 +val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
1.416 + rew_ord' = "e_rew_ord'": rew_ord',
1.417 + erls = e_rls, srls = e_rls, prls = e_rls,
1.418 + calc = [], crls = e_rls, nrls = e_rls,
1.419 + (*asm_thm = []: thm' list,
1.420 + asm_rls = []: rls' list,*)
1.421 + ppc = []: (string * (term * term)) list,
1.422 + pre = []: term list,
1.423 + scr = EmptyScr: scr}:met;
1.424 +
1.425 +
1.426 +(** problem-types stored in format for usage in specify **)
1.427 +(*25.8.01 ----
1.428 +val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
1.429 + (term * (* description *)
1.430 + term)) (* id | struct-var *)
1.431 + list)
1.432 + ) list);*)
1.433 +
1.434 +(*deprecated due to 'type pat'*)
1.435 +type pbt_ = (string * (* field "#Given",..*)
1.436 + (term * (* description *)
1.437 + term)); (* id | struct-var *)
1.438 +val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_;
1.439 +type pbt =
1.440 + {guh : guh, (*unique within this isac-knowledge*)
1.441 + mathauthors: string list, (*copyright*)
1.442 + init : pblID, (*to start refinement with*)
1.443 + thy : theory, (* which allows to compile that pbt
1.444 + TODO: search generalized for subthy (ref.p.69*)
1.445 + (*^^^ WN050912 NOT used during application of the problem,
1.446 + because applied terms may be from 'subthy' as well as from super;
1.447 + thus we take 'maxthy'; see match_ags !*)
1.448 + cas : term option,(*'CAS-command'*)
1.449 + prls : rls, (* for preds in where_*)
1.450 + where_: term list, (* where - predicates*)
1.451 + ppc : pat list,
1.452 + (*this is the model-pattern;
1.453 + it contains "#Given","#Where","#Find","#Relate"-patterns*)
1.454 + met : metID list}; (* methods solving the pbt*)
1.455 +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy,
1.456 + cas=None,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
1.457 +fun pbt2 (str, (t1, t2)) =
1.458 + pair2str (str, pair2str (term2str t1, term2str t2));
1.459 +fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;
1.460 +
1.461 +
1.462 +val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]);
1.463 +val e_Mets = Ptyp ("e_metID",[e_met],[]);
1.464 +
1.465 +type ptyps = (pbt ptyp) list;
1.466 +val ptyps = ref ([e_Ptyp]:ptyps);
1.467 +
1.468 +type mets = (met ptyp) list;
1.469 +val mets = ref ([e_Mets]:mets);
1.470 +
1.471 +
1.472 +(**+ breadth-first search on hierarchy of problem-types +**)
1.473 +
1.474 +type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)
1.475 + (* eg. ["equations","univariate","normalize"] while
1.476 + ["normalize","univariate","equations"] is the related pblID
1.477 + WN.24.4.03: also used for metID*)
1.478 +
1.479 +fun get_py thy d _ [] =
1.480 + error ("get_pbt not found: "^(strs2str d))
1.481 + | get_py thy d [k] ((Ptyp (k',[py],_))::pys) =
1.482 + if k=k' then py
1.483 + else get_py thy d ([k]:pblRD) pys
1.484 + | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') =
1.485 + if k=k' then get_py thy d ks pys
1.486 + else get_py thy d (k::ks) pys';
1.487 +(*> ptyps:=
1.488 +[Ptyp ("1",[("ptyp 1",([],[]))],
1.489 + [Ptyp ("11",[("ptyp 11",([],[]))],
1.490 + [])
1.491 + ]),
1.492 + Ptyp ("2",[("ptyp 2",([],[]))],
1.493 + [Ptyp ("21",[("ptyp 21",([],[]))],
1.494 + [])
1.495 + ])
1.496 + ];
1.497 +> get_py SqRoot.thy ["1"] ["1"] (!ptyps);
1.498 +> get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);
1.499 + _REVERSE_ .......... !!!!!!!!!!*)
1.500 +
1.501 +(*TODO: search generalized for subthy*)
1.502 +fun get_pbt (pblID:pblID) =
1.503 + let val pblRD = rev pblID;
1.504 + in get_py ProtoPure.thy pblID pblRD (!ptyps) end;
1.505 +(* get_pbt thy ["1"];
1.506 + get_pbt thy ["21","2"];
1.507 + *)
1.508 +
1.509 +(*TODO: throws exn 'get_pbt not found: ' ... confusing !!
1.510 + take 'ketype' as an argument !!!!!*)
1.511 +fun get_met (metID:metID) = get_py ProtoPure.thy metID metID (!mets);
1.512 +fun get_the (theID:theID) = get_py ProtoPure.thy theID theID (!thehier);
1.513 +
1.514 +
1.515 +
1.516 +fun del_eq k ptyps =
1.517 +let fun del k ptyps [] = ptyps
1.518 + | del k ptyps ((Ptyp (k', [p], ps))::pys) =
1.519 + if k=k' then del k ptyps pys
1.520 + else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
1.521 +in del k [] ptyps end;
1.522 +
1.523 +fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])]
1.524 +
1.525 + | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
1.526 +((*writeln("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
1.527 + if k=k'
1.528 + then ((Ptyp (k', [pbt], ps))::pys)
1.529 + else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
1.530 + ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
1.531 +)
1.532 + | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
1.533 +((*writeln("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
1.534 + if k=k'
1.535 + then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
1.536 + else
1.537 + if length pys = 0
1.538 + then error ("insert: not found "^(strs2str (d:pblID)))
1.539 + else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
1.540 +);
1.541 +
1.542 +
1.543 +fun coll_pblguhs pbls =
1.544 + let fun node coll (Ptyp (_,[n],ns)) =
1.545 + [(#guh : pbt -> guh) n] @ (nodes coll ns)
1.546 + and nodes coll [] = coll
1.547 + | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.548 + in nodes [] pbls end;
1.549 +fun coll_metguhs mets =
1.550 + let fun node coll (Ptyp (_,[n],ns)) =
1.551 + [(#guh : met -> guh) n]
1.552 + and nodes coll [] = coll
1.553 + | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.554 + in nodes [] mets end;
1.555 +
1.556 +(*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
1.557 +fun guh2kestoreID (guh:guh) =
1.558 + case (implode o (take_fromto 1 4) o explode) guh of
1.559 + "pbl_" =>
1.560 + let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
1.561 + if gu = guh
1.562 + then Some ((ids@[id]) : kestoreID)
1.563 + else nodes (ids@[id]) gu ns
1.564 + and nodes _ _ [] = None
1.565 + | nodes ids gu (n::ns) =
1.566 + case node ids gu n of Some id => Some id
1.567 + | None => nodes ids gu ns
1.568 + in case nodes [] guh (!ptyps) of
1.569 + Some id => rev id
1.570 + | None => error ("guh2kestoreID: '" ^ guh ^ "' " ^
1.571 + "not found in (!ptyps)")
1.572 + end
1.573 + | "met_" =>
1.574 + let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =
1.575 + if gu = guh
1.576 + then Some ((ids@[id]) : kestoreID)
1.577 + else nodes (ids@[id]) gu ns
1.578 + and nodes _ _ [] = None
1.579 + | nodes ids gu (n::ns) =
1.580 + case node ids gu n of Some id => Some id
1.581 + | None => nodes ids gu ns
1.582 + in case nodes [] guh (!mets) of
1.583 + Some id => id
1.584 + | None => error ("guh2kestoreID: '" ^ guh ^ "' " ^
1.585 + "not found in (!mets)") end
1.586 + | _ => error ("guh2kestoreID called with '" ^ guh ^ "'");
1.587 +(*> guh2kestoreID "pbl_equ_univ_lin";
1.588 +val it = ["linear", "univariate", "equation"] : string list*)
1.589 +
1.590 +
1.591 +fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
1.592 + if guh mem (coll_pblguhs pbls)
1.593 + then error ("check_guh_unique failed with '"^guh^"';\n"^
1.594 + "use 'sort_pblguhs()' for a list of guhs;\n"^
1.595 + "consider setting 'check_guhs_unique := false'")
1.596 + else ();
1.597 +(* val (guh, mets) = ("met_test", !mets);
1.598 + *)
1.599 +fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
1.600 + if guh mem (coll_metguhs mets)
1.601 + then error ("check_guh_unique failed with '"^guh^"';\n"^
1.602 + "use 'sort_metguhs()' for a list of guhs;\n"^
1.603 + "consider setting 'check_guhs_unique := false'")
1.604 + else ();
1.605 +
1.606 +
1.607 +
1.608 +(*.the pblID has the leaf-element as first; better readability achieved;.*)
1.609 +fun store_pbt (pbt as {guh,...}, pblID) =
1.610 + (if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else ();
1.611 + ptyps:= insrt pblID pbt (rev pblID) (!ptyps));
1.612 +
1.613 +(*.the metID has the root-element as first; compare 'fun store_pbt'.*)
1.614 +(* val (met as {guh,...}, metID) =
1.615 + ((prep_met EqSystem.thy "met_eqsys" [] e_metID
1.616 + (["EqSystem"],
1.617 + [],
1.618 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.619 + srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
1.620 + "empty_script"
1.621 + )));
1.622 + *)
1.623 +fun store_met (met as {guh,...}, metID) =
1.624 + (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
1.625 + mets:= insrt metID met metID (!mets));
1.626 +
1.627 +
1.628 +(*. prepare problem-types before storing in pbltypes;
1.629 + dont forget to 'check_guh_unique' before ins.*)
1.630 +fun prep_pbt thy guh maa init
1.631 + (pblID, dsc_dats: (string * (string list)) list,
1.632 + ev:rls, ca: string option, metIDs:metID list) =
1.633 +(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
1.634 + ev:rls, ca: string option, metIDs:metID list)) =
1.635 + ((EqSystem.thy, (["system"],
1.636 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.637 + ("#Find" ,["solution ss___"](*___ is copy-named*))
1.638 + ],
1.639 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.640 + Some "solveSystem es_ vs_",
1.641 + [])));
1.642 + *)
1.643 + let fun eq f (f', _) = f = f';
1.644 + val gi = filter (eq "#Given") dsc_dats;
1.645 +(*val gi = [("#Given",["equality e_","solveFor v_"])]
1.646 + : (string * string list) list*)
1.647 + val gi = (case gi of
1.648 + [] => []
1.649 + | ((_,gi')::[]) =>
1.650 + ((map (split_did o term_of o the o (parse thy)) gi')
1.651 + handle _ => error
1.652 + ("prep_pbt: syntax error in '#Given' of "^
1.653 + (strs2str pblID)))
1.654 + | _ =>
1.655 + (error ("prep_pbt: more than one '#Given' in "^
1.656 + (strs2str pblID))));
1.657 +(*val gi =
1.658 + [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")),
1.659 + (Const ("Descript.solveFor","RealDef.real => Tools.una"),
1.660 + Free ("v_","RealDef.real"))] : (term * term) list *)
1.661 + val gi = map (pair "#Given") gi;
1.662 +(*val gi =
1.663 + [("#Given",
1.664 + (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))),
1.665 + ("#Given",
1.666 + (Const ("Descript.solveFor","RealDef.real => Tools.una"),
1.667 + Free ("v_","RealDef.real")))] : (string * (term * term)) list*)
1.668 +
1.669 + val fi = filter (eq "#Find") dsc_dats;
1.670 + val fi = (case fi of
1.671 + [] => [](*28.8.01: ["tool"] ...// raise error
1.672 + ("prep_pbt: no '#Find' in "^(strs2str pblID))*)
1.673 +(* val ((_,fi')::[]) = fi;
1.674 + *)
1.675 + | ((_,fi')::[]) =>
1.676 + ((map (split_did o term_of o the o (parse thy)) fi')
1.677 + handle _ => raise error
1.678 + ("prep_pbt: syntax error in '#Find' of "^
1.679 + (strs2str pblID)))
1.680 + | _ =>
1.681 + (raise error ("prep_pbt: more than one '#Find' in "^
1.682 + (strs2str pblID))));
1.683 + val fi = map (pair "#Find") fi;
1.684 +
1.685 + val re = filter (eq "#Relate") dsc_dats;
1.686 + val re = (case re of
1.687 + [] => []
1.688 + | ((_,re')::[]) =>
1.689 + ((map (split_did o term_of o the o (parse thy)) re')
1.690 + handle _ => raise error
1.691 + ("prep_pbt: syntax error in '#Relate' of "^
1.692 + (strs2str pblID)))
1.693 + | _ =>
1.694 + (raise error ("prep_pbt: more than one '#Relate' in "^
1.695 + (strs2str pblID))));
1.696 + val re = map (pair "#Relate") re;
1.697 +
1.698 + val wh = filter (eq "#Where") dsc_dats;
1.699 + val wh = (case wh of
1.700 + [] => []
1.701 + | ((_,wh')::[]) =>
1.702 + ((map (term_of o the o (parse thy)) wh')
1.703 + handle _ => raise error
1.704 + ("prep_pbt: syntax error in '#Where' of "^
1.705 + (strs2str pblID)))
1.706 + | _ =>
1.707 + (raise error ("prep_pbt: more than one '#Where' in "^
1.708 + (strs2str pblID))));
1.709 + in ({guh=guh,mathauthors=maa,init=init,
1.710 + thy=thy,cas= case ca of None => None
1.711 + | Some s =>
1.712 + Some ((term_of o the o (parse thy)) s),
1.713 + prls=ev,where_=wh,ppc= gi @ fi @ re,
1.714 + met=metIDs}, pblID):pbt * pblID end;
1.715 +(* prep_pbt thy (pblID, dsc_dats, metIDs);
1.716 + val it =
1.717 + ({met=[],
1.718 + ppc=[("#Given",(Const (#,#),Free (#,#))),
1.719 + ("#Given",(Const (#,#),Free (#,#))),
1.720 + ("#Find",(Const (#,#),Free (#,#)))],
1.721 + thy={ProtoPure, ..., Atools, RatArith},
1.722 + where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $
1.723 + Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *)
1.724 +
1.725 +
1.726 +
1.727 +
1.728 +(*. prepare met for storage analogous to pbt .*)
1.729 +fun prep_met thy guh maa init
1.730 + (metID, ppc: (string * string list) list (*'#Where' -> #pre*),
1.731 + {rew_ord'=ro, rls'=rls, srls=srls, prls=prls,
1.732 + calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
1.733 + crls=cr, nrls=nr}, scr) =
1.734 + let fun eq f (f', _) = f = f';
1.735 + (*val thy = (assoc_thy o fst) metID*)
1.736 + val gi = filter (eq "#Given") ppc;
1.737 + val gi = (case gi of
1.738 + [] => []
1.739 + | ((_,gi')::[]) =>
1.740 + ((map (split_did o term_of o the o (parse thy)) gi')
1.741 + handle _ => raise error
1.742 + ("prep_pbt: syntax error in '#Given' of "^
1.743 + (strs2str metID)))
1.744 + | _ =>
1.745 + (raise error ("prep_pbt: more than one '#Given' in "^
1.746 + (strs2str metID))));
1.747 + val gi = map (pair "#Given") gi;
1.748 +
1.749 + val fi = filter (eq "#Find") ppc;
1.750 + val fi = (case fi of
1.751 + [] => [](*28.8.01: ["tool"] ...// raise error
1.752 + ("prep_pbt: no '#Find' in "^(strs2str metID))*)
1.753 + | ((_,fi')::[]) =>
1.754 + ((map (split_did o term_of o the o (parse thy)) fi')
1.755 + handle _ => raise error
1.756 + ("prep_pbt: syntax error in '#Find' of "^
1.757 + (strs2str metID)))
1.758 + | _ =>
1.759 + (raise error ("prep_pbt: more than one '#Find' in "^
1.760 + (strs2str metID))));
1.761 + val fi = map (pair "#Find") fi;
1.762 +
1.763 + val re = filter (eq "#Relate") ppc;
1.764 + val re = (case re of
1.765 + [] => []
1.766 + | ((_,re')::[]) =>
1.767 + ((map (split_did o term_of o the o (parse thy)) re')
1.768 + handle _ => raise error
1.769 + ("prep_pbt: syntax error in '#Relate' of "^
1.770 + (strs2str metID)))
1.771 + | _ =>
1.772 + (raise error ("prep_pbt: more than one '#Relate' in "^
1.773 + (strs2str metID))));
1.774 + val re = map (pair "#Relate") re;
1.775 +
1.776 + val wh = filter (eq "#Where") ppc;
1.777 + val wh = (case wh of
1.778 + [] => []
1.779 + | ((_,wh')::[]) =>
1.780 + ((map (term_of o the o (parse thy)) wh')
1.781 + handle _ => raise error
1.782 + ("prep_pbt: syntax error in '#Where' of "^
1.783 + (strs2str metID)))
1.784 + | _ =>
1.785 + (raise error ("prep_pbt: more than one '#Where' in "^
1.786 + (strs2str metID))));
1.787 + val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
1.788 + in ({guh=guh,mathauthors=maa,init=init,
1.789 + ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
1.790 + calc = if scr = "empty_script" then []
1.791 + else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
1.792 + (filter is_calc) o stacpbls) sc,
1.793 + crls=cr, nrls=nr, scr=Script sc}:met,
1.794 + metID:metID)
1.795 + end;
1.796 +
1.797 +
1.798 +(**. get pblIDs of all entries in mat3D .**)
1.799 +
1.800 +
1.801 +fun format_pblID strl = enclose " [" "]" (commas_quote strl);
1.802 +fun format_pblIDl strll = enclose "[\n" "\n]\n"
1.803 + (space_implode ",\n" (map format_pblID strll));
1.804 +
1.805 +fun scan _ [] = [] (* no base case, for empty doms only *)
1.806 + | scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]]
1.807 + | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl
1.808 + | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
1.809 + | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
1.810 +
1.811 +fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);
1.812 +(* ptyps:=[];
1.813 + show_ptyps();
1.814 + *)
1.815 +fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);
1.816 +
1.817 +
1.818 +
1.819 +(*vvvvv---------- preparational work 8.01. UNUSED *)
1.820 +(**+ instantiate a problem-type +**)
1.821 +
1.822 +(*+ transform oris +*)
1.823 +
1.824 +fun coll_vats (vats, ((_,vs,_,_,_):ori)) = vats union vs;
1.825 +(*> coll_vats [11,22] (hd oris);
1.826 +val it = [22,11,1,2,3] : int list
1.827 +
1.828 +> foldl coll_vats ([],oris);
1.829 +val it = [1,2,3] : int list
1.830 +
1.831 +> val i=1;
1.832 +> filter ((curry (op mem) i) o #2) oris;
1.833 +val it =
1.834 + [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.835 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.836 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.837 + (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
1.838 + (6,[1],"#undef",Const (#,#),[Free #]),
1.839 + (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.840 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
1.841 +
1.842 +fun filter_vat oris i = filter ((curry (op mem) i)o(#2:ori -> int list))oris;
1.843 +(*> map (filter_vat oris) [1,2,3];
1.844 +val it =
1.845 + [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.846 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.847 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.848 + (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
1.849 + (6,[1],"#undef",Const (#,#),[Free #]),
1.850 + (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.851 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
1.852 + [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.853 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.854 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.855 + (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
1.856 + (7,[2],"#undef",Const (#,#),[Free #]),
1.857 + (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.858 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
1.859 + [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.860 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.861 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.862 + (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
1.863 + (8,[3],"#undef",Const (#,#),[Free #]),
1.864 + (10,[3],"#undef",Const (#,#),[# $ #]),
1.865 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
1.866 +
1.867 +
1.868 +fun separate_vats oris =
1.869 + let val vats = foldl coll_vats ([],oris);
1.870 + in map (filter_vat oris) vats end;
1.871 +(*^^^ end preparational work 8.01.*)
1.872 +
1.873 +
1.874 +
1.875 +(**. check a problem (ie. itm list) for matching a problemtype .**)
1.876 +
1.877 +fun eq1 d (_,(d',_)) = (d = d');
1.878 +fun itm_id ((i,_,_,_,_):itm) = i;
1.879 +fun ori_id ((i,_,_,_,_):ori) = i;
1.880 +fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm);
1.881 +(*see + add_sel_ppc ~~~~~~~*)
1.882 +fun field_eq f ((_,_,f',_,_):ori) = f = f';
1.883 +
1.884 +(*. check an item (with arbitrary itm_ from previous matchings)
1.885 + for matching a problemtype; returns true only for itms found in pbt .*)
1.886 +fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
1.887 + (case find_first (eq1 d) pbt of
1.888 + Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
1.889 + (id, pbl_ids' thy d vs))):itm)
1.890 + | None => (i,vats,false,f,Sup (d,vs)))
1.891 + | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
1.892 + (case find_first (eq1 d) pbt of
1.893 + Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
1.894 + (id, pbl_ids' thy d vs))):itm)
1.895 + | None => (i,vats,false,f,Sup (d,vs)))
1.896 +
1.897 + | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
1.898 + | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm
1.899 +
1.900 + | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
1.901 + (case find_first (eq1 d) pbt of
1.902 + Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
1.903 + (id, pbl_ids' thy d vs))):itm)
1.904 + | None => (i,vats,false,f,Sup (d,vs)))
1.905 +(* val (i,vats,b,f,Mis (d,vs)) = i4;
1.906 + *)
1.907 + | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
1.908 + (case find_first (eq1 d) pbt of
1.909 +(* val Some (_,(_,id)) = find_first (eq1 d) pbt;
1.910 + *)
1.911 + Some (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
1.912 + \(id, pbl_ids' d vs))):itm)"
1.913 + | None => (i,vats,false,f,Sup (d,[vs])));
1.914 +
1.915 +(* chk_ thy pbt i
1.916 + *)
1.917 +
1.918 +fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1.919 +fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
1.920 +fun eq0 ((0,_,_,_,_):itm) = true
1.921 + | eq0 _ = false;
1.922 +fun max_i i [] = i
1.923 + | max_i i ((id,_,_,_,_)::is) =
1.924 + if i > id then max_i i is else max_i id is;
1.925 +fun max_id [] = 0
1.926 + | max_id ((id,_,_,_,_)::is) = max_i id is;
1.927 +fun add_idvat itms _ _ [] = itms
1.928 + | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) =
1.929 + add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *)
1.930 + ],b,f,itm_):itm]) (i+1) mvat its;
1.931 +
1.932 +
1.933 +(*. find elements of pbt not contained in itms;
1.934 + if such one is untouched, return this one, otherwise create new itm .*)
1.935 +fun chk_m (itms:itm list) untouched (p as (f,(d,id))) =
1.936 + case find_first (eq2 p) itms of
1.937 + Some _ => []
1.938 + | None => (case find_first (eq2 p) untouched of
1.939 + Some itm => [itm]
1.940 + | None => [(0,[],false,f,Mis (d,id)):itm]);
1.941 +(* val itms = itms'';
1.942 + *)
1.943 +fun chk_mis mvat itms untouched pbt =
1.944 + let val mis = (flat o (map (chk_m itms untouched))) pbt;
1.945 + val mid = max_id itms;
1.946 + in add_idvat [] (mid + 1) mvat mis end;
1.947 +
1.948 +(*. check a problem (ie. itm list) for matching a problemtype,
1.949 + takes the max_vt for concluding completeness (could be another!) .*)
1.950 +(* val itms = itms'; val (pbt,pre) = (ppc, pre);
1.951 + val itms = itms; val (pbt,pre) = (ppc, pre);
1.952 + *)
1.953 +fun match_itms thy itms (pbt,pre,prls) =
1.954 + (let fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b;
1.955 + val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
1.956 + val mvat = max_vt itms';
1.957 + val itms'' = filter (okv mvat) itms';
1.958 + val untouched = filter eq0 itms;(*i.e. dsc only (from init)*)
1.959 + val mis = chk_mis mvat itms'' untouched pbt;
1.960 + val pre' = check_preconds' prls pre itms'' mvat
1.961 + val pb = foldl and_ (true, map fst pre')
1.962 + in (length mis = 0 andalso pb, (itms'@ mis, pre')) end);
1.963 +
1.964 +(*. check a problem pbl (ie. itm list) for matching a problemtype pbt,
1.965 + for missing items get data from formalization (ie. ori list);
1.966 + takes the max_vt for concluding completeness (could be another!) .*)
1.967 +(* (0) determine the most frequent variant mv in pbl
1.968 + ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1.969 + (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
1.970 + (3) newitms = filter (mv mem vat(news)) news
1.971 + (4) pbt @ newitms *)
1.972 +(* val (pbl, pbt, pre) = (met, mtt, pre);
1.973 + val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt);
1.974 + val (pbl, pbt, pre) = (itms, ppc, where_);
1.975 + *)
1.976 +fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris =
1.977 + let
1.978 + (*0*)val mv = max_vt pbl;
1.979 +
1.980 + fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1.981 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1.982 + Some _ => false | None => true;
1.983 + (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;
1.984 +
1.985 + fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
1.986 + fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) =
1.987 + (i,v,false,f,Mis (d,pid)):itm;
1.988 + (*2*)fun oris2itms oris mis1 =
1.989 + ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
1.990 + val news = (flat o (map (oris2itms oris))) mis;
1.991 + (*3*)fun mem_vat (_,vats,b,_,_) = mv mem vats;
1.992 + val newitms = filter mem_vat news;
1.993 + (*4*)val itms' = pbl @ newitms;
1.994 + val pre' = check_preconds' prls pre itms' mv
1.995 + val pb = foldl and_ (true, map fst pre')
1.996 + in (length mis = 0 andalso pb, (itms', pre')) end;
1.997 + (*handle _ => (false,([],[]))*);
1.998 +
1.999 +
1.1000 +(*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris
1.1001 + allow for faster access to descriptions and terms *)
1.1002 +(**. check a problem (ie. itm list) for matching a problemtype .**)
1.1003 +
1.1004 +(*. check an ori for matching a problemtype by description;
1.1005 + returns true only for itms found in pbt .*)
1.1006 +fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
1.1007 + case find_first (eq1 d) pbt of
1.1008 + Some (_,(_,id)) => [(i,vats,true,f,
1.1009 + Cor ((d,vs), (id, pbl_ids' thy d vs))):itm]
1.1010 + | None => [];
1.1011 +
1.1012 +(* elem 'p' of pbt contained in itms ? *)
1.1013 +fun chk1_m (itms:itm list) p =
1.1014 + case find_first (eq2 p) itms of
1.1015 + Some _ => true | None => false;
1.1016 +fun chk1_m' (oris: ori list) (p as (f,(d,t))) =
1.1017 + case find_first (eq2' p) oris of
1.1018 + Some _ => []
1.1019 + | None => [(f, Mis (d, t))];
1.1020 +fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;
1.1021 +
1.1022 +fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
1.1023 +fun chk1_mis' oris ppc =
1.1024 + map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
1.1025 +
1.1026 +
1.1027 +(*. check a problem (ie. ori list) for matching a problemtype,
1.1028 + takes the max_vt for concluding completeness (FIXME could be another!) .*)
1.1029 +(* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py);
1.1030 + *)
1.1031 +fun match_oris thy prls oris (pbt,pre) =
1.1032 + let val itms = (flat o (map (chk1_ thy pbt))) oris;
1.1033 + val mvat = max_vt itms;
1.1034 + val complete = chk1_mis mvat itms pbt;
1.1035 + val pre' = check_preconds' prls pre itms mvat
1.1036 + val pb = foldl and_ (true, map fst pre')
1.1037 + in if complete andalso pb then true else false end;
1.1038 +(*run subp-rooteq.sml 'root-eq + subpbl: solve_linear'
1.1039 + until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"...
1.1040 +> val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_,
1.1041 + Nd(PblObj{origin=(oris,_,_),...},[])]) = pt;
1.1042 +> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1.1043 + (#where_ o get_pbt) ["linear","univariate","equation"]);
1.1044 +> match_oris oris (pbt,pre);
1.1045 +val it = true : bool
1.1046 +
1.1047 +
1.1048 +> val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"],
1.1049 + (#where_ o get_pbt)["plain_square","univariate","equation"]);
1.1050 +> match_oris oris (pbt,pre);
1.1051 +val it = false : bool
1.1052 +
1.1053 +
1.1054 + ---------------------------------------------------
1.1055 + run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square'
1.1056 + until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ...
1.1057 +> val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]),
1.1058 + Nd (PblObj {origin=(oris,_,_),...},[])]) = pt;
1.1059 +> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1.1060 + (#where_ o get_pbt) ["linear","univariate","equation"]);
1.1061 +> match_oris oris (pbt,pre);
1.1062 +val it = false : bool
1.1063 +
1.1064 +
1.1065 +> val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"],
1.1066 + (#where_ o get_pbt) ["plain_square","univariate","equation"]);
1.1067 +> match_oris oris (pbt,pre);
1.1068 +val it = true : bool
1.1069 +*)
1.1070 +(*^^^--- doubled 20.9.01 *)
1.1071 +
1.1072 +
1.1073 +(*. check a problem (ie. ori list) for matching a problemtype,
1.1074 + returns items for output to math-experts .*)
1.1075 +(* val (ppc,pre) = (#ppc py, #where_ py);
1.1076 + *)
1.1077 +fun match_oris' thy oris (ppc,pre,prls) =
1.1078 +(* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));
1.1079 + *)
1.1080 + let val itms = (flat o (map (chk1_ thy ppc))) oris;
1.1081 + val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris;
1.1082 + val mvat = max_vt itms;
1.1083 + val miss = chk1_mis' oris ppc;
1.1084 + val pre' = check_preconds' prls pre itms mvat
1.1085 + val pb = foldl and_ (true, map fst pre')
1.1086 + in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
1.1087 +
1.1088 +(*. for the user .*)
1.1089 +datatype match' =
1.1090 + Matches' of item ppc
1.1091 +| NoMatch' of item ppc;
1.1092 +
1.1093 +(*. match a formalization with a problem type .*)
1.1094 +fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
1.1095 + let val oris = prep_ori fmz thy ppc;
1.1096 + val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
1.1097 + in if bool then Matches' (itms2itemppc thy itms pre')
1.1098 + else NoMatch' (itms2itemppc thy itms pre') end;
1.1099 +(*
1.1100 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.1101 + "solveFor x","errorBound (eps=0)","solutions L"];
1.1102 +val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
1.1103 + get_pbt ["univariate","equation"];
1.1104 +match_pbl fmz pbt;
1.1105 +*)
1.1106 +
1.1107 +
1.1108 +(*. refine a problem; construct pblRD while scanning .*)
1.1109 +(* val (pblRD,ori)=("xxx",oris);
1.1110 + val py = get_pbt ["equation"];
1.1111 + val py = get_pbt ["univariate","equation"];
1.1112 + val py = get_pbt ["linear","univariate","equation"];
1.1113 + val py = get_pbt ["root","univariate","equation"];
1.1114 + match_oris (#prls py) ori (#ppc py, #where_ py);
1.1115 +
1.1116 + *)
1.1117 +fun refin (pblRD:pblRD) ori
1.1118 +((Ptyp (pI,[py],[])):pbt ptyp) =
1.1119 + if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
1.1120 + then Some ((pblRD @ [pI]):pblRD)
1.1121 + else None
1.1122 + | refin pblRD ori (Ptyp (pI,[py],pys)) =
1.1123 + if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
1.1124 + then (case refins (pblRD @ [pI]) ori pys of
1.1125 + Some pblRD' => Some pblRD'
1.1126 + | None => Some (pblRD @ [pI]))
1.1127 + else None
1.1128 +and refins pblRD ori [] = None
1.1129 + | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =
1.1130 + (case refin pblRD ori p of
1.1131 + Some pblRD' => Some pblRD'
1.1132 + | None => refins pblRD ori pts);
1.1133 +
1.1134 +(*. refine a problem; version providing output for math-experts .*)
1.1135 +fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
1.1136 +(* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
1.1137 + (rev ["linear","system"], fmz, [(*match list*)],
1.1138 + ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
1.1139 + *)
1.1140 + let val _ = (writeln o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
1.1141 + val {thy,ppc,where_,prls,...} = py
1.1142 + val oris = prep_ori fmz thy ppc
1.1143 + (*8.3.02: itms!: oris ev. are _not_ complete here*)
1.1144 + val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
1.1145 + in if b then pbls @ [Matches (rev (pblRD @ [pI]),
1.1146 + itms2itemppc thy itms pre')]
1.1147 + else pbls @ [NoMatch (rev (pblRD @ [pI]),
1.1148 + itms2itemppc thy itms pre')]
1.1149 + end
1.1150 +(* val pblRD = ["pbla"]; val fmz = fmz1; val pbls = [];
1.1151 + val Ptyp (pI,[py],pys) = hd (!ptyps);
1.1152 + refin' pblRD fmz pbls (Ptyp (pI,[py],pys));
1.1153 +*)
1.1154 + | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) =
1.1155 + let val _ = (writeln o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
1.1156 + val {thy,ppc,where_,prls,...} = py
1.1157 + val oris = prep_ori fmz thy ppc;
1.1158 + (*8.3.02: itms!: oris ev. are _not_ complete here*)
1.1159 + val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
1.1160 + in if b
1.1161 + then let val pbl = Matches (rev (pblRD @ [pI]),
1.1162 + itms2itemppc thy itms pre')
1.1163 + in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
1.1164 + else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
1.1165 + end
1.1166 +and refins' pblRD fmz pbls [] = pbls
1.1167 + | refins' pblRD fmz pbls ((p as Ptyp (pI,_,_))::pts) =
1.1168 + let val pbls' = refin' pblRD fmz pbls p
1.1169 + in case last_elem pbls' of
1.1170 + Matches _ => pbls'
1.1171 + | NoMatch _ => refins' pblRD fmz pbls' pts end;
1.1172 +
1.1173 +(*. refine a problem; version for tactic Refine_Problem .*)
1.1174 +fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
1.1175 + let (*val _ = writeln("### refin''1: pI="^pI);*)
1.1176 + val {thy,ppc,where_,prls,...} = py
1.1177 + val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
1.1178 + in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
1.1179 + else pbls @ [NoMatch_]
1.1180 + end
1.1181 +(* val pblRD = (rev o tl) pblID; val pbls = [];
1.1182 + val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);
1.1183 + *)
1.1184 + | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =
1.1185 + let (*val _ = writeln("### refin''2: pI="^pI);*)
1.1186 + val {thy,ppc,where_,prls,...} = py
1.1187 + val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
1.1188 + in if b
1.1189 + then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
1.1190 + in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
1.1191 + else (pbls @ [NoMatch_])
1.1192 + end
1.1193 +and refins'' thy pblRD itms pbls [] = pbls
1.1194 + | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) =
1.1195 + let val pbls' = refin'' thy pblRD itms pbls p
1.1196 + in case last_elem pbls' of
1.1197 + Match_ _ => pbls'
1.1198 + | NoMatch_ => refins'' thy pblRD itms pbls' pts end;
1.1199 +
1.1200 +
1.1201 +(*. apply a fun to a ptyps node; copied from get_py .*)
1.1202 +fun app_ptyp f (d:pblID) _ [] =
1.1203 + raise error ("app_ptyp not found: "^(strs2str d))
1.1204 + | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =
1.1205 + if k=k' then f p
1.1206 + else app_ptyp f d ([k]:pblRD) pys
1.1207 + | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') =
1.1208 + if k=k' then app_ptyp f d ks pys
1.1209 + else app_ptyp f d (k::ks) pys';
1.1210 +
1.1211 +(*. for tactic Refine_Tacitly .*)
1.1212 +(*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*)
1.1213 +(* val (thy,pblID) = (assoc_thy dI',pI);
1.1214 + *)
1.1215 +fun refine_ori oris (pblID:pblID) =
1.1216 + let val opt = app_ptyp (refin ((rev o tl) pblID) oris)
1.1217 + pblID (rev pblID) (!ptyps);
1.1218 + in case opt of
1.1219 + Some pblRD => let val (pblID':pblID) =(rev pblRD)
1.1220 + in if pblID' = pblID then None
1.1221 + else Some pblID' end
1.1222 + | None => None end;
1.1223 +fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
1.1224 +
1.1225 +(*. for tactic Refine_Problem .*);
1.1226 +(* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
1.1227 +(* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);
1.1228 + *)
1.1229 +fun refine_pbl thy (pblID:pblID) itms =
1.1230 + case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms [])
1.1231 + pblID (rev pblID) (!ptyps)) of
1.1232 + None => None
1.1233 + | Some (Match_ (rfd as (pI',_))) =>
1.1234 + if pblID = pI' then None else Some rfd;
1.1235 +
1.1236 +
1.1237 +(*. for math-experts .*)
1.1238 +(*19.10.02FIXME: needs thy for parsing fmz*)
1.1239 +(* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
1.1240 + val pbls = []; val ptys = !ptyps;
1.1241 + *)
1.1242 +fun refine (fmz:fmz_) (pblID:pblID) =
1.1243 + app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps);
1.1244 +
1.1245 +
1.1246 +(*.make a guh from a reference to an element in the kestore;
1.1247 + EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
1.1248 +fun pblID2guh (pblID:pblID) =
1.1249 + (((#guh o get_pbt) pblID)
1.1250 + handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
1.1251 +fun metID2guh (metID:metID) =
1.1252 + (((#guh o get_met) metID)
1.1253 + handle _ => raise error ("metID2guh: no 'Met_' for '"^
1.1254 + strs2str' metID ^ "'"));
1.1255 +fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
1.1256 + | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
1.1257 + | kestoreID2guh ketype kestoreID =
1.1258 + raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
1.1259 + strs2str' kestoreID ^ "'");
1.1260 +
1.1261 +fun show_pblguhs () =
1.1262 + (print_depth 999;
1.1263 + (writeln o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));
1.1264 + print_depth 3);
1.1265 +fun sort_pblguhs () =
1.1266 + (print_depth 999;
1.1267 + (writeln o strs2str o (map linefeed))
1.1268 + (((sort string_ord) o coll_pblguhs) (!ptyps));
1.1269 + print_depth 3);
1.1270 +
1.1271 +fun show_metguhs () =
1.1272 + (print_depth 999;
1.1273 + (writeln o strs2str o (map linefeed)) (coll_metguhs (!mets));
1.1274 + print_depth 3);
1.1275 +fun sort_metguhs () =
1.1276 + (print_depth 999;
1.1277 + (writeln o strs2str o (map linefeed))
1.1278 + (((sort string_ord) o coll_metguhs) (!mets));
1.1279 + print_depth 3);