1 (* the problems and methods as stored in hierarchies
2 author Walther Neuper 1998, Mathias Lehnfeld
3 (c) due to copyright terms
6 signature MODEL_SPECIFY =
8 val hack_until_review_Specify_1: Celem.metID -> Model.itm list -> Model.itm list
9 val hack_until_review_Specify_2: Celem.metID -> Model.itm list -> Model.itm list
11 val get_fun_ids : theory -> (string * typ) list
13 (* for calchead.sml, if below at left margin *)
14 val prep_ori : Selem.fmz_ -> theory -> field list -> Model.ori list * Proof.context
15 val add_id : 'a list -> (int * 'a) list
16 val add_field' : theory -> field list -> Model.ori list -> Model.ori list
17 val match_itms_oris : theory -> Model.itm list -> field list * term list * Rule_Set.T ->
18 Model.ori list -> bool * (Model.itm list * (bool * term) list)
19 val refine_ori : Model.ori list -> Celem.pblID -> Celem.pblID option
20 val refine_ori' : Model.ori list -> Celem.pblID -> Celem.pblID
21 val refine_pbl : theory -> Celem.pblID -> Model.itm list ->
22 (Celem.pblID * (Model.itm list * (bool * term) list)) option
24 val appc : ('a list -> 'b list) -> 'a Model.ppc -> 'b Model.ppc
25 val mappc : ('a -> 'b) -> 'a Model.ppc -> 'b Model.ppc
26 val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *)
28 val get_pbt : Celem.pblID -> Celem.pbt
29 val get_met : Celem.metID -> Celem.met (* for generate.sml *)
30 val get_met' : theory -> Celem.metID -> Celem.met (* for pbl-met-hierarchy.sml *)
31 val get_the : Celem.theID -> Celem.thydata (* for inform.sml *)
33 type pblRD = string list (* for pbl-met-hierarchy.sml *)
34 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
35 val scan : string list -> 'a Celem.ptyp list -> string list list (* for thy-hierarchy.sml *)
36 val itm_out : theory -> Model.itm_ -> string
37 val dsc_unknown : term
39 val pblID2guh : Celem.pblID -> Celem.guh (* for datatypes.sml *)
40 val metID2guh : Celem.metID -> Celem.guh (* for datatypes.sml *)
41 val kestoreID2guh : Celem.ketype -> Celem.kestoreID -> Celem.guh (* for datatypes.sml *)
42 val guh2kestoreID : Celem.guh -> string list (* for interface.sml *)
43 (* for Knowledge/, if below at left margin *)
44 val prep_pbt : theory -> Celem.guh -> string list -> Celem.pblID ->
45 string list * (string * string list) list * Rule_Set.T * string option * Celem.metID list ->
46 Celem.pbt * Celem.pblID
47 val prep_met : theory -> string -> string list -> Celem.pblID ->
48 string list * (string * string list) list *
49 {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
50 rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
51 Celem.met * Celem.metID
52 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
53 val show_ptyps : unit -> unit
54 val show_mets : unit -> unit
55 datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
56 val match_pbl : Selem.fmz_ -> Celem.pbt -> match'
57 val refine : Selem.fmz_ -> Celem.pblID -> Stool.match list
58 val e_errpat : Error_Fill_Def.errpat
59 val show_pblguhs : unit -> unit
60 val sort_pblguhs : unit -> unit
61 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
62 val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b
63 val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
64 val coll_variants: ('a * ''b) list -> ('a list * ''b) list
65 val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
66 val max: int list -> int
67 val replace_0: int -> int list -> int list
68 val split_did: term -> term * term
69 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
71 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
72 val e_fillpat : string * term * string
73 val coll_vats : ''a list * ('b * ''a list * 'c * 'd * 'e) -> ''a list
74 val filter_vat : Model.ori list -> int -> Model.ori list
75 val show_metguhs : unit -> unit
76 val sort_metguhs : unit -> unit
79 structure Specify(**) : MODEL_SPECIFY(**) =
82 (* hack until review of Specify:
83 introduction of Lucas-Interpretation to Isabelle's functioj package enforced
84 to make additional variables on the right hand side to arguments of programs.
85 These additional arguments are partially handled by these hacks. *)
86 fun hack_until_review_Specify_1 metID itms =
87 if metID = ["Biegelinien", "ausBelastung"]
89 [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
90 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
91 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
92 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
93 (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
94 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
95 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
96 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
98 fun hack_until_review_Specify_2 metID itms =
99 if metID = ["IntegrierenUndKonstanteBestimmen2"]
101 [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
102 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
103 (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
104 [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
105 (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
106 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
107 (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
108 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
113 fun fun_id_of ({scr = prog, ...} : Celem.met) =
115 Rule.Empty_Prog => NONE
118 Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
119 | _ => SOME (Program.get_fun_id t))
120 | Rule.Rfuns _ => NONE
122 (* get all data from a Ptyp tree *)
126 | scan ((Celem.Ptyp ((_, data, []))) :: []) = data
127 | scan ((Celem.Ptyp ((_, data, pl))) :: []) = data @ scan pl
128 | scan ((Celem.Ptyp ((_, data, []))) :: ps) = data @ scan ps
129 | scan ((Celem.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
132 fun get_fun_ids thy =
134 val mets = get_data (KEStore_Elems.get_mets thy)
135 (* all mets of the respective theory PLUS of all ancestor theories*)
136 val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
138 filter (fn (str, _) => ThyC.thyID_of_derivation_name str = Context.theory_name thy) fun_ids
141 type field = string * (term * term)
142 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
144 fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (Model.comp_dts (d, ts)))
145 | itm_2item _ (Model.Syn c) = Model.SyntaxE c
146 | itm_2item _ (Model.Typ c) = Model.TypeE c
147 | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (Model.comp_dts (d, ts)))
148 | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (Model.comp_dts (d, ts)))
149 | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
150 | itm_2item _ _ = error "itm_2item: uncovered definition"
152 fun mappc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} =
153 {Given= map f gi, Where = map f wh, Find = map f fi, With = map f wi, Relate = map f re}
154 fun appc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} =
155 {Given = f gi, Where = f wh, Find = f fi, With = f wi, Relate = f re}
157 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
159 "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
160 | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
161 | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
162 | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
163 | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
164 | _ => error ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
165 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
166 {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
168 (* split a term into description and (id | structured variable) for pbt, met.ppc *)
171 val (hd, arg) = case strip_comb t of
172 (hd, [arg]) => (hd, arg)
173 | _ => error ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)
176 (*create output-string for itm_*)
177 fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (Model.comp_dts (d, ts))
178 | itm_out _ (Model.Syn c) = c
179 | itm_out _ (Model.Typ c) = c
180 | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (Model.comp_dts (d, ts))
181 | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (Model.comp_dts (d, ts))
182 | itm_out _ (Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
183 | itm_out _ _ = error "itm_out: uncovered definition"
185 fun boolterm2item (true, term) = Model.Correct (UnparseC.term term)
186 | boolterm2item (false, term) = Model.False (UnparseC.term term);
188 fun itms2itemppc thy itms pre =
190 fun coll ppc [] = ppc
191 | coll ppc ((_,_,_,field,itm_)::itms) =
192 coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
193 val gfr = coll Model.empty_ppc itms;
194 in add_where gfr (map boolterm2item pre) end;
196 (* compare d and dsc in pbt and transfer field to pre-ori *)
197 fun add_field (_: theory) pbt (d,ts) =
198 let fun eq d pt = (d = (fst o snd) pt);
199 in case filter (eq d) pbt of
200 [(fi, (_, _))] => (fi, d, ts)
201 | [] => ("#undef", d, ts) (*may come with met.ppc*)
202 | _ => error ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
205 (* take over field from met.ppc at 'Specify_Method' into ori,
206 i.e. also removes "#undef" fields *)
207 fun add_field' (_: theory) mpc ori =
209 fun eq d pt = (d = (fst o snd) pt);
210 fun repl mpc (i, v, _, d, ts) =
211 case filter (eq d) mpc of
212 [(fi, (_, _))] => [(i, v, fi, d, ts)]
213 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
214 | _ => error ("add_field': " ^ UnparseC.term d ^ " more than once in met");
215 in flat ((map (repl mpc)) ori) end;
217 (* mark an element with the position within a plateau;
218 a plateau with length 1 is marked with 0 *)
219 fun mark _ [] = error "mark []"
222 fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
223 | mar _ _ [] _ = error "mark []"
224 | mar xx eq (x:: x' :: xs) n =
225 if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
226 else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
227 in mar [] eq xs 1 end;
229 (* assumes equal descriptions to be in adjacent 'plateaus',
230 items at a certain position within the plateaus form a variant;
231 length = 1 ... marked with 0: covers all variants *)
232 fun add_variants fdts =
234 fun eq (a, b) = curry op= (snd3 a) (snd3 b);
237 fun max [] = error "max of []"
240 | mx x (y :: ys) = if x < y then mx y ys else mx x ys;
243 fun coll_variants (((v,x) :: vxs)) =
245 fun col xs (vs, x) [] = xs @ [(vs, x)]
246 | col xs (vs, x) ((v', x') :: vxs') =
247 if x = x' then col xs (vs @ [v'], x') vxs'
248 else col (xs @ [(vs, x)]) ([v'], x') vxs';
249 in col [] ([v], x) vxs end
250 | coll_variants _ = error "coll_variants: called with []";
252 fun replace_0 vm [0] = intsto vm
253 | replace_0 _ vs = vs;
255 fun add_id [] = error "add_id []"
259 | add n (x :: xs) = (n, x) :: add (n + 1) xs;
262 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
264 fun prep_ori [] _ _ = ([], ContextC.empty)
265 | prep_ori fmz thy pbt =
267 val ctxt = ContextC.initialise' thy fmz;
268 val ori = map (add_field thy pbt o Model.split_dts o TermC.parseNEW' ctxt) fmz
270 val maxv = map fst ori |> max;
271 val maxv = if maxv = 0 then 1 else maxv;
272 val oris = coll_variants ori
273 |> map (replace_0 maxv |> apfst)
278 val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Fill_Def.errpat
279 val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
281 (** breadth-first search on hierarchy of problem-types **)
283 (* pblID are reverted _on calling_ the retrieve-funs *)
284 type pblRD = (*e.g. ["equations","univariate","normalise"] for internal retrieval *)
285 Celem.pblID; (*e.g. ["normalise","univariate","equations"] presented to student *)
287 (* apply a fun to a ptyps node *)
288 fun app_ptyp x = Celem.app_py (get_ptyps ()) x;
290 (* TODO: generalize search for subthy *)
291 fun get_pbt (pblID: Celem.pblID) = Celem.get_py (get_ptyps ()) pblID (rev pblID)
293 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
294 fun get_met metID = Celem.get_py (get_mets ()) metID metID;
295 fun get_met' thy metID = Celem.get_py (KEStore_Elems.get_mets thy) metID metID;
296 fun get_the theID = Celem.get_py (get_thes ()) theID theID;
298 (* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)
299 fun guh2kestoreID guh =
300 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
303 fun node ids gu (Celem.Ptyp (id, [{guh, ...}], ns)) =
304 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
305 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
306 and nodes _ _ [] = NONE
307 | nodes ids gu (n :: ns) = case node ids gu n of
309 | NONE => nodes ids gu ns
310 in case nodes [] guh (get_ptyps ()) of
312 | NONE => error ("guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in ptyps")
316 fun node ids gu (Celem.Ptyp (id, [{guh, ...}], ns)) =
317 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
318 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
319 and nodes _ _ [] = NONE
320 | nodes ids gu (n :: ns) = case node ids gu n of
322 | NONE => nodes ids gu ns
323 in case nodes [] guh (get_mets ()) of
325 | NONE => error ("guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in mets")
327 | _ => error ("guh2kestoreID called with \"" ^ guh ^ "\":");
329 (* prepare problem-types before storing in pbltypes;
330 dont forget to "check_guh_unique" before ins *)
331 fun prep_pbt thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
333 fun eq f (f', _) = f = f';
334 val gi = filter (eq "#Given") dsc_dats;
337 | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
338 handle _ => error ("prep_pbt: syntax error in '#Given' of " ^ strs2str pblID))
339 | _ => error ("prep_pbt: more than one '#Given' in " ^ strs2str pblID));
340 val gi = map (pair "#Given") gi;
342 val fi = filter (eq "#Find") dsc_dats;
345 | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
346 handle _ => error ("prep_pbt: syntax error in '#Find' of " ^ strs2str pblID))
347 | _ => error ("prep_pbt: more than one '#Find' in " ^ strs2str pblID));
348 val fi = map (pair "#Find") fi;
350 val re = filter (eq "#Relate") dsc_dats;
353 | ((_, re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
354 handle _ => error ("prep_pbt: syntax error in '#Relate' of " ^ strs2str pblID))
355 | _ => error ("prep_pbt: more than one '#Relate' in " ^ strs2str pblID));
356 val re = map (pair "#Relate") re;
358 val wh = filter (eq "#Where") dsc_dats;
361 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
362 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str pblID))
363 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str pblID));
365 ({guh = guh, mathauthors = maa, init = init, thy = thy,
368 | SOME s => SOME ((Thm.term_of o the o (TermC.parse thy)) s),
369 prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
372 (* prepare met for storage analogous to pbt *)
373 fun prep_met thy guh maa init
375 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
376 errpats = ep, nrls = nr}, scr) =
378 fun eq f (f', _) = f = f';
379 val gi = filter (eq "#Given") ppc;
381 [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])
382 | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
383 handle _ => error ("prep_pbt: syntax error in '#Given' of " ^ strs2str metID))
384 | _ => error ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
385 val gi = map (pair "#Given") gi;
387 val fi = filter (eq "#Find") ppc;
389 [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])
390 | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
391 handle _ => error ("prep_pbt: syntax error in '#Find' of " ^ strs2str metID))
392 | _ => error ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
393 val fi = map (pair "#Find") fi;
395 val re = filter (eq "#Relate") ppc;
397 [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])
398 | ((_,re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
399 handle _ => error ("prep_pbt: syntax error in '#Relate' of " ^ strs2str metID))
400 | _ => error ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
401 val re = map (pair "#Relate") re;
403 val wh = filter (eq "#Where") ppc;
405 [] => (writeln ("prep_met: in " ^ guh ^ " #Where is empty ?!?"); [])
406 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
407 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str metID))
408 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
409 val sc = Program.prep_program scr
410 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
412 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
413 erls = rls, srls = srls, prls = prls, calc = calc,
414 crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
418 (** get pblIDs of all entries in mat3D **)
420 fun format_pblID strl = enclose " [" "]" (commas_quote strl);
421 fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
423 fun scan _ [] = [] (* no base case, for empty doms only *)
424 | scan id ((Celem.Ptyp ((i, _, []))) :: []) = [id @ [i]]
425 | scan id ((Celem.Ptyp ((i, _, pl))) :: []) = scan (id @ [i]) pl
426 | scan id ((Celem.Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
427 | scan id ((Celem.Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
429 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ()); (* for tests *)
430 fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)
434 fun coll_vats (vats, (_, vs, _, _, _)) = union op = vats vs;
435 fun filter_vat oris i = filter ((member_swap op = i) o (#2 : Model.ori -> int list)) oris;
437 (** check a problem (ie. itm list) for matching a problemtype **)
439 fun eq1 d (_, (d', _)) = (d = d');
440 fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", Model.Sup (d, ts));
441 (*see + add_sel_ppc ~~~~~~~*)
443 fun field_eq f (_, _, f', _, _) = f = f';
445 (* check an item (with arbitrary itm_ from previous matchings)
446 for matching a problemtype; returns true only for itms found in pbt *)
447 fun chk_ (_: theory) pbt (i, vats, b, f, Model.Cor ((d, vs), _)) =
448 (case find_first (eq1 d) pbt of
449 SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
450 | NONE => (i, vats, false, f, Model.Sup (d, vs)))
451 | chk_ _ pbt (i, vats, b, f, Model.Inc ((d, vs), _)) =
452 (case find_first (eq1 d) pbt of
453 SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
454 | NONE => (i, vats, false, f, Model.Sup (d, vs)))
455 | chk_ _ _ (itm as (_, _, _, _, Model.Syn _)) = itm
456 | chk_ _ _ (itm as (_, _, _, _, Model.Typ _)) = itm
457 | chk_ _ pbt (i, vats, b, f, Model.Sup (d, vs)) =
458 (case find_first (eq1 d) pbt of
459 SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))
460 | NONE => (i, vats, false, f, Model.Sup (d, vs)))
461 | chk_ _ pbt (i, vats, _, f, Model.Mis (d, vs)) =
462 (case find_first (eq1 d) pbt of
463 SOME (_, _) => error "chk_: ((i,vats,b,f,Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"
464 | NONE => (i, vats, false, f, Model.Sup (d, [vs])))
465 | chk_ _ _ _ = error "chk_: uncovered fun def.";
467 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = Model.d_in itm_;
468 fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
469 fun eq0 (0, _, _, _, _) = true
472 | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
474 | max_id ((id, _, _, _, _) :: is) = max_i id is;
475 fun add_idvat itms _ _ [] = itms
476 | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
477 add_idvat (itms @ [(i,[],b,f,itm_)]) (i + 1) mvat its;
478 (* ^^ mvat ...meaningless with pbl-identifier *)
480 (* find elements of pbt not contained in itms;
481 if such one is untouched, return this one, otherwise create new itm *)
482 fun chk_m itms untouched (p as (f, (d, id))) =
483 case find_first (eq2 p) itms of
486 (case find_first (eq2 p) untouched of
488 | NONE => [(0, [], false, f, Model.Mis (d, id))]);
490 fun chk_mis mvat itms untouched pbt =
491 let val mis = (flat o (map (chk_m itms untouched))) pbt;
492 val mid = max_id itms;
493 in add_idvat [] (mid + 1) mvat mis end;
495 (* check a problem (ie. itm list) for matching a problemtype,
496 takes the Model.max_vt for concluding completeness (could be another!) *)
497 fun match_itms thy itms (pbt, pre, prls) =
499 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
500 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
501 val mvat = Model.max_vt itms';
502 val itms'' = filter (okv mvat) itms';
503 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
504 val mis = chk_mis mvat itms'' untouched pbt;
505 val pre' = Stool.check_preconds' prls pre itms'' mvat
506 val pb = foldl and_ (true, map fst pre')
507 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
509 (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
510 for missing items get data from formalization (ie. ori list);
511 takes the Model.max_vt for concluding completeness (could be another!)
513 (0) determine the most frequent variant mv in pbl
514 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
515 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
516 (3) newitms = filter (mv mem vat(news)) news
518 fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
520 (*0*)val mv = Model.max_vt pbl;
522 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = Model.d_in itm_;
523 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
524 SOME _ => false | NONE => true;
525 (*1*)val mis = (filter (notmem pbl)) pbt;
527 fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
528 fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, Model.Mis (d, pid));
529 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
530 val news = (flat o (map (oris2itms oris))) mis;
531 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
532 val newitms = filter mem_vat news;
533 (*4*)val itms' = pbl @ newitms;
534 val pre' = Stool.check_preconds' prls pre itms' mv;
535 val pb = foldl and_ (true, map fst pre');
536 in (length mis = 0 andalso pb, (itms', pre')) end;
539 (** check a problem (ie. itm list) for matching a problemtype **)
541 (* check an ori for matching a problemtype by description;
542 returns true only for itms found in pbt *)
543 fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
544 case find_first (eq1 d) pbt of
545 SOME (_, (_, id)) => [(i, vats, true, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]
548 (* elem 'p' of pbt contained in itms ? *)
549 fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
550 fun chk1_m' oris (p as (f, (d, t))) =
551 case find_first (eq2' p) oris of
553 | NONE => [(f, Model.Mis (d, t))];
554 fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
556 fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
557 fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
559 (* check a problem (ie. ori list) for matching a problemtype,
560 takes the Model.max_vt for concluding completeness (FIXME could be another!) *)
561 fun match_oris thy prls oris (pbt,pre) =
563 val itms = (flat o (map (chk1_ thy pbt))) oris;
564 val mvat = Model.max_vt itms;
565 val complete = chk1_mis mvat itms pbt;
566 val pre' = Stool.check_preconds' prls pre itms mvat;
567 val pb = foldl and_ (true, map fst pre');
568 in if complete andalso pb then true else false end;
570 (* check a problem (ie. ori list) for matching a problemtype,
571 returns items for output to math-experts *)
572 fun match_oris' thy oris (ppc,pre,prls) =
574 val itms = (flat o (map (chk1_ thy ppc))) oris;
575 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
576 val mvat = Model.max_vt itms;
577 val miss = chk1_mis' oris ppc;
578 val pre' = Stool.check_preconds' prls pre itms mvat;
579 val pb = foldl and_ (true, map fst pre');
580 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
582 datatype match' = (* for the user *)
583 Matches' of Model.item Model.ppc
584 | NoMatch' of Model.item Model.ppc;
586 (* match a formalization with a problem type, for tests *)
587 fun match_pbl fmz {thy = thy, where_ = pre, ppc, prls = er, ...} =
589 val oris = prep_ori fmz thy ppc |> #1;
590 val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
593 then Matches' (itms2itemppc thy itms pre')
594 else NoMatch' (itms2itemppc thy itms pre')
597 (* refine a problem; construct pblRD while scanning *)
598 fun refin (pblRD: pblRD) ori (Celem.Ptyp (pI, [py], [])) =
599 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
600 then SOME ((pblRD @ [pI]): pblRD)
602 | refin pblRD ori (Celem.Ptyp (pI, [py], pys)) =
603 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
604 then (case refins (pblRD @ [pI]) ori pys of
605 SOME pblRD' => SOME pblRD'
606 | NONE => SOME (pblRD @ [pI]))
608 | refin _ _ _ = error "refin: uncovered fun def."
609 and refins _ _ [] = NONE
610 | refins pblRD ori ((p as Celem.Ptyp _) :: pts) =
611 (case refin pblRD ori p of
612 SOME pblRD' => SOME pblRD'
613 | NONE => refins pblRD ori pts);
615 (* refine a problem; version providing output for math-experts *)
616 fun refin' (pblRD: pblRD) fmz pbls (Celem.Ptyp (pI, [py], [])) =
618 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
619 val {thy, ppc, where_, prls, ...} = py
620 val oris = prep_ori fmz thy ppc |> #1;
621 (* WN020803: itms!: oris might _not_ be complete here *)
622 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
625 then pbls @ [Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
626 else pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
628 | refin' pblRD fmz pbls (Celem.Ptyp (pI, [py], pys)) =
630 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
631 val {thy, ppc, where_, prls, ...} = py
632 val oris = prep_ori fmz thy ppc |> #1;
633 (* WN020803: itms!: oris might _not_ be complete here *)
634 val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
638 let val pbl = Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')
639 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
640 else (pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
642 | refin' _ _ _ _ = error "refin': uncovered fun def."
643 and refins' _ _ pbls [] = pbls
644 | refins' pblRD fmz pbls ((p as Celem.Ptyp _) :: pts) =
646 val pbls' = refin' pblRD fmz pbls p
648 case last_elem pbls' of
649 Stool.Matches _ => pbls'
650 | Stool.NoMatch _ => refins' pblRD fmz pbls' pts
653 (* refine a problem; version for tactic Refine_Problem *)
654 fun refin'' _ (pblRD: pblRD) itms pbls (Celem.Ptyp (pI, [py], [])) =
656 val {thy, ppc, where_, prls, ...} = py
657 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
660 then pbls @ [Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))]
661 else pbls @ [Stool.NoMatch_]
663 | refin'' _ pblRD itms pbls (Celem.Ptyp (pI, [py], pys)) =
665 val {thy, ppc, where_, prls, ...} = py
666 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
668 then let val pbl = Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))
669 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
670 else (pbls @ [Stool.NoMatch_])
672 | refin'' _ _ _ _ _ = error "refin': uncovered fun def."
673 and refins'' _ _ _ pbls [] = pbls
674 | refins'' thy pblRD itms pbls ((p as Celem.Ptyp _) :: pts) =
676 val pbls' = refin'' thy pblRD itms pbls p
677 in case last_elem pbls' of
678 Stool.Match_ _ => pbls'
679 | Stool.NoMatch_ => refins'' thy pblRD itms pbls' pts
682 (* for tactic Refine_Tacitly
683 oris are already created wrt. some pbt; pbt contains thy for parsing *)
684 fun refine_ori oris pblID =
686 val opt = app_ptyp (refin ((rev o tl) pblID) oris) pblID (rev pblID);
689 let val pblID': Celem.pblID = rev pblRD
690 in if pblID' = pblID then NONE else SOME pblID' end
693 fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
695 (* for tactic Refine_Problem
696 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
697 fun refine_pbl thy pblID itms =
698 case Stool.refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) of
700 | SOME (Stool.Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
701 | _ => error "refine_pbl: uncovered case refined_";
704 (* for math-experts and test;
705 FIXME.WN021019: needs thy for parsing fmz *)
706 fun refine fmz pblID =
707 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID);
709 (* make a guh from a reference to an element in the kestore;
710 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
711 fun pblID2guh pblID = (((#guh o get_pbt) pblID)
712 handle _ => error ("pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
713 fun metID2guh metID = (((#guh o get_met) metID)
714 handle _ => error ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
715 fun kestoreID2guh Celem.Pbl_ kestoreID = pblID2guh kestoreID
716 | kestoreID2guh Celem.Met_ kestoreID = metID2guh kestoreID
717 | kestoreID2guh ketype kestoreID =
718 error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");
720 fun show_pblguhs () = (* for tests *)
721 (tracing o strs2str o (map Celem.linefeed)) (Celem.coll_pblguhs (get_ptyps ()))
722 fun sort_pblguhs () = (* for tests *)
723 (tracing o strs2str o (map Celem.linefeed)) (((sort string_ord) o Celem.coll_pblguhs) (get_ptyps ()))
725 fun show_metguhs () = (* for tests *)
726 (tracing o strs2str o (map Celem.linefeed)) (Celem.coll_metguhs (get_mets ()))
727 fun sort_metguhs () = (* for tests *)
728 (tracing o strs2str o (map Celem.linefeed)) (((sort string_ord) o Celem.coll_metguhs) (get_mets ()))