1 (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in mstools.sml.
3 Author: Walther Neuper 991122, Mathias Lehnfeld
4 (c) due to copyright terms
10 datatype appl = Appl of Ctree.tac_ | Notappl of string
11 val nxt_specify_init_calc : Ctree.fmz -> calcstate
12 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree ->
13 Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree
14 val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate'
15 val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
18 val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
19 val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd
20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
21 val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
23 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
24 val insert_ppc' : itm -> itm list -> itm list
26 val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
27 val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool
28 val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
29 val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool
30 val some_spec : spec -> spec -> spec
31 (* these could go to Ctree ..*)
32 val show_pt : Ctree.ptree -> unit
33 val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list
34 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list
36 val match_ags : theory -> pat list -> term list -> ori list
37 val match_ags_msg : pblID -> term -> term list -> unit
38 val oris2fmz_vals : ori list -> string list * term list
39 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
40 val is_known : Proof.context -> string -> ori list -> term -> string * ori * term list
41 val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list
43 val e_calcstate' : calcstate'
44 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
45 val vals_of_oris : ori list -> term list
46 val is_error : itm_ -> bool
47 val is_copy_named : 'a * ('b * term) -> bool
48 val ori2Coritm : pat list -> ori -> itm
49 val ppc2list : 'a ppc -> 'a list
50 val is_copy_named_idstr : string -> bool
51 val matc : theory -> (string * (term * term)) list -> term list -> preori list -> preori list
52 val mtc : theory -> pat -> term -> preori option
53 val cpy_nam : pat list -> preori list -> pat -> preori
54 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
57 structure Chead(**): CALC_HEAD(**) =
62 (* the state wich is stored after each step of calculation; it contains
63 the calc-state and a list of [tac,istate](="tacis") to be applied next.
64 the last_elem tacis is the first to apply to the calc-state and
65 the (only) one shown to the front-end as the 'proposed tac'.
66 the calc-state resulting from the application of tacis is not stored,
67 because the tacis hold enough information for efficiently rebuilding
68 this state just by "fun generate "
71 (ptree * pos') * (* the calc-state to which the tacis could be applied *)
72 (Generate.taci list) (* ev. several (hidden) steps;
73 in REVERSE order: first tac_ to apply is last_elem *)
74 val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate;
76 (*the state used during one calculation within the mathengine; it contains
77 a list of [tac,istate](="tacis") which generated the the calc-state;
78 while this state's tacis are extended by each (internal) step,
79 the calc-state is used for creating new nodes in the calc-tree
80 (eg. applicable_in requires several particular nodes of the calc-tree)
81 and then replaced by the the newly created;
82 on leave of the mathengine the resuing calc-state is dropped anyway,
83 because the tacis hold enought information for efficiently rebuilding
84 this state just by "fun generate ".*)
86 Generate.taci list * (* cas. several (hidden) steps;
87 in REVERSE order: first tac_ to apply is last_elem *)
88 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
89 (ptree * pos') (* the calc-state resulting from the application of tacis *)
90 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
92 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
93 fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f
94 | f_mout _ _ = error "f_mout: not called with formula";
96 (* is the calchead complete ? *)
97 fun ocalhd_complete its pre (dI, pI, mI) =
98 foldl and_ (true, map #3 its) andalso
99 foldl and_ (true, map #1 pre) andalso
100 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID
102 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
103 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
104 fun oris2fmz_vals oris =
105 let fun ori2fmz_vals ((_, _, _, dsc, ts): ori) =
106 ((term2str o comp_dts') (dsc, ts), last_elem ts)
107 handle _ => error ("ori2fmz_env called with " ^ terms2str ts)
108 in (split_list o (map ori2fmz_vals)) oris end
110 (* make a term 'typeless' for comparing with another 'typeless' term;
111 'type-less' usually is illtyped *)
112 fun typeless (Const (s, _)) = (Const (s, e_type))
113 | typeless (Free (s, _)) = (Free (s, e_type))
114 | typeless (Var (n, _)) = (Var (n, e_type))
115 | typeless (Bound i) = (Bound i)
116 | typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t)
117 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
119 (* to an input (d,ts) find the according ori and insert the ts)
120 WN.11.03: + dont take first inter<>[] *)
121 fun seek_oridts ctxt sel (d, ts) [] =
122 ("seek_oridts: input ('" ^
123 (term_to_string' ctxt (comp_dts (d, ts))) ^ "') not found in oris (typed)",
126 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
127 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
128 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
129 else seek_oridts ctxt sel (d, ts) oris
131 (* to an input (_,ts) find the according ori and insert the ts *)
132 fun seek_orits ctxt _ ts [] =
133 ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
134 "') not found in oris (typed)", e_ori_, [])
135 | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: (oris: ori list)) =
136 if sel = sel' andalso (inter op = ts ts') <> []
139 then ("", (id, vat, sel, d, inter op = ts ts'): ori, ts')
140 else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
141 else seek_orits ctxt sel ts oris
143 (* find_first item with #1 equal to id *)
144 fun seek_ppc _ [] = NONE
145 | seek_ppc id (p :: (ppc: itm list)) = if id = #1 p then SOME p else seek_ppc id ppc
148 Appl of tac_ (* tactic is applicable at a certain position in the Ctree *)
149 | Notappl of string (* tactic is NOT applicable *)
151 fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) =
152 gis @ whs @ fis @ wis @ res
153 fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res
155 (* get the number of variants in a problem in 'original',
156 assumes equal descriptions in immediate sequence *)
159 fun eq (x, y) = head_of x = head_of y
160 fun cnt _ [] _ n = ([n], [])
161 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
162 fun coll _ xs [] = xs
163 | coll eq xs (y :: ys) =
164 let val (n, ys') = cnt eq (y :: ys) y 0
165 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
166 val vts = subtract op = [1] (distinct (coll eq [] ts))
171 | _ => error "different variants in formalization"
174 fun is_list_type (Type ("List.list", _)) = true
175 | is_list_type _ = false
176 fun has_list_type (Free (_, T)) = is_list_type T
177 | has_list_type _ = false
178 fun is_parsed (Syn _) = false
180 fun parse_ok its = foldl and_ (true, map is_parsed its)
182 fun all_dsc_in itm_s =
184 fun d_in (Cor ((d, _), _)) = [d]
187 | d_in (Inc ((d,_),_)) = [d]
188 | d_in (Sup (d,_)) = [d]
189 | d_in (Mis (d,_)) = [d]
190 | d_in i = error ("all_dsc_in: uncovered case with " ^ itm_2str i)
191 in (flat o (map d_in)) itm_s end;
193 fun is_error (Cor _) = false
194 | is_error (Sup _) = false
195 | is_error (Inc _) = false
196 | is_error (Mis _) = false
199 (* get the first term in ts from ori *)
200 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
201 (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm')
203 (* get a term from ori, notyet input in itm.
204 the term from ori is thrown back to a string in order to reuse
205 machinery for immediate input by the user. *)
206 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
207 (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
209 (* in FE dsc, not dat: this is in itms ...*)
210 fun is_untouched ((_, _, false, _, Inc ((_, []), _)): itm) = true
211 | is_untouched _ = false
213 (* select an item in oris, notyet input in itms
214 (precondition: in itms are only Cor, Sup, Inc) *)
217 oris: from formalization 'type fmz', structured for efficient access
218 pbt : the problem-pattern to be matched with oris in order to get itms
219 itms: already input items
221 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
223 fun test_d d ((i, _, _, _, itm_): itm) = (d = (d_in itm_)) andalso i <> 0
224 fun is_elem itms (_, (d, _)) =
225 case find_first (test_d d) itms of SOME _ => true | NONE => false
227 case filter_out (is_elem itms) pbt of
228 (f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
231 | nxt_add thy oris _ itms =
233 fun testr_vt v ori = member op= (#2 (ori:ori)) v andalso (#3 ori) <> "#undef"
234 fun testi_vt v itm =member op= (#2 (itm:itm)) v
235 fun test_id ids r = member op= ids (#1 (r:ori))
236 fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
237 (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts)
238 fun false_and_not_Sup ((_, _, false, _, Sup _): itm) = false
239 | false_and_not_Sup (_, _, false, _, _) = true
240 | false_and_not_Sup _ = false
241 val v = if itms = [] then 1 else max_vt itms
242 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
245 then itms (* because of dsc without dat *)
246 else filter (testi_vt v) itms; (* itms..vat *)
247 val icl = filter false_and_not_Sup vits; (* incomplete *)
250 then case filter_out (test_id (map #1 vits)) vors of
252 | miss => SOME (getr_ct thy (hd miss))
254 case find_first (test_subset (hd icl)) vors of
255 NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
256 | SOME ori => SOME (geti_ct thy ori (hd icl))
259 fun mk_delete thy "#Given" itm_ = Del_Given (Specify.itm_out thy itm_)
260 | mk_delete thy "#Find" itm_ = Del_Find (Specify.itm_out thy itm_)
261 | mk_delete thy "#Relate" itm_ = Del_Relation(Specify.itm_out thy itm_)
262 | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
263 fun mk_additem "#Given" ct = Add_Given ct
264 | mk_additem "#Find" ct = Add_Find ct
265 | mk_additem "#Relate"ct = Add_Relation ct
266 | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
268 (* determine the next step of specification;
269 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
270 eg. in rootpbl 'no_met':
272 preok predicates are _all_ ok (and problem matches completely)
273 oris immediately from formalization
274 (dI',pI',mI') specification coming from author/parent-problem
275 (pbl, item lists specified by user
276 met) -"-, tacitly completed by copy_probl
277 (dI,pI,mI) specification explicitly done by the user
278 (pbt, mpc) problem type, guard of method
280 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
281 ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
282 (if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
283 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
285 case find_first (is_error o #5) (pbl:itm list) of
286 SOME (_, _, _, fd, itm_) =>
287 (Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
289 (case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of
290 SOME (fd,ct') => (Pbl, mk_additem fd ct')
291 | NONE => (*pbl-items complete*)
292 if not preok then (Pbl, Refine_Problem pI')
293 else if dI = e_domID then (Pbl, Specify_Theory dI')
294 else if pI = e_pblID then (Pbl, Specify_Problem pI')
295 else if mI = e_metID then (Pbl, Specify_Method mI')
297 case find_first (is_error o #5) met of
298 SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_)
300 (case nxt_add (assoc_thy dI) oris mpc met of
301 SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
302 | NONE => (Met, Apply_Method mI))))
303 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
304 (case find_first (is_error o #5) met of
305 SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
307 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
308 SOME (fd,ct') => (Met, mk_additem fd ct')
310 (if dI = e_domID then (Met, Specify_Theory dI')
311 else if pI = e_pblID then (Met, Specify_Problem pI')
312 else if not preok then (Met, Specify_Method mI)
313 else (Met, Apply_Method mI)))
314 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
316 fun is_field_correct sel d dscpbt =
317 case assoc (dscpbt, sel) of
319 | SOME ds => member op = ds d
321 (* update the itm_ already input, all..from ori *)
322 fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) =
324 val ts' = union op = (ts_in itm_) ts;
325 val pval = pbl_ids' d ts'
326 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
327 val complete = if eq_set op = (ts', all) then true else false
331 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
332 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval)))): itm
333 | (Syn c) => error ("ori_2itm wants to overwrite " ^ c)
334 | (Typ c) => error ("ori_2itm wants to overwrite " ^ c)
337 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
338 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
339 | (Sup (d,ts')) => (*4.9.01 lost env*)
340 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
341 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
342 (* 28.1.00: not completely clear ---^^^ etc.*)
343 | (Mis _) => (* 4.9.01: Mis just copied *)
345 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
346 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
347 | i => error ("ori_2itm: uncovered case of "^ itm_2str i)
350 fun eq1 d (_, (d', _)) = (d = d')
351 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
353 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
354 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
355 pval: value for problem-environment _NOT_ checked for 'inter' --
356 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
357 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
358 (*. is_input ori itms <=>
359 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
360 (2) ori(ts) subset itm(ts) --- Err "already input"
361 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
362 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
363 fun is_notyet_input ctxt (itms: itm list) all ((i, v, f, d, ts): ori) pbt =
364 case find_first (eq1 d) pbt of
365 SOME (_, (_, pid)) =>
366 (case find_first (eq3 f d) itms of
367 SOME (_,_,_,_,itm_) =>
368 let val ts' = inter op = (ts_in itm_) ts
370 if subset op = (ts, ts')
371 then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm) (*2*)
372 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
374 | NONE => ("", ori_2itm (Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
375 | NONE => ("", ori_2itm (Sup (d, ts)) e_term all (i, v, f, d, ts))
377 fun test_types ctxt (d,ts) =
379 val opt = (try comp_dts) (d, ts)
380 val msg = case opt of
382 | NONE => (term_to_string' ctxt d ^ " " ^
383 (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped")
386 (* is the input term t known in oris ?
387 give feedback on all(?) strange input;
388 return _all_ terms already input to this item (e.g. valuesFor a,b) *)
389 fun is_known ctxt sel ori t =
391 val _ = tracing ("RM is_known: t=" ^ term2str t)
392 val ots = (distinct o flat o (map #5)) (ori:ori list)
393 val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots
394 val (d, ts) = split_dts t
395 val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts)
397 if (subtract op = oids ids) <> []
398 then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), e_ori_, [])
402 if not (subset op = (map typeless ts, map typeless ots))
403 then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
404 "' not in example (typeless)", e_ori_, [])
406 (case seek_orits ctxt sel ts ori of
407 ("", ori_ as (_,_,_,d,ts), all) =>
408 (case test_types ctxt (d,ts) of
409 "" => ("", ori_, all)
410 | msg => (msg, e_ori_, []))
411 | (msg,_,_) => (msg, e_ori_, []))
413 if member op = (map #4 ori) d
414 then seek_oridts ctxt sel (d, ts) ori
415 else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
420 Add of itm (* return-value of appl_add *)
421 | Err of string (* error-message *)
423 (* add an item to the model; check wrt. oris and pbt.
424 in contrary to oris<>[] below, this part handles user-input
425 extremely acceptive, i.e. accept input instead error-msg *)
426 fun appl_add ctxt sel [] ppc pbt ct =
428 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
430 case parseNEW ctxt ct of
431 NONE => Add (i, [], false, sel, Syn ct)
433 let val (d, ts) = split_dts t
436 then Add (i, [], false, sel, Mis (Specify.dsc_unknown, hd ts))
438 (case find_first (eq1 d) pbt of
439 NONE => Add (i, [], true, sel, Sup (d,ts))
440 | SOME (f, (_, id)) =>
441 let fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
442 in case find_first (eq2 d) ppc of
443 NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
444 | SOME (i', _, _, _, itm_) =>
448 val in_itm = ts_in itm_
449 val ts' = union op = ts in_itm
450 val i'' = if in_itm = [] then i else i'
451 in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
452 else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
456 | appl_add ctxt sel oris ppc pbt str =
457 case parseNEW ctxt str of
458 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
460 case is_known ctxt sel oris t of
462 (case is_notyet_input ctxt ppc all ori' pbt of
464 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
465 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
467 (* make oris from args of the stac SubProblem and from pbt.
468 can this formal argument (of a model-pattern) be omitted in the arg-list
469 of a SubProblem ? see calcelems.sml 'type met ' *)
470 fun is_copy_named_idstr str =
471 case (rev o Symbol.explode) str of
472 "'" :: _ :: "'" :: _ =>
473 (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true)
475 (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false)
476 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t
478 (* should this formal argument (of a model-pattern) create a new identifier? *)
479 fun is_copy_named_generating_idstr str =
480 if is_copy_named_idstr str
482 case (rev o Symbol.explode) str of
483 "'" :: "'" :: "'" :: _ => false
486 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t
488 (* split type-wrapper from scr-arg and build part of an ori;
489 an type-error is reported immediately, raises an exn,
490 subsequent handling of exn provides 2nd part of error message *)
491 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
492 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
493 SOME ((([1], str, dsc, (*[var]*)
494 split_dts' (dsc, var))): preori)(*:ori without leading #*))
495 handle e as TYPE _ =>
496 (tracing (dashs 70 ^ "\n"
497 ^ "*** ERROR while creating the items for the model of the ->problem\n"
498 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
499 ^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n"
500 ^ "*** description: " ^ term_detail2str dsc
501 ^ "*** value: " ^ term_detail2str var
502 ^ "*** typeconstructor in script: " ^ term_detail2str ty
503 ^ "*** checked by theory: " ^ theory2str thy ^ "\n"
505 writeln (PolyML.makestring e);
506 reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
508 | mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t)
510 (* match each pat of the model-pattern with an actual argument;
511 precondition: copy-named vars are filtered out *)
512 fun matc _ ([]:pat list) _ (oris:preori list) = oris
515 error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
516 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
517 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
519 let val opt = mtc thy p a
522 SOME ori => matc thy pbt ags (oris @ [ori])
523 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
526 (* generate a new variable "x_i" name from a related given one "x"
527 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
528 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
529 but leave is_copy_named_generating as is, e.t. ss''' *)
530 fun cpy_nam (pbt: pat list) (oris: preori list) (p as (field, (dsc, t)): pat) =
531 (if is_copy_named_generating p
532 then (*WN051014 kept strange old code ...*)
533 let fun sel (_,_,d,ts) = comp_ts (d, ts)
534 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
535 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
536 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
537 val vals = map sel oris
538 val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
539 in ([1], field, dsc, [mk_free (type_of t) cy_ext]): preori end
540 else ([1], field, dsc, [t])
541 ) handle _ => error ("cpy_nam: for "^(term2str t))
543 (* match the actual arguments of a SubProblem with a model-pattern
544 and create an ori list (in root-pbl created from formalization).
545 expects ags:pats = 1:1, while copy-named are filtered out of pats;
546 if no 1:1 the exn raised by matc/mtc and handled at call.
547 copy-named pats are appended in order to get them into the model-items *)
548 fun match_ags thy (pbt: pat list) ags =
549 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_)
550 val pbt' = filter_out is_copy_named pbt
551 val cy = filter is_copy_named pbt
552 val oris' = matc thy pbt' ags []
553 val cy' = map (cpy_nam pbt' oris') cy
554 val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
555 in (map flattup ors): ori list end
557 (* report part of the error-msg which is not available in match_args *)
558 fun match_ags_msg pI stac ags =
560 val pats = (#ppc o Specify.get_pbt) pI
561 val msg = (dots 70^"\n"
562 ^ "*** problem "^strs2str pI ^ " has the ...\n"
563 ^ "*** model-pattern "^pats2str pats ^ "\n"
564 ^ "*** stac '"^term2str stac ^ "' has the ...\n"
565 ^ "*** arg-list "^terms2str ags ^ "\n"
567 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
570 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
571 fun vars_of_pbl_ pbl_ =
573 fun var_of_pbl_ (_, (_, t)) = t
574 in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end
575 fun vars_of_pbl_' pbl_ =
577 fun var_of_pbl_ (_, (_, t)) = t: term
578 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
580 fun overwrite_ppc thy itm ppc =
582 fun repl _ (_, _, _, _, itm_) [] =
583 error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ " not found")
584 | repl ppc' itm (p :: ppc) =
585 if (#1 itm) = (#1 (p: itm))
586 then ppc' @ [itm] @ ppc
587 else repl (ppc' @ [p]) itm ppc
588 in repl [] itm ppc end
590 (* 10.3.00: insert the already compiled itm into model;
591 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
592 fun insert_ppc thy itm ppc =
594 fun eq_untouched d ((0, _, _, _, itm_): itm) = (d = d_in itm_)
595 | eq_untouched _ _ = false
596 val ppc' = case seek_ppc (#1 itm) ppc of
597 SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
598 | NONE => (ppc @ [itm])
599 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end
601 fun eq_dsc ((_, _, _, _, itm_): itm, (_, _, _, _, iitm_): itm) = (d_in itm_ = d_in iitm_)
603 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
604 handles superfluous items carelessly *)
605 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
607 (* output the headline to a ppc *)
608 fun header p_ pI mI =
609 case p_ of Pbl => Generate.Problem (if pI = e_pblID then [] else pI)
610 | Met => Generate.Method mI
611 | pos => error ("header called with "^ pos_2str pos)
613 fun specify_additem sel (ct, _) (p, Met) _ pt =
615 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
616 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
617 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
618 | _ => error "specify_additem: uncovered case of get_obj I pt p"
619 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
620 val cpI = if pI = e_pblID then pI' else pI
621 val cmI = if mI = e_metID then mI' else mI
622 val {ppc, pre, prls, ...} = Specify.get_met cmI
624 case appl_add ctxt sel oris met ppc ct of
625 Add itm => (*..union old input *)
627 val met' = insert_ppc thy itm met
628 val arg = case sel of
629 "#Given" => Add_Given' (ct, met')
630 | "#Find" => Add_Find' (ct, met')
631 | "#Relate"=> Add_Relation'(ct, met')
632 | str => error ("specify_additem: uncovered case with " ^ str)
633 val (p, Met, pt') = case Generate.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
634 ((p, Met), _, _, pt') => (p, Met, pt')
635 | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
636 val pre' = check_preconds thy prls pre met'
637 val pb = foldl and_ (true, map fst pre')
639 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
640 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
641 in ((p, p_), ((p, p_), Uistate),
642 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt')
646 val pre' = check_preconds thy prls pre met
647 val pb = foldl and_ (true, map fst pre')
649 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
650 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
651 in ((p,p_), ((p,p_),Uistate), Generate.Error' msg, nxt, Safe,pt) end
653 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
655 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
656 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
657 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
658 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
659 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
660 val cpI = if pI = e_pblID then pI' else pI
661 val cmI = if mI = e_metID then mI' else mI
662 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
664 case appl_add ctxt sel oris pbl ppc ct of
665 Add itm => (*..union old input *)
667 val pbl' = insert_ppc thy itm pbl
668 val arg = case sel of
669 "#Given" => Add_Given' (ct, pbl')
670 | "#Find" => Add_Find' (ct, pbl')
671 | "#Relate"=> Add_Relation'(ct, pbl')
672 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
673 val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
674 val pre = check_preconds thy prls where_ pbl'
675 val pb = foldl and_ (true, map fst pre)
677 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
678 val ppc = if p_= Pbl then pbl' else met
680 ((p, p_), ((p, p_), Uistate),
681 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt')
685 val pre = check_preconds thy prls where_ pbl
686 val pb = foldl and_ (true, map fst pre)
688 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
689 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
690 in ((p, p_), ((p, p_), Uistate), Generate.Error' msg, nxt, Safe,pt) end
693 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
694 let (* either """"""""""""""" all empty or complete *)
695 val thy = assoc_thy dI'
697 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
699 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
700 val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
701 (oris, (dI',pI',mI'), e_term)
702 val pt = update_ctxt pt [] ctxt
703 val (pbl, pre) = ([], [])
707 (([], Pbl), (([], Pbl), Uistate),
708 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
709 Refine_Tacitly pI', Safe, pt)
711 (([], Pbl), (([], Pbl), Uistate),
712 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
713 Model_Problem, Safe, pt)
715 (* ONLY for STARTING modeling phase *)
716 | specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
718 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
719 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
720 (oris, dI',pI',mI', dI, ctxt)
721 | _ => error "specify (Model_Problem': uncovered case get_obj"
722 val thy' = if dI = e_domID then dI' else dI
723 val thy = assoc_thy thy'
724 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
725 val pre = check_preconds thy prls where_ pbl
726 val pb = foldl and_ (true, map fst pre)
727 val ((p, _), _, _, pt) =
728 Generate.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
729 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
730 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
732 ((p, Pbl), ((p, p_), Uistate),
733 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
736 (* called only if no_met is specified *)
737 | specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
739 val (dI', ctxt) = case get_obj I pt p of
740 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
741 | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
742 val {met, thy,...} = Specify.get_pbt pIre
743 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
744 val ((p,_), _, _, pt) =
745 Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
746 val (pbl, pre, _) = ([], [], false)
747 in ((p, Pbl), (pos, Uistate),
748 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
749 Model_Problem, Safe, pt)
751 | specify (Refine_Problem' rfd) pos _ pt =
753 val ctxt = get_ctxt pt pos
754 val (pos, _, _, pt) =
755 Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
757 (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Generate.RefinedKF rfd, Model_Problem, Safe, pt)
759 (*WN110515 initialise ctxt again from itms and add preconds*)
760 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
762 val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
763 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
764 (oris, dI', pI', mI', dI, mI, ctxt, met)
765 | _ => error "specify (Specify_Problem': uncovered case get_obj"
766 val thy = assoc_thy dI
768 case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
769 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
770 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
771 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
772 val mI'' = if mI=e_metID then mI' else mI
773 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
774 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
776 ((p,Pbl), (pos,Uistate),
777 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
780 (*WN110515 initialise ctxt again from itms and add preconds*)
781 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt =
783 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
784 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
785 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
786 | _ => error "specify (Specify_Problem': uncovered case get_obj"
787 val {ppc,pre,prls,...} = Specify.get_met mID
788 val thy = assoc_thy dI
789 val oris = Specify.add_field' thy ppc oris
790 val dI'' = if dI=e_domID then dI' else dI
791 val pI'' = if pI = e_pblID then pI' else pI
792 val met = if met = [] then pbl else met
793 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
794 val (pos, _, _, pt) =
795 Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
796 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
797 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
800 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
803 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
804 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
805 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
806 | specify (Specify_Theory' domID) (pos as (p,p_)) _ pt =
808 val p_ = case p_ of Met => Met | _ => Pbl
809 val thy = assoc_thy domID
810 val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
811 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
812 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
813 | _ => error "specify (Specify_Theory': uncovered case get_obj"
814 val mppc = case p_ of Met => met | _ => pbl
815 val cpI = if pI = e_pblID then pI' else pI
816 val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
817 val cmI = if mI = e_metID then mI' else mI
818 val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
820 Met => (check_preconds thy mer mwh met)
821 | _ => (check_preconds thy per pwh pbl)
822 val pb = foldl and_ (true, map fst pre)
826 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
828 ((p, p_), (pos, Uistate),
829 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
832 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
834 val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
835 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
837 ((p,p_), (pos,Uistate),
838 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
842 | specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m')
844 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
845 -- for input from scratch*)
846 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
848 val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
849 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
850 (oris, dI', pI', dI, pI, pbl, ctxt)
851 | _ => error "specify (Specify_Theory': uncovered case get_obj"
852 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
853 val cpI = if pI = e_pblID then pI' else pI;
855 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
856 Add itm (*..union old input *) =>
858 val pbl' = insert_ppc thy itm pbl
859 val (tac, tac_) = case sel of
860 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
861 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
862 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
863 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
864 val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
865 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
866 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
868 ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
870 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
871 FIXME ..and dont abuse a tactic for that purpose*)
872 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
873 (e_pos', (e_istate, e_ctxt)))], [], ptp)
875 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
877 val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
878 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
879 (oris, dI', mI', dI, mI, met, ctxt)
880 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
881 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
882 val cmI = if mI = e_metID then mI' else mI;
884 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
885 Add itm (*..union old input *) =>
887 val met' = insert_ppc thy itm met;
888 val (tac,tac_) = case sel of
889 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
890 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
891 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
892 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
893 val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
894 ((p, Met), c, _, pt') => (p, Met, c, pt')
895 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
897 ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))
899 | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
901 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
903 fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) =
904 ((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm)
905 handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm)
906 (*dsc in oris, but not in pbl pat list: keep this dsc*)
908 (* filter out oris which have same description in itms *)
909 fun filter_outs oris [] = oris
910 | filter_outs oris (i::itms) =
912 val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris
917 (* filter oris which are in pbt, too *)
918 fun filter_pbt oris pbt =
920 val dscs = map (fst o snd) pbt
922 filter ((member op= dscs) o (#4 : ori -> term)) oris
925 (* combine itms from pbl + met and complete them wrt. pbt *)
926 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
927 fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met =
929 val vat = max_vt pits;
930 val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits)
931 val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris
932 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
934 itms @ (map (ori2Coritm met) os)
937 (* complete model and guard of a calc-head *)
938 fun complete_mod_ (oris, mpc, ppc, probl) =
940 val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl
941 val vat = if probl = [] then 1 else max_vt probl
942 val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris
943 val pors = filter_outs pors pits (*which are in pbl already*)
944 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
945 val pits = pits @ (map (ori2Coritm ppc) pors)
946 val mits = complete_metitms oris pits [] mpc
949 fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =
950 (if dI = e_domID then odI else dI,
951 if pI = e_pblID then opI else pI,
952 if mI = e_metID then omI else mI) : spec
954 (* find a next applicable tac (for calcstate) and update ptree
955 (for ev. finding several more tacs due to hide) *)
956 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
957 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
958 (* WN.24.10.03 fun nxt_solv = ...................................?? *)
959 fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) =
961 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
962 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
963 | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
964 val (dI, pI, mI) = some_spec ospec spec
965 val thy = assoc_thy dI
966 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
967 val {cas, ppc, ...} = Specify.get_pbt pI
968 val pbl = Generate.init_pbl ppc (* fill in descriptions *)
969 (*----------------if you think, this should be done by the Dialog
970 in the java front-end, search there for WN060225-modelProblem----*)
971 val (pbl, met) = case cas of
973 | _ => complete_mod_ (oris, mpc, ppc, probl)
974 (*----------------------------------------------------------------*)
975 val tac_ = Model_Problem' (pI, pbl, met)
976 val (pos,c,_,pt) = Generate.generate1 thy tac_ (Uistate, ctxt) pos pt
977 in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
978 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
979 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
980 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
981 (*. called only if no_met is specified .*)
982 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
984 val (oris, dI, ctxt) = case get_obj I pt p of
985 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
986 | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
987 val opt = Specify.refine_ori oris pI
992 val {met, ...} = Specify.get_pbt pI'
993 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
994 val mI = if length met = 0 then e_metID else hd met
995 val thy = assoc_thy dI
996 val (pos, c, _, pt) =
997 Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
999 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1000 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1002 | NONE => ([], [], ptp)
1004 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1006 val (dI, dI', probl, ctxt) = case get_obj I pt p of
1007 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
1008 (dI, dI', probl, ctxt)
1009 | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
1010 val thy = if dI' = e_domID then dI else dI'
1012 case Specify.refine_pbl (assoc_thy thy) pI probl of
1013 NONE => ([], [], ptp)
1016 val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1018 ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1021 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1023 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
1024 PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>
1025 (oris, dI, dI', pI', probl, ctxt)
1027 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1028 val {ppc,where_,prls,...} = Specify.get_pbt pI
1030 if pI' = e_pblID andalso pI = e_pblID
1031 then (false, (Generate.init_pbl ppc, []))
1032 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
1033 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1034 val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1035 ((_, Pbl), c, _, pt) => (c, pt)
1038 ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1040 (* transfers oris (not required in pbl) to met-model for script-env
1041 FIXME.WN.8.03: application of several mIDs to SAME model? *)
1042 | nxt_specif (Specify_Method mID) (pt, pos as (p,_)) =
1044 val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
1045 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
1046 => (oris, pbl, dI, met, ctxt)
1047 | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
1048 val {ppc,pre,prls,...} = Specify.get_met mID
1049 val thy = assoc_thy dI
1050 val oris = Specify.add_field' thy ppc oris
1051 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1052 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
1053 val (pos, c, _, pt) =
1054 Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1056 ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
1058 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =
1060 val ctxt = get_ctxt pt pos
1061 val (pos, c, _, pt) =
1062 Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1063 in (*FIXXXME: check if pbl can still be parsed*)
1064 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
1067 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
1069 val ctxt = get_ctxt pt pos
1070 val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1071 in (*FIXXXME: check if met can still be parsed*)
1072 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
1074 | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')
1076 (* get the values from oris; handle the term list w.r.t. penv *)
1077 fun vals_of_oris oris =
1078 ((map (mkval' o (#5 : ori -> term list))) o
1079 (filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris
1081 (* create a calc-tree with oris via an cas.refined pbl *)
1082 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1084 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1086 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
1087 val dI = if dI = "" then theory2theory' thy else dI
1088 val mI = if mI = [] then hd met else mI
1089 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1090 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
1091 ([], (dI,pI,mI), hdl)
1092 val pt = update_spec pt [] (dI, pI, mI)
1093 val pits = Generate.init_pbl' ppc
1094 val pt = update_pbl pt [] pits
1095 in ((pt, ([] , Pbl)), []) : calcstate end
1098 then (* from met-browser *)
1100 val {ppc, ...} = Specify.get_met mI
1101 val dI = if dI = "" then "Isac" else dI
1103 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1104 val pt = update_spec pt [] (dI, pI, mI)
1105 val mits = Generate.init_pbl' ppc
1106 val pt = update_met pt [] mits
1107 in ((pt, ([], Met)), []) end
1108 else (* new example, pepare for interactive modeling *)
1111 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
1112 in ((pt, ([], Pbl)), []) end
1113 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1114 let (* both """"""""""""""""""""""""" either empty or complete *)
1115 val thy = assoc_thy dI
1116 val (pI, (pors, pctxt), mI) =
1120 val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
1121 val pI' = Specify.refine_ori' pors pI;
1122 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1123 (hd o #met o Specify.get_pbt) pI')
1125 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
1126 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
1127 val dI = theory2theory' (maxthy thy thy')
1128 val hdl = case cas of
1129 NONE => pblterm dI pI
1130 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
1132 cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1133 val pt = update_ctxt pt [] pctxt
1135 ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1138 fun get_spec_form m ((p, p_) : pos') pt =
1139 let val (_, _, f, _, _, _) = specify m (p, p_) [] pt
1142 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1143 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1144 fun tag_form thy (formal, given) =
1146 val gf = (head_of given) $ formal;
1147 val _ = Thm.global_cterm_of thy gf
1149 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1150 " .. " ^ term_to_string''' thy formal ^ " ..types do not match")
1152 fun chktyp thy (n, fs, gs) =
1153 ((writeln o (term_to_string''' thy) o (nth n)) fs;
1154 (writeln o (term_to_string''' thy) o (nth n)) gs;
1155 tag_form thy (nth n fs, nth n gs))
1156 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
1158 (* check pbltypes, announces one failure a time *)
1159 fun chk_vars ctppc =
1161 val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
1162 val chked = subtract op = gi wh
1164 if chked <> [] then ("wh\\gi", chked)
1166 let val chked = subtract op = (union op = gi fi) re
1169 then ("re\\(gi union fi)", chked)
1174 (* check a new pbltype: variables (Free) unbound by given, find*)
1175 fun unbound_ppc ctppc =
1177 val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
1179 distinct (subtract op = (union op = gi fi) re)
1182 (* f, a binary operator, is nested right associative *)
1185 fun fld _ (x :: []) = x
1186 | fld f (x :: x' :: []) = f (x', x)
1187 | fld f (x :: x' :: xs) = f (fld f (x' :: xs), x)
1188 | fld _ _ = error "foldr1 uncovered definition"
1189 in ((fld f) o rev) xs end
1191 (* f, a binary operator, is nested leftassociative *)
1192 fun foldl1 _ (x :: []) = x
1193 | foldl1 f (x :: x' :: []) = f (x, x')
1194 | foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs))
1195 | foldl1 _ _ = error "foldl1 uncovered definition"
1197 (* called only once, if a Subproblem has been located in the script*)
1198 fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
1200 ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1201 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1202 (*all stored in tac_ itms^^^^^^^^^^*)
1203 | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_)
1205 (* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *)
1206 fun eq4 v (_, vts, _, _, _) = member op = vts v
1207 fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d
1209 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1210 + met from fmz; assumes pos on PblObj, meth = [] *)
1211 fun complete_mod (pt, pos as (p, p_) : pos') =
1213 val _ = if p_ <> Pbl
1214 then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
1216 val (oris, ospec, probl, spec) = case get_obj I pt p of
1217 PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
1218 | _ => error "complete_mod: unvered case get_obj"
1219 val (_, pI, mI) = some_spec ospec spec
1220 val mpc = (#ppc o Specify.get_met) mI
1221 val ppc = (#ppc o Specify.get_pbt) pI
1222 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1223 val pt = update_pblppc pt p pits
1224 val pt = update_metppc pt p mits
1225 in (pt, (p, Met) : pos') end
1227 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1228 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1229 fun all_modspec (pt, (p, _) : pos') =
1231 val (pors, dI, pI, mI) = case get_obj I pt p of
1232 PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
1233 | _ => error "all_modspec: uncovered case get_obj"
1234 val {ppc, ...} = Specify.get_met mI
1235 val (_, vals) = oris2fmz_vals pors
1236 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1237 |> declare_constraints' vals
1238 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
1239 val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
1240 val pt = update_spec pt p (dI, pI, mI)
1241 val pt = update_ctxt pt p ctxt
1243 (pt, (p, Met) : pos')
1246 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
1247 fun is_complete_mod_ ([] : itm list) = false
1248 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
1250 fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
1251 if (is_pblobj o (get_obj I pt)) p
1252 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1253 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1254 | is_complete_mod (pt, pos as (p, Met)) =
1255 if (is_pblobj o (get_obj I pt)) p
1256 then (is_complete_mod_ o (get_obj g_met pt)) p
1257 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1258 | is_complete_mod (_, pos) =
1259 error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
1261 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
1262 fun is_complete_spec (pt, pos as (p, _) : pos') =
1263 if (not o is_pblobj o (get_obj I pt)) p
1264 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1266 let val (dI,pI,mI) = get_obj g_spec pt p
1267 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end
1269 (* complete empty items in specification from origin (pbl, met ev.refined);
1270 assumes 'is_complete_mod' *)
1271 fun complete_spec (pt, pos as (p, _) : pos') =
1273 val (ospec, spec) = case get_obj I pt p of
1274 PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
1275 | _ => error "complete_spec: uncovered case get_obj"
1276 val pt = update_spec pt p (some_spec ospec spec)
1281 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
1283 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
1285 val (_, _, metID) = get_somespec' spec spec'
1286 val pre = if metID = e_metID then []
1289 val {prls, pre= where_, ...} = Specify.get_met metID
1290 val pre = check_preconds' prls where_ meth 0
1292 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
1294 ModSpec (allcorrect, Met, hdl, meth, pre, spec)
1296 | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
1298 val (_, pI, _) = get_somespec' spec spec'
1299 val pre = if pI = e_pblID then []
1302 val {prls, where_, ...} = Specify.get_pbt pI
1303 val pre = check_preconds' prls where_ probl 0
1305 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
1307 ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
1309 | pt_model _ _ = error "pt_model: uncovered definition"
1311 fun pt_form (PrfObj {form, ...}) = Form form
1312 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
1314 val (dI, pI, _) = get_somespec' spec spec'
1315 val {cas, ...} = Specify.get_pbt pI
1317 NONE => Form (pblterm dI pI)
1318 | SOME t => Form (subst_atomic (mk_env probl) t)
1321 (* pt_extract returns
1322 # the formula at pos
1323 # the tactic applied to this formula
1324 # the list of assumptions generated at this formula
1325 (by application of another tac to the preceding formula !)
1326 pos is assumed to come from the frontend, ie. generated by moveDown.
1327 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
1328 TODO 110417 get assumptions from ctxt !?
1330 fun pt_extract (pt, ([], Res)) =
1331 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
1333 val (f, asm) = get_obj g_result pt []
1334 in (Form f, NONE, asm) end
1335 | pt_extract (pt,(p,Res)) =
1337 val (f, asm) = get_obj g_result pt p
1341 if is_pblobj' pt (lev_up p)
1344 val pI = case get_obj I pt (lev_up p) of
1345 PblObj{spec = (_, pI, _), ...} => pI
1346 | _ => error "pt_extract last_onlev: uncovered case get_obj"
1347 in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
1348 else SOME End_Trans (* WN0502 TODO for other branches *)
1350 let val p' = lev_on p
1355 val (dI ,pI) = case get_obj I pt p' of
1356 PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
1357 | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
1358 in SOME (Subproblem (dI, pI)) end
1360 if f = get_obj g_form pt p'
1361 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1362 else SOME (Take (term2str (get_obj g_form pt p')))
1364 in (Form f, tac, asm) end
1365 | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
1367 val ppobj = get_obj I pt p
1368 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1369 val tac = g_tac ppobj
1370 in (f, SOME tac, []) end
1372 (** get the formula from a ctree-node:
1373 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1374 take res from all other PrfObj's
1375 Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
1376 fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
1377 [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
1378 | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
1379 [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
1380 | formres _ _ = error "formres: uncovered definition"
1381 fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
1382 [("stepform", (p, Res), r)]
1383 | form _ _ = error "form: uncovered definition"
1385 (* assumes to take whole level, in particular hd -- for use in interSteps *)
1386 fun get_formress fs _ [] = flat fs
1387 | get_formress fs p (nd::nds) =
1388 (* start with 'form+res' and continue with trying 'res' only*)
1389 get_forms (fs @ [formres p nd]) (lev_on p) nds
1390 and get_forms fs _ [] = flat fs
1391 | get_forms fs p (nd::nds) =
1393 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1394 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1395 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1396 (* continue with trying 'res' only*)
1397 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1399 (** get an 'interval' 'from' 'to' of formulae from a ptree **)
1400 (* WN0401 this functionality belongs to ctree.sml *)
1401 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
1402 | eq_pos' (p1, Res) (p2, Res) = p1 = p2
1403 | eq_pos' (p1, Pbl) (p2, p2_) =
1404 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1405 | eq_pos' (p1, Met) (p2, p2_) =
1406 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1407 | eq_pos' _ _ = false;
1409 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
1410 total ordering Position#compareTo(Position p) in the java-code
1411 val get_interval = fn
1412 : pos' -> : from is "move_up 1st-element" to return
1413 pos' -> : to the last element to be returned; from < to
1414 int -> : level: 0 gets the flattest sub-tree possible
1415 >999 gets the deepest sub-tree possible
1417 (pos' * : of the formula
1418 Term.term) : the formula
1420 fun get_interval from to level pt =
1422 fun get_inter c (from : pos') (to : pos') lev pt =
1423 if eq_pos' from to orelse from = ([], Res)
1425 let val (f, _, _) = pt_extract (pt, from)
1427 ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)]
1428 | Form t => c @ [(from, t)]
1431 if lev < lev_of from
1432 then (get_inter c (move_dn [] pt from) to lev pt)
1433 handle (PTREE _(*from move_dn too far*)) => c
1436 val (f, _, _) = pt_extract (pt, from)
1437 val term = case f of
1438 ModSpec (_,_,headline,_,_,_) => headline
1440 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1441 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1443 in get_inter [] from to level pt end
1446 fun posform2str (pos : pos', form) =
1447 "(" ^ pos'2str pos ^ ", " ^
1448 (case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^
1450 fun posforms2str pfs =
1451 (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs
1452 fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"
1453 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
1455 (* WN050225 omits the last step, if pt is incomplete *)
1456 fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
1458 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
1459 fun get_ocalhd (pt, (p, Pbl) : pos') =
1461 val (ospec, hdf', spec, probl) = case get_obj I pt p of
1462 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1463 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1464 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
1465 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1467 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1469 | get_ocalhd (pt, (p, Met)) =
1471 val (ospec, hdf', spec, meth) = case get_obj I pt p of
1472 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1473 | _ => error "get_ocalhd Met: uncovered case get_obj"
1474 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
1475 val pre = check_preconds (assoc_thy"Isac") prls pre meth
1477 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1479 | get_ocalhd _ = error "get_ocalhd: uncovered definition"
1481 (* at the activeFormula set the Model, the Guard and the Specification
1482 to empty and return a CalcHead;
1483 the 'origin' remains (for reconstructing all that) *)
1484 fun reset_calchead (pt, (p,_) : pos') =
1486 val () = case get_obj I pt p of
1488 | _ => error "reset_calchead: uncovered case get_obj"
1489 val pt = update_pbl pt p []
1490 val pt = update_met pt p []
1491 val pt = update_spec pt p e_spec
1492 in (pt, (p, Pbl) : pos') end