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 tac_ | Notappl of string
11 val nxt_specify_init_calc : fmz -> calcstate
12 val specify : tac_ -> pos' -> cid -> ptree ->
13 (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac * safe * ptree
14 val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
15 val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
16 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
18 val reset_calchead : ptree * pos' -> ptree * pos'
19 val get_ocalhd : ptree * pos' -> ocalhd
20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
21 val all_modspec : ptree * pos' -> ptree * 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 : ptree * pos' -> ptree * pos'
27 val is_complete_mod : ptree * pos' -> bool
28 val complete_spec : ptree * pos' -> ptree * pos'
29 val is_complete_spec : ptree * pos' -> bool
30 val some_spec : spec -> spec -> spec
31 (* these could go to Ctree ..*)
32 val show_pt : ptree -> unit
33 val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list
34 val get_interval : int list * pos_ -> pos' -> int -> ptree -> (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 (taci list) (* ev. several (hidden) steps;
73 in REVERSE order: first tac_ to apply is last_elem *)
74 val e_calcstate = ((EmptyPtree, e_pos'), [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 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' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
92 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
93 fun f_mout thy (Form' (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 (itm_out thy itm_)
260 | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
261 | mk_delete thy "#Relate" itm_ = Del_Relation(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 (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 = 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 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 => Problem (if pI = e_pblID then [] else pI)
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, ...} = 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 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 get_pbt) cpI,ppc) (dI,pI,mI);
641 in ((p, p_), ((p, p_), Uistate),
642 Form' (PpcKF (0,EdUndef,(length p),Nundef,
643 (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
647 val pre' = check_preconds thy prls pre met
648 val pb = foldl and_ (true, map fst pre')
650 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
651 ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
652 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
654 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
656 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
657 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
658 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
659 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
660 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
661 val cpI = if pI = e_pblID then pI' else pI
662 val cmI = if mI = e_metID then mI' else mI
663 val {ppc, where_, prls, ...} = get_pbt cpI
665 case appl_add ctxt sel oris pbl ppc ct of
666 Add itm => (*..union old input *)
668 val pbl' = insert_ppc thy itm pbl
669 val arg = case sel of
670 "#Given" => Add_Given' (ct, pbl')
671 | "#Find" => Add_Find' (ct, pbl')
672 | "#Relate"=> Add_Relation'(ct, pbl')
673 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
674 val ((p, Pbl), _, _, pt') = generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
675 val pre = check_preconds thy prls where_ pbl'
676 val pb = foldl and_ (true, map fst pre)
678 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
679 val ppc = if p_= Pbl then pbl' else met
681 ((p, p_), ((p, p_), Uistate),
682 Form' (PpcKF (0, EdUndef, (length p), Nundef,
683 (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')
687 val pre = check_preconds thy prls where_ pbl
688 val pb = foldl and_ (true, map fst pre)
690 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
691 (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
692 in ((p, p_), ((p, p_), Uistate), Error' (Error_ msg), nxt, Safe,pt) end
695 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
696 let (* either """"""""""""""" all empty or complete *)
697 val thy = assoc_thy dI'
699 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
701 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
702 val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
703 (oris, (dI',pI',mI'), e_term)
704 val pt = update_ctxt pt [] ctxt
705 val (pbl, pre) = ([], [])
709 (([], Pbl), (([], Pbl), Uistate),
710 Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
711 Refine_Tacitly pI', Safe, pt)
713 (([], Pbl), (([], Pbl), Uistate),
714 Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
715 Model_Problem, Safe, pt)
717 (* ONLY for STARTING modeling phase *)
718 | specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
720 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
721 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
722 (oris, dI',pI',mI', dI, ctxt)
723 | _ => error "specify (Model_Problem': uncovered case get_obj"
724 val thy' = if dI = e_domID then dI' else dI
725 val thy = assoc_thy thy'
726 val {ppc, prls, where_, ...} = get_pbt pI'
727 val pre = check_preconds thy prls where_ pbl
728 val pb = foldl and_ (true, map fst pre)
729 val ((p, _), _, _, pt) =
730 generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
731 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
732 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
734 ((p, Pbl), ((p, p_), Uistate),
735 Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
738 (* called only if no_met is specified *)
739 | specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
741 val (dI', ctxt) = case get_obj I pt p of
742 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
743 | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
744 val {met, thy,...} = get_pbt pIre
745 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
746 val ((p,_), _, _, pt) =
747 generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
748 val (pbl, pre, _) = ([], [], false)
749 in ((p, Pbl), (pos, Uistate),
750 Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
751 Model_Problem, Safe, pt)
753 | specify (Refine_Problem' rfd) pos _ pt =
755 val ctxt = get_ctxt pt pos
756 val (pos, _, _, pt) =
757 generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
759 (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Problems (RefinedKF rfd), Model_Problem, Safe, pt)
761 (*WN110515 initialise ctxt again from itms and add preconds*)
762 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
764 val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
765 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
766 (oris, dI', pI', mI', dI, mI, ctxt, met)
767 | _ => error "specify (Specify_Problem': uncovered case get_obj"
768 val thy = assoc_thy dI
770 case generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
771 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
772 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
773 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
774 val mI'' = if mI=e_metID then mI' else mI
775 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o get_pbt) pI,
776 (#ppc o get_met) mI'') (dI, pI, mI);
778 ((p,Pbl), (pos,Uistate),
779 Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
782 (*WN110515 initialise ctxt again from itms and add preconds*)
783 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt =
785 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
786 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
787 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
788 | _ => error "specify (Specify_Problem': uncovered case get_obj"
789 val {ppc,pre,prls,...} = get_met mID
790 val thy = assoc_thy dI
791 val oris = add_field' thy ppc oris
792 val dI'' = if dI=e_domID then dI' else dI
793 val pI'' = if pI = e_pblID then pI' else pI
794 val met = if met = [] then pbl else met
795 val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris
796 val (pos, _, _, pt) =
797 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
798 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
799 ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
802 Form' (PpcKF (0, EdUndef, length p, Nundef, (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
805 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
806 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
807 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
808 | specify (Specify_Theory' domID) (pos as (p,p_)) _ pt =
810 val p_ = case p_ of Met => Met | _ => Pbl
811 val thy = assoc_thy domID
812 val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
813 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
814 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
815 | _ => error "specify (Specify_Theory': uncovered case get_obj"
816 val mppc = case p_ of Met => met | _ => pbl
817 val cpI = if pI = e_pblID then pI' else pI
818 val {prls = per, ppc, where_ = pwh, ...} = get_pbt cpI
819 val cmI = if mI = e_metID then mI' else mI
820 val {prls = mer, ppc = mpc, pre= mwh, ...} = get_met cmI
822 Met => (check_preconds thy mer mwh met)
823 | _ => (check_preconds thy per pwh pbl)
824 val pb = foldl and_ (true, map fst pre)
828 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
830 ((p, p_), (pos, Uistate),
831 Form'(PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
834 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
836 val ((p, p_), _, _, pt) = generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
837 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
839 ((p,p_), (pos,Uistate),
840 Form' (PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
844 | specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m')
846 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
847 -- for input from scratch*)
848 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
850 val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
851 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
852 (oris, dI', pI', dI, pI, pbl, ctxt)
853 | _ => error "specify (Specify_Theory': uncovered case get_obj"
854 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
855 val cpI = if pI = e_pblID then pI' else pI;
857 case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
858 Add itm (*..union old input *) =>
860 val pbl' = insert_ppc thy itm pbl
861 val (tac, tac_) = case sel of
862 "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
863 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
864 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
865 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
866 val (p, Pbl, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
867 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
868 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
870 ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
872 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
873 FIXME ..and dont abuse a tactic for that purpose*)
874 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
875 (e_pos', (e_istate, e_ctxt)))], [], ptp)
877 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
879 val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
880 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
881 (oris, dI', mI', dI, mI, met, ctxt)
882 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
883 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
884 val cmI = if mI = e_metID then mI' else mI;
886 case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
887 Add itm (*..union old input *) =>
889 val met' = insert_ppc thy itm met;
890 val (tac,tac_) = case sel of
891 "#Given" => (Add_Given ct, Add_Given' (ct, met'))
892 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
893 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
894 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
895 val (p, Met, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
896 ((p, Met), c, _, pt') => (p, Met, c, pt')
897 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
899 ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))
901 | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
903 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
905 fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) =
906 ((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm)
907 handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm)
908 (*dsc in oris, but not in pbl pat list: keep this dsc*)
910 (* filter out oris which have same description in itms *)
911 fun filter_outs oris [] = oris
912 | filter_outs oris (i::itms) =
914 val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris
919 (* filter oris which are in pbt, too *)
920 fun filter_pbt oris pbt =
922 val dscs = map (fst o snd) pbt
924 filter ((member op= dscs) o (#4 : ori -> term)) oris
927 (* combine itms from pbl + met and complete them wrt. pbt *)
928 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
929 fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met =
931 val vat = max_vt pits;
932 val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits)
933 val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris
934 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
936 itms @ (map (ori2Coritm met) os)
939 (* complete model and guard of a calc-head *)
940 fun complete_mod_ (oris, mpc, ppc, probl) =
942 val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl
943 val vat = if probl = [] then 1 else max_vt probl
944 val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris
945 val pors = filter_outs pors pits (*which are in pbl already*)
946 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
947 val pits = pits @ (map (ori2Coritm ppc) pors)
948 val mits = complete_metitms oris pits [] mpc
951 fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =
952 (if dI = e_domID then odI else dI,
953 if pI = e_pblID then opI else pI,
954 if mI = e_metID then omI else mI) : spec
956 (* find a next applicable tac (for calcstate) and update ptree
957 (for ev. finding several more tacs due to hide) *)
958 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
959 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
960 (* WN.24.10.03 fun nxt_solv = ...................................?? *)
961 fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) =
963 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
964 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
965 | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
966 val (dI, pI, mI) = some_spec ospec spec
967 val thy = assoc_thy dI
968 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
969 val {cas, ppc, ...} = get_pbt pI
970 val pbl = init_pbl ppc (* fill in descriptions *)
971 (*----------------if you think, this should be done by the Dialog
972 in the java front-end, search there for WN060225-modelProblem----*)
973 val (pbl, met) = case cas of
975 | _ => complete_mod_ (oris, mpc, ppc, probl)
976 (*----------------------------------------------------------------*)
977 val tac_ = Model_Problem' (pI, pbl, met)
978 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
979 in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
980 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
981 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
982 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
983 (*. called only if no_met is specified .*)
984 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
986 val (oris, dI, ctxt) = case get_obj I pt p of
987 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
988 | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
989 val opt = refine_ori oris pI
994 val {met, ...} = get_pbt pI'
995 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
996 val mI = if length met = 0 then e_metID else hd met
997 val thy = assoc_thy dI
998 val (pos, c, _, pt) =
999 generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1001 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1002 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1004 | NONE => ([], [], ptp)
1006 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1008 val (dI, dI', probl, ctxt) = case get_obj I pt p of
1009 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
1010 (dI, dI', probl, ctxt)
1011 | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
1012 val thy = if dI' = e_domID then dI else dI'
1014 case refine_pbl (assoc_thy thy) pI probl of
1015 NONE => ([], [], ptp)
1018 val (pos,c,_,pt) = generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1020 ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1023 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1025 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
1026 PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>
1027 (oris, dI, dI', pI', probl, ctxt)
1029 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1030 val {ppc,where_,prls,...} = get_pbt pI
1032 if pI' = e_pblID andalso pI = e_pblID
1033 then (false, (init_pbl ppc, []))
1034 else match_itms_oris thy probl (ppc,where_,prls) oris
1035 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1036 val (c, pt) = case generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1037 ((_, Pbl), c, _, pt) => (c, pt)
1040 ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1042 (* transfers oris (not required in pbl) to met-model for script-env
1043 FIXME.WN.8.03: application of several mIDs to SAME model? *)
1044 | nxt_specif (Specify_Method mID) (pt, pos as (p,_)) =
1046 val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
1047 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
1048 => (oris, pbl, dI, met, ctxt)
1049 | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
1050 val {ppc,pre,prls,...} = get_met mID
1051 val thy = assoc_thy dI
1052 val oris = add_field' thy ppc oris
1053 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1054 val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris
1055 val (pos, c, _, pt) =
1056 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1058 ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
1060 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =
1062 val ctxt = get_ctxt pt pos
1063 val (pos, c, _, pt) =
1064 generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1065 in (*FIXXXME: check if pbl can still be parsed*)
1066 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
1069 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
1071 val ctxt = get_ctxt pt pos
1072 val (pos, c, _, pt) = generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1073 in (*FIXXXME: check if met can still be parsed*)
1074 ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
1076 | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')
1078 (* get the values from oris; handle the term list w.r.t. penv *)
1079 fun vals_of_oris oris =
1080 ((map (mkval' o (#5 : ori -> term list))) o
1081 (filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris
1083 (* create a calc-tree with oris via an cas.refined pbl *)
1084 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1086 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1088 val {cas, met, ppc, thy, ...} = get_pbt pI
1089 val dI = if dI = "" then theory2theory' thy else dI
1090 val mI = if mI = [] then hd met else mI
1091 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1092 val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
1093 ([], (dI,pI,mI), hdl)
1094 val pt = update_spec pt [] (dI, pI, mI)
1095 val pits = init_pbl' ppc
1096 val pt = update_pbl pt [] pits
1097 in ((pt, ([] , Pbl)), []) : calcstate end
1100 then (* from met-browser *)
1102 val {ppc, ...} = get_met mI
1103 val dI = if dI = "" then "Isac" else dI
1105 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1106 val pt = update_spec pt [] (dI, pI, mI)
1107 val mits = init_pbl' ppc
1108 val pt = update_met pt [] mits
1109 in ((pt, ([], Met)), []) end
1110 else (* new example, pepare for interactive modeling *)
1113 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
1114 in ((pt, ([], Pbl)), []) end
1115 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1116 let (* both """"""""""""""""""""""""" either empty or complete *)
1117 val thy = assoc_thy dI
1118 val (pI, (pors, pctxt), mI) =
1122 val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1123 val pI' = refine_ori' pors pI;
1124 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1125 (hd o #met o get_pbt) pI')
1127 else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1128 val {cas, ppc, thy = thy', ...} = get_pbt pI (*take dI from _refined_ pbl*)
1129 val dI = theory2theory' (maxthy thy thy')
1130 val hdl = case cas of
1131 NONE => pblterm dI pI
1132 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
1134 cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1135 val pt = update_ctxt pt [] pctxt
1137 ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1140 fun get_spec_form m ((p, p_) : pos') pt =
1141 let val (_, _, f, _, _, _) = specify m (p, p_) [] pt
1144 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1145 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1146 fun tag_form thy (formal, given) =
1148 val gf = (head_of given) $ formal;
1149 val _ = Thm.global_cterm_of thy gf
1151 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1152 " .. " ^ term_to_string''' thy formal ^ " ..types do not match")
1154 fun chktyp thy (n, fs, gs) =
1155 ((writeln o (term_to_string''' thy) o (nth n)) fs;
1156 (writeln o (term_to_string''' thy) o (nth n)) gs;
1157 tag_form thy (nth n fs, nth n gs))
1158 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
1160 (* check pbltypes, announces one failure a time *)
1161 fun chk_vars ctppc =
1163 val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
1164 val chked = subtract op = gi wh
1166 if chked <> [] then ("wh\\gi", chked)
1168 let val chked = subtract op = (union op = gi fi) re
1171 then ("re\\(gi union fi)", chked)
1176 (* check a new pbltype: variables (Free) unbound by given, find*)
1177 fun unbound_ppc ctppc =
1179 val {Given = gi, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
1181 distinct (subtract op = (union op = gi fi) re)
1184 (* f, a binary operator, is nested right associative *)
1187 fun fld _ (x :: []) = x
1188 | fld f (x :: x' :: []) = f (x', x)
1189 | fld f (x :: x' :: xs) = f (fld f (x' :: xs), x)
1190 | fld _ _ = error "foldr1 uncovered definition"
1191 in ((fld f) o rev) xs end
1193 (* f, a binary operator, is nested leftassociative *)
1194 fun foldl1 _ (x :: []) = x
1195 | foldl1 f (x :: x' :: []) = f (x, x')
1196 | foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs))
1197 | foldl1 _ _ = error "foldl1 uncovered definition"
1199 (* called only once, if a Subproblem has been located in the script*)
1200 fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
1202 ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1203 | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1204 (*all stored in tac_ itms^^^^^^^^^^*)
1205 | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_)
1207 (* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *)
1208 fun eq4 v (_, vts, _, _, _) = member op = vts v
1209 fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d
1211 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1212 + met from fmz; assumes pos on PblObj, meth = [] *)
1213 fun complete_mod (pt, pos as (p, p_) : pos') =
1215 val _ = if p_ <> Pbl
1216 then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
1218 val (oris, ospec, probl, spec) = case get_obj I pt p of
1219 PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
1220 | _ => error "complete_mod: unvered case get_obj"
1221 val (_, pI, mI) = some_spec ospec spec
1222 val mpc = (#ppc o get_met) mI
1223 val ppc = (#ppc o get_pbt) pI
1224 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1225 val pt = update_pblppc pt p pits
1226 val pt = update_metppc pt p mits
1227 in (pt, (p, Met) : pos') end
1229 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1230 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1231 fun all_modspec (pt, (p, _) : pos') =
1233 val (pors, dI, pI, mI) = case get_obj I pt p of
1234 PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
1235 | _ => error "all_modspec: uncovered case get_obj"
1236 val {ppc, ...} = get_met mI
1237 val (_, vals) = oris2fmz_vals pors
1238 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1239 |> declare_constraints' vals
1240 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
1241 val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
1242 val pt = update_spec pt p (dI, pI, mI)
1243 val pt = update_ctxt pt p ctxt
1245 (pt, (p, Met) : pos')
1248 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
1249 fun is_complete_mod_ ([] : itm list) = false
1250 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
1252 fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
1253 if (is_pblobj o (get_obj I pt)) p
1254 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1255 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1256 | is_complete_mod (pt, pos as (p, Met)) =
1257 if (is_pblobj o (get_obj I pt)) p
1258 then (is_complete_mod_ o (get_obj g_met pt)) p
1259 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1260 | is_complete_mod (_, pos) =
1261 error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
1263 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
1264 fun is_complete_spec (pt, pos as (p, _) : pos') =
1265 if (not o is_pblobj o (get_obj I pt)) p
1266 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1268 let val (dI,pI,mI) = get_obj g_spec pt p
1269 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end
1271 (* complete empty items in specification from origin (pbl, met ev.refined);
1272 assumes 'is_complete_mod' *)
1273 fun complete_spec (pt, pos as (p, _) : pos') =
1275 val (ospec, spec) = case get_obj I pt p of
1276 PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
1277 | _ => error "complete_spec: uncovered case get_obj"
1278 val pt = update_spec pt p (some_spec ospec spec)
1283 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
1285 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
1287 val (_, _, metID) = get_somespec' spec spec'
1288 val pre = if metID = e_metID then []
1291 val {prls, pre= where_, ...} = get_met metID
1292 val pre = check_preconds' prls where_ meth 0
1294 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
1296 ModSpec (allcorrect, Met, hdl, meth, pre, spec)
1298 | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
1300 val (_, pI, _) = get_somespec' spec spec'
1301 val pre = if pI = e_pblID then []
1304 val {prls, where_, ...} = get_pbt pI
1305 val pre = check_preconds' prls where_ probl 0
1307 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
1309 ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
1311 | pt_model _ _ = error "pt_model: uncovered definition"
1313 fun pt_form (PrfObj {form, ...}) = Form form
1314 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
1316 val (dI, pI, _) = get_somespec' spec spec'
1317 val {cas, ...} = get_pbt pI
1319 NONE => Form (pblterm dI pI)
1320 | SOME t => Form (subst_atomic (mk_env probl) t)
1323 (* pt_extract returns
1324 # the formula at pos
1325 # the tactic applied to this formula
1326 # the list of assumptions generated at this formula
1327 (by application of another tac to the preceding formula !)
1328 pos is assumed to come from the frontend, ie. generated by moveDown.
1329 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
1330 TODO 110417 get assumptions from ctxt !?
1332 fun pt_extract (pt, ([], Res)) =
1333 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
1335 val (f, asm) = get_obj g_result pt []
1336 in (Form f, NONE, asm) end
1337 | pt_extract (pt,(p,Res)) =
1339 val (f, asm) = get_obj g_result pt p
1343 if is_pblobj' pt (lev_up p)
1346 val pI = case get_obj I pt (lev_up p) of
1347 PblObj{spec = (_, pI, _), ...} => pI
1348 | _ => error "pt_extract last_onlev: uncovered case get_obj"
1349 in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
1350 else SOME End_Trans (* WN0502 TODO for other branches *)
1352 let val p' = lev_on p
1357 val (dI ,pI) = case get_obj I pt p' of
1358 PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
1359 | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
1360 in SOME (Subproblem (dI, pI)) end
1362 if f = get_obj g_form pt p'
1363 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1364 else SOME (Take (term2str (get_obj g_form pt p')))
1366 in (Form f, tac, asm) end
1367 | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
1369 val ppobj = get_obj I pt p
1370 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1371 val tac = g_tac ppobj
1372 in (f, SOME tac, []) end
1374 (** get the formula from a ctree-node:
1375 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1376 take res from all other PrfObj's
1377 Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
1378 fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
1379 [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
1380 | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
1381 [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
1382 | formres _ _ = error "formres: uncovered definition"
1383 fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
1384 [("stepform", (p, Res), r)]
1385 | form _ _ = error "form: uncovered definition"
1387 (* assumes to take whole level, in particular hd -- for use in interSteps *)
1388 fun get_formress fs _ [] = flat fs
1389 | get_formress fs p (nd::nds) =
1390 (* start with 'form+res' and continue with trying 'res' only*)
1391 get_forms (fs @ [formres p nd]) (lev_on p) nds
1392 and get_forms fs _ [] = flat fs
1393 | get_forms fs p (nd::nds) =
1395 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1396 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1397 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1398 (* continue with trying 'res' only*)
1399 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1401 (** get an 'interval' 'from' 'to' of formulae from a ptree **)
1402 (* WN0401 this functionality belongs to ctree.sml *)
1403 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
1404 | eq_pos' (p1, Res) (p2, Res) = p1 = p2
1405 | eq_pos' (p1, Pbl) (p2, p2_) =
1406 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1407 | eq_pos' (p1, Met) (p2, p2_) =
1408 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1409 | eq_pos' _ _ = false;
1411 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
1412 total ordering Position#compareTo(Position p) in the java-code
1413 val get_interval = fn
1414 : pos' -> : from is "move_up 1st-element" to return
1415 pos' -> : to the last element to be returned; from < to
1416 int -> : level: 0 gets the flattest sub-tree possible
1417 >999 gets the deepest sub-tree possible
1419 (pos' * : of the formula
1420 Term.term) : the formula
1422 fun get_interval from to level pt =
1424 fun get_inter c (from : pos') (to : pos') lev pt =
1425 if eq_pos' from to orelse from = ([], Res)
1427 let val (f, _, _) = pt_extract (pt, from)
1429 ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)]
1430 | Form t => c @ [(from, t)]
1433 if lev < lev_of from
1434 then (get_inter c (move_dn [] pt from) to lev pt)
1435 handle (PTREE _(*from move_dn too far*)) => c
1438 val (f, _, _) = pt_extract (pt, from)
1439 val term = case f of
1440 ModSpec (_,_,headline,_,_,_) => headline
1442 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1443 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1445 in get_inter [] from to level pt end
1448 fun posform2str (pos : pos', form) =
1449 "(" ^ pos'2str pos ^ ", " ^
1450 (case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^
1452 fun posforms2str pfs =
1453 (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs
1454 fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"
1455 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
1457 (* WN050225 omits the last step, if pt is incomplete *)
1458 fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
1460 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
1461 fun get_ocalhd (pt, (p, Pbl) : pos') =
1463 val (ospec, hdf', spec, probl) = case get_obj I pt p of
1464 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1465 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1466 val {prls, where_, ...} = get_pbt (#2 (some_spec ospec spec))
1467 val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1469 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1471 | get_ocalhd (pt, (p, Met)) =
1473 val (ospec, hdf', spec, meth) = case get_obj I pt p of
1474 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1475 | _ => error "get_ocalhd Met: uncovered case get_obj"
1476 val {prls, pre, ...} = get_met (#3 (some_spec ospec spec))
1477 val pre = check_preconds (assoc_thy"Isac") prls pre meth
1479 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1481 | get_ocalhd _ = error "get_ocalhd: uncovered definition"
1483 (* at the activeFormula set the Model, the Guard and the Specification
1484 to empty and return a CalcHead;
1485 the 'origin' remains (for reconstructing all that) *)
1486 fun reset_calchead (pt, (p,_) : pos') =
1488 val () = case get_obj I pt p of
1490 | _ => error "reset_calchead: uncovered case get_obj"
1491 val pt = update_pbl pt p []
1492 val pt = update_met pt p []
1493 val pt = update_spec pt p e_spec
1494 in (pt, (p, Pbl) : pos') end