1 (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in Selem and Stool (mstools.sml).
3 TODO: allocate elements of structure Selem and of structure Stool appropriately.
4 Author: Walther Neuper 991122, Mathias Lehnfeld
5 (c) due to copyright terms
11 datatype appl = Appl of Tac.tac_ | Notappl of string
12 val nxt_specify_init_calc : Selem.fmz -> calcstate
13 val specify : Tac.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
14 Ctree.pos' * (Ctree.pos' * Selem.istate) * Generate.mout * Tac.tac * Selem.safe * Ctree.ctree
15 val nxt_specif : Tac.tac -> Ctree.state -> calcstate'
16 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> spec -> Model.itm list * Model.itm list ->
17 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Tac.tac
19 val reset_calchead : Ctree.state -> Ctree.state
20 val get_ocalhd : Ctree.state -> Ctree.ocalhd
21 val ocalhd_complete : Model.itm list -> (bool * term) list -> domID * pblID * metID -> bool
22 val all_modspec : Ctree.state -> Ctree.state
24 val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> pat list -> Model.itm list
25 val insert_ppc' : Model.itm -> Model.itm list -> Model.itm list
27 val complete_mod : Ctree.state -> Ctree.state
28 val is_complete_mod : Ctree.state -> bool
29 val complete_spec : Ctree.state -> Ctree.state
30 val is_complete_spec : Ctree.state -> bool
31 val some_spec : spec -> spec -> spec
32 (* these could go to Ctree ..*)
33 val show_pt : Ctree.ctree -> unit
34 val pt_extract : Ctree.state -> Ctree.ptform * Tac.tac option * term list
35 val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list
37 val match_ags : theory -> pat list -> term list -> Model.ori list
38 val match_ags_msg : pblID -> term -> term list -> unit
39 val oris2fmz_vals : Model.ori list -> string list * term list
40 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
41 val is_known : Proof.context -> string -> Model.ori list -> term -> string * Model.ori * term list
42 val is_notyet_input : Proof.context -> Model.itm list -> term list -> Model.ori -> ('a * (term * term)) list
44 val ppc2list : 'a Model.ppc -> 'a list
45 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
46 val e_calcstate : Ctree.state * Generate.taci list
47 val e_calcstate' : calcstate'
48 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
49 val vals_of_oris : Model.ori list -> term list
50 val is_error : Model.itm_ -> bool
51 val is_copy_named : 'a * ('b * term) -> bool
52 val ori2Coritm : pat list -> Model.ori -> Model.itm
53 val is_copy_named_idstr : string -> bool
54 val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
55 val mtc : theory -> pat -> term -> Model.preori option
56 val cpy_nam : pat list -> Model.preori list -> pat -> Model.preori
57 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
59 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
60 val variants_in : term list -> int
61 val is_untouched : Model.itm -> bool
62 val is_list_type : typ -> bool
63 val parse_ok : Model.itm_ list -> bool
64 val all_dsc_in : Model.itm_ list -> term list
65 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
66 val chk_vars : term Model.ppc -> string * term list
67 val unbound_ppc : term Model.ppc -> term list
68 val nxt_model_pbl : Tac.tac_ -> Ctree.state -> Tac.tac_
69 val is_complete_modspec : Ctree.state -> bool
70 val get_formress : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
71 (string * Ctree.pos' * term) list
72 val get_forms : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
73 (string * Ctree.pos' * term) list
76 structure Chead(**): CALC_HEAD(**) =
81 (* the state wich is stored after each step of calculation; it contains
82 the calc-state and a list of [tac,istate](="tacis") to be applied next.
83 the last_elem tacis is the first to apply to the calc-state and
84 the (only) one shown to the front-end as the 'proposed tac'.
85 the calc-state resulting from the application of tacis is not stored,
86 because the tacis hold enough information for efficiently rebuilding
87 this state just by "fun generate "
90 (ctree * pos') * (* the calc-state to which the tacis could be applied *)
91 (Generate.taci list) (* ev. several (hidden) steps;
92 in REVERSE order: first tac_ to apply is last_elem *)
93 val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]);
95 (*the state used during one calculation within the mathengine; it contains
96 a list of [tac,istate](="tacis") which generated the the calc-state;
97 while this state's tacis are extended by each (internal) step,
98 the calc-state is used for creating new nodes in the calc-tree
99 (eg. applicable_in requires several particular nodes of the calc-tree)
100 and then replaced by the the newly created;
101 on leave of the mathengine the resuing calc-state is dropped anyway,
102 because the tacis hold enought information for efficiently rebuilding
103 this state just by "fun generate ".*)
105 Generate.taci list * (* cas. several (hidden) steps;
106 in REVERSE order: first tac_ to apply is last_elem *)
107 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
108 (ctree * pos') (* the calc-state resulting from the application of tacis *)
109 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
111 (* is the calchead complete ? *)
112 fun ocalhd_complete its pre (dI, pI, mI) =
113 foldl and_ (true, map #3 its) andalso
114 foldl and_ (true, map #1 pre) andalso
115 dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID
117 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
118 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
119 fun oris2fmz_vals oris =
120 let fun ori2fmz_vals (_, _, _, dsc, ts) =
121 ((term2str o Model.comp_dts') (dsc, ts), last_elem ts)
122 handle _ => error ("ori2fmz_env called with " ^ terms2str ts)
123 in (split_list o (map ori2fmz_vals)) oris end
125 (* make a term 'typeless' for comparing with another 'typeless' term;
126 'type-less' usually is illtyped *)
127 fun typeless (Const (s, _)) = (Const (s, e_type))
128 | typeless (Free (s, _)) = (Free (s, e_type))
129 | typeless (Var (n, _)) = (Var (n, e_type))
130 | typeless (Bound i) = (Bound i)
131 | typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t)
132 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
134 (* to an input (d,ts) find the according ori and insert the ts)
135 WN.11.03: + dont take first inter<>[] *)
136 fun seek_oridts ctxt sel (d, ts) [] =
137 ("seek_oridts: input ('" ^
138 (term_to_string' ctxt (Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
141 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
142 if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
143 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
144 else seek_oridts ctxt sel (d, ts) oris
146 (* to an input (_,ts) find the according ori and insert the ts *)
147 fun seek_orits ctxt _ ts [] =
148 ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
149 "') not found in oris (typed)", Model.e_ori, [])
150 | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
151 if sel = sel' andalso (inter op = ts ts') <> []
154 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
155 else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, Model.e_ori, [])
156 else seek_orits ctxt sel ts oris
158 (* find_first item with #1 equal to id *)
159 fun seek_ppc _ [] = NONE
160 | seek_ppc id (p :: ppc) = if id = #1 p then SOME p else seek_ppc id ppc
163 Appl of Tac.tac_ (* tactic is applicable at a certain position in the Ctree *)
164 | Notappl of string (* tactic is NOT applicable *)
166 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
167 gis @ whs @ fis @ wis @ res
169 (* get the number of variants in a problem in 'original',
170 assumes equal descriptions in immediate sequence *)
173 fun eq (x, y) = head_of x = head_of y
174 fun cnt _ [] _ n = ([n], [])
175 | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
176 fun coll _ xs [] = xs
177 | coll eq xs (y :: ys) =
178 let val (n, ys') = cnt eq (y :: ys) y 0
179 in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
180 val vts = subtract op = [1] (distinct (coll eq [] ts))
185 | _ => error "different variants in formalization"
188 fun is_list_type (Type ("List.list", _)) = true
189 | is_list_type _ = false
190 fun is_parsed (Model.Syn _) = false
192 fun parse_ok its = foldl and_ (true, map is_parsed its)
194 fun all_dsc_in itm_s =
196 fun d_in (Model.Cor ((d, _), _)) = [d]
197 | d_in (Model.Syn _) = []
198 | d_in (Model.Typ _) = []
199 | d_in (Model.Inc ((d,_),_)) = [d]
200 | d_in (Model.Sup (d,_)) = [d]
201 | d_in (Model.Mis (d,_)) = [d]
202 | d_in i = error ("all_dsc_in: uncovered case with " ^ Model.itm_2str i)
203 in (flat o (map d_in)) itm_s end;
205 fun is_error (Model.Cor _) = false
206 | is_error (Model.Sup _) = false
207 | is_error (Model.Inc _) = false
208 | is_error (Model.Mis _) = false
211 (* get the first term in ts from ori *)
212 fun getr_ct thy (_, _, fd, d, ts) =
213 (fd, ((term_to_string''' thy) o Model.comp_dts) (d,[hd ts]) : cterm')
215 (* get a term from ori, notyet input in itm.
216 the term from ori is thrown back to a string in order to reuse
217 machinery for immediate input by the user. *)
218 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
219 (fd, ((term_to_string''' thy) o Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts) : cterm')
221 (* in FE dsc, not dat: this is in itms ...*)
222 fun is_untouched (_, _, false, _, Model.Inc ((_, []), _)) = true
223 | is_untouched _ = false
225 (* select an item in oris, notyet input in itms
226 (precondition: in itms are only Model.Cor, Model.Sup, Model.Inc) *)
229 oris: from formalization 'type fmz', structured for efficient access
230 pbt : the problem-pattern to be matched with oris in order to get itms
231 itms: already input items
233 fun nxt_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
235 fun test_d d (i, _, _, _, itm_) = (d = (Model.d_in itm_)) andalso i <> 0
236 fun is_elem itms (_, (d, _)) =
237 case find_first (test_d d) itms of SOME _ => true | NONE => false
239 case filter_out (is_elem itms) pbt of
240 (f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o Model.comp_dts) (d, []) : cterm')
243 | nxt_add thy oris _ itms =
245 fun testr_vt v ori = member op= (#2 ori) v andalso (#3 ori) <> "#undef"
246 fun testi_vt v itm =member op= (#2 itm) v
247 fun test_id ids r = member op= ids (#1 r)
248 fun test_subset itm (_,_,_,d,ts) =
249 (Model.d_in (#5 itm)) = d andalso subset op = (Model.ts_in (#5 itm), ts)
250 fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false
251 | false_and_not_Sup (_, _, false, _, _) = true
252 | false_and_not_Sup _ = false
253 val v = if itms = [] then 1 else Model.max_vt itms
254 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
257 then itms (* because of dsc without dat *)
258 else filter (testi_vt v) itms; (* itms..vat *)
259 val icl = filter false_and_not_Sup vits; (* incomplete *)
262 then case filter_out (test_id (map #1 vits)) vors of
264 | miss => SOME (getr_ct thy (hd miss))
266 case find_first (test_subset (hd icl)) vors of
267 NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
268 | SOME ori => SOME (geti_ct thy ori (hd icl))
271 fun mk_delete thy "#Given" itm_ = Tac.Del_Given (Specify.itm_out thy itm_)
272 | mk_delete thy "#Find" itm_ = Tac.Del_Find (Specify.itm_out thy itm_)
273 | mk_delete thy "#Relate" itm_ = Tac.Del_Relation (Specify.itm_out thy itm_)
274 | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
275 fun mk_additem "#Given" ct = Tac.Add_Given ct
276 | mk_additem "#Find" ct = Tac.Add_Find ct
277 | mk_additem "#Relate"ct = Tac.Add_Relation ct
278 | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
280 (* determine the next step of specification;
281 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
282 eg. in rootpbl 'no_met':
284 preok predicates are _all_ ok (and problem matches completely)
285 oris immediately from formalization
286 (dI',pI',mI') specification coming from author/parent-problem
287 (pbl, item lists specified by user
288 met) -"-, tacitly completed by copy_probl
289 (dI,pI,mI) specification explicitly done by the user
290 (pbt, mpc) problem type, guard of method
292 fun nxt_spec Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
293 (if dI' = e_domID andalso dI = e_domID then (Pbl, Tac.Specify_Theory dI')
294 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Tac.Specify_Problem pI')
296 case find_first (is_error o #5) pbl of
297 SOME (_, _, _, fd, itm_) =>
298 (Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
300 (case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of
301 SOME (fd,ct') => (Pbl, mk_additem fd ct')
302 | NONE => (*pbl-items complete*)
303 if not preok then (Pbl, Tac.Refine_Problem pI')
304 else if dI = e_domID then (Pbl, Tac.Specify_Theory dI')
305 else if pI = e_pblID then (Pbl, Tac.Specify_Problem pI')
306 else if mI = e_metID then (Pbl, Tac.Specify_Method mI')
308 case find_first (is_error o #5) met of
309 SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_)
311 (case nxt_add (assoc_thy dI) oris mpc met of
312 SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
313 | NONE => (Met, Tac.Apply_Method mI))))
314 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
315 (case find_first (is_error o #5) met of
316 SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
318 case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
319 SOME (fd,ct') => (Met, mk_additem fd ct')
321 (if dI = e_domID then (Met, Tac.Specify_Theory dI')
322 else if pI = e_pblID then (Met, Tac.Specify_Problem pI')
323 else if not preok then (Met, Tac.Specify_Method mI)
324 else (Met, Tac.Apply_Method mI)))
325 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
327 (* update the itm_ already input, all..from ori *)
328 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
330 val ts' = union op = (Model.ts_in itm_) ts;
331 val pval = Model.pbl_ids' d ts'
332 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
333 val complete = if eq_set op = (ts', all) then true else false
337 (if fd = "#undef" then (id, vt, complete, fd, Model.Sup (d, ts'))
338 else (id, vt, complete, fd, Model.Cor ((d, ts'), (pid, pval))))
339 | (Model.Syn c) => error ("ori_2itm wants to overwrite " ^ c)
340 | (Model.Typ c) => error ("ori_2itm wants to overwrite " ^ c)
343 then (id, vt, true, fd, Model.Cor ((d, ts'), (pid, pval)))
344 else (id, vt, false, fd, Model.Inc ((d, ts'), (pid, pval)))
345 | (Model.Sup (d,ts')) => (*4.9.01 lost env*)
346 (*if fd = "#undef" then*) (id,vt,complete,fd,Model.Sup(d,ts'))
347 (*else (id,vt,complete,fd,Model.Cor((d,ts'),e))*)
348 (* 28.1.00: not completely clear ---^^^ etc.*)
349 | (Model.Mis _) => (* 4.9.01: Model.Mis just copied *)
351 then (id, vt, true, fd, Model.Cor ((d,ts'), (pid, pval)))
352 else (id, vt, false, fd, Model.Inc ((d,ts'), (pid, pval)))
353 | i => error ("ori_2itm: uncovered case of "^ Model.itm_2str i)
356 fun eq1 d (_, (d', _)) = (d = d')
357 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (Model.d_in itm_)
359 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
360 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
361 pval: value for problem-environment _NOT_ checked for 'inter' --
362 -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
363 (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
364 (*. is_input ori itms <=>
365 EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
366 (2) ori(ts) subset itm(ts) --- Err "already input"
367 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
368 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
369 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
370 case find_first (eq1 d) pbt of
371 SOME (_, (_, pid)) =>
372 (case find_first (eq3 f d) itms of
373 SOME (_,_,_,_,itm_) =>
374 let val ts' = inter op = (Model.ts_in itm_) ts
376 if subset op = (ts, ts')
377 then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", Model.e_itm) (*2*)
378 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
380 | NONE => ("", ori_2itm (Model.Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
381 | NONE => ("", ori_2itm (Model.Sup (d, ts)) e_term all (i, v, f, d, ts))
383 fun test_types ctxt (d,ts) =
385 val opt = (try Model.comp_dts) (d, ts)
386 val msg = case opt of
388 | NONE => (term_to_string' ctxt d ^ " " ^
389 (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped")
392 (* is the input term t known in oris ?
393 give feedback on all(?) strange input;
394 return _all_ terms already input to this item (e.g. valuesFor a,b) *)
395 fun is_known ctxt sel ori t =
397 val _ = tracing ("RM is_known: t=" ^ term2str t)
398 val ots = (distinct o flat o (map #5)) ori
399 val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots
400 val (d, ts) = Model.split_dts t
401 val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts)
403 if (subtract op = oids ids) <> []
404 then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), Model.e_ori, [])
408 if not (subset op = (map typeless ts, map typeless ots))
409 then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
410 "' not in example (typeless)", Model.e_ori, [])
412 (case seek_orits ctxt sel ts ori of
413 ("", ori_ as (_,_,_,d,ts), all) =>
414 (case test_types ctxt (d,ts) of
415 "" => ("", ori_, all)
416 | msg => (msg, Model.e_ori, []))
417 | (msg,_,_) => (msg, Model.e_ori, []))
419 if member op = (map #4 ori) d
420 then seek_oridts ctxt sel (d, ts) ori
421 else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
426 Add of Model.itm (* return-value of appl_add *)
427 | Err of string (* error-message *)
429 (* add an item to the model; check wrt. oris and pbt.
430 in contrary to oris<>[] below, this part handles user-input
431 extremely acceptive, i.e. accept input instead error-msg *)
432 fun appl_add ctxt sel [] ppc pbt ct =
434 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
436 case parseNEW ctxt ct of
437 NONE => Add (i, [], false, sel, Model.Syn ct)
439 let val (d, ts) = Model.split_dts t
442 then Add (i, [], false, sel, Model.Mis (Specify.dsc_unknown, hd ts))
444 (case find_first (eq1 d) pbt of
445 NONE => Add (i, [], true, sel, Model.Sup (d,ts))
446 | SOME (f, (_, id)) =>
447 let fun eq2 d (i, _, _, _, itm_) = d = (Model.d_in itm_) andalso i <> 0
448 in case find_first (eq2 d) ppc of
449 NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
450 | SOME (i', _, _, _, itm_) =>
454 val in_itm = Model.ts_in itm_
455 val ts' = union op = ts in_itm
456 val i'' = if in_itm = [] then i else i'
457 in Add (i'', [], true, f, Model.Cor ((d, ts'), (id, Model.pbl_ids' d ts')))end
458 else Add (i', [], true, f, Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
462 | appl_add ctxt sel oris ppc pbt str =
463 case parseNEW ctxt str of
464 NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
466 case is_known ctxt sel oris t of
468 (case is_notyet_input ctxt ppc all ori' pbt of
470 | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
471 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
473 (* make oris from args of the stac SubProblem and from pbt.
474 can this formal argument (of a model-pattern) be omitted in the arg-list
475 of a SubProblem ? see calcelems.sml 'type met ' *)
476 fun is_copy_named_idstr str =
477 case (rev o Symbol.explode) str of
478 "'" :: _ :: "'" :: _ =>
479 (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true)
481 (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false)
482 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t
484 (* should this formal argument (of a model-pattern) create a new identifier? *)
485 fun is_copy_named_generating_idstr str =
486 if is_copy_named_idstr str
488 case (rev o Symbol.explode) str of
489 "'" :: "'" :: "'" :: _ => false
492 fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t
494 (* split type-wrapper from scr-arg and build part of an ori;
495 an type-error is reported immediately, raises an exn,
496 subsequent handling of exn provides 2nd part of error message *)
497 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
498 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
499 SOME (([1], str, dsc, (*[var]*)
500 Model.split_dts' (dsc, var))) (*:ori without leading #*))
501 handle e as TYPE _ =>
502 (tracing (dashs 70 ^ "\n"
503 ^ "*** ERROR while creating the items for the model of the ->problem\n"
504 ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
505 ^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n"
506 ^ "*** description: " ^ term_detail2str dsc
507 ^ "*** value: " ^ term_detail2str var
508 ^ "*** typeconstructor in script: " ^ term_detail2str ty
509 ^ "*** checked by theory: " ^ theory2str thy ^ "\n"
511 writeln (@{make_string} e);
512 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
514 | mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t)
516 (* match each pat of the model-pattern with an actual argument;
517 precondition: copy-named vars are filtered out *)
518 fun matc _ ([]:pat list) _ oris = oris
521 error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
522 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
523 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
525 let val opt = mtc thy p a
528 SOME ori => matc thy pbt ags (oris @ [ori])
529 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
532 (* generate a new variable "x_i" name from a related given one "x"
533 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
534 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
535 but leave is_copy_named_generating as is, e.t. ss''' *)
536 fun cpy_nam (pbt: pat list) oris (p as (field, (dsc, t)): pat) =
537 (if is_copy_named_generating p
538 then (*WN051014 kept strange old code ...*)
539 let fun sel (_,_,d,ts) = Model.comp_ts (d, ts)
540 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
541 val ext = (last_elem o drop_last o Symbol.explode o free2str) t
542 val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
543 val vals = map sel oris
544 val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
545 in ([1], field, dsc, [mk_free (type_of t) cy_ext]) end
546 else ([1], field, dsc, [t])
547 ) handle _ => error ("cpy_nam: for "^(term2str t))
549 (* match the actual arguments of a SubProblem with a model-pattern
550 and create an ori list (in root-pbl created from formalization).
551 expects ags:pats = 1:1, while copy-named are filtered out of pats;
552 if no 1:1 the exn raised by matc/mtc and handled at call.
553 copy-named pats are appended in order to get them into the model-items *)
554 fun match_ags thy (pbt: pat list) ags =
555 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_)
556 val pbt' = filter_out is_copy_named pbt
557 val cy = filter is_copy_named pbt
558 val oris' = matc thy pbt' ags []
559 val cy' = map (cpy_nam pbt' oris') cy
560 val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
561 in (map flattup ors) end
563 (* report part of the error-msg which is not available in match_args *)
564 fun match_ags_msg pI stac ags =
566 val pats = (#ppc o Specify.get_pbt) pI
567 val msg = (dots 70^"\n"
568 ^ "*** problem "^strs2str pI ^ " has the ...\n"
569 ^ "*** model-pattern "^pats2str pats ^ "\n"
570 ^ "*** stac '"^term2str stac ^ "' has the ...\n"
571 ^ "*** arg-list "^terms2str ags ^ "\n"
573 (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
576 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
577 fun vars_of_pbl_' pbl_ =
579 fun var_of_pbl_ (_, (_, t)) = t: term
580 in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
582 fun overwrite_ppc thy itm ppc =
584 fun repl _ (_, _, _, _, itm_) [] =
585 error ("overwrite_ppc: " ^ (Model.itm_2str_ (thy2ctxt thy) itm_) ^ " not found")
586 | repl ppc' itm (p :: ppc) =
588 then ppc' @ [itm] @ ppc
589 else repl (ppc' @ [p]) itm ppc
590 in repl [] itm ppc end
592 (* 10.3.00: insert the already compiled itm into model;
593 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
594 fun insert_ppc thy itm ppc =
596 fun eq_untouched d (0, _, _, _, itm_) = (d = Model.d_in itm_)
597 | eq_untouched _ _ = false
598 val ppc' = case seek_ppc (#1 itm) ppc of
599 SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
600 | NONE => (ppc @ [itm])
601 in filter_out (eq_untouched ((Model.d_in o #5) itm)) ppc' end
603 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (Model.d_in itm_ = Model.d_in iitm_)
605 (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
606 handles superfluous items carelessly *)
607 fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
609 (* output the headline to a ppc *)
610 fun header p_ pI mI =
611 case p_ of Pbl => Generate.Problem (if pI = e_pblID then [] else pI)
612 | Met => Generate.Method mI
613 | pos => error ("header called with "^ pos_2str pos)
615 fun specify_additem sel (ct, _) (p, Met) _ pt =
617 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
618 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
619 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
620 | _ => error "specify_additem: uncovered case of get_obj I pt p"
621 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
622 val cpI = if pI = e_pblID then pI' else pI
623 val cmI = if mI = e_metID then mI' else mI
624 val {ppc, pre, prls, ...} = Specify.get_met cmI
626 case appl_add ctxt sel oris met ppc ct of
627 Add itm => (*..union old input *)
629 val met' = insert_ppc thy itm met
630 val arg = case sel of
631 "#Given" => Tac.Add_Given' (ct, met')
632 | "#Find" => Tac.Add_Find' (ct, met')
633 | "#Relate"=> Tac.Add_Relation'(ct, met')
634 | str => error ("specify_additem: uncovered case with " ^ str)
635 val (p, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p, Met) pt of
636 ((p, Met), _, _, pt') => (p, pt')
637 | _ => error "specify_additem: uncovered case of generate1"
638 val pre' = Stool.check_preconds thy prls pre met'
639 val pb = foldl and_ (true, map fst pre')
641 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
642 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
643 in ((p, p_), ((p, p_), Selem.Uistate),
644 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Selem.Safe, pt')
648 val pre' = Stool.check_preconds thy prls pre met
649 val pb = foldl and_ (true, map fst pre')
651 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
652 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
653 in ((p,p_), ((p,p_),Selem.Uistate), Generate.Error' msg, nxt, Selem.Safe, pt) end
655 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
657 val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
658 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
659 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
660 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
661 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
662 val cpI = if pI = e_pblID then pI' else pI
663 val cmI = if mI = e_metID then mI' else mI
664 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
666 case appl_add ctxt sel oris pbl ppc ct of
667 Add itm => (*..union old input *)
669 val pbl' = insert_ppc thy itm pbl
670 val arg = case sel of
671 "#Given" => Tac.Add_Given' (ct, pbl')
672 | "#Find" => Tac.Add_Find' (ct, pbl')
673 | "#Relate"=> Tac.Add_Relation'(ct, pbl')
674 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
675 val (p, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p,Pbl) pt of
676 ((p, Pbl), _, _, pt') => (p, pt')
677 | _ => error "specify_additem: uncovered case of Generate.generate1"
678 val pre = Stool.check_preconds thy prls where_ pbl'
679 val pb = foldl and_ (true, map fst pre)
681 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
682 val ppc = if p_= Pbl then pbl' else met
684 ((p, p_), ((p, p_), Selem.Uistate),
685 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Selem.Safe, pt')
689 val pre = Stool.check_preconds thy prls where_ pbl
690 val pb = foldl and_ (true, map fst pre)
692 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
693 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
694 in ((p, p_), ((p, p_), Selem.Uistate), Generate.Error' msg, nxt, Selem.Safe,pt) end
697 fun specify (Tac.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
698 let (* either """"""""""""""" all empty or complete *)
699 val thy = assoc_thy dI'
701 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
702 then ([], Selem.e_ctxt)
703 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
704 val (pt, _) = cappend_problem e_ctree [] (Selem.e_istate, ctxt) (fmz, spec')
705 (oris, (dI',pI',mI'), e_term)
706 val pt = update_ctxt pt [] ctxt
707 val (pbl, pre) = ([], [])
711 (([], Pbl), (([], Pbl), Selem.Uistate),
712 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
713 Tac.Refine_Tacitly pI', Selem.Safe, pt)
715 (([], Pbl), (([], Pbl), Selem.Uistate),
716 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
717 Tac.Model_Problem, Selem.Safe, pt)
719 (* ONLY for STARTING modeling phase *)
720 | specify (Tac.Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
722 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
723 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
724 (oris, dI',pI',mI', dI, ctxt)
725 | _ => error "specify (Model_Problem': uncovered case get_obj"
726 val thy' = if dI = e_domID then dI' else dI
727 val thy = assoc_thy thy'
728 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
729 val pre = Stool.check_preconds thy prls where_ pbl
730 val pb = foldl and_ (true, map fst pre)
731 val ((p, _), _, _, pt) =
732 Generate.generate1 thy (Tac.Model_Problem'([],pbl,met)) (Selem.Uistate, ctxt) pos pt
733 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
734 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
736 ((p, Pbl), ((p, p_), Selem.Uistate),
737 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
740 (* called only if no_met is specified *)
741 | specify (Tac.Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
743 val (dI', ctxt) = case get_obj I pt p of
744 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
745 | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
746 val {met, thy,...} = Specify.get_pbt pIre
747 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
748 val ((p,_), _, _, pt) =
749 Generate.generate1 thy (Tac.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Selem.Uistate, ctxt) pos pt
750 val (pbl, pre, _) = ([], [], false)
751 in ((p, Pbl), (pos, Selem.Uistate),
752 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
753 Tac.Model_Problem, Selem.Safe, pt)
755 | specify (Tac.Refine_Problem' rfd) pos _ pt =
757 val ctxt = get_ctxt pt pos
758 val (pos, _, _, pt) =
759 Generate.generate1 (assoc_thy "Isac") (Tac.Refine_Problem' rfd) (Selem.Uistate, ctxt) pos pt
761 (pos(*p,Pbl*), (pos(*p,Pbl*), Selem.Uistate), Generate.RefinedKF rfd, Tac.Model_Problem, Selem.Safe, pt)
763 (*WN110515 initialise ctxt again from itms and add preconds*)
764 | specify (Tac.Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
766 val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
767 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
768 (oris, dI', pI', mI', dI, mI, ctxt, met)
769 | _ => error "specify (Specify_Problem': uncovered case get_obj"
770 val thy = assoc_thy dI
772 case Generate.generate1 thy (Tac.Specify_Problem' (pI, (ok, (itms, pre)))) (Selem.Uistate, ctxt) pos pt of
773 ((p, Pbl), _, _, pt) => (p, pt)
774 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
775 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
776 val mI'' = if mI=e_metID then mI' else mI
777 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
778 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
780 ((p,Pbl), (pos,Selem.Uistate),
781 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
784 (*WN110515 initialise ctxt again from itms and add preconds*)
785 | specify (Tac.Specify_Method' (mID, _, _)) (pos as (p, _)) _ pt =
787 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
788 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
789 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
790 | _ => error "specify (Specify_Problem': uncovered case get_obj"
791 val {ppc,pre,prls,...} = Specify.get_met mID
792 val thy = assoc_thy dI
793 val oris = Specify.add_field' thy ppc oris
794 val dI'' = if dI=e_domID then dI' else dI
795 val pI'' = if pI = e_pblID then pI' else pI
796 val met = if met = [] then pbl else met
797 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
798 val (pos, _, _, pt) =
799 Generate.generate1 thy (Tac.Specify_Method' (mID, oris, itms)) (Selem.Uistate, ctxt) pos pt
800 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
801 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
803 (pos, (pos,Selem.Uistate),
804 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
807 | specify (Tac.Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
808 | specify (Tac.Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
809 | specify (Tac.Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
810 | specify (Tac.Specify_Theory' domID) (pos as (p,p_)) _ pt =
812 val p_ = case p_ of Met => Met | _ => Pbl
813 val thy = assoc_thy domID
814 val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
815 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
816 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
817 | _ => error "specify (Specify_Theory': uncovered case get_obj"
818 val mppc = case p_ of Met => met | _ => pbl
819 val cpI = if pI = e_pblID then pI' else pI
820 val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
821 val cmI = if mI = e_metID then mI' else mI
822 val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
824 Met => (Stool.check_preconds thy mer mwh met)
825 | _ => (Stool.check_preconds thy per pwh pbl)
826 val pb = foldl and_ (true, map fst pre)
830 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
832 ((p, p_), (pos, Selem.Uistate),
833 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
836 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
838 val ((p, p_), _, _, pt) = Generate.generate1 thy (Tac.Specify_Theory' domID) (Selem.Uistate, ctxt) (p,p_) pt
839 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
841 ((p,p_), (pos,Selem.Uistate),
842 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
846 | specify m' _ _ _ = error ("specify: not impl. for " ^ Tac.tac_2str m')
848 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
849 -- for input from scratch*)
850 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
852 val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
853 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
854 (oris, dI', pI', dI, pI, pbl, ctxt)
855 | _ => error "specify (Specify_Theory': uncovered case get_obj"
856 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
857 val cpI = if pI = e_pblID then pI' else pI;
859 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
860 Add itm (*..union old input *) =>
862 val pbl' = insert_ppc thy itm pbl
863 val (tac, tac_) = case sel of
864 "#Given" => (Tac.Add_Given ct, Tac.Add_Given' (ct, pbl'))
865 | "#Find" => (Tac.Add_Find ct, Tac.Add_Find' (ct, pbl'))
866 | "#Relate"=> (Tac.Add_Relation ct, Tac.Add_Relation'(ct, pbl'))
867 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
868 val (p, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p,Pbl) pt of
869 ((p, Pbl), c, _, pt') => (p, c, pt')
870 | _ => error "nxt_specif_additem: uncovered case generate1"
872 ([(tac, tac_, ((p, Pbl), (Selem.Uistate, ctxt)))], c, (pt', (p, Pbl)))
874 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
875 FIXME ..and dont abuse a tactic for that purpose*)
876 ([(Tac.Tac msg, Tac.Tac_ (Thy_Info_get_theory "Pure", msg,msg,msg),
877 (e_pos', (Selem.e_istate, Selem.e_ctxt)))], [], ptp)
879 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
881 val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
882 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
883 (oris, dI', mI', dI, mI, met, ctxt)
884 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
885 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
886 val cmI = if mI = e_metID then mI' else mI;
888 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
889 Add itm (*..union old input *) =>
891 val met' = insert_ppc thy itm met;
892 val (tac,tac_) = case sel of
893 "#Given" => (Tac.Add_Given ct, Tac.Add_Given' (ct, met'))
894 | "#Find" => (Tac.Add_Find ct, Tac.Add_Find' (ct, met'))
895 | "#Relate"=> (Tac.Add_Relation ct, Tac.Add_Relation'(ct, met'))
896 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
897 val (p, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p, Met) pt of
898 ((p, Met), c, _, pt') => (p, c, pt')
899 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
901 ([(tac, tac_, ((p, Met), (Selem.Uistate, ctxt)))], c, (pt', (p, Met)))
903 | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
905 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
907 fun ori2Coritm (pbt : pat list) (i, v, f, d, ts) =
908 (i, v, true, f, Model.Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts)))
909 handle _ => (i, v, true, f, Model.Cor ((d, ts), (d, ts)))
910 (*dsc in oris, but not in pbl pat list: keep this dsc*)
912 (* filter out oris which have same description in itms *)
913 fun filter_outs oris [] = oris
914 | filter_outs oris (i::itms) =
916 val ors = filter_out ((curry op = ((Model.d_in o #5) i)) o (#4)) oris
921 (* filter oris which are in pbt, too *)
922 fun filter_pbt oris pbt =
924 val dscs = map (fst o snd) pbt
926 filter ((member op= dscs) o (#4)) oris
929 (* combine itms from pbl + met and complete them wrt. pbt *)
930 (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
931 fun complete_metitms oris pits mits met =
933 val vat = Model.max_vt pits;
934 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
935 val ors = filter ((member_swap op= vat) o (#2)) oris
936 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
938 itms @ (map (ori2Coritm met) os)
941 (* complete model and guard of a calc-head *)
942 fun complete_mod_ (oris, mpc, ppc, probl) =
944 val pits = filter_out ((curry op= false) o (#3)) probl
945 val vat = if probl = [] then 1 else Model.max_vt probl
946 val pors = filter ((member_swap op = vat) o (#2)) oris
947 val pors = filter_outs pors pits (*which are in pbl already*)
948 val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
949 val pits = pits @ (map (ori2Coritm ppc) pors)
950 val mits = complete_metitms oris pits [] mpc
953 fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =
954 (if dI = e_domID then odI else dI,
955 if pI = e_pblID then opI else pI,
956 if mI = e_metID then omI else mI) : spec
958 (* find a next applicable tac (for calcstate) and update ctree
959 (for ev. finding several more tacs due to hide) *)
960 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
961 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
962 (* WN.24.10.03 fun nxt_solv = ...................................?? *)
963 fun nxt_specif (tac as Tac.Model_Problem) (pt, pos as (p, _)) =
965 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
966 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
967 | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
968 val (dI, pI, mI) = some_spec ospec spec
969 val thy = assoc_thy dI
970 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
971 val {cas, ppc, ...} = Specify.get_pbt pI
972 val pbl = Generate.init_pbl ppc (* fill in descriptions *)
973 (*----------------if you think, this should be done by the Dialog
974 in the java front-end, search there for WN060225-modelProblem----*)
975 val (pbl, met) = case cas of
977 | _ => complete_mod_ (oris, mpc, ppc, probl)
978 (*----------------------------------------------------------------*)
979 val tac_ = Tac.Model_Problem' (pI, pbl, met)
980 val (pos,c,_,pt) = Generate.generate1 thy tac_ (Selem.Uistate, ctxt) pos pt
981 in ([(tac, tac_, (pos, (Selem.Uistate, Selem.e_ctxt)))], c, (pt,pos)) end
982 | nxt_specif (Tac.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
983 | nxt_specif (Tac.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
984 | nxt_specif (Tac.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
985 (*. called only if no_met is specified .*)
986 | nxt_specif (Tac.Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
988 val (oris, dI, ctxt) = case get_obj I pt p of
989 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
990 | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
991 val opt = Specify.refine_ori oris pI
996 val {met, ...} = Specify.get_pbt pI'
997 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
998 val mI = if length met = 0 then e_metID else hd met
999 val thy = assoc_thy dI
1000 val (pos, c, _, pt) =
1001 Generate.generate1 thy (Tac.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Selem.Uistate, ctxt) pos pt
1003 ([(Tac.Refine_Tacitly pI, Tac.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1004 (pos, (Selem.Uistate, Selem.e_ctxt)))], c, (pt,pos))
1006 | NONE => ([], [], ptp)
1008 | nxt_specif (Tac.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1010 val (dI, dI', probl, ctxt) = case get_obj I pt p of
1011 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
1012 (dI, dI', probl, ctxt)
1013 | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
1014 val thy = if dI' = e_domID then dI else dI'
1016 case Specify.refine_pbl (assoc_thy thy) pI probl of
1017 NONE => ([], [], ptp)
1020 val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Tac.Refine_Problem' rfd) (Selem.Uistate, ctxt) pos pt
1022 ([(Tac.Refine_Problem pI, Tac.Refine_Problem' rfd, (pos, (Selem.Uistate, Selem.e_ctxt)))], c, (pt,pos))
1025 | nxt_specif (Tac.Specify_Problem pI) (pt, pos as (p,_)) =
1027 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
1028 PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>
1029 (oris, dI, dI', pI', probl, ctxt)
1031 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1032 val {ppc,where_,prls,...} = Specify.get_pbt pI
1034 if pI' = e_pblID andalso pI = e_pblID
1035 then (false, (Generate.init_pbl ppc, []))
1036 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
1037 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1038 val (c, pt) = case Generate.generate1 thy (Tac.Specify_Problem' (pI, pbl)) (Selem.Uistate, ctxt) pos pt of
1039 ((_, Pbl), c, _, pt) => (c, pt)
1042 ([(Tac.Specify_Problem pI, Tac.Specify_Problem' (pI, pbl), (pos, (Selem.Uistate, Selem.e_ctxt)))], c, (pt,pos))
1044 (* transfers oris (not required in pbl) to met-model for script-env
1045 FIXME.WN.8.03: application of several mIDs to SAME model? *)
1046 | nxt_specif (Tac.Specify_Method mID) (pt, pos as (p,_)) =
1048 val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
1049 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
1050 => (oris, pbl, dI, met, ctxt)
1051 | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
1052 val {ppc,pre,prls,...} = Specify.get_met mID
1053 val thy = assoc_thy dI
1054 val oris = Specify.add_field' thy ppc oris
1055 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1056 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
1057 val (pos, c, _, pt) =
1058 Generate.generate1 thy (Tac.Specify_Method' (mID, oris, itms)) (Selem.Uistate, ctxt) pos pt
1060 ([(Tac.Specify_Method mID, Tac.Specify_Method' (mID, oris, itms), (pos, (Selem.Uistate, Selem.e_ctxt)))], c, (pt, pos))
1062 | nxt_specif (Tac.Specify_Theory dI) (pt, pos as (_, Pbl)) =
1064 val ctxt = get_ctxt pt pos
1065 val (pos, c, _, pt) =
1066 Generate.generate1 (assoc_thy "Isac") (Tac.Specify_Theory' dI) (Selem.Uistate, ctxt) pos pt
1067 in (*FIXXXME: check if pbl can still be parsed*)
1068 ([(Tac.Specify_Theory dI, Tac.Specify_Theory' dI, (pos, (Selem.Uistate, ctxt)))], c,
1071 | nxt_specif (Tac.Specify_Theory dI) (pt, pos as (_, Met)) =
1073 val ctxt = get_ctxt pt pos
1074 val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Tac.Specify_Theory' dI) (Selem.Uistate, ctxt) pos pt
1075 in (*FIXXXME: check if met can still be parsed*)
1076 ([(Tac.Specify_Theory dI, Tac.Specify_Theory' dI, (pos, (Selem.Uistate, ctxt)))], c, (pt, pos))
1078 | nxt_specif m' _ = error ("nxt_specif: not impl. for " ^ Tac.tac2str m')
1080 (* get the values from oris; handle the term list w.r.t. penv *)
1081 fun vals_of_oris oris =
1082 ((map (Model.mkval' o (#5))) o
1083 (filter ((member_swap op= 1) o (#2)))) oris
1085 (* create a calc-tree with oris via an cas.refined pbl *)
1086 fun nxt_specify_init_calc ([], (dI, pI, mI)) =
1088 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1090 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
1091 val dI = if dI = "" then theory2theory' thy else dI
1092 val mI = if mI = [] then hd met else mI
1093 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1094 val (pt,_) = cappend_problem e_ctree [] (Selem.Uistate, Selem.e_ctxt) ([], (dI, pI, mI))
1095 ([], (dI,pI,mI), hdl)
1096 val pt = update_spec pt [] (dI, pI, mI)
1097 val pits = Generate.init_pbl' ppc
1098 val pt = update_pbl pt [] pits
1099 in ((pt, ([] , Pbl)), []) end
1102 then (* from met-browser *)
1104 val {ppc, ...} = Specify.get_met mI
1105 val dI = if dI = "" then "Isac" else dI
1107 cappend_problem e_ctree [] (Selem.e_istate, Selem.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1108 val pt = update_spec pt [] (dI, pI, mI)
1109 val mits = Generate.init_pbl' ppc
1110 val pt = update_met pt [] mits
1111 in ((pt, ([], Met)), []) end
1112 else (* new example, pepare for interactive modeling *)
1115 cappend_problem e_ctree [] (Selem.e_istate, Selem.e_ctxt) ([], e_spec) ([], e_spec, e_term)
1116 in ((pt, ([], Pbl)), []) end
1117 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
1118 let (* both """"""""""""""""""""""""" either empty or complete *)
1119 val thy = assoc_thy dI
1120 val (pI, (pors, pctxt), mI) =
1124 val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
1125 val pI' = Specify.refine_ori' pors pI;
1126 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1127 (hd o #met o Specify.get_pbt) pI')
1129 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
1130 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
1131 val dI = theory2theory' (maxthy thy thy')
1132 val hdl = case cas of
1133 NONE => pblterm dI pI
1134 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
1136 cappend_problem e_ctree [] (Selem.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1137 val pt = update_ctxt pt [] pctxt
1139 ((pt, ([], Pbl)), fst3 (nxt_specif Tac.Model_Problem (pt, ([], Pbl))))
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 chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
1154 (* check pbltypes, announces one failure a time *)
1155 fun chk_vars ctppc =
1157 val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
1158 val chked = subtract op = gi wh
1160 if chked <> [] then ("wh\\gi", chked)
1162 let val chked = subtract op = (union op = gi fi) re
1165 then ("re\\(gi union fi)", chked)
1170 (* check a new pbltype: variables (Free) unbound by given, find*)
1171 fun unbound_ppc ctppc =
1173 val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc)
1175 distinct (subtract op = (union op = gi fi) re)
1178 (* called only once, if a Subproblem has been located in the script*)
1179 fun nxt_model_pbl (Tac.Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
1181 ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Tac.Refine_Tacitly pblID) ptp)
1182 | _ => (snd3 o hd o fst3) (nxt_specif Tac.Model_Problem ptp))
1183 (*all stored in tac_ itms^^^^^^^^^^*)
1184 | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ Tac.tac_2str tac_)
1186 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1187 + met from fmz; assumes pos on PblObj, meth = [] *)
1188 fun complete_mod (pt, pos as (p, p_) : pos') =
1190 val _ = if p_ <> Pbl
1191 then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
1193 val (oris, ospec, probl, spec) = case get_obj I pt p of
1194 PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
1195 | _ => error "complete_mod: unvered case get_obj"
1196 val (_, pI, mI) = some_spec ospec spec
1197 val mpc = (#ppc o Specify.get_met) mI
1198 val ppc = (#ppc o Specify.get_pbt) pI
1199 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1200 val pt = update_pblppc pt p pits
1201 val pt = update_metppc pt p mits
1202 in (pt, (p, Met) : pos') end
1204 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1205 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1206 fun all_modspec (pt, (p, _) : pos') =
1208 val (pors, dI, pI, mI) = case get_obj I pt p of
1209 PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
1210 | _ => error "all_modspec: uncovered case get_obj"
1211 val {ppc, ...} = Specify.get_met mI
1212 val (_, vals) = oris2fmz_vals pors
1213 val ctxt = dI |> Thy_Info_get_theory |> Proof_Context.init_global
1214 |> Stool.declare_constraints' vals
1215 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
1216 val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
1217 val pt = update_spec pt p (dI, pI, mI)
1218 val pt = update_ctxt pt p ctxt
1220 (pt, (p, Met) : pos')
1223 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
1224 fun is_complete_mod_ [] = false
1225 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
1227 fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
1228 if (is_pblobj o (get_obj I pt)) p
1229 then (is_complete_mod_ o (get_obj g_pbl pt)) p
1230 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1231 | is_complete_mod (pt, pos as (p, Met)) =
1232 if (is_pblobj o (get_obj I pt)) p
1233 then (is_complete_mod_ o (get_obj g_met pt)) p
1234 else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1235 | is_complete_mod (_, pos) =
1236 error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
1238 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
1239 fun is_complete_spec (pt, pos as (p, _) : pos') =
1240 if (not o is_pblobj o (get_obj I pt)) p
1241 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1243 let val (dI,pI,mI) = get_obj g_spec pt p
1244 in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end
1246 (* complete empty items in specification from origin (pbl, met ev.refined);
1247 assumes 'is_complete_mod' *)
1248 fun complete_spec (pt, pos as (p, _) : pos') =
1250 val (ospec, spec) = case get_obj I pt p of
1251 PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
1252 | _ => error "complete_spec: uncovered case get_obj"
1253 val pt = update_spec pt p (some_spec ospec spec)
1258 fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
1260 fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
1262 val (_, _, metID) = get_somespec' spec spec'
1263 val pre = if metID = e_metID then []
1266 val {prls, pre= where_, ...} = Specify.get_met metID
1267 val pre = Stool.check_preconds' prls where_ meth 0
1269 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
1271 ModSpec (allcorrect, Met, hdl, meth, pre, spec)
1273 | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
1275 val (_, pI, _) = get_somespec' spec spec'
1276 val pre = if pI = e_pblID then []
1279 val {prls, where_, ...} = Specify.get_pbt pI
1280 val pre = Stool.check_preconds' prls where_ probl 0
1282 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
1284 ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
1286 | pt_model _ _ = error "pt_model: uncovered definition"
1288 fun pt_form (PrfObj {form, ...}) = Form form
1289 | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
1291 val (dI, pI, _) = get_somespec' spec spec'
1292 val {cas, ...} = Specify.get_pbt pI
1294 NONE => Form (pblterm dI pI)
1295 | SOME t => Form (subst_atomic (Model.mk_env probl) t)
1298 (* pt_extract returns
1299 # the formula at pos
1300 # the tactic applied to this formula
1301 # the list of assumptions generated at this formula
1302 (by application of another tac to the preceding formula !)
1303 pos is assumed to come from the frontend, ie. generated by moveDown.
1304 Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
1305 TODO 110417 get assumptions from ctxt !?
1307 fun pt_extract (pt, ([], Res)) =
1308 (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
1310 val (f, asm) = get_obj g_result pt []
1311 in (Form f, NONE, asm) end
1312 | pt_extract (pt,(p,Res)) =
1314 val (f, asm) = get_obj g_result pt p
1318 if is_pblobj' pt (lev_up p)
1321 val pI = case get_obj I pt (lev_up p) of
1322 PblObj{spec = (_, pI, _), ...} => pI
1323 | _ => error "pt_extract last_onlev: uncovered case get_obj"
1324 in if pI = e_pblID then NONE else SOME (Tac.Check_Postcond pI) end
1325 else SOME Tac.End_Trans (* WN0502 TODO for other branches *)
1327 let val p' = lev_on p
1332 val (dI ,pI) = case get_obj I pt p' of
1333 PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
1334 | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
1335 in SOME (Tac.Subproblem (dI, pI)) end
1337 if f = get_obj g_form pt p'
1338 then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1339 else SOME (Tac.Take (term2str (get_obj g_form pt p')))
1341 in (Form f, tac, asm) end
1342 | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
1344 val ppobj = get_obj I pt p
1345 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1346 val tac = g_tac ppobj
1347 in (f, SOME tac, []) end
1349 (** get the formula from a ctree-node:
1350 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1351 take res from all other PrfObj's
1352 Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
1353 fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
1354 [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
1355 | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
1356 [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
1357 | formres _ _ = error "formres: uncovered definition"
1358 fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
1359 [("stepform", (p, Res), r)]
1360 | form _ _ = error "form: uncovered definition"
1362 (* assumes to take whole level, in particular hd -- for use in interSteps *)
1363 fun get_formress fs _ [] = flat fs
1364 | get_formress fs p (nd::nds) =
1365 (* start with 'form+res' and continue with trying 'res' only*)
1366 get_forms (fs @ [formres p nd]) (lev_on p) nds
1367 and get_forms fs _ [] = flat fs
1368 | get_forms fs p (nd::nds) =
1370 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1371 then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1372 then get_forms (fs @ [formres p nd]) (lev_on p) nds
1373 (* continue with trying 'res' only*)
1374 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1376 (** get an 'interval' 'from' 'to' of formulae from a ctree **)
1377 (* WN0401 this functionality belongs to ctree.sml *)
1378 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
1379 | eq_pos' (p1, Res) (p2, Res) = p1 = p2
1380 | eq_pos' (p1, Pbl) (p2, p2_) =
1381 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1382 | eq_pos' (p1, Met) (p2, p2_) =
1383 p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1384 | eq_pos' _ _ = false;
1386 (* get an 'interval' from the ctree; 'interval' is w.r.t. the
1387 total ordering Position#compareTo(Position p) in the java-code
1388 val get_interval = fn
1389 : pos' -> : from is "move_up 1st-element" to return
1390 pos' -> : to the last element to be returned; from < to
1391 int -> : level: 0 gets the flattest sub-tree possible
1392 >999 gets the deepest sub-tree possible
1394 (pos' * : of the formula
1395 Term.term) : the formula
1397 fun get_interval from to level pt =
1399 fun get_inter c (from : pos') (to : pos') lev pt =
1400 if eq_pos' from to orelse from = ([], Res)
1402 let val (f, _, _) = pt_extract (pt, from)
1404 ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)]
1405 | Form t => c @ [(from, t)]
1408 if lev < lev_of from
1409 then (get_inter c (move_dn [] pt from) to lev pt)
1410 handle (PTREE _(*from move_dn too far*)) => c
1413 val (f, _, _) = pt_extract (pt, from)
1414 val term = case f of
1415 ModSpec (_,_,headline,_,_,_) => headline
1417 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1418 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1420 in get_inter [] from to level pt end
1422 fun posterm2str (pos, t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"
1423 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
1425 (* WN050225 omits the last step, if pt is incomplete *)
1426 fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
1428 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
1429 fun get_ocalhd (pt, (p, Pbl) : pos') =
1431 val (ospec, hdf', spec, probl) = case get_obj I pt p of
1432 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1433 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1434 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
1435 val pre = Stool.check_preconds (assoc_thy"Isac") prls where_ probl
1437 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1439 | get_ocalhd (pt, (p, Met)) =
1441 val (ospec, hdf', spec, meth) = case get_obj I pt p of
1442 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1443 | _ => error "get_ocalhd Met: uncovered case get_obj"
1444 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
1445 val pre = Stool.check_preconds (assoc_thy"Isac") prls pre meth
1447 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1449 | get_ocalhd _ = error "get_ocalhd: uncovered definition"
1451 (* at the activeFormula set the Model, the Guard and the Specification
1452 to empty and return a CalcHead;
1453 the 'origin' remains (for reconstructing all that) *)
1454 fun reset_calchead (pt, (p,_) : pos') =
1456 val () = case get_obj I pt p of
1458 | _ => error "reset_calchead: uncovered case get_obj"
1459 val pt = update_pbl pt p []
1460 val pt = update_met pt p []
1461 val pt = update_spec pt p e_spec
1462 in (pt, (p, Pbl) : pos') end